Proof of Theorem asinsin
Step | Hyp | Ref
| Expression |
1 | | sincl 14856 |
. . . 4
|
2 | 1 | adantr 481 |
. . 3
|
3 | | asinval 24609 |
. . 3
arcsin |
4 | 2, 3 | syl 17 |
. 2
arcsin |
5 | | ax-icn 9995 |
. . . . . . . 8
|
6 | | mulcl 10020 |
. . . . . . . 8
|
7 | 5, 2, 6 | sylancr 695 |
. . . . . . 7
|
8 | | simpl 473 |
. . . . . . . . 9
|
9 | | mulcl 10020 |
. . . . . . . . 9
|
10 | 5, 8, 9 | sylancr 695 |
. . . . . . . 8
|
11 | | efcl 14813 |
. . . . . . . 8
|
12 | 10, 11 | syl 17 |
. . . . . . 7
|
13 | 7, 12 | pncan3d 10395 |
. . . . . 6
|
14 | 12, 7 | subcld 10392 |
. . . . . . . 8
|
15 | | ax-1cn 9994 |
. . . . . . . . 9
|
16 | 2 | sqcld 13006 |
. . . . . . . . 9
|
17 | | subcl 10280 |
. . . . . . . . 9
|
18 | 15, 16, 17 | sylancr 695 |
. . . . . . . 8
|
19 | | binom2sub 12981 |
. . . . . . . . . 10
|
20 | 12, 7, 19 | syl2anc 693 |
. . . . . . . . 9
|
21 | 12 | sqvald 13005 |
. . . . . . . . . . . 12
|
22 | | 2cn 11091 |
. . . . . . . . . . . . . 14
|
23 | 22 | a1i 11 |
. . . . . . . . . . . . 13
|
24 | 23, 12, 7 | mul12d 10245 |
. . . . . . . . . . . 12
|
25 | 21, 24 | oveq12d 6668 |
. . . . . . . . . . 11
|
26 | | coscl 14857 |
. . . . . . . . . . . . . 14
|
27 | 26 | adantr 481 |
. . . . . . . . . . . . 13
|
28 | | subsq 12972 |
. . . . . . . . . . . . 13
|
29 | 27, 7, 28 | syl2anc 693 |
. . . . . . . . . . . 12
|
30 | | sqmul 12926 |
. . . . . . . . . . . . . . . 16
|
31 | 5, 2, 30 | sylancr 695 |
. . . . . . . . . . . . . . 15
|
32 | | i2 12965 |
. . . . . . . . . . . . . . . . 17
|
33 | 32 | oveq1i 6660 |
. . . . . . . . . . . . . . . 16
|
34 | 16 | mulm1d 10482 |
. . . . . . . . . . . . . . . 16
|
35 | 33, 34 | syl5eq 2668 |
. . . . . . . . . . . . . . 15
|
36 | 31, 35 | eqtrd 2656 |
. . . . . . . . . . . . . 14
|
37 | 36 | oveq2d 6666 |
. . . . . . . . . . . . 13
|
38 | 27 | sqcld 13006 |
. . . . . . . . . . . . . 14
|
39 | 38, 16 | subnegd 10399 |
. . . . . . . . . . . . 13
|
40 | 38, 16 | addcomd 10238 |
. . . . . . . . . . . . 13
|
41 | 37, 39, 40 | 3eqtrd 2660 |
. . . . . . . . . . . 12
|
42 | | efival 14882 |
. . . . . . . . . . . . . . 15
|
43 | 42 | adantr 481 |
. . . . . . . . . . . . . 14
|
44 | 7 | 2timesd 11275 |
. . . . . . . . . . . . . . . 16
|
45 | 43, 44 | oveq12d 6668 |
. . . . . . . . . . . . . . 15
|
46 | 27, 7, 7 | pnpcan2d 10430 |
. . . . . . . . . . . . . . 15
|
47 | 45, 46 | eqtrd 2656 |
. . . . . . . . . . . . . 14
|
48 | 43, 47 | oveq12d 6668 |
. . . . . . . . . . . . 13
|
49 | | mulcl 10020 |
. . . . . . . . . . . . . . 15
|
50 | 22, 7, 49 | sylancr 695 |
. . . . . . . . . . . . . 14
|
51 | 12, 12, 50 | subdid 10486 |
. . . . . . . . . . . . 13
|
52 | 48, 51 | eqtr3d 2658 |
. . . . . . . . . . . 12
|
53 | 29, 41, 52 | 3eqtr3d 2664 |
. . . . . . . . . . 11
|
54 | | sincossq 14906 |
. . . . . . . . . . . 12
|
55 | 54 | adantr 481 |
. . . . . . . . . . 11
|
56 | 25, 53, 55 | 3eqtr2d 2662 |
. . . . . . . . . 10
|
57 | 56, 36 | oveq12d 6668 |
. . . . . . . . 9
|
58 | | negsub 10329 |
. . . . . . . . . 10
|
59 | 15, 16, 58 | sylancr 695 |
. . . . . . . . 9
|
60 | 20, 57, 59 | 3eqtrd 2660 |
. . . . . . . 8
|
61 | | halfre 11246 |
. . . . . . . . . . . 12
|
62 | 61 | a1i 11 |
. . . . . . . . . . 11
|
63 | | negicn 10282 |
. . . . . . . . . . . . . . 15
|
64 | | mulcl 10020 |
. . . . . . . . . . . . . . 15
|
65 | 63, 8, 64 | sylancr 695 |
. . . . . . . . . . . . . 14
|
66 | | efcl 14813 |
. . . . . . . . . . . . . 14
|
67 | 65, 66 | syl 17 |
. . . . . . . . . . . . 13
|
68 | 12, 67 | addcld 10059 |
. . . . . . . . . . . 12
|
69 | 68 | recld 13934 |
. . . . . . . . . . 11
|
70 | | halfgt0 11248 |
. . . . . . . . . . . 12
|
71 | 70 | a1i 11 |
. . . . . . . . . . 11
|
72 | 12 | recld 13934 |
. . . . . . . . . . . . 13
|
73 | 67 | recld 13934 |
. . . . . . . . . . . . 13
|
74 | | asinsinlem 24618 |
. . . . . . . . . . . . 13
|
75 | | negcl 10281 |
. . . . . . . . . . . . . . . 16
|
76 | 75 | adantr 481 |
. . . . . . . . . . . . . . 15
|
77 | | reneg 13865 |
. . . . . . . . . . . . . . . . 17
|
78 | 77 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
79 | | recl 13850 |
. . . . . . . . . . . . . . . . . . 19
|
80 | | halfpire 24216 |
. . . . . . . . . . . . . . . . . . . . 21
|
81 | 80 | renegcli 10342 |
. . . . . . . . . . . . . . . . . . . 20
|
82 | | iooneg 12292 |
. . . . . . . . . . . . . . . . . . . 20
|
83 | 81, 80, 82 | mp3an12 1414 |
. . . . . . . . . . . . . . . . . . 19
|
84 | 79, 83 | syl 17 |
. . . . . . . . . . . . . . . . . 18
|
85 | 84 | biimpa 501 |
. . . . . . . . . . . . . . . . 17
|
86 | 80 | recni 10052 |
. . . . . . . . . . . . . . . . . . 19
|
87 | 86 | negnegi 10351 |
. . . . . . . . . . . . . . . . . 18
|
88 | 87 | oveq2i 6661 |
. . . . . . . . . . . . . . . . 17
|
89 | 85, 88 | syl6eleq 2711 |
. . . . . . . . . . . . . . . 16
|
90 | 78, 89 | eqeltrd 2701 |
. . . . . . . . . . . . . . 15
|
91 | | asinsinlem 24618 |
. . . . . . . . . . . . . . 15
|
92 | 76, 90, 91 | syl2anc 693 |
. . . . . . . . . . . . . 14
|
93 | | mulneg12 10468 |
. . . . . . . . . . . . . . . . 17
|
94 | 5, 8, 93 | sylancr 695 |
. . . . . . . . . . . . . . . 16
|
95 | 94 | fveq2d 6195 |
. . . . . . . . . . . . . . 15
|
96 | 95 | fveq2d 6195 |
. . . . . . . . . . . . . 14
|
97 | 92, 96 | breqtrrd 4681 |
. . . . . . . . . . . . 13
|
98 | 72, 73, 74, 97 | addgt0d 10602 |
. . . . . . . . . . . 12
|
99 | 12, 67 | readdd 13954 |
. . . . . . . . . . . 12
|
100 | 98, 99 | breqtrrd 4681 |
. . . . . . . . . . 11
|
101 | 62, 69, 71, 100 | mulgt0d 10192 |
. . . . . . . . . 10
|
102 | | cosval 14853 |
. . . . . . . . . . . . . 14
|
103 | 102 | adantr 481 |
. . . . . . . . . . . . 13
|
104 | | 2ne0 11113 |
. . . . . . . . . . . . . . 15
|
105 | 104 | a1i 11 |
. . . . . . . . . . . . . 14
|
106 | 68, 23, 105 | divrec2d 10805 |
. . . . . . . . . . . . 13
|
107 | 103, 106 | eqtrd 2656 |
. . . . . . . . . . . 12
|
108 | 107 | fveq2d 6195 |
. . . . . . . . . . 11
|
109 | | remul2 13870 |
. . . . . . . . . . . 12
|
110 | 61, 68, 109 | sylancr 695 |
. . . . . . . . . . 11
|
111 | 108, 110 | eqtrd 2656 |
. . . . . . . . . 10
|
112 | 101, 111 | breqtrrd 4681 |
. . . . . . . . 9
|
113 | 43 | oveq1d 6665 |
. . . . . . . . . . 11
|
114 | 27, 7 | pncand 10393 |
. . . . . . . . . . 11
|
115 | 113, 114 | eqtrd 2656 |
. . . . . . . . . 10
|
116 | 115 | fveq2d 6195 |
. . . . . . . . 9
|
117 | 112, 116 | breqtrrd 4681 |
. . . . . . . 8
|
118 | 14, 18, 60, 117 | eqsqrt2d 14108 |
. . . . . . 7
|
119 | 118 | oveq2d 6666 |
. . . . . 6
|
120 | 13, 119 | eqtr3d 2658 |
. . . . 5
|
121 | 120 | fveq2d 6195 |
. . . 4
|
122 | | pire 24210 |
. . . . . . . . . 10
|
123 | 122 | renegcli 10342 |
. . . . . . . . 9
|
124 | 123 | a1i 11 |
. . . . . . . 8
|
125 | 81 | a1i 11 |
. . . . . . . 8
|
126 | | elioore 12205 |
. . . . . . . . 9
|
127 | 126 | adantl 482 |
. . . . . . . 8
|
128 | | pirp 24213 |
. . . . . . . . . . 11
|
129 | | rphalflt 11860 |
. . . . . . . . . . 11
|
130 | 128, 129 | ax-mp 5 |
. . . . . . . . . 10
|
131 | 80, 122 | ltnegi 10572 |
. . . . . . . . . 10
|
132 | 130, 131 | mpbi 220 |
. . . . . . . . 9
|
133 | 132 | a1i 11 |
. . . . . . . 8
|
134 | | eliooord 12233 |
. . . . . . . . . 10
|
135 | 134 | adantl 482 |
. . . . . . . . 9
|
136 | 135 | simpld 475 |
. . . . . . . 8
|
137 | 124, 125,
127, 133, 136 | lttrd 10198 |
. . . . . . 7
|
138 | | imre 13848 |
. . . . . . . . 9
|
139 | 10, 138 | syl 17 |
. . . . . . . 8
|
140 | 5, 5 | mulneg1i 10476 |
. . . . . . . . . . . 12
|
141 | | ixi 10656 |
. . . . . . . . . . . . 13
|
142 | 141 | negeqi 10274 |
. . . . . . . . . . . 12
|
143 | 15 | negnegi 10351 |
. . . . . . . . . . . 12
|
144 | 140, 142,
143 | 3eqtri 2648 |
. . . . . . . . . . 11
|
145 | 144 | oveq1i 6660 |
. . . . . . . . . 10
|
146 | 63 | a1i 11 |
. . . . . . . . . . 11
|
147 | 5 | a1i 11 |
. . . . . . . . . . 11
|
148 | 146, 147,
8 | mulassd 10063 |
. . . . . . . . . 10
|
149 | | mulid2 10038 |
. . . . . . . . . . 11
|
150 | 149 | adantr 481 |
. . . . . . . . . 10
|
151 | 145, 148,
150 | 3eqtr3a 2680 |
. . . . . . . . 9
|
152 | 151 | fveq2d 6195 |
. . . . . . . 8
|
153 | 139, 152 | eqtrd 2656 |
. . . . . . 7
|
154 | 137, 153 | breqtrrd 4681 |
. . . . . 6
|
155 | 122 | a1i 11 |
. . . . . . . 8
|
156 | 80 | a1i 11 |
. . . . . . . . 9
|
157 | 135 | simprd 479 |
. . . . . . . . 9
|
158 | 130 | a1i 11 |
. . . . . . . . 9
|
159 | 127, 156,
155, 157, 158 | lttrd 10198 |
. . . . . . . 8
|
160 | 127, 155,
159 | ltled 10185 |
. . . . . . 7
|
161 | 153, 160 | eqbrtrd 4675 |
. . . . . 6
|
162 | | ellogrn 24306 |
. . . . . 6
|
163 | 10, 154, 161, 162 | syl3anbrc 1246 |
. . . . 5
|
164 | | logef 24328 |
. . . . 5
|
165 | 163, 164 | syl 17 |
. . . 4
|
166 | 121, 165 | eqtr3d 2658 |
. . 3
|
167 | 166 | oveq2d 6666 |
. 2
|
168 | 4, 167, 151 | 3eqtrd 2660 |
1
arcsin |