Step | Hyp | Ref
| Expression |
1 | | reelprrecn 9649 |
. . . 4
    |
2 | 1 | a1i 11 |
. . 3

     |
3 | | elioore 11691 |
. . . . . . . 8
        |
4 | 3 | recnd 9687 |
. . . . . . 7
        |
5 | 4 | adantl 473 |
. . . . . 6
          |
6 | | rpcn 11333 |
. . . . . . 7

  |
7 | 6 | adantr 472 |
. . . . . 6
       
  |
8 | | rpne0 11340 |
. . . . . . 7

  |
9 | 8 | adantr 472 |
. . . . . 6
          |
10 | 5, 7, 9 | divcld 10405 |
. . . . 5
            |
11 | | asincl 23878 |
. . . . 5
   arcsin      |
12 | 10, 11 | syl 17 |
. . . 4
        arcsin      |
13 | | 1cnd 9677 |
. . . . . . 7
          |
14 | 10 | sqcld 12452 |
. . . . . . 7
                |
15 | 13, 14 | subcld 10005 |
. . . . . 6
                  |
16 | 15 | sqrtcld 13576 |
. . . . 5
                      |
17 | 10, 16 | mulcld 9681 |
. . . 4
                          |
18 | 12, 17 | addcld 9680 |
. . 3
         arcsin                       |
19 | | ovex 6336 |
. . . 4
                   |
20 | 19 | a1i 11 |
. . 3
                            |
21 | | rpre 11331 |
. . . . . . . . . 10

  |
22 | 21 | renegcld 10067 |
. . . . . . . . 9

   |
23 | 22 | rexrd 9708 |
. . . . . . . 8

   |
24 | | rpxr 11332 |
. . . . . . . 8

  |
25 | | elioo2 11702 |
. . . . . . . 8
                |
26 | 23, 24, 25 | syl2anc 673 |
. . . . . . 7

     
      |
27 | | simpr 468 |
. . . . . . . . . . . 12
     |
28 | 21 | adantr 472 |
. . . . . . . . . . . 12
     |
29 | 8 | adantr 472 |
. . . . . . . . . . . 12
     |
30 | 27, 28, 29 | redivcld 10457 |
. . . . . . . . . . 11
       |
31 | 30 | a1d 25 |
. . . . . . . . . 10
     
      |
32 | 6 | mulm1d 10091 |
. . . . . . . . . . . . . . 15

      |
33 | 32 | adantr 472 |
. . . . . . . . . . . . . 14
         |
34 | 33 | breq1d 4405 |
. . . . . . . . . . . . 13
      
    |
35 | | neg1rr 10736 |
. . . . . . . . . . . . . . 15
  |
36 | 35 | a1i 11 |
. . . . . . . . . . . . . 14
      |
37 | | simpl 464 |
. . . . . . . . . . . . . 14
     |
38 | 36, 27, 37 | ltmuldivd 11408 |
. . . . . . . . . . . . 13
      
      |
39 | 34, 38 | bitr3d 263 |
. . . . . . . . . . . 12
    
      |
40 | 39 | biimpd 212 |
. . . . . . . . . . 11
           |
41 | 40 | adantrd 475 |
. . . . . . . . . 10
     
       |
42 | | 1red 9676 |
. . . . . . . . . . . . . 14
     |
43 | 27, 42, 37 | ltdivmuld 11412 |
. . . . . . . . . . . . 13
     
     |
44 | 6 | mulid1d 9678 |
. . . . . . . . . . . . . . 15

    |
45 | 44 | adantr 472 |
. . . . . . . . . . . . . 14
   
   |
46 | 45 | breq2d 4407 |
. . . . . . . . . . . . 13
   
 
   |
47 | 43, 46 | bitr2d 262 |
. . . . . . . . . . . 12
   
     |
48 | 47 | biimpd 212 |
. . . . . . . . . . 11
   
     |
49 | 48 | adantld 474 |
. . . . . . . . . 10
     
      |
50 | 31, 41, 49 | 3jcad 1211 |
. . . . . . . . 9
     
      
      |
51 | 50 | exp4b 618 |
. . . . . . . 8

       
   
      |
52 | 51 | 3impd 1247 |
. . . . . . 7

       
   
    |
53 | 26, 52 | sylbid 223 |
. . . . . 6

             
    |
54 | 53 | imp 436 |
. . . . 5
           
   
   |
55 | 35 | rexri 9711 |
. . . . . 6
  |
56 | | 1re 9660 |
. . . . . . 7
 |
57 | 56 | rexri 9711 |
. . . . . 6
 |
58 | | elioo2 11702 |
. . . . . 6
                 
      |
59 | 55, 57, 58 | mp2an 686 |
. . . . 5
       
     
     |
60 | 54, 59 | sylibr 217 |
. . . 4
                 |
61 | | ovex 6336 |
. . . . 5
   |
62 | 61 | a1i 11 |
. . . 4
            |
63 | | elioore 11691 |
. . . . . . 7
        |
64 | 63 | recnd 9687 |
. . . . . 6
        |
65 | | asincl 23878 |
. . . . . . 7
 arcsin    |
66 | | id 22 |
. . . . . . . 8
   |
67 | | 1cnd 9677 |
. . . . . . . . . 10
   |
68 | | sqcl 12375 |
. . . . . . . . . 10
       |
69 | 67, 68 | subcld 10005 |
. . . . . . . . 9
         |
70 | 69 | sqrtcld 13576 |
. . . . . . . 8
             |
71 | 66, 70 | mulcld 9681 |
. . . . . . 7
               |
72 | 65, 71 | addcld 9680 |
. . . . . 6
  arcsin                 |
73 | 64, 72 | syl 17 |
. . . . 5
       arcsin                 |
74 | 73 | adantl 473 |
. . . 4
         arcsin                 |
75 | | ovex 6336 |
. . . . 5
             |
76 | 75 | a1i 11 |
. . . 4
                      |
77 | | recn 9647 |
. . . . . . 7
   |
78 | 77 | adantl 473 |
. . . . . 6
     |
79 | | 1cnd 9677 |
. . . . . 6
     |
80 | 2 | dvmptid 22990 |
. . . . . 6

        |
81 | | ioossre 11721 |
. . . . . . 7
      |
82 | 81 | a1i 11 |
. . . . . 6

       |
83 | | eqid 2471 |
. . . . . . 7
  ℂfld   ℂfld |
84 | 83 | tgioo2 21899 |
. . . . . 6
       ℂfld
↾t   |
85 | | iooretop 21864 |
. . . . . . 7
          |
86 | 85 | a1i 11 |
. . . . . 6

           |
87 | 2, 78, 79, 80, 82, 84, 83, 86 | dvmptres 22996 |
. . . . 5

                  |
88 | 2, 5, 13, 87, 6, 8 | dvmptdivc 22998 |
. . . 4

                      |
89 | 64, 65 | syl 17 |
. . . . . . 7
      arcsin    |
90 | 89 | adantl 473 |
. . . . . 6
        arcsin    |
91 | | ovex 6336 |
. . . . . . 7
             |
92 | 91 | a1i 11 |
. . . . . 6
                      |
93 | | dvreasin 32094 |
. . . . . . 7
 arcsin
                           |
94 | | asinf 23877 |
. . . . . . . . . 10
arcsin    |
95 | 94 | a1i 11 |
. . . . . . . . 9

arcsin     |
96 | | ioossre 11721 |
. . . . . . . . . . 11
      |
97 | | ax-resscn 9614 |
. . . . . . . . . . 11
 |
98 | 96, 97 | sstri 3427 |
. . . . . . . . . 10
      |
99 | 98 | a1i 11 |
. . . . . . . . 9

       |
100 | 95, 99 | feqresmpt 5933 |
. . . . . . . 8

arcsin             arcsin     |
101 | 100 | oveq2d 6324 |
. . . . . . 7

 arcsin
              arcsin      |
102 | 93, 101 | syl5reqr 2520 |
. . . . . 6

       arcsin                         |
103 | 64, 71 | syl 17 |
. . . . . . 7
                    |
104 | 103 | adantl 473 |
. . . . . 6
                      |
105 | | ovex 6336 |
. . . . . . 7
                              |
106 | 105 | a1i 11 |
. . . . . 6
                                       |
107 | 64 | adantl 473 |
. . . . . . 7
       
  |
108 | | 1cnd 9677 |
. . . . . . 7
          |
109 | | recn 9647 |
. . . . . . . . 9
   |
110 | 109 | adantl 473 |
. . . . . . . 8
     |
111 | | 1cnd 9677 |
. . . . . . . 8
     |
112 | 2 | dvmptid 22990 |
. . . . . . . 8

        |
113 | 96 | a1i 11 |
. . . . . . . 8

       |
114 | | iooretop 21864 |
. . . . . . . . 9
          |
115 | 114 | a1i 11 |
. . . . . . . 8

           |
116 | 2, 110, 111, 112, 113, 84, 83, 115 | dvmptres 22996 |
. . . . . . 7

                  |
117 | 64, 70 | syl 17 |
. . . . . . . 8
                  |
118 | 117 | adantl 473 |
. . . . . . 7
                    |
119 | | ovex 6336 |
. . . . . . . 8
              |
120 | 119 | a1i 11 |
. . . . . . 7
                       |
121 | | 1red 9676 |
. . . . . . . . . . . 12
        |
122 | 63 | resqcld 12480 |
. . . . . . . . . . . 12
            |
123 | 121, 122 | resubcld 10068 |
. . . . . . . . . . 11
              |
124 | | elioo2 11702 |
. . . . . . . . . . . . 13
                |
125 | 55, 57, 124 | mp2an 686 |
. . . . . . . . . . . 12
     
     |
126 | | id 22 |
. . . . . . . . . . . . . . . 16
   |
127 | | 1red 9676 |
. . . . . . . . . . . . . . . 16
   |
128 | 126, 127 | absltd 13568 |
. . . . . . . . . . . . . . 15
     
      |
129 | 109 | abscld 13575 |
. . . . . . . . . . . . . . . . 17
       |
130 | 109 | absge0d 13583 |
. . . . . . . . . . . . . . . . 17
       |
131 | | 0le1 10158 |
. . . . . . . . . . . . . . . . . 18
 |
132 | 131 | a1i 11 |
. . . . . . . . . . . . . . . . 17
   |
133 | 129, 127,
130, 132 | lt2sqd 12488 |
. . . . . . . . . . . . . . . 16
     
               |
134 | | absresq 13442 |
. . . . . . . . . . . . . . . . 17
               |
135 | | sq1 12407 |
. . . . . . . . . . . . . . . . . 18
     |
136 | 135 | a1i 11 |
. . . . . . . . . . . . . . . . 17
       |
137 | 134, 136 | breq12d 4408 |
. . . . . . . . . . . . . . . 16
             
       |
138 | | resqcl 12380 |
. . . . . . . . . . . . . . . . 17
       |
139 | 138, 127 | posdifd 10221 |
. . . . . . . . . . . . . . . 16
               |
140 | 133, 137,
139 | 3bitrd 287 |
. . . . . . . . . . . . . . 15
     
         |
141 | 128, 140 | bitr3d 263 |
. . . . . . . . . . . . . 14
   
          |
142 | 141 | biimpd 212 |
. . . . . . . . . . . . 13
   

         |
143 | 142 | 3impib 1229 |
. . . . . . . . . . . 12
   
        |
144 | 125, 143 | sylbi 200 |
. . . . . . . . . . 11
              |
145 | 123, 144 | elrpd 11361 |
. . . . . . . . . 10
              |
146 | 145 | adantl 473 |
. . . . . . . . 9
                |
147 | | negex 9893 |
. . . . . . . . . 10
    |
148 | 147 | a1i 11 |
. . . . . . . . 9
             |
149 | | rpcn 11333 |
. . . . . . . . . . 11

  |
150 | 149 | sqrtcld 13576 |
. . . . . . . . . 10

      |
151 | 150 | adantl 473 |
. . . . . . . . 9
         |
152 | | ovex 6336 |
. . . . . . . . . 10
         |
153 | 152 | a1i 11 |
. . . . . . . . 9
             |
154 | | 1cnd 9677 |
. . . . . . . . . . . 12
   |
155 | 109 | sqcld 12452 |
. . . . . . . . . . . 12
       |
156 | 154, 155 | subcld 10005 |
. . . . . . . . . . 11
         |
157 | 156 | adantl 473 |
. . . . . . . . . 10
           |
158 | 147 | a1i 11 |
. . . . . . . . . 10
        |
159 | | 0red 9662 |
. . . . . . . . . . . 12
     |
160 | | 1cnd 9677 |
. . . . . . . . . . . . 13

  |
161 | 2, 160 | dvmptc 22991 |
. . . . . . . . . . . 12

        |
162 | 155 | adantl 473 |
. . . . . . . . . . . 12
         |
163 | | ovex 6336 |
. . . . . . . . . . . . 13
   |
164 | 163 | a1i 11 |
. . . . . . . . . . . 12
       |
165 | 83 | cnfldtopon 21881 |
. . . . . . . . . . . . . 14
  ℂfld TopOn   |
166 | | toponmax 20020 |
. . . . . . . . . . . . . 14
   ℂfld TopOn 
  ℂfld  |
167 | 165, 166 | mp1i 13 |
. . . . . . . . . . . . 13

  ℂfld  |
168 | | df-ss 3404 |
. . . . . . . . . . . . . . 15
     |
169 | 97, 168 | mpbi 213 |
. . . . . . . . . . . . . 14
   |
170 | 169 | a1i 11 |
. . . . . . . . . . . . 13

    |
171 | 68 | adantl 473 |
. . . . . . . . . . . . 13
         |
172 | 163 | a1i 11 |
. . . . . . . . . . . . 13
       |
173 | | 2nn 10790 |
. . . . . . . . . . . . . . . 16
 |
174 | | dvexp 22986 |
. . . . . . . . . . . . . . . 16
                     |
175 | 173, 174 | ax-mp 5 |
. . . . . . . . . . . . . . 15
                   |
176 | | 2m1e1 10746 |
. . . . . . . . . . . . . . . . . . 19
   |
177 | 176 | oveq2i 6319 |
. . . . . . . . . . . . . . . . . 18
           |
178 | | exp1 12316 |
. . . . . . . . . . . . . . . . . 18
       |
179 | 177, 178 | syl5eq 2517 |
. . . . . . . . . . . . . . . . 17
         |
180 | 179 | oveq2d 6324 |
. . . . . . . . . . . . . . . 16
             |
181 | 180 | mpteq2ia 4478 |
. . . . . . . . . . . . . . 15
               |
182 | 175, 181 | eqtri 2493 |
. . . . . . . . . . . . . 14
             |
183 | 182 | a1i 11 |
. . . . . . . . . . . . 13

              |
184 | 83, 2, 167, 170, 171, 172, 183 | dvmptres3 22989 |
. . . . . . . . . . . 12

              |
185 | 2, 111, 159, 161, 162, 164, 184 | dvmptsub 23000 |
. . . . . . . . . . 11

                  |
186 | | df-neg 9883 |
. . . . . . . . . . . 12
        |
187 | 186 | mpteq2i 4479 |
. . . . . . . . . . 11
            |
188 | 185, 187 | syl6eqr 2523 |
. . . . . . . . . 10

                 |
189 | 2, 157, 158, 188, 113, 84, 83, 115 | dvmptres 22996 |
. . . . . . . . 9

                           |
190 | | dvsqrt 23761 |
. . . . . . . . . 10
                   |
191 | 190 | a1i 11 |
. . . . . . . . 9

                    |
192 | | fveq2 5879 |
. . . . . . . . 9
                       |
193 | 192 | oveq2d 6324 |
. . . . . . . . . 10
                           |
194 | 193 | oveq2d 6324 |
. . . . . . . . 9
                               |
195 | 2, 2, 146, 148, 151, 153, 189, 191, 192, 194 | dvmptco 23005 |
. . . . . . . 8

                                               |
196 | | 2cnd 10704 |
. . . . . . . . . . . 12
        |
197 | 196, 64 | mulneg2d 10093 |
. . . . . . . . . . 11
              |
198 | 197 | oveq1d 6323 |
. . . . . . . . . 10
                                          |
199 | 64 | negcld 9992 |
. . . . . . . . . . 11
         |
200 | 144 | gt0ne0d 10199 |
. . . . . . . . . . . 12
              |
201 | 64, 69 | syl 17 |
. . . . . . . . . . . . . . . 16
              |
202 | 201 | adantr 472 |
. . . . . . . . . . . . . . 15
                          |
203 | | simpr 468 |
. . . . . . . . . . . . . . 15
                              |
204 | 202, 203 | sqr00d 13580 |
. . . . . . . . . . . . . 14
                          |
205 | 204 | ex 441 |
. . . . . . . . . . . . 13
                          |
206 | 205 | necon3d 2664 |
. . . . . . . . . . . 12
                          |
207 | 200, 206 | mpd 15 |
. . . . . . . . . . 11
                  |
208 | | 2ne0 10724 |
. . . . . . . . . . . 12
 |
209 | 208 | a1i 11 |
. . . . . . . . . . 11
        |
210 | 199, 117,
196, 207, 209 | divcan5d 10431 |
. . . . . . . . . 10
                                      |
211 | 196, 64 | mulcld 9681 |
. . . . . . . . . . . 12
          |
212 | 211 | negcld 9992 |
. . . . . . . . . . 11
           |
213 | 196, 117 | mulcld 9681 |
. . . . . . . . . . 11
                    |
214 | 196, 117,
209, 207 | mulne0d 10286 |
. . . . . . . . . . 11
                    |
215 | 212, 213,
214 | divrec2d 10409 |
. . . . . . . . . 10
                                            |
216 | 198, 210,
215 | 3eqtr3rd 2514 |
. . . . . . . . 9
                                        |
217 | 216 | mpteq2ia 4478 |
. . . . . . . 8
                                               |
218 | 195, 217 | syl6eq 2521 |
. . . . . . 7

                                         |
219 | 2, 107, 108, 116, 118, 120, 218 | dvmptmul 22994 |
. . . . . 6

                                                           |
220 | 2, 90, 92, 102, 104, 106, 219 | dvmptadd 22993 |
. . . . 5

        arcsin                                                                     |
221 | 117 | mulid2d 9679 |
. . . . . . . . . 10
                              |
222 | 199, 117,
207 | divcld 10405 |
. . . . . . . . . . . 12
                     |
223 | 222, 64 | mulcomd 9682 |
. . . . . . . . . . 11
                                      |
224 | 64, 199, 117, 207 | divassd 10440 |
. . . . . . . . . . 11
                                      |
225 | 64, 64 | mulneg2d 10093 |
. . . . . . . . . . . . 13
              |
226 | 64 | sqvald 12451 |
. . . . . . . . . . . . . 14
              |
227 | 226 | negeqd 9889 |
. . . . . . . . . . . . 13
                |
228 | 225, 227 | eqtr4d 2508 |
. . . . . . . . . . . 12
                |
229 | 228 | oveq1d 6323 |
. . . . . . . . . . 11
                                        |
230 | 223, 224,
229 | 3eqtr2d 2511 |
. . . . . . . . . 10
                                        |
231 | 221, 230 | oveq12d 6326 |
. . . . . . . . 9
                                                                  |
232 | 64 | sqcld 12452 |
. . . . . . . . . . . 12
            |
233 | 232 | negcld 9992 |
. . . . . . . . . . 11
             |
234 | 233, 117,
207 | divcld 10405 |
. . . . . . . . . 10
                         |
235 | 117, 234 | addcomd 9853 |
. . . . . . . . 9
                                                                  |
236 | 231, 235 | eqtrd 2505 |
. . . . . . . 8
                                                                  |
237 | 236 | oveq2d 6324 |
. . . . . . 7
                                                                                              |
238 | 117 | 2timesd 10878 |
. . . . . . . 8
                                          |
239 | 67, 68 | negsubd 10011 |
. . . . . . . . . . . . 13
                |
240 | 69 | sqsqrtd 13578 |
. . . . . . . . . . . . 13
                       |
241 | 70 | sqvald 12451 |
. . . . . . . . . . . . 13
                                       |
242 | 239, 240,
241 | 3eqtr2d 2511 |
. . . . . . . . . . . 12
                                |
243 | 64, 242 | syl 17 |
. . . . . . . . . . 11
                                     |
244 | 243 | oveq1d 6323 |
. . . . . . . . . 10
                                                             |
245 | | 1cnd 9677 |
. . . . . . . . . . 11
        |
246 | 245, 233,
117, 207 | divdird 10443 |
. . . . . . . . . 10
                                                          |
247 | 117, 117,
207 | divcan3d 10410 |
. . . . . . . . . 10
                                                    |
248 | 244, 246,
247 | 3eqtr3rd 2514 |
. . . . . . . . 9
                                                 |
249 | 248 | oveq1d 6323 |
. . . . . . . 8
                                                                         |
250 | 117, 207 | reccld 10398 |
. . . . . . . . 9
                    |
251 | 250, 234,
117 | addassd 9683 |
. . . . . . . 8
                                                                                              |
252 | 238, 249,
251 | 3eqtrrd 2510 |
. . . . . . 7
                                                               |
253 | 237, 252 | eqtrd 2505 |
. . . . . 6
                                                               |
254 | 253 | mpteq2ia 4478 |
. . . . 5
                                                                      |
255 | 220, 254 | syl6eq 2521 |
. . . 4

        arcsin                                      |
256 | | fveq2 5879 |
. . . . 5
   arcsin  arcsin      |
257 | | id 22 |
. . . . . 6
       |
258 | | oveq1 6315 |
. . . . . . . 8
               |
259 | 258 | oveq2d 6324 |
. . . . . . 7
                   |
260 | 259 | fveq2d 5883 |
. . . . . 6
                           |
261 | 257, 260 | oveq12d 6326 |
. . . . 5
                                 |
262 | 256, 261 | oveq12d 6326 |
. . . 4
    arcsin                arcsin                       |
263 | 260 | oveq2d 6324 |
. . . 4
                               |
264 | 2, 2, 60, 62, 74, 76, 88, 255, 262, 263 | dvmptco 23005 |
. . 3

        arcsin                                                  |
265 | 6 | sqcld 12452 |
. . 3

      |
266 | 2, 18, 20, 264, 265 | dvmptcmul 22997 |
. 2

             arcsin                                                         |
267 | | 2cnd 10704 |
. . . . . . 7
          |
268 | 267, 16 | mulcld 9681 |
. . . . . 6
                        |
269 | 6, 8 | reccld 10398 |
. . . . . . 7

    |
270 | 269 | adantr 472 |
. . . . . 6
            |
271 | 268, 270 | mulcomd 9682 |
. . . . 5
                                              |
272 | 271 | oveq2d 6324 |
. . . 4
                                                          |
273 | 265 | adantr 472 |
. . . . 5
              |
274 | 273, 270,
268 | mulassd 9684 |
. . . 4
                                                          |
275 | 6 | sqvald 12451 |
. . . . . . . . 9

        |
276 | 275 | oveq1d 6323 |
. . . . . . . 8

            |
277 | 265, 6, 8 | divrecd 10408 |
. . . . . . . 8

                |
278 | 6, 6, 8 | divcan3d 10410 |
. . . . . . . 8

      |
279 | 276, 277,
278 | 3eqtr3d 2513 |
. . . . . . 7

          |
280 | 279 | adantr 472 |
. . . . . 6
                  |
281 | 280 | oveq1d 6323 |
. . . . 5
                                                  |
282 | 7, 267, 16 | mul12d 9860 |
. . . . 5
                                          |
283 | 21 | resqcld 12480 |
. . . . . . . . 9

      |
284 | 283 | adantr 472 |
. . . . . . . 8
              |
285 | 21 | sqge0d 12481 |
. . . . . . . . 9

      |
286 | 285 | adantr 472 |
. . . . . . . 8
       
      |
287 | | 1red 9676 |
. . . . . . . . 9
          |
288 | 3 | adantl 473 |
. . . . . . . . . . 11
          |
289 | 21 | adantr 472 |
. . . . . . . . . . 11
       
  |
290 | 288, 289,
9 | redivcld 10457 |
. . . . . . . . . 10
            |
291 | 290 | resqcld 12480 |
. . . . . . . . 9
                |
292 | 287, 291 | resubcld 10068 |
. . . . . . . 8
                  |
293 | | 0red 9662 |
. . . . . . . . 9
          |
294 | 27, 28 | absltd 13568 |
. . . . . . . . . . . . . . 15
       
      |
295 | 77 | abscld 13575 |
. . . . . . . . . . . . . . . . . 18
       |
296 | 295 | adantl 473 |
. . . . . . . . . . . . . . . . 17
         |
297 | 77 | absge0d 13583 |
. . . . . . . . . . . . . . . . . 18
       |
298 | 297 | adantl 473 |
. . . . . . . . . . . . . . . . 17
         |
299 | | rpge0 11337 |
. . . . . . . . . . . . . . . . . 18

  |
300 | 299 | adantr 472 |
. . . . . . . . . . . . . . . . 17
     |
301 | 296, 28, 298, 300 | lt2sqd 12488 |
. . . . . . . . . . . . . . . 16
       
               |
302 | | absresq 13442 |
. . . . . . . . . . . . . . . . . 18
               |
303 | 302 | adantl 473 |
. . . . . . . . . . . . . . . . 17
                 |
304 | 265 | adantr 472 |
. . . . . . . . . . . . . . . . . . 19
         |
305 | 304 | mulid1d 9678 |
. . . . . . . . . . . . . . . . . 18
               |
306 | 305 | eqcomd 2477 |
. . . . . . . . . . . . . . . . 17
               |
307 | 303, 306 | breq12d 4408 |
. . . . . . . . . . . . . . . 16
               
             |
308 | 6 | adantr 472 |
. . . . . . . . . . . . . . . . . . 19
     |
309 | 78, 308, 29 | sqdivd 12467 |
. . . . . . . . . . . . . . . . . 18
                     |
310 | 309 | breq1d 4405 |
. . . . . . . . . . . . . . . . 17
                       |
311 | 30 | resqcld 12480 |
. . . . . . . . . . . . . . . . . 18
           |
312 | 311, 42 | posdifd 10221 |
. . . . . . . . . . . . . . . . 17
                     |
313 | | resqcl 12380 |
. . . . . . . . . . . . . . . . . . 19
       |
314 | 313 | adantl 473 |
. . . . . . . . . . . . . . . . . 18
         |
315 | | rpgt0 11336 |
. . . . . . . . . . . . . . . . . . . . 21

  |
316 | | 0red 9662 |
. . . . . . . . . . . . . . . . . . . . . . 23

  |
317 | | 0le0 10721 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 |
318 | 317 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23

  |
319 | 316, 21, 318, 299 | lt2sqd 12488 |
. . . . . . . . . . . . . . . . . . . . . 22


           |
320 | | sq0 12404 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     |
321 | 320 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23

      |
322 | 321 | breq1d 4405 |
. . . . . . . . . . . . . . . . . . . . . 22

        
       |
323 | 319, 322 | bitrd 261 |
. . . . . . . . . . . . . . . . . . . . 21


       |
324 | 315, 323 | mpbid 215 |
. . . . . . . . . . . . . . . . . . . 20

      |
325 | 283, 324 | elrpd 11361 |
. . . . . . . . . . . . . . . . . . 19

      |
326 | 325 | adantr 472 |
. . . . . . . . . . . . . . . . . 18
         |
327 | 314, 42, 326 | ltdivmuld 11412 |
. . . . . . . . . . . . . . . . 17
             
             |
328 | 310, 312,
327 | 3bitr3rd 292 |
. . . . . . . . . . . . . . . 16
             
           |
329 | 301, 307,
328 | 3bitrd 287 |
. . . . . . . . . . . . . . 15
       
           |
330 | 294, 329 | bitr3d 263 |
. . . . . . . . . . . . . 14
     
            |
331 | 330 | biimpd 212 |
. . . . . . . . . . . . 13
     
            |
332 | 331 | exp4b 618 |
. . . . . . . . . . . 12

                 |
333 | 332 | 3impd 1247 |
. . . . . . . . . . 11

   
           |
334 | 26, 333 | sylbid 223 |
. . . . . . . . . 10

                 |
335 | 334 | imp 436 |
. . . . . . . . 9
       
          |
336 | 293, 292,
335 | ltled 9800 |
. . . . . . . 8
       
          |
337 | 284, 286,
292, 336 | sqrtmuld 13563 |
. . . . . . 7
                                                  |
338 | 273, 13, 14 | subdid 10095 |
. . . . . . . . 9
                                            |
339 | 273 | mulid1d 9678 |
. . . . . . . . . 10
                    |
340 | 5, 7, 9 | sqdivd 12467 |
. . . . . . . . . . . 12
                          |
341 | 340 | oveq2d 6324 |
. . . . . . . . . . 11
                                      |
342 | 4 | sqcld 12452 |
. . . . . . . . . . . . 13
            |
343 | 342 | adantl 473 |
. . . . . . . . . . . 12
              |
344 | | sqne0 12379 |
. . . . . . . . . . . . . . 15
         |
345 | 6, 344 | syl 17 |
. . . . . . . . . . . . . 14

    
   |
346 | 8, 345 | mpbird 240 |
. . . . . . . . . . . . 13

      |
347 | 346 | adantr 472 |
. . . . . . . . . . . 12
              |
348 | 343, 273,
347 | divcan2d 10407 |
. . . . . . . . . . 11
                              |
349 | 341, 348 | eqtrd 2505 |
. . . . . . . . . 10
                          |
350 | 339, 349 | oveq12d 6326 |
. . . . . . . . 9
                                        |
351 | 338, 350 | eqtrd 2505 |
. . . . . . . 8
                                  |
352 | 351 | fveq2d 5883 |
. . . . . . 7
                                          |
353 | 21, 299 | sqrtsqd 13558 |
. . . . . . . . 9

          |
354 | 353 | adantr 472 |
. . . . . . . 8
                  |
355 | 354 | oveq1d 6323 |
. . . . . . 7
                                              |
356 | 337, 352,
355 | 3eqtr3rd 2514 |
. . . . . 6
                                      |
357 | 356 | oveq2d 6324 |
. . . . 5
         
                                |
358 | 281, 282,
357 | 3eqtrd 2509 |
. . . 4
                                                  |
359 | 272, 274,
358 | 3eqtr2d 2511 |
. . 3
                                                  |
360 | 359 | mpteq2dva 4482 |
. 2

                                                        |
361 | 266, 360 | eqtrd 2505 |
1

             arcsin                                                 |