Step | Hyp | Ref
| Expression |
1 | | fourierdlem62.k |
. . . 4
    ![[,] [,]](_icc.gif)                   |
2 | | eqeq1 2454 |
. . . . . 6
     |
3 | | id 22 |
. . . . . . 7
   |
4 | | oveq1 6295 |
. . . . . . . . 9
       |
5 | 4 | fveq2d 5867 |
. . . . . . . 8
               |
6 | 5 | oveq2d 6304 |
. . . . . . 7
                   |
7 | 3, 6 | oveq12d 6306 |
. . . . . 6
                       |
8 | 2, 7 | ifbieq2d 3905 |
. . . . 5
                                 |
9 | 8 | cbvmptv 4494 |
. . . 4
    ![[,] [,]](_icc.gif)                      ![[,] [,]](_icc.gif)                   |
10 | 1, 9 | eqtri 2472 |
. . 3
    ![[,] [,]](_icc.gif)                   |
11 | 10 | fourierdlem43 38008 |
. 2
     ![[,] [,]](_icc.gif)     |
12 | | ax-resscn 9593 |
. . 3
 |
13 | | fss 5735 |
. . . . . 6
       ![[,] [,]](_icc.gif)   
      ![[,] [,]](_icc.gif)      |
14 | 11, 12, 13 | mp2an 677 |
. . . . 5
     ![[,] [,]](_icc.gif)     |
15 | 14 | a1i 11 |
. . . . . . . . 9
      ![[,] [,]](_icc.gif)      |
16 | | difss 3559 |
. . . . . . . . . . . . . . . . 17
        
      |
17 | | elioore 11663 |
. . . . . . . . . . . . . . . . . 18
        |
18 | 17 | ssriv 3435 |
. . . . . . . . . . . . . . . . 17
      |
19 | 16, 18 | sstri 3440 |
. . . . . . . . . . . . . . . 16
        
 |
20 | 19 | a1i 11 |
. . . . . . . . . . . . . . 15
           |
21 | | eqid 2450 |
. . . . . . . . . . . . . . . . 17
                       |
22 | 19 | sseli 3427 |
. . . . . . . . . . . . . . . . 17
            |
23 | 21, 22 | fmpti 6043 |
. . . . . . . . . . . . . . . 16
                  
      |
24 | 23 | a1i 11 |
. . . . . . . . . . . . . . 15
      
                   |
25 | | eqid 2450 |
. . . . . . . . . . . . . . . . 17
                                       |
26 | | 2re 10676 |
. . . . . . . . . . . . . . . . . . 19
 |
27 | 26 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
            |
28 | 22 | rehalfcld 10856 |
. . . . . . . . . . . . . . . . . . 19
              |
29 | 28 | resincld 14190 |
. . . . . . . . . . . . . . . . . 18
                  |
30 | 27, 29 | remulcld 9668 |
. . . . . . . . . . . . . . . . 17
                    |
31 | 25, 30 | fmpti 6043 |
. . . . . . . . . . . . . . . 16
                                 |
32 | 31 | a1i 11 |
. . . . . . . . . . . . . . 15
      
                           |
33 | | iooretop 21779 |
. . . . . . . . . . . . . . . 16
          |
34 | 33 | a1i 11 |
. . . . . . . . . . . . . . 15
    
  
   |
35 | | 0re 9640 |
. . . . . . . . . . . . . . . . 17
 |
36 | | negpilt0 37484 |
. . . . . . . . . . . . . . . . 17
  |
37 | | pipos 23408 |
. . . . . . . . . . . . . . . . 17
 |
38 | | pire 23406 |
. . . . . . . . . . . . . . . . . . . 20
 |
39 | 38 | renegcli 9932 |
. . . . . . . . . . . . . . . . . . 19
  |
40 | 39 | rexri 9690 |
. . . . . . . . . . . . . . . . . 18
  |
41 | 38 | rexri 9690 |
. . . . . . . . . . . . . . . . . 18
 |
42 | | elioo2 11674 |
. . . . . . . . . . . . . . . . . 18
           
    |
43 | 40, 41, 42 | mp2an 677 |
. . . . . . . . . . . . . . . . 17
     
     |
44 | 35, 36, 37, 43 | mpbir3an 1189 |
. . . . . . . . . . . . . . . 16
      |
45 | 44 | a1i 11 |
. . . . . . . . . . . . . . 15
       |
46 | | eqid 2450 |
. . . . . . . . . . . . . . 15
                   |
47 | | 1ex 9635 |
. . . . . . . . . . . . . . . . . . 19
 |
48 | | eqid 2450 |
. . . . . . . . . . . . . . . . . . 19
                       |
49 | 47, 48 | dmmpti 5705 |
. . . . . . . . . . . . . . . . . 18
                     |
50 | | reelprrecn 9628 |
. . . . . . . . . . . . . . . . . . . . . . 23
    |
51 | 50 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
     |
52 | 12 | sseli 3427 |
. . . . . . . . . . . . . . . . . . . . . . 23
   |
53 | 52 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . 22
    |
54 | | 1red 9655 |
. . . . . . . . . . . . . . . . . . . . . 22
    |
55 | 51 | dvmptid 22904 |
. . . . . . . . . . . . . . . . . . . . . 22
        |
56 | | eqid 2450 |
. . . . . . . . . . . . . . . . . . . . . . 23
  ℂfld   ℂfld |
57 | 56 | tgioo2 21814 |
. . . . . . . . . . . . . . . . . . . . . 22
       ℂfld
↾t   |
58 | | sncldre 37367 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
             |
59 | 35, 58 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . 24
           |
60 | | retopon 21777 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
    TopOn   |
61 | 60 | toponunii 19940 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
      |
62 | 61 | difopn 20042 |
. . . . . . . . . . . . . . . . . . . . . . . 24
      
  
                           |
63 | 33, 59, 62 | mp2an 677 |
. . . . . . . . . . . . . . . . . . . . . . 23
              |
64 | 63 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
               |
65 | 51, 53, 54, 55, 20, 57, 56, 64 | dvmptres 22910 |
. . . . . . . . . . . . . . . . . . . . 21
                          |
66 | 65 | trud 1452 |
. . . . . . . . . . . . . . . . . . . 20
                         |
67 | 66 | eqcomi 2459 |
. . . . . . . . . . . . . . . . . . 19
                         |
68 | 67 | dmeqi 5035 |
. . . . . . . . . . . . . . . . . 18
            
            |
69 | 49, 68 | eqtr3i 2474 |
. . . . . . . . . . . . . . . . 17
                       |
70 | 69 | eqimssi 3485 |
. . . . . . . . . . . . . . . 16
        
              |
71 | 70 | a1i 11 |
. . . . . . . . . . . . . . 15
                        |
72 | | fvex 5873 |
. . . . . . . . . . . . . . . . . . 19
       |
73 | | eqid 2450 |
. . . . . . . . . . . . . . . . . . 19
                                   |
74 | 72, 73 | dmmpti 5705 |
. . . . . . . . . . . . . . . . . 18
                      
    |
75 | | 2cnd 10679 |
. . . . . . . . . . . . . . . . . . . . . . 23
    |
76 | 53 | halfcld 10854 |
. . . . . . . . . . . . . . . . . . . . . . . 24
      |
77 | 76 | sincld 14177 |
. . . . . . . . . . . . . . . . . . . . . . 23
          |
78 | 75, 77 | mulcld 9660 |
. . . . . . . . . . . . . . . . . . . . . 22
            |
79 | 76 | coscld 14178 |
. . . . . . . . . . . . . . . . . . . . . 22
          |
80 | | 2cnd 10679 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
   |
81 | | 2ne0 10699 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
 |
82 | 81 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
   |
83 | 52, 80, 82 | divrec2d 10384 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
         |
84 | 83 | fveq2d 5867 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
                 |
85 | 84 | oveq2d 6304 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                     |
86 | 85 | mpteq2ia 4484 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                       |
87 | 86 | oveq2i 6299 |
. . . . . . . . . . . . . . . . . . . . . . . 24
             
             |
88 | | resmpt 5153 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28

                            |
89 | 12, 88 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
                           |
90 | 89 | eqcomi 2459 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                           |
91 | 90 | oveq2i 6299 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                               |
92 | | eqid 2450 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
                         |
93 | | 2cnd 10679 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
   |
94 | | halfcn 10826 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
   |
95 | 94 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
     |
96 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
   |
97 | 95, 96 | mulcld 9660 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
       |
98 | 97 | sincld 14177 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
           |
99 | 93, 98 | mulcld 9660 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
             |
100 | 92, 99 | fmpti 6043 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                 |
101 | | eqid 2450 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
                                 |
102 | | 2cn 10677 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
 |
103 | 102, 94 | mulcli 9645 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
     |
104 | 103 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
       |
105 | 97 | coscld 14178 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
           |
106 | 104, 105 | mulcld 9660 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
                 |
107 | 106 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
                  |
108 | 101, 107 | dmmptd 5706 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
                  |
109 | 108 | trud 1452 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
                 |
110 | 12, 109 | sseqtr4i 3464 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
                 |
111 | | dvasinbx 37786 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
      
                              |
112 | 102, 94, 111 | mp2an 677 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
                               |
113 | 112 | dmeqi 5035 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
                               |
114 | 110, 113 | sseqtr4i 3464 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
               |
115 | | dvcnre 37780 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                                
                              
   |
116 | 100, 114,
115 | mp2an 677 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                              
  |
117 | 112 | reseq1i 5100 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                                
  |
118 | | resmpt 5153 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27

                                    |
119 | 12, 118 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                                   |
120 | 102, 81 | recidi 10335 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
     |
121 | 120 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
       |
122 | 83 | eqcomd 2456 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
         |
123 | 122 | fveq2d 5867 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
                 |
124 | 121, 123 | oveq12d 6306 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
                         |
125 | 52 | halfcld 10854 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
     |
126 | 125 | coscld 14178 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
         |
127 | 126 | mulid2d 9658 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
                 |
128 | 124, 127 | eqtrd 2484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
                       |
129 | 128 | mpteq2ia 4484 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                         |
130 | 117, 119,
129 | 3eqtri 2476 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                         |
131 | 91, 116, 130 | 3eqtri 2476 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                       |
132 | 87, 131 | eqtri 2472 |
. . . . . . . . . . . . . . . . . . . . . . 23
                     |
133 | 132 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
                      |
134 | 51, 78, 79, 133, 20, 57, 56, 64 | dvmptres 22910 |
. . . . . . . . . . . . . . . . . . . . 21
                                        |
135 | 134 | trud 1452 |
. . . . . . . . . . . . . . . . . . . 20
                                       |
136 | 135 | eqcomi 2459 |
. . . . . . . . . . . . . . . . . . 19
                                       |
137 | 136 | dmeqi 5035 |
. . . . . . . . . . . . . . . . . 18
                 
                     |
138 | 74, 137 | eqtr3i 2474 |
. . . . . . . . . . . . . . . . 17
                               |
139 | 138 | eqimssi 3485 |
. . . . . . . . . . . . . . . 16
        
                      |
140 | 139 | a1i 11 |
. . . . . . . . . . . . . . 15
                                |
141 | 17 | recnd 9666 |
. . . . . . . . . . . . . . . . . . . . . . . 24
        |
142 | 141 | ssriv 3435 |
. . . . . . . . . . . . . . . . . . . . . . 23
      |
143 | 142 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
    
  |
144 | | ssid 3450 |
. . . . . . . . . . . . . . . . . . . . . . 23
 |
145 | 144 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
  |
146 | 143, 145 | idcncfg 37743 |
. . . . . . . . . . . . . . . . . . . . 21
                  |
147 | 146 | trud 1452 |
. . . . . . . . . . . . . . . . . . . 20
                 |
148 | | cnlimc 22836 |
. . . . . . . . . . . . . . . . . . . . 21
                             
                                    lim      |
149 | 142, 148 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
                
                                         
 lim     |
150 | 147, 149 | mpbi 212 |
. . . . . . . . . . . . . . . . . . 19
                                         
 lim    |
151 | 150 | simpri 464 |
. . . . . . . . . . . . . . . . . 18
                        
 lim   |
152 | | fveq2 5863 |
. . . . . . . . . . . . . . . . . . . 20
                         |
153 | | oveq2 6296 |
. . . . . . . . . . . . . . . . . . . 20
         lim          lim    |
154 | 152, 153 | eleq12d 2522 |
. . . . . . . . . . . . . . . . . . 19
        
          
 lim 
                   lim     |
155 | 154 | rspccva 3148 |
. . . . . . . . . . . . . . . . . 18
                          
 lim 
            
          
 lim    |
156 | 151, 44, 155 | mp2an 677 |
. . . . . . . . . . . . . . . . 17
                   lim   |
157 | | id 22 |
. . . . . . . . . . . . . . . . . . 19
   |
158 | | eqid 2450 |
. . . . . . . . . . . . . . . . . . 19
            
  |
159 | | c0ex 9634 |
. . . . . . . . . . . . . . . . . . 19
 |
160 | 157, 158,
159 | fvmpt 5946 |
. . . . . . . . . . . . . . . . . 18
                   |
161 | 44, 160 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
            |
162 | | elioore 11663 |
. . . . . . . . . . . . . . . . . . . . . . 23
        |
163 | 162 | recnd 9666 |
. . . . . . . . . . . . . . . . . . . . . 22
        |
164 | 158, 163 | fmpti 6043 |
. . . . . . . . . . . . . . . . . . . . 21
                 |
165 | 164 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
                  |
166 | 165 | limcdif 22824 |
. . . . . . . . . . . . . . . . . . 19
      
 lim                     lim    |
167 | 166 | trud 1452 |
. . . . . . . . . . . . . . . . . 18
        lim          
          lim   |
168 | | resmpt 5153 |
. . . . . . . . . . . . . . . . . . . 20
      
                                       |
169 | 16, 168 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
       
                      |
170 | 169 | oveq1i 6298 |
. . . . . . . . . . . . . . . . . 18
                   lim              lim   |
171 | 167, 170 | eqtri 2472 |
. . . . . . . . . . . . . . . . 17
        lim              lim   |
172 | 156, 161,
171 | 3eltr3i 2540 |
. . . . . . . . . . . . . . . 16
            lim   |
173 | 172 | a1i 11 |
. . . . . . . . . . . . . . 15
       
    lim    |
174 | | eqid 2450 |
. . . . . . . . . . . . . . . . . . . . . . 23
     |
175 | 144 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   |
176 | | 2cnd 10679 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   |
177 | 175, 176,
175 | constcncfg 37742 |
. . . . . . . . . . . . . . . . . . . . . . . 24
         |
178 | 102, 177 | mp1i 13 |
. . . . . . . . . . . . . . . . . . . . . . 23
        |
179 | | 2cnd 10679 |
. . . . . . . . . . . . . . . . . . . . . . 23
         |
180 | 174, 178,
143, 145, 179 | cncfmptssg 37741 |
. . . . . . . . . . . . . . . . . . . . . 22
                  |
181 | | sincn 23392 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     |
182 | 181 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
      |
183 | | eqid 2450 |
. . . . . . . . . . . . . . . . . . . . . . . 24
         |
184 | 183 | divccncf 21931 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
    
        |
185 | 102, 81, 184 | mp2an 677 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
         |
186 | 185 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
        |
187 | 163 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
         |
188 | 187 | halfcld 10854 |
. . . . . . . . . . . . . . . . . . . . . . . 24
           |
189 | 183, 186,
143, 145, 188 | cncfmptssg 37741 |
. . . . . . . . . . . . . . . . . . . . . . 23
                    |
190 | 182, 189 | cncfmpt1f 21938 |
. . . . . . . . . . . . . . . . . . . . . 22
                        |
191 | 180, 190 | mulcncf 22391 |
. . . . . . . . . . . . . . . . . . . . 21
                          |
192 | 191 | trud 1452 |
. . . . . . . . . . . . . . . . . . . 20
                         |
193 | | cnlimc 22836 |
. . . . . . . . . . . . . . . . . . . . 21
                                     
                  
                               
         lim      |
194 | 142, 193 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
                                                  
                               
         lim     |
195 | 192, 194 | mpbi 212 |
. . . . . . . . . . . . . . . . . . 19
                                                                   lim    |
196 | 195 | simpri 464 |
. . . . . . . . . . . . . . . . . 18
                                          lim   |
197 | | fveq2 5863 |
. . . . . . . . . . . . . . . . . . . 20
                                         |
198 | | oveq2 6296 |
. . . . . . . . . . . . . . . . . . . 20
                 lim                  lim    |
199 | 197, 198 | eleq12d 2522 |
. . . . . . . . . . . . . . . . . . 19
        
                            lim 
                         
         lim     |
200 | 199 | rspccva 3148 |
. . . . . . . . . . . . . . . . . 18
                                            lim                                           lim    |
201 | 196, 44, 200 | mp2an 677 |
. . . . . . . . . . . . . . . . 17
                         
         lim   |
202 | | oveq1 6295 |
. . . . . . . . . . . . . . . . . . . . . . . 24
       |
203 | 102, 81 | div0i 10338 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   |
204 | 202, 203 | syl6eq 2500 |
. . . . . . . . . . . . . . . . . . . . . . 23
     |
205 | 204 | fveq2d 5867 |
. . . . . . . . . . . . . . . . . . . . . 22
             |
206 | | sin0 14196 |
. . . . . . . . . . . . . . . . . . . . . 22
     |
207 | 205, 206 | syl6eq 2500 |
. . . . . . . . . . . . . . . . . . . . 21
         |
208 | 207 | oveq2d 6304 |
. . . . . . . . . . . . . . . . . . . 20
             |
209 | | 2t0e0 10762 |
. . . . . . . . . . . . . . . . . . . 20
   |
210 | 208, 209 | syl6eq 2500 |
. . . . . . . . . . . . . . . . . . 19
           |
211 | | eqid 2450 |
. . . . . . . . . . . . . . . . . . 19
                               |
212 | 210, 211,
159 | fvmpt 5946 |
. . . . . . . . . . . . . . . . . 18
                           |
213 | 44, 212 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
                    |
214 | | 2cnd 10679 |
. . . . . . . . . . . . . . . . . . . . . . 23
        |
215 | 163 | halfcld 10854 |
. . . . . . . . . . . . . . . . . . . . . . . 24
          |
216 | 215 | sincld 14177 |
. . . . . . . . . . . . . . . . . . . . . . 23
              |
217 | 214, 216 | mulcld 9660 |
. . . . . . . . . . . . . . . . . . . . . 22
                |
218 | 211, 217 | fmpti 6043 |
. . . . . . . . . . . . . . . . . . . . 21
                         |
219 | 218 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
                          |
220 | 219 | limcdif 22824 |
. . . . . . . . . . . . . . . . . . 19
      
         lim         
                   lim    |
221 | 220 | trud 1452 |
. . . . . . . . . . . . . . . . . 18
                lim                             lim   |
222 | | resmpt 5153 |
. . . . . . . . . . . . . . . . . . . 20
      
                                                       |
223 | 16, 222 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
                                              |
224 | 223 | oveq1i 6298 |
. . . . . . . . . . . . . . . . . 18
                           lim                      lim   |
225 | 221, 224 | eqtri 2472 |
. . . . . . . . . . . . . . . . 17
                lim                      lim   |
226 | 201, 213,
225 | 3eltr3i 2540 |
. . . . . . . . . . . . . . . 16
                    lim   |
227 | 226 | a1i 11 |
. . . . . . . . . . . . . . 15
       
            lim    |
228 | | eqidd 2451 |
. . . . . . . . . . . . . . . . . . . . 21
                                                  |
229 | | oveq1 6295 |
. . . . . . . . . . . . . . . . . . . . . . . 24
       |
230 | 229 | fveq2d 5867 |
. . . . . . . . . . . . . . . . . . . . . . 23
               |
231 | 230 | oveq2d 6304 |
. . . . . . . . . . . . . . . . . . . . . 22
                   |
232 | 231 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . 21
                              |
233 | | id 22 |
. . . . . . . . . . . . . . . . . . . . 21
               
     |
234 | 26 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
            |
235 | 19 | sseli 3427 |
. . . . . . . . . . . . . . . . . . . . . . . 24
            |
236 | 235 | rehalfcld 10856 |
. . . . . . . . . . . . . . . . . . . . . . 23
              |
237 | 236 | resincld 14190 |
. . . . . . . . . . . . . . . . . . . . . 22
                  |
238 | 234, 237 | remulcld 9668 |
. . . . . . . . . . . . . . . . . . . . 21
                    |
239 | 228, 232,
233, 238 | fvmptd 5952 |
. . . . . . . . . . . . . . . . . . . 20
                                           |
240 | | 2cnd 10679 |
. . . . . . . . . . . . . . . . . . . . 21
            |
241 | 237 | recnd 9666 |
. . . . . . . . . . . . . . . . . . . . 21
                  |
242 | 81 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
            |
243 | | ioossicc 11717 |
. . . . . . . . . . . . . . . . . . . . . . 23
        ![[,] [,]](_icc.gif)   |
244 | | eldifi 3554 |
. . . . . . . . . . . . . . . . . . . . . . 23
                 |
245 | 243, 244 | sseldi 3429 |
. . . . . . . . . . . . . . . . . . . . . 22
             ![[,] [,]](_icc.gif)    |
246 | | eldifsni 4097 |
. . . . . . . . . . . . . . . . . . . . . 22
            |
247 | | fourierdlem44 38009 |
. . . . . . . . . . . . . . . . . . . . . 22
     ![[,] [,]](_icc.gif)           |
248 | 245, 246,
247 | syl2anc 666 |
. . . . . . . . . . . . . . . . . . . . 21
                  |
249 | 240, 241,
242, 248 | mulne0d 10261 |
. . . . . . . . . . . . . . . . . . . 20
                    |
250 | 239, 249 | eqnetrd 2690 |
. . . . . . . . . . . . . . . . . . 19
                                   |
251 | 250 | neneqd 2628 |
. . . . . . . . . . . . . . . . . 18
         
                         |
252 | 251 | nrex 2841 |
. . . . . . . . . . . . . . . . 17

                                  |
253 | 25 | fnmpt 5702 |
. . . . . . . . . . . . . . . . . . 19
 
                        
                       |
254 | 253, 30 | mprg 2750 |
. . . . . . . . . . . . . . . . . 18
                             |
255 | | ssid 3450 |
. . . . . . . . . . . . . . . . . 18
        
          |
256 | | fvelimab 5919 |
. . . . . . . . . . . . . . . . . 18
        
                                                                               
                              |
257 | 254, 255,
256 | mp2an 677 |
. . . . . . . . . . . . . . . . 17
                                
                  
                 |
258 | 252, 257 | mtbir 301 |
. . . . . . . . . . . . . . . 16
                                 |
259 | 258 | a1i 11 |
. . . . . . . . . . . . . . 15
       
                          |
260 | | eqidd 2451 |
. . . . . . . . . . . . . . . . . . . . . 22
                                              |
261 | 229 | fveq2d 5867 |
. . . . . . . . . . . . . . . . . . . . . . 23
               |
262 | 261 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . 22
                          |
263 | 235 | recnd 9666 |
. . . . . . . . . . . . . . . . . . . . . . . 24
            |
264 | 263 | halfcld 10854 |
. . . . . . . . . . . . . . . . . . . . . . 23
              |
265 | 264 | coscld 14178 |
. . . . . . . . . . . . . . . . . . . . . 22
                  |
266 | 260, 262,
233, 265 | fvmptd 5952 |
. . . . . . . . . . . . . . . . . . . . 21
                                       |
267 | 236 | rered 13280 |
. . . . . . . . . . . . . . . . . . . . . . 23
                    |
268 | | halfpire 23412 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
   |
269 | 268 | renegcli 9932 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
  |
270 | 269 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
               |
271 | 270 | rexrd 9687 |
. . . . . . . . . . . . . . . . . . . . . . . 24
               |
272 | 268 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
              |
273 | 272 | rexrd 9687 |
. . . . . . . . . . . . . . . . . . . . . . . 24
              |
274 | | picn 23407 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 |
275 | | divneg 10299 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
  
      |
276 | 274, 102,
81, 275 | mp3an 1363 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
     |
277 | 39 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
             |
278 | | 2rp 11304 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 |
279 | 278 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
            |
280 | 40 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
             |
281 | 41 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
            |
282 | | ioogtlb 37586 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
            |
283 | 280, 281,
244, 282 | syl3anc 1267 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
             |
284 | 277, 235,
279, 283 | ltdiv1dd 11392 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                 |
285 | 276, 284 | syl5eqbr 4435 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                 |
286 | 38 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
            |
287 | | iooltub 37604 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
           |
288 | 280, 281,
244, 287 | syl3anc 1267 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
            |
289 | 235, 286,
279, 288 | ltdiv1dd 11392 |
. . . . . . . . . . . . . . . . . . . . . . . 24
            
   |
290 | 271, 273,
236, 285, 289 | eliood 37589 |
. . . . . . . . . . . . . . . . . . . . . . 23
                  
    |
291 | 267, 290 | eqeltrd 2528 |
. . . . . . . . . . . . . . . . . . . . . 22
                      
    |
292 | | cosne0 23472 |
. . . . . . . . . . . . . . . . . . . . . 22
            
               |
293 | 264, 291,
292 | syl2anc 666 |
. . . . . . . . . . . . . . . . . . . . 21
                  |
294 | 266, 293 | eqnetrd 2690 |
. . . . . . . . . . . . . . . . . . . 20
                                 |
295 | 294 | neneqd 2628 |
. . . . . . . . . . . . . . . . . . 19
         
                       |
296 | 295 | nrex 2841 |
. . . . . . . . . . . . . . . . . 18

                                |
297 | 72, 73 | fnmpti 5704 |
. . . . . . . . . . . . . . . . . . 19
                           |
298 | | fvelimab 5919 |
. . . . . . . . . . . . . . . . . . 19
        
                                                                    
                  
                |
299 | 297, 255,
298 | mp2an 677 |
. . . . . . . . . . . . . . . . . 18
                              
                  
               |
300 | 296, 299 | mtbir 301 |
. . . . . . . . . . . . . . . . 17
                               |
301 | 135 | imaeq1i 5164 |
. . . . . . . . . . . . . . . . . 18
                                         
                       |
302 | 301 | eleq2i 2520 |
. . . . . . . . . . . . . . . . 17
                                  
                                |
303 | 300, 302 | mtbir 301 |
. . . . . . . . . . . . . . . 16
  
                                |
304 | 303 | a1i 11 |
. . . . . . . . . . . . . . 15
                                    |
305 | | eqid 2450 |
. . . . . . . . . . . . . . . . 17
                                   |
306 | | eqid 2450 |
. . . . . . . . . . . . . . . . 17
                                       |
307 | 19 | sseli 3427 |
. . . . . . . . . . . . . . . . . . . . . 22
            |
308 | 307 | recnd 9666 |
. . . . . . . . . . . . . . . . . . . . 21
            |
309 | 308 | halfcld 10854 |
. . . . . . . . . . . . . . . . . . . 20
              |
310 | 309 | coscld 14178 |
. . . . . . . . . . . . . . . . . . 19
                  |
311 | 307 | rehalfcld 10856 |
. . . . . . . . . . . . . . . . . . . . . . . 24
              |
312 | 311 | rered 13280 |
. . . . . . . . . . . . . . . . . . . . . . 23
                    |
313 | 269 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
               |
314 | 313 | rexrd 9687 |
. . . . . . . . . . . . . . . . . . . . . . . 24
               |
315 | 268 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
              |
316 | 315 | rexrd 9687 |
. . . . . . . . . . . . . . . . . . . . . . . 24
              |
317 | 38 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
            |
318 | 317 | renegcld 10043 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
             |
319 | 278 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
            |
320 | 40 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
             |
321 | 41 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
            |
322 | | eldifi 3554 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
                 |
323 | | ioogtlb 37586 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
            |
324 | 320, 321,
322, 323 | syl3anc 1267 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
             |
325 | 318, 307,
319, 324 | ltdiv1dd 11392 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                 |
326 | 276, 325 | syl5eqbr 4435 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                 |
327 | | iooltub 37604 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
           |
328 | 320, 321,
322, 327 | syl3anc 1267 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
            |
329 | 307, 317,
319, 328 | ltdiv1dd 11392 |
. . . . . . . . . . . . . . . . . . . . . . . 24
            
   |
330 | 314, 316,
311, 326, 329 | eliood 37589 |
. . . . . . . . . . . . . . . . . . . . . . 23
                  
    |
331 | 312, 330 | eqeltrd 2528 |
. . . . . . . . . . . . . . . . . . . . . 22
                      
    |
332 | | cosne0 23472 |
. . . . . . . . . . . . . . . . . . . . . 22
            
               |
333 | 309, 331,
332 | syl2anc 666 |
. . . . . . . . . . . . . . . . . . . . 21
                  |
334 | 333 | neneqd 2628 |
. . . . . . . . . . . . . . . . . . . 20
         
        |
335 | 311 | recoscld 14191 |
. . . . . . . . . . . . . . . . . . . . 21
                  |
336 | | elsncg 3990 |
. . . . . . . . . . . . . . . . . . . . 21
                         |
337 | 335, 336 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
                  
         |
338 | 334, 337 | mtbird 303 |
. . . . . . . . . . . . . . . . . . 19
         
          |
339 | 310, 338 | eldifd 3414 |
. . . . . . . . . . . . . . . . . 18
                      |
340 | 339 | adantl 468 |
. . . . . . . . . . . . . . . . 17
                       |
341 | 309 | ad2antrl 733 |
. . . . . . . . . . . . . . . . . 18
                   |
342 | | cosf 14172 |
. . . . . . . . . . . . . . . . . . . 20
     |
343 | 342 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
      |
344 | 343 | ffvelrnda 6020 |
. . . . . . . . . . . . . . . . . 18
        |
345 | | eqid 2450 |
. . . . . . . . . . . . . . . . . . . . 21
         |
346 | 345 | divccncf 21931 |
. . . . . . . . . . . . . . . . . . . . . . 23
             |
347 | 102, 81, 346 | mp2an 677 |
. . . . . . . . . . . . . . . . . . . . . 22
         |
348 | 347 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
          |
349 | 141 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . 22
         |
350 | 349 | halfcld 10854 |
. . . . . . . . . . . . . . . . . . . . 21
           |
351 | 345, 348,
143, 145, 350 | cncfmptssg 37741 |
. . . . . . . . . . . . . . . . . . . 20
                    |
352 | | oveq1 6295 |
. . . . . . . . . . . . . . . . . . . . 21
       |
353 | 352, 203 | syl6eq 2500 |
. . . . . . . . . . . . . . . . . . . 20
     |
354 | 351, 45, 353 | cnmptlimc 22838 |
. . . . . . . . . . . . . . . . . . 19
          lim    |
355 | | eqid 2450 |
. . . . . . . . . . . . . . . . . . . . . . . 24
              
    |
356 | 141 | halfcld 10854 |
. . . . . . . . . . . . . . . . . . . . . . . 24
          |
357 | 355, 356 | fmpti 6043 |
. . . . . . . . . . . . . . . . . . . . . . 23
                   |
358 | 357 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
                    |
359 | 358 | limcdif 22824 |
. . . . . . . . . . . . . . . . . . . . 21
      
   lim                       lim    |
360 | 359 | trud 1452 |
. . . . . . . . . . . . . . . . . . . 20
          lim            
          lim   |
361 | | resmpt 5153 |
. . . . . . . . . . . . . . . . . . . . . 22
      
                                           |
362 | 16, 361 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . 21
         
                        |
363 | 362 | oveq1i 6298 |
. . . . . . . . . . . . . . . . . . . 20
                     lim                lim   |
364 | 360, 363 | eqtri 2472 |
. . . . . . . . . . . . . . . . . . 19
          lim                lim   |
365 | 354, 364 | syl6eleq 2538 |
. . . . . . . . . . . . . . . . . 18
       
      lim    |
366 | | ffn 5726 |
. . . . . . . . . . . . . . . . . . . . . . 23
       |
367 | 342, 366 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . 22
 |
368 | | dffn5 5908 |
. . . . . . . . . . . . . . . . . . . . . 22

        |
369 | 367, 368 | mpbi 212 |
. . . . . . . . . . . . . . . . . . . . 21

      |
370 | | coscn 23393 |
. . . . . . . . . . . . . . . . . . . . 21
     |
371 | 369, 370 | eqeltrri 2525 |
. . . . . . . . . . . . . . . . . . . 20
           |
372 | 371 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
            |
373 | | 0cnd 9633 |
. . . . . . . . . . . . . . . . . . 19
  |
374 | | fveq2 5863 |
. . . . . . . . . . . . . . . . . . . 20
           |
375 | | cos0 14197 |
. . . . . . . . . . . . . . . . . . . 20
     |
376 | 374, 375 | syl6eq 2500 |
. . . . . . . . . . . . . . . . . . 19
       |
377 | 372, 373,
376 | cnmptlimc 22838 |
. . . . . . . . . . . . . . . . . 18
       lim    |
378 | | fveq2 5863 |
. . . . . . . . . . . . . . . . . 18
               |
379 | | fveq2 5863 |
. . . . . . . . . . . . . . . . . . . 20
               |
380 | 379, 375 | syl6eq 2500 |
. . . . . . . . . . . . . . . . . . 19
           |
381 | 380 | ad2antll 734 |
. . . . . . . . . . . . . . . . . 18
                       |
382 | 341, 344,
365, 377, 378, 381 | limcco 22841 |
. . . . . . . . . . . . . . . . 17
       
          lim    |
383 | | ax-1ne0 9605 |
. . . . . . . . . . . . . . . . . 18
 |
384 | 383 | a1i 11 |
. . . . . . . . . . . . . . . . 17
  |
385 | 305, 306,
340, 382, 384 | reclimc 37728 |
. . . . . . . . . . . . . . . 16
                      lim    |
386 | | 1div1e1 10297 |
. . . . . . . . . . . . . . . 16
   |
387 | 66 | fveq1i 5864 |
. . . . . . . . . . . . . . . . . . . 20
                        
        |
388 | | eqidd 2451 |
. . . . . . . . . . . . . . . . . . . . 21
                                  |
389 | | eqidd 2451 |
. . . . . . . . . . . . . . . . . . . . 21
              |
390 | | id 22 |
. . . . . . . . . . . . . . . . . . . . 21
               
     |
391 | | 1red 9655 |
. . . . . . . . . . . . . . . . . . . . 21
            |
392 | 388, 389,
390, 391 | fvmptd 5952 |
. . . . . . . . . . . . . . . . . . . 20
                           |
393 | 387, 392 | syl5req 2497 |
. . . . . . . . . . . . . . . . . . 19
                             |
394 | 135 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
           
                                      |
395 | | oveq1 6295 |
. . . . . . . . . . . . . . . . . . . . . . 23
       |
396 | 395 | fveq2d 5867 |
. . . . . . . . . . . . . . . . . . . . . 22
               |
397 | 396 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . 21
                          |
398 | 394, 397,
390, 335 | fvmptd 5952 |
. . . . . . . . . . . . . . . . . . . 20
                                           |
399 | 398 | eqcomd 2456 |
. . . . . . . . . . . . . . . . . . 19
                                           |
400 | 393, 399 | oveq12d 6306 |
. . . . . . . . . . . . . . . . . 18
                     
                
                         |
401 | 400 | mpteq2ia 4484 |
. . . . . . . . . . . . . . . . 17
                                                                           |
402 | 401 | oveq1i 6298 |
. . . . . . . . . . . . . . . 16
                    lim         
                       
                        lim   |
403 | 385, 386,
402 | 3eltr3g 2544 |
. . . . . . . . . . . . . . 15
       
                       
                        lim    |
404 | 20, 24, 32, 34, 45, 46, 71, 140, 173, 227, 259, 304, 403 | lhop 22961 |
. . . . . . . . . . . . . 14
       
           
                                lim    |
405 | 404 | trud 1452 |
. . . . . . . . . . . . 13
                                                    lim   |
406 | | eqidd 2451 |
. . . . . . . . . . . . . . . . 17
                                  |
407 | | simpr 463 |
. . . . . . . . . . . . . . . . 17
              |
408 | 406, 407,
390, 307 | fvmptd 5952 |
. . . . . . . . . . . . . . . 16
                           |
409 | | eqidd 2451 |
. . . . . . . . . . . . . . . . 17
                                                  |
410 | 407 | oveq1d 6303 |
. . . . . . . . . . . . . . . . . . 19
                  |
411 | 410 | fveq2d 5867 |
. . . . . . . . . . . . . . . . . 18
                          |
412 | 411 | oveq2d 6304 |
. . . . . . . . . . . . . . . . 17
                              |
413 | 26 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
            |
414 | 311 | resincld 14190 |
. . . . . . . . . . . . . . . . . 18
                  |
415 | 413, 414 | remulcld 9668 |
. . . . . . . . . . . . . . . . 17
                    |
416 | 409, 412,
390, 415 | fvmptd 5952 |
. . . . . . . . . . . . . . . 16
                                           |
417 | 408, 416 | oveq12d 6306 |
. . . . . . . . . . . . . . 15
                                 
                            |
418 | 417 | mpteq2ia 4484 |
. . . . . . . . . . . . . 14
                                                                         |
419 | 418 | oveq1i 6298 |
. . . . . . . . . . . . 13
                                  
                 lim                        lim   |
420 | 405, 419 | eleqtri 2526 |
. . . . . . . . . . . 12
                      lim   |
421 | 10 | oveq1i 6298 |
. . . . . . . . . . . . . 14
 lim       ![[,] [,]](_icc.gif) 
                lim   |
422 | 10 | feq1i 5718 |
. . . . . . . . . . . . . . . . . . 19
      ![[,] [,]](_icc.gif)   
    ![[,] [,]](_icc.gif) 
                     ![[,] [,]](_icc.gif)      |
423 | 14, 422 | mpbi 212 |
. . . . . . . . . . . . . . . . . 18
    ![[,] [,]](_icc.gif)       |