Proof of Theorem fourierdlem57
Step | Hyp | Ref
| Expression |
1 | | fourierdlem57.fdv |
. . . . . . . . . 10
                           |
2 | 1 | adantr 467 |
. . . . . . . . 9
 
    
                          |
3 | | fourierdlem57.xre |
. . . . . . . . . . . . 13
   |
4 | | fourierdlem57.a |
. . . . . . . . . . . . 13
   |
5 | 3, 4 | readdcld 9667 |
. . . . . . . . . . . 12
     |
6 | 5 | rexrd 9687 |
. . . . . . . . . . 11
     |
7 | 6 | adantr 467 |
. . . . . . . . . 10
 
    
    |
8 | | fourierdlem57.b |
. . . . . . . . . . . . 13
   |
9 | 3, 8 | readdcld 9667 |
. . . . . . . . . . . 12
     |
10 | 9 | rexrd 9687 |
. . . . . . . . . . 11
     |
11 | 10 | adantr 467 |
. . . . . . . . . 10
 
    
    |
12 | 3 | adantr 467 |
. . . . . . . . . . 11
 
    
  |
13 | | elioore 11663 |
. . . . . . . . . . . 12
       |
14 | 13 | adantl 468 |
. . . . . . . . . . 11
 
    
  |
15 | 12, 14 | readdcld 9667 |
. . . . . . . . . 10
 
    
    |
16 | 4 | adantr 467 |
. . . . . . . . . . 11
 
    
  |
17 | 16 | rexrd 9687 |
. . . . . . . . . . . 12
 
    
  |
18 | 8 | rexrd 9687 |
. . . . . . . . . . . . 13
   |
19 | 18 | adantr 467 |
. . . . . . . . . . . 12
 
    
  |
20 | | simpr 463 |
. . . . . . . . . . . 12
 
    
      |
21 | | ioogtlb 37586 |
. . . . . . . . . . . 12
         |
22 | 17, 19, 20, 21 | syl3anc 1267 |
. . . . . . . . . . 11
 
    
  |
23 | 16, 14, 12, 22 | ltadd2dd 9791 |
. . . . . . . . . 10
 
    
  
   |
24 | 8 | adantr 467 |
. . . . . . . . . . 11
 
    
  |
25 | | iooltub 37604 |
. . . . . . . . . . . 12
         |
26 | 17, 19, 20, 25 | syl3anc 1267 |
. . . . . . . . . . 11
 
    
  |
27 | 14, 24, 12, 26 | ltadd2dd 9791 |
. . . . . . . . . 10
 
    
      |
28 | 7, 11, 15, 23, 27 | eliood 37589 |
. . . . . . . . 9
 
    
       
    |
29 | 2, 28 | ffvelrnd 6021 |
. . . . . . . 8
 
    
        
      
    |
30 | | 2re 10676 |
. . . . . . . . . 10
 |
31 | 30 | a1i 11 |
. . . . . . . . 9
 
    
  |
32 | | rehalfcl 10836 |
. . . . . . . . . . 11
     |
33 | 14, 32 | syl 17 |
. . . . . . . . . 10
 
    
    |
34 | 33 | resincld 14190 |
. . . . . . . . 9
 
    
        |
35 | 31, 34 | remulcld 9668 |
. . . . . . . 8
 
    
          |
36 | 29, 35 | remulcld 9668 |
. . . . . . 7
 
    
                              |
37 | 33 | recoscld 14191 |
. . . . . . . 8
 
    
        |
38 | | fourierdlem57.f |
. . . . . . . . . . 11
       |
39 | 38 | adantr 467 |
. . . . . . . . . 10
 
    
      |
40 | 39, 15 | ffvelrnd 6021 |
. . . . . . . . 9
 
    
        |
41 | | fourierdlem57.c |
. . . . . . . . . 10
   |
42 | 41 | adantr 467 |
. . . . . . . . 9
 
    
  |
43 | 40, 42 | resubcld 10044 |
. . . . . . . 8
 
    
          |
44 | 37, 43 | remulcld 9668 |
. . . . . . 7
 
    
           
      |
45 | 36, 44 | resubcld 10044 |
. . . . . 6
 
    
    
                                           |
46 | 35 | resqcld 12439 |
. . . . . 6
 
    
              |
47 | | 2cnd 10679 |
. . . . . . . . 9
   |
48 | 32 | recnd 9666 |
. . . . . . . . . 10
     |
49 | 48 | sincld 14177 |
. . . . . . . . 9
         |
50 | 47, 49 | mulcld 9660 |
. . . . . . . 8
           |
51 | 14, 50 | syl 17 |
. . . . . . 7
 
    
          |
52 | | 2cnd 10679 |
. . . . . . . 8
 
    
  |
53 | 14, 49 | syl 17 |
. . . . . . . 8
 
    
        |
54 | | 2ne0 10699 |
. . . . . . . . 9
 |
55 | 54 | a1i 11 |
. . . . . . . 8
 
    
  |
56 | | fourierdlem57.ab |
. . . . . . . . . 10
    
   ![[,] [,]](_icc.gif)    |
57 | 56 | sselda 3431 |
. . . . . . . . 9
 
    
   ![[,] [,]](_icc.gif)    |
58 | | eqcom 2457 |
. . . . . . . . . . . . . . 15

  |
59 | 58 | biimpi 198 |
. . . . . . . . . . . . . 14
   |
60 | 59 | adantl 468 |
. . . . . . . . . . . . 13
     
   |
61 | | simpl 459 |
. . . . . . . . . . . . 13
     
       |
62 | 60, 61 | eqeltrd 2528 |
. . . . . . . . . . . 12
     
       |
63 | 62 | adantll 719 |
. . . . . . . . . . 11
               |
64 | | fourierdlem57.n0 |
. . . . . . . . . . . 12
       |
65 | 64 | ad2antrr 731 |
. . . . . . . . . . 11
        
      |
66 | 63, 65 | pm2.65da 579 |
. . . . . . . . . 10
 
    
  |
67 | 66 | neqned 2630 |
. . . . . . . . 9
 
    
  |
68 | | fourierdlem44 38009 |
. . . . . . . . 9
     ![[,] [,]](_icc.gif)           |
69 | 57, 67, 68 | syl2anc 666 |
. . . . . . . 8
 
    
        |
70 | 52, 53, 55, 69 | mulne0d 10261 |
. . . . . . 7
 
    
          |
71 | | 2z 10966 |
. . . . . . . 8
 |
72 | 71 | a1i 11 |
. . . . . . 7
 
    
  |
73 | 51, 70, 72 | expne0d 12419 |
. . . . . 6
 
    
              |
74 | 45, 46, 73 | redivcld 10432 |
. . . . 5
 
    
           
      
                      
                    |
75 | | eqid 2450 |
. . . . 5
                
      
                      
                                   
      
                      
                    |
76 | 74, 75 | fmptd 6044 |
. . . 4
                                                                             |
77 | | fourierdlem57.o |
. . . . . . . 8
                         |
78 | 77 | a1i 11 |
. . . . . . 7
           
               |
79 | 78 | oveq2d 6304 |
. . . . . 6
                               |
80 | | reelprrecn 9628 |
. . . . . . . 8
    |
81 | 80 | a1i 11 |
. . . . . . 7
      |
82 | 43 | recnd 9666 |
. . . . . . 7
 
    
          |
83 | 40 | recnd 9666 |
. . . . . . . . 9
 
    
        |
84 | | eqid 2450 |
. . . . . . . . . 10
       
                 |
85 | 38, 3, 4, 8, 84, 1 | fourierdlem28 37991 |
. . . . . . . . 9
                                         |
86 | 42 | recnd 9666 |
. . . . . . . . 9
 
    
  |
87 | | 0red 9641 |
. . . . . . . . 9
 
    
  |
88 | | iooretop 21779 |
. . . . . . . . . . . 12
         |
89 | | eqid 2450 |
. . . . . . . . . . . . 13
  ℂfld   ℂfld |
90 | 89 | tgioo2 21814 |
. . . . . . . . . . . 12
       ℂfld
↾t   |
91 | 88, 90 | eleqtri 2526 |
. . . . . . . . . . 11
       ℂfld
↾t   |
92 | 91 | a1i 11 |
. . . . . . . . . 10
        ℂfld ↾t    |
93 | 41 | recnd 9666 |
. . . . . . . . . 10
   |
94 | 81, 92, 93 | dvmptconst 37779 |
. . . . . . . . 9
                 |
95 | 81, 83, 29, 85, 86, 87, 94 | dvmptsub 22914 |
. . . . . . . 8
           
             
                   |
96 | 29 | recnd 9666 |
. . . . . . . . . 10
 
    
        
      
    |
97 | 96 | subid1d 9972 |
. . . . . . . . 9
 
    
                                        |
98 | 97 | mpteq2dva 4488 |
. . . . . . . 8
               
      
                              |
99 | 95, 98 | eqtrd 2484 |
. . . . . . 7
           
                               |
100 | | eldifsn 4096 |
. . . . . . . 8
            
                    |
101 | 51, 70, 100 | sylanbrc 669 |
. . . . . . 7
 
    
              |
102 | | recn 9626 |
. . . . . . . . . . . . 13
   |
103 | 54 | a1i 11 |
. . . . . . . . . . . . 13
   |
104 | 102, 47, 103 | divrec2d 10384 |
. . . . . . . . . . . 12
         |
105 | 104 | eqcomd 2456 |
. . . . . . . . . . 11
         |
106 | 13, 105 | syl 17 |
. . . . . . . . . 10
             |
107 | 106 | fveq2d 5867 |
. . . . . . . . 9
                     |
108 | | halfcn 10826 |
. . . . . . . . . . . . 13
   |
109 | 108 | a1i 11 |
. . . . . . . . . . . 12
     |
110 | | id 22 |
. . . . . . . . . . . 12
   |
111 | 109, 110 | mulcld 9660 |
. . . . . . . . . . 11
       |
112 | 111 | coscld 14178 |
. . . . . . . . . 10
           |
113 | 13, 102, 112 | 3syl 18 |
. . . . . . . . 9
               |
114 | 107, 113 | eqeltrrd 2529 |
. . . . . . . 8
             |
115 | 114 | adantl 468 |
. . . . . . 7
 
    
        |
116 | | ioossre 11693 |
. . . . . . . . . . . . 13
     |
117 | | resmpt 5153 |
. . . . . . . . . . . . 13
    
                                |
118 | 116, 117 | ax-mp 5 |
. . . . . . . . . . . 12
                               |
119 | 118 | eqcomi 2459 |
. . . . . . . . . . 11
                               |
120 | 119 | oveq2i 6299 |
. . . . . . . . . 10
                                   |
121 | | ax-resscn 9593 |
. . . . . . . . . . 11
 |
122 | | eqid 2450 |
. . . . . . . . . . . 12
                     |
123 | 122, 50 | fmpti 6043 |
. . . . . . . . . . 11
               |
124 | | ssid 3450 |
. . . . . . . . . . 11
 |
125 | 89, 90 | dvres 22859 |
. . . . . . . . . . 11
                                                       
                   |
126 | 121, 123,
124, 116, 125 | mp4an 678 |
. . . . . . . . . 10
                              
                  |
127 | | resmpt 5153 |
. . . . . . . . . . . . . . 15

                            |
128 | 121, 127 | ax-mp 5 |
. . . . . . . . . . . . . 14
                           |
129 | 105 | fveq2d 5867 |
. . . . . . . . . . . . . . . 16
                 |
130 | 129 | oveq2d 6304 |
. . . . . . . . . . . . . . 15
                     |
131 | 130 | mpteq2ia 4484 |
. . . . . . . . . . . . . 14
                       |
132 | 128, 131 | eqtr2i 2473 |
. . . . . . . . . . . . 13
                         |
133 | 132 | oveq2i 6299 |
. . . . . . . . . . . 12
                             |
134 | | ioontr 37605 |
. . . . . . . . . . . 12
                     |
135 | 133, 134 | reseq12i 5102 |
. . . . . . . . . . 11
                   
                                 |
136 | | eqid 2450 |
. . . . . . . . . . . . . 14
                         |
137 | | 2cnd 10679 |
. . . . . . . . . . . . . . 15
   |
138 | 111 | sincld 14177 |
. . . . . . . . . . . . . . 15
           |
139 | 137, 138 | mulcld 9660 |
. . . . . . . . . . . . . 14
             |
140 | 136, 139 | fmpti 6043 |
. . . . . . . . . . . . 13
                 |
141 | | ssid 3450 |
. . . . . . . . . . . . 13
 |
142 | | dmmptg 5331 |
. . . . . . . . . . . . . . . 16
 
             
                  |
143 | | 2cn 10677 |
. . . . . . . . . . . . . . . . . . 19
 |
144 | 143, 108 | mulcli 9645 |
. . . . . . . . . . . . . . . . . 18
     |
145 | 144 | a1i 11 |
. . . . . . . . . . . . . . . . 17
       |
146 | 145, 112 | mulcld 9660 |
. . . . . . . . . . . . . . . 16
                 |
147 | 142, 146 | mprg 2750 |
. . . . . . . . . . . . . . 15
                 |
148 | 121, 147 | sseqtr4i 3464 |
. . . . . . . . . . . . . 14
                 |
149 | | dvasinbx 37786 |
. . . . . . . . . . . . . . . 16
                                     |
150 | 143, 108,
149 | mp2an 677 |
. . . . . . . . . . . . . . 15
                               |
151 | 150 | dmeqi 5035 |
. . . . . . . . . . . . . 14
                               |
152 | 148, 151 | sseqtr4i 3464 |
. . . . . . . . . . . . 13
               |
153 | | dvres3 22861 |
. . . . . . . . . . . . 13
    
                   
                            
                    |
154 | 80, 140, 141, 152, 153 | mp4an 678 |
. . . . . . . . . . . 12
                              
  |
155 | 154 | reseq1i 5100 |
. . . . . . . . . . 11
                                     
       |
156 | 150 | reseq1i 5100 |
. . . . . . . . . . . . 13
                                
  |
157 | 156 | reseq1i 5100 |
. . . . . . . . . . . 12
               
                        
      |
158 | | resabs1 5132 |
. . . . . . . . . . . . 13
    
                 
                      
       |
159 | 116, 158 | ax-mp 5 |
. . . . . . . . . . . 12
                 
                      
      |
160 | | ioosscn 37585 |
. . . . . . . . . . . . 13
     |
161 | | resmpt 5153 |
. . . . . . . . . . . . 13
    
                                            |
162 | 160, 161 | ax-mp 5 |
. . . . . . . . . . . 12
                                           |
163 | 157, 159,
162 | 3eqtri 2476 |
. . . . . . . . . . 11
               
                           |
164 | 135, 155,
163 | 3eqtri 2476 |
. . . . . . . . . 10
                   
                               |
165 | 120, 126,
164 | 3eqtri 2476 |
. . . . . . . . 9
                                     |
166 | 143, 54 | recidi 10335 |
. . . . . . . . . . . . 13
     |
167 | 166 | oveq1i 6298 |
. . . . . . . . . . . 12
                         |
168 | 167 | a1i 11 |
. . . . . . . . . . 11
                               |
169 | 113 | mulid2d 9658 |
. . . . . . . . . . 11
                         |
170 | 168, 169,
107 | 3eqtrd 2488 |
. . . . . . . . . 10
                           |
171 | 170 | mpteq2ia 4484 |
. . . . . . . . 9
                                 |
172 | 165, 171 | eqtri 2472 |
. . . . . . . 8
                             |
173 | 172 | a1i 11 |
. . . . . . 7
                               |
174 | 81, 82, 29, 99, 101, 115, 173 | dvmptdiv 37783 |
. . . . . 6
            
                              
      
                      
                     |
175 | 79, 174 | eqtrd 2484 |
. . . . 5
                   
      
                      
                     |
176 | 175 | feq1d 5712 |
. . . 4
                      
                                                                  |
177 | 76, 176 | mpbird 236 |
. . 3
             |
178 | 177, 175 | jca 535 |
. 2
                                                                                   |
179 | 178, 172 | pm3.2i 457 |
1
                                                                                                                 |