Step | Hyp | Ref
| Expression |
1 | | prfi 7846 |
. . . 4
     
 |
2 | 1 | a1i 11 |
. . 3
     
   |
3 | | fourierdlem71.f |
. . . . . . 7
       |
4 | 3 | adantr 467 |
. . . . . 6
 
     
 
      |
5 | | simpl 459 |
. . . . . . 7
 
     
 
  |
6 | | simpr 463 |
. . . . . . . 8
 
     
 
     
   |
7 | | fourierdlem71.q |
. . . . . . . . . . . 12
           |
8 | | ovex 6318 |
. . . . . . . . . . . . 13
     |
9 | 8 | a1i 11 |
. . . . . . . . . . . 12
       |
10 | | fex 6138 |
. . . . . . . . . . . 12
                 |
11 | 7, 9, 10 | syl2anc 667 |
. . . . . . . . . . 11
   |
12 | | rnexg 6725 |
. . . . . . . . . . 11
   |
13 | | inex1g 4546 |
. . . . . . . . . . 11
     |
14 | 11, 12, 13 | 3syl 18 |
. . . . . . . . . 10
     |
15 | 14 | adantr 467 |
. . . . . . . . 9
 
     
 

   |
16 | | fourierdlem71.i |
. . . . . . . . . . . . . 14
  ..^                 |
17 | | ovex 6318 |
. . . . . . . . . . . . . . 15
 ..^  |
18 | 17 | mptex 6136 |
. . . . . . . . . . . . . 14
  ..^                 |
19 | 16, 18 | eqeltri 2525 |
. . . . . . . . . . . . 13
 |
20 | 19 | rnex 6727 |
. . . . . . . . . . . 12
 |
21 | 20 | a1i 11 |
. . . . . . . . . . 11
   |
22 | | uniexg 6588 |
. . . . . . . . . . 11
    |
23 | 21, 22 | syl 17 |
. . . . . . . . . 10
    |
24 | 23 | adantr 467 |
. . . . . . . . 9
 
     
 
   |
25 | | uniprg 4212 |
. . . . . . . . 9
    

  
           |
26 | 15, 24, 25 | syl2anc 667 |
. . . . . . . 8
 
     
 
      
 
     |
27 | 6, 26 | eleqtrd 2531 |
. . . . . . 7
 
     
 
   
   |
28 | | elinel2 3620 |
. . . . . . . . 9
  
  |
29 | 28 | adantl 468 |
. . . . . . . 8
      
 
     |
30 | | simpll 760 |
. . . . . . . . 9
      
 
     |
31 | | elunnel1 3575 |
. . . . . . . . . 10
      

 
   |
32 | 31 | adantll 720 |
. . . . . . . . 9
      
 
  
   |
33 | 16 | funmpt2 5619 |
. . . . . . . . . . . . 13
 |
34 | | elunirn 6156 |
. . . . . . . . . . . . 13

 
        |
35 | 33, 34 | ax-mp 5 |
. . . . . . . . . . . 12
  
      |
36 | 35 | biimpi 198 |
. . . . . . . . . . 11
  
      |
37 | 36 | adantl 468 |
. . . . . . . . . 10
 
  
      |
38 | | id 22 |
. . . . . . . . . . . . . . . . . . 19
   |
39 | | ovex 6318 |
. . . . . . . . . . . . . . . . . . . 20
               |
40 | 39, 16 | dmmpti 5707 |
. . . . . . . . . . . . . . . . . . 19
 ..^  |
41 | 38, 40 | syl6eleq 2539 |
. . . . . . . . . . . . . . . . . 18
  ..^   |
42 | 41 | adantl 468 |
. . . . . . . . . . . . . . . . 17
 
  ..^   |
43 | 39 | a1i 11 |
. . . . . . . . . . . . . . . . 17
 
                 |
44 | 16 | fvmpt2 5957 |
. . . . . . . . . . . . . . . . 17
   ..^                                    |
45 | 42, 43, 44 | syl2anc 667 |
. . . . . . . . . . . . . . . 16
 
                     |
46 | | fourierdlem71.fcn |
. . . . . . . . . . . . . . . . . . 19
 
 ..^                                      |
47 | | cncff 21925 |
. . . . . . . . . . . . . . . . . . 19
 
                                                                     |
48 | | fdm 5733 |
. . . . . . . . . . . . . . . . . . 19
 
                                 
                               |
49 | 46, 47, 48 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
 
 ..^ 
                                |
50 | 41, 49 | sylan2 477 |
. . . . . . . . . . . . . . . . 17
 
 
                               |
51 | | ssdmres 5126 |
. . . . . . . . . . . . . . . . 17
              
                                |
52 | 50, 51 | sylibr 216 |
. . . . . . . . . . . . . . . 16
 
              
  |
53 | 45, 52 | eqsstrd 3466 |
. . . . . . . . . . . . . . 15
 
       |
54 | 53 | 3adant3 1028 |
. . . . . . . . . . . . . 14
 
           |
55 | | simp3 1010 |
. . . . . . . . . . . . . 14
 
           |
56 | 54, 55 | sseldd 3433 |
. . . . . . . . . . . . 13
 
       |
57 | 56 | 3exp 1207 |
. . . . . . . . . . . 12
      
    |
58 | 57 | adantr 467 |
. . . . . . . . . . 11
 
       
    |
59 | 58 | rexlimdv 2877 |
. . . . . . . . . 10
 
       
   |
60 | 37, 59 | mpd 15 |
. . . . . . . . 9
 
 
  |
61 | 30, 32, 60 | syl2anc 667 |
. . . . . . . 8
      
 
  
  |
62 | 29, 61 | pm2.61dan 800 |
. . . . . . 7
 
   
 
  |
63 | 5, 27, 62 | syl2anc 667 |
. . . . . 6
 
     
 
  |
64 | 4, 63 | ffvelrnd 6023 |
. . . . 5
 
     
 
      |
65 | 64 | recnd 9669 |
. . . 4
 
     
 
      |
66 | 65 | abscld 13498 |
. . 3
 
     
 
          |
67 | | simpr 463 |
. . . . . . 7
 
       |
68 | | fzfid 12186 |
. . . . . . . . . 10
       |
69 | | rnffi 37440 |
. . . . . . . . . 10
              
  |
70 | 7, 68, 69 | syl2anc 667 |
. . . . . . . . 9
   |
71 | | infi 7795 |
. . . . . . . . 9
     |
72 | 70, 71 | syl 17 |
. . . . . . . 8
     |
73 | 72 | adantr 467 |
. . . . . . 7
 
       |
74 | 67, 73 | eqeltrd 2529 |
. . . . . 6
 
     |
75 | | simpll 760 |
. . . . . . . 8
      
  |
76 | | simpr 463 |
. . . . . . . . . 10
  
 
  |
77 | | simpl 459 |
. . . . . . . . . 10
  
 
    |
78 | 76, 77 | eleqtrd 2531 |
. . . . . . . . 9
  
 
    |
79 | 78 | adantll 720 |
. . . . . . . 8
      
    |
80 | 3 | adantr 467 |
. . . . . . . . . . 11
 
         |
81 | 28 | adantl 468 |
. . . . . . . . . . 11
 
     |
82 | 80, 81 | ffvelrnd 6023 |
. . . . . . . . . 10
 
         |
83 | 82 | recnd 9669 |
. . . . . . . . 9
 
         |
84 | 83 | abscld 13498 |
. . . . . . . 8
 
             |
85 | 75, 79, 84 | syl2anc 667 |
. . . . . . 7
      
          |
86 | 85 | ralrimiva 2802 |
. . . . . 6
 
   
          |
87 | | fimaxre3 10553 |
. . . . . 6
            
           |
88 | 74, 86, 87 | syl2anc 667 |
. . . . 5
 
            
  |
89 | 88 | adantlr 721 |
. . . 4
       
 
            
  |
90 | | simpll 760 |
. . . . 5
       
 
     |
91 | | neqne 37374 |
. . . . . . 7
 
     |
92 | | elprn1 37713 |
. . . . . . 7
       
  
   |
93 | 91, 92 | sylan2 477 |
. . . . . 6
       
      |
94 | 93 | adantll 720 |
. . . . 5
       
 
      |
95 | | fzofi 12187 |
. . . . . . . 8
 ..^  |
96 | 16 | rnmptfi 37435 |
. . . . . . . 8
  ..^
  |
97 | 95, 96 | ax-mp 5 |
. . . . . . 7
 |
98 | 97 | a1i 11 |
. . . . . 6
 
    |
99 | 3 | adantr 467 |
. . . . . . . . . 10
 
        |
100 | 99, 60 | ffvelrnd 6023 |
. . . . . . . . 9
 
        |
101 | 100 | recnd 9669 |
. . . . . . . 8
 
        |
102 | 101 | adantlr 721 |
. . . . . . 7
             |
103 | 102 | abscld 13498 |
. . . . . 6
                 |
104 | 39, 16 | fnmpti 5706 |
. . . . . . . . . . 11
 ..^  |
105 | | fvelrnb 5912 |
. . . . . . . . . . 11
  ..^

  ..^         |
106 | 104, 105 | ax-mp 5 |
. . . . . . . . . 10

  ..^        |
107 | 106 | biimpi 198 |
. . . . . . . . 9
 
 ..^        |
108 | 107 | adantl 468 |
. . . . . . . 8
 
   ..^        |
109 | 7 | adantr 467 |
. . . . . . . . . . . . . . 15
 
 ..^            |
110 | | elfzofz 11935 |
. . . . . . . . . . . . . . . 16
  ..^
      |
111 | 110 | adantl 468 |
. . . . . . . . . . . . . . 15
 
 ..^        |
112 | 109, 111 | ffvelrnd 6023 |
. . . . . . . . . . . . . 14
 
 ..^        |
113 | | fzofzp1 12008 |
. . . . . . . . . . . . . . . 16
  ..^
        |
114 | 113 | adantl 468 |
. . . . . . . . . . . . . . 15
 
 ..^          |
115 | 109, 114 | ffvelrnd 6023 |
. . . . . . . . . . . . . 14
 
 ..^          |
116 | | fourierdlem71.l |
. . . . . . . . . . . . . 14
 
 ..^                   lim          |
117 | | fourierdlem71.r |
. . . . . . . . . . . . . 14
 
 ..^                   lim        |
118 | 112, 115,
46, 116, 117 | cncfioobd 37775 |
. . . . . . . . . . . . 13
 
 ..^                       
                     |
119 | 118 | 3adant3 1028 |
. . . . . . . . . . . 12
 
 ..^                           
                     |
120 | | fvres 5879 |
. . . . . . . . . . . . . . . . . . 19
                                         |
121 | 120 | fveq2d 5869 |
. . . . . . . . . . . . . . . . . 18
                                                 |
122 | 121 | breq1d 4412 |
. . . . . . . . . . . . . . . . 17
                                       
           |
123 | 122 | adantl 468 |
. . . . . . . . . . . . . . . 16
    ..^                                         
           |
124 | 123 | ralbidva 2824 |
. . . . . . . . . . . . . . 15
 
 ..^                                          
                       
   |
125 | 124 | rexbidv 2901 |
. . . . . . . . . . . . . 14
 
 ..^                                           
                        
   |
126 | 125 | 3adant3 1028 |
. . . . . . . . . . . . 13
 
 ..^                                               
                        
   |
127 | 39, 44 | mpan2 677 |
. . . . . . . . . . . . . . . . 17
  ..^
                    |
128 | | id 22 |
. . . . . . . . . . . . . . . . 17
           |
129 | 127, 128 | sylan9req 2506 |
. . . . . . . . . . . . . . . 16
   ..^                      |
130 | 129 | 3adant1 1026 |
. . . . . . . . . . . . . . 15
 
 ..^                      |
131 | 130 | raleqdv 2993 |
. . . . . . . . . . . . . 14
 
 ..^                              

           |
132 | 131 | rexbidv 2901 |
. . . . . . . . . . . . 13
 
 ..^                               
         
   |
133 | 126, 132 | bitrd 257 |
. . . . . . . . . . . 12
 
 ..^                                               
         
   |
134 | 119, 133 | mpbid 214 |
. . . . . . . . . . 11
 
 ..^                  |
135 | 134 | 3exp 1207 |
. . . . . . . . . 10
   ..^                    |
136 | 135 | adantr 467 |
. . . . . . . . 9
 
   ..^      
             |
137 | 136 | rexlimdv 2877 |
. . . . . . . 8
 
  
 ..^               
   |
138 | 108, 137 | mpd 15 |
. . . . . . 7
 
          
  |
139 | 138 | adantlr 721 |
. . . . . 6
               
  |
140 | | eqimss 3484 |
. . . . . . 7
 
   |
141 | 140 | adantl 468 |
. . . . . 6
 
     |
142 | 98, 103, 139, 141 | ssfiunibd 37527 |
. . . . 5
 
  
           |
143 | 90, 94, 142 | syl2anc 667 |
. . . 4
       
 
               |
144 | 89, 143 | pm2.61dan 800 |
. . 3
 
       
           |
145 | | simpr 463 |
. . . . . . . . 9
      ![[,] [,]](_icc.gif)    
  |
146 | | elinel2 3620 |
. . . . . . . . . 10
    ![[,] [,]](_icc.gif)  
  |
147 | 146 | ad2antlr 733 |
. . . . . . . . 9
      ![[,] [,]](_icc.gif)    
  |
148 | 145, 147 | elind 3618 |
. . . . . . . 8
      ![[,] [,]](_icc.gif)    

   |
149 | | elun1 3601 |
. . . . . . . 8
  
       |
150 | 148, 149 | syl 17 |
. . . . . . 7
      ![[,] [,]](_icc.gif)    
       |
151 | | fourierdlem71.7 |
. . . . . . . . . . . 12
   |
152 | 151 | ad2antrr 732 |
. . . . . . . . . . 11
      ![[,] [,]](_icc.gif)   
   |
153 | 7 | ad2antrr 732 |
. . . . . . . . . . 11
      ![[,] [,]](_icc.gif)   
           |
154 | | elinel1 3619 |
. . . . . . . . . . . . . 14
    ![[,] [,]](_icc.gif)  
  ![[,] [,]](_icc.gif)    |
155 | 154 | adantl 468 |
. . . . . . . . . . . . 13
 
   ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)    |
156 | | fourierdlem71.q0 |
. . . . . . . . . . . . . . . 16
       |
157 | 156 | eqcomd 2457 |
. . . . . . . . . . . . . . 15
       |
158 | 157 | adantr 467 |
. . . . . . . . . . . . . 14
 
   ![[,] [,]](_icc.gif)          |
159 | | fourierdlem71.10 |
. . . . . . . . . . . . . . . 16
       |
160 | 159 | eqcomd 2457 |
. . . . . . . . . . . . . . 15
       |
161 | 160 | adantr 467 |
. . . . . . . . . . . . . 14
 
   ![[,] [,]](_icc.gif)          |
162 | 158, 161 | oveq12d 6308 |
. . . . . . . . . . . . 13
 
   ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)        |
163 | 155, 162 | eleqtrd 2531 |
. . . . . . . . . . . 12
 
   ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)        |
164 | 163 | adantr 467 |
. . . . . . . . . . 11
      ![[,] [,]](_icc.gif)   
       ![[,] [,]](_icc.gif)        |
165 | | simpr 463 |
. . . . . . . . . . 11
      ![[,] [,]](_icc.gif)   

  |
166 | | fveq2 5865 |
. . . . . . . . . . . . . 14
           |
167 | 166 | breq1d 4412 |
. . . . . . . . . . . . 13
     
       |
168 | 167 | cbvrabv 3044 |
. . . . . . . . . . . 12
  ..^        ..^       |
169 | 168 | supeq1i 7961 |
. . . . . . . . . . 11
    ..^    
       ..^         |
170 | 152, 153,
164, 165, 169 | fourierdlem25 37994 |
. . . . . . . . . 10
      ![[,] [,]](_icc.gif)   
   ..^                  |
171 | 41 | ad2antrl 734 |
. . . . . . . . . . . . . 14
 
        ..^   |
172 | | simprr 766 |
. . . . . . . . . . . . . . 15
 
      
      |
173 | 171, 127 | syl 17 |
. . . . . . . . . . . . . . 15
 
                           |
174 | 172, 173 | eleqtrd 2531 |
. . . . . . . . . . . . . 14
 
      
                |
175 | 171, 174 | jca 535 |
. . . . . . . . . . . . 13
 
         ..^
                 |
176 | | id 22 |
. . . . . . . . . . . . . . . 16
  ..^
 ..^   |
177 | 176, 40 | syl6eleqr 2540 |
. . . . . . . . . . . . . . 15
  ..^
  |
178 | 177 | ad2antrl 734 |
. . . . . . . . . . . . . 14
 
  ..^                   |
179 | | simprr 766 |
. . . . . . . . . . . . . . 15
 
  ..^                                 |
180 | 127 | eqcomd 2457 |
. . . . . . . . . . . . . . . 16
  ..^
                    |
181 | 180 | ad2antrl 734 |
. . . . . . . . . . . . . . 15
 
  ..^                                     |
182 | 179, 181 | eleqtrd 2531 |
. . . . . . . . . . . . . 14
 
  ..^                       |
183 | 178, 182 | jca 535 |
. . . . . . . . . . . . 13
 
  ..^                 
       |
184 | 175, 183 | impbida 843 |
. . . . . . . . . . . 12
       
  ..^                   |
185 | 184 | rexbidv2 2897 |
. . . . . . . . . . 11
         ..^                   |
186 | 185 | ad2antrr 732 |
. . . . . . . . . 10
      ![[,] [,]](_icc.gif)   
         ..^                   |
187 | 170, 186 | mpbird 236 |
. . . . . . . . 9
      ![[,] [,]](_icc.gif)   
 
      |
188 | 187, 35 | sylibr 216 |
. . . . . . . 8
      ![[,] [,]](_icc.gif)   
    |
189 | | elun2 3602 |
. . . . . . . 8
         |
190 | 188, 189 | syl 17 |
. . . . . . 7
      ![[,] [,]](_icc.gif)   
        |
191 | 150, 190 | pm2.61dan 800 |
. . . . . 6
 
   ![[,] [,]](_icc.gif)       
   |
192 | 191 | ralrimiva 2802 |
. . . . 5
     ![[,] [,]](_icc.gif) 
         |
193 | | dfss3 3422 |
. . . . 5
    ![[,] [,]](_icc.gif) 
  
       ![[,] [,]](_icc.gif) 
         |
194 | 192, 193 | sylibr 216 |
. . . 4
    ![[,] [,]](_icc.gif)  
       |
195 | 14, 23, 25 | syl2anc 667 |
. . . 4
   
   
       |
196 | 194, 195 | sseqtr4d 3469 |
. . 3
    ![[,] [,]](_icc.gif)  
         |
197 | 2, 66, 144, 196 | ssfiunibd 37527 |
. 2
      ![[,] [,]](_icc.gif) 
         
  |
198 | | nfv 1761 |
. . . . . 6
   |
199 | | nfra1 2769 |
. . . . . 6
  
   ![[,] [,]](_icc.gif) 
         
 |
200 | 198, 199 | nfan 2011 |
. . . . 5
  
    ![[,] [,]](_icc.gif)           
  |
201 | | fourierdlem71.dmf |
. . . . . . . . . . . . 13
   |
202 | 201 | sselda 3432 |
. . . . . . . . . . . 12
 
   |
203 | | fourierdlem71.b |
. . . . . . . . . . . . . . . . . . 19
   |
204 | 203 | adantr 467 |
. . . . . . . . . . . . . . . . . 18
 
   |
205 | 204, 202 | resubcld 10047 |
. . . . . . . . . . . . . . . . 17
 
 
   |
206 | | fourierdlem71.t |
. . . . . . . . . . . . . . . . . . 19
   |
207 | | fourierdlem71.a |
. . . . . . . . . . . . . . . . . . . 20
   |
208 | 203, 207 | resubcld 10047 |
. . . . . . . . . . . . . . . . . . 19
     |
209 | 206, 208 | syl5eqel 2533 |
. . . . . . . . . . . . . . . . . 18
   |
210 | 209 | adantr 467 |
. . . . . . . . . . . . . . . . 17
 
   |
211 | | fourierdlem71.altb |
. . . . . . . . . . . . . . . . . . . . 21
   |
212 | 207, 203 | posdifd 10200 |
. . . . . . . . . . . . . . . . . . . . 21
       |
213 | 211, 212 | mpbid 214 |
. . . . . . . . . . . . . . . . . . . 20
     |
214 | 213, 206 | syl6breqr 4443 |
. . . . . . . . . . . . . . . . . . 19
   |
215 | 214 | gt0ne0d 10178 |
. . . . . . . . . . . . . . . . . 18
   |
216 | 215 | adantr 467 |
. . . . . . . . . . . . . . . . 17
 
   |
217 | 205, 210,
216 | redivcld 10435 |
. . . . . . . . . . . . . . . 16
 
       |
218 | 217 | flcld 12034 |
. . . . . . . . . . . . . . 15
 
           |
219 | 218 | zred 11040 |
. . . . . . . . . . . . . 14
 
           |
220 | 219, 210 | remulcld 9671 |
. . . . . . . . . . . . 13
 
             |
221 | 202, 220 | readdcld 9670 |
. . . . . . . . . . . 12
 
               |
222 | | fourierdlem71.e |
. . . . . . . . . . . . 13
 
             |
223 | 222 | fvmpt2 5957 |
. . . . . . . . . . . 12
  
                              |
224 | 202, 221,
223 | syl2anc 667 |
. . . . . . . . . . 11
 
                   |
225 | 224 | fveq2d 5869 |
. . . . . . . . . 10
 
                           |
226 | | fvex 5875 |
. . . . . . . . . . . 12
         |
227 | | eleq1 2517 |
. . . . . . . . . . . . . 14
         
           |
228 | 227 | anbi2d 710 |
. . . . . . . . . . . . 13
           
   
             |
229 | | oveq1 6297 |
. . . . . . . . . . . . . . . 16
                       |
230 | 229 | oveq2d 6306 |
. . . . . . . . . . . . . . 15
                           |
231 | 230 | fveq2d 5869 |
. . . . . . . . . . . . . 14
                    
              |
232 | 231 | eqeq1d 2453 |
. . . . . . . . . . . . 13
                     
                       |
233 | 228, 232 | imbi12d 322 |
. . . . . . . . . . . 12
             

            
  
                                  |
234 | | fourierdlem71.fxpt |
. . . . . . . . . . . 12
   
               |
235 | 226, 233,
234 | vtocl 3100 |
. . . . . . . . . . 11
                                   |
236 | 218, 235 | mpdan 674 |
. . . . . . . . . 10
 
                       |
237 | 225, 236 | eqtr2d 2486 |
. . . . . . . . 9
 
               |
238 | 237 | fveq2d 5869 |
. . . . . . . 8
 
                       |
239 | 238 | adantlr 721 |
. . . . . . 7
   
   ![[,] [,]](_icc.gif)            
                       |
240 | | fveq2 5865 |
. . . . . . . . . . . . 13
           |
241 | 240 | fveq2d 5869 |
. . . . . . . . . . . 12
                   |
242 | 241 | breq1d 4412 |
. . . . . . . . . . 11
         
           |
243 | 242 | cbvralv 3019 |
. . . . . . . . . 10
 
   ![[,] [,]](_icc.gif)           
    ![[,] [,]](_icc.gif)           
  |
244 | 243 | biimpi 198 |
. . . . . . . . 9
 
   ![[,] [,]](_icc.gif)                ![[,] [,]](_icc.gif)           
  |
245 | 244 | ad2antlr 733 |
. . . . . . . 8
   
   ![[,] [,]](_icc.gif)            
     ![[,] [,]](_icc.gif) 
         
  |
246 | | iocssicc 11722 |
. . . . . . . . . . 11
  ![(,] (,]](_ioc.gif)    ![[,] [,]](_icc.gif)   |
247 | 207 | adantr 467 |
. . . . . . . . . . . . 13
 
   |
248 | 211 | adantr 467 |
. . . . . . . . . . . . 13
 
   |
249 | | id 22 |
. . . . . . . . . . . . . . . 16
   |
250 | | oveq2 6298 |
. . . . . . . . . . . . . . . . . . 19
 
     |
251 | 250 | oveq1d 6305 |
. . . . . . . . . . . . . . . . . 18
           |
252 | 251 | fveq2d 5869 |
. . . . . . . . . . . . . . . . 17
                   |
253 | 252 | oveq1d 6305 |
. . . . . . . . . . . . . . . 16
                       |
254 | 249, 253 | oveq12d 6308 |
. . . . . . . . . . . . . . 15
                           |
255 | 254 | cbvmptv 4495 |
. . . . . . . . . . . . . 14
                             |
256 | 222, 255 | eqtri 2473 |
. . . . . . . . . . . . 13
               |
257 | 247, 204,
248, 206, 256 | fourierdlem4 37973 |
. . . . . . . . . . . 12
 
       ![(,] (,]](_ioc.gif)    |
258 | 257, 202 | ffvelrnd 6023 |
. . . . . . . . . . 11
 
       ![(,] (,]](_ioc.gif)    |
259 | 246, 258 | sseldi 3430 |
. . . . . . . . . 10
 
       ![[,] [,]](_icc.gif)    |
260 | 230 | eleq1d 2513 |
. . . . . . . . . . . . . 14
                             |
261 | 228, 260 | imbi12d 322 |
. . . . . . . . . . . . 13
             

    
  
                          |
262 | | fourierdlem71.xpt |
. . . . . . . . . . . . 13
   
       |
263 | 226, 261,
262 | vtocl 3100 |
. . . . . . . . . . . 12
                           |
264 | 218, 263 | mpdan 674 |
. . . . . . . . . . 11
 
               |
265 | 224, 264 | eqeltrd 2529 |
. . . . . . . . . 10
 
       |
266 | 259, 265 | elind 3618 |
. . . . . . . . 9
 
        ![[,] [,]](_icc.gif)     |
267 | 266 | adantlr 721 |
. . . . . . . 8
   
   ![[,] [,]](_icc.gif)            
        ![[,] [,]](_icc.gif) 
   |
268 | | fveq2 5865 |
. . . . . . . . . . 11
                   |
269 | 268 | fveq2d 5869 |
. . . . . . . . . 10
                           |
270 | 269 | breq1d 4412 |
. . . . . . . . 9
             
               |
271 | 270 | rspccva 3149 |
. . . . . . . 8
      ![[,] [,]](_icc.gif) 
         
       ![[,] [,]](_icc.gif)                  |
272 | 245, 267,
271 | syl2anc 667 |
. . . . . . 7
   
   ![[,] [,]](_icc.gif)            
               |
273 | 239, 272 | eqbrtrd 4423 |
. . . . . 6
   
   ![[,] [,]](_icc.gif)            
        
  |
274 | 273 | ex 436 |
. . . . 5
 
    ![[,] [,]](_icc.gif)           
         
   |
275 | 200, 274 | ralrimi 2788 |
. . . 4
 
    ![[,] [,]](_icc.gif)           
          
  |
276 | 275 | ex 436 |
. . 3
      ![[,] [,]](_icc.gif)           
         
   |
277 | 276 | reximdv 2861 |
. 2
       ![[,] [,]](_icc.gif)           
 
            |
278 | 197, 277 | mpd 15 |
1
           
  |