:: Inverse Trigonometric Functions Arctan and Arccot
:: by Xiquan Liang and Bing Xie
::
:: Received March 18, 2008
:: Copyright (c) 2008 Association of Mizar Users
theorem Th1: :: SIN_COS9:1
theorem Th2: :: SIN_COS9:2
Lm1:
tan is_differentiable_on ].(- (PI / 2)),(PI / 2).[
Lm2:
cot is_differentiable_on ].0 ,PI .[
Lm3:
for x being Real st x in ].(- (PI / 2)),(PI / 2).[ holds
diff tan ,x = 1 / ((cos . x) ^2 )
Lm4:
for x being Real st x in ].0 ,PI .[ holds
diff cot ,x = - (1 / ((sin . x) ^2 ))
theorem :: SIN_COS9:3
theorem :: SIN_COS9:4
theorem :: SIN_COS9:5
theorem :: SIN_COS9:6
theorem Th7: :: SIN_COS9:7
theorem Th8: :: SIN_COS9:8
theorem :: SIN_COS9:9
theorem :: SIN_COS9:10
:: deftheorem defines arctan SIN_COS9:def 1 :
:: deftheorem defines arccot SIN_COS9:def 2 :
:: deftheorem defines arctan SIN_COS9:def 3 :
:: deftheorem defines arccot SIN_COS9:def 4 :
Lm5:
arctan " = tan | ].(- (PI / 2)),(PI / 2).[
by FUNCT_1:65;
Lm6:
arccot " = cot | ].0 ,PI .[
by FUNCT_1:65;
theorem Th11: :: SIN_COS9:11
theorem Th12: :: SIN_COS9:12
Lm7:
- (PI / 4) in ].(- (PI / 2)),(PI / 2).[
Lm8:
PI / 4 in ].(- (PI / 2)),(PI / 2).[
Lm9:
PI / 4 in ].0 ,PI .[
Lm10:
(3 / 4) * PI in ].0 ,PI .[
Lm11:
dom (tan | [.(- (PI / 4)),(PI / 4).]) = [.(- (PI / 4)),(PI / 4).]
Lm12:
dom (cot | [.(PI / 4),((3 / 4) * PI ).]) = [.(PI / 4),((3 / 4) * PI ).]
theorem Th13: :: SIN_COS9:13
theorem Th14: :: SIN_COS9:14
theorem :: SIN_COS9:15
theorem :: SIN_COS9:16
theorem Th15: :: SIN_COS9:17
theorem Th16: :: SIN_COS9:18
theorem Th17: :: SIN_COS9:19
theorem Th18: :: SIN_COS9:20
theorem Th19: :: SIN_COS9:21
theorem Th20: :: SIN_COS9:22
theorem Th21: :: SIN_COS9:23
theorem Th22: :: SIN_COS9:24
Lm13:
(tan | [.(- (PI / 4)),(PI / 4).]) | [.(- (PI / 4)),(PI / 4).] is increasing
Lm14:
(cot | [.(PI / 4),((3 / 4) * PI ).]) | [.(PI / 4),((3 / 4) * PI ).] is decreasing
Lm15:
tan | [.(- (PI / 4)),(PI / 4).] is one-to-one
Lm16:
cot | [.(PI / 4),((3 / 4) * PI ).] is one-to-one
theorem Th23: :: SIN_COS9:25
theorem Th24: :: SIN_COS9:26
theorem :: SIN_COS9:27
theorem :: SIN_COS9:28
theorem :: SIN_COS9:29
theorem :: SIN_COS9:30
theorem Th29: :: SIN_COS9:31
theorem Th30: :: SIN_COS9:32
theorem :: SIN_COS9:33
theorem :: SIN_COS9:34
theorem Th33: :: SIN_COS9:35
theorem Th34: :: SIN_COS9:36
theorem Th35: :: SIN_COS9:37
theorem Th36: :: SIN_COS9:38
theorem Th37: :: SIN_COS9:39
theorem Th38: :: SIN_COS9:40
theorem Th39: :: SIN_COS9:41
theorem Th40: :: SIN_COS9:42
theorem :: SIN_COS9:43
theorem :: SIN_COS9:44
theorem Th43: :: SIN_COS9:45
theorem Th44: :: SIN_COS9:46
theorem Th45: :: SIN_COS9:47
theorem Th46: :: SIN_COS9:48
theorem Th47: :: SIN_COS9:49
theorem Th48: :: SIN_COS9:50
theorem Th49: :: SIN_COS9:51
theorem Th50: :: SIN_COS9:52
theorem Th51: :: SIN_COS9:53
theorem Th52: :: SIN_COS9:54
theorem Th53: :: SIN_COS9:55
theorem Th54: :: SIN_COS9:56
theorem :: SIN_COS9:57
theorem :: SIN_COS9:58
theorem :: SIN_COS9:59
theorem :: SIN_COS9:60
theorem :: SIN_COS9:61
theorem :: SIN_COS9:62
theorem Th61: :: SIN_COS9:63
theorem Th62: :: SIN_COS9:64
theorem :: SIN_COS9:65
theorem :: SIN_COS9:66
theorem :: SIN_COS9:67
theorem :: SIN_COS9:68
theorem :: SIN_COS9:69
theorem :: SIN_COS9:70
theorem Th69: :: SIN_COS9:71
theorem Th70: :: SIN_COS9:72
theorem Th71: :: SIN_COS9:73
theorem Th72: :: SIN_COS9:74
theorem Th73: :: SIN_COS9:75
theorem Th74: :: SIN_COS9:76
theorem :: SIN_COS9:77
theorem :: SIN_COS9:78
theorem :: SIN_COS9:79
theorem :: SIN_COS9:80
theorem Th79: :: SIN_COS9:81
theorem Th80: :: SIN_COS9:82
theorem :: SIN_COS9:83
theorem :: SIN_COS9:84
theorem Th83: :: SIN_COS9:85
theorem Th84: :: SIN_COS9:86
theorem Th85: :: SIN_COS9:87
theorem Th86: :: SIN_COS9:88
theorem :: SIN_COS9:89
theorem :: SIN_COS9:90
theorem Th89: :: SIN_COS9:91
theorem Th90: :: SIN_COS9:92
theorem :: SIN_COS9:93
theorem :: SIN_COS9:94
theorem Th93: :: SIN_COS9:95
theorem Th94: :: SIN_COS9:96
theorem :: SIN_COS9:97
theorem :: SIN_COS9:98
theorem :: SIN_COS9:99
theorem :: SIN_COS9:100
theorem Th99: :: SIN_COS9:101
theorem Th100: :: SIN_COS9:102
theorem :: SIN_COS9:103
theorem :: SIN_COS9:104
theorem Th103: :: SIN_COS9:105
theorem Th104: :: SIN_COS9:106
theorem Th105: :: SIN_COS9:107
theorem Th106: :: SIN_COS9:108
theorem :: SIN_COS9:109
theorem :: SIN_COS9:110
theorem :: SIN_COS9:111
theorem :: SIN_COS9:112
theorem :: SIN_COS9:113
theorem :: SIN_COS9:114
theorem :: SIN_COS9:115
theorem :: SIN_COS9:116
theorem :: SIN_COS9:117
theorem :: SIN_COS9:118
theorem :: SIN_COS9:119
theorem :: SIN_COS9:120
theorem :: SIN_COS9:121
theorem :: SIN_COS9:122
theorem :: SIN_COS9:123
theorem :: SIN_COS9:124
theorem :: SIN_COS9:125
theorem :: SIN_COS9:126
theorem :: SIN_COS9:127
theorem :: SIN_COS9:128
theorem :: SIN_COS9:129
theorem :: SIN_COS9:130