:: Inverse Trigonometric Functions Arcsin and Arccos
:: by Artur Korni{\l}owicz and Yasunari Shidama
::
:: Received September 25, 2004
:: Copyright (c) 2004 Association of Mizar Users
theorem Th1: :: SIN_COS6:1
theorem Th2: :: SIN_COS6:2
theorem Th3: :: SIN_COS6:3
theorem Th4: :: SIN_COS6:4
theorem Th5: :: SIN_COS6:5
theorem Th6: :: SIN_COS6:6
deffunc H1( Integer) -> Element of REAL = (2 * PI ) * $1;
Lm1:
dom sin = REAL
by SIN_COS:27;
Lm2:
dom cos = REAL
by SIN_COS:27;
Lm3:
[.((- (PI / 2)) + H1( 0 )),((PI / 2) + H1( 0 )).] = [.(- (PI / 2)),(PI / 2).]
;
Lm4:
[.((PI / 2) + H1( 0 )),(((3 / 2) * PI ) + H1( 0 )).] = [.(PI / 2),((3 / 2) * PI ).]
;
Lm5:
[.H1( 0 ),(PI + H1( 0 )).] = [.0 ,PI .]
;
Lm6:
[.(PI + H1( 0 )),((2 * PI ) + H1( 0 )).] = [.PI ,(2 * PI ).]
;
Lm7:
for r, s being real number st (r ^2 ) + (s ^2 ) = 1 holds
( - 1 <= r & r <= 1 )
Lm9:
PI / 2 < PI / 1
by XREAL_1:78;
Lm10:
1 * PI < (3 / 2) * PI
by XREAL_1:70;
Lm11:
0 + H1(1) < (PI / 2) + H1(1)
by XREAL_1:8;
Lm12:
(3 / 2) * PI < 2 * PI
by XREAL_1:70;
Lm13:
1 * PI < 2 * PI
by XREAL_1:70;
Lm14:
].(- 1),1.[ c= [.(- 1),1.]
by XXREAL_1:25;
Lm15:
].(- (PI / 2)),0 .[ c= [.(- (PI / 2)),0 .]
by XXREAL_1:25;
Lm16:
].(- (PI / 2)),(PI / 2).[ c= [.(- (PI / 2)),(PI / 2).]
by XXREAL_1:25;
Lm17:
].0 ,(PI / 2).[ c= [.0 ,(PI / 2).]
by XXREAL_1:25;
Lm18:
].0 ,PI .[ c= [.0 ,PI .]
by XXREAL_1:25;
Lm19:
].(PI / 2),PI .[ c= [.(PI / 2),PI .]
by XXREAL_1:25;
Lm20:
].(PI / 2),((3 / 2) * PI ).[ c= [.(PI / 2),((3 / 2) * PI ).]
by XXREAL_1:25;
Lm21:
].PI ,((3 / 2) * PI ).[ c= [.PI ,((3 / 2) * PI ).]
by XXREAL_1:25;
Lm22:
].PI ,(2 * PI ).[ c= [.PI ,(2 * PI ).]
by XXREAL_1:25;
Lm23:
].((3 / 2) * PI ),(2 * PI ).[ c= [.((3 / 2) * PI ),(2 * PI ).]
by XXREAL_1:25;
theorem Th7: :: SIN_COS6:7
theorem Th8: :: SIN_COS6:8
theorem Th9: :: SIN_COS6:9
theorem Th10: :: SIN_COS6:10
theorem Th11: :: SIN_COS6:11
theorem Th12: :: SIN_COS6:12
theorem Th13: :: SIN_COS6:13
theorem Th14: :: SIN_COS6:14
theorem Th15: :: SIN_COS6:15
theorem :: SIN_COS6:16
theorem :: SIN_COS6:17
theorem :: SIN_COS6:18
theorem :: SIN_COS6:19
theorem :: SIN_COS6:20
theorem Th21: :: SIN_COS6:21
theorem Th22: :: SIN_COS6:22
theorem Th23: :: SIN_COS6:23
theorem Th24: :: SIN_COS6:24
theorem Th25: :: SIN_COS6:25
theorem Th26: :: SIN_COS6:26
theorem Th27: :: SIN_COS6:27
theorem Th28: :: SIN_COS6:28
theorem Th29: :: SIN_COS6:29
theorem Th30: :: SIN_COS6:30
theorem Th31: :: SIN_COS6:31
theorem Th32: :: SIN_COS6:32
theorem Th33: :: SIN_COS6:33
theorem Th34: :: SIN_COS6:34
theorem Th35: :: SIN_COS6:35
theorem Th36: :: SIN_COS6:36
theorem :: SIN_COS6:37
theorem :: SIN_COS6:38
theorem :: SIN_COS6:39
theorem :: SIN_COS6:40
theorem :: SIN_COS6:41
theorem :: SIN_COS6:42
theorem :: SIN_COS6:43
theorem :: SIN_COS6:44
theorem Th45: :: SIN_COS6:45
theorem Th46: :: SIN_COS6:46
theorem :: SIN_COS6:47
theorem :: SIN_COS6:48
theorem Th49: :: SIN_COS6:49
theorem Th50: :: SIN_COS6:50
theorem :: SIN_COS6:51
theorem :: SIN_COS6:52
Lm24:
now
let i be
integer number ;
:: thesis: for r, p1, p2 being real number st r in [.(p1 + H1(i)),(p2 + H1(i)).] holds
r + (2 * PI ) in [.(p1 + H1(i + 1)),(p2 + H1(i + 1)).]let r be
real number ;
:: thesis: for p1, p2 being real number st r in [.(p1 + H1(i)),(p2 + H1(i)).] holds
r + (2 * PI ) in [.(p1 + H1(i + 1)),(p2 + H1(i + 1)).]let p1,
p2 be
real number ;
:: thesis: ( r in [.(p1 + H1(i)),(p2 + H1(i)).] implies r + (2 * PI ) in [.(p1 + H1(i + 1)),(p2 + H1(i + 1)).] )assume
r in [.(p1 + H1(i)),(p2 + H1(i)).]
;
:: thesis: r + (2 * PI ) in [.(p1 + H1(i + 1)),(p2 + H1(i + 1)).]then
(
p1 + H1(
i)
<= r &
r <= p2 + H1(
i) )
by XXREAL_1:1;
then
(
(p1 + H1(i)) + (2 * PI ) <= r + (2 * PI ) &
r + (2 * PI ) <= (p2 + H1(i)) + (2 * PI ) )
by XREAL_1:8;
hence
r + (2 * PI ) in [.(p1 + H1(i + 1)),(p2 + H1(i + 1)).]
by XXREAL_1:1;
:: thesis: verum
end;
Lm25:
now
let i be
integer number ;
:: thesis: for r, p1, p2 being real number st r in [.(p1 + H1(i)),(p2 + H1(i)).] /\ REAL holds
r + (2 * PI ) in [.(p1 + H1(i + 1)),(p2 + H1(i + 1)).] /\ REAL let r be
real number ;
:: thesis: for p1, p2 being real number st r in [.(p1 + H1(i)),(p2 + H1(i)).] /\ REAL holds
r + (2 * PI ) in [.(p1 + H1(i + 1)),(p2 + H1(i + 1)).] /\ REAL let p1,
p2 be
real number ;
:: thesis: ( r in [.(p1 + H1(i)),(p2 + H1(i)).] /\ REAL implies r + (2 * PI ) in [.(p1 + H1(i + 1)),(p2 + H1(i + 1)).] /\ REAL )assume
r in [.(p1 + H1(i)),(p2 + H1(i)).] /\ REAL
;
:: thesis: r + (2 * PI ) in [.(p1 + H1(i + 1)),(p2 + H1(i + 1)).] /\ REAL then
(
r in [.(p1 + H1(i)),(p2 + H1(i)).] &
r in REAL )
by XBOOLE_0:def 4;
then
(
r + (2 * PI ) in [.(p1 + H1(i + 1)),(p2 + H1(i + 1)).] &
r + (2 * PI ) in REAL )
by Lm24;
hence
r + (2 * PI ) in [.(p1 + H1(i + 1)),(p2 + H1(i + 1)).] /\ REAL
by XBOOLE_0:def 4;
:: thesis: verum
end;
Lm26:
now
let i be
integer number ;
:: thesis: for r, p1, p2 being real number st r in [.(p1 + H1(i)),(p2 + H1(i)).] holds
r - (2 * PI ) in [.(p1 + H1(i - 1)),(p2 + H1(i - 1)).]let r be
real number ;
:: thesis: for p1, p2 being real number st r in [.(p1 + H1(i)),(p2 + H1(i)).] holds
r - (2 * PI ) in [.(p1 + H1(i - 1)),(p2 + H1(i - 1)).]let p1,
p2 be
real number ;
:: thesis: ( r in [.(p1 + H1(i)),(p2 + H1(i)).] implies r - (2 * PI ) in [.(p1 + H1(i - 1)),(p2 + H1(i - 1)).] )assume
r in [.(p1 + H1(i)),(p2 + H1(i)).]
;
:: thesis: r - (2 * PI ) in [.(p1 + H1(i - 1)),(p2 + H1(i - 1)).]then
(
p1 + H1(
i)
<= r &
r <= p2 + H1(
i) )
by XXREAL_1:1;
then
(
(p1 + H1(i)) - (2 * PI ) <= r - (2 * PI ) &
r - (2 * PI ) <= (p2 + H1(i)) - (2 * PI ) )
by XREAL_1:11;
hence
r - (2 * PI ) in [.(p1 + H1(i - 1)),(p2 + H1(i - 1)).]
by XXREAL_1:1;
:: thesis: verum
end;
Lm27:
now
let i be
integer number ;
:: thesis: for r, p1, p2 being real number st r in [.(p1 + H1(i)),(p2 + H1(i)).] /\ REAL holds
r - (2 * PI ) in [.(p1 + H1(i - 1)),(p2 + H1(i - 1)).] /\ REAL let r be
real number ;
:: thesis: for p1, p2 being real number st r in [.(p1 + H1(i)),(p2 + H1(i)).] /\ REAL holds
r - (2 * PI ) in [.(p1 + H1(i - 1)),(p2 + H1(i - 1)).] /\ REAL let p1,
p2 be
real number ;
:: thesis: ( r in [.(p1 + H1(i)),(p2 + H1(i)).] /\ REAL implies r - (2 * PI ) in [.(p1 + H1(i - 1)),(p2 + H1(i - 1)).] /\ REAL )assume
r in [.(p1 + H1(i)),(p2 + H1(i)).] /\ REAL
;
:: thesis: r - (2 * PI ) in [.(p1 + H1(i - 1)),(p2 + H1(i - 1)).] /\ REAL then
(
r in [.(p1 + H1(i)),(p2 + H1(i)).] &
r in REAL )
by XBOOLE_0:def 4;
then
(
r - (2 * PI ) in [.(p1 + H1(i - 1)),(p2 + H1(i - 1)).] &
r - (2 * PI ) in REAL )
by Lm26;
hence
r - (2 * PI ) in [.(p1 + H1(i - 1)),(p2 + H1(i - 1)).] /\ REAL
by XBOOLE_0:def 4;
:: thesis: verum
end;
theorem Th53: :: SIN_COS6:53
theorem Th54: :: SIN_COS6:54
theorem Th55: :: SIN_COS6:55
theorem Th56: :: SIN_COS6:56
theorem Th57: :: SIN_COS6:57
theorem Th58: :: SIN_COS6:58
registration
cluster sin | [.(- (PI / 2)),0 .] -> one-to-one ;
coherence
sin | [.(- (PI / 2)),0 .] is one-to-one
cluster sin | [.0 ,(PI / 2).] -> one-to-one ;
coherence
sin | [.0 ,(PI / 2).] is one-to-one
cluster sin | [.(PI / 2),PI .] -> one-to-one ;
coherence
sin | [.(PI / 2),PI .] is one-to-one
cluster sin | [.PI ,((3 / 2) * PI ).] -> one-to-one ;
coherence
sin | [.PI ,((3 / 2) * PI ).] is one-to-one
cluster sin | [.((3 / 2) * PI ),(2 * PI ).] -> one-to-one ;
coherence
sin | [.((3 / 2) * PI ),(2 * PI ).] is one-to-one
end;
registration
cluster sin | ].(- (PI / 2)),(PI / 2).[ -> one-to-one ;
coherence
sin | ].(- (PI / 2)),(PI / 2).[ is one-to-one
cluster sin | ].(PI / 2),((3 / 2) * PI ).[ -> one-to-one ;
coherence
sin | ].(PI / 2),((3 / 2) * PI ).[ is one-to-one
cluster sin | ].(- (PI / 2)),0 .[ -> one-to-one ;
coherence
sin | ].(- (PI / 2)),0 .[ is one-to-one
cluster sin | ].0 ,(PI / 2).[ -> one-to-one ;
coherence
sin | ].0 ,(PI / 2).[ is one-to-one
cluster sin | ].(PI / 2),PI .[ -> one-to-one ;
coherence
sin | ].(PI / 2),PI .[ is one-to-one
cluster sin | ].PI ,((3 / 2) * PI ).[ -> one-to-one ;
coherence
sin | ].PI ,((3 / 2) * PI ).[ is one-to-one
cluster sin | ].((3 / 2) * PI ),(2 * PI ).[ -> one-to-one ;
coherence
sin | ].((3 / 2) * PI ),(2 * PI ).[ is one-to-one
end;
theorem Th59: :: SIN_COS6:59
theorem Th60: :: SIN_COS6:60
registration
cluster cos | ].0 ,PI .[ -> one-to-one ;
coherence
cos | ].0 ,PI .[ is one-to-one
cluster cos | ].PI ,(2 * PI ).[ -> one-to-one ;
coherence
cos | ].PI ,(2 * PI ).[ is one-to-one
cluster cos | ].0 ,(PI / 2).[ -> one-to-one ;
coherence
cos | ].0 ,(PI / 2).[ is one-to-one
cluster cos | ].(PI / 2),PI .[ -> one-to-one ;
coherence
cos | ].(PI / 2),PI .[ is one-to-one
cluster cos | ].PI ,((3 / 2) * PI ).[ -> one-to-one ;
coherence
cos | ].PI ,((3 / 2) * PI ).[ is one-to-one
cluster cos | ].((3 / 2) * PI ),(2 * PI ).[ -> one-to-one ;
coherence
cos | ].((3 / 2) * PI ),(2 * PI ).[ is one-to-one
end;
theorem :: SIN_COS6:61
:: deftheorem defines arcsin SIN_COS6:def 1 :
:: deftheorem defines arcsin SIN_COS6:def 2 :
Lm28:
arcsin " = sin | [.(- (PI / 2)),(PI / 2).]
by FUNCT_1:65;
theorem :: SIN_COS6:62
canceled;
theorem Th63: :: SIN_COS6:63
theorem Th64: :: SIN_COS6:64
theorem Th65: :: SIN_COS6:65
theorem :: SIN_COS6:66
theorem Th67: :: SIN_COS6:67
theorem :: SIN_COS6:68
theorem Th69: :: SIN_COS6:69
theorem Th70: :: SIN_COS6:70
theorem :: SIN_COS6:71
theorem :: SIN_COS6:72
theorem :: SIN_COS6:73
theorem :: SIN_COS6:74
theorem :: SIN_COS6:75
theorem :: SIN_COS6:76
theorem Th77: :: SIN_COS6:77
theorem Th78: :: SIN_COS6:78
theorem Th79: :: SIN_COS6:79
theorem Th80: :: SIN_COS6:80
theorem :: SIN_COS6:81
theorem Th82: :: SIN_COS6:82
theorem :: SIN_COS6:83
theorem :: SIN_COS6:84
theorem :: SIN_COS6:85
:: deftheorem defines arccos SIN_COS6:def 3 :
:: deftheorem defines arccos SIN_COS6:def 4 :
Lm29:
arccos " = cos | [.0 ,PI .]
by FUNCT_1:65;
theorem :: SIN_COS6:86
canceled;
theorem Th87: :: SIN_COS6:87
theorem Th88: :: SIN_COS6:88
theorem Th89: :: SIN_COS6:89
theorem :: SIN_COS6:90
theorem Th91: :: SIN_COS6:91
theorem :: SIN_COS6:92
theorem Th93: :: SIN_COS6:93
theorem Th94: :: SIN_COS6:94
theorem :: SIN_COS6:95
theorem :: SIN_COS6:96
theorem :: SIN_COS6:97
theorem :: SIN_COS6:98
theorem :: SIN_COS6:99
theorem :: SIN_COS6:100
theorem Th101: :: SIN_COS6:101
theorem Th102: :: SIN_COS6:102
theorem Th103: :: SIN_COS6:103
theorem Th104: :: SIN_COS6:104
theorem :: SIN_COS6:105
theorem Th106: :: SIN_COS6:106
theorem :: SIN_COS6:107
theorem :: SIN_COS6:108
theorem :: SIN_COS6:109
theorem Th110: :: SIN_COS6:110
theorem :: SIN_COS6:111
theorem :: SIN_COS6:112