Step | Hyp | Ref
| Expression |
1 | | fourierdlem76.ch |
. . 3
   
 ..^ 
 ..^               
                 |
2 | | eqid 2451 |
. . . . 5
                    
                                |
3 | | eqid 2451 |
. . . . 5
                                                     |
4 | | eqid 2451 |
. . . . 5
                     
                                                       |
5 | | simplll 768 |
. . . . . . . . . . 11
   
 ..^ 
 ..^               
                 |
6 | 1, 5 | sylbi 199 |
. . . . . . . . . 10
   |
7 | 6 | adantr 467 |
. . . . . . . . 9
                   |
8 | | ioossicc 11720 |
. . . . . . . . . 10
      ![[,] [,]](_icc.gif)   |
9 | | fourierdlem76.a |
. . . . . . . . . . . . . 14
   |
10 | 9 | rexrd 9690 |
. . . . . . . . . . . . 13
   |
11 | 6, 10 | syl 17 |
. . . . . . . . . . . 12

  |
12 | 11 | adantr 467 |
. . . . . . . . . . 11
                   |
13 | | fourierdlem76.b |
. . . . . . . . . . . . . 14
   |
14 | 13 | rexrd 9690 |
. . . . . . . . . . . . 13
   |
15 | 6, 14 | syl 17 |
. . . . . . . . . . . 12

  |
16 | 15 | adantr 467 |
. . . . . . . . . . 11
                   |
17 | | elioore 11666 |
. . . . . . . . . . . 12
                 |
18 | 17 | adantl 468 |
. . . . . . . . . . 11
                   |
19 | 6, 9 | syl 17 |
. . . . . . . . . . . . 13

  |
20 | 19 | adantr 467 |
. . . . . . . . . . . 12
                   |
21 | | fourierdlem76.t |
. . . . . . . . . . . . . . . . . . 19
   
        |
22 | | prfi 7846 |
. . . . . . . . . . . . . . . . . . . . 21
    |
23 | 22 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
   
  |
24 | | fzfid 12186 |
. . . . . . . . . . . . . . . . . . . . 21
       |
25 | | fourierdlem76.q |
. . . . . . . . . . . . . . . . . . . . . 22
             |
26 | 25 | rnmptfi 37435 |
. . . . . . . . . . . . . . . . . . . . 21
       |
27 | | infi 7795 |
. . . . . . . . . . . . . . . . . . . . 21
         |
28 | 24, 26, 27 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . 20
         |
29 | | unfi 7838 |
. . . . . . . . . . . . . . . . . . . 20
    
          
         |
30 | 23, 28, 29 | syl2anc 667 |
. . . . . . . . . . . . . . . . . . 19
    
         |
31 | 21, 30 | syl5eqel 2533 |
. . . . . . . . . . . . . . . . . 18
   |
32 | | prssg 4127 |
. . . . . . . . . . . . . . . . . . . . . 22
 
   
      |
33 | 9, 13, 32 | syl2anc 667 |
. . . . . . . . . . . . . . . . . . . . 21
   
      |
34 | 9, 13, 33 | mpbi2and 932 |
. . . . . . . . . . . . . . . . . . . 20
      |
35 | | inss2 3653 |
. . . . . . . . . . . . . . . . . . . . . 22

          |
36 | | ioossre 11696 |
. . . . . . . . . . . . . . . . . . . . . 22
     |
37 | 35, 36 | sstri 3441 |
. . . . . . . . . . . . . . . . . . . . 21

      |
38 | 37 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
      
  |
39 | 34, 38 | unssd 3610 |
. . . . . . . . . . . . . . . . . . 19
    
      
  |
40 | 21, 39 | syl5eqss 3476 |
. . . . . . . . . . . . . . . . . 18

  |
41 | | fourierdlem76.s |
. . . . . . . . . . . . . . . . . 18
            |
42 | | fourierdlem76.n |
. . . . . . . . . . . . . . . . . 18
       |
43 | 31, 40, 41, 42 | fourierdlem36 38006 |
. . . . . . . . . . . . . . . . 17

         |
44 | 6, 43 | syl 17 |
. . . . . . . . . . . . . . . 16

         |
45 | | isof1o 6216 |
. . . . . . . . . . . . . . . 16
                  |
46 | | f1of 5814 |
. . . . . . . . . . . . . . . 16
        
          |
47 | 44, 45, 46 | 3syl 18 |
. . . . . . . . . . . . . . 15
           |
48 | 6, 40 | syl 17 |
. . . . . . . . . . . . . . 15

  |
49 | 47, 48 | fssd 5738 |
. . . . . . . . . . . . . 14
           |
50 | 49 | adantr 467 |
. . . . . . . . . . . . 13
                           |
51 | | simpllr 769 |
. . . . . . . . . . . . . . . 16
   
 ..^ 
 ..^               
                ..^   |
52 | 1, 51 | sylbi 199 |
. . . . . . . . . . . . . . 15

 ..^   |
53 | | elfzofz 11935 |
. . . . . . . . . . . . . . 15
  ..^
      |
54 | 52, 53 | syl 17 |
. . . . . . . . . . . . . 14

      |
55 | 54 | adantr 467 |
. . . . . . . . . . . . 13
                       |
56 | 50, 55 | ffvelrnd 6023 |
. . . . . . . . . . . 12
                       |
57 | 43, 45, 46 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
           |
58 | | frn 5735 |
. . . . . . . . . . . . . . . . . 18
        
  |
59 | 57, 58 | syl 17 |
. . . . . . . . . . . . . . . . 17
   |
60 | 9 | leidd 10180 |
. . . . . . . . . . . . . . . . . . . . 21

  |
61 | | fourierdlem76.altb |
. . . . . . . . . . . . . . . . . . . . . 22
   |
62 | 9, 13, 61 | ltled 9783 |
. . . . . . . . . . . . . . . . . . . . 21

  |
63 | 9, 13, 9, 60, 62 | eliccd 37601 |
. . . . . . . . . . . . . . . . . . . 20
   ![[,] [,]](_icc.gif)    |
64 | 13 | leidd 10180 |
. . . . . . . . . . . . . . . . . . . . 21

  |
65 | 9, 13, 13, 62, 64 | eliccd 37601 |
. . . . . . . . . . . . . . . . . . . 20
   ![[,] [,]](_icc.gif)    |
66 | | prssg 4127 |
. . . . . . . . . . . . . . . . . . . . 21
 
     ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)     |
67 | 9, 13, 66 | syl2anc 667 |
. . . . . . . . . . . . . . . . . . . 20
     ![[,] [,]](_icc.gif) 
  ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)     |
68 | 63, 65, 67 | mpbi2and 932 |
. . . . . . . . . . . . . . . . . . 19
      ![[,] [,]](_icc.gif)    |
69 | 35, 8 | sstri 3441 |
. . . . . . . . . . . . . . . . . . . 20

       ![[,] [,]](_icc.gif)   |
70 | 69 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
      
  ![[,] [,]](_icc.gif)    |
71 | 68, 70 | unssd 3610 |
. . . . . . . . . . . . . . . . . 18
    
      
  ![[,] [,]](_icc.gif)    |
72 | 21, 71 | syl5eqss 3476 |
. . . . . . . . . . . . . . . . 17

  ![[,] [,]](_icc.gif)    |
73 | 59, 72 | sstrd 3442 |
. . . . . . . . . . . . . . . 16
   ![[,] [,]](_icc.gif)    |
74 | 6, 73 | syl 17 |
. . . . . . . . . . . . . . 15
   ![[,] [,]](_icc.gif)    |
75 | | ffun 5731 |
. . . . . . . . . . . . . . . . 17
           |
76 | 49, 75 | syl 17 |
. . . . . . . . . . . . . . . 16
   |
77 | | fdm 5733 |
. . . . . . . . . . . . . . . . . . 19
               |
78 | 49, 77 | syl 17 |
. . . . . . . . . . . . . . . . . 18
       |
79 | 78 | eqcomd 2457 |
. . . . . . . . . . . . . . . . 17
       |
80 | 54, 79 | eleqtrd 2531 |
. . . . . . . . . . . . . . . 16

  |
81 | | fvelrn 6015 |
. . . . . . . . . . . . . . . 16
         |
82 | 76, 80, 81 | syl2anc 667 |
. . . . . . . . . . . . . . 15
       |
83 | 74, 82 | sseldd 3433 |
. . . . . . . . . . . . . 14
       ![[,] [,]](_icc.gif)    |
84 | | iccgelb 11691 |
. . . . . . . . . . . . . 14
        ![[,] [,]](_icc.gif)         |
85 | 11, 15, 83, 84 | syl3anc 1268 |
. . . . . . . . . . . . 13

      |
86 | 85 | adantr 467 |
. . . . . . . . . . . 12
                       |
87 | 56 | rexrd 9690 |
. . . . . . . . . . . . 13
                       |
88 | | fzofzp1 12008 |
. . . . . . . . . . . . . . . . 17
  ..^
        |
89 | 52, 88 | syl 17 |
. . . . . . . . . . . . . . . 16
         |
90 | 49, 89 | ffvelrnd 6023 |
. . . . . . . . . . . . . . 15
         |
91 | 90 | rexrd 9690 |
. . . . . . . . . . . . . 14
         |
92 | 91 | adantr 467 |
. . . . . . . . . . . . 13
                         |
93 | | simpr 463 |
. . . . . . . . . . . . 13
                                 |
94 | | ioogtlb 37592 |
. . . . . . . . . . . . 13
           
                     |
95 | 87, 92, 93, 94 | syl3anc 1268 |
. . . . . . . . . . . 12
                       |
96 | 20, 56, 18, 86, 95 | lelttrd 9793 |
. . . . . . . . . . 11
                   |
97 | 90 | adantr 467 |
. . . . . . . . . . . 12
                         |
98 | 6, 13 | syl 17 |
. . . . . . . . . . . . 13

  |
99 | 98 | adantr 467 |
. . . . . . . . . . . 12
                   |
100 | | iooltub 37610 |
. . . . . . . . . . . . 13
           
                       |
101 | 87, 92, 93, 100 | syl3anc 1268 |
. . . . . . . . . . . 12
                         |
102 | 89, 79 | eleqtrd 2531 |
. . . . . . . . . . . . . . . 16
     |
103 | | fvelrn 6015 |
. . . . . . . . . . . . . . . 16
             |
104 | 76, 102, 103 | syl2anc 667 |
. . . . . . . . . . . . . . 15
         |
105 | 74, 104 | sseldd 3433 |
. . . . . . . . . . . . . 14
         ![[,] [,]](_icc.gif)    |
106 | | iccleub 11690 |
. . . . . . . . . . . . . 14
          ![[,] [,]](_icc.gif)           |
107 | 11, 15, 105, 106 | syl3anc 1268 |
. . . . . . . . . . . . 13
      
  |
108 | 107 | adantr 467 |
. . . . . . . . . . . 12
                         |
109 | 18, 97, 99, 101, 108 | ltletrd 9795 |
. . . . . . . . . . 11
                   |
110 | 12, 16, 18, 96, 109 | eliood 37595 |
. . . . . . . . . 10
                       |
111 | 8, 110 | sseldi 3430 |
. . . . . . . . 9
                   ![[,] [,]](_icc.gif)    |
112 | | fourierdlem76.f |
. . . . . . . . . . 11
       |
113 | 112 | adantr 467 |
. . . . . . . . . 10
 
  ![[,] [,]](_icc.gif)  
      |
114 | | fourierdlem76.xre |
. . . . . . . . . . . 12
   |
115 | 114 | adantr 467 |
. . . . . . . . . . 11
 
  ![[,] [,]](_icc.gif)  
  |
116 | 9, 13 | iccssred 37602 |
. . . . . . . . . . . 12
   ![[,] [,]](_icc.gif) 
  |
117 | 116 | sselda 3432 |
. . . . . . . . . . 11
 
  ![[,] [,]](_icc.gif)  
  |
118 | 115, 117 | readdcld 9670 |
. . . . . . . . . 10
 
  ![[,] [,]](_icc.gif)  
    |
119 | 113, 118 | ffvelrnd 6023 |
. . . . . . . . 9
 
  ![[,] [,]](_icc.gif)  
        |
120 | 7, 111, 119 | syl2anc 667 |
. . . . . . . 8
                         |
121 | 120 | recnd 9669 |
. . . . . . 7
                         |
122 | | fourierdlem76.c |
. . . . . . . . . 10
   |
123 | 122 | recnd 9669 |
. . . . . . . . 9
   |
124 | 6, 123 | syl 17 |
. . . . . . . 8

  |
125 | 124 | adantr 467 |
. . . . . . 7
                   |
126 | 121, 125 | subcld 9986 |
. . . . . 6
                     
     |
127 | | ioossre 11696 |
. . . . . . . . 9
               |
128 | 127 | a1i 11 |
. . . . . . . 8
              
  |
129 | 128 | sselda 3432 |
. . . . . . 7
                   |
130 | 129 | recnd 9669 |
. . . . . 6
                   |
131 | | nne 2628 |
. . . . . . . . . . . 12
   |
132 | 131 | biimpi 198 |
. . . . . . . . . . 11
   |
133 | 132 | eqcomd 2457 |
. . . . . . . . . 10
   |
134 | 133 | adantl 468 |
. . . . . . . . 9
     ![[,] [,]](_icc.gif)      |
135 | | simpr 463 |
. . . . . . . . . 10
 
  ![[,] [,]](_icc.gif)  
  ![[,] [,]](_icc.gif)    |
136 | 135 | adantr 467 |
. . . . . . . . 9
     ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)    |
137 | 134, 136 | eqeltrd 2529 |
. . . . . . . 8
     ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)    |
138 | | fourierdlem76.n0 |
. . . . . . . . 9
   ![[,] [,]](_icc.gif)    |
139 | 138 | ad2antrr 732 |
. . . . . . . 8
     ![[,] [,]](_icc.gif)   
  ![[,] [,]](_icc.gif)    |
140 | 137, 139 | condan 803 |
. . . . . . 7
 
  ![[,] [,]](_icc.gif)  
  |
141 | 7, 111, 140 | syl2anc 667 |
. . . . . 6
                   |
142 | 126, 130,
141 | divcld 10383 |
. . . . 5
                      
      |
143 | | 2cnd 10682 |
. . . . . . 7
                   |
144 | 130 | halfcld 10857 |
. . . . . . . 8
                     |
145 | 144 | sincld 14184 |
. . . . . . 7
                         |
146 | 143, 145 | mulcld 9663 |
. . . . . 6
                           |
147 | 17 | recnd 9669 |
. . . . . . . . . 10
                 |
148 | 147 | adantl 468 |
. . . . . . . . 9
                   |
149 | 148 | halfcld 10857 |
. . . . . . . 8
                     |
150 | 149 | sincld 14184 |
. . . . . . 7
                         |
151 | | 2ne0 10702 |
. . . . . . . 8
 |
152 | 151 | a1i 11 |
. . . . . . 7
                   |
153 | | fourierdlem76.ab |
. . . . . . . . . . 11
   ![[,] [,]](_icc.gif) 
   ![[,] [,]](_icc.gif)    |
154 | 6, 153 | syl 17 |
. . . . . . . . . 10
   ![[,] [,]](_icc.gif) 
   ![[,] [,]](_icc.gif)    |
155 | 154 | adantr 467 |
. . . . . . . . 9
                   ![[,] [,]](_icc.gif)     ![[,] [,]](_icc.gif)    |
156 | 155, 111 | sseldd 3433 |
. . . . . . . 8
                    ![[,] [,]](_icc.gif)    |
157 | | fourierdlem44 38015 |
. . . . . . . 8
     ![[,] [,]](_icc.gif)           |
158 | 156, 141,
157 | syl2anc 667 |
. . . . . . 7
                         |
159 | 143, 150,
152, 158 | mulne0d 10264 |
. . . . . 6
                           |
160 | 130, 146,
159 | divcld 10383 |
. . . . 5
                             |
161 | | eqid 2451 |
. . . . . 6
                                                 |
162 | | eqid 2451 |
. . . . . 6
                                 |
163 | 141 | neneqd 2629 |
. . . . . . . 8
                
  |
164 | | elsn 3982 |
. . . . . . . 8
     |
165 | 163, 164 | sylnibr 307 |
. . . . . . 7
                
    |
166 | 130, 165 | eldifd 3415 |
. . . . . 6
                       |
167 | | eqid 2451 |
. . . . . . 7
                                        
    |
168 | | eqid 2451 |
. . . . . . 7
                                 |
169 | | elfzofz 11935 |
. . . . . . . . . . . . . . 15
  ..^
      |
170 | 169 | adantl 468 |
. . . . . . . . . . . . . 14
 
 ..^        |
171 | | pire 23413 |
. . . . . . . . . . . . . . . . . . . . 21
 |
172 | 171 | renegcli 9935 |
. . . . . . . . . . . . . . . . . . . 20
  |
173 | 172 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
    |
174 | 173, 114 | readdcld 9670 |
. . . . . . . . . . . . . . . . . 18
      |
175 | 171 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
   |
176 | 175, 114 | readdcld 9670 |
. . . . . . . . . . . . . . . . . 18
     |
177 | 174, 176 | iccssred 37602 |
. . . . . . . . . . . . . . . . 17
      ![[,] [,]](_icc.gif)   
  |
178 | 177 | adantr 467 |
. . . . . . . . . . . . . . . 16
 
 ..^       ![[,] [,]](_icc.gif)      |
179 | | fourierdlem76.p |
. . . . . . . . . . . . . . . . . . 19
 
                        ..^                |
180 | | fourierdlem76.m |
. . . . . . . . . . . . . . . . . . 19
   |
181 | | fourierdlem76.v |
. . . . . . . . . . . . . . . . . . 19
       |
182 | 179, 180,
181 | fourierdlem15 37984 |
. . . . . . . . . . . . . . . . . 18
              ![[,] [,]](_icc.gif)      |
183 | 182 | adantr 467 |
. . . . . . . . . . . . . . . . 17
 
 ..^               ![[,] [,]](_icc.gif)      |
184 | 183, 170 | ffvelrnd 6023 |
. . . . . . . . . . . . . . . 16
 
 ..^           ![[,] [,]](_icc.gif)      |
185 | 178, 184 | sseldd 3433 |
. . . . . . . . . . . . . . 15
 
 ..^        |
186 | 114 | adantr 467 |
. . . . . . . . . . . . . . 15
 
 ..^    |
187 | 185, 186 | resubcld 10047 |
. . . . . . . . . . . . . 14
 
 ..^          |
188 | 25 | fvmpt2 5957 |
. . . . . . . . . . . . . 14
                         |
189 | 170, 187,
188 | syl2anc 667 |
. . . . . . . . . . . . 13
 
 ..^              |
190 | 189, 187 | eqeltrd 2529 |
. . . . . . . . . . . 12
 
 ..^        |
191 | 190 | adantlr 721 |
. . . . . . . . . . 11
    ..^   ..^ 
      |
192 | 191 | adantr 467 |
. . . . . . . . . 10
   
 ..^ 
 ..^               
                     |
193 | 1, 192 | sylbi 199 |
. . . . . . . . 9
       |
194 | | fveq2 5865 |
. . . . . . . . . . . . . . . . . 18
           |
195 | 194 | oveq1d 6305 |
. . . . . . . . . . . . . . . . 17
               |
196 | 195 | cbvmptv 4495 |
. . . . . . . . . . . . . . . 16
                         |
197 | 25, 196 | eqtri 2473 |
. . . . . . . . . . . . . . 15
             |
198 | 197 | a1i 11 |
. . . . . . . . . . . . . 14
 
 ..^                |
199 | | fveq2 5865 |
. . . . . . . . . . . . . . . 16
               |
200 | 199 | oveq1d 6305 |
. . . . . . . . . . . . . . 15
                   |
201 | 200 | adantl 468 |
. . . . . . . . . . . . . 14
    ..^                     |
202 | | fzofzp1 12008 |
. . . . . . . . . . . . . . 15
  ..^
        |
203 | 202 | adantl 468 |
. . . . . . . . . . . . . 14
 
 ..^          |
204 | 183, 203 | ffvelrnd 6023 |
. . . . . . . . . . . . . . . 16
 
 ..^             ![[,] [,]](_icc.gif)      |
205 | 178, 204 | sseldd 3433 |
. . . . . . . . . . . . . . 15
 
 ..^          |
206 | 205, 186 | resubcld 10047 |
. . . . . . . . . . . . . 14
 
 ..^            |
207 | 198, 201,
203, 206 | fvmptd 5954 |
. . . . . . . . . . . . 13
 
 ..^                  |
208 | 207, 206 | eqeltrd 2529 |
. . . . . . . . . . . 12
 
 ..^          |
209 | 208 | adantlr 721 |
. . . . . . . . . . 11
    ..^   ..^ 
        |
210 | 209 | adantr 467 |
. . . . . . . . . 10
   
 ..^ 
 ..^               
                       |
211 | 1, 210 | sylbi 199 |
. . . . . . . . 9
         |
212 | 179 | fourierdlem2 37971 |
. . . . . . . . . . . . . . . . . 18
 
   
                         ..^                 |
213 | 180, 212 | syl 17 |
. . . . . . . . . . . . . . . . 17
                               ..^                 |
214 | 181, 213 | mpbid 214 |
. . . . . . . . . . . . . . . 16
                          ..^                |
215 | 214 | simprrd 767 |
. . . . . . . . . . . . . . 15
   ..^              |
216 | 215 | r19.21bi 2757 |
. . . . . . . . . . . . . 14
 
 ..^              |
217 | 185, 205,
186, 216 | ltsub1dd 10225 |
. . . . . . . . . . . . 13
 
 ..^                  |
218 | 217, 189,
207 | 3brtr4d 4433 |
. . . . . . . . . . . 12
 
 ..^              |
219 | 218 | adantlr 721 |
. . . . . . . . . . 11
    ..^   ..^ 
            |
220 | 219 | adantr 467 |
. . . . . . . . . 10
   
 ..^ 
 ..^               
                  
        |
221 | 1, 220 | sylbi 199 |
. . . . . . . . 9
    
        |
222 | 1 | biimpi 198 |
. . . . . . . . . . . . . . . . . 18
     ..^ 
 ..^               
                 |
223 | 222 | simplrd 763 |
. . . . . . . . . . . . . . . . 17

 ..^   |
224 | 6, 223, 185 | syl2anc 667 |
. . . . . . . . . . . . . . . 16
       |
225 | 224 | rexrd 9690 |
. . . . . . . . . . . . . . 15
       |
226 | 225 | adantr 467 |
. . . . . . . . . . . . . 14
                       |
227 | 6, 223, 205 | syl2anc 667 |
. . . . . . . . . . . . . . . 16
         |
228 | 227 | rexrd 9690 |
. . . . . . . . . . . . . . 15
         |
229 | 228 | adantr 467 |
. . . . . . . . . . . . . 14
                         |
230 | 6, 114 | syl 17 |
. . . . . . . . . . . . . . . 16

  |
231 | 230 | adantr 467 |
. . . . . . . . . . . . . . 15
                   |
232 | | elioore 11666 |
. . . . . . . . . . . . . . . 16
                 |
233 | 232 | adantl 468 |
. . . . . . . . . . . . . . 15
                   |
234 | 231, 233 | readdcld 9670 |
. . . . . . . . . . . . . 14
                 
   |
235 | 6, 223, 189 | syl2anc 667 |
. . . . . . . . . . . . . . . . . 18
             |
236 | 235 | oveq2d 6306 |
. . . . . . . . . . . . . . . . 17
                 |
237 | 230 | recnd 9669 |
. . . . . . . . . . . . . . . . . 18

  |
238 | 224 | recnd 9669 |
. . . . . . . . . . . . . . . . . 18
       |
239 | 237, 238 | pncan3d 9989 |
. . . . . . . . . . . . . . . . 17
               |
240 | 236, 239 | eqtr2d 2486 |
. . . . . . . . . . . . . . . 16
             |
241 | 240 | adantr 467 |
. . . . . . . . . . . . . . 15
                             |
242 | 193 | adantr 467 |
. . . . . . . . . . . . . . . 16
                       |
243 | 193 | rexrd 9690 |
. . . . . . . . . . . . . . . . . 18
       |
244 | 243 | adantr 467 |
. . . . . . . . . . . . . . . . 17
                       |
245 | 211 | rexrd 9690 |
. . . . . . . . . . . . . . . . . 18
         |
246 | 245 | adantr 467 |
. . . . . . . . . . . . . . . . 17
                         |
247 | | simpr 463 |
. . . . . . . . . . . . . . . . 17
                                 |
248 | | ioogtlb 37592 |
. . . . . . . . . . . . . . . . 17
           
                     |
249 | 244, 246,
247, 248 | syl3anc 1268 |
. . . . . . . . . . . . . . . 16
                       |
250 | 242, 233,
231, 249 | ltadd2dd 9794 |
. . . . . . . . . . . . . . 15
                 
         |
251 | 241, 250 | eqbrtrd 4423 |
. . . . . . . . . . . . . 14
                         |
252 | 211 | adantr 467 |
. . . . . . . . . . . . . . . 16
                         |
253 | | iooltub 37610 |
. . . . . . . . . . . . . . . . 17
           
                       |
254 | 244, 246,
247, 253 | syl3anc 1268 |
. . . . . . . . . . . . . . . 16
                         |
255 | 233, 252,
231, 254 | ltadd2dd 9794 |
. . . . . . . . . . . . . . 15
                 
           |
256 | 6, 223, 207 | syl2anc 667 |
. . . . . . . . . . . . . . . . . 18
                 |
257 | 256 | oveq2d 6306 |
. . . . . . . . . . . . . . . . 17
                     |
258 | 227 | recnd 9669 |
. . . . . . . . . . . . . . . . . 18
         |
259 | 237, 258 | pncan3d 9989 |
. . . . . . . . . . . . . . . . 17
                   |
260 | 257, 259 | eqtrd 2485 |
. . . . . . . . . . . . . . . 16
                 |
261 | 260 | adantr 467 |
. . . . . . . . . . . . . . 15
                 
               |
262 | 255, 261 | breqtrd 4427 |
. . . . . . . . . . . . . 14
                 
         |
263 | 226, 229,
234, 251, 262 | eliood 37595 |
. . . . . . . . . . . . 13
                 
                 |
264 | | fvres 5879 |
. . . . . . . . . . . . 13
                                          
    |
265 | 263, 264 | syl 17 |
. . . . . . . . . . . 12
                                          
    |
266 | 265 | eqcomd 2457 |
. . . . . . . . . . 11
                                          
    |
267 | 266 | mpteq2dva 4489 |
. . . . . . . . . 10
                   
                                           |
268 | | ioosscn 37591 |
. . . . . . . . . . . 12
               |
269 | 268 | a1i 11 |
. . . . . . . . . . 11
              
  |
270 | | fourierdlem76.fcn |
. . . . . . . . . . . 12
 
 ..^                                      |
271 | 6, 223, 270 | syl2anc 667 |
. . . . . . . . . . 11
                                     |
272 | | ioosscn 37591 |
. . . . . . . . . . . 12
               |
273 | 272 | a1i 11 |
. . . . . . . . . . 11
              
  |
274 | 269, 271,
273, 237, 263 | fourierdlem23 37992 |
. . . . . . . . . 10
                                   
                       |
275 | 267, 274 | eqeltrd 2529 |
. . . . . . . . 9
                   
                       |
276 | 6, 112 | syl 17 |
. . . . . . . . . 10
       |
277 | | ioossre 11696 |
. . . . . . . . . . 11
               |
278 | 277 | a1i 11 |
. . . . . . . . . 10
              
  |
279 | | eqid 2451 |
. . . . . . . . . 10
                                        
    |
280 | | ioossre 11696 |
. . . . . . . . . . 11
               |
281 | 280 | a1i 11 |
. . . . . . . . . 10
              
  |
282 | 233, 254 | ltned 9771 |
. . . . . . . . . 10
                         |
283 | | fourierdlem76.l |
. . . . . . . . . . . 12
 
 ..^                   lim          |
284 | 6, 223, 283 | syl2anc 667 |
. . . . . . . . . . 11

                 lim          |
285 | 260 | eqcomd 2457 |
. . . . . . . . . . . 12
                 |
286 | 285 | oveq2d 6306 |
. . . . . . . . . . 11
                  lim         
               lim 
          |
287 | 284, 286 | eleqtrd 2531 |
. . . . . . . . . 10

                 lim            |
288 | 211 | recnd 9669 |
. . . . . . . . . 10
         |
289 | 276, 230,
278, 279, 263, 281, 282, 287, 288 | fourierdlem53 38023 |
. . . . . . . . 9

                   
   lim          |
290 | 49, 54 | ffvelrnd 6023 |
. . . . . . . . 9
       |
291 | | elfzoelz 11920 |
. . . . . . . . . . . 12
  ..^
  |
292 | | zre 10941 |
. . . . . . . . . . . 12
   |
293 | 52, 291, 292 | 3syl 18 |
. . . . . . . . . . 11

  |
294 | 293 | ltp1d 10537 |
. . . . . . . . . 10

    |
295 | | isorel 6217 |
. . . . . . . . . . 11
 
           
              
         |
296 | 44, 54, 89, 295 | syl12anc 1266 |
. . . . . . . . . 10
       
         |
297 | 294, 296 | mpbid 214 |
. . . . . . . . 9
    
        |
298 | 1 | simprbi 466 |
. . . . . . . . 9
              
                |
299 | | eqid 2451 |
. . . . . . . . 9
                                                                                                   |
300 | | eqid 2451 |
. . . . . . . . 9
   ℂfld ↾t                             ℂfld ↾t                           |
301 | 193, 211,
221, 275, 289, 290, 90, 297, 298, 299, 300 | fourierdlem33 38003 |
. . . . . . . 8
                                    
                                 
                  lim          |
302 | | eqidd 2452 |
. . . . . . . . . 10
                                 
                           |
303 | | simpr 463 |
. . . . . . . . . . . 12
               
               |
304 | 303 | oveq2d 6306 |
. . . . . . . . . . 11
               
                   |
305 | 304 | fveq2d 5869 |
. . . . . . . . . 10
               
          
                |
306 | 243 | adantr 467 |
. . . . . . . . . . 11
                     |
307 | 245 | adantr 467 |
. . . . . . . . . . 11
                       |
308 | 90 | adantr 467 |
. . . . . . . . . . 11
                       |
309 | 193, 211,
290, 90, 297, 298 | fourierdlem10 37979 |
. . . . . . . . . . . . . 14
               
         |
310 | 309 | simpld 461 |
. . . . . . . . . . . . 13
    
      |
311 | 193, 290,
90, 310, 297 | lelttrd 9793 |
. . . . . . . . . . . 12
    
        |
312 | 311 | adantr 467 |
. . . . . . . . . . 11
                  
        |
313 | 211 | adantr 467 |
. . . . . . . . . . . 12
                       |
314 | 309 | simprd 465 |
. . . . . . . . . . . . 13
      
        |
315 | 314 | adantr 467 |
. . . . . . . . . . . 12
                    
        |
316 | | neqne 37374 |
. . . . . . . . . . . . . 14
                           |
317 | 316 | necomd 2679 |
. . . . . . . . . . . . 13
                           |
318 | 317 | adantl 468 |
. . . . . . . . . . . 12
                             |
319 | 308, 313,
315, 318 | leneltd 9789 |
. . . . . . . . . . 11
                             |
320 | 306, 307,
308, 312, 319 | eliood 37595 |
. . . . . . . . . 10
                                     |
321 | 230, 90 | readdcld 9670 |
. . . . . . . . . . . 12
           |
322 | 276, 321 | ffvelrnd 6023 |
. . . . . . . . . . 11
    
          |
323 | 322 | adantr 467 |
. . . . . . . . . 10
                  
          |
324 | 302, 305,
320, 323 | fvmptd 5954 |
. . . . . . . . 9
                                  
                          |
325 | 324 | ifeq2da 3912 |
. . . . . . . 8
                                    
                                            |
326 | 298 | resmptd 5156 |
. . . . . . . . 9
                    
                                          |
327 | 326 | oveq1d 6305 |
. . . . . . . 8
                                        lim                               lim          |
328 | 301, 325,
327 | 3eltr3d 2543 |
. . . . . . 7
                    
                                lim          |
329 | | ax-resscn 9596 |
. . . . . . . . 9
 |
330 | 128, 329 | syl6ss 3444 |
. . . . . . . 8
              
  |
331 | 90 | recnd 9669 |
. . . . . . . 8
         |
332 | 168, 330,
124, 331 | constlimc 37704 |
. . . . . . 7

                 lim          |
333 | 167, 168,
161, 121, 125, 328, 332 | sublimc 37733 |
. . . . . 6
                     
                              
    lim          |
334 | 330, 162,
331 | idlimc 37706 |
. . . . . 6
                        lim          |
335 | 6, 105 | jca 535 |
. . . . . . 7
          ![[,] [,]](_icc.gif)     |
336 | | eleq1 2517 |
. . . . . . . . . 10
          ![[,] [,]](_icc.gif) 
        ![[,] [,]](_icc.gif)     |
337 | 336 | anbi2d 710 |
. . . . . . . . 9
        
  ![[,] [,]](_icc.gif)  
         ![[,] [,]](_icc.gif)      |
338 | | neeq1 2686 |
. . . . . . . . 9
                 |
339 | 337, 338 | imbi12d 322 |
. . . . . . . 8
         
  ![[,] [,]](_icc.gif)              ![[,] [,]](_icc.gif)             |
340 | 339, 140 | vtoclg 3107 |
. . . . . . 7
        
        ![[,] [,]](_icc.gif)            |
341 | 90, 335, 340 | sylc 62 |
. . . . . 6
         |
342 | 161, 162,
2, 126, 166, 333, 334, 341, 141 | divlimc 37737 |
. . . . 5
                                                             
     lim          |
343 | | eqid 2451 |
. . . . . 6
                                                 |
344 | 143, 150 | mulcld 9663 |
. . . . . . 7
                           |
345 | 159 | neneqd 2629 |
. . . . . . . 8
                           |
346 | | 2re 10679 |
. . . . . . . . . . 11
 |
347 | 346 | a1i 11 |
. . . . . . . . . 10
                   |
348 | 17 | rehalfcld 10859 |
. . . . . . . . . . . 12
                   |
349 | 348 | resincld 14197 |
. . . . . . . . . . 11
                       |
350 | 349 | adantl 468 |
. . . . . . . . . 10
                         |
351 | 347, 350 | remulcld 9671 |
. . . . . . . . 9
                           |
352 | | elsncg 3991 |
. . . . . . . . 9
        
          
           |
353 | 351, 352 | syl 17 |
. . . . . . . 8
                                       |
354 | 345, 353 | mtbird 303 |
. . . . . . 7
                             |
355 | 344, 354 | eldifd 3415 |
. . . . . 6
                               |
356 | | eqid 2451 |
. . . . . . 7
                                 |
357 | | eqid 2451 |
. . . . . . 7
                                             |
358 | | 2cnd 10682 |
. . . . . . . 8

  |
359 | 356, 330,
358, 331 | constlimc 37704 |
. . . . . . 7

                 lim          |
360 | 348 | ad2antrl 734 |
. . . . . . . 8
                                 |
361 | | recn 9629 |
. . . . . . . . . 10
   |
362 | 361 | sincld 14184 |
. . . . . . . . 9
       |
363 | 362 | adantl 468 |
. . . . . . . 8
         |
364 | | eqid 2451 |
. . . . . . . . 9
                                     |
365 | | 2cn 10680 |
. . . . . . . . . . 11
 |
366 | | eldifsn 4097 |
. . . . . . . . . . 11
         |
367 | 365, 151,
366 | mpbir2an 931 |
. . . . . . . . . 10
     |
368 | 367 | a1i 11 |
. . . . . . . . 9
                       |
369 | 151 | a1i 11 |
. . . . . . . . 9

  |
370 | 162, 356,
364, 148, 368, 334, 359, 369, 152 | divlimc 37737 |
. . . . . . . 8
                            lim          |
371 | | sinf 14178 |
. . . . . . . . . . . . . 14
     |
372 | 371 | a1i 11 |
. . . . . . . . . . . . 13
      |
373 | 329 | a1i 11 |
. . . . . . . . . . . . 13
  |
374 | 372, 373 | feqresmpt 5919 |
. . . . . . . . . . . 12
          |
375 | 374 | trud 1453 |
. . . . . . . . . . 11
         |
376 | | resincncf 37752 |
. . . . . . . . . . 11
       |
377 | 375, 376 | eqeltrri 2526 |
. . . . . . . . . 10
           |
378 | 377 | a1i 11 |
. . . . . . . . 9
             |
379 | 90 | rehalfcld 10859 |
. . . . . . . . 9
           |
380 | | fveq2 5865 |
. . . . . . . . 9
                           |
381 | 378, 379,
380 | cnmptlimc 22845 |
. . . . . . . 8
                    lim            |
382 | | fveq2 5865 |
. . . . . . . 8
               |
383 | | fveq2 5865 |
. . . . . . . . 9
                               |
384 | 383 | ad2antll 735 |
. . . . . . . 8
                                                 |
385 | 360, 363,
370, 381, 382, 384 | limcco 22848 |
. . . . . . 7
                                    lim          |
386 | 356, 357,
343, 143, 150, 359, 385 | mullimc 37696 |
. . . . . 6
                                        lim          |
387 | 331 | halfcld 10857 |
. . . . . . . 8
           |
388 | 387 | sincld 14184 |
. . . . . . 7
               |
389 | 154, 105 | sseldd 3433 |
. . . . . . . 8
          ![[,] [,]](_icc.gif)    |
390 | | fourierdlem44 38015 |
. . . . . . . 8
           ![[,] [,]](_icc.gif)                       |
391 | 389, 341,
390 | syl2anc 667 |
. . . . . . 7
               |
392 | 358, 388,
369, 391 | mulne0d 10264 |
. . . . . 6
                 |
393 | 162, 343,
3, 148, 355, 334, 386, 392, 159 | divlimc 37737 |
. . . . 5
                                                  lim          |
394 | 2, 3, 4, 142, 160, 342, 393 | mullimc 37696 |
. . . 4
                                                                                                       lim          |
395 | | fourierdlem76.d |
. . . . 5
                                                                |
396 | 395 | a1i 11 |
. . . 4

                                                                 |
397 | | fourierdlem76.o |
. . . . . . 7
   ![[,] [,]](_icc.gif)                          |
398 | 397 | reseq1i 5101 |
. . . . . 6
                    ![[,] [,]](_icc.gif)                        
                |
399 | | ioossicc 11720 |
. . . . . . . 8
                    ![[,] [,]](_icc.gif)         |
400 | | iccss 11702 |
. . . . . . . . 9
        
              ![[,] [,]](_icc.gif)          ![[,] [,]](_icc.gif)    |
401 | 19, 98, 85, 107, 400 | syl22anc 1269 |
. . . . . . . 8
       ![[,] [,]](_icc.gif)       
  ![[,] [,]](_icc.gif)    |
402 | 399, 401 | syl5ss 3443 |
. . . . . . 7
              
  ![[,] [,]](_icc.gif)    |
403 | 402 | resmptd 5156 |
. . . . . 6
     ![[,] [,]](_icc.gif)        
                                                    
                  |
404 | 398, 403 | syl5eq 2497 |
. . . . 5
                                      
                  |
405 | 404 | oveq1d 6305 |
. . . 4
                  lim                                               lim          |
406 | 394, 396,
405 | 3eltr4d 2544 |
. . 3

                 lim          |
407 | 1, 406 | sylbir 217 |
. 2
   
 ..^ 
 ..^               
              
                 lim          |
408 | 242, 249 | gtned 9770 |
. . . . . . . . . 10
                       |
409 | | fourierdlem76.r |
. . . . . . . . . . . 12
 
 ..^                   lim        |
410 | 6, 223, 409 | syl2anc 667 |
. . . . . . . . . . 11

                 lim        |
411 | 240 | oveq2d 6306 |
. . . . . . . . . . 11
                  lim       
               lim 
        |
412 | 410, 411 | eleqtrd 2531 |
. . . . . . . . . 10

                 lim          |
413 | 193 | recnd 9669 |
. . . . . . . . . 10
       |
414 | 276, 230,
278, 279, 263, 281, 408, 412, 413 | fourierdlem53 38023 |
. . . . . . . . 9

                   
   lim        |
415 | | eqid 2451 |
. . . . . . . . 9
                                                                                       |
416 | | eqid 2451 |
. . . . . . . . 9
   ℂfld ↾t                   ℂfld
↾t                 |
417 | 193, 211,
221, 275, 414, 290, 90, 297, 298, 415, 416 | fourierdlem32 38002 |
. . . . . . . 8
                                
                               
                  lim        |
418 | | eqidd 2452 |
. . . . . . . . . 10
                             
                           |
419 | | oveq2 6298 |
. . . . . . . . . . . 12
     
         |
420 | 419 | fveq2d 5869 |
. . . . . . . . . . 11
              
        |
421 | 420 | adantl 468 |
. . . . . . . . . 10
           
        
              |
422 | 243 | adantr 467 |
. . . . . . . . . . 11
                 |
423 | 245 | adantr 467 |
. . . . . . . . . . 11
                   |
424 | 290 | adantr 467 |
. . . . . . . . . . 11
                 |
425 | 193 | adantr 467 |
. . . . . . . . . . . 12
   |