Step | Hyp | Ref
| Expression |
1 | | df-asin 23870 |
. . . . 5
arcsin                         |
2 | 1 | reseq1i 5107 |
. . . 4
arcsin                            |
3 | | dvasin.d |
. . . . . 6
   ![(,] (,]](_ioc.gif)         |
4 | | difss 3549 |
. . . . . 6
   ![(,] (,]](_ioc.gif)         |
5 | 3, 4 | eqsstri 3448 |
. . . . 5
 |
6 | | resmpt 5160 |
. . . . 5

                       
                          |
7 | 5, 6 | ax-mp 5 |
. . . 4
                       
                         |
8 | 2, 7 | eqtri 2493 |
. . 3
arcsin                          |
9 | 8 | oveq2i 6319 |
. 2
 arcsin
                            |
10 | | cnelprrecn 9650 |
. . . . 5
    |
11 | 10 | a1i 11 |
. . . 4
     |
12 | 5 | sseli 3414 |
. . . . . . 7
   |
13 | | ax-icn 9616 |
. . . . . . . . 9
 |
14 | | mulcl 9641 |
. . . . . . . . 9
 
     |
15 | 13, 14 | mpan 684 |
. . . . . . . 8
 
   |
16 | | ax-1cn 9615 |
. . . . . . . . . 10
 |
17 | | sqcl 12375 |
. . . . . . . . . 10
       |
18 | | subcl 9894 |
. . . . . . . . . 10
               |
19 | 16, 17, 18 | sylancr 676 |
. . . . . . . . 9
         |
20 | 19 | sqrtcld 13576 |
. . . . . . . 8
             |
21 | 15, 20 | addcld 9680 |
. . . . . . 7
                 |
22 | 12, 21 | syl 17 |
. . . . . 6
                 |
23 | | asinlem 23873 |
. . . . . . 7
                 |
24 | 12, 23 | syl 17 |
. . . . . 6
                 |
25 | 22, 24 | logcld 23599 |
. . . . 5
                     |
26 | 25 | adantl 473 |
. . . 4
                      |
27 | | ovex 6336 |
. . . . 5
             |
28 | 27 | a1i 11 |
. . . 4
  
             |
29 | | simpr 468 |
. . . . . . . . . . . . . . . 16
                                 |
30 | | asinlem3 23876 |
. . . . . . . . . . . . . . . . 17
                     |
31 | | rere 13262 |
. . . . . . . . . . . . . . . . . . 19
              
                                  |
32 | 31 | breq2d 4407 |
. . . . . . . . . . . . . . . . . 18
              
                  
                 |
33 | 32 | biimpac 494 |
. . . . . . . . . . . . . . . . 17
 
                                                 |
34 | 30, 33 | sylan 479 |
. . . . . . . . . . . . . . . 16
                                 |
35 | 23 | adantr 472 |
. . . . . . . . . . . . . . . 16
                                 |
36 | 29, 34, 35 | ne0gt0d 9789 |
. . . . . . . . . . . . . . 15
                                 |
37 | | 0re 9661 |
. . . . . . . . . . . . . . . . 17
 |
38 | | ltnle 9731 |
. . . . . . . . . . . . . . . . 17
                               
 
               |
39 | 37, 38 | mpan 684 |
. . . . . . . . . . . . . . . 16
              
              
                 |
40 | 39 | adantl 473 |
. . . . . . . . . . . . . . 15
                               
 
               |
41 | 36, 40 | mpbid 215 |
. . . . . . . . . . . . . 14
                
 
              |
42 | 41 | ex 441 |
. . . . . . . . . . . . 13
                             
   |
43 | 12, 42 | syl 17 |
. . . . . . . . . . . 12
                             
   |
44 | | imor 419 |
. . . . . . . . . . . 12
                             
                                 |
45 | 43, 44 | sylib 201 |
. . . . . . . . . . 11
                             
   |
46 | 45 | orcomd 395 |
. . . . . . . . . 10
               
                 |
47 | 46 | olcd 400 |
. . . . . . . . 9
 
 
                          
                  |
48 | | 3ianor 1024 |
. . . . . . . . . . 11
                                            
              
 
                         
   |
49 | | 3orrot 1013 |
. . . . . . . . . . 11
                                                                                           |
50 | | 3orass 1010 |
. . . . . . . . . . 11
                                                                                             |
51 | 48, 49, 50 | 3bitrri 280 |
. . . . . . . . . 10
                                              
                                              |
52 | | mnfxr 11437 |
. . . . . . . . . . 11
 |
53 | | elioc2 11722 |
. . . . . . . . . . 11
                  ![(,] (,]](_ioc.gif) 
                                          
    |
54 | 52, 37, 53 | mp2an 686 |
. . . . . . . . . 10
                ![(,] (,]](_ioc.gif)                                                |
55 | 51, 54 | xchbinxr 318 |
. . . . . . . . 9
                                              
               ![(,] (,]](_ioc.gif)    |
56 | 47, 55 | sylib 201 |
. . . . . . . 8
                ![(,] (,]](_ioc.gif)    |
57 | 22, 56 | eldifd 3401 |
. . . . . . 7
                 ![(,] (,]](_ioc.gif)     |
58 | 57 | adantl 473 |
. . . . . 6
                  ![(,] (,]](_ioc.gif)     |
59 | | ovex 6336 |
. . . . . . 7
                             |
60 | 59 | a1i 11 |
. . . . . 6
                                |
61 | | eldifi 3544 |
. . . . . . . 8
   ![(,] (,]](_ioc.gif)  
  |
62 | | eldifn 3545 |
. . . . . . . . 9
   ![(,] (,]](_ioc.gif)  
 ![(,] (,]](_ioc.gif)    |
63 | | 0xr 9705 |
. . . . . . . . . . . 12
 |
64 | | mnflt0 11450 |
. . . . . . . . . . . 12
 |
65 | | ubioc1 11713 |
. . . . . . . . . . . 12
 
 ![(,] (,]](_ioc.gif)    |
66 | 52, 63, 64, 65 | mp3an 1390 |
. . . . . . . . . . 11
 ![(,] (,]](_ioc.gif)   |
67 | | eleq1 2537 |
. . . . . . . . . . 11
   ![(,] (,]](_ioc.gif) 
 ![(,] (,]](_ioc.gif)     |
68 | 66, 67 | mpbiri 241 |
. . . . . . . . . 10

 ![(,] (,]](_ioc.gif)    |
69 | 68 | necon3bi 2669 |
. . . . . . . . 9
  ![(,] (,]](_ioc.gif)    |
70 | 62, 69 | syl 17 |
. . . . . . . 8
   ![(,] (,]](_ioc.gif)  
  |
71 | 61, 70 | logcld 23599 |
. . . . . . 7
   ![(,] (,]](_ioc.gif)  
      |
72 | 71 | adantl 473 |
. . . . . 6
   ![(,] (,]](_ioc.gif)   
      |
73 | | ovex 6336 |
. . . . . . 7
   |
74 | 73 | a1i 11 |
. . . . . 6
   ![(,] (,]](_ioc.gif)   
    |
75 | 13 | a1i 11 |
. . . . . . . . . 10
   |
76 | 75, 12 | mulcld 9681 |
. . . . . . . . 9
 
   |
77 | 76 | adantl 473 |
. . . . . . . 8
  
   |
78 | 13 | a1i 11 |
. . . . . . . 8
    |
79 | 12 | adantl 473 |
. . . . . . . . . 10
    |
80 | | 1cnd 9677 |
. . . . . . . . . 10
    |
81 | | simpr 468 |
. . . . . . . . . . 11
    |
82 | | 1cnd 9677 |
. . . . . . . . . . 11
    |
83 | 11 | dvmptid 22990 |
. . . . . . . . . . 11
        |
84 | 5 | a1i 11 |
. . . . . . . . . . 11
  |
85 | | eqid 2471 |
. . . . . . . . . . . . . 14
  ℂfld   ℂfld |
86 | 85 | cnfldtopon 21881 |
. . . . . . . . . . . . 13
  ℂfld TopOn   |
87 | 86 | toponunii 20024 |
. . . . . . . . . . . . . 14
   ℂfld |
88 | 87 | restid 15410 |
. . . . . . . . . . . . 13
   ℂfld TopOn 
   ℂfld ↾t    ℂfld  |
89 | 86, 88 | ax-mp 5 |
. . . . . . . . . . . 12
   ℂfld ↾t    ℂfld |
90 | 89 | eqcomi 2480 |
. . . . . . . . . . 11
  ℂfld    ℂfld ↾t   |
91 | 85 | recld2 21910 |
. . . . . . . . . . . . . . 15
     ℂfld  |
92 | | neg1rr 10736 |
. . . . . . . . . . . . . . . . . 18
  |
93 | | iocmnfcld 21867 |
. . . . . . . . . . . . . . . . . 18
   ![(,] (,]](_ioc.gif)             |
94 | 92, 93 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
 ![(,] (,]](_ioc.gif)        
   |
95 | | 1re 9660 |
. . . . . . . . . . . . . . . . . 18
 |
96 | | icopnfcld 21866 |
. . . . . . . . . . . . . . . . . 18
  
      
    |
97 | 95, 96 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
        
   |
98 | | uncld 20133 |
. . . . . . . . . . . . . . . . 17
   ![(,] (,]](_ioc.gif)          
        
     ![(,] (,]](_ioc.gif)            
    |
99 | 94, 97, 98 | mp2an 686 |
. . . . . . . . . . . . . . . 16
  ![(,] (,]](_ioc.gif)            
   |
100 | 85 | tgioo2 21899 |
. . . . . . . . . . . . . . . . 17
       ℂfld
↾t   |
101 | 100 | fveq2i 5882 |
. . . . . . . . . . . . . . . 16
              ℂfld
↾t    |
102 | 99, 101 | eleqtri 2547 |
. . . . . . . . . . . . . . 15
  ![(,] (,]](_ioc.gif)             ℂfld
↾t    |
103 | | restcldr 20267 |
. . . . . . . . . . . . . . 15
       ℂfld   ![(,] (,]](_ioc.gif)             ℂfld
↾t      ![(,] (,]](_ioc.gif)            ℂfld   |
104 | 91, 102, 103 | mp2an 686 |
. . . . . . . . . . . . . 14
  ![(,] (,]](_ioc.gif)            ℂfld  |
105 | 87 | cldopn 20123 |
. . . . . . . . . . . . . 14
   ![(,] (,]](_ioc.gif)            ℂfld    ![(,] (,]](_ioc.gif)          ℂfld  |
106 | 104, 105 | ax-mp 5 |
. . . . . . . . . . . . 13
   ![(,] (,]](_ioc.gif)          ℂfld |
107 | 3, 106 | eqeltri 2545 |
. . . . . . . . . . . 12
  ℂfld |
108 | 107 | a1i 11 |
. . . . . . . . . . 11
  ℂfld  |
109 | 11, 81, 82, 83, 84, 90, 85, 108 | dvmptres 22996 |
. . . . . . . . . 10
        |
110 | 13 | a1i 11 |
. . . . . . . . . 10
  |
111 | 11, 79, 80, 109, 110 | dvmptcmul 22997 |
. . . . . . . . 9
            |
112 | 13 | mulid1i 9663 |
. . . . . . . . . 10
   |
113 | 112 | mpteq2i 4479 |
. . . . . . . . 9
       |
114 | 111, 113 | syl6eq 2521 |
. . . . . . . 8
          |
115 | 12 | sqcld 12452 |
. . . . . . . . . . 11
       |
116 | 16, 115, 18 | sylancr 676 |
. . . . . . . . . 10
         |
117 | 116 | sqrtcld 13576 |
. . . . . . . . 9
             |
118 | 117 | adantl 473 |
. . . . . . . 8
              |
119 | | ovex 6336 |
. . . . . . . . 9
              |
120 | 119 | a1i 11 |
. . . . . . . 8
                 |
121 | | elin 3608 |
. . . . . . . . . . . . . . 15
       |
122 | 3 | asindmre 32091 |
. . . . . . . . . . . . . . . . 17
        |
123 | 122 | eqimssi 3472 |
. . . . . . . . . . . . . . . 16
        |
124 | 123 | sseli 3414 |
. . . . . . . . . . . . . . 15
  
       |
125 | 121, 124 | sylbir 218 |
. . . . . . . . . . . . . 14
 
        |
126 | | incom 3616 |
. . . . . . . . . . . . . . . 16
   
 ![(,] (,]](_ioc.gif)     ![(,] (,]](_ioc.gif) 
     |
127 | | pnfxr 11435 |
. . . . . . . . . . . . . . . . 17
 |
128 | | df-ioc 11665 |
. . . . . . . . . . . . . . . . . 18




    |
129 | | df-ioo 11664 |
. . . . . . . . . . . . . . . . . 18




    |
130 | | xrltnle 9719 |
. . . . . . . . . . . . . . . . . 18
   
   |
131 | 128, 129,
130 | ixxdisj 11675 |
. . . . . . . . . . . . . . . . 17
 
  ![(,] (,]](_ioc.gif)        |
132 | 52, 63, 127, 131 | mp3an 1390 |
. . . . . . . . . . . . . . . 16
  ![(,] (,]](_ioc.gif)       |
133 | 126, 132 | eqtri 2493 |
. . . . . . . . . . . . . . 15
   
 ![(,] (,]](_ioc.gif)    |
134 | | elioore 11691 |
. . . . . . . . . . . . . . . . . . 19
        |
135 | 134 | resqcld 12480 |
. . . . . . . . . . . . . . . . . 18
            |
136 | | resubcl 9958 |
. . . . . . . . . . . . . . . . . 18
               |
137 | 95, 135, 136 | sylancr 676 |
. . . . . . . . . . . . . . . . 17
              |
138 | 92 | rexri 9711 |
. . . . . . . . . . . . . . . . . . 19
  |
139 | 95 | rexri 9711 |
. . . . . . . . . . . . . . . . . . 19
 |
140 | | elioo2 11702 |
. . . . . . . . . . . . . . . . . . 19
                |
141 | 138, 139,
140 | mp2an 686 |
. . . . . . . . . . . . . . . . . 18
     
     |
142 | | recn 9647 |
. . . . . . . . . . . . . . . . . . . . . . 23
   |
143 | 142 | abscld 13575 |
. . . . . . . . . . . . . . . . . . . . . 22
       |
144 | 142 | absge0d 13583 |
. . . . . . . . . . . . . . . . . . . . . 22
       |
145 | | 0le1 10158 |
. . . . . . . . . . . . . . . . . . . . . . 23
 |
146 | | lt2sq 12386 |
. . . . . . . . . . . . . . . . . . . . . . 23
                                   |
147 | 95, 145, 146 | mpanr12 699 |
. . . . . . . . . . . . . . . . . . . . . 22
               
               |
148 | 143, 144,
147 | syl2anc 673 |
. . . . . . . . . . . . . . . . . . . . 21
     
               |
149 | | abslt 13454 |
. . . . . . . . . . . . . . . . . . . . . 22
 
     
      |
150 | 95, 149 | mpan2 685 |
. . . . . . . . . . . . . . . . . . . . 21
     
      |
151 | | absresq 13442 |
. . . . . . . . . . . . . . . . . . . . . . 23
               |
152 | | sq1 12407 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     |
153 | 152 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
       |
154 | 151, 153 | breq12d 4408 |
. . . . . . . . . . . . . . . . . . . . . 22
             
       |
155 | | resqcl 12380 |
. . . . . . . . . . . . . . . . . . . . . . 23
       |
156 | | posdif 10128 |
. . . . . . . . . . . . . . . . . . . . . . 23
     
               |
157 | 155, 95, 156 | sylancl 675 |
. . . . . . . . . . . . . . . . . . . . . 22
               |
158 | 154, 157 | bitrd 261 |
. . . . . . . . . . . . . . . . . . . . 21
             
         |
159 | 148, 150,
158 | 3bitr3d 291 |
. . . . . . . . . . . . . . . . . . . 20
   
          |
160 | 159 | biimpd 212 |
. . . . . . . . . . . . . . . . . . 19
   

         |
161 | 160 | 3impib 1229 |
. . . . . . . . . . . . . . . . . 18
   
        |
162 | 141, 161 | sylbi 200 |
. . . . . . . . . . . . . . . . 17
              |
163 | 137, 162 | elrpd 11361 |
. . . . . . . . . . . . . . . 16
              |
164 | | ioorp 11737 |
. . . . . . . . . . . . . . . 16
    |
165 | 163, 164 | syl6eleqr 2560 |
. . . . . . . . . . . . . . 15
                 |
166 | | disjel 3815 |
. . . . . . . . . . . . . . 15
     
 ![(,] (,]](_ioc.gif)  
                 ![(,] (,]](_ioc.gif)    |
167 | 133, 165,
166 | sylancr 676 |
. . . . . . . . . . . . . 14
             ![(,] (,]](_ioc.gif)    |
168 | 125, 167 | syl 17 |
. . . . . . . . . . . . 13
 
        ![(,] (,]](_ioc.gif)    |
169 | | elioc2 11722 |
. . . . . . . . . . . . . . . . . . . . . . . 24
          ![(,] (,]](_ioc.gif) 
                       |
170 | 52, 37, 169 | mp2an 686 |
. . . . . . . . . . . . . . . . . . . . . . 23
        ![(,] (,]](_ioc.gif) 
                      |
171 | 170 | biimpi 199 |
. . . . . . . . . . . . . . . . . . . . . 22
        ![(,] (,]](_ioc.gif)                        |
172 | 171 | simp1d 1042 |
. . . . . . . . . . . . . . . . . . . . 21
        ![(,] (,]](_ioc.gif)          |
173 | | resubcl 9958 |
. . . . . . . . . . . . . . . . . . . . 21
                   |
174 | 95, 172, 173 | sylancr 676 |
. . . . . . . . . . . . . . . . . . . 20
        ![(,] (,]](_ioc.gif)            |
175 | | nncan 9923 |
. . . . . . . . . . . . . . . . . . . . . . 23
                     |
176 | 16, 175 | mpan 684 |
. . . . . . . . . . . . . . . . . . . . . 22
                   |
177 | 176 | eleq1d 2533 |
. . . . . . . . . . . . . . . . . . . . 21
             
       |
178 | 177 | biimpa 492 |
. . . . . . . . . . . . . . . . . . . 20
                     |
179 | 174, 178 | sylan2 482 |
. . . . . . . . . . . . . . . . . . 19
             ![(,] (,]](_ioc.gif)         |
180 | 172 | adantl 473 |
. . . . . . . . . . . . . . . . . . . . . 22
             ![(,] (,]](_ioc.gif)           |
181 | 171 | simp3d 1044 |
. . . . . . . . . . . . . . . . . . . . . . 23
        ![(,] (,]](_ioc.gif)          |
182 | 181 | adantl 473 |
. . . . . . . . . . . . . . . . . . . . . 22
             ![(,] (,]](_ioc.gif)        
  |
183 | | letr 9745 |
. . . . . . . . . . . . . . . . . . . . . . . 24
       
        
          |
184 | 37, 95, 183 | mp3an23 1382 |
. . . . . . . . . . . . . . . . . . . . . . 23
              
          |
185 | 145, 184 | mpan2i 691 |
. . . . . . . . . . . . . . . . . . . . . 22
             
         |
186 | 180, 182,
185 | sylc 61 |
. . . . . . . . . . . . . . . . . . . . 21
             ![(,] (,]](_ioc.gif)        
  |
187 | | subge0 10148 |
. . . . . . . . . . . . . . . . . . . . . 22
                           |
188 | 95, 180, 187 | sylancr 676 |
. . . . . . . . . . . . . . . . . . . . 21
             ![(,] (,]](_ioc.gif)                 
   |
189 | 186, 188 | mpbird 240 |
. . . . . . . . . . . . . . . . . . . 20
             ![(,] (,]](_ioc.gif)  
          |
190 | 176 | adantr 472 |
. . . . . . . . . . . . . . . . . . . 20
             ![(,] (,]](_ioc.gif)                 |
191 | 189, 190 | breqtrd 4420 |
. . . . . . . . . . . . . . . . . . 19
             ![(,] (,]](_ioc.gif)  
      |
192 | 179, 191 | resqrtcld 13556 |
. . . . . . . . . . . . . . . . . 18
             ![(,] (,]](_ioc.gif)             |
193 | 17, 192 | sylan 479 |
. . . . . . . . . . . . . . . . 17
         ![(,] (,]](_ioc.gif)             |
194 | | eleq1 2537 |
. . . . . . . . . . . . . . . . 17
        
            |
195 | 193, 194 | syl5ibrcom 230 |
. . . . . . . . . . . . . . . 16
         ![(,] (,]](_ioc.gif)               |
196 | 193 | renegcld 10067 |
. . . . . . . . . . . . . . . . 17
         ![(,] (,]](_ioc.gif)              |
197 | | eleq1 2537 |
. . . . . . . . . . . . . . . . 17
         
             |
198 | 196, 197 | syl5ibrcom 230 |
. . . . . . . . . . . . . . . 16
         ![(,] (,]](_ioc.gif)                |
199 | | eqid 2471 |
. . . . . . . . . . . . . . . . . 18
         |
200 | | eqsqrtor 13506 |
. . . . . . . . . . . . . . . . . . 19
                                      |
201 | 17, 200 | mpdan 681 |
. . . . . . . . . . . . . . . . . 18
         
                      |
202 | 199, 201 | mpbii 216 |
. . . . . . . . . . . . . . . . 17
                      |
203 | 202 | adantr 472 |
. . . . . . . . . . . . . . . 16
         ![(,] (,]](_ioc.gif)                        |
204 | 195, 198,
203 | mpjaod 388 |
. . . . . . . . . . . . . . 15
         ![(,] (,]](_ioc.gif)  
  |
205 | 204 | stoic1a 1663 |
. . . . . . . . . . . . . 14
 

       ![(,] (,]](_ioc.gif)    |
206 | 12, 205 | sylan 479 |
. . . . . . . . . . . . 13
 

       ![(,] (,]](_ioc.gif)    |
207 | 168, 206 | pm2.61dan 808 |
. . . . . . . . . . . 12
        ![(,] (,]](_ioc.gif)    |
208 | 116, 207 | eldifd 3401 |
. . . . . . . . . . 11
         ![(,] (,]](_ioc.gif)     |
209 | 208 | adantl 473 |
. . . . . . . . . 10
          ![(,] (,]](_ioc.gif)     |
210 | | 2cnd 10704 |
. . . . . . . . . . . . . 14
   |
211 | | id 22 |
. . . . . . . . . . . . . 14
   |
212 | 210, 211 | mulcld 9681 |
. . . . . . . . . . . . 13
     |
213 | 212 | negcld 9992 |
. . . . . . . . . . . 12
      |
214 | 213 | adantl 473 |
. . . . . . . . . . 11
       |
215 | 12, 214 | sylan2 482 |
. . . . . . . . . 10
       |
216 | 61 | sqrtcld 13576 |
. . . . . . . . . . 11
   ![(,] (,]](_ioc.gif)  
      |
217 | 216 | adantl 473 |
. . . . . . . . . 10
   ![(,] (,]](_ioc.gif)   
      |
218 | | ovex 6336 |
. . . . . . . . . . 11
         |
219 | 218 | a1i 11 |
. . . . . . . . . 10
   ![(,] (,]](_ioc.gif)   
          |
220 | 19 | adantl 473 |
. . . . . . . . . . 11
          |
221 | 37 | a1i 11 |
. . . . . . . . . . . . 13
    |
222 | | 1cnd 9677 |
. . . . . . . . . . . . . 14
  |
223 | 11, 222 | dvmptc 22991 |
. . . . . . . . . . . . 13
        |
224 | 17 | adantl 473 |
. . . . . . . . . . . . 13
        |
225 | | 2cn 10702 |
. . . . . . . . . . . . . . 15
 |
226 | | mulcl 9641 |
. . . . . . . . . . . . . . 15
 
     |
227 | 225, 226 | mpan 684 |
. . . . . . . . . . . . . 14
     |
228 | 227 | adantl 473 |
. . . . . . . . . . . . 13
      |
229 | | 2nn 10790 |
. . . . . . . . . . . . . . . 16
 |
230 | | dvexp 22986 |
. . . . . . . . . . . . . . . 16
                     |
231 | 229, 230 | ax-mp 5 |
. . . . . . . . . . . . . . 15
                   |
232 | | 2m1e1 10746 |
. . . . . . . . . . . . . . . . . . 19
   |
233 | 232 | oveq2i 6319 |
. . . . . . . . . . . . . . . . . 18
           |
234 | | exp1 12316 |
. . . . . . . . . . . . . . . . . 18
       |
235 | 233, 234 | syl5eq 2517 |
. . . . . . . . . . . . . . . . 17
         |
236 | 235 | oveq2d 6324 |
. . . . . . . . . . . . . . . 16
             |
237 | 236 | mpteq2ia 4478 |
. . . . . . . . . . . . . . 15
               |
238 | 231, 237 | eqtri 2493 |
. . . . . . . . . . . . . 14
             |
239 | 238 | a1i 11 |
. . . . . . . . . . . . 13
              |
240 | 11, 82, 221, 223, 224, 228, 239 | dvmptsub 23000 |
. . . . . . . . . . . 12
                  |
241 | | df-neg 9883 |
. . . . . . . . . . . . 13
        |
242 | 241 | mpteq2i 4479 |
. . . . . . . . . . . 12
            |
243 | 240, 242 | syl6eqr 2523 |
. . . . . . . . . . 11
                 |
244 | 11, 220, 214, 243, 84, 90, 85, 108 | dvmptres 22996 |
. . . . . . . . . 10
                 |
245 | | eqid 2471 |
. . . . . . . . . . . 12
  ![(,] (,]](_ioc.gif)     ![(,] (,]](_ioc.gif)    |
246 | 245 | dvcnsqrt 23763 |
. . . . . . . . . . 11
    ![(,] (,]](_ioc.gif)            ![(,] (,]](_ioc.gif)             |
247 | 246 | a1i 11 |
. . . . . . . . . 10
    ![(,] (,]](_ioc.gif)            ![(,] (,]](_ioc.gif)              |
248 | | fveq2 5879 |
. . . . . . . . . 10
                       |
249 | 248 | oveq2d 6324 |
. . . . . . . . . . 11
                           |
250 | 249 | oveq2d 6324 |
. . . . . . . . . 10
                               |
251 | 11, 11, 209, 215, 217, 219, 244, 247, 248, 250 | dvmptco 23005 |
. . . . . . . . 9
                                     |
252 | | mulneg2 10077 |
. . . . . . . . . . . . 13
 
         |
253 | 225, 12, 252 | sylancr 676 |
. . . . . . . . . . . 12
         |
254 | 253 | oveq1d 6323 |
. . . . . . . . . . 11
                                     |
255 | 12 | negcld 9992 |
. . . . . . . . . . . 12
    |
256 | | eldifn 3545 |
. . . . . . . . . . . . . . 15
    ![(,] (,]](_ioc.gif)    
  
  ![(,] (,]](_ioc.gif)         |
257 | 256, 3 | eleq2s 2567 |
. . . . . . . . . . . . . 14

  ![(,] (,]](_ioc.gif)         |
258 | | id 22 |
. . . . . . . . . . . . . . . . . 18
     |
259 | | mnflt 11448 |
. . . . . . . . . . . . . . . . . . . 20
     |
260 | 92, 259 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
  |
261 | | ubioc1 11713 |
. . . . . . . . . . . . . . . . . . 19
    
 ![(,] (,]](_ioc.gif)     |
262 | 52, 138, 260, 261 | mp3an 1390 |
. . . . . . . . . . . . . . . . . 18

 ![(,] (,]](_ioc.gif)    |
263 | 258, 262 | syl6eqel 2557 |
. . . . . . . . . . . . . . . . 17
 
 ![(,] (,]](_ioc.gif)     |
264 | | id 22 |
. . . . . . . . . . . . . . . . . 18
   |
265 | | ltpnf 11445 |
. . . . . . . . . . . . . . . . . . . 20
   |
266 | 95, 265 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
 |
267 | | lbico1 11714 |
. . . . . . . . . . . . . . . . . . 19
  
     |
268 | 139, 127,
266, 267 | mp3an 1390 |
. . . . . . . . . . . . . . . . . 18
    |
269 | 264, 268 | syl6eqel 2557 |
. . . . . . . . . . . . . . . . 17
      |
270 | 263, 269 | orim12i 525 |
. . . . . . . . . . . . . . . 16
  


 ![(,] (,]](_ioc.gif)         |
271 | 270 | orcoms 396 |
. . . . . . . . . . . . . . 15
   

 ![(,] (,]](_ioc.gif)         |
272 | | elun 3565 |
. . . . . . . . . . . . . . 15
   ![(,] (,]](_ioc.gif)      

 ![(,] (,]](_ioc.gif)         |
273 | 271, 272 | sylibr 217 |
. . . . . . . . . . . . . 14
   
  ![(,] (,]](_ioc.gif)    
    |
274 | 257, 273 | nsyl 125 |
. . . . . . . . . . . . 13
 
    |
275 | | 1cnd 9677 |
. . . . . . . . . . . . . . . . . 18
               |
276 | 17 | adantr 472 |
. . . . . . . . . . . . . . . . . 18
                   |
277 | 19 | adantr 472 |
. . . . . . . . . . . . . . . . . . 19
                     |
278 | | simpr 468 |
. . . . . . . . . . . . . . . . . . 19
                         |
279 | 277, 278 | sqr00d 13580 |
. . . . . . . . . . . . . . . . . 18
                     |
280 | 275, 276,
279 | subeq0d 10013 |
. . . . . . . . . . . . . . . . 17
                   |
281 | 152, 280 | syl5req 2518 |
. . . . . . . . . . . . . . . 16
                       |
282 | 281 | ex 441 |
. . . . . . . . . . . . . . 15
                       |
283 | | sqeqor 12426 |
. . . . . . . . . . . . . . . 16
 
                |
284 | 16, 283 | mpan2 685 |
. . . . . . . . . . . . . . 15
         
      |
285 | 282, 284 | sylibd 222 |
. . . . . . . . . . . . . 14
                  |
286 | 285 | necon3bd 2657 |
. . . . . . . . . . . . 13
                  |
287 | 12, 274, 286 | sylc 61 |
. . . . . . . . . . . 12
             |
288 | | 2cnne0 10847 |
. . . . . . . . . . . . 13
   |
289 | | divcan5 10331 |
. . . . . . . . . . . . 13
                           
                                |
290 | 288, 289 | mp3an3 1379 |
. . . . . . . . . . . 12
                                                          |
291 | 255, 117,
287, 290 | syl12anc 1290 |
. . . . . . . . . . 11
                                 |
292 | 225, 12, 226 | sylancr 676 |
. . . . . . . . . . . . 13
     |
293 | 292 | negcld 9992 |
. . . . . . . . . . . 12
      |
294 | | mulcl 9641 |
. . . . . . . . . . . . 13
                           |
295 | 225, 117,
294 | sylancr 676 |
. . . . . . . . . . . 12
               |
296 | | mulne0 10276 |
. . . . . . . . . . . . . 14
                          
              |
297 | 288, 296 | mpan 684 |
. . . . . . . . . . . . 13
                                     |
298 | 117, 287,
297 | syl2anc 673 |
. . . . . . . . . . . 12
               |
299 | 293, 295,
298 | divrec2d 10409 |
. . . . . . . . . . 11
                                       |
300 | 254, 291,
299 | 3eqtr3rd 2514 |
. . . . . . . . . 10
                                   |
301 | 300 | mpteq2ia 4478 |
. . . . . . . . 9
                                     |
302 | 251, 301 | syl6eq 2521 |
. . . . . . . 8
                               |
303 | 11, 77, 78, 114, 118, 120, 302 | dvmptadd 22993 |
. . . . . . 7
                                     |
304 | | mulcl 9641 |
. . . . . . . . . . . 12
                           |
305 | 13, 20, 304 | sylancr 676 |
. . . . . . . . . . 11
 
             |
306 | 12, 305 | syl 17 |
. . . . . . . . . 10
 
             |
307 | 306, 255,
117, 287 | divdird 10443 |
. . . . . . . . 9
                                                                     |
308 | | ixi 10263 |
. . . . . . . . . . . . . . . 16
    |
309 | 308 | eqcomi 2480 |
. . . . . . . . . . . . . . 15
    |
310 | 309 | oveq1i 6318 |
. . . . . . . . . . . . . 14
        |
311 | | mulm1 10081 |
. . . . . . . . . . . . . 14
       |
312 | | mulass 9645 |
. . . . . . . . . . . . . . 15
     
  
    |
313 | 13, 13, 312 | mp3an12 1380 |
. . . . . . . . . . . . . 14
   
  
    |
314 | 310, 311,
313 | 3eqtr3a 2529 |
. . . . . . . . . . . . 13
   
    |
315 | 314 | oveq1d 6323 |
. . . . . . . . . . . 12
                  
                 |
316 | | negcl 9895 |
. . . . . . . . . . . . 13
    |
317 | 305, 316 | addcomd 9853 |
. . . . . . . . . . . 12
                  
              |
318 | 13 | a1i 11 |
. . . . . . . . . . . . 13
   |
319 | 318, 15, 20 | adddid 9685 |
. . . . . . . . . . . 12
 
 
               
                 |
320 | 315, 317,
319 | 3eqtr4d 2515 |
. . . . . . . . . . 11
                                  |
321 | 12, 320 | syl 17 |
. . . . . . . . . 10
                                  |
322 | 321 | oveq1d 6323 |
. . . . . . . . 9
                                                          |
323 | 75, 117, 287 | divcan4d 10411 |
. . . . . . . . . 10
                           |
324 | 323 | oveq1d 6323 |
. . . . . . . . 9
                                                         |
325 | 307, 322,
324 | 3eqtr3rd 2514 |
. . . . . . . 8
                                              |
326 | 325 | mpteq2ia 4478 |
. . . . . . 7
                                                |
327 | 303, 326 | syl6eq 2521 |
. . . . . 6
                                                  |
328 | 245 | dvlog 23675 |
. . . . . . 7
    ![(,] (,]](_ioc.gif)        ![(,] (,]](_ioc.gif)       |
329 | | logf1o 23593 |
. . . . . . . . . 10
         |
330 | | f1of 5828 |
. . . . . . . . . 10
                
  |
331 | 329, 330 | mp1i 13 |
. . . . . . . . 9
       
  |
332 | | snssi 4107 |
. . . . . . . . . . 11
  ![(,] (,]](_ioc.gif)   
 ![(,] (,]](_ioc.gif)    |
333 | 66, 332 | ax-mp 5 |
. . . . . . . . . 10
 
 ![(,] (,]](_ioc.gif)   |
334 | | sscon 3556 |
. . . . . . . . . 10
    ![(,] (,]](_ioc.gif)    ![(,] (,]](_ioc.gif)         |
335 | 333, 334 | mp1i 13 |
. . . . . . . . 9
  ![(,] (,]](_ioc.gif)         |
336 | 331, 335 | feqresmpt 5933 |
. . . . . . . 8
   ![(,] (,]](_ioc.gif)       ![(,] (,]](_ioc.gif)          |
337 | 336 | oveq2d 6324 |
. . . . . . 7
    ![(,] (,]](_ioc.gif)         ![(,] (,]](_ioc.gif)           |
338 | 328, 337 | syl5reqr 2520 |
. . . . . 6
    ![(,] (,]](_ioc.gif)            ![(,] (,]](_ioc.gif)        |
339 | | fveq2 5879 |
. . . . . 6
                                       |
340 | | oveq2 6316 |
. . . . . 6
                                   |
341 | 11, 11, 58, 60, 72, 74, 327, 338, 339, 340 | dvmptco 23005 |
. . . . 5
                                                                        |
342 | 22, 24 | reccld 10398 |
. . . . . . . 8
                   |
343 | | mulcl 9641 |
. . . . . . . . . 10
                                   |
344 | 13, 21, 343 | sylancr 676 |
. . . . . . . . 9
 
 
               |
345 | 12, 344 | syl 17 |
. . . . . . . 8
 
 
               |
346 | 342, 345,
117, 287 | divassd 10440 |
. . . . . . 7
                   
 
                                                                         |
347 | 345, 22, 24 | divrec2d 10409 |
. . . . . . . . 9
                                                  
 
                |
348 | 75, 22, 24 | divcan4d 10411 |
. . . . . . . . 9
                                   |
349 | 347, 348 | eqtr3d 2507 |
. . . . . . . 8
                                     |
350 | 349 | oveq1d 6323 |
. . . . . . 7
                   
 
                                       |
351 | 346, 350 | eqtr3d 2507 |
. . . . . 6
                                                             |
352 | 351 | mpteq2ia 4478 |
. . . . 5
                                                               |
353 | 341, 352 | syl6eq 2521 |
. . . 4
                                      |
354 | | negicn 9896 |
. . . . 5
  |
355 | 354 | a1i 11 |
. . . 4
   |
356 | 11, 26, 28, 353, 355 | dvmptcmul 22997 |
. . 3
                            
               |
357 | 356 | trud 1461 |
. 2
                            
              |
358 | 13, 13 | mulneg1i 10085 |
. . . . . 6
       |
359 | 308 | negeqi 9888 |
. . . . . 6
 
    |
360 | | negneg1e1 10739 |
. . . . . 6
   |
361 | 358, 359,
360 | 3eqtri 2497 |
. . . . 5
    |
362 | 361 | oveq1i 6318 |
. . . 4
                            |
363 | | divass 10310 |
. . . . . 6
                                           
              |
364 | 354, 13, 363 | mp3an12 1380 |
. . . . 5
                                                       |
365 | 117, 287,
364 | syl2anc 673 |
. . . 4
                  
              |
366 | 362, 365 | syl5reqr 2520 |
. . 3
                              |
367 | 366 | mpteq2ia 4478 |
. 2
                                |
368 | 9, 357, 367 | 3eqtri 2497 |
1
 arcsin
                 |