Proof of Theorem fourierdlem78
Step | Hyp | Ref
| Expression |
1 | | fourierdlem78.g |
. . . . 5
    ![[,] [,]](_icc.gif)              |
2 | 1 | a1i 11 |
. . . 4
     ![[,] [,]](_icc.gif)               |
3 | 2 | reseq1d 5104 |
. . 3
            ![[,] [,]](_icc.gif)                    |
4 | | pire 23413 |
. . . . . . . . 9
 |
5 | 4 | renegcli 9935 |
. . . . . . . 8
  |
6 | 5 | a1i 11 |
. . . . . . 7
 
    
   |
7 | 4 | a1i 11 |
. . . . . . 7
 
    
  |
8 | | elioore 11666 |
. . . . . . . 8
       |
9 | 8 | adantl 468 |
. . . . . . 7
 
    
  |
10 | 5 | a1i 11 |
. . . . . . . . . . . 12
    |
11 | 4 | a1i 11 |
. . . . . . . . . . . 12
   |
12 | 10, 11 | iccssred 37602 |
. . . . . . . . . . 11
    ![[,] [,]](_icc.gif) 
  |
13 | | fourierdlem78.a |
. . . . . . . . . . 11
    ![[,] [,]](_icc.gif)    |
14 | 12, 13 | sseldd 3433 |
. . . . . . . . . 10
   |
15 | 14 | adantr 467 |
. . . . . . . . 9
 
    
  |
16 | 5, 4 | elicc2i 11700 |
. . . . . . . . . . . 12
    ![[,] [,]](_icc.gif) 
     |
17 | 16 | simp2bi 1024 |
. . . . . . . . . . 11
    ![[,] [,]](_icc.gif)     |
18 | 13, 17 | syl 17 |
. . . . . . . . . 10
    |
19 | 18 | adantr 467 |
. . . . . . . . 9
 
    
   |
20 | 15 | rexrd 9690 |
. . . . . . . . . 10
 
    
  |
21 | | fourierdlem78.b |
. . . . . . . . . . . . 13
    ![[,] [,]](_icc.gif)    |
22 | 12, 21 | sseldd 3433 |
. . . . . . . . . . . 12
   |
23 | 22 | rexrd 9690 |
. . . . . . . . . . 11
   |
24 | 23 | adantr 467 |
. . . . . . . . . 10
 
    
  |
25 | | simpr 463 |
. . . . . . . . . 10
 
    
      |
26 | | ioogtlb 37592 |
. . . . . . . . . 10
         |
27 | 20, 24, 25, 26 | syl3anc 1268 |
. . . . . . . . 9
 
    
  |
28 | 6, 15, 9, 19, 27 | lelttrd 9793 |
. . . . . . . 8
 
    
   |
29 | 6, 9, 28 | ltled 9783 |
. . . . . . 7
 
    
   |
30 | 22 | adantr 467 |
. . . . . . . . 9
 
    
  |
31 | | iooltub 37610 |
. . . . . . . . . 10
         |
32 | 20, 24, 25, 31 | syl3anc 1268 |
. . . . . . . . 9
 
    
  |
33 | 5, 4 | elicc2i 11700 |
. . . . . . . . . . . 12
    ![[,] [,]](_icc.gif) 
     |
34 | 33 | simp3bi 1025 |
. . . . . . . . . . 11
    ![[,] [,]](_icc.gif)    |
35 | 21, 34 | syl 17 |
. . . . . . . . . 10

  |
36 | 35 | adantr 467 |
. . . . . . . . 9
 
    
  |
37 | 9, 30, 7, 32, 36 | ltletrd 9795 |
. . . . . . . 8
 
    
  |
38 | 9, 7, 37 | ltled 9783 |
. . . . . . 7
 
    
  |
39 | 6, 7, 9, 29, 38 | eliccd 37601 |
. . . . . 6
 
    
   ![[,] [,]](_icc.gif)    |
40 | 39 | ex 436 |
. . . . 5
         ![[,] [,]](_icc.gif)     |
41 | 40 | ssrdv 3438 |
. . . 4
    
   ![[,] [,]](_icc.gif)    |
42 | 41 | resmptd 5156 |
. . 3
      ![[,] [,]](_icc.gif) 
                                  |
43 | 3, 42 | eqtrd 2485 |
. 2
                         |
44 | | 0red 9644 |
. . . . . . . . . . 11
 
    
  |
45 | | fourierdlem78.f |
. . . . . . . . . . . . . . 15
       |
46 | 45 | adantr 467 |
. . . . . . . . . . . . . 14
 
    
      |
47 | | fourierdlem78.x |
. . . . . . . . . . . . . . . 16
   |
48 | 47 | adantr 467 |
. . . . . . . . . . . . . . 15
 
    
  |
49 | 48, 9 | readdcld 9670 |
. . . . . . . . . . . . . 14
 
    
    |
50 | 46, 49 | ffvelrnd 6023 |
. . . . . . . . . . . . 13
 
    
        |
51 | | fourierdlem78.y |
. . . . . . . . . . . . . . 15
   |
52 | | fourierdlem78.w |
. . . . . . . . . . . . . . 15
   |
53 | 51, 52 | ifcld 3924 |
. . . . . . . . . . . . . 14
        |
54 | 53 | adantr 467 |
. . . . . . . . . . . . 13
 
    
 
 
   |
55 | 50, 54 | resubcld 10047 |
. . . . . . . . . . . 12
 
    
               |
56 | | eleq1 2517 |
. . . . . . . . . . . . . . . 16
     
       |
57 | 56 | biimpac 489 |
. . . . . . . . . . . . . . 15
     
       |
58 | 57 | adantll 720 |
. . . . . . . . . . . . . 14
               |
59 | | fourierdlem78.nxelab |
. . . . . . . . . . . . . . 15
       |
60 | 59 | ad2antrr 732 |
. . . . . . . . . . . . . 14
        
      |
61 | 58, 60 | pm2.65da 580 |
. . . . . . . . . . . . 13
 
    
  |
62 | 61 | neqned 2631 |
. . . . . . . . . . . 12
 
    
  |
63 | 55, 9, 62 | redivcld 10435 |
. . . . . . . . . . 11
 
    
     
           |
64 | 44, 63 | ifcld 3924 |
. . . . . . . . . 10
 
    
         
            |
65 | | fourierdlem78.h |
. . . . . . . . . . 11
    ![[,] [,]](_icc.gif)                        |
66 | 65 | fvmpt2 5957 |
. . . . . . . . . 10
     ![[,] [,]](_icc.gif)           
                        
            |
67 | 39, 64, 66 | syl2anc 667 |
. . . . . . . . 9
 
    
             
            |
68 | 67, 64 | eqeltrd 2529 |
. . . . . . . 8
 
    
      |
69 | | 1red 9658 |
. . . . . . . . . . 11
 
    
  |
70 | | 2re 10679 |
. . . . . . . . . . . . . 14
 |
71 | 70 | a1i 11 |
. . . . . . . . . . . . 13
 
    
  |
72 | 9 | rehalfcld 10859 |
. . . . . . . . . . . . . 14
 
    
    |
73 | 72 | resincld 14197 |
. . . . . . . . . . . . 13
 
    
        |
74 | 71, 73 | remulcld 9671 |
. . . . . . . . . . . 12
 
    
          |
75 | 71 | recnd 9669 |
. . . . . . . . . . . . 13
 
    
  |
76 | 73 | recnd 9669 |
. . . . . . . . . . . . 13
 
    
        |
77 | | 2ne0 10702 |
. . . . . . . . . . . . . 14
 |
78 | 77 | a1i 11 |
. . . . . . . . . . . . 13
 
    
  |
79 | | fourierdlem44 38015 |
. . . . . . . . . . . . . 14
     ![[,] [,]](_icc.gif)           |
80 | 39, 62, 79 | syl2anc 667 |
. . . . . . . . . . . . 13
 
    
        |
81 | 75, 76, 78, 80 | mulne0d 10264 |
. . . . . . . . . . . 12
 
    
          |
82 | 9, 74, 81 | redivcld 10435 |
. . . . . . . . . . 11
 
    
            |
83 | 69, 82 | ifcld 3924 |
. . . . . . . . . 10
 
    
                 |
84 | | fourierdlem78.k |
. . . . . . . . . . 11
    ![[,] [,]](_icc.gif)                   |
85 | 84 | fvmpt2 5957 |
. . . . . . . . . 10
     ![[,] [,]](_icc.gif)                                       |
86 | 39, 83, 85 | syl2anc 667 |
. . . . . . . . 9
 
    
                     |
87 | 86, 83 | eqeltrd 2529 |
. . . . . . . 8
 
    
      |
88 | 68, 87 | remulcld 9671 |
. . . . . . 7
 
    
            |
89 | | fourierdlem78.u |
. . . . . . . 8
    ![[,] [,]](_icc.gif)              |
90 | 89 | fvmpt2 5957 |
. . . . . . 7
     ![[,] [,]](_icc.gif)                             |
91 | 39, 88, 90 | syl2anc 667 |
. . . . . 6
 
    
                |
92 | 91, 88 | eqeltrd 2529 |
. . . . 5
 
    
      |
93 | | fourierdlem78.n |
. . . . . . . . . . 11
   |
94 | 93 | adantr 467 |
. . . . . . . . . 10
 
    
  |
95 | 71, 78 | rereccld 10434 |
. . . . . . . . . 10
 
    
    |
96 | 94, 95 | readdcld 9670 |
. . . . . . . . 9
 
    
      |
97 | 96, 9 | remulcld 9671 |
. . . . . . . 8
 
    
 
      |
98 | 97 | resincld 14197 |
. . . . . . 7
 
    
            |
99 | | fourierdlem78.s |
. . . . . . . 8
    ![[,] [,]](_icc.gif)              |
100 | 99 | fvmpt2 5957 |
. . . . . . 7
     ![[,] [,]](_icc.gif)                             |
101 | 39, 98, 100 | syl2anc 667 |
. . . . . 6
 
    
                |
102 | 101, 98 | eqeltrd 2529 |
. . . . 5
 
    
      |
103 | 92, 102 | remulcld 9671 |
. . . 4
 
    
            |
104 | | eqid 2451 |
. . . 4
                                 |
105 | 103, 104 | fmptd 6046 |
. . 3
                           |
106 | | ax-resscn 9596 |
. . . . 5
 |
107 | 106 | a1i 11 |
. . . 4

  |
108 | 91 | mpteq2dva 4489 |
. . . . . 6
                             |
109 | 61 | iffalsed 3892 |
. . . . . . . . . 10
 
    
         
               
           |
110 | 55 | recnd 9669 |
. . . . . . . . . . 11
 
    
               |
111 | 9 | recnd 9669 |
. . . . . . . . . . 11
 
    
  |
112 | 110, 111,
62 | divrecd 10386 |
. . . . . . . . . 10
 
    
     
                            |
113 | 67, 109, 112 | 3eqtrd 2489 |
. . . . . . . . 9
 
    
         
             |
114 | 113 | mpteq2dva 4489 |
. . . . . . . 8
                     
              |
115 | 50 | recnd 9669 |
. . . . . . . . . . . . 13
 
    
        |
116 | 54 | recnd 9669 |
. . . . . . . . . . . . 13
 
    
 
 
   |
117 | 115, 116 | negsubd 9992 |
. . . . . . . . . . . 12
 
    
                  
          |
118 | 117 | eqcomd 2457 |
. . . . . . . . . . 11
 
    
                 
           |
119 | 118 | mpteq2dva 4489 |
. . . . . . . . . 10
          
                  
            |
120 | 14, 47 | readdcld 9670 |
. . . . . . . . . . . . . . . . . 18
     |
121 | 120 | rexrd 9690 |
. . . . . . . . . . . . . . . . 17
     |
122 | 121 | adantr 467 |
. . . . . . . . . . . . . . . 16
 
    
    |
123 | 22, 47 | readdcld 9670 |
. . . . . . . . . . . . . . . . . 18
     |
124 | 123 | rexrd 9690 |
. . . . . . . . . . . . . . . . 17
     |
125 | 124 | adantr 467 |
. . . . . . . . . . . . . . . 16
 
    
    |
126 | 14 | recnd 9669 |
. . . . . . . . . . . . . . . . . . 19
   |
127 | 47 | recnd 9669 |
. . . . . . . . . . . . . . . . . . 19
   |
128 | 126, 127 | addcomd 9835 |
. . . . . . . . . . . . . . . . . 18
       |
129 | 128 | adantr 467 |
. . . . . . . . . . . . . . . . 17
 
    
      |
130 | 15, 9, 48, 27 | ltadd2dd 9794 |
. . . . . . . . . . . . . . . . 17
 
    
  
   |
131 | 129, 130 | eqbrtrd 4423 |
. . . . . . . . . . . . . . . 16
 
    
  
   |
132 | 9, 30, 48, 32 | ltadd2dd 9794 |
. . . . . . . . . . . . . . . . 17
 
    
      |
133 | 22 | recnd 9669 |
. . . . . . . . . . . . . . . . . . 19
   |
134 | 127, 133 | addcomd 9835 |
. . . . . . . . . . . . . . . . . 18
       |
135 | 134 | adantr 467 |
. . . . . . . . . . . . . . . . 17
 
    
      |
136 | 132, 135 | breqtrd 4427 |
. . . . . . . . . . . . . . . 16
 
    
      |
137 | 122, 125,
49, 131, 136 | eliood 37595 |
. . . . . . . . . . . . . . 15
 
    
       
    |
138 | | fvres 5879 |
. . . . . . . . . . . . . . 15
                              
    |
139 | 137, 138 | syl 17 |
. . . . . . . . . . . . . 14
 
    
             
          |
140 | 139 | eqcomd 2457 |
. . . . . . . . . . . . 13
 
    
                        |
141 | 140 | mpteq2dva 4489 |
. . . . . . . . . . . 12
         
                           |
142 | | ioosscn 37591 |
. . . . . . . . . . . . . 14
         |
143 | 142 | a1i 11 |
. . . . . . . . . . . . 13
      
 
  |
144 | | fourierdlem78.fcn |
. . . . . . . . . . . . 13
                         |
145 | | ioosscn 37591 |
. . . . . . . . . . . . . 14
     |
146 | 145 | a1i 11 |
. . . . . . . . . . . . 13
    
  |
147 | 143, 144,
146, 127, 137 | fourierdlem23 37992 |
. . . . . . . . . . . 12
             
     
             |
148 | 141, 147 | eqeltrd 2529 |
. . . . . . . . . . 11
         
             |
149 | | 0red 9644 |
. . . . . . . . . . . . . . . . 17
           |
150 | 14 | ad2antrr 732 |
. . . . . . . . . . . . . . . . 17
           |
151 | 8 | adantl 468 |
. . . . . . . . . . . . . . . . 17
           |
152 | | simplr 762 |
. . . . . . . . . . . . . . . . 17
           |
153 | 27 | adantlr 721 |
. . . . . . . . . . . . . . . . 17
           |
154 | 149, 150,
151, 152, 153 | lelttrd 9793 |
. . . . . . . . . . . . . . . 16
           |
155 | 154 | iftrued 3889 |
. . . . . . . . . . . . . . 15
                |
156 | 155 | negeqd 9869 |
. . . . . . . . . . . . . 14
                  |
157 | 156 | mpteq2dva 4489 |
. . . . . . . . . . . . 13
 

                     |
158 | 51 | renegcld 10046 |
. . . . . . . . . . . . . . . 16
    |
159 | 158 | recnd 9669 |
. . . . . . . . . . . . . . 15
    |
160 | | ssid 3451 |
. . . . . . . . . . . . . . . 16
 |
161 | 160 | a1i 11 |
. . . . . . . . . . . . . . 15

  |
162 | 146, 159,
161 | constcncfg 37748 |
. . . . . . . . . . . . . 14
                  |
163 | 162 | adantr 467 |
. . . . . . . . . . . . 13
 

                 |
164 | 157, 163 | eqeltrd 2529 |
. . . . . . . . . . . 12
 

                      |
165 | | simpl 459 |
. . . . . . . . . . . . 13
 
   |
166 | 14 | rexrd 9690 |
. . . . . . . . . . . . . . . 16
   |
167 | 166 | ad2antrr 732 |
. . . . . . . . . . . . . . 15
   
   |
168 | 23 | ad2antrr 732 |
. . . . . . . . . . . . . . 15
   
   |
169 | | 0red 9644 |
. . . . . . . . . . . . . . 15
   
   |
170 | | simpr 463 |
. . . . . . . . . . . . . . . . 17
 
   |
171 | 14 | adantr 467 |
. . . . . . . . . . . . . . . . . 18
 
   |
172 | | 0red 9644 |
. . . . . . . . . . . . . . . . . 18
 
   |
173 | 171, 172 | ltnled 9782 |
. . . . . . . . . . . . . . . . 17
 
 
   |
174 | 170, 173 | mpbird 236 |
. . . . . . . . . . . . . . . 16
 
   |
175 | 174 | adantr 467 |
. . . . . . . . . . . . . . 15
   
   |
176 | | simpr 463 |
. . . . . . . . . . . . . . . . 17
 
   |
177 | | 0red 9644 |
. . . . . . . . . . . . . . . . . 18
 
   |
178 | 22 | adantr 467 |
. . . . . . . . . . . . . . . . . 18
 
   |
179 | 177, 178 | ltnled 9782 |
. . . . . . . . . . . . . . . . 17
 
 
   |
180 | 176, 179 | mpbird 236 |
. . . . . . . . . . . . . . . 16
 
   |
181 | 180 | adantlr 721 |
. . . . . . . . . . . . . . 15
   
   |
182 | 167, 168,
169, 175, 181 | eliood 37595 |
. . . . . . . . . . . . . 14
   
       |
183 | 59 | ad2antrr 732 |
. . . . . . . . . . . . . 14
   

      |
184 | 182, 183 | condan 803 |
. . . . . . . . . . . . 13
 
   |
185 | 8 | adantl 468 |
. . . . . . . . . . . . . . . . . 18
           |
186 | | 0red 9644 |
. . . . . . . . . . . . . . . . . 18
           |
187 | 22 | ad2antrr 732 |
. . . . . . . . . . . . . . . . . . 19
           |
188 | 32 | adantlr 721 |
. . . . . . . . . . . . . . . . . . 19
           |
189 | | simplr 762 |
. . . . . . . . . . . . . . . . . . 19
           |
190 | 185, 187,
186, 188, 189 | ltletrd 9795 |
. . . . . . . . . . . . . . . . . 18
           |
191 | 185, 186,
190 | ltnsymd 9784 |
. . . . . . . . . . . . . . . . 17
           |
192 | 191 | iffalsed 3892 |
. . . . . . . . . . . . . . . 16
                |
193 | 192 | negeqd 9869 |
. . . . . . . . . . . . . . 15
                  |
194 | 193 | mpteq2dva 4489 |
. . . . . . . . . . . . . 14
 

                     |
195 | 52 | recnd 9669 |
. . . . . . . . . . . . . . . . 17
   |
196 | 195 | negcld 9973 |
. . . . . . . . . . . . . . . 16
    |
197 | 146, 196,
161 | constcncfg 37748 |
. . . . . . . . . . . . . . 15
                  |
198 | 197 | adantr 467 |
. . . . . . . . . . . . . 14
 

                 |
199 | 194, 198 | eqeltrd 2529 |
. . . . . . . . . . . . 13
 

                      |
200 | 165, 184,
199 | syl2anc 667 |
. . . . . . . . . . . 12
 
                       |
201 | 164, 200 | pm2.61dan 800 |
. . . . . . . . . . 11
                       |
202 | 148, 201 | addcncf 37750 |
. . . . . . . . . 10
          
                    |
203 | 119, 202 | eqeltrd 2529 |
. . . . . . . . 9
          
                   |
204 | | eqid 2451 |
. . . . . . . . . 10
                 |
205 | | 1cnd 9659 |
. . . . . . . . . . 11
   |
206 | 204 | cdivcncf 21949 |
. . . . . . . . . . 11
                   |
207 | 205, 206 | syl 17 |
. . . . . . . . . 10
                   |
208 | | elsn 3982 |
. . . . . . . . . . . . . 14
     |
209 | 61, 208 | sylnibr 307 |
. . . . . . . . . . . . 13
 
    
    |
210 | 111, 209 | eldifd 3415 |
. . . . . . . . . . . 12
 
    

     |
211 | 210 | ralrimiva 2802 |
. . . . . . . . . . 11
             |
212 | | dfss3 3422 |
. . . . . . . . . . 11
         
           |
213 | 211, 212 | sylibr 216 |
. . . . . . . . . 10
    
      |
214 | 9, 62 | rereccld 10434 |
. . . . . . . . . . 11
 
    
    |
215 | 214 | recnd 9669 |
. . . . . . . . . 10
 
    
    |
216 | 204, 207,
213, 161, 215 | cncfmptssg 37747 |
. . . . . . . . 9
                   |
217 | 203, 216 | mulcncf 22398 |
. . . . . . . 8
                                  |
218 | 114, 217 | eqeltrd 2529 |
. . . . . . 7
                     |
219 | 61 | iffalsed 3892 |
. . . . . . . . . 10
 
    
                           |
220 | 74 | recnd 9669 |
. . . . . . . . . . 11
 
    
          |
221 | 111, 220,
81 | divrecd 10386 |
. . . . . . . . . 10
 
    
                        |
222 | 86, 219, 221 | 3eqtrd 2489 |
. . . . . . . . 9
 
    
                  |
223 | 222 | mpteq2dva 4489 |
. . . . . . . 8
                               |
224 | 219, 221 | eqtr2d 2486 |
. . . . . . . . . 10
 
    
                             |
225 | 224 | mpteq2dva 4489 |
. . . . . . . . 9
                                          |
226 | | eqid 2451 |
. . . . . . . . . 10
    ![[,] [,]](_icc.gif)                      ![[,] [,]](_icc.gif)                   |
227 | | cncfss 21931 |
. . . . . . . . . . . 12
 
     ![[,] [,]](_icc.gif)         ![[,] [,]](_icc.gif)       |
228 | 106, 160,
227 | mp2an 678 |
. . . . . . . . . . 11
    ![[,] [,]](_icc.gif)         ![[,] [,]](_icc.gif)      |
229 | 226 | fourierdlem62 38032 |
. . . . . . . . . . . 12
    ![[,] [,]](_icc.gif)                      ![[,] [,]](_icc.gif)      |
230 | 229 | a1i 11 |
. . . . . . . . . . 11
     ![[,] [,]](_icc.gif)                      ![[,] [,]](_icc.gif)       |
231 | 228, 230 | sseldi 3430 |
. . . . . . . . . 10
     ![[,] [,]](_icc.gif)                      ![[,] [,]](_icc.gif)       |
232 | 83 | recnd 9669 |
. . . . . . . . . 10
 
    
                 |
233 | 226, 231,
41, 161, 232 | cncfmptssg 37747 |
. . . . . . . . 9
                                |
234 | 225, 233 | eqeltrd 2529 |
. . . . . . . 8
                             |
235 | 223, 234 | eqeltrd 2529 |
. . . . . . 7
                     |
236 | 218, 235 | mulcncf 22398 |
. . . . . 6
                           |
237 | 108, 236 | eqeltrd 2529 |
. . . . 5
                     |
238 | 101 | mpteq2dva 4489 |
. . . . . 6
                             |
239 | | sincn 23399 |
. . . . . . . 8
     |
240 | 239 | a1i 11 |
. . . . . . 7
       |
241 | | halfre 10828 |
. . . . . . . . . . . 12
   |
242 | 241 | a1i 11 |
. . . . . . . . . . 11
     |
243 | 93, 242 | readdcld 9670 |
. . . . . . . . . 10
       |
244 | 243 | recnd 9669 |
. . . . . . . . 9
       |
245 | 146, 244,
161 | constcncfg 37748 |
. . . . . . . 8
                     |
246 | 146, 161 | idcncfg 37749 |
. . . . . . . 8
                 |
247 | 245, 246 | mulcncf 22398 |
. . . . . . 7
                       |
248 | 240, 247 | cncfmpt1f 21945 |
. . . . . 6
                           |
249 | 238, 248 | eqeltrd 2529 |
. . . . 5
                     |
250 | 237, 249 | mulcncf 22398 |
. . . 4
                           |
251 | | cncffvrn 21930 |
. . . 4
 
                                                                             |
252 | 107, 250,
251 | syl2anc 667 |
. . 3
                                                     |
253 | 105, 252 | mpbird 236 |
. 2
                           |
254 | 43, 253 | eqeltrd 2529 |
1
                 |