Step | Hyp | Ref
| Expression |
1 | | simpr 463 |
. . . . . 6
 
    
      |
2 | | fourierdlem41.q |
. . . . . . . . . . 11
       |
3 | | fourierdlem41.m |
. . . . . . . . . . . 12
   |
4 | | fourierdlem41.p |
. . . . . . . . . . . . 13
 
                 
 ..^                |
5 | 4 | fourierdlem2 37965 |
. . . . . . . . . . . 12
 
   
                  
 ..^                 |
6 | 3, 5 | syl 17 |
. . . . . . . . . . 11
                        
 ..^                 |
7 | 2, 6 | mpbid 214 |
. . . . . . . . . 10
                   
 ..^                |
8 | 7 | simpld 461 |
. . . . . . . . 9
         |
9 | | elmapi 7490 |
. . . . . . . . 9
                 |
10 | | ffn 5726 |
. . . . . . . . 9
               |
11 | 8, 9, 10 | 3syl 18 |
. . . . . . . 8
       |
12 | 11 | adantr 467 |
. . . . . . 7
 
    
      |
13 | | fvelrnb 5910 |
. . . . . . 7
                           |
14 | 12, 13 | syl 17 |
. . . . . 6
 
    
    
                 |
15 | 1, 14 | mpbid 214 |
. . . . 5
 
    
                |
16 | | 0zd 10946 |
. . . . . . . . . . 11
 
   
        
  |
17 | | elfzelz 11797 |
. . . . . . . . . . . . 13
       |
18 | 17 | 3ad2ant2 1029 |
. . . . . . . . . . . 12
 
   
        
  |
19 | | 1zzd 10965 |
. . . . . . . . . . . 12
 
   
        
  |
20 | 18, 19 | zsubcld 11042 |
. . . . . . . . . . 11
 
   
        
    |
21 | | simpll 759 |
. . . . . . . . . . . . . . 15
           |
22 | | elfzle1 11799 |
. . . . . . . . . . . . . . . . . . 19
       |
23 | 22 | anim1i 571 |
. . . . . . . . . . . . . . . . . 18
     
 
   |
24 | | 0red 9641 |
. . . . . . . . . . . . . . . . . . 19
     
   |
25 | 17 | zred 11037 |
. . . . . . . . . . . . . . . . . . . 20
       |
26 | 25 | adantr 467 |
. . . . . . . . . . . . . . . . . . 19
     
   |
27 | 24, 26 | eqleltd 9776 |
. . . . . . . . . . . . . . . . . 18
     
  
    |
28 | 23, 27 | mpbird 236 |
. . . . . . . . . . . . . . . . 17
     
   |
29 | 28 | eqcomd 2456 |
. . . . . . . . . . . . . . . 16
     
   |
30 | 29 | adantll 719 |
. . . . . . . . . . . . . . 15
           |
31 | | fveq2 5863 |
. . . . . . . . . . . . . . . 16
           |
32 | 7 | simprld 764 |
. . . . . . . . . . . . . . . . 17
             |
33 | 32 | simpld 461 |
. . . . . . . . . . . . . . . 16
       |
34 | 31, 33 | sylan9eqr 2506 |
. . . . . . . . . . . . . . 15
 
       |
35 | 21, 30, 34 | syl2anc 666 |
. . . . . . . . . . . . . 14
               |
36 | 35 | 3adantl3 1165 |
. . . . . . . . . . . . 13
      
                |
37 | | simpr 463 |
. . . . . . . . . . . . . . . . 17
 
        
          |
38 | | fourierdlem41.a |
. . . . . . . . . . . . . . . . . . 19
   |
39 | 38 | rexrd 9687 |
. . . . . . . . . . . . . . . . . . . 20
   |
40 | | fourierdlem41.b |
. . . . . . . . . . . . . . . . . . . . 21
   |
41 | 40 | rexrd 9687 |
. . . . . . . . . . . . . . . . . . . 20
   |
42 | | fourierdlem41.altb |
. . . . . . . . . . . . . . . . . . . . . . 23
   |
43 | | fourierdlem41.t |
. . . . . . . . . . . . . . . . . . . . . . 23
   |
44 | | eqid 2450 |
. . . . . . . . . . . . . . . . . . . . . . 23
                             |
45 | 38, 40, 42, 43, 44 | fourierdlem4 37967 |
. . . . . . . . . . . . . . . . . . . . . 22
  
                  ![(,] (,]](_ioc.gif)    |
46 | | fourierdlem41.e |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
       |
47 | 46 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
           |
48 | | simpr 463 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 

  |
49 | 40 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
 

  |
50 | 49, 48 | resubcld 10044 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
 

    |
51 | 40, 38 | resubcld 10044 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
     |
52 | 43, 51 | syl5eqel 2532 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
   |
53 | 52 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
 

  |
54 | | 0red 9641 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
   |
55 | 38, 40 | posdifd 10197 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
       |
56 | 42, 55 | mpbid 214 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
     |
57 | 43 | eqcomi 2459 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
   |
58 | 57 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
     |
59 | 56, 58 | breqtrd 4426 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
   |
60 | 54, 59 | gtned 9767 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
   |
61 | 60 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
 

  |
62 | 50, 53, 61 | redivcld 10432 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
 

      |
63 | 62 | flcld 12031 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
 

          |
64 | 63 | zred 11037 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 

          |
65 | 64, 53 | remulcld 9668 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 

            |
66 | | fourierdlem41.z |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
             |
67 | 66 | fvmpt2 5955 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
                             |
68 | 48, 65, 67 | syl2anc 666 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 

                |
69 | 68 | oveq2d 6304 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 

                    |
70 | 69 | mpteq2dva 4488 |
. . . . . . . . . . . . . . . . . . . . . . . 24
  
                      |
71 | 47, 70 | eqtrd 2484 |
. . . . . . . . . . . . . . . . . . . . . . 23
                 |
72 | 71 | feq1d 5712 |
. . . . . . . . . . . . . . . . . . . . . 22
        ![(,] (,]](_ioc.gif)   
                  ![(,] (,]](_ioc.gif)     |
73 | 45, 72 | mpbird 236 |
. . . . . . . . . . . . . . . . . . . . 21
       ![(,] (,]](_ioc.gif)    |
74 | | fourierdlem41.x |
. . . . . . . . . . . . . . . . . . . . 21
   |
75 | 73, 74 | ffvelrnd 6021 |
. . . . . . . . . . . . . . . . . . . 20
       ![(,] (,]](_ioc.gif)    |
76 | | iocgtlb 37593 |
. . . . . . . . . . . . . . . . . . . 20
        ![(,] (,]](_ioc.gif)         |
77 | 39, 41, 75, 76 | syl3anc 1267 |
. . . . . . . . . . . . . . . . . . 19
       |
78 | 38, 77 | gtned 9767 |
. . . . . . . . . . . . . . . . . 18
       |
79 | 78 | adantr 467 |
. . . . . . . . . . . . . . . . 17
 
        
      |
80 | 37, 79 | eqnetrd 2690 |
. . . . . . . . . . . . . . . 16
 
        
      |
81 | 80 | adantr 467 |
. . . . . . . . . . . . . . 15
           
       |
82 | 81 | 3adantl2 1164 |
. . . . . . . . . . . . . 14
      
                |
83 | 82 | neneqd 2628 |
. . . . . . . . . . . . 13
      
                |
84 | 36, 83 | condan 802 |
. . . . . . . . . . . 12
 
   
        
  |
85 | | zltlem1 10986 |
. . . . . . . . . . . . 13
 
       |
86 | 16, 18, 85 | syl2anc 666 |
. . . . . . . . . . . 12
 
   
        

     |
87 | 84, 86 | mpbid 214 |
. . . . . . . . . . 11
 
   
        
    |
88 | | eluz2 11162 |
. . . . . . . . . . 11
               |
89 | 16, 20, 87, 88 | syl3anbrc 1191 |
. . . . . . . . . 10
 
   
        
        |
90 | | elfzel2 11795 |
. . . . . . . . . . 11
       |
91 | 90 | 3ad2ant2 1029 |
. . . . . . . . . 10
 
   
        
  |
92 | | 1red 9655 |
. . . . . . . . . . . . 13
       |
93 | 25, 92 | resubcld 10044 |
. . . . . . . . . . . 12
         |
94 | 90 | zred 11037 |
. . . . . . . . . . . 12
       |
95 | 25 | ltm1d 10536 |
. . . . . . . . . . . 12
         |
96 | | elfzle2 11800 |
. . . . . . . . . . . 12
       |
97 | 93, 25, 94, 95, 96 | ltletrd 9792 |
. . . . . . . . . . 11
         |
98 | 97 | 3ad2ant2 1029 |
. . . . . . . . . 10
 
   
        
    |
99 | | elfzo2 11920 |
. . . . . . . . . 10
    ..^       
     |
100 | 89, 91, 98, 99 | syl3anbrc 1191 |
. . . . . . . . 9
 
   
        
   ..^   |
101 | 8, 9 | syl 17 |
. . . . . . . . . . . . 13
           |
102 | 101 | 3ad2ant1 1028 |
. . . . . . . . . . . 12
 
   
        
          |
103 | 16, 91, 20 | 3jca 1187 |
. . . . . . . . . . . . . 14
 
   
        
      |
104 | 93, 94, 97 | ltled 9780 |
. . . . . . . . . . . . . . 15
         |
105 | 104 | 3ad2ant2 1029 |
. . . . . . . . . . . . . 14
 
   
        
    |
106 | 103, 87, 105 | jca32 538 |
. . . . . . . . . . . . 13
 
   
        
 
            |
107 | | elfz2 11788 |
. . . . . . . . . . . . 13
      
 
            |
108 | 106, 107 | sylibr 216 |
. . . . . . . . . . . 12
 
   
        
        |
109 | 102, 108 | ffvelrnd 6021 |
. . . . . . . . . . 11
 
   
        
        |
110 | 109 | rexrd 9687 |
. . . . . . . . . 10
 
   
        
        |
111 | 25 | recnd 9666 |
. . . . . . . . . . . . . . 15
       |
112 | | 1cnd 9656 |
. . . . . . . . . . . . . . 15
       |
113 | 111, 112 | npcand 9987 |
. . . . . . . . . . . . . 14
           |
114 | 113 | fveq2d 5867 |
. . . . . . . . . . . . 13
                   |
115 | 114 | adantl 468 |
. . . . . . . . . . . 12
 
                   |
116 | 101 | ffvelrnda 6020 |
. . . . . . . . . . . . 13
 
           |
117 | 116 | rexrd 9687 |
. . . . . . . . . . . 12
 
           |
118 | 115, 117 | eqeltrd 2528 |
. . . . . . . . . . 11
 
               |
119 | 118 | 3adant3 1027 |
. . . . . . . . . 10
 
   
        
          |
120 | | id 22 |
. . . . . . . . . . . . . . . 16
   |
121 | | fveq2 5863 |
. . . . . . . . . . . . . . . 16
           |
122 | 120, 121 | oveq12d 6306 |
. . . . . . . . . . . . . . 15
               |
123 | 122 | adantl 468 |
. . . . . . . . . . . . . 14
 
               |
124 | 66 | a1i 11 |
. . . . . . . . . . . . . . . . 17
               |
125 | | oveq2 6296 |
. . . . . . . . . . . . . . . . . . . . 21
 
     |
126 | 125 | oveq1d 6303 |
. . . . . . . . . . . . . . . . . . . 20
           |
127 | 126 | fveq2d 5867 |
. . . . . . . . . . . . . . . . . . 19
                   |
128 | 127 | oveq1d 6303 |
. . . . . . . . . . . . . . . . . 18
                       |
129 | 128 | adantl 468 |
. . . . . . . . . . . . . . . . 17
 
                       |
130 | 40, 74 | resubcld 10044 |
. . . . . . . . . . . . . . . . . . . . 21
     |
131 | 130, 52, 60 | redivcld 10432 |
. . . . . . . . . . . . . . . . . . . 20
       |
132 | 131 | flcld 12031 |
. . . . . . . . . . . . . . . . . . 19
           |
133 | 132 | zred 11037 |
. . . . . . . . . . . . . . . . . 18
           |
134 | 133, 52 | remulcld 9668 |
. . . . . . . . . . . . . . . . 17
             |
135 | 124, 129,
74, 134 | fvmptd 5952 |
. . . . . . . . . . . . . . . 16
                 |
136 | 135, 134 | eqeltrd 2528 |
. . . . . . . . . . . . . . 15
       |
137 | 74, 136 | readdcld 9667 |
. . . . . . . . . . . . . 14
         |
138 | 47, 123, 74, 137 | fvmptd 5952 |
. . . . . . . . . . . . 13
             |
139 | 138, 137 | eqeltrd 2528 |
. . . . . . . . . . . 12
       |
140 | 139 | rexrd 9687 |
. . . . . . . . . . 11
       |
141 | 140 | 3ad2ant1 1028 |
. . . . . . . . . 10
 
   
        
      |
142 | | simp1 1007 |
. . . . . . . . . . . . 13
 
   
        
  |
143 | | ovex 6316 |
. . . . . . . . . . . . . 14
   |
144 | | eleq1 2516 |
. . . . . . . . . . . . . . . 16
     ..^
   ..^    |
145 | 144 | anbi2d 709 |
. . . . . . . . . . . . . . 15
    
 ..^      ..^     |
146 | | fveq2 5863 |
. . . . . . . . . . . . . . . 16
               |
147 | | oveq1 6295 |
. . . . . . . . . . . . . . . . 17
           |
148 | 147 | fveq2d 5867 |
. . . . . . . . . . . . . . . 16
                   |
149 | 146, 148 | breq12d 4414 |
. . . . . . . . . . . . . . 15
       
     
                 |
150 | 145, 149 | imbi12d 322 |
. . . . . . . . . . . . . 14
     
 ..^     
      
     ..^                    |
151 | 7 | simprrd 766 |
. . . . . . . . . . . . . . 15
   ..^              |
152 | 151 | r19.21bi 2756 |
. . . . . . . . . . . . . 14
 
 ..^              |
153 | 143, 150,
152 | vtocl 3099 |
. . . . . . . . . . . . 13
 
   ..^ 
                |
154 | 142, 100,
153 | syl2anc 666 |
. . . . . . . . . . . 12
 
   
        
                |
155 | 114 | 3ad2ant2 1029 |
. . . . . . . . . . . 12
 
   
        
              |
156 | 154, 155 | breqtrd 4426 |
. . . . . . . . . . 11
 
   
        
            |
157 | | simp3 1009 |
. . . . . . . . . . 11
 
   
        
          |
158 | 156, 157 | breqtrd 4426 |
. . . . . . . . . 10
 
   
        
            |
159 | 139 | leidd 10177 |
. . . . . . . . . . . . . 14
    
      |
160 | 159 | adantr 467 |
. . . . . . . . . . . . 13
 
        
          |
161 | 37 | eqcomd 2456 |
. . . . . . . . . . . . 13
 
        
          |
162 | 160, 161 | breqtrd 4426 |
. . . . . . . . . . . 12
 
        
          |
163 | 162 | 3adant2 1026 |
. . . . . . . . . . 11
 
   
        
          |
164 | 113 | eqcomd 2456 |
. . . . . . . . . . . . 13
           |
165 | 164 | fveq2d 5867 |
. . . . . . . . . . . 12
                   |
166 | 165 | 3ad2ant2 1029 |
. . . . . . . . . . 11
 
   
        
              |
167 | 163, 166 | breqtrd 4426 |
. . . . . . . . . 10
 
   
        
              |
168 | 110, 119,
141, 158, 167 | eliocd 37599 |
. . . . . . . . 9
 
   
        
            ![(,] (,]](_ioc.gif)            |
169 | 146, 148 | oveq12d 6306 |
. . . . . . . . . . 11
         ![(,] (,]](_ioc.gif)                ![(,] (,]](_ioc.gif)            |
170 | 169 | eleq2d 2513 |
. . . . . . . . . 10
              ![(,] (,]](_ioc.gif)       
            ![(,] (,]](_ioc.gif)             |
171 | 170 | rspcev 3149 |
. . . . . . . . 9
     ..^             ![(,] (,]](_ioc.gif)             ..^            ![(,] (,]](_ioc.gif)          |
172 | 100, 168,
171 | syl2anc 666 |
. . . . . . . 8
 
   
        
  ..^            ![(,] (,]](_ioc.gif)          |
173 | 172 | 3exp 1206 |
. . . . . . 7
              
  ..^            ![(,] (,]](_ioc.gif)            |
174 | 173 | adantr 467 |
. . . . . 6
 
    
    
           ..^            ![(,] (,]](_ioc.gif)            |
175 | 174 | rexlimdv 2876 |
. . . . 5
 
    
 
               ..^            ![(,] (,]](_ioc.gif)           |
176 | 15, 175 | mpd 15 |
. . . 4
 
    
  ..^            ![(,] (,]](_ioc.gif)          |
177 | 3 | adantr 467 |
. . . . . 6
 
    
  |
178 | 101 | adantr 467 |
. . . . . 6
 
               |
179 | | iocssicc 11719 |
. . . . . . . 8
      ![(,] (,]](_ioc.gif)            ![[,] [,]](_icc.gif)       |
180 | 32 | simprd 465 |
. . . . . . . . . 10
       |
181 | 33, 180 | oveq12d 6306 |
. . . . . . . . 9
       ![(,] (,]](_ioc.gif)        ![(,] (,]](_ioc.gif)    |
182 | 75, 181 | eleqtrrd 2531 |
. . . . . . . 8
           ![(,] (,]](_ioc.gif)        |
183 | 179, 182 | sseldi 3429 |
. . . . . . 7
           ![[,] [,]](_icc.gif)        |
184 | 183 | adantr 467 |
. . . . . 6
 
               ![[,] [,]](_icc.gif)        |
185 | | simpr 463 |
. . . . . 6
 
           |
186 | | fveq2 5863 |
. . . . . . . . 9
           |
187 | 186 | breq1d 4411 |
. . . . . . . 8
     
   
           |
188 | 187 | cbvrabv 3043 |
. . . . . . 7
  ..^            ..^           |
189 | 188 | supeq1i 7958 |
. . . . . 6
    ..^    
      
    ..^             |
190 | 177, 178,
184, 185, 189 | fourierdlem25 37988 |
. . . . 5
 
     
 ..^                      |
191 | | ioossioc 37582 |
. . . . . . . 8
                    ![(,] (,]](_ioc.gif)         |
192 | 191 | a1i 11 |
. . . . . . 7
         ..^                      ![(,] (,]](_ioc.gif)          |
193 | 192 | sseld 3430 |
. . . . . 6
         ..^                    
          ![(,] (,]](_ioc.gif)           |
194 | 193 | reximdva 2861 |
. . . . 5
 
        ..^                    
 ..^            ![(,] (,]](_ioc.gif)           |
195 | 190, 194 | mpd 15 |
. . . 4
 
     
 ..^            ![(,] (,]](_ioc.gif)          |
196 | 176, 195 | pm2.61dan 799 |
. . 3
   ..^            ![(,] (,]](_ioc.gif)          |
197 | 101 | adantr 467 |
. . . . . . . . 9
 
 ..^            |
198 | | elfzofz 11932 |
. . . . . . . . . 10
  ..^
      |
199 | 198 | adantl 468 |
. . . . . . . . 9
 
 ..^        |
200 | 197, 199 | ffvelrnd 6021 |
. . . . . . . 8
 
 ..^        |
201 | 200 | 3adant3 1027 |
. . . . . . 7
 
 ..^           ![(,] (,]](_ioc.gif)               |
202 | 136 | 3ad2ant1 1028 |
. . . . . . 7
 
 ..^           ![(,] (,]](_ioc.gif)               |
203 | 201, 202 | resubcld 10044 |
. . . . . 6
 
 ..^           ![(,] (,]](_ioc.gif)                     |
204 | 139 | 3ad2ant1 1028 |
. . . . . . . 8
 
 ..^           ![(,] (,]](_ioc.gif)               |
205 | 201 | rexrd 9687 |
. . . . . . . . 9
 
 ..^           ![(,] (,]](_ioc.gif)               |
206 | | fzofzp1 12005 |
. . . . . . . . . . . . 13
  ..^
        |
207 | 206 | adantl 468 |
. . . . . . . . . . . 12
 
 ..^          |
208 | 197, 207 | ffvelrnd 6021 |
. . . . . . . . . . 11
 
 ..^          |
209 | 208 | rexrd 9687 |
. . . . . . . . . 10
 
 ..^          |
210 | 209 | 3adant3 1027 |
. . . . . . . . 9
 
 ..^           ![(,] (,]](_ioc.gif)                 |
211 | | simp3 1009 |
. . . . . . . . 9
 
 ..^           ![(,] (,]](_ioc.gif)                   ![(,] (,]](_ioc.gif)          |
212 | | iocgtlb 37593 |
. . . . . . . . 9
           
          ![(,] (,]](_ioc.gif)                   |
213 | 205, 210,
211, 212 | syl3anc 1267 |
. . . . . . . 8
 
 ..^           ![(,] (,]](_ioc.gif)            
      |
214 | 201, 204,
202, 213 | ltsub1dd 10222 |
. . . . . . 7
 
 ..^           ![(,] (,]](_ioc.gif)                  
            |
215 | 138 | oveq1d 6303 |
. . . . . . . . 9
                         |
216 | 74 | recnd 9666 |
. . . . . . . . . 10
   |
217 | 136 | recnd 9666 |
. . . . . . . . . 10
       |
218 | 216, 217 | pncand 9984 |
. . . . . . . . 9
               |
219 | 215, 218 | eqtrd 2484 |
. . . . . . . 8
             |
220 | 219 | 3ad2ant1 1028 |
. . . . . . 7
 
 ..^           ![(,] (,]](_ioc.gif)                     |
221 | 214, 220 | breqtrd 4426 |
. . . . . 6
 
 ..^           ![(,] (,]](_ioc.gif)                  
  |
222 | | elioore 11663 |
. . . . . . . . . . 11
                 |
223 | 135 | oveq2d 6304 |
. . . . . . . . . . . . . 14
                     |
224 | 133 | recnd 9666 |
. . . . . . . . . . . . . . 15
           |
225 | 52 | recnd 9666 |
. . . . . . . . . . . . . . 15
   |
226 | 224, 225 | mulneg1d 10068 |
. . . . . . . . . . . . . 14
                         |
227 | 223, 226 | oveq12d 6306 |
. . . . . . . . . . . . 13
                                               |
228 | 227 | adantr 467 |
. . . . . . . . . . . 12
 

                                              |
229 | | simpr 463 |
. . . . . . . . . . . . . . 15
 

  |
230 | 134 | adantr 467 |
. . . . . . . . . . . . . . 15
 

            |
231 | 229, 230 | readdcld 9667 |
. . . . . . . . . . . . . 14
 

              |
232 | 231 | recnd 9666 |
. . . . . . . . . . . . 13
 

              |
233 | 230 | recnd 9666 |
. . . . . . . . . . . . 13
 

            |
234 | 232, 233 | negsubd 9989 |
. . . . . . . . . . . 12
 

                                                   |
235 | 229 | recnd 9666 |
. . . . . . . . . . . . 13
 

  |
236 | 235, 233 | pncand 9984 |
. . . . . . . . . . . 12
 

                          |
237 | 228, 234,
236 | 3eqtrrd 2489 |
. . . . . . . . . . 11
 

                     |
238 | 222, 237 | sylan2 477 |
. . . . . . . . . 10
 
              
                     |
239 | 238 | 3ad2antl1 1169 |
. . . . . . . . 9
    ..^           ![(,] (,]](_ioc.gif)                       
                     |
240 | | simpl1 1010 |
. . . . . . . . . 10
    ..^           ![(,] (,]](_ioc.gif)                       
  |
241 | | fourierdlem41.qssd |
. . . . . . . . . . . . 13
 
 ..^                  |
242 | 241 | 3adant3 1027 |
. . . . . . . . . . . 12
 
 ..^           ![(,] (,]](_ioc.gif)                      
  |
243 | 242 | adantr 467 |
. . . . . . . . . . 11
    ..^           ![(,] (,]](_ioc.gif)                       
                |
244 | 205 | adantr 467 |
. . . . . . . . . . . 12
    ..^           ![(,] (,]](_ioc.gif)                       
      |
245 | 210 | adantr 467 |
. . . . . . . . . . . 12
    ..^           ![(,] (,]](_ioc.gif)                       
        |
246 | 222 | adantl 468 |
. . . . . . . . . . . . . 14
 
              
  |
247 | 136 | adantr 467 |
. . . . . . . . . . . . . 14
 
              
      |
248 | 246, 247 | readdcld 9667 |
. . . . . . . . . . . . 13
 
              
        |
249 | 248 | 3ad2antl1 1169 |
. . . . . . . . . . . 12
    ..^           ![(,] (,]](_ioc.gif)                       
        |
250 | 136 | adantr 467 |
. . . . . . . . . . . . . . . . . 18
 
 ..^        |
251 | 200, 250 | resubcld 10044 |
. . . . . . . . . . . . . . . . 17
 
 ..^              |
252 | 251 | rexrd 9687 |
. . . . . . . . . . . . . . . 16
 
 ..^              |
253 | 252 | adantr 467 |
. . . . . . . . . . . . . . 15
    ..^                
            |
254 | 74 | rexrd 9687 |
. . . . . . . . . . . . . . . 16
   |
255 | 254 | ad2antrr 731 |
. . . . . . . . . . . . . . 15
    ..^                
  |
256 | | simpr 463 |
. . . . . . . . . . . . . . 15
    ..^                
                |
257 | | ioogtlb 37586 |
. . . . . . . . . . . . . . 15
                          
            |
258 | 253, 255,
256, 257 | syl3anc 1267 |
. . . . . . . . . . . . . 14
    ..^                
            |
259 | 200 | adantr 467 |
. . . . . . . . . . . . . . 15
    ..^                
      |
260 | 136 | ad2antrr 731 |
. . . . . . . . . . . . . . 15
    ..^                
      |
261 | 222 | adantl 468 |
. . . . . . . . . . . . . . 15
    ..^                
  |
262 | 259, 260,
261 | ltsubaddd 10206 |
. . . . . . . . . . . . . 14
    ..^                
          
             |
263 | 258, 262 | mpbid 214 |
. . . . . . . . . . . . 13
    ..^                
            |
264 | 263 | 3adantl3 1165 |
. . . . . . . . . . . 12
    ..^           ![(,] (,]](_ioc.gif)                       
            |
265 | 240, 139 | syl 17 |
. . . . . . . . . . . . 13
    ..^           ![(,] (,]](_ioc.gif)                       
      |
266 | 208 | adantr 467 |
. . . . . . . . . . . . . 14
    ..^                
        |
267 | 266 | 3adantl3 1165 |
. . . . . . . . . . . . 13
    ..^           ![(,] (,]](_ioc.gif)                       
        |
268 | 74 | ad2antrr 731 |
. . . . . . . . . . . . . . . 16
    ..^                
  |
269 | | iooltub 37604 |
. . . . . . . . . . . . . . . . 17
                          
  |
270 | 253, 255,
256, 269 | syl3anc 1267 |
. . . . . . . . . . . . . . . 16
    ..^                
  |
271 | 261, 268,
260, 270 | ltadd1dd 10221 |
. . . . . . . . . . . . . . 15
    ..^                
              |
272 | 138 | eqcomd 2456 |
. . . . . . . . . . . . . . . 16
             |
273 | 272 | ad2antrr 731 |
. . . . . . . . . . . . . . 15
    ..^                
            |
274 | 271, 273 | breqtrd 4426 |
. . . . . . . . . . . . . 14
    ..^                
            |
275 | 274 | 3adantl3 1165 |
. . . . . . . . . . . . 13
    ..^           ![(,] (,]](_ioc.gif)                       
            |
276 | | iocleub 37594 |
. . . . . . . . . . . . . . 15
           
          ![(,] (,]](_ioc.gif)                     |
277 | 205, 210,
211, 276 | syl3anc 1267 |
. . . . . . . . . . . . . 14
 
 ..^           ![(,] (,]](_ioc.gif)            
        |
278 | 277 | adantr 467 |
. . . . . . . . . . . . 13
    ..^           ![(,] (,]](_ioc.gif)                       
            |
279 | 249, 265,
267, 275, 278 | ltletrd 9792 |
. . . . . . . . . . . 12
    ..^           ![(,] (,]](_ioc.gif)                       
              |
280 | 244, 245,
249, 264, 279 | eliood 37589 |
. . . . . . . . . . 11
    ..^           ![(,] (,]](_ioc.gif)                       
                      |
281 | 243, 280 | sseldd 3432 |
. . . . . . . . . 10
    ..^           ![(,] (,]](_ioc.gif)                       
        |
282 | 240, 131 | syl 17 |
. . . . . . . . . . . 12
    ..^           ![(,] (,]](_ioc.gif)                       
 
    |
283 | 282 | flcld 12031 |
. . . . . . . . . . 11
    ..^           ![(,] (,]](_ioc.gif)                       
          |
284 | 283 | znegcld 11039 |
. . . . . . . . . 10
    ..^           ![(,] (,]](_ioc.gif)                       
           |
285 | | negex 9870 |
. . . . . . . . . . 11
          |
286 | | eleq1 2516 |
. . . . . . . . . . . . 13
          
            |
287 | 286 | 3anbi3d 1344 |
. . . . . . . . . . . 12
           
      
                    |
288 | | oveq1 6295 |
. . . . . . . . . . . . . 14
                         |
289 | 288 | oveq2d 6304 |
. . . . . . . . . . . . 13
                                         |
290 | 289 | eleq1d 2512 |
. . . . . . . . . . . 12
                    
                      |
291 | 287, 290 | imbi12d 322 |
. . . . . . . . . . 11
                  
                                                     |
292 | | ovex 6316 |
. . . . . . . . . . . 12
       |
293 | | eleq1 2516 |
. . . . . . . . . . . . . 14
       
         |
294 | 293 | 3anbi2d 1343 |
. . . . . . . . . . . . 13
        

      
    |
295 | | oveq1 6295 |
. . . . . . . . . . . . . 14
                       |
296 | 295 | eleq1d 2512 |
. . . . . . . . . . . . 13
           
             |
297 | 294, 296 | imbi12d 322 |
. . . . . . . . . . . 12
         
             
               |
298 | | fourierdlem41.dper |
. . . . . . . . . . . 12
 
       |
299 | 292, 297,
298 | vtocl 3099 |
. . . . . . . . . . 11
 
                   |
300 | 285, 291,
299 | vtocl 3099 |
. . . . . . . . . 10
 
                                     |
301 | 240, 281,
284, 300 | syl3anc 1267 |
. . . . . . . . 9
    ..^           ![(,] (,]](_ioc.gif)                       
                     |
302 | 239, 301 | eqeltrd 2528 |
. . . . . . . 8
    ..^           ![(,] (,]](_ioc.gif)                       
  |
303 | 302 | ralrimiva 2801 |
. . . . . . 7
 
 ..^           ![(,] (,]](_ioc.gif)         
                 |
304 | | dfss3 3421 |
. . . . . . 7
              
                  |
305 | 303, 304 | sylibr 216 |
. . . . . 6
 
 ..^           ![(,] (,]](_ioc.gif)                         |
306 | | breq1 4404 |
. . . . . . . 8
          
              |
307 | | oveq1 6295 |
. . . . . . . . 9
          
                    |
308 | 307 | sseq1d 3458 |
. . . . . . . 8
          
    
                 |
309 | 306, 308 | anbi12d 716 |
. . . . . . 7
          
 
   
           
                  |
310 | 309 | rspcev 3149 |
. . . . . 6
                                            
   |
311 | 203, 221,
305, 310 | syl12anc 1265 |
. . . . 5
 
 ..^           ![(,] (,]](_ioc.gif)         
    
   |
312 | 311 | 3exp 1206 |
. . . 4
   ..^            ![(,] (,]](_ioc.gif)             
     |
313 | 312 | rexlimdv 2876 |
. . 3
    ..^            ![(,] (,]](_ioc.gif)        
    
    |
314 | 196, 313 | mpd 15 |
. 2
      
   |
315 | | 0zd 10946 |
. . . . . . . . . 10
   |
316 | 3 | nnzd 11036 |
. . . . . . . . . 10
   |
317 | | 1zzd 10965 |
. . . . . . . . . 10
   |
318 | 315, 316,
317 | 3jca 1187 |
. . . . . . . . 9
 
   |
319 | | 0le1 10134 |
. . . . . . . . . 10
 |
320 | 319 | a1i 11 |
. . . . . . . . 9

  |
321 | 3 | nnge1d 10649 |
. . . . . . . . 9

  |
322 | 318, 320,
321 | jca32 538 |
. . . . . . . 8
    
    |
323 | | elfz2 11788 |
. . . . . . . 8
    
 
 
    |
324 | 322, 323 | sylibr 216 |
. . . . . . 7
       |
325 | 101, 324 | ffvelrnd 6021 |
. . . . . 6
       |
326 | 136, 52 | resubcld 10044 |
. . . . . 6
         |
327 | 325, 326 | resubcld 10044 |
. . . . 5
               |
328 | 327 | adantr 467 |
. . . 4
 
    
              |
329 | 38 | recnd 9666 |
. . . . . . . . . 10
   |
330 | 329, 225 | pncand 9984 |
. . . . . . . . 9
       |
331 | 330 | adantr 467 |
. . . . . . . 8
 
    
 
    |
332 | 43 | oveq2i 6299 |
. . . . . . . . . . 11
       |
333 | 332 | a1i 11 |
. . . . . . . . . 10
 
    
        |
334 | 40 | recnd 9666 |
. . . . . . . . . . . 12
   |
335 | 329, 334 | pncan3d 9986 |
. . . . . . . . . . 11
       |
336 | 335 | adantr 467 |
. . . . . . . . . 10
 
    
      |
337 | | id 22 |
. . . . . . . . . . . 12
           |
338 | 337 | eqcomd 2456 |
. . . . . . . . . . 11
           |
339 | 338 | adantl 468 |
. . . . . . . . . 10
 
    
      |
340 | 333, 336,
339 | 3eqtrrd 2489 |
. . . . . . . . 9
 
    
        |
341 | 340 | oveq1d 6303 |
. . . . . . . 8
 
    
            |
342 | 33 | adantr 467 |
. . . . . . . 8
 
    
      |
343 | 331, 341,
342 | 3eqtr4rd 2495 |
. . . . . . 7
 
    
            |
344 | 343 | oveq1d 6303 |
. . . . . 6
 
    
                            |
345 | 139 | recnd 9666 |
. . . . . . . 8
       |
346 | 345, 217,
225 | nnncan2d 10018 |
. . . . . . 7
                           |
347 | 346 | adantr 467 |
. . . . . 6
 
    
                          |
348 | 219 | adantr 467 |
. . . . . 6
 
    
            |
349 | 344, 347,
348 | 3eqtrrd 2489 |
. . . . 5
 
    
              |
350 | 33, 38 | eqeltrd 2528 |
. . . . . . 7
       |
351 | 3 | nngt0d 10650 |
. . . . . . . . . 10
   |
352 | | fzolb 11923 |
. . . . . . . . . 10
  ..^     |
353 | 315, 316,
351, 352 | syl3anbrc 1191 |
. . . . . . . . 9
  ..^   |
354 | | 0re 9640 |
. . . . . . . . . 10
 |
355 | | eleq1 2516 |
. . . . . . . . . . . . 13
   ..^
 ..^    |
356 | 355 | anbi2d 709 |
. . . . . . . . . . . 12
  
 ..^  
 ..^     |
357 | | fveq2 5863 |
. . . . . . . . . . . . 13
           |
358 | | oveq1 6295 |
. . . . . . . . . . . . . 14
       |
359 | 358 | fveq2d 5867 |
. . . . . . . . . . . . 13
               |
360 | 357, 359 | breq12d 4414 |
. . . . . . . . . . . 12
     
     
             |
361 | 356, 360 | imbi12d 322 |
. . . . . . . . . . 11
   
 ..^     
      
   ..^                |
362 | 361, 152 | vtoclg 3106 |
. . . . . . . . . 10
  
 ..^ 
             |
363 | 354, 362 | ax-mp 5 |
. . . . . . . . 9
 
 ..^              |
364 | 353, 363 | mpdan 673 |
. . . . . . . 8
    
        |
365 | | 0p1e1 10718 |
. . . . . . . . . 10
   |
366 | 365 | fveq2i 5866 |
. . . . . . . . 9
           |
367 | 366 | a1i 11 |
. . . . . . . 8
             |
368 | 364, 367 | breqtrd 4426 |
. . . . . . 7
    
      |
369 | 350, 325,
326, 368 | ltsub1dd 10222 |
. . . . . 6
                           |
370 | 369 | adantr 467 |
. . . . 5
 
    
                          |
371 | 349, 370 | eqbrtrd 4422 |
. . . 4
 
    
              |
372 | | elioore 11663 |
. . . . . . . . 9
                   |
373 | 135 | eqcomd 2456 |
. . . . . . . . . . . . . . . 16
                 |
374 | 373 | negeqd 9866 |
. . . . . . . . . . . . . . 15
                   |
375 | 226, 374 | eqtrd 2484 |
. . . . . . . . . . . . . 14
                   |
376 | 225 | mulid2d 9658 |
. . . . . . . . . . . . . 14
     |
377 | 375, 376 | oveq12d 6306 |
. . . . . . . . . . . . 13
                         |
378 | 224 | negcld 9970 |
. . . . . . . . . . . . . 14
            |
379 | | 1cnd 9656 |
. . . . . . . . . . . . . 14
   |
380 | 378, 379,
225 | adddird 9665 |
. . . . . . . . . . . . 13
                               |
381 | 217, 225 | negsubdid 9998 |
. . . . . . . . . . . . 13
                 |
382 | 377, 380,
381 | 3eqtr4d 2494 |
. . . . . . . . . . . 12
                       |
383 | 382 | oveq2d 6304 |
. . . . . . . . . . 11
                                           |
384 | 383 | adantr 467 |
. . . . . . . . . 10
 

                                          |
385 | 326 | adantr 467 |
. . . . . . . . . . . . 13
 

        |
386 | 229, 385 | readdcld 9667 |
. . . . . . . . . . . 12
 

          |
387 | 386 | recnd 9666 |
. . . . . . . . . . 11
 

          |
388 | 385 | recnd 9666 |
. . . . . . . . . . 11
 

        |
389 | 387, 388 | negsubd 9989 |
. . . . . . . . . 10
 

                                   |
390 | 235, 388 | pncand 9984 |
. . . . . . . . . 10
 

                  |
391 | 384, 389,
390 | 3eqtrrd 2489 |
. . . . . . . . 9
 

                         |
392 | 372, 391 | sylan2 477 |
. . . . . . . 8
 
                
                         |
393 | 392 | adantlr 720 |
. . . . . . 7
                                                  |
394 | | simpll 759 |
. . . . . . . 8
                           |
395 | 367 | eqcomd 2456 |
. . . . . . . . . . . 12
             |
396 | 395 | oveq2d 6304 |
. . . . . . . . . . 11
                             |
397 | 357, 359 | oveq12d 6306 |
. . . . . . . . . . . . . . . 16
                               |
398 | 397 | sseq1d 3458 |
. . . . . . . . . . . . . . 15
               
                 |
399 | 356, 398 | imbi12d 322 |
. . . . . . . . . . . . . 14
   
 ..^               
    ..^ 
                  |
400 | 399, 241 | vtoclg 3106 |
. . . . . . . . . . . . 13
  
 ..^ 
                 |
401 | 354, 400 | ax-mp 5 |
. . . . . . . . . . . 12
 
 ..^                  |
402 | 353, 401 | mpdan 673 |
. . . . . . . . . . 11
              
  |
403 | 396, 402 | eqsstrd 3465 |
. . . . . . . . . 10
            
  |
404 | 403 | ad2antrr 731 |
. . . . . . . . 9
                                       |
405 | 33, 39 | eqeltrd 2528 |
. . . . . . . . . . 11
       |
406 | 405 | ad2antrr 731 |
. . . . . . . . . 10
                               |
407 | 325 | rexrd 9687 |
. . . . . . . . . . 11
       |
408 | 407 | ad2antrr 731 |
. . . . . . . . . 10
                               |
409 | 372, 386 | sylan2 477 |
. . . . . . . . . . 11
 
                
          |
410 | 409 | adantlr 720 |
. . . . . . . . . 10
                                   |
411 | 345, 216,
217 | subaddd 10001 |
. . . . . . . . . . . . . . . . 17
                         |
412 | 272, 411 | mpbird 236 |
. . . . . . . . . . . . . . . 16
             |
413 | | oveq1 6295 |
. . . . . . . . . . . . . . . 16
               |
414 | 412, 413 | sylan9req 2505 |
. . . . . . . . . . . . . . 15
 
    
        |
415 | 414 | oveq1d 6303 |
. . . . . . . . . . . . . 14
 
    
            |
416 | 415 | oveq2d 6304 |
. . . . . . . . . . . . 13
 
    
                |
417 | 130 | recnd 9666 |
. . . . . . . . . . . . . . . 16
     |
418 | 216, 417,
225 | addsubassd 10003 |
. . . . . . . . . . . . . . 15
   
           |
419 | 418 | eqcomd 2456 |
. . . . . . . . . . . . . 14
               |
420 | 419 | adantr 467 |
. . . . . . . . . . . . 13
 
    
        
     |
421 | 334, 225,
329 | subsub23d 37494 |
. . . . . . . . . . . . . . . 16
         |
422 | 58, 421 | mpbird 236 |
. . . . . . . . . . . . . . 15
     |
423 | 216, 334 | pncan3d 9986 |
. . . . . . . . . . . . . . . 16
       |
424 | 423 | oveq1d 6303 |
. . . . . . . . . . . . . . 15
   
       |
425 | 422, 424,
33 | 3eqtr4d 2494 |
. . . . . . . . . . . . . 14
   
         |
426 | 425 | adantr 467 |
. . . . . . . . . . . . 13
 
    
 
          |
427 | 416, 420,
426 | 3eqtrrd 2489 |
. . . . . . . . . . . 12
 
    
              |
428 | 427 | adantr 467 |
. . . . . . . . . . 11
                                       |
429 | 74 | adantr 467 |
. . . . . . . . . . . . 13
 
                
  |
430 | 372 | adantl 468 |
. . . . . . . . . . . . 13
 
                
  |
431 | 326 | adantr 467 |
. . . . . . . . . . . . 13
 
                
        |
432 | 254 | adantr 467 |
. . . . . . . . . . . . . 14
 
                
  |
433 | 327 | rexrd 9687 |
. . . . . . . . . . . . . . 15
               |
434 | 433 | adantr 467 |
. . . . . . . . . . . . . 14
 
                
              |
435 | | simpr 463 |
. . . . . . . . . . . . . 14
 
           |