Step | Hyp | Ref
| Expression |
1 | | fourierdlem15.3 |
. . . . . 6
       |
2 | | fourierdlem15.2 |
. . . . . . 7
   |
3 | | fourierdlem15.1 |
. . . . . . . 8
 
                 
 ..^                |
4 | 3 | fourierdlem2 38008 |
. . . . . . 7
 
   
                  
 ..^                 |
5 | 2, 4 | syl 17 |
. . . . . 6
                        
 ..^                 |
6 | 1, 5 | mpbid 215 |
. . . . 5
                   
 ..^                |
7 | 6 | simpld 465 |
. . . 4
         |
8 | | reex 9655 |
. . . . . 6
 |
9 | 8 | a1i 11 |
. . . . 5
   |
10 | | ovex 6342 |
. . . . . 6
     |
11 | 10 | a1i 11 |
. . . . 5
       |
12 | 9, 11 | elmapd 7511 |
. . . 4
                   |
13 | 7, 12 | mpbid 215 |
. . 3
           |
14 | | ffn 5750 |
. . 3
               |
15 | 13, 14 | syl 17 |
. 2
       |
16 | 6 | simprd 469 |
. . . . . . . . 9
            
 ..^               |
17 | 16 | simpld 465 |
. . . . . . . 8
             |
18 | 17 | simpld 465 |
. . . . . . 7
       |
19 | | nnnn0 10904 |
. . . . . . . . . . 11
   |
20 | | nn0uz 11221 |
. . . . . . . . . . 11
     |
21 | 19, 20 | syl6eleq 2549 |
. . . . . . . . . 10
       |
22 | 2, 21 | syl 17 |
. . . . . . . . 9
       |
23 | | eluzfz1 11834 |
. . . . . . . . 9
    
      |
24 | 22, 23 | syl 17 |
. . . . . . . 8
       |
25 | 13, 24 | ffvelrnd 6045 |
. . . . . . 7
       |
26 | 18, 25 | eqeltrrd 2540 |
. . . . . 6
   |
27 | 26 | adantr 471 |
. . . . 5
 
       |
28 | 17 | simprd 469 |
. . . . . . 7
       |
29 | | eluzfz2 11835 |
. . . . . . . . 9
    
      |
30 | 22, 29 | syl 17 |
. . . . . . . 8
       |
31 | 13, 30 | ffvelrnd 6045 |
. . . . . . 7
       |
32 | 28, 31 | eqeltrrd 2540 |
. . . . . 6
   |
33 | 32 | adantr 471 |
. . . . 5
 
       |
34 | 13 | ffvelrnda 6044 |
. . . . 5
 
           |
35 | 18 | eqcomd 2467 |
. . . . . . 7
       |
36 | 35 | adantr 471 |
. . . . . 6
 
           |
37 | | elfzuz 11824 |
. . . . . . . 8
           |
38 | 37 | adantl 472 |
. . . . . . 7
 
           |
39 | 13 | ad2antrr 737 |
. . . . . . . 8
                       |
40 | | elfzle1 11830 |
. . . . . . . . . . 11
       |
41 | 40 | adantl 472 |
. . . . . . . . . 10
     
       |
42 | | elfzelz 11828 |
. . . . . . . . . . . . 13
       |
43 | 42 | zred 11068 |
. . . . . . . . . . . 12
       |
44 | 43 | adantl 472 |
. . . . . . . . . . 11
     
       |
45 | | elfzelz 11828 |
. . . . . . . . . . . . 13
       |
46 | 45 | zred 11068 |
. . . . . . . . . . . 12
       |
47 | 46 | adantr 471 |
. . . . . . . . . . 11
     
       |
48 | | elfzel2 11826 |
. . . . . . . . . . . . 13
       |
49 | 48 | zred 11068 |
. . . . . . . . . . . 12
       |
50 | 49 | adantr 471 |
. . . . . . . . . . 11
     
       |
51 | | elfzle2 11831 |
. . . . . . . . . . . 12
       |
52 | 51 | adantl 472 |
. . . . . . . . . . 11
     
       |
53 | | elfzle2 11831 |
. . . . . . . . . . . 12
       |
54 | 53 | adantr 471 |
. . . . . . . . . . 11
     
       |
55 | 44, 47, 50, 52, 54 | letrd 9817 |
. . . . . . . . . 10
     
       |
56 | 42 | adantl 472 |
. . . . . . . . . . 11
     
       |
57 | | 0zd 10977 |
. . . . . . . . . . 11
     
       |
58 | 48 | adantr 471 |
. . . . . . . . . . 11
     
       |
59 | | elfz 11818 |
. . . . . . . . . . 11
 
     
     |
60 | 56, 57, 58, 59 | syl3anc 1276 |
. . . . . . . . . 10
     
          
    |
61 | 41, 55, 60 | mpbir2and 938 |
. . . . . . . . 9
     
           |
62 | 61 | adantll 725 |
. . . . . . . 8
                   |
63 | 39, 62 | ffvelrnd 6045 |
. . . . . . 7
                   |
64 | | simpll 765 |
. . . . . . . 8
                 |
65 | | elfzle1 11830 |
. . . . . . . . . . 11
         |
66 | 65 | adantl 472 |
. . . . . . . . . 10
     
         |
67 | | elfzelz 11828 |
. . . . . . . . . . . . 13
         |
68 | 67 | zred 11068 |
. . . . . . . . . . . 12
         |
69 | 68 | adantl 472 |
. . . . . . . . . . 11
     
         |
70 | 46 | adantr 471 |
. . . . . . . . . . 11
     
         |
71 | 49 | adantr 471 |
. . . . . . . . . . 11
     
         |
72 | | peano2rem 9966 |
. . . . . . . . . . . . 13
     |
73 | 70, 72 | syl 17 |
. . . . . . . . . . . 12
     
           |
74 | | elfzle2 11831 |
. . . . . . . . . . . . 13
           |
75 | 74 | adantl 472 |
. . . . . . . . . . . 12
     
           |
76 | 70 | ltm1d 10566 |
. . . . . . . . . . . 12
     
           |
77 | 69, 73, 70, 75, 76 | lelttrd 9818 |
. . . . . . . . . . 11
     
         |
78 | 53 | adantr 471 |
. . . . . . . . . . 11
     
         |
79 | 69, 70, 71, 77, 78 | ltletrd 9820 |
. . . . . . . . . 10
     
         |
80 | 67 | adantl 472 |
. . . . . . . . . . 11
     
         |
81 | | 0zd 10977 |
. . . . . . . . . . 11
     
         |
82 | 48 | adantr 471 |
. . . . . . . . . . 11
     
         |
83 | | elfzo 11952 |
. . . . . . . . . . 11
 
   ..^
     |
84 | 80, 81, 82, 83 | syl3anc 1276 |
. . . . . . . . . 10
     
         ..^ 
    |
85 | 66, 79, 84 | mpbir2and 938 |
. . . . . . . . 9
     
        ..^   |
86 | 85 | adantll 725 |
. . . . . . . 8
                ..^   |
87 | 13 | adantr 471 |
. . . . . . . . . 10
 
 ..^            |
88 | | elfzofz 11965 |
. . . . . . . . . . 11
  ..^
      |
89 | 88 | adantl 472 |
. . . . . . . . . 10
 
 ..^        |
90 | 87, 89 | ffvelrnd 6045 |
. . . . . . . . 9
 
 ..^        |
91 | | fzofzp1 12038 |
. . . . . . . . . . 11
  ..^
        |
92 | 91 | adantl 472 |
. . . . . . . . . 10
 
 ..^          |
93 | 87, 92 | ffvelrnd 6045 |
. . . . . . . . 9
 
 ..^          |
94 | | eleq1 2527 |
. . . . . . . . . . . 12
   ..^
 ..^    |
95 | 94 | anbi2d 715 |
. . . . . . . . . . 11
  
 ..^  
 ..^     |
96 | | fveq2 5887 |
. . . . . . . . . . . 12
           |
97 | | oveq1 6321 |
. . . . . . . . . . . . 13
       |
98 | 97 | fveq2d 5891 |
. . . . . . . . . . . 12
               |
99 | 96, 98 | breq12d 4428 |
. . . . . . . . . . 11
     
     
             |
100 | 95, 99 | imbi12d 326 |
. . . . . . . . . 10
   
 ..^     
      
   ..^                |
101 | 16 | simprd 469 |
. . . . . . . . . . 11
   ..^              |
102 | 101 | r19.21bi 2768 |
. . . . . . . . . 10
 
 ..^              |
103 | 100, 102 | chvarv 2117 |
. . . . . . . . 9
 
 ..^              |
104 | 90, 93, 103 | ltled 9808 |
. . . . . . . 8
 
 ..^              |
105 | 64, 86, 104 | syl2anc 671 |
. . . . . . 7
                           |
106 | 38, 63, 105 | monoord 12274 |
. . . . . 6
 
               |
107 | 36, 106 | eqbrtrd 4436 |
. . . . 5
 
           |
108 | | elfzuz3 11825 |
. . . . . . . 8
           |
109 | 108 | adantl 472 |
. . . . . . 7
 
           |
110 | 13 | ad2antrr 737 |
. . . . . . . 8
                       |
111 | | fz0fzelfz0 11925 |
. . . . . . . . 9
     
           |
112 | 111 | adantll 725 |
. . . . . . . 8
                   |
113 | 110, 112 | ffvelrnd 6045 |
. . . . . . 7
                   |
114 | 13 | ad2antrr 737 |
. . . . . . . . 9
           
             |
115 | | 0red 9669 |
. . . . . . . . . . . 12
     
         |
116 | 46 | adantr 471 |
. . . . . . . . . . . 12
     
         |
117 | | elfzelz 11828 |
. . . . . . . . . . . . . 14
         |
118 | 117 | zred 11068 |
. . . . . . . . . . . . 13
         |
119 | 118 | adantl 472 |
. . . . . . . . . . . 12
     
         |
120 | | elfzle1 11830 |
. . . . . . . . . . . . 13
       |
121 | 120 | adantr 471 |
. . . . . . . . . . . 12
     
      
  |
122 | | elfzle1 11830 |
. . . . . . . . . . . . 13
         |
123 | 122 | adantl 472 |
. . . . . . . . . . . 12
     
      
  |
124 | 115, 116,
119, 121, 123 | letrd 9817 |
. . . . . . . . . . 11
     
      
  |
125 | 124 | adantll 725 |
. . . . . . . . . 10
           
     |
126 | 118 | adantl 472 |
. . . . . . . . . . . 12
 
   
     |
127 | 2 | nnred 10651 |
. . . . . . . . . . . . 13
   |
128 | 127 | adantr 471 |
. . . . . . . . . . . 12
 
   
     |
129 | | 1red 9683 |
. . . . . . . . . . . . . 14
 
   
     |
130 | 128, 129 | resubcld 10074 |
. . . . . . . . . . . . 13
 
   
   
   |
131 | | elfzle2 11831 |
. . . . . . . . . . . . . 14
           |
132 | 131 | adantl 472 |
. . . . . . . . . . . . 13
 
   
       |
133 | 128 | ltm1d 10566 |
. . . . . . . . . . . . 13
 
   
   
   |
134 | 126, 130,
128, 132, 133 | lelttrd 9818 |
. . . . . . . . . . . 12
 
   
     |
135 | 126, 128,
134 | ltled 9808 |
. . . . . . . . . . 11
 
   
     |
136 | 135 | adantlr 726 |
. . . . . . . . . 10
           
     |
137 | 117 | adantl 472 |
. . . . . . . . . . 11
           
     |
138 | | 0zd 10977 |
. . . . . . . . . . 11
           
     |
139 | 48 | ad2antlr 738 |
. . . . . . . . . . 11
           
     |
140 | 137, 138,
139, 59 | syl3anc 1276 |
. . . . . . . . . 10
           
       
     |
141 | 125, 136,
140 | mpbir2and 938 |
. . . . . . . . 9
           
         |
142 | 114, 141 | ffvelrnd 6045 |
. . . . . . . 8
           
         |
143 | 118 | adantl 472 |
. . . . . . . . . . 11
           
     |
144 | | 1red 9683 |
. . . . . . . . . . 11
           
     |
145 | | 0le1 10164 |
. . . . . . . . . . . 12
 |
146 | 145 | a1i 11 |
. . . . . . . . . . 11
           
     |
147 | 143, 144,
125, 146 | addge0d 10216 |
. . . . . . . . . 10
           
       |
148 | 126, 130,
129, 132 | leadd1dd 10254 |
. . . . . . . . . . . 12
 
   
           |
149 | 2 | nncnd 10652 |
. . . . . . . . . . . . . 14
   |
150 | 149 | adantr 471 |
. . . . . . . . . . . . 13
 
   
     |
151 | | 1cnd 9684 |
. . . . . . . . . . . . 13
 
   
     |
152 | 150, 151 | npcand 10015 |
. . . . . . . . . . . 12
 
   
         |
153 | 148, 152 | breqtrd 4440 |
. . . . . . . . . . 11
 
   
       |
154 | 153 | adantlr 726 |
. . . . . . . . . 10
           
       |
155 | 137 | peano2zd 11071 |
. . . . . . . . . . 11
           
       |
156 | | elfz 11818 |
. . . . . . . . . . 11
   
       
         |
157 | 155, 138,
139, 156 | syl3anc 1276 |
. . . . . . . . . 10
           
         
         |
158 | 147, 154,
157 | mpbir2and 938 |
. . . . . . . . 9
           
           |
159 | 114, 158 | ffvelrnd 6045 |
. . . . . . . 8
           
           |
160 | | simpll 765 |
. . . . . . . . 9
           
     |
161 | 134 | adantlr 726 |
. . . . . . . . . 10
           
     |
162 | 137, 138,
139, 83 | syl3anc 1276 |
. . . . . . . . . 10
           
     ..^
     |
163 | 125, 161,
162 | mpbir2and 938 |
. . . . . . . . 9
           
    ..^   |
164 | 160, 163,
103 | syl2anc 671 |
. . . . . . . 8
           
               |
165 | 142, 159,
164 | ltled 9808 |
. . . . . . 7
           
               |
166 | 109, 113,
165 | monoord 12274 |
. . . . . 6
 
               |
167 | 28 | adantr 471 |
. . . . . 6
 
           |
168 | 166, 167 | breqtrd 4440 |
. . . . 5
 
           |
169 | 27, 33, 34, 107, 168 | eliccd 37638 |
. . . 4
 
           ![[,] [,]](_icc.gif)    |
170 | 169 | ralrimiva 2813 |
. . 3
             ![[,] [,]](_icc.gif)    |
171 | | fnfvrnss 6073 |
. . 3
                  ![[,] [,]](_icc.gif)  
  ![[,] [,]](_icc.gif)    |
172 | 15, 170, 171 | syl2anc 671 |
. 2
   ![[,] [,]](_icc.gif)    |
173 | | df-f 5604 |
. 2
           ![[,] [,]](_icc.gif) 
    
  ![[,] [,]](_icc.gif)     |
174 | 15, 172, 173 | sylanbrc 675 |
1
           ![[,] [,]](_icc.gif)    |