:: Inverse Trigonometric Functions Arcsec1, Arcsec2, Arccosec1 and Arccosec2
:: by Bing Xie , Xiquan Liang and Fuguo Ge
::
:: Received March 18, 2008
:: Copyright (c) 2008 Association of Mizar Users
Lm1:
[.0 ,(PI / 2).[ c= ].(- (PI / 2)),(PI / 2).[
theorem Th1: :: SINCOS10:1
Lm2:
].(PI / 2),PI .] c= ].(PI / 2),((3 / 2) * PI ).[
theorem Th2: :: SINCOS10:2
Lm3:
[.(- (PI / 2)),0 .[ c= ].(- PI ),0 .[
theorem Th3: :: SINCOS10:3
Lm4:
].0 ,(PI / 2).] c= ].0 ,PI .[
theorem Th4: :: SINCOS10:4
theorem Th5: :: SINCOS10:5
theorem Th6: :: SINCOS10:6
theorem Th7: :: SINCOS10:7
theorem Th8: :: SINCOS10:8
theorem :: SINCOS10:9
theorem :: SINCOS10:10
theorem :: SINCOS10:11
theorem :: SINCOS10:12
Lm9:
( 0 in [.0 ,(PI / 2).[ & PI / 4 in [.0 ,(PI / 2).[ )
Lm10:
( (3 / 4) * PI in ].(PI / 2),PI .] & PI in ].(PI / 2),PI .] )
Lm11:
( - (PI / 2) in [.(- (PI / 2)),0 .[ & - (PI / 4) in [.(- (PI / 2)),0 .[ )
Lm12:
( PI / 4 in ].0 ,(PI / 2).] & PI / 2 in ].0 ,(PI / 2).] )
Y1:
].0 ,(PI / 2).[ c= [.0 ,(PI / 2).[
by XXREAL_1:22;
then X1:
].0 ,(PI / 2).[ c= dom sec
by Th1, XBOOLE_1:1;
Y2:
].(PI / 2),PI .[ c= ].(PI / 2),PI .]
by XXREAL_1:21;
then X2:
].(PI / 2),PI .[ c= dom sec
by Th2, XBOOLE_1:1;
[.0 ,(PI / 4).] c= [.0 ,(PI / 2).[
by Lm9, XXREAL_2:def 12;
then X5:
[.0 ,(PI / 4).] c= dom sec
by Th1, XBOOLE_1:1;
[.((3 / 4) * PI ),PI .] c= ].(PI / 2),PI .]
by Lm10, XXREAL_2:def 12;
then X6:
[.((3 / 4) * PI ),PI .] c= dom sec
by Th2, XBOOLE_1:1;
Y3:
].(- (PI / 2)),0 .[ c= [.(- (PI / 2)),0 .[
by XXREAL_1:22;
then X3:
].(- (PI / 2)),0 .[ c= dom cosec
by Th3, XBOOLE_1:1;
Y4:
].0 ,(PI / 2).[ c= ].0 ,(PI / 2).]
by XXREAL_1:21;
then X4:
].0 ,(PI / 2).[ c= dom cosec
by Th4, XBOOLE_1:1;
[.(- (PI / 2)),(- (PI / 4)).] c= [.(- (PI / 2)),0 .[
by Lm11, XXREAL_2:def 12;
then X7:
[.(- (PI / 2)),(- (PI / 4)).] c= dom cosec
by Th3, XBOOLE_1:1;
[.(PI / 4),(PI / 2).] c= ].0 ,(PI / 2).]
by Lm12, XXREAL_2:def 12;
then X8:
[.(PI / 4),(PI / 2).] c= dom cosec
by Th4, XBOOLE_1:1;
].0 ,(PI / 2).[ = dom (sec | ].0 ,(PI / 2).[)
by X1, RELAT_1:91;
then X15:
].0 ,(PI / 2).[ c= dom ((sec | [.0 ,(PI / 2).[) | ].0 ,(PI / 2).[)
by Y1, RELAT_1:103;
].(PI / 2),PI .[ = dom (sec | ].(PI / 2),PI .[)
by X2, RELAT_1:91;
then X16:
].(PI / 2),PI .[ c= dom ((sec | ].(PI / 2),PI .]) | ].(PI / 2),PI .[)
by Y2, RELAT_1:103;
].(- (PI / 2)),0 .[ = dom (cosec | ].(- (PI / 2)),0 .[)
by X3, RELAT_1:91;
then X17:
].(- (PI / 2)),0 .[ c= dom ((cosec | [.(- (PI / 2)),0 .[) | ].(- (PI / 2)),0 .[)
by Y3, RELAT_1:103;
].0 ,(PI / 2).[ = dom (cosec | ].0 ,(PI / 2).[)
by X4, RELAT_1:91;
then X18:
].0 ,(PI / 2).[ c= dom ((cosec | ].0 ,(PI / 2).]) | ].0 ,(PI / 2).[)
by Y4, RELAT_1:103;
theorem Th13: :: SINCOS10:13
theorem Th14: :: SINCOS10:14
theorem Th15: :: SINCOS10:15
theorem Th16: :: SINCOS10:16
theorem Th17: :: SINCOS10:17
theorem Th18: :: SINCOS10:18
theorem Th19: :: SINCOS10:19
theorem Th20: :: SINCOS10:20
theorem :: SINCOS10:21
theorem :: SINCOS10:22
theorem :: SINCOS10:23
theorem :: SINCOS10:24
registration
cluster K7(
sec ,
[.0 ,(PI / 2).[)
-> one-to-one ;
coherence
sec | [.0 ,(PI / 2).[ is one-to-one
by Th17, FCONT_3:16;
cluster K7(
sec ,
].(PI / 2),PI .])
-> one-to-one ;
coherence
sec | ].(PI / 2),PI .] is one-to-one
by Th18, FCONT_3:16;
cluster K7(
cosec ,
[.(- (PI / 2)),0 .[)
-> one-to-one ;
coherence
cosec | [.(- (PI / 2)),0 .[ is one-to-one
by Th19, FCONT_3:16;
cluster K7(
cosec ,
].0 ,(PI / 2).])
-> one-to-one ;
coherence
cosec | ].0 ,(PI / 2).] is one-to-one
by Th20, FCONT_3:16;
end;
definition
func arcsec1 -> PartFunc of
REAL ,
REAL equals :: SINCOS10:def 1
(sec | [.0 ,(PI / 2).[) " ;
coherence
(sec | [.0 ,(PI / 2).[) " is PartFunc of REAL , REAL
;
func arcsec2 -> PartFunc of
REAL ,
REAL equals :: SINCOS10:def 2
(sec | ].(PI / 2),PI .]) " ;
coherence
(sec | ].(PI / 2),PI .]) " is PartFunc of REAL , REAL
;
func arccosec1 -> PartFunc of
REAL ,
REAL equals :: SINCOS10:def 3
(cosec | [.(- (PI / 2)),0 .[) " ;
coherence
(cosec | [.(- (PI / 2)),0 .[) " is PartFunc of REAL , REAL
;
func arccosec2 -> PartFunc of
REAL ,
REAL equals :: SINCOS10:def 4
(cosec | ].0 ,(PI / 2).]) " ;
coherence
(cosec | ].0 ,(PI / 2).]) " is PartFunc of REAL , REAL
;
end;
:: deftheorem defines arcsec1 SINCOS10:def 1 :
:: deftheorem defines arcsec2 SINCOS10:def 2 :
:: deftheorem defines arccosec1 SINCOS10:def 3 :
:: deftheorem defines arccosec2 SINCOS10:def 4 :
:: deftheorem defines arcsec1 SINCOS10:def 5 :
:: deftheorem defines arcsec2 SINCOS10:def 6 :
:: deftheorem defines arccosec1 SINCOS10:def 7 :
:: deftheorem defines arccosec2 SINCOS10:def 8 :
Lm5:
arcsec1 " = sec | [.0 ,(PI / 2).[
by FUNCT_1:65;
Lm6:
arcsec2 " = sec | ].(PI / 2),PI .]
by FUNCT_1:65;
Lm7:
arccosec1 " = cosec | [.(- (PI / 2)),0 .[
by FUNCT_1:65;
Lm8:
arccosec2 " = cosec | ].0 ,(PI / 2).]
by FUNCT_1:65;
theorem Th25: :: SINCOS10:25
theorem Th26: :: SINCOS10:26
theorem Th27: :: SINCOS10:27
theorem Th28: :: SINCOS10:28
theorem Th29: :: SINCOS10:29
theorem Th30: :: SINCOS10:30
theorem Th31: :: SINCOS10:31
theorem Th32: :: SINCOS10:32
theorem Th33: :: SINCOS10:33
theorem Th34: :: SINCOS10:34
theorem Th35: :: SINCOS10:35
theorem Th36: :: SINCOS10:36
Lm13:
dom (sec | [.0 ,(PI / 4).]) = [.0 ,(PI / 4).]
Lm14:
dom (sec | [.((3 / 4) * PI ),PI .]) = [.((3 / 4) * PI ),PI .]
Lm15:
dom (cosec | [.(- (PI / 2)),(- (PI / 4)).]) = [.(- (PI / 2)),(- (PI / 4)).]
Lm16:
dom (cosec | [.(PI / 4),(PI / 2).]) = [.(PI / 4),(PI / 2).]
Lm17:
( dom (sec | [.0 ,(PI / 2).[) = [.0 ,(PI / 2).[ & ( for th being real number st th in [.0 ,(PI / 2).[ holds
(sec | [.0 ,(PI / 2).[) . th = sec . th ) )
Lm18:
( dom (sec | ].(PI / 2),PI .]) = ].(PI / 2),PI .] & ( for th being real number st th in ].(PI / 2),PI .] holds
(sec | ].(PI / 2),PI .]) . th = sec . th ) )
Lm19:
( dom (cosec | [.(- (PI / 2)),0 .[) = [.(- (PI / 2)),0 .[ & ( for th being real number st th in [.(- (PI / 2)),0 .[ holds
(cosec | [.(- (PI / 2)),0 .[) . th = cosec . th ) )
Lm20:
( dom (cosec | ].0 ,(PI / 2).]) = ].0 ,(PI / 2).] & ( for th being real number st th in ].0 ,(PI / 2).] holds
(cosec | ].0 ,(PI / 2).]) . th = cosec . th ) )
theorem Th37: :: SINCOS10:37
theorem Th38: :: SINCOS10:38
theorem Th39: :: SINCOS10:39
theorem Th40: :: SINCOS10:40
theorem Th41: :: SINCOS10:41
theorem Th42: :: SINCOS10:42
theorem Th43: :: SINCOS10:43
theorem Th44: :: SINCOS10:44
theorem Th45: :: SINCOS10:45
theorem Th46: :: SINCOS10:46
theorem Th47: :: SINCOS10:47
theorem Th48: :: SINCOS10:48
Lm21:
(sec | [.0 ,(PI / 4).]) | [.0 ,(PI / 4).] is increasing
Lm22:
(sec | [.((3 / 4) * PI ),PI .]) | [.((3 / 4) * PI ),PI .] is increasing
Lm23:
(cosec | [.(- (PI / 2)),(- (PI / 4)).]) | [.(- (PI / 2)),(- (PI / 4)).] is decreasing
Lm24:
(cosec | [.(PI / 4),(PI / 2).]) | [.(PI / 4),(PI / 2).] is decreasing
Lm25:
sec | [.0 ,(PI / 4).] is one-to-one
Lm26:
sec | [.((3 / 4) * PI ),PI .] is one-to-one
Lm27:
cosec | [.(- (PI / 2)),(- (PI / 4)).] is one-to-one
Lm28:
cosec | [.(PI / 4),(PI / 2).] is one-to-one
registration
cluster K7(
sec ,
[.0 ,(PI / 4).])
-> one-to-one ;
coherence
sec | [.0 ,(PI / 4).] is one-to-one
by Lm25;
cluster K7(
sec ,
[.((3 / 4) * PI ),PI .])
-> one-to-one ;
coherence
sec | [.((3 / 4) * PI ),PI .] is one-to-one
by Lm26;
cluster K7(
cosec ,
[.(- (PI / 2)),(- (PI / 4)).])
-> one-to-one ;
coherence
cosec | [.(- (PI / 2)),(- (PI / 4)).] is one-to-one
by Lm27;
cluster K7(
cosec ,
[.(PI / 4),(PI / 2).])
-> one-to-one ;
coherence
cosec | [.(PI / 4),(PI / 2).] is one-to-one
by Lm28;
end;
theorem Th49: :: SINCOS10:49
theorem Th50: :: SINCOS10:50
theorem Th51: :: SINCOS10:51
theorem Th52: :: SINCOS10:52
theorem :: SINCOS10:53
theorem :: SINCOS10:54
theorem :: SINCOS10:55
theorem :: SINCOS10:56
theorem :: SINCOS10:57
theorem :: SINCOS10:58
theorem :: SINCOS10:59
theorem :: SINCOS10:60
theorem :: SINCOS10:61
theorem :: SINCOS10:62
theorem :: SINCOS10:63
theorem :: SINCOS10:64
theorem Th65: :: SINCOS10:65
theorem Th66: :: SINCOS10:66
theorem Th67: :: SINCOS10:67
theorem Th68: :: SINCOS10:68
theorem Th69: :: SINCOS10:69
theorem Th70: :: SINCOS10:70
theorem Th71: :: SINCOS10:71
theorem Th72: :: SINCOS10:72
theorem Th73: :: SINCOS10:73
theorem Th74: :: SINCOS10:74
theorem Th75: :: SINCOS10:75
theorem Th76: :: SINCOS10:76
theorem Th77: :: SINCOS10:77
theorem Th78: :: SINCOS10:78
theorem Th79: :: SINCOS10:79
theorem Th80: :: SINCOS10:80
theorem Th81: :: SINCOS10:81
theorem Th82: :: SINCOS10:82
theorem Th83: :: SINCOS10:83
theorem Th84: :: SINCOS10:84
theorem Th85: :: SINCOS10:85
theorem Th86: :: SINCOS10:86
theorem Th87: :: SINCOS10:87
theorem Th88: :: SINCOS10:88
theorem Th89: :: SINCOS10:89
theorem Th90: :: SINCOS10:90
theorem Th91: :: SINCOS10:91
theorem Th92: :: SINCOS10:92
theorem Th93: :: SINCOS10:93
theorem Th94: :: SINCOS10:94
theorem Th95: :: SINCOS10:95
theorem Th96: :: SINCOS10:96
theorem Th97: :: SINCOS10:97
theorem Th98: :: SINCOS10:98
theorem Th99: :: SINCOS10:99
theorem Th100: :: SINCOS10:100
theorem :: SINCOS10:101
theorem :: SINCOS10:102
theorem :: SINCOS10:103
theorem :: SINCOS10:104
theorem Th105: :: SINCOS10:105
theorem Th106: :: SINCOS10:106
theorem Th107: :: SINCOS10:107
theorem Th108: :: SINCOS10:108
theorem Th109: :: SINCOS10:109
theorem Th110: :: SINCOS10:110
theorem Th111: :: SINCOS10:111
theorem Th112: :: SINCOS10:112
theorem Th113: :: SINCOS10:113
theorem Th114: :: SINCOS10:114
theorem Th115: :: SINCOS10:115
theorem Th116: :: SINCOS10:116
theorem :: SINCOS10:117
theorem :: SINCOS10:118
theorem :: SINCOS10:119
theorem :: SINCOS10:120
theorem Th121: :: SINCOS10:121
theorem Th122: :: SINCOS10:122
theorem Th123: :: SINCOS10:123
theorem Th124: :: SINCOS10:124
theorem :: SINCOS10:125
theorem :: SINCOS10:126
theorem :: SINCOS10:127
theorem :: SINCOS10:128
theorem :: SINCOS10:129
theorem :: SINCOS10:130
theorem :: SINCOS10:131
theorem :: SINCOS10:132