Step | Hyp | Ref
| Expression |
1 | | cosf 14256 |
. . . 4
     |
2 | | ffun 5742 |
. . . 4
       |
3 | | difpreima 6023 |
. . . 4
                          |
4 | 1, 2, 3 | mp2b 10 |
. . 3
                        |
5 | | fimacnv 6027 |
. . . . 5
            |
6 | 1, 5 | ax-mp 5 |
. . . 4
      |
7 | | 0re 9661 |
. . . . . 6
 |
8 | | ffn 5739 |
. . . . . . . . 9
       |
9 | 1, 8 | ax-mp 5 |
. . . . . . . 8
 |
10 | | dffn5 5924 |
. . . . . . . 8

        |
11 | 9, 10 | mpbi 213 |
. . . . . . 7

      |
12 | 11 | mptiniseg 5336 |
. . . . . 6
                |
13 | 7, 12 | ax-mp 5 |
. . . . 5
              |
14 | | sinhalfpip 23526 |
. . . . . . . 8
               |
15 | 14 | eqeq1d 2473 |
. . . . . . 7
                 |
16 | | halfpire 23498 |
. . . . . . . . . 10
   |
17 | 16 | recni 9673 |
. . . . . . . . 9
   |
18 | | addcl 9639 |
. . . . . . . . 9
   
       |
19 | 17, 18 | mpan 684 |
. . . . . . . 8
       |
20 | | sineq0 23555 |
. . . . . . . 8
                       |
21 | 19, 20 | syl 17 |
. . . . . . 7
                   |
22 | 15, 21 | bitr3d 263 |
. . . . . 6
               |
23 | 22 | rabbiia 3019 |
. . . . 5
               |
24 | 13, 23 | eqtri 2493 |
. . . 4
             
  |
25 | 6, 24 | difeq12i 3538 |
. . 3
                         |
26 | 4, 25 | eqtri 2493 |
. 2
                    |
27 | | eqid 2471 |
. . . . 5
  ℂfld   ℂfld |
28 | 27 | recld2 21910 |
. . . 4
     ℂfld  |
29 | | nftru 1685 |
. . . . . . . . 9
  |
30 | | nfcv 2612 |
. . . . . . . . 9
  
    
              |
31 | | nfcv 2612 |
. . . . . . . . . 10
   |
32 | | nfrab1 2957 |
. . . . . . . . . 10
  
     
  |
33 | 31, 32 | nfdif 3543 |
. . . . . . . . 9
         
   |
34 | | eliun 4274 |
. . . . . . . . . . 11
                
  
     
               |
35 | | elioore 11691 |
. . . . . . . . . . . . . . 15
               
     |
36 | 35 | adantl 473 |
. . . . . . . . . . . . . 14
 
              
      |
37 | | zre 10965 |
. . . . . . . . . . . . . . . . . . 19
   |
38 | | pire 23492 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 |
39 | | remulcl 9642 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
     |
40 | 38, 39 | mpan 684 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
   |
41 | | resubcl 9958 |
. . . . . . . . . . . . . . . . . . . . . . 23
    
     
    |
42 | 40, 16, 41 | sylancl 675 |
. . . . . . . . . . . . . . . . . . . . . 22
         |
43 | 42 | rexrd 9708 |
. . . . . . . . . . . . . . . . . . . . 21
         |
44 | | peano2re 9824 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     |
45 | | remulcl 9642 |
. . . . . . . . . . . . . . . . . . . . . . . 24
           |
46 | 38, 44, 45 | sylancr 676 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
     |
47 | | resubcl 9958 |
. . . . . . . . . . . . . . . . . . . . . . 23
      
       
    |
48 | 46, 16, 47 | sylancl 675 |
. . . . . . . . . . . . . . . . . . . . . 22
           |
49 | 48 | rexrd 9708 |
. . . . . . . . . . . . . . . . . . . . 21
           |
50 | | elioo2 11702 |
. . . . . . . . . . . . . . . . . . . . 21
     
                          
  
      
            |
51 | 43, 49, 50 | syl2anc 673 |
. . . . . . . . . . . . . . . . . . . 20
                
  
      
            |
52 | | ltadd2 9756 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
     
 

      
                   |
53 | 16, 52 | mp3an3 1379 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
     
 
     
                   |
54 | 42, 53 | sylan 479 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
     
                   |
55 | | readdcl 9640 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
       
         
     |
56 | 16, 42, 55 | sylancr 676 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
             |
57 | | readdcl 9640 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
   
       |
58 | 16, 57 | mpan 684 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
       |
59 | | pipos 23494 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 |
60 | 38, 59 | pm3.2i 462 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
   |
61 | | ltdiv1 10491 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
                
 
              
                     |
62 | 60, 61 | mp3an3 1379 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                        
              
   
         |
63 | 56, 58, 62 | syl2an 485 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
        
              
             |
64 | | recn 9647 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
   |
65 | | picn 23493 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
 |
66 | | mulcl 9641 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
 
     |
67 | 65, 66 | mpan 684 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
 
   |
68 | | pncan3 9903 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
    
        
       |
69 | 17, 67, 68 | sylancr 676 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
               |
70 | 69 | oveq1d 6323 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
                   |
71 | 7, 59 | gtneii 9764 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
 |
72 | | divcan3 10316 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
         |
73 | 65, 71, 72 | mp3an23 1382 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
       |
74 | 70, 73 | eqtrd 2505 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
               |
75 | 64, 74 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
               |
76 | 75 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
        
   
  |
77 | 76 | breq1d 4405 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
         
   
     
         |
78 | 54, 63, 77 | 3bitrd 287 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
     
           |
79 | 38, 45 | mpan 684 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
   
     |
80 | 79, 16, 47 | sylancl 675 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
             |
81 | | ltadd2 9756 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
       
  
        
                     |
82 | 16, 81 | mp3an3 1379 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
       
         
                     |
83 | 80, 82 | sylan2 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
           
                     |
84 | | readdcl 9640 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
         
           
     |
85 | 16, 80, 84 | sylancr 676 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
                 |
86 | | ltdiv1 10491 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
                  
 
             
  
               
       |
87 | 60, 86 | mp3an3 1379 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
                                         
                 |
88 | 58, 85, 87 | syl2an 485 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
                           
                 |
89 | | recn 9647 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
       |
90 | | mulcl 9641 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
           |
91 | 65, 90 | mpan 684 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
   
     |
92 | | pncan3 9903 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
    
            
         |
93 | 17, 91, 92 | sylancr 676 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
                     |
94 | 93 | oveq1d 6323 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
                         |
95 | | divcan3 10316 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
               |
96 | 65, 71, 95 | mp3an23 1382 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
             |
97 | 94, 96 | eqtrd 2505 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
                     |
98 | 89, 97 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
                     |
99 | 98 | adantl 473 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
              
   
    |
100 | 99 | breq2d 4407 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
                     
               |
101 | 83, 88, 100 | 3bitrd 287 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
           
       
     |
102 | 44, 101 | sylan2 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
                     |
103 | 102 | ancoms 460 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
                     |
104 | 78, 103 | anbi12d 725 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
        
                     
      |
105 | 104 | biimpd 212 |
. . . . . . . . . . . . . . . . . . . . . 22
 
        
        
            
      |
106 | 105 | exp4b 618 |
. . . . . . . . . . . . . . . . . . . . 21
      
                       
        |
107 | 106 | 3impd 1247 |
. . . . . . . . . . . . . . . . . . . 20
      
       
               
      |
108 | 51, 107 | sylbid 223 |
. . . . . . . . . . . . . . . . . . 19
                
               
      |
109 | 37, 108 | syl 17 |
. . . . . . . . . . . . . . . . . 18
                
               
      |
110 | 109 | imp 436 |
. . . . . . . . . . . . . . . . 17
 
              
                
     |
111 | | btwnnz 11035 |
. . . . . . . . . . . . . . . . . 18
       
              
  |
112 | 111 | 3expb 1232 |
. . . . . . . . . . . . . . . . 17
              
   
        |
113 | 110, 112 | syldan 478 |
. . . . . . . . . . . . . . . 16
 
              
   
        |
114 | 113 | olcd 400 |
. . . . . . . . . . . . . . 15
 
              
              |
115 | | ianor 496 |
. . . . . . . . . . . . . . . 16
       
       
   |
116 | | rabid 2953 |
. . . . . . . . . . . . . . . 16
        
          |
117 | 115, 116 | xchnxbir 316 |
. . . . . . . . . . . . . . 15
        

     
   |
118 | 114, 117 | sylibr 217 |
. . . . . . . . . . . . . 14
 
              
   
      
   |
119 | 36, 118 | eldifd 3401 |
. . . . . . . . . . . . 13
 
              
                |
120 | 119 | rexlimiva 2868 |
. . . . . . . . . . . 12
      
            

           |
121 | | eldif 3400 |
. . . . . . . . . . . . . 14
  
     
 
       
    |
122 | | recn 9647 |
. . . . . . . . . . . . . . . . . 18
   |
123 | 122 | biantrurd 516 |
. . . . . . . . . . . . . . . . 17
       
           |
124 | 123, 116 | syl6bbr 271 |
. . . . . . . . . . . . . . . 16
       
      
    |
125 | 124 | notbid 301 |
. . . . . . . . . . . . . . 15
       
      
    |
126 | 125 | pm5.32i 649 |
. . . . . . . . . . . . . 14
       
 
           |
127 | 121, 126 | bitr4i 260 |
. . . . . . . . . . . . 13
  
     
 
          |
128 | | redivcl 10348 |
. . . . . . . . . . . . . . . . . 18
               |
129 | 38, 71, 128 | mp3an23 1382 |
. . . . . . . . . . . . . . . . 17
             |
130 | 58, 129 | syl 17 |
. . . . . . . . . . . . . . . 16
         |
131 | 130 | flcld 12067 |
. . . . . . . . . . . . . . 15
             |
132 | 131 | adantr 472 |
. . . . . . . . . . . . . 14
       
             |
133 | | simpl 464 |
. . . . . . . . . . . . . . 15
       
   |
134 | | flle 12068 |
. . . . . . . . . . . . . . . . . . 19
                         |
135 | 130, 134 | syl 17 |
. . . . . . . . . . . . . . . . . 18
                   |
136 | 135 | adantr 472 |
. . . . . . . . . . . . . . . . 17
       
          
        |
137 | | nelne2 2740 |
. . . . . . . . . . . . . . . . . . 19
                 
                   |
138 | 137 | necomd 2698 |
. . . . . . . . . . . . . . . . . 18
                 
                   |
139 | 131, 138 | sylan 479 |
. . . . . . . . . . . . . . . . 17
       
                   |
140 | 131 | zred 11063 |
. . . . . . . . . . . . . . . . . . . 20
             |
141 | | pirp 23495 |
. . . . . . . . . . . . . . . . . . . . 21
 |
142 | 141 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
   |
143 | 140, 130,
142 | ltmul2d 11403 |
. . . . . . . . . . . . . . . . . . 19
                 
            
          |
144 | 140, 130 | ltlend 9797 |
. . . . . . . . . . . . . . . . . . 19
                 
                      
              |
145 | | remulcl 9642 |
. . . . . . . . . . . . . . . . . . . . 21
                           |
146 | 38, 140, 145 | sylancr 676 |
. . . . . . . . . . . . . . . . . . . 20
 
             |
147 | | remulcl 9642 |
. . . . . . . . . . . . . . . . . . . . 21
       
           |
148 | 38, 130, 147 | sylancr 676 |
. . . . . . . . . . . . . . . . . . . 20
 
         |
149 | 16 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
 
   |
150 | 146, 148,
149 | ltsub1d 10243 |
. . . . . . . . . . . . . . . . . . 19
                                   
                 |
151 | 143, 144,
150 | 3bitr3rd 292 |
. . . . . . . . . . . . . . . . . 18
                           
                        
              |
152 | 151 | adantr 472 |
. . . . . . . . . . . . . . . . 17
       
               
                                    
              |
153 | 136, 139,
152 | mpbir2and 936 |
. . . . . . . . . . . . . . . 16
       
                          
    |
154 | | divcan2 10300 |
. . . . . . . . . . . . . . . . . . . . . 22
       
             |
155 | 65, 71, 154 | mp3an23 1382 |
. . . . . . . . . . . . . . . . . . . . 21
     
             |
156 | 19, 155 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
 
             |
157 | 156 | oveq1d 6323 |
. . . . . . . . . . . . . . . . . . 19
                  
    |
158 | | pncan2 9902 |
. . . . . . . . . . . . . . . . . . . 20
   
      
    |
159 | 17, 158 | mpan 684 |
. . . . . . . . . . . . . . . . . . 19
           |
160 | 157, 159 | eqtrd 2505 |
. . . . . . . . . . . . . . . . . 18
               |
161 | 122, 160 | syl 17 |
. . . . . . . . . . . . . . . . 17
               |
162 | 161 | adantr 472 |
. . . . . . . . . . . . . . . 16
       
          
    |
163 | 153, 162 | breqtrd 4420 |
. . . . . . . . . . . . . . 15
       
                   |
164 | | peano2re 9824 |
. . . . . . . . . . . . . . . . . . . 20
                         |
165 | 140, 164 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
               |
166 | | remulcl 9642 |
. . . . . . . . . . . . . . . . . . 19
                               |
167 | 38, 165, 166 | sylancr 676 |
. . . . . . . . . . . . . . . . . 18
 
               |
168 | | flltp1 12069 |
. . . . . . . . . . . . . . . . . . . 20
                           |
169 | 130, 168 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
                     |
170 | 130, 165,
142, 169 | ltmul2dd 11417 |
. . . . . . . . . . . . . . . . . 18
 
                       |
171 | 148, 167,
149, 170 | ltsub1dd 10246 |
. . . . . . . . . . . . . . . . 17
                            
    |
172 | 161, 171 | eqbrtrrd 4418 |
. . . . . . . . . . . . . . . 16
                
    |
173 | 172 | adantr 472 |
. . . . . . . . . . . . . . 15
       
                     |
174 | | resubcl 9958 |
. . . . . . . . . . . . . . . . . . 19
                              
    |
175 | 146, 16, 174 | sylancl 675 |
. . . . . . . . . . . . . . . . . 18
              
    |
176 | 175 | rexrd 9708 |
. . . . . . . . . . . . . . . . 17
              
    |
177 | | resubcl 9958 |
. . . . . . . . . . . . . . . . . . 19
                
                 
    |
178 | 167, 16, 177 | sylancl 675 |
. . . . . . . . . . . . . . . . . 18
                     |
179 | 178 | rexrd 9708 |
. . . . . . . . . . . . . . . . 17
                     |
180 | | elioo2 11702 |
. . . . . . . . . . . . . . . . 17
                 
                                  
                                     
 
                      |
181 | 176, 179,
180 | syl2anc 673 |
. . . . . . . . . . . . . . . 16
                
                                     
 
                      |
182 | 181 | adantr 472 |
. . . . . . . . . . . . . . 15
       
                                    
  
              
 
                      |
183 | 133, 163,
173, 182 | mpbir3and 1213 |
. . . . . . . . . . . . . 14
       
               
                         |
184 | | oveq2 6316 |
. . . . . . . . . . . . . . . . . 18
           
               |
185 | 184 | oveq1d 6323 |
. . . . . . . . . . . . . . . . 17
                              
    |
186 | | oveq1 6315 |
. . . . . . . . . . . . . . . . . . 19
                           |
187 | 186 | oveq2d 6324 |
. . . . . . . . . . . . . . . . . 18
           
                   |
188 | 187 | oveq1d 6323 |
. . . . . . . . . . . . . . . . 17
                                  
    |
189 | 185, 188 | oveq12d 6326 |
. . . . . . . . . . . . . . . 16
               
                           
                         |
190 | 189 | eleq2d 2534 |
. . . . . . . . . . . . . . 15
                          
  
              
                          |
191 | 190 | rspcev 3136 |
. . . . . . . . . . . . . 14
           
              
                             
               |
192 | 132, 183,
191 | syl2anc 673 |
. . . . . . . . . . . . 13
       
 
              
     |
193 | 127, 192 | sylbi 200 |
. . . . . . . . . . . 12
  
     
       
               |
194 | 120, 193 | impbii 192 |
. . . . . . . . . . 11
      
            
            |
195 | 34, 194 | bitri 257 |
. . . . . . . . . 10
                
  

           |
196 | 195 | a1i 11 |
. . . . . . . . 9
 
    
                          |
197 | 29, 30, 33, 196 | eqrd 3436 |
. . . . . . . 8
     
                         |
198 | 197 | trud 1461 |
. . . . . . 7
               
              |
199 | | retop 21860 |
. . . . . . . 8
     |
200 | | iooretop 21864 |
. . . . . . . . 9
              
        |
201 | 200 | rgenw 2768 |
. . . . . . . 8
               
        |
202 | | iunopn 20005 |
. . . . . . . 8
                     
       
               
         |
203 | 199, 201,
202 | mp2an 686 |
. . . . . . 7
               
        |
204 | 198, 203 | eqeltrri 2546 |
. . . . . 6
               |
205 | | rabss 3492 |
. . . . . . . 8
       
        
   |
206 | | zre 10965 |
. . . . . . . . . . 11
               |
207 | | remulcl 9642 |
. . . . . . . . . . 11
       
       
   |
208 | 206, 38, 207 | sylancl 675 |
. . . . . . . . . 10
             
   |
209 | | resubcl 9958 |
. . . . . . . . . 10
        


           
    |
210 | 208, 16, 209 | sylancl 675 |
. . . . . . . . 9
              

     |
211 | | divcan1 10301 |
. . . . . . . . . . . . . 14
             
       |
212 | 65, 71, 211 | mp3an23 1382 |
. . . . . . . . . . . . 13
           
       |
213 | 19, 212 | syl 17 |
. . . . . . . . . . . 12
       
       |
214 | 213 | oveq1d 6323 |
. . . . . . . . . . 11
        

        
    |
215 | 214, 159 | eqtrd 2505 |
. . . . . . . . . 10
        

     |
216 | 215 | eleq1d 2533 |
. . . . . . . . 9
           
 
   |
217 | 210, 216 | syl5ib 227 |
. . . . . . . 8
       
   |
218 | 205, 217 | mprgbir 2771 |
. . . . . . 7
         |
219 | | uniretop 21861 |
. . . . . . . 8
      |
220 | 219 | iscld2 20120 |
. . . . . . 7
                               
       
         |
221 | 199, 218,
220 | mp2an 686 |
. . . . . 6
       
        
       
        |
222 | 204, 221 | mpbir 214 |
. . . . 5
                 |
223 | 27 | tgioo2 21899 |
. . . . . 6
       ℂfld
↾t   |
224 | 223 | fveq2i 5882 |
. . . . 5
              ℂfld
↾t    |
225 | 222, 224 | eleqtri 2547 |
. . . 4
              ℂfld ↾t    |
226 | | restcldr 20267 |
. . . 4
       ℂfld       
       ℂfld ↾t                 ℂfld   |
227 | 28, 225, 226 | mp2an 686 |
. . 3
             ℂfld  |
228 | 27 | cnfldtopon 21881 |
. . . . 5
  ℂfld TopOn   |
229 | 228 | toponunii 20024 |
. . . 4
   ℂfld |
230 | 229 | cldopn 20123 |
. . 3
       
      ℂfld             ℂfld  |
231 | 227, 230 | ax-mp 5 |
. 2
            ℂfld |
232 | 26, 231 | eqeltri 2545 |
1
           ℂfld |