Step | Hyp | Ref
| Expression |
1 | | eleq1 2517 |
. . . . . 6
 
   |
2 | 1 | anbi2d 710 |
. . . . 5
  

     |
3 | | fveq2 5865 |
. . . . . 6
           |
4 | | fveq2 5865 |
. . . . . . . . . 10
           |
5 | 4 | fveq1d 5867 |
. . . . . . . . 9
                       |
6 | 5 | oveq2d 6306 |
. . . . . . . 8
                                   |
7 | 6 | adantr 467 |
. . . . . . 7
 
                                        |
8 | 7 | itgeq2dv 22739 |
. . . . . 6
                                                   |
9 | 3, 8 | eqeq12d 2466 |
. . . . 5
                                                             |
10 | 2, 9 | imbi12d 322 |
. . . 4
   
                                                                 |
11 | | fourierdlem111.6 |
. . . . . 6
       |
12 | 11 | adantr 467 |
. . . . 5
 

      |
13 | | eqid 2451 |
. . . . 5
           |
14 | | ioossre 11696 |
. . . . . . . . 9
      |
15 | 14 | a1i 11 |
. . . . . . . 8
     
  |
16 | 11, 15 | feqresmpt 5919 |
. . . . . . 7
                     |
17 | | ioossicc 11720 |
. . . . . . . . 9
        ![[,] [,]](_icc.gif)   |
18 | 17 | a1i 11 |
. . . . . . . 8
     
   ![[,] [,]](_icc.gif)    |
19 | | ioombl 22518 |
. . . . . . . . 9
      |
20 | 19 | a1i 11 |
. . . . . . . 8
     
  |
21 | 11 | adantr 467 |
. . . . . . . . 9
 
   ![[,] [,]](_icc.gif)         |
22 | | pire 23413 |
. . . . . . . . . . . . . . 15
 |
23 | 22 | renegcli 9935 |
. . . . . . . . . . . . . 14
  |
24 | 23, 22 | elicc2i 11700 |
. . . . . . . . . . . . 13
    ![[,] [,]](_icc.gif) 
     |
25 | 24 | simp1bi 1023 |
. . . . . . . . . . . 12
    ![[,] [,]](_icc.gif)    |
26 | 25 | ssriv 3436 |
. . . . . . . . . . 11
   ![[,] [,]](_icc.gif)   |
27 | 26 | a1i 11 |
. . . . . . . . . 10
    ![[,] [,]](_icc.gif) 
  |
28 | 27 | sselda 3432 |
. . . . . . . . 9
 
   ![[,] [,]](_icc.gif)     |
29 | 21, 28 | ffvelrnd 6023 |
. . . . . . . 8
 
   ![[,] [,]](_icc.gif)         |
30 | 11, 27 | feqresmpt 5919 |
. . . . . . . . 9
     ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)         |
31 | | fourierdlem111.p |
. . . . . . . . . 10
 
                  
 ..^                |
32 | | fourierdlem111.m |
. . . . . . . . . 10
   |
33 | | fourierdlem111.q |
. . . . . . . . . 10
       |
34 | | ax-resscn 9596 |
. . . . . . . . . . . . 13
 |
35 | 34 | a1i 11 |
. . . . . . . . . . . 12

  |
36 | 11, 35 | fssd 5738 |
. . . . . . . . . . 11
       |
37 | 36, 27 | fssresd 5750 |
. . . . . . . . . 10
     ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)      |
38 | | ioossicc 11720 |
. . . . . . . . . . . . 13
                    ![[,] [,]](_icc.gif)         |
39 | 23 | rexri 9693 |
. . . . . . . . . . . . . . 15
  |
40 | 39 | a1i 11 |
. . . . . . . . . . . . . 14
 
 ..^     |
41 | 22 | rexri 9693 |
. . . . . . . . . . . . . . 15
 |
42 | 41 | a1i 11 |
. . . . . . . . . . . . . 14
 
 ..^    |
43 | 31, 32, 33 | fourierdlem15 37984 |
. . . . . . . . . . . . . . 15
            ![[,] [,]](_icc.gif)    |
44 | 43 | adantr 467 |
. . . . . . . . . . . . . 14
 
 ..^             ![[,] [,]](_icc.gif)    |
45 | | simpr 463 |
. . . . . . . . . . . . . 14
 
 ..^   ..^   |
46 | 40, 42, 44, 45 | fourierdlem8 37977 |
. . . . . . . . . . . . 13
 
 ..^        ![[,] [,]](_icc.gif)           ![[,] [,]](_icc.gif)    |
47 | 38, 46 | syl5ss 3443 |
. . . . . . . . . . . 12
 
 ..^                   ![[,] [,]](_icc.gif)    |
48 | 47 | resabs1d 5134 |
. . . . . . . . . . 11
 
 ..^       ![[,] [,]](_icc.gif)                                    |
49 | | fourierdlem111.fcn |
. . . . . . . . . . 11
 
 ..^                                      |
50 | 48, 49 | eqeltrd 2529 |
. . . . . . . . . 10
 
 ..^       ![[,] [,]](_icc.gif)                                      |
51 | | fourierdlem111.r |
. . . . . . . . . . 11
 
 ..^                   lim        |
52 | 48 | oveq1d 6305 |
. . . . . . . . . . 11
 
 ..^    
   ![[,] [,]](_icc.gif)                  lim       
               lim        |
53 | 51, 52 | eleqtrrd 2532 |
. . . . . . . . . 10
 
 ..^        ![[,] [,]](_icc.gif)                  lim        |
54 | | fourierdlem111.l |
. . . . . . . . . . 11
 
 ..^                   lim          |
55 | 48 | oveq1d 6305 |
. . . . . . . . . . 11
 
 ..^    
   ![[,] [,]](_icc.gif)                  lim         
               lim          |
56 | 54, 55 | eleqtrrd 2532 |
. . . . . . . . . 10
 
 ..^        ![[,] [,]](_icc.gif)                  lim          |
57 | 31, 32, 33, 37, 50, 53, 56 | fourierdlem69 38039 |
. . . . . . . . 9
     ![[,] [,]](_icc.gif)      |
58 | 30, 57 | eqeltrrd 2530 |
. . . . . . . 8
     ![[,] [,]](_icc.gif)          |
59 | 18, 20, 29, 58 | iblss 22762 |
. . . . . . 7
               |
60 | 16, 59 | eqeltrd 2529 |
. . . . . 6
           |
61 | 60 | adantr 467 |
. . . . 5
 

          |
62 | | fourierdlem111.a |
. . . . 5
                         |
63 | | fourierdlem111.b |
. . . . 5
                         |
64 | | fourierdlem111.x |
. . . . . 6
   |
65 | 64 | adantr 467 |
. . . . 5
 

  |
66 | | fourierdlem111.s |
. . . . 5
                                           |
67 | | fourierdlem111.d |
. . . . 5
                                            |
68 | | simpr 463 |
. . . . 5
 

  |
69 | 12, 13, 61, 62, 63, 65, 66, 67, 68 | fourierdlem83 38053 |
. . . 4
 

                              |
70 | 10, 69 | chvarv 2107 |
. . 3
 

                              |
71 | 23 | a1i 11 |
. . . . 5
 

   |
72 | 22 | a1i 11 |
. . . . 5
 

  |
73 | 36 | adantr 467 |
. . . . . . . 8
 
   ![[,] [,]](_icc.gif)         |
74 | 25 | adantl 468 |
. . . . . . . 8
 
   ![[,] [,]](_icc.gif)     |
75 | 73, 74 | ffvelrnd 6023 |
. . . . . . 7
 
   ![[,] [,]](_icc.gif)         |
76 | 75 | adantlr 721 |
. . . . . 6
       ![[,] [,]](_icc.gif)         |
77 | 67 | dirkerf 37959 |
. . . . . . . . 9
           |
78 | 77 | ad2antlr 733 |
. . . . . . . 8
       ![[,] [,]](_icc.gif)             |
79 | 64 | adantr 467 |
. . . . . . . . . 10
 
   ![[,] [,]](_icc.gif)     |
80 | 74, 79 | resubcld 10047 |
. . . . . . . . 9
 
   ![[,] [,]](_icc.gif)       |
81 | 80 | adantlr 721 |
. . . . . . . 8
       ![[,] [,]](_icc.gif)       |
82 | 78, 81 | ffvelrnd 6023 |
. . . . . . 7
       ![[,] [,]](_icc.gif)               |
83 | 82 | recnd 9669 |
. . . . . 6
       ![[,] [,]](_icc.gif)               |
84 | 76, 83 | mulcld 9663 |
. . . . 5
       ![[,] [,]](_icc.gif)                     |
85 | 71, 72, 84 | itgioo 22773 |
. . . 4
 

                            ![[,] [,]](_icc.gif)                      |
86 | | fvres 5879 |
. . . . . . . 8
    ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)            |
87 | 86 | eqcomd 2457 |
. . . . . . 7
    ![[,] [,]](_icc.gif)           ![[,] [,]](_icc.gif)        |
88 | 87 | oveq1d 6305 |
. . . . . 6
    ![[,] [,]](_icc.gif)                    
   ![[,] [,]](_icc.gif)                   |
89 | 88 | adantl 468 |
. . . . 5
       ![[,] [,]](_icc.gif)                     
   ![[,] [,]](_icc.gif)                   |
90 | 89 | itgeq2dv 22739 |
. . . 4
 

    ![[,] [,]](_icc.gif)                        ![[,] [,]](_icc.gif)         ![[,] [,]](_icc.gif)                    |
91 | | simpl 459 |
. . . . . . . . . . . . 13
 
   |
92 | 91 | oveq2d 6306 |
. . . . . . . . . . . 12
 
       |
93 | 92 | oveq1d 6305 |
. . . . . . . . . . 11
 
           |
94 | 93 | oveq1d 6305 |
. . . . . . . . . 10
 
                   |
95 | 91 | oveq1d 6305 |
. . . . . . . . . . . . 13
 
           |
96 | 95 | oveq1d 6305 |
. . . . . . . . . . . 12
 
               |
97 | 96 | fveq2d 5869 |
. . . . . . . . . . 11
 
                       |
98 | 97 | oveq1d 6305 |
. . . . . . . . . 10
 
                                               |
99 | 94, 98 | ifeq12d 3901 |
. . . . . . . . 9
 
                                                                     
           |
100 | 99 | mpteq2dva 4489 |
. . . . . . . 8
                                                                                     |
101 | 100 | cbvmptv 4495 |
. . . . . . 7
                                                                                       |
102 | 67, 101 | eqtri 2473 |
. . . . . 6
                                            |
103 | | fveq2 5865 |
. . . . . . . 8
      ![[,] [,]](_icc.gif)           ![[,] [,]](_icc.gif)        |
104 | | oveq1 6297 |
. . . . . . . . 9
       |
105 | 104 | fveq2d 5869 |
. . . . . . . 8
                       |
106 | 103, 105 | oveq12d 6308 |
. . . . . . 7
       ![[,] [,]](_icc.gif)                   
   ![[,] [,]](_icc.gif)                   |
107 | 106 | cbvmptv 4495 |
. . . . . 6
    ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)                      ![[,] [,]](_icc.gif) 
      ![[,] [,]](_icc.gif)                   |
108 | 33 | adantr 467 |
. . . . . 6
 

      |
109 | 32 | adantr 467 |
. . . . . 6
 

  |
110 | | simpr 463 |
. . . . . 6
 

  |
111 | 64 | adantr 467 |
. . . . . 6
 

  |
112 | 37 | adantr 467 |
. . . . . 6
 

    ![[,] [,]](_icc.gif)        ![[,] [,]](_icc.gif)      |
113 | 50 | adantlr 721 |
. . . . . 6
     ..^ 
     ![[,] [,]](_icc.gif)                                      |
114 | 53 | adantlr 721 |
. . . . . 6
     ..^ 
      ![[,] [,]](_icc.gif)                  lim        |
115 | 56 | adantlr 721 |
. . . . . 6
     ..^ 
      ![[,] [,]](_icc.gif)                  lim          |
116 | 102, 31, 107, 108, 109, 110, 111, 112, 113, 114, 115 | fourierdlem101 38071 |
. . . . 5
 

    ![[,] [,]](_icc.gif)     
   ![[,] [,]](_icc.gif)                        ![[,] [,]](_icc.gif) 
     
   ![[,] [,]](_icc.gif)     
              |
117 | | oveq2 6298 |
. . . . . . . . . 10
 
     |
118 | 117 | fveq2d 5869 |
. . . . . . . . 9
          
    |
119 | | fveq2 5865 |
. . . . . . . . 9
                   |
120 | 118, 119 | oveq12d 6308 |
. . . . . . . 8
     
                             |
121 | 120 | cbvitgv 22734 |
. . . . . . 7
       
                                   
             |
122 | 121 | a1i 11 |
. . . . . 6
 

       
                                   
              |
123 | 23 | a1i 11 |
. . . . . . . . 9
    |
124 | 123, 64 | resubcld 10047 |
. . . . . . . 8
      |
125 | 124 | adantr 467 |
. . . . . . 7
 

     |
126 | 22 | a1i 11 |
. . . . . . . . 9
   |
127 | 126, 64 | resubcld 10047 |
. . . . . . . 8
     |
128 | 127 | adantr 467 |
. . . . . . 7
 

    |
129 | 36 | adantr 467 |
. . . . . . . . . 10
 
     ![[,] [,]](_icc.gif) 
         |
130 | 64 | adantr 467 |
. . . . . . . . . . 11
 
     ![[,] [,]](_icc.gif) 
     |
131 | | simpr 463 |
. . . . . . . . . . . . 13
 
     ![[,] [,]](_icc.gif) 
        ![[,] [,]](_icc.gif) 
    |
132 | 124 | adantr 467 |
. . . . . . . . . . . . . 14
 
     ![[,] [,]](_icc.gif) 
        |
133 | 127 | adantr 467 |
. . . . . . . . . . . . . 14
 
     ![[,] [,]](_icc.gif) 
   
   |
134 | | elicc2 11699 |
. . . . . . . . . . . . . 14
              ![[,] [,]](_icc.gif) 
     
      |
135 | 132, 133,
134 | syl2anc 667 |
. . . . . . . . . . . . 13
 
     ![[,] [,]](_icc.gif) 
         ![[,] [,]](_icc.gif)       
      |
136 | 131, 135 | mpbid 214 |
. . . . . . . . . . . 12
 
     ![[,] [,]](_icc.gif) 
      
     |
137 | 136 | simp1d 1020 |
. . . . . . . . . . 11
 
     ![[,] [,]](_icc.gif) 
     |
138 | 130, 137 | readdcld 9670 |
. . . . . . . . . 10
 
     ![[,] [,]](_icc.gif) 
   
   |
139 | 129, 138 | ffvelrnd 6023 |
. . . . . . . . 9
 
     ![[,] [,]](_icc.gif) 
           |
140 | 139 | adantlr 721 |
. . . . . . . 8
         ![[,] [,]](_icc.gif) 
           |
141 | 77 | ad2antlr 733 |
. . . . . . . . . 10
         ![[,] [,]](_icc.gif) 
             |
142 | 137 | adantlr 721 |
. . . . . . . . . 10
         ![[,] [,]](_icc.gif) 
     |
143 | 141, 142 | ffvelrnd 6023 |
. . . . . . . . 9
         ![[,] [,]](_icc.gif) 
             |
144 | 143 | recnd 9669 |
. . . . . . . 8
         ![[,] [,]](_icc.gif) 
             |
145 | 140, 144 | mulcld 9663 |
. . . . . . 7
         ![[,] [,]](_icc.gif) 
       
             |
146 | 125, 128,
145 | itgioo 22773 |
. . . . . 6
 

       
                          ![[,] [,]](_icc.gif)         
              |
147 | 23 | a1i 11 |
. . . . . . . . . . . 12
 
     ![[,] [,]](_icc.gif) 
      |
148 | 22 | a1i 11 |
. . . . . . . . . . . 12
 
     ![[,] [,]](_icc.gif) 
     |
149 | 64 | recnd 9669 |
. . . . . . . . . . . . . . . 16
   |
150 | 126 | recnd 9669 |
. . . . . . . . . . . . . . . . 17
   |
151 | 150 | negcld 9973 |
. . . . . . . . . . . . . . . 16
    |
152 | 149, 151 | pncan3d 9989 |
. . . . . . . . . . . . . . 15
         |
153 | 152 | eqcomd 2457 |
. . . . . . . . . . . . . 14
         |
154 | 153 | adantr 467 |
. . . . . . . . . . . . 13
 
     ![[,] [,]](_icc.gif) 
           |
155 | 136 | simp2d 1021 |
. . . . . . . . . . . . . 14
 
     ![[,] [,]](_icc.gif) 
        |
156 | 132, 137,
130, 155 | leadd2dd 10228 |
. . . . . . . . . . . . 13
 
     ![[,] [,]](_icc.gif) 
   
        |
157 | 154, 156 | eqbrtrd 4423 |
. . . . . . . . . . . 12
 
     ![[,] [,]](_icc.gif) 
        |
158 | 136 | simp3d 1022 |
. . . . . . . . . . . . . 14
 
     ![[,] [,]](_icc.gif) 
       |
159 | 137, 133,
130, 158 | leadd2dd 10228 |
. . . . . . . . . . . . 13
 
     ![[,] [,]](_icc.gif) 
   
       |
160 | 149 | adantr 467 |
. . . . . . . . . . . . . 14
 
     ![[,] [,]](_icc.gif) 
     |
161 | 150 | adantr 467 |
. . . . . . . . . . . . . 14
 
     ![[,] [,]](_icc.gif) 
     |
162 | 160, 161 | pncan3d 9989 |
. . . . . . . . . . . . 13
 
     ![[,] [,]](_icc.gif) 
   
     |
163 | 159, 162 | breqtrd 4427 |
. . . . . . . . . . . 12
 
     ![[,] [,]](_icc.gif) 
   
   |
164 | 147, 148,
138, 157, 163 | eliccd 37601 |
. . . . . . . . . . 11
 
     ![[,] [,]](_icc.gif) 
   
    ![[,] [,]](_icc.gif)    |
165 | | fvres 5879 |
. . . . . . . . . . 11
      ![[,] [,]](_icc.gif)       ![[,] [,]](_icc.gif)           
    |
166 | 164, 165 | syl 17 |
. . . . . . . . . 10
 
     ![[,] [,]](_icc.gif) 
        ![[,] [,]](_icc.gif)           
    |
167 | 166 | eqcomd 2457 |
. . . . . . . . 9
 
     ![[,] [,]](_icc.gif) 
              ![[,] [,]](_icc.gif)     
    |
168 | 167 | adantlr 721 |
. . . . . . . 8
         ![[,] [,]](_icc.gif) 
              ![[,] [,]](_icc.gif)     
    |
169 | 168 | oveq1d 6305 |
. . . . . . 7
         ![[,] [,]](_icc.gif) 
       
             
   ![[,] [,]](_icc.gif)     
             |
170 | 169 | itgeq2dv 22739 |
. . . . . 6
 

      ![[,] [,]](_icc.gif) 
                          ![[,] [,]](_icc.gif)           ![[,] [,]](_icc.gif)     
              |
171 | 122, 146,
170 | 3eqtrrd 2490 |
. . . . 5
 

      ![[,] [,]](_icc.gif) 
     
   ![[,] [,]](_icc.gif)     
                                          |
172 | 116, 171 | eqtrd 2485 |
. . . 4
 

    ![[,] [,]](_icc.gif)     
   ![[,] [,]](_icc.gif)                         
                      |
173 | 85, 90, 172 | 3eqtrd 2489 |
. . 3
 

                                       
              |
174 | | elioore 11666 |
. . . . . . . . 9
            |
175 | 174 | adantl 468 |
. . . . . . . 8
          
     |
176 | 36 | adantr 467 |
. . . . . . . . . . 11
 
      
         |
177 | 64 | adantr 467 |
. . . . . . . . . . . 12
 
      
     |
178 | 174 | adantl 468 |
. . . . . . . . . . . 12
 
      
     |
179 | 177, 178 | readdcld 9670 |
. . . . . . . . . . 11
 
      
   
   |
180 | 176, 179 | ffvelrnd 6023 |
. . . . . . . . . 10
 
      
           |
181 | 180 | adantlr 721 |
. . . . . . . . 9
          
           |
182 | 77 | ad2antlr 733 |
. . . . . . . . . . 11
          
             |
183 | 182, 175 | ffvelrnd 6023 |
. . . . . . . . . 10
          
             |
184 | 183 | recnd 9669 |
. . . . . . . . 9
          
             |
185 | 181, 184 | mulcld 9663 |
. . . . . . . 8
          
       
             |
186 | | fourierdlem111.g |
. . . . . . . . . 10
     
             |
187 | | oveq2 6298 |
. . . . . . . . . . . . 13
 
     |
188 | 187 | fveq2d 5869 |
. . . . . . . . . . . 12
          
    |
189 | | fveq2 5865 |
. . . . . . . . . . . 12
                   |
190 | 188, 189 | oveq12d 6308 |
. . . . . . . . . . 11
     
                             |
191 | 190 | cbvmptv 4495 |
. . . . . . . . . 10
                                     |
192 | 186, 191 | eqtri 2473 |
. . . . . . . . 9
     
             |
193 | 192 | fvmpt2 5957 |
. . . . . . . 8
      
                    
             |
194 | 175, 185,
193 | syl2anc 667 |
. . . . . . 7
          
                         |
195 | 194 | eqcomd 2457 |
. . . . . 6
          
       
                 |
196 | 195 | itgeq2dv 22739 |
. . . . 5
 

       
                                      |
197 | 36 | adantr 467 |
. . . . . . . . . . . . 13
 

      |
198 | 64 | adantr 467 |
. . . . . . . . . . . . . 14
 

  |
199 | | simpr 463 |
. . . . . . . . . . . . . 14
 

  |
200 | 198, 199 | readdcld 9670 |
. . . . . . . . . . . . 13
 

    |
201 | 197, 200 | ffvelrnd 6023 |
. . . . . . . . . . . 12
 

        |
202 | 201 | adantlr 721 |
. . . . . . . . . . 11
             |
203 | 77 | adantl 468 |
. . . . . . . . . . . . 13
 

          |
204 | 203 | ffvelrnda 6022 |
. . . . . . . . . . . 12
               |
205 | 204 | recnd 9669 |
. . . . . . . . . . 11
               |
206 | 202, 205 | mulcld 9663 |
. . . . . . . . . 10
         
             |
207 | 206, 186 | fmptd 6046 |
. . . . . . . . 9
 

      |
208 | 207 | adantr 467 |
. . . . . . . 8
         ![[,] [,]](_icc.gif) 
         |
209 | 124 | adantr 467 |
. . . . . . . . . 10
 
     ![[,] [,]](_icc.gif) 
        |
210 | 127 | adantr 467 |
. . . . . . . . . 10
 
     ![[,] [,]](_icc.gif) 
   
   |
211 | | simpr 463 |
. . . . . . . . . 10
 
     ![[,] [,]](_icc.gif) 
        ![[,] [,]](_icc.gif) 
    |
212 | | eliccre 37603 |
. . . . . . . . . 10
      
     ![[,] [,]](_icc.gif)       |
213 | 209, 210,
211, 212 | syl3anc 1268 |
. . . . . . . . 9
 
     ![[,] [,]](_icc.gif) 
     |
214 | 213 | adantlr 721 |
. . . . . . . 8
         ![[,] [,]](_icc.gif) 
     |
215 | 208, 214 | ffvelrnd 6023 |
. . . . . . 7
         ![[,] [,]](_icc.gif) 
         |
216 | 125, 128,
215 | itgioo 22773 |
. . . . . 6
 

       
              ![[,] [,]](_icc.gif)            |
217 | | fveq2 5865 |
. . . . . . 7
           |
218 | 217 | cbvitgv 22734 |
. . . . . 6
      ![[,] [,]](_icc.gif) 
              ![[,] [,]](_icc.gif)           |
219 | 216, 218 | syl6eq 2501 |
. . . . 5
 

       
              ![[,] [,]](_icc.gif)            |
220 | 196, 219 | eqtrd 2485 |
. . . 4
 

       
                          ![[,] [,]](_icc.gif)            |
221 | | eqid 2451 |
. . . . . . 7
               |
222 | 111 | renegcld 10046 |
. . . . . . 7
 

   |
223 | | fourierdlem111.o |
. . . . . . 7
 
                        ..^                |
224 | 31 | fourierdlem2 37971 |
. . . . . . . . . . . . . . . . . 18
 
   
                   
 ..^                 |
225 | 32, 224 | syl 17 |
. . . . . . . . . . . . . . . . 17
                         
 ..^                 |
226 | 33, 225 | mpbid 214 |
. . . . . . . . . . . . . . . 16
                    
 ..^                |
227 | 226 | simpld 461 |
. . . . . . . . . . . . . . 15
         |
228 | | elmapi 7493 |
. . . . . . . . . . . . . . 15
                 |
229 | 227, 228 | syl 17 |
. . . . . . . . . . . . . 14
           |
230 | 229 | fnvinran 37335 |
. . . . . . . . . . . . 13
 
           |
231 | 64 | adantr 467 |
. . . . . . . . . . . . 13
 
       |
232 | 230, 231 | resubcld 10047 |
. . . . . . . . . . . 12
 
             |
233 | | fourierdlem111.14 |
. . . . . . . . . . . 12
             |
234 | 232, 233 | fmptd 6046 |
. . . . . . . . . . 11
           |
235 | | reex 9630 |
. . . . . . . . . . . . 13
 |
236 | | ovex 6318 |
. . . . . . . . . . . . 13
     |
237 | 235, 236 | pm3.2i 457 |
. . . . . . . . . . . 12
       |
238 | | elmapg 7485 |
. . . . . . . . . . . 12
                         |
239 | 237, 238 | mp1i 13 |
. . . . . . . . . . 11
                   |
240 | 234, 239 | mpbird 236 |
. . . . . . . . . 10
         |
241 | 233 | a1i 11 |
. . . . . . . . . . . 12
               |
242 | | fveq2 5865 |
. . . . . . . . . . . . . 14
           |
243 | 226 | simprd 465 |
. . . . . . . . . . . . . . . 16
             
 ..^               |
244 | 243 | simpld 461 |
. . . . . . . . . . . . . . 15
              |
245 | 244 | simpld 461 |
. . . . . . . . . . . . . 14
        |
246 | 242, 245 | sylan9eqr 2507 |
. . . . . . . . . . . . 13
 
        |
247 | 246 | oveq1d 6305 |
. . . . . . . . . . . 12
 
            |
248 | | 0zd 10949 |
. . . . . . . . . . . . . 14
   |
249 | 32 | nnzd 11039 |
. . . . . . . . . . . . . 14
   |
250 | | 0red 9644 |
. . . . . . . . . . . . . . . 16
   |
251 | | nnre 10616 |
. . . . . . . . . . . . . . . 16
   |
252 | | nngt0 10638 |
. . . . . . . . . . . . . . . 16
   |
253 | 250, 251,
252 | ltled 9783 |
. . . . . . . . . . . . . . 15
   |
254 | 32, 253 | syl 17 |
. . . . . . . . . . . . . 14

  |
255 | | eluz2 11165 |
. . . . . . . . . . . . . 14
         |
256 | 248, 249,
254, 255 | syl3anbrc 1192 |
. . . . . . . . . . . . 13
       |
257 | | eluzfz1 11806 |
. . . . . . . . . . . . 13
    
      |
258 | 256, 257 | syl 17 |
. . . . . . . . . . . 12
       |
259 | 241, 247,
258, 124 | fvmptd 5954 |
. . . . . . . . . . 11
          |
260 | | fveq2 5865 |
. . . . . . . . . . . . . 14
           |
261 | 244 | simprd 465 |
. . . . . . . . . . . . . 14
       |
262 | 260, 261 | sylan9eqr 2507 |
. . . . . . . . . . . . 13
 
       |
263 | 262 | oveq1d 6305 |
. . . . . . . . . . . 12
 
           |
264 | | eluzfz2 11807 |
. . . . . . . . . . . . 13
    
      |
265 | 256, 264 | syl 17 |
. . . . . . . . . . . 12
       |
266 | 241, 263,
265, 127 | fvmptd 5954 |
. . . . . . . . . . 11
         |
267 | 259, 266 | jca 535 |
. . . . . . . . . 10
        
         |
268 | 229 | adantr 467 |
. . . . . . . . . . . . . 14
 
 ..^            |
269 | | elfzofz 11935 |
. . . . . . . . . . . . . . 15
  ..^
      |
270 | 269 | adantl 468 |
. . . . . . . . . . . . . 14
 
 ..^        |
271 | 268, 270 | ffvelrnd 6023 |
. . . . . . . . . . . . 13
 
 ..^        |
272 | | fzofzp1 12008 |
. . . . . . . . . . . . . . 15
  ..^
        |
273 | 272 | adantl 468 |
. . . . . . . . . . . . . 14
 
 ..^          |
274 | 268, 273 | ffvelrnd 6023 |
. . . . . . . . . . . . 13
 
 ..^          |
275 | 64 | adantr 467 |
. . . . . . . . . . . . 13
 
 ..^    |
276 | 243 | simprd 465 |
. . . . . . . . . . . . . 14
   ..^              |
277 | 276 | r19.21bi 2757 |
. . . . . . . . . . . . 13
 
 ..^              |
278 | 271, 274,
275, 277 | ltsub1dd 10225 |
. . . . . . . . . . . 12
 
 ..^                  |
279 | 270, 232 | syldan 473 |
. . . . . . . . . . . . 13
 
 ..^          |
280 | 233 | fvmpt2 5957 |
. . . . . . . . . . . . 13
                         |
281 | 270, 279,
280 | syl2anc 667 |
. . . . . . . . . . . 12
 
 ..^              |
282 | | fveq2 5865 |
. . . . . . . . . . . . . . . . 17
           |
283 | 282 | oveq1d 6305 |
. . . . . . . . . . . . . . . 16
               |
284 | 283 | cbvmptv 4495 |
. . . . . . . . . . . . . . 15
                         |
285 | 233, 284 | eqtri 2473 |
. . . . . . . . . . . . . 14
             |
286 | 285 | a1i 11 |
. . . . . . . . . . . . 13
 
 ..^                |
287 | | fveq2 5865 |
. . . . . . . . . . . . . . 15
               |
288 | 287 | oveq1d 6305 |
. . . . . . . . . . . . . 14
                   |
289 | 288 | adantl 468 |
. . . . . . . . . . . . 13
    ..^                     |
290 | 274, 275 | resubcld 10047 |
. . . . . . . . . . . . 13
 
 ..^            |
291 | 286, 289,
273, 290 | fvmptd 5954 |
. . . . . . . . . . . 12
 
 ..^                  |
292 | 278, 281,
291 | 3brtr4d 4433 |
. . . . . . . . . . 11
 
 ..^              |
293 | 292 | ralrimiva 2802 |
. . . . . . . . . 10
   ..^              |
294 | 240, 267,
293 | jca32 538 |
. . . . . . . . 9
                          ..^                |
295 | 223 | fourierdlem2 37971 |
. . . . . . . . . 10
 
   
                         ..^                 |
296 | 32, 295 | syl 17 |
. . . . . . . . 9
                               ..^                 |
297 | 294, 296 | mpbird 236 |
. . . . . . . 8
       |
298 | 297 | adantr 467 |
. . . . . . 7
 

      |
299 | 150, 151,
149 | nnncan2d 10021 |
. . . . . . . . . . . 12
             |
300 | | picn 23414 |
. . . . . . . . . . . . . 14
 |
301 | 300 | 2timesi 10730 |
. . . . . . . . . . . . 13
     |
302 | | fourierdlem111.t |
. . . . . . . . . . . . 13
   |
303 | 300, 300 | subnegi 9953 |
. . . . . . . . . . . . 13
      |
304 | 301, 302,
303 | 3eqtr4i 2483 |
. . . . . . . . . . . 12
    |
305 | 299, 304 | syl6eqr 2503 |
. . . . . . . . . . 11
          |
306 | 305 | oveq2d 6306 |
. . . . . . . . . 10
              |
307 | 306 | fveq2d 5869 |
. . . . . . . . 9
                      |
308 | 307 | ad2antrr 732 |
. . . . . . . 8
                     
    |
309 | | simpr 463 |
. . . . . . . . . 10
       |
310 | 186 | fvmpt2 5957 |
. . . . . . . . . 10
      
                    
             |
311 | 309, 206,
310 | syl2anc 667 |
. . . . . . . . 9
                           |
312 | 149 | adantr 467 |
. . . . . . . . . . . . . . 15
 

  |
313 | 199 | recnd 9669 |
. . . . . . . . . . . . . . 15
 

  |
314 | | 2re 10679 |
. . . . . . . . . . . . . . . . . . . 20
 |
315 | 314, 22 | remulcli 9657 |
. . . . . . . . . . . . . . . . . . 19
   |
316 | 302, 315 | eqeltri 2525 |
. . . . . . . . . . . . . . . . . 18
 |
317 | 316 | a1i 11 |
. . . . . . . . . . . . . . . . 17
   |
318 | 317 | recnd 9669 |
. . . . . . . . . . . . . . . 16
   |
319 | 318 | adantr 467 |
. . . . . . . . . . . . . . 15
 

  |
320 | 312, 313,
319 | addassd 9665 |
. . . . . . . . . . . . . 14
 

          |
321 | 320 | eqcomd 2457 |
. . . . . . . . . . . . 13
 

          |
322 | 321 | fveq2d 5869 |
. . . . . . . . . . . 12
 

    
             |
323 | | simpl 459 |
. . . . . . . . . . . . . 14
 

  |
324 | 323, 200 | jca 535 |
. . . . . . . . . . . . 13
 

      |
325 | | eleq1 2517 |
. . . . . . . . . . . . . . . 16
   
     |
326 | 325 | anbi2d 710 |
. . . . . . . . . . . . . . 15
    

       |
327 | | oveq1 6297 |
. . . . . . . . . . . . . . . . 17
           |
328 | 327 | fveq2d 5869 |
. . . . . . . . . . . . . . . 16
                   |
329 | | fveq2 5865 |
. . . . . . . . . . . . . . . 16
          
    |
330 | 328, 329 | eqeq12d 2466 |
. . . . . . . . . . . . . . 15
             
                 |
331 | 326, 330 | imbi12d 322 |
. . . . . . . . . . . . . 14
     
              
                    |
332 | | eleq1 2517 |
. . . . . . . . . . . . . . . . 17
 
   |
333 | 332 | anbi2d 710 |
. . . . . . . . . . . . . . . 16
  

     |
334 | | oveq1 6297 |
. . . . . . . . . . . . . . . . . 18
       |
335 | 334 | fveq2d 5869 |
. . . . . . . . . . . . . . . . 17
               |
336 | | fveq2 5865 |
. . . . . . . . . . . . . . . . 17
           |
337 | 335, 336 | eqeq12d 2466 |
. . . . . . . . . . . . . . . 16
           
             |
338 | 333, 337 | imbi12d 322 |
. . . . . . . . . . . . . . 15
   
             
               |
339 | | fourierdlem111.fper |
. . . . . . . . . . . . . . 15
 

            |
340 | 338, 339 | chvarv 2107 |
. . . . . . . . . . . . . 14
 

            |
341 | 331, 340 | vtoclg 3107 |
. . . . . . . . . . . . 13
    

      
      
     |
342 | 200, 324,
341 | sylc 62 |
. . . . . . . . . . . 12
 

           
    |
343 | 322, 342 | eqtr2d 2486 |
. . . . . . . . . . 11
 

         
      |
344 | 343 | adantlr 721 |
. . . . . . . . . 10
              
      |
345 | 67, 302 | dirkerper 37958 |
. . . . . . . . . . . 12
 
                     |
346 | 345 | eqcomd 2457 |
. . . . . . . . . . 11
 
                     |
347 | 346 | adantll 720 |
. . . . . . . . . 10
                    
    |
348 | 344, 347 | oveq12d 6308 |
. . . . . . . . 9
         
                
                |
349 | 192 | a1i 11 |
. . . . . . . . . . 11
                         |
350 | | oveq2 6298 |
. . . . . . . . . . . . . 14
   
  
    |
351 | 350 | fveq2d 5869 |
. . . . . . . . . . . . 13
            
      |
352 | | fveq2 5865 |
. . . . . . . . . . . . 13
                  
    |
353 | 351, 352 | oveq12d 6308 |
. . . . . . . . . . . 12
       
                
                |
354 | 353 | adantl 468 |
. . . . . . . . . . 11
   

   
                    
                 |
355 | 316 | a1i 11 |
. . . . . . . . . . . 12
       |
356 | 309, 355 | readdcld 9670 |
. . . . . . . . . . 11
         |
357 | 316 | a1i 11 |
. . . . . . . . . . . . . . . 16
 

  |
358 | 199, 357 | readdcld 9670 |
. . . . . . . . . . . . . . 15
 

    |
359 | 198, 358 | readdcld 9670 |
. . . . . . . . . . . . . 14
 

      |
360 | 197, 359 | ffvelrnd 6023 |
. . . . . . . . . . . . 13
 

    
     |
361 | 360 | adantlr 721 |
. . . . . . . . . . . 12
               |
362 | 77 | ad2antlr 733 |
. . . . . . . . . . . . . 14
               |
363 | 362, 356 | ffvelrnd 6023 |
. . . . . . . . . . . . 13
                 |
364 | 363 | recnd 9669 |
. . . . . . . . . . . 12
                 |
365 | 361, 364 | mulcld 9663 |
. . . . . . . . . . 11
         
           
     |
366 | 349, 354,
356, 365 | fvmptd 5954 |
. . . . . . . . . 10
               
                 |
367 | 366 | eqcomd 2457 |
. . . . . . . . 9
         
           
           |
368 | 311, 348,
367 | 3eqtrrd 2490 |
. . . . . . . 8
                 |
369 | 308, 368 | eqtrd 2485 |
. . . . . . 7
                        |
370 | 192 | reseq1i 5101 |
. . . . . . . . . 10
                      
                            |
371 | 370 | a1i 11 |
. . . . . . . . 9
     ..^ 
                      
                             |
372 | | ioossre 11696 |
. . . . . . . . . 10
               |
373 | | resmpt 5154 |
. . . . . . . . . 10
              
      
           
                                  
              |
374 | 372, 373 | ax-mp 5 |
. . . . . . . . 9
      
           
                                  
             |
375 | 371, 374 | syl6eq 2501 |
. . . . . . . 8
     ..^ 
                                   
              |
376 | 271 | rexrd 9690 |
. . . . . . . . . . . . . 14
 
 ..^        |
377 | 376 | adantr 467 |
. . . . . . . . . . . . 13
    ..^                       |
378 | 274 | rexrd 9690 |
. . . . . . . . . . . . . 14
 
 ..^          |
379 | 378 | adantr 467 |
. . . . . . . . . . . . 13
    ..^                         |
380 | 64 | adantr 467 |
. . . . . . . . . . . . . . 15
 
                 |
381 | | elioore 11666 |
. . . . . . . . . . . . . . . 16
                 |
382 | 381 | adantl 468 |
. . . . . . . . . . . . . . 15
 
                 |
383 | 380, 382 | readdcld 9670 |
. . . . . . . . . . . . . 14
 
               
   |
384 | 383 | adantlr 721 |
. . . . . . . . . . . . 13
    ..^                 
   |
385 | | eleq1 2517 |
. . . . . . . . . . . . . . . 16
               
                 |
386 | 385 | anbi2d 710 |
. . . . . . . . . . . . . . 15
   
 ..^ 
              
   ..^                    |
387 | 187 | breq2d 4414 |
. . . . . . . . . . . . . . 15
     
 
    
    |
388 | 386, 387 | imbi12d 322 |
. . . . . . . . . . . . . 14
      ..^ 
                  
  
  
 ..^                           |
389 | 149 | adantr 467 |
. . . . . . . . . . . . . . . . . 18
 
 ..^    |
390 | 281, 279 | eqeltrd 2529 |
. . . . . . . . . . . . . . . . . . 19
 
 ..^        |
391 | 390 | recnd 9669 |
. . . . . . . . . . . . . . . . . 18
 
 ..^        |
392 | 389, 391 | addcomd 9835 |
. . . . . . . . . . . . . . . . 17
 
 ..^                |
393 | 281 | oveq1d 6305 |
. . . . . . . . . . . . . . . . 17
 
 ..^                  |
394 | 271 | recnd 9669 |
. . . . . . . . . . . . . . . . . 18
 
 ..^        |
395 | 394, 389 | npcand 9990 |
. . . . . . . . . . . . . . . . 17
 
 ..^                |
396 | 392, 393,
395 | 3eqtrrd 2490 |
. . . . . . . . . . . . . . . 16
 
 ..^              |
397 | 396 | adantr 467 |
. . . . . . . . . . . . . . 15
    ..^                             |
398 | 390 | adantr 467 |
. . . . . . . . . . . . . . . 16
    ..^                       |
399 | | elioore 11666 |
. . . . . . . . . . . . . . . . 17
                 |
400 | 399 | adantl 468 |
. . . . . . . . . . . . . . . 16
    ..^                   |
401 | 64 | ad2antrr 732 |
. . . . . . . . . . . . . . . 16
    ..^                   |
402 | 390 | rexrd 9690 |
. . . . . . . . . . . . . . . . . 18
 
 ..^        |
403 | 402 | adantr 467 |
. . . . . . . . . . . . . . . . 17
    ..^                       |
404 | 291, 290 | eqeltrd 2529 |
. . . . . . . . . . . . . . . . . . 19
 
 ..^          |
405 | 404 | rexrd 9690 |
. . . . . . . . . . . . . . . . . 18
 
 ..^          |
406 | 405 | adantr 467 |
. . . . . . . . . . . . . . . . 17
    ..^                         |
407 | | simpr 463 |
. . . . . . . . . . . . . . . . 17
    ..^                                 |
408 | | ioogtlb 37592 |
. . . . . . . . . . . . . . . . 17
           
                     |
409 | 403, 406,
407, 408 | syl3anc 1268 |
. . . . . . . . . . . . . . . 16
    ..^                       |
410 | 398, 400,
401, 409 | ltadd2dd 9794 |
. . . . . . . . . . . . . . 15
    ..^                 
         |
411 | 397, 410 | eqbrtrd 4423 |
. . . . . . . . . . . . . 14
    ..^                         |
412 | 388, 411 | chvarv 2107 |
. . . . . . . . . . . . 13
    ..^                         |
413 | 187 | breq1d 4412 |
. . . . . . . . . . . . . . 15
   
     
           |
414 | 386, 413 | imbi12d 322 |
. . . . . . . . . . . . . 14
      ..^ 
                
      
  
 ..^                 
           |
415 | 404 | adantr 467 |
. . . . . . . . . . . . . . . 16
    ..^                         |
416 | | iooltub 37610 |
. . . . . . . . . . . . . . . . 17
           
                       |
417 | 403, 406,
407, 416 | syl3anc 1268 |
. . . . . . . . . . . . . . . 16
    ..^                         |
418 | 400, 415,
401, 417 | ltadd2dd 9794 |
. . . . . . . . . . . . . . 15
    ..^                 
        |