Step | Hyp | Ref
| Expression |
1 | | pire 23492 |
. . . . 5
 |
2 | 1 | renegcli 9955 |
. . . 4
  |
3 | 2 | a1i 11 |
. . 3
    |
4 | 1 | a1i 11 |
. . 3
   |
5 | | negpilt0 37580 |
. . . . 5
  |
6 | | pipos 23494 |
. . . . 5
 |
7 | | 0re 9661 |
. . . . . 6
 |
8 | 2, 7, 1 | lttri 9778 |
. . . . 5
  
    |
9 | 5, 6, 8 | mp2an 686 |
. . . 4
  |
10 | 9 | a1i 11 |
. . 3
    |
11 | | fourierdlem94.p |
. . 3
 
                  
 ..^                |
12 | | picn 23493 |
. . . . 5
 |
13 | 12 | 2timesi 10753 |
. . . 4
     |
14 | | fourierdlem94.t |
. . . 4
   |
15 | 12, 12 | subnegi 9973 |
. . . 4
      |
16 | 13, 14, 15 | 3eqtr4i 2503 |
. . 3
    |
17 | | fourierdlem94.m |
. . 3
   |
18 | | fourierdlem94.q |
. . 3
       |
19 | | ssid 3437 |
. . . 4
 |
20 | 19 | a1i 11 |
. . 3

  |
21 | | fourierdlem94.f |
. . 3
       |
22 | | simp2 1031 |
. . . 4
 
   |
23 | | zre 10965 |
. . . . . 6
   |
24 | 23 | 3ad2ant3 1053 |
. . . . 5
 
   |
25 | | 2re 10701 |
. . . . . . . . . 10
 |
26 | 25, 1 | remulcli 9675 |
. . . . . . . . 9
   |
27 | 26 | a1i 11 |
. . . . . . . 8
  
  |
28 | 14, 27 | syl5eqel 2553 |
. . . . . . 7
   |
29 | 28 | adantr 472 |
. . . . . 6
 

  |
30 | 29 | 3adant2 1049 |
. . . . 5
 
   |
31 | 24, 30 | remulcld 9689 |
. . . 4
 
     |
32 | 22, 31 | readdcld 9688 |
. . 3
 
       |
33 | | simp1 1030 |
. . . 4
 
   |
34 | | simp3 1032 |
. . . 4
 
   |
35 | | ax-resscn 9614 |
. . . . . . . . 9
 |
36 | 35 | a1i 11 |
. . . . . . . 8

  |
37 | 21, 36 | fssd 5750 |
. . . . . . 7
       |
38 | 37 | adantr 472 |
. . . . . 6
 

      |
39 | 38 | adantr 472 |
. . . . 5
           |
40 | 29 | adantr 472 |
. . . . 5
       |
41 | | simplr 770 |
. . . . 5
       |
42 | | simpr 468 |
. . . . 5
       |
43 | | eleq1 2537 |
. . . . . . . . 9
 
   |
44 | 43 | anbi2d 718 |
. . . . . . . 8
  

     |
45 | | oveq1 6315 |
. . . . . . . . . 10
       |
46 | 45 | fveq2d 5883 |
. . . . . . . . 9
               |
47 | | fveq2 5879 |
. . . . . . . . 9
           |
48 | 46, 47 | eqeq12d 2486 |
. . . . . . . 8
           
             |
49 | 44, 48 | imbi12d 327 |
. . . . . . 7
   
             
               |
50 | | fourierdlem94.per |
. . . . . . 7
 

            |
51 | 49, 50 | chvarv 2120 |
. . . . . 6
 

            |
52 | 51 | adant423 37430 |
. . . . 5
   

              |
53 | 39, 40, 41, 42, 52 | fperiodmul 37610 |
. . . 4
                   |
54 | 33, 34, 22, 53 | syl21anc 1291 |
. . 3
 
    
          |
55 | 35 | a1i 11 |
. . . 4
 
 ..^    |
56 | | ioossre 11721 |
. . . . . . . 8
               |
57 | 56 | a1i 11 |
. . . . . . 7
              
  |
58 | 21, 57 | fssresd 5762 |
. . . . . 6
                                     |
59 | 58, 36 | fssd 5750 |
. . . . 5
                                     |
60 | 59 | adantr 472 |
. . . 4
 
 ..^                                      |
61 | 56 | a1i 11 |
. . . 4
 
 ..^                  |
62 | 37 | adantr 472 |
. . . . . . 7
 
 ..^        |
63 | 19 | a1i 11 |
. . . . . . 7
 
 ..^    |
64 | | eqid 2471 |
. . . . . . . 8
  ℂfld   ℂfld |
65 | 64 | tgioo2 21899 |
. . . . . . . 8
       ℂfld
↾t   |
66 | 64, 65 | dvres 22945 |
. . . . . . 7
                                                    
                      |
67 | 55, 62, 63, 61, 66 | syl22anc 1293 |
. . . . . 6
 
 ..^   
                         
                      |
68 | 67 | dmeqd 5042 |
. . . . 5
 
 ..^ 
                           
                      |
69 | | ioontr 37707 |
. . . . . . . 8
                                         |
70 | 69 | reseq2i 5108 |
. . . . . . 7
         
                                       |
71 | 70 | dmeqi 5041 |
. . . . . 6
                                                 |
72 | 71 | a1i 11 |
. . . . 5
 
 ..^ 
         
                                        |
73 | | fourierdlem94.dvcn |
. . . . . 6
 
 ..^                                        |
74 | | cncff 22003 |
. . . . . 6
                                                                           |
75 | | fdm 5745 |
. . . . . 6
                                                                       |
76 | 73, 74, 75 | 3syl 18 |
. . . . 5
 
 ..^ 
                                  |
77 | 68, 72, 76 | 3eqtrd 2509 |
. . . 4
 
 ..^ 
                                  |
78 | | dvcn 22954 |
. . . 4
                                                                                                                         |
79 | 55, 60, 61, 77, 78 | syl31anc 1295 |
. . 3
 
 ..^                                      |
80 | 61, 35 | syl6ss 3430 |
. . . 4
 
 ..^                  |
81 | 11 | fourierdlem2 38083 |
. . . . . . . . . . . 12
 
   
                   
 ..^                 |
82 | 17, 81 | syl 17 |
. . . . . . . . . . 11
                         
 ..^                 |
83 | 18, 82 | mpbid 215 |
. . . . . . . . . 10
                    
 ..^                |
84 | 83 | simpld 466 |
. . . . . . . . 9
         |
85 | | elmapi 7511 |
. . . . . . . . 9
                 |
86 | 84, 85 | syl 17 |
. . . . . . . 8
           |
87 | 86 | adantr 472 |
. . . . . . 7
 
 ..^            |
88 | | elfzofz 11962 |
. . . . . . . 8
  ..^
      |
89 | 88 | adantl 473 |
. . . . . . 7
 
 ..^        |
90 | 87, 89 | ffvelrnd 6038 |
. . . . . 6
 
 ..^        |
91 | 90 | rexrd 9708 |
. . . . 5
 
 ..^        |
92 | | fzofzp1 12037 |
. . . . . . 7
  ..^
        |
93 | 92 | adantl 473 |
. . . . . 6
 
 ..^          |
94 | 87, 93 | ffvelrnd 6038 |
. . . . 5
 
 ..^          |
95 | 83 | simprrd 775 |
. . . . . 6
   ..^              |
96 | 95 | r19.21bi 2776 |
. . . . 5
 
 ..^              |
97 | 64, 91, 94, 96 | lptioo2cn 37823 |
. . . 4
 
 ..^              ℂfld                    |
98 | 58 | adantr 472 |
. . . . 5
 
 ..^                                      |
99 | 36, 37, 20 | dvbss 22935 |
. . . . . . . 8
     |
100 | | dvfre 22984 |
. . . . . . . . 9
                 |
101 | 21, 20, 100 | syl2anc 673 |
. . . . . . . 8
           |
102 | 83 | simprd 470 |
. . . . . . . . 9
             
 ..^               |
103 | 102 | simplld 769 |
. . . . . . . 8
        |
104 | 102 | simplrd 771 |
. . . . . . . 8
       |
105 | 73, 74 | syl 17 |
. . . . . . . . 9
 
 ..^                                        |
106 | 94 | rexrd 9708 |
. . . . . . . . . 10
 
 ..^          |
107 | 64, 106, 90, 96 | lptioo1cn 37824 |
. . . . . . . . 9
 
 ..^            ℂfld                    |
108 | | fourierdlem94.dvlb |
. . . . . . . . 9
 
 ..^                     lim        |
109 | 105, 80, 107, 108, 64 | ellimciota 37791 |
. . . . . . . 8
 
 ..^    
                   lim                          lim        |
110 | | fourierdlem94.dvub |
. . . . . . . . 9
 
 ..^                     lim          |
111 | 105, 80, 97, 110, 64 | ellimciota 37791 |
. . . . . . . 8
 
 ..^    
                   lim                            lim          |
112 | 23 | adantl 473 |
. . . . . . . . . . . 12
 

  |
113 | 112, 29 | remulcld 9689 |
. . . . . . . . . . 11
 

    |
114 | 38 | adantr 472 |
. . . . . . . . . . . 12
           |
115 | 29 | adantr 472 |
. . . . . . . . . . . 12
       |
116 | | simplr 770 |
. . . . . . . . . . . 12
       |
117 | | simpr 468 |
. . . . . . . . . . . 12
       |
118 | 50 | adant423 37430 |
. . . . . . . . . . . 12
   

     
        |
119 | 114, 115,
116, 117, 118 | fperiodmul 37610 |
. . . . . . . . . . 11
                   |
120 | | eqid 2471 |
. . . . . . . . . . 11
     |
121 | 38, 113, 119, 120 | fperdvper 37887 |
. . . . . . . . . 10
            

                   |
122 | 121 | an32s 821 |
. . . . . . . . 9
     
      

                   |
123 | 122 | simpld 466 |
. . . . . . . 8
     
         |
124 | 122 | simprd 470 |
. . . . . . . 8
     
                   |
125 | | fveq2 5879 |
. . . . . . . . . 10
           |
126 | | oveq1 6315 |
. . . . . . . . . . 11
       |
127 | 126 | fveq2d 5883 |
. . . . . . . . . 10
               |
128 | 125, 127 | oveq12d 6326 |
. . . . . . . . 9
                               |
129 | 128 | cbvmptv 4488 |
. . . . . . . 8
  ..^                  ..^                 |
130 | | eqid 2471 |
. . . . . . . 8
                             |
131 | 99, 101, 3, 4, 10, 16, 17, 86, 103, 104, 73, 109, 111, 123, 124, 129, 130 | fourierdlem71 38153 |
. . . . . . 7
                  |
132 | 131 | adantr 472 |
. . . . . 6
 
 ..^                   |
133 | | nfv 1769 |
. . . . . . . . . 10
    ..^   |
134 | | nfra1 2785 |
. . . . . . . . . 10
   
           
 |
135 | 133, 134 | nfan 2031 |
. . . . . . . . 9
   
 ..^                  |
136 | 67, 70 | syl6eq 2521 |
. . . . . . . . . . . . . . 15
 
 ..^   
                                    |
137 | 136 | fveq1d 5881 |
. . . . . . . . . . . . . 14
 
 ..^                                                |
138 | | fvres 5893 |
. . . . . . . . . . . . . 14
                                             |
139 | 137, 138 | sylan9eq 2525 |
. . . . . . . . . . . . 13
    ..^                                               |
140 | 139 | fveq2d 5883 |
. . . . . . . . . . . 12
    ..^                                                       |
141 | 140 | adantlr 729 |
. . . . . . . . . . 11
   
 ..^                
                                                     |
142 | | simplr 770 |
. . . . . . . . . . . 12
   
 ..^                
               

           
  |
143 | | ssdmres 5132 |
. . . . . . . . . . . . . . 15
              
 
                                  |
144 | 76, 143 | sylibr 217 |
. . . . . . . . . . . . . 14
 
 ..^                
   |
145 | 144 | ad2antrr 740 |
. . . . . . . . . . . . 13
   
 ..^                
                            
    |
146 | | simpr 468 |
. . . . . . . . . . . . 13
   
 ..^                
                               |
147 | 145, 146 | sseldd 3419 |
. . . . . . . . . . . 12
   
 ..^                
                   |
148 | | rspa 2774 |
. . . . . . . . . . . 12
   
           
            
  |
149 | 142, 147,
148 | syl2anc 673 |
. . . . . . . . . . 11
   
 ..^                
                        
  |
150 | 141, 149 | eqbrtrd 4416 |
. . . . . . . . . 10
   
 ..^                
                                           |
151 | 150 | ex 441 |
. . . . . . . . 9
    ..^                
              
     
                   
   |
152 | 135, 151 | ralrimi 2800 |
. . . . . . . 8
    ..^                
                                            |
153 | 152 | ex 441 |
. . . . . . 7
 
 ..^                                                              |
154 | 153 | reximdv 2857 |
. . . . . 6
 
 ..^                                                                |
155 | 132, 154 | mpd 15 |
. . . . 5
 
 ..^                                               |
156 | 90, 94, 98, 77, 155 | ioodvbdlimc2 37907 |
. . . 4
 
 ..^                   lim          |
157 | 60, 80, 97, 156, 64 | ellimciota 37791 |
. . 3
 
 ..^      
               lim                          lim          |
158 | | fourierdlem94.x |
. . 3
   |
159 | | oveq2 6316 |
. . . . . . 7
 
     |
160 | 159 | oveq1d 6323 |
. . . . . 6
           |
161 | 160 | fveq2d 5883 |
. . . . 5
                   |
162 | 161 | oveq1d 6323 |
. . . 4
                       |
163 | 162 | cbvmptv 4488 |
. . 3
                         |
164 | | id 22 |
. . . . 5
   |
165 | | fveq2 5879 |
. . . . 5
                                   |
166 | 164, 165 | oveq12d 6326 |
. . . 4
                                       |
167 | 166 | cbvmptv 4488 |
. . 3
                                         |
168 | 3, 4, 10, 11, 16, 17, 18, 20, 21, 32, 54, 79, 157, 158, 163, 167 | fourierdlem49 38131 |
. 2
       lim    |
169 | 90, 94, 98, 77, 155 | ioodvbdlimc1 37904 |
. . . 4
 
 ..^                   lim        |
170 | 60, 80, 107, 169, 64 | ellimciota 37791 |
. . 3
 
 ..^      
               lim                        lim        |
171 | | biid 244 |
. . 3
      ..^ 
              


       
 ..^                         |
172 | 3, 4, 10, 11, 16, 17, 18, 21, 32, 54, 79, 170, 158, 163, 167, 171 | fourierdlem48 38130 |
. 2
       lim
   |
173 | 168, 172 | jca 541 |
1
   
    lim        lim     |