| Step | 
						Hyp | 
						Ref | 
						Expression | 
					
						
							| 1 | 
							
								
							 | 
							fourierdlem103.f | 
							   | 
						
						
							| 2 | 
							
								
							 | 
							fourierdlem103.xre | 
							   | 
						
						
							| 3 | 
							
								
							 | 
							fourierdlem103.p | 
							   | 
						
						
							| 4 | 
							
								
							 | 
							fourierdlem103.m | 
							   | 
						
						
							| 5 | 
							
								
							 | 
							fourierdlem103.v | 
							   | 
						
						
							| 6 | 
							
								
							 | 
							fourierdlem103.x | 
							   | 
						
						
							| 7 | 
							
								
							 | 
							fourierdlem103.fcn | 
							   | 
						
						
							| 8 | 
							
								
							 | 
							fourierdlem103.fbdioo | 
							   | 
						
						
							| 9 | 
							
								
							 | 
							fourierdlem103.fdvcn | 
							   | 
						
						
							| 10 | 
							
								
							 | 
							fourierdlem103.fdvbd | 
							   | 
						
						
							| 11 | 
							
								
							 | 
							fourierdlem103.r | 
							   | 
						
						
							| 12 | 
							
								
							 | 
							fourierdlem103.l | 
							   | 
						
						
							| 13 | 
							
								
							 | 
							fourierdlem103.h | 
							   | 
						
						
							| 14 | 
							
								
							 | 
							fourierdlem103.k | 
							   | 
						
						
							| 15 | 
							
								
							 | 
							fourierdlem103.u | 
							   | 
						
						
							| 16 | 
							
								
							 | 
							fourierdlem103.s | 
							   | 
						
						
							| 17 | 
							
								
							 | 
							fourierdlem103.g | 
							   | 
						
						
							| 18 | 
							
								
							 | 
							fourierdlem103.z | 
							   | 
						
						
							| 19 | 
							
								
							 | 
							fourierdlem103.e | 
							   | 
						
						
							| 20 | 
							
								
							 | 
							fourierdlem103.y | 
							   | 
						
						
							| 21 | 
							
								
							 | 
							fourierdlem103.w | 
							   | 
						
						
							| 22 | 
							
								
							 | 
							fourierdlem103.a | 
							   | 
						
						
							| 23 | 
							
								
							 | 
							fourierdlem103.b | 
							   | 
						
						
							| 24 | 
							
								
							 | 
							fourierdlem103.d | 
							   | 
						
						
							| 25 | 
							
								
							 | 
							fourierdlem103.o | 
							   | 
						
						
							| 26 | 
							
								
							 | 
							fourierdlem103.t | 
							   | 
						
						
							| 27 | 
							
								
							 | 
							fourierdlem103.n | 
							   | 
						
						
							| 28 | 
							
								
							 | 
							fourierdlem103.j | 
							   | 
						
						
							| 29 | 
							
								
							 | 
							fourierdlem103.q | 
							   | 
						
						
							| 30 | 
							
								
							 | 
							fourierdlem103.1 | 
							   | 
						
						
							| 31 | 
							
								
							 | 
							fourierdlem103.ch | 
							   | 
						
						
							| 32 | 
							
								
							 | 
							eqid | 
							   | 
						
						
							| 33 | 
							
								
							 | 
							1zzd | 
							   | 
						
						
							| 34 | 
							
								
							 | 
							nfv | 
							   | 
						
						
							| 35 | 
							
								
							 | 
							nfmpt1 | 
							   | 
						
						
							| 36 | 
							
								
							 | 
							nfmpt1 | 
							   | 
						
						
							| 37 | 
							
								
							 | 
							nfmpt1 | 
							   | 
						
						
							| 38 | 
							
								19 37
							 | 
							nfcxfr | 
							   | 
						
						
							| 39 | 
							
								
							 | 
							nnuz | 
							   | 
						
						
							| 40 | 
							
								
							 | 
							pire | 
							   | 
						
						
							| 41 | 
							
								40
							 | 
							renegcli | 
							   | 
						
						
							| 42 | 
							
								41
							 | 
							a1i | 
							   | 
						
						
							| 43 | 
							
								
							 | 
							elioore | 
							   | 
						
						
							| 44 | 
							
								43
							 | 
							adantl | 
							   | 
						
						
							| 45 | 
							
								
							 | 
							ioossre | 
							   | 
						
						
							| 46 | 
							
								45
							 | 
							a1i | 
							   | 
						
						
							| 47 | 
							
								1 46
							 | 
							fssresd | 
							   | 
						
						
							| 48 | 
							
								
							 | 
							ioosscn | 
							   | 
						
						
							| 49 | 
							
								48
							 | 
							a1i | 
							   | 
						
						
							| 50 | 
							
								
							 | 
							eqid | 
							   | 
						
						
							| 51 | 
							
								
							 | 
							pnfxr | 
							   | 
						
						
							| 52 | 
							
								51
							 | 
							a1i | 
							   | 
						
						
							| 53 | 
							
								2
							 | 
							ltpnfd | 
							   | 
						
						
							| 54 | 
							
								50 52 2 53
							 | 
							lptioo1cn | 
							   | 
						
						
							| 55 | 
							
								47 49 54 20
							 | 
							limcrecl | 
							   | 
						
						
							| 56 | 
							
								
							 | 
							ioossre | 
							   | 
						
						
							| 57 | 
							
								56
							 | 
							a1i | 
							   | 
						
						
							| 58 | 
							
								1 57
							 | 
							fssresd | 
							   | 
						
						
							| 59 | 
							
								
							 | 
							ioosscn | 
							   | 
						
						
							| 60 | 
							
								59
							 | 
							a1i | 
							   | 
						
						
							| 61 | 
							
								
							 | 
							mnfxr | 
							   | 
						
						
							| 62 | 
							
								61
							 | 
							a1i | 
							   | 
						
						
							| 63 | 
							
								2
							 | 
							mnfltd | 
							   | 
						
						
							| 64 | 
							
								50 62 2 63
							 | 
							lptioo2cn | 
							   | 
						
						
							| 65 | 
							
								58 60 64 21
							 | 
							limcrecl | 
							   | 
						
						
							| 66 | 
							
								1 2 55 65 13 14 15
							 | 
							fourierdlem55 | 
							   | 
						
						
							| 67 | 
							
								
							 | 
							ax-resscn | 
							   | 
						
						
							| 68 | 
							
								67
							 | 
							a1i | 
							   | 
						
						
							| 69 | 
							
								66 68
							 | 
							fssd | 
							   | 
						
						
							| 70 | 
							
								69
							 | 
							adantr | 
							   | 
						
						
							| 71 | 
							
								41
							 | 
							a1i | 
							   | 
						
						
							| 72 | 
							
								40
							 | 
							a1i | 
							   | 
						
						
							| 73 | 
							
								71
							 | 
							leidd | 
							   | 
						
						
							| 74 | 
							
								
							 | 
							0red | 
							   | 
						
						
							| 75 | 
							
								41
							 | 
							rexri | 
							   | 
						
						
							| 76 | 
							
								
							 | 
							0xr | 
							   | 
						
						
							| 77 | 
							
								
							 | 
							iooltub | 
							   | 
						
						
							| 78 | 
							
								75 76 77
							 | 
							mp3an12 | 
							   | 
						
						
							| 79 | 
							
								
							 | 
							pipos | 
							   | 
						
						
							| 80 | 
							
								79
							 | 
							a1i | 
							   | 
						
						
							| 81 | 
							
								43 74 72 78 80
							 | 
							lttrd | 
							   | 
						
						
							| 82 | 
							
								43 72 81
							 | 
							ltled | 
							   | 
						
						
							| 83 | 
							
								
							 | 
							iccss | 
							   | 
						
						
							| 84 | 
							
								71 72 73 82 83
							 | 
							syl22anc | 
							   | 
						
						
							| 85 | 
							
								84
							 | 
							adantl | 
							   | 
						
						
							| 86 | 
							
								70 85
							 | 
							fssresd | 
							   | 
						
						
							| 87 | 
							
								25
							 | 
							a1i | 
							   | 
						
						
							| 88 | 
							
								87
							 | 
							feq1d | 
							   | 
						
						
							| 89 | 
							
								86 88
							 | 
							mpbird | 
							   | 
						
						
							| 90 | 
							
								41
							 | 
							elexi | 
							   | 
						
						
							| 91 | 
							
								90
							 | 
							prid1 | 
							   | 
						
						
							| 92 | 
							
								
							 | 
							elun1 | 
							   | 
						
						
							| 93 | 
							
								91 92
							 | 
							ax-mp | 
							   | 
						
						
							| 94 | 
							
								93 26
							 | 
							eleqtrri | 
							   | 
						
						
							| 95 | 
							
								94
							 | 
							ne0ii | 
							   | 
						
						
							| 96 | 
							
								95
							 | 
							a1i | 
							   | 
						
						
							| 97 | 
							
								
							 | 
							prfi | 
							   | 
						
						
							| 98 | 
							
								97
							 | 
							a1i | 
							   | 
						
						
							| 99 | 
							
								
							 | 
							fzfi | 
							   | 
						
						
							| 100 | 
							
								29
							 | 
							rnmptfi | 
							   | 
						
						
							| 101 | 
							
								99 100
							 | 
							ax-mp | 
							   | 
						
						
							| 102 | 
							
								101
							 | 
							a1i | 
							   | 
						
						
							| 103 | 
							
								
							 | 
							infi | 
							   | 
						
						
							| 104 | 
							
								102 103
							 | 
							syl | 
							   | 
						
						
							| 105 | 
							
								
							 | 
							unfi | 
							   | 
						
						
							| 106 | 
							
								98 104 105
							 | 
							syl2anc | 
							   | 
						
						
							| 107 | 
							
								26 106
							 | 
							eqeltrid | 
							   | 
						
						
							| 108 | 
							
								
							 | 
							hashnncl | 
							   | 
						
						
							| 109 | 
							
								107 108
							 | 
							syl | 
							   | 
						
						
							| 110 | 
							
								96 109
							 | 
							mpbird | 
							   | 
						
						
							| 111 | 
							
								
							 | 
							nnm1nn0 | 
							   | 
						
						
							| 112 | 
							
								110 111
							 | 
							syl | 
							   | 
						
						
							| 113 | 
							
								27 112
							 | 
							eqeltrid | 
							   | 
						
						
							| 114 | 
							
								113
							 | 
							adantr | 
							   | 
						
						
							| 115 | 
							
								
							 | 
							0red | 
							   | 
						
						
							| 116 | 
							
								
							 | 
							1red | 
							   | 
						
						
							| 117 | 
							
								114
							 | 
							nn0red | 
							   | 
						
						
							| 118 | 
							
								
							 | 
							0lt1 | 
							   | 
						
						
							| 119 | 
							
								118
							 | 
							a1i | 
							   | 
						
						
							| 120 | 
							
								
							 | 
							2re | 
							   | 
						
						
							| 121 | 
							
								120
							 | 
							a1i | 
							   | 
						
						
							| 122 | 
							
								110
							 | 
							nnred | 
							   | 
						
						
							| 123 | 
							
								122
							 | 
							adantr | 
							   | 
						
						
							| 124 | 
							
								
							 | 
							ioogtlb | 
							   | 
						
						
							| 125 | 
							
								75 76 124
							 | 
							mp3an12 | 
							   | 
						
						
							| 126 | 
							
								71 125
							 | 
							ltned | 
							   | 
						
						
							| 127 | 
							
								126
							 | 
							adantl | 
							   | 
						
						
							| 128 | 
							
								
							 | 
							hashprg | 
							   | 
						
						
							| 129 | 
							
								42 44 128
							 | 
							syl2anc | 
							   | 
						
						
							| 130 | 
							
								127 129
							 | 
							mpbid | 
							   | 
						
						
							| 131 | 
							
								130
							 | 
							eqcomd | 
							   | 
						
						
							| 132 | 
							
								107
							 | 
							adantr | 
							   | 
						
						
							| 133 | 
							
								
							 | 
							ssun1 | 
							   | 
						
						
							| 134 | 
							
								133 26
							 | 
							sseqtrri | 
							   | 
						
						
							| 135 | 
							
								
							 | 
							hashssle | 
							   | 
						
						
							| 136 | 
							
								132 134 135
							 | 
							sylancl | 
							   | 
						
						
							| 137 | 
							
								131 136
							 | 
							eqbrtrd | 
							   | 
						
						
							| 138 | 
							
								121 123 116 137
							 | 
							lesub1dd | 
							   | 
						
						
							| 139 | 
							
								
							 | 
							1e2m1 | 
							   | 
						
						
							| 140 | 
							
								138 139 27
							 | 
							3brtr4g | 
							   | 
						
						
							| 141 | 
							
								115 116 117 119 140
							 | 
							ltletrd | 
							   | 
						
						
							| 142 | 
							
								141
							 | 
							gt0ne0d | 
							   | 
						
						
							| 143 | 
							
								114 142
							 | 
							jca | 
							   | 
						
						
							| 144 | 
							
								
							 | 
							elnnne0 | 
							   | 
						
						
							| 145 | 
							
								143 144
							 | 
							sylibr | 
							   | 
						
						
							| 146 | 
							
								73
							 | 
							adantl | 
							   | 
						
						
							| 147 | 
							
								71 43 125
							 | 
							ltled | 
							   | 
						
						
							| 148 | 
							
								147
							 | 
							adantl | 
							   | 
						
						
							| 149 | 
							
								42 44 42 146 148
							 | 
							eliccd | 
							   | 
						
						
							| 150 | 
							
								44
							 | 
							leidd | 
							   | 
						
						
							| 151 | 
							
								42 44 44 148 150
							 | 
							eliccd | 
							   | 
						
						
							| 152 | 
							
								149 151
							 | 
							jca | 
							   | 
						
						
							| 153 | 
							
								
							 | 
							vex | 
							   | 
						
						
							| 154 | 
							
								90 153
							 | 
							prss | 
							   | 
						
						
							| 155 | 
							
								152 154
							 | 
							sylib | 
							   | 
						
						
							| 156 | 
							
								
							 | 
							inss2 | 
							   | 
						
						
							| 157 | 
							
								156
							 | 
							a1i | 
							   | 
						
						
							| 158 | 
							
								
							 | 
							ioossicc | 
							   | 
						
						
							| 159 | 
							
								157 158
							 | 
							sstrdi | 
							   | 
						
						
							| 160 | 
							
								155 159
							 | 
							unssd | 
							   | 
						
						
							| 161 | 
							
								26 160
							 | 
							eqsstrid | 
							   | 
						
						
							| 162 | 
							
								94
							 | 
							a1i | 
							   | 
						
						
							| 163 | 
							
								153
							 | 
							prid2 | 
							   | 
						
						
							| 164 | 
							
								
							 | 
							elun1 | 
							   | 
						
						
							| 165 | 
							
								163 164
							 | 
							ax-mp | 
							   | 
						
						
							| 166 | 
							
								165 26
							 | 
							eleqtrri | 
							   | 
						
						
							| 167 | 
							
								166
							 | 
							a1i | 
							   | 
						
						
							| 168 | 
							
								132 27 28 42 44 161 162 167
							 | 
							fourierdlem52 | 
							   | 
						
						
							| 169 | 
							
								168
							 | 
							simpld | 
							   | 
						
						
							| 170 | 
							
								169
							 | 
							simpld | 
							   | 
						
						
							| 171 | 
							
								169
							 | 
							simprd | 
							   | 
						
						
							| 172 | 
							
								168
							 | 
							simprd | 
							   | 
						
						
							| 173 | 
							
								
							 | 
							elfzoelz | 
							   | 
						
						
							| 174 | 
							
								173
							 | 
							zred | 
							   | 
						
						
							| 175 | 
							
								174
							 | 
							adantl | 
							   | 
						
						
							| 176 | 
							
								175
							 | 
							ltp1d | 
							   | 
						
						
							| 177 | 
							
								71 43
							 | 
							jca | 
							   | 
						
						
							| 178 | 
							
								90 153
							 | 
							prss | 
							   | 
						
						
							| 179 | 
							
								177 178
							 | 
							sylib | 
							   | 
						
						
							| 180 | 
							
								179
							 | 
							adantl | 
							   | 
						
						
							| 181 | 
							
								
							 | 
							ioossre | 
							   | 
						
						
							| 182 | 
							
								156 181
							 | 
							sstri | 
							   | 
						
						
							| 183 | 
							
								182
							 | 
							a1i | 
							   | 
						
						
							| 184 | 
							
								180 183
							 | 
							unssd | 
							   | 
						
						
							| 185 | 
							
								26 184
							 | 
							eqsstrid | 
							   | 
						
						
							| 186 | 
							
								132 185 28 27
							 | 
							fourierdlem36 | 
							   | 
						
						
							| 187 | 
							
								186
							 | 
							adantr | 
							   | 
						
						
							| 188 | 
							
								
							 | 
							elfzofz | 
							   | 
						
						
							| 189 | 
							
								188
							 | 
							adantl | 
							   | 
						
						
							| 190 | 
							
								
							 | 
							fzofzp1 | 
							   | 
						
						
							| 191 | 
							
								190
							 | 
							adantl | 
							   | 
						
						
							| 192 | 
							
								
							 | 
							isorel | 
							   | 
						
						
							| 193 | 
							
								187 189 191 192
							 | 
							syl12anc | 
							   | 
						
						
							| 194 | 
							
								176 193
							 | 
							mpbid | 
							   | 
						
						
							| 195 | 
							
								66
							 | 
							adantr | 
							   | 
						
						
							| 196 | 
							
								195 85
							 | 
							feqresmpt | 
							   | 
						
						
							| 197 | 
							
								85
							 | 
							sselda | 
							   | 
						
						
							| 198 | 
							
								1 2 55 65 13
							 | 
							fourierdlem9 | 
							   | 
						
						
							| 199 | 
							
								198
							 | 
							ad2antrr | 
							   | 
						
						
							| 200 | 
							
								199 197
							 | 
							ffvelcdmd | 
							   | 
						
						
							| 201 | 
							
								14
							 | 
							fourierdlem43 | 
							   | 
						
						
							| 202 | 
							
								201
							 | 
							a1i | 
							   | 
						
						
							| 203 | 
							
								202 197
							 | 
							ffvelcdmd | 
							   | 
						
						
							| 204 | 
							
								200 203
							 | 
							remulcld | 
							   | 
						
						
							| 205 | 
							
								15
							 | 
							fvmpt2 | 
							   | 
						
						
							| 206 | 
							
								197 204 205
							 | 
							syl2anc | 
							   | 
						
						
							| 207 | 
							
								41
							 | 
							a1i | 
							   | 
						
						
							| 208 | 
							
								43
							 | 
							adantr | 
							   | 
						
						
							| 209 | 
							
								
							 | 
							simpr | 
							   | 
						
						
							| 210 | 
							
								
							 | 
							eliccre | 
							   | 
						
						
							| 211 | 
							
								207 208 209 210
							 | 
							syl3anc | 
							   | 
						
						
							| 212 | 
							
								
							 | 
							0red | 
							   | 
						
						
							| 213 | 
							
								75
							 | 
							a1i | 
							   | 
						
						
							| 214 | 
							
								208
							 | 
							rexrd | 
							   | 
						
						
							| 215 | 
							
								
							 | 
							iccleub | 
							   | 
						
						
							| 216 | 
							
								213 214 209 215
							 | 
							syl3anc | 
							   | 
						
						
							| 217 | 
							
								78
							 | 
							adantr | 
							   | 
						
						
							| 218 | 
							
								211 208 212 216 217
							 | 
							lelttrd | 
							   | 
						
						
							| 219 | 
							
								211 218
							 | 
							ltned | 
							   | 
						
						
							| 220 | 
							
								219
							 | 
							adantll | 
							   | 
						
						
							| 221 | 
							
								220
							 | 
							neneqd | 
							   | 
						
						
							| 222 | 
							
								221
							 | 
							iffalsed | 
							   | 
						
						
							| 223 | 
							
								211 212 218
							 | 
							ltnsymd | 
							   | 
						
						
							| 224 | 
							
								223
							 | 
							adantll | 
							   | 
						
						
							| 225 | 
							
								224
							 | 
							iffalsed | 
							   | 
						
						
							| 226 | 
							
								225
							 | 
							oveq2d | 
							   | 
						
						
							| 227 | 
							
								226
							 | 
							oveq1d | 
							   | 
						
						
							| 228 | 
							
								222 227
							 | 
							eqtrd | 
							   | 
						
						
							| 229 | 
							
								1
							 | 
							ad2antrr | 
							   | 
						
						
							| 230 | 
							
								2
							 | 
							ad2antrr | 
							   | 
						
						
							| 231 | 
							
								
							 | 
							iccssre | 
							   | 
						
						
							| 232 | 
							
								41 40 231
							 | 
							mp2an | 
							   | 
						
						
							| 233 | 
							
								232 197
							 | 
							sselid | 
							   | 
						
						
							| 234 | 
							
								230 233
							 | 
							readdcld | 
							   | 
						
						
							| 235 | 
							
								229 234
							 | 
							ffvelcdmd | 
							   | 
						
						
							| 236 | 
							
								65
							 | 
							ad2antrr | 
							   | 
						
						
							| 237 | 
							
								235 236
							 | 
							resubcld | 
							   | 
						
						
							| 238 | 
							
								237 233 220
							 | 
							redivcld | 
							   | 
						
						
							| 239 | 
							
								228 238
							 | 
							eqeltrd | 
							   | 
						
						
							| 240 | 
							
								13
							 | 
							fvmpt2 | 
							   | 
						
						
							| 241 | 
							
								197 239 240
							 | 
							syl2anc | 
							   | 
						
						
							| 242 | 
							
								241 222 227
							 | 
							3eqtrd | 
							   | 
						
						
							| 243 | 
							
								40
							 | 
							a1i | 
							   | 
						
						
							| 244 | 
							
								243
							 | 
							renegcld | 
							   | 
						
						
							| 245 | 
							
								
							 | 
							iccgelb | 
							   | 
						
						
							| 246 | 
							
								213 214 209 245
							 | 
							syl3anc | 
							   | 
						
						
							| 247 | 
							
								81
							 | 
							adantr | 
							   | 
						
						
							| 248 | 
							
								211 208 243 216 247
							 | 
							lelttrd | 
							   | 
						
						
							| 249 | 
							
								211 243 248
							 | 
							ltled | 
							   | 
						
						
							| 250 | 
							
								244 243 211 246 249
							 | 
							eliccd | 
							   | 
						
						
							| 251 | 
							
								219
							 | 
							neneqd | 
							   | 
						
						
							| 252 | 
							
								251
							 | 
							iffalsed | 
							   | 
						
						
							| 253 | 
							
								120
							 | 
							a1i | 
							   | 
						
						
							| 254 | 
							
								211
							 | 
							rehalfcld | 
							   | 
						
						
							| 255 | 
							
								254
							 | 
							resincld | 
							   | 
						
						
							| 256 | 
							
								253 255
							 | 
							remulcld | 
							   | 
						
						
							| 257 | 
							
								
							 | 
							2cn | 
							   | 
						
						
							| 258 | 
							
								257
							 | 
							a1i | 
							   | 
						
						
							| 259 | 
							
								211
							 | 
							recnd | 
							   | 
						
						
							| 260 | 
							
								259
							 | 
							halfcld | 
							   | 
						
						
							| 261 | 
							
								260
							 | 
							sincld | 
							   | 
						
						
							| 262 | 
							
								
							 | 
							2ne0 | 
							   | 
						
						
							| 263 | 
							
								262
							 | 
							a1i | 
							   | 
						
						
							| 264 | 
							
								
							 | 
							fourierdlem44 | 
							   | 
						
						
							| 265 | 
							
								250 219 264
							 | 
							syl2anc | 
							   | 
						
						
							| 266 | 
							
								258 261 263 265
							 | 
							mulne0d | 
							   | 
						
						
							| 267 | 
							
								211 256 266
							 | 
							redivcld | 
							   | 
						
						
							| 268 | 
							
								252 267
							 | 
							eqeltrd | 
							   | 
						
						
							| 269 | 
							
								14
							 | 
							fvmpt2 | 
							   | 
						
						
							| 270 | 
							
								250 268 269
							 | 
							syl2anc | 
							   | 
						
						
							| 271 | 
							
								270
							 | 
							adantll | 
							   | 
						
						
							| 272 | 
							
								242 271
							 | 
							oveq12d | 
							   | 
						
						
							| 273 | 
							
								221
							 | 
							iffalsed | 
							   | 
						
						
							| 274 | 
							
								273
							 | 
							oveq2d | 
							   | 
						
						
							| 275 | 
							
								206 272 274
							 | 
							3eqtrd | 
							   | 
						
						
							| 276 | 
							
								275
							 | 
							mpteq2dva | 
							   | 
						
						
							| 277 | 
							
								87 196 276
							 | 
							3eqtrd | 
							   | 
						
						
							| 278 | 
							
								277
							 | 
							adantr | 
							   | 
						
						
							| 279 | 
							
								278
							 | 
							reseq1d | 
							   | 
						
						
							| 280 | 
							
								1
							 | 
							adantr | 
							   | 
						
						
							| 281 | 
							
								2
							 | 
							adantr | 
							   | 
						
						
							| 282 | 
							
								4
							 | 
							adantr | 
							   | 
						
						
							| 283 | 
							
								5
							 | 
							adantr | 
							   | 
						
						
							| 284 | 
							
								7
							 | 
							adantlr | 
							   | 
						
						
							| 285 | 
							
								11
							 | 
							adantlr | 
							   | 
						
						
							| 286 | 
							
								12
							 | 
							adantlr | 
							   | 
						
						
							| 287 | 
							
								125
							 | 
							adantl | 
							   | 
						
						
							| 288 | 
							
								75
							 | 
							a1i | 
							   | 
						
						
							| 289 | 
							
								76
							 | 
							a1i | 
							   | 
						
						
							| 290 | 
							
								78
							 | 
							adantl | 
							   | 
						
						
							| 291 | 
							
								288 44 289 290
							 | 
							gtnelicc | 
							   | 
						
						
							| 292 | 
							
								65
							 | 
							adantr | 
							   | 
						
						
							| 293 | 
							
								
							 | 
							eqid | 
							   | 
						
						
							| 294 | 
							
								
							 | 
							eqid | 
							   | 
						
						
							| 295 | 
							
								
							 | 
							eqid | 
							   | 
						
						
							| 296 | 
							
								
							 | 
							fveq2 | 
							   | 
						
						
							| 297 | 
							
								
							 | 
							oveq1 | 
							   | 
						
						
							| 298 | 
							
								297
							 | 
							fveq2d | 
							   | 
						
						
							| 299 | 
							
								296 298
							 | 
							oveq12d | 
							   | 
						
						
							| 300 | 
							
								299
							 | 
							sseq2d | 
							   | 
						
						
							| 301 | 
							
								300
							 | 
							cbvriotavw | 
							   | 
						
						
							| 302 | 
							
								280 281 3 282 283 284 285 286 42 44 287 85 291 292 293 29 26 27 28 294 295 301
							 | 
							fourierdlem86 | 
							   | 
						
						
							| 303 | 
							
								302
							 | 
							simprd | 
							   | 
						
						
							| 304 | 
							
								279 303
							 | 
							eqeltrd | 
							   | 
						
						
							| 305 | 
							
								302
							 | 
							simpld | 
							   | 
						
						
							| 306 | 
							
								305
							 | 
							simpld | 
							   | 
						
						
							| 307 | 
							
								278
							 | 
							eqcomd | 
							   | 
						
						
							| 308 | 
							
								307
							 | 
							reseq1d | 
							   | 
						
						
							| 309 | 
							
								308
							 | 
							oveq1d | 
							   | 
						
						
							| 310 | 
							
								306 309
							 | 
							eleqtrd | 
							   | 
						
						
							| 311 | 
							
								305
							 | 
							simprd | 
							   | 
						
						
							| 312 | 
							
								308
							 | 
							oveq1d | 
							   | 
						
						
							| 313 | 
							
								311 312
							 | 
							eleqtrd | 
							   | 
						
						
							| 314 | 
							
								
							 | 
							eqid | 
							   | 
						
						
							| 315 | 
							
								89
							 | 
							adantr | 
							   | 
						
						
							| 316 | 
							
								41
							 | 
							a1i | 
							   | 
						
						
							| 317 | 
							
								44
							 | 
							ad2antrr | 
							   | 
						
						
							| 318 | 
							
								
							 | 
							elioore | 
							   | 
						
						
							| 319 | 
							
								318
							 | 
							adantl | 
							   | 
						
						
							| 320 | 
							
								85 232
							 | 
							sstrdi | 
							   | 
						
						
							| 321 | 
							
								320
							 | 
							adantr | 
							   | 
						
						
							| 322 | 
							
								170
							 | 
							adantr | 
							   | 
						
						
							| 323 | 
							
								322 189
							 | 
							ffvelcdmd | 
							   | 
						
						
							| 324 | 
							
								321 323
							 | 
							sseldd | 
							   | 
						
						
							| 325 | 
							
								324
							 | 
							adantr | 
							   | 
						
						
							| 326 | 
							
								75
							 | 
							a1i | 
							   | 
						
						
							| 327 | 
							
								44
							 | 
							adantr | 
							   | 
						
						
							| 328 | 
							
								327
							 | 
							rexrd | 
							   | 
						
						
							| 329 | 
							
								
							 | 
							iccgelb | 
							   | 
						
						
							| 330 | 
							
								326 328 323 329
							 | 
							syl3anc | 
							   | 
						
						
							| 331 | 
							
								330
							 | 
							adantr | 
							   | 
						
						
							| 332 | 
							
								325
							 | 
							rexrd | 
							   | 
						
						
							| 333 | 
							
								322 191
							 | 
							ffvelcdmd | 
							   | 
						
						
							| 334 | 
							
								321 333
							 | 
							sseldd | 
							   | 
						
						
							| 335 | 
							
								334
							 | 
							rexrd | 
							   | 
						
						
							| 336 | 
							
								335
							 | 
							adantr | 
							   | 
						
						
							| 337 | 
							
								
							 | 
							simpr | 
							   | 
						
						
							| 338 | 
							
								
							 | 
							ioogtlb | 
							   | 
						
						
							| 339 | 
							
								332 336 337 338
							 | 
							syl3anc | 
							   | 
						
						
							| 340 | 
							
								316 325 319 331 339
							 | 
							lelttrd | 
							   | 
						
						
							| 341 | 
							
								316 319 340
							 | 
							ltled | 
							   | 
						
						
							| 342 | 
							
								334
							 | 
							adantr | 
							   | 
						
						
							| 343 | 
							
								
							 | 
							iooltub | 
							   | 
						
						
							| 344 | 
							
								332 336 337 343
							 | 
							syl3anc | 
							   | 
						
						
							| 345 | 
							
								
							 | 
							iccleub | 
							   | 
						
						
							| 346 | 
							
								326 328 333 345
							 | 
							syl3anc | 
							   | 
						
						
							| 347 | 
							
								346
							 | 
							adantr | 
							   | 
						
						
							| 348 | 
							
								319 342 317 344 347
							 | 
							ltletrd | 
							   | 
						
						
							| 349 | 
							
								319 317 348
							 | 
							ltled | 
							   | 
						
						
							| 350 | 
							
								316 317 319 341 349
							 | 
							eliccd | 
							   | 
						
						
							| 351 | 
							
								350
							 | 
							ralrimiva | 
							   | 
						
						
							| 352 | 
							
								
							 | 
							dfss3 | 
							   | 
						
						
							| 353 | 
							
								351 352
							 | 
							sylibr | 
							   | 
						
						
							| 354 | 
							
								315 353
							 | 
							feqresmpt | 
							   | 
						
						
							| 355 | 
							
								
							 | 
							simplll | 
							   | 
						
						
							| 356 | 
							
								
							 | 
							simpllr | 
							   | 
						
						
							| 357 | 
							
								25
							 | 
							fveq1i | 
							   | 
						
						
							| 358 | 
							
								357
							 | 
							a1i | 
							   | 
						
						
							| 359 | 
							
								
							 | 
							fvres | 
							   | 
						
						
							| 360 | 
							
								359
							 | 
							adantl | 
							   | 
						
						
							| 361 | 
							
								271 273
							 | 
							eqtrd | 
							   | 
						
						
							| 362 | 
							
								242 361
							 | 
							oveq12d | 
							   | 
						
						
							| 363 | 
							
								237
							 | 
							recnd | 
							   | 
						
						
							| 364 | 
							
								259
							 | 
							adantll | 
							   | 
						
						
							| 365 | 
							
								257
							 | 
							a1i | 
							   | 
						
						
							| 366 | 
							
								364
							 | 
							halfcld | 
							   | 
						
						
							| 367 | 
							
								366
							 | 
							sincld | 
							   | 
						
						
							| 368 | 
							
								365 367
							 | 
							mulcld | 
							   | 
						
						
							| 369 | 
							
								266
							 | 
							adantll | 
							   | 
						
						
							| 370 | 
							
								363 364 368 220 369
							 | 
							dmdcan2d | 
							   | 
						
						
							| 371 | 
							
								206 362 370
							 | 
							3eqtrd | 
							   | 
						
						
							| 372 | 
							
								358 360 371
							 | 
							3eqtrd | 
							   | 
						
						
							| 373 | 
							
								355 356 350 372
							 | 
							syl21anc | 
							   | 
						
						
							| 374 | 
							
								355 356 350 370
							 | 
							syl21anc | 
							   | 
						
						
							| 375 | 
							
								374
							 | 
							eqcomd | 
							   | 
						
						
							| 376 | 
							
								
							 | 
							eqidd | 
							   | 
						
						
							| 377 | 
							
								
							 | 
							oveq2 | 
							   | 
						
						
							| 378 | 
							
								377
							 | 
							fveq2d | 
							   | 
						
						
							| 379 | 
							
								378
							 | 
							oveq1d | 
							   | 
						
						
							| 380 | 
							
								
							 | 
							id | 
							   | 
						
						
							| 381 | 
							
								379 380
							 | 
							oveq12d | 
							   | 
						
						
							| 382 | 
							
								381
							 | 
							adantl | 
							   | 
						
						
							| 383 | 
							
								
							 | 
							simpr | 
							   | 
						
						
							| 384 | 
							
								
							 | 
							ovex | 
							   | 
						
						
							| 385 | 
							
								384
							 | 
							a1i | 
							   | 
						
						
							| 386 | 
							
								376 382 383 385
							 | 
							fvmptd | 
							   | 
						
						
							| 387 | 
							
								
							 | 
							eqidd | 
							   | 
						
						
							| 388 | 
							
								
							 | 
							oveq1 | 
							   | 
						
						
							| 389 | 
							
								388
							 | 
							fveq2d | 
							   | 
						
						
							| 390 | 
							
								389
							 | 
							oveq2d | 
							   | 
						
						
							| 391 | 
							
								380 390
							 | 
							oveq12d | 
							   | 
						
						
							| 392 | 
							
								391
							 | 
							adantl | 
							   | 
						
						
							| 393 | 
							
								
							 | 
							ovex | 
							   | 
						
						
							| 394 | 
							
								393
							 | 
							a1i | 
							   | 
						
						
							| 395 | 
							
								387 392 383 394
							 | 
							fvmptd | 
							   | 
						
						
							| 396 | 
							
								386 395
							 | 
							oveq12d | 
							   | 
						
						
							| 397 | 
							
								396
							 | 
							eqcomd | 
							   | 
						
						
							| 398 | 
							
								397
							 | 
							adantllr | 
							   | 
						
						
							| 399 | 
							
								373 375 398
							 | 
							3eqtrd | 
							   | 
						
						
							| 400 | 
							
								399
							 | 
							mpteq2dva | 
							   | 
						
						
							| 401 | 
							
								354 400
							 | 
							eqtr2d | 
							   | 
						
						
							| 402 | 
							
								401
							 | 
							oveq2d | 
							   | 
						
						
							| 403 | 
							
								67
							 | 
							a1i | 
							   | 
						
						
							| 404 | 
							
								353 321
							 | 
							sstrd | 
							   | 
						
						
							| 405 | 
							
								
							 | 
							tgioo4 | 
							   | 
						
						
							| 406 | 
							
								50 405
							 | 
							dvres | 
							   | 
						
						
							| 407 | 
							
								403 315 321 404 406
							 | 
							syl22anc | 
							   | 
						
						
							| 408 | 
							
								
							 | 
							ioontr | 
							   | 
						
						
							| 409 | 
							
								408
							 | 
							a1i | 
							   | 
						
						
							| 410 | 
							
								409
							 | 
							reseq2d | 
							   | 
						
						
							| 411 | 
							
								402 407 410
							 | 
							3eqtrrd | 
							   | 
						
						
							| 412 | 
							
								1
							 | 
							ad2antrr | 
							   | 
						
						
							| 413 | 
							
								2
							 | 
							ad2antrr | 
							   | 
						
						
							| 414 | 
							
								4
							 | 
							ad2antrr | 
							   | 
						
						
							| 415 | 
							
								5
							 | 
							ad2antrr | 
							   | 
						
						
							| 416 | 
							
								9
							 | 
							ad4ant14 | 
							   | 
						
						
							| 417 | 
							
								85
							 | 
							adantr | 
							   | 
						
						
							| 418 | 
							
								353 417
							 | 
							sstrd | 
							   | 
						
						
							| 419 | 
							
								324
							 | 
							rexrd | 
							   | 
						
						
							| 420 | 
							
								76
							 | 
							a1i | 
							   | 
						
						
							| 421 | 
							
								
							 | 
							0red | 
							   | 
						
						
							| 422 | 
							
								78
							 | 
							ad2antlr | 
							   | 
						
						
							| 423 | 
							
								334 327 421 346 422
							 | 
							lelttrd | 
							   | 
						
						
							| 424 | 
							
								419 334 420 423
							 | 
							gtnelicc | 
							   | 
						
						
							| 425 | 
							
								65
							 | 
							ad2antrr | 
							   | 
						
						
							| 426 | 
							
								41
							 | 
							a1i | 
							   | 
						
						
							| 427 | 
							
								125
							 | 
							ad2antlr | 
							   | 
						
						
							| 428 | 
							
								
							 | 
							simpr | 
							   | 
						
						
							| 429 | 
							
								
							 | 
							biid | 
							   | 
						
						
							| 430 | 
							
								413 3 414 415 426 327 427 417 29 26 27 28 428 301 429
							 | 
							fourierdlem50 | 
							   | 
						
						
							| 431 | 
							
								430
							 | 
							simpld | 
							   | 
						
						
							| 432 | 
							
								430
							 | 
							simprd | 
							   | 
						
						
							| 433 | 
							
								381
							 | 
							cbvmptv | 
							   | 
						
						
							| 434 | 
							
								391
							 | 
							cbvmptv | 
							   | 
						
						
							| 435 | 
							
								
							 | 
							eqid | 
							   | 
						
						
							| 436 | 
							
								412 413 3 414 415 416 324 334 194 418 424 425 29 431 432 433 434 435
							 | 
							fourierdlem72 | 
							   | 
						
						
							| 437 | 
							
								411 436
							 | 
							eqeltrd | 
							   | 
						
						
							| 438 | 
							
								
							 | 
							eqid | 
							   | 
						
						
							| 439 | 
							
								
							 | 
							eqid | 
							   | 
						
						
							| 440 | 
							
								30 431
							 | 
							eqeltrid | 
							   | 
						
						
							| 441 | 
							
								
							 | 
							simpll | 
							   | 
						
						
							| 442 | 
							
								441 440
							 | 
							jca | 
							   | 
						
						
							| 443 | 
							
								
							 | 
							eleq1 | 
							   | 
						
						
							| 444 | 
							
								443
							 | 
							anbi2d | 
							   | 
						
						
							| 445 | 
							
								
							 | 
							fveq2 | 
							   | 
						
						
							| 446 | 
							
								
							 | 
							oveq1 | 
							   | 
						
						
							| 447 | 
							
								446
							 | 
							fveq2d | 
							   | 
						
						
							| 448 | 
							
								445 447
							 | 
							oveq12d | 
							   | 
						
						
							| 449 | 
							
								
							 | 
							raleq | 
							   | 
						
						
							| 450 | 
							
								448 449
							 | 
							syl | 
							   | 
						
						
							| 451 | 
							
								450
							 | 
							rexbidv | 
							   | 
						
						
							| 452 | 
							
								444 451
							 | 
							imbi12d | 
							   | 
						
						
							| 453 | 
							
								452 8
							 | 
							vtoclg | 
							   | 
						
						
							| 454 | 
							
								440 442 453
							 | 
							sylc | 
							   | 
						
						
							| 455 | 
							
								
							 | 
							nfv | 
							   | 
						
						
							| 456 | 
							
								
							 | 
							nfra1 | 
							   | 
						
						
							| 457 | 
							
								455 456
							 | 
							nfan | 
							   | 
						
						
							| 458 | 
							
								
							 | 
							simplr | 
							   | 
						
						
							| 459 | 
							
								41
							 | 
							a1i | 
							   | 
						
						
							| 460 | 
							
								459 2
							 | 
							readdcld | 
							   | 
						
						
							| 461 | 
							
								40
							 | 
							a1i | 
							   | 
						
						
							| 462 | 
							
								461 2
							 | 
							readdcld | 
							   | 
						
						
							| 463 | 
							
								460 462
							 | 
							iccssred | 
							   | 
						
						
							| 464 | 
							
								
							 | 
							ressxr | 
							   | 
						
						
							| 465 | 
							
								463 464
							 | 
							sstrdi | 
							   | 
						
						
							| 466 | 
							
								465
							 | 
							ad2antrr | 
							   | 
						
						
							| 467 | 
							
								3 414 415
							 | 
							fourierdlem15 | 
							   | 
						
						
							| 468 | 
							
								
							 | 
							elfzofz | 
							   | 
						
						
							| 469 | 
							
								440 468
							 | 
							syl | 
							   | 
						
						
							| 470 | 
							
								467 469
							 | 
							ffvelcdmd | 
							   | 
						
						
							| 471 | 
							
								466 470
							 | 
							sseldd | 
							   | 
						
						
							| 472 | 
							
								471
							 | 
							adantr | 
							   | 
						
						
							| 473 | 
							
								
							 | 
							fzofzp1 | 
							   | 
						
						
							| 474 | 
							
								440 473
							 | 
							syl | 
							   | 
						
						
							| 475 | 
							
								467 474
							 | 
							ffvelcdmd | 
							   | 
						
						
							| 476 | 
							
								466 475
							 | 
							sseldd | 
							   | 
						
						
							| 477 | 
							
								476
							 | 
							adantr | 
							   | 
						
						
							| 478 | 
							
								
							 | 
							elioore | 
							   | 
						
						
							| 479 | 
							
								478
							 | 
							adantl | 
							   | 
						
						
							| 480 | 
							
								40
							 | 
							a1i | 
							   | 
						
						
							| 481 | 
							
								426 480 413 3 414 415 469 29
							 | 
							fourierdlem13 | 
							   | 
						
						
							| 482 | 
							
								481
							 | 
							simprd | 
							   | 
						
						
							| 483 | 
							
								482
							 | 
							adantr | 
							   | 
						
						
							| 484 | 
							
								463
							 | 
							ad2antrr | 
							   | 
						
						
							| 485 | 
							
								484 470
							 | 
							sseldd | 
							   | 
						
						
							| 486 | 
							
								485
							 | 
							adantr | 
							   | 
						
						
							| 487 | 
							
								483 486
							 | 
							eqeltrrd | 
							   | 
						
						
							| 488 | 
							
								413 324
							 | 
							readdcld | 
							   | 
						
						
							| 489 | 
							
								488
							 | 
							adantr | 
							   | 
						
						
							| 490 | 
							
								481
							 | 
							simpld | 
							   | 
						
						
							| 491 | 
							
								485 413
							 | 
							resubcld | 
							   | 
						
						
							| 492 | 
							
								490 491
							 | 
							eqeltrd | 
							   | 
						
						
							| 493 | 
							
								426 480 413 3 414 415 474 29
							 | 
							fourierdlem13 | 
							   | 
						
						
							| 494 | 
							
								493
							 | 
							simpld | 
							   | 
						
						
							| 495 | 
							
								484 475
							 | 
							sseldd | 
							   | 
						
						
							| 496 | 
							
								495 413
							 | 
							resubcld | 
							   | 
						
						
							| 497 | 
							
								494 496
							 | 
							eqeltrd | 
							   | 
						
						
							| 498 | 
							
								30
							 | 
							eqcomi | 
							   | 
						
						
							| 499 | 
							
								498
							 | 
							fveq2i | 
							   | 
						
						
							| 500 | 
							
								498
							 | 
							oveq1i | 
							   | 
						
						
							| 501 | 
							
								500
							 | 
							fveq2i | 
							   | 
						
						
							| 502 | 
							
								499 501
							 | 
							oveq12i | 
							   | 
						
						
							| 503 | 
							
								432 502
							 | 
							sseqtrdi | 
							   | 
						
						
							| 504 | 
							
								492 497 324 334 194 503
							 | 
							fourierdlem10 | 
							   | 
						
						
							| 505 | 
							
								504
							 | 
							simpld | 
							   | 
						
						
							| 506 | 
							
								492 324 413 505
							 | 
							leadd2dd | 
							   | 
						
						
							| 507 | 
							
								506
							 | 
							adantr | 
							   | 
						
						
							| 508 | 
							
								489
							 | 
							rexrd | 
							   | 
						
						
							| 509 | 
							
								413 334
							 | 
							readdcld | 
							   | 
						
						
							| 510 | 
							
								509
							 | 
							rexrd | 
							   | 
						
						
							| 511 | 
							
								510
							 | 
							adantr | 
							   | 
						
						
							| 512 | 
							
								
							 | 
							simpr | 
							   | 
						
						
							| 513 | 
							
								
							 | 
							ioogtlb | 
							   | 
						
						
							| 514 | 
							
								508 511 512 513
							 | 
							syl3anc | 
							   | 
						
						
							| 515 | 
							
								487 489 479 507 514
							 | 
							lelttrd | 
							   | 
						
						
							| 516 | 
							
								483 515
							 | 
							eqbrtrd | 
							   | 
						
						
							| 517 | 
							
								509
							 | 
							adantr | 
							   | 
						
						
							| 518 | 
							
								493
							 | 
							simprd | 
							   | 
						
						
							| 519 | 
							
								518 495
							 | 
							eqeltrrd | 
							   | 
						
						
							| 520 | 
							
								519
							 | 
							adantr | 
							   | 
						
						
							| 521 | 
							
								
							 | 
							iooltub | 
							   | 
						
						
							| 522 | 
							
								508 511 512 521
							 | 
							syl3anc | 
							   | 
						
						
							| 523 | 
							
								504
							 | 
							simprd | 
							   | 
						
						
							| 524 | 
							
								334 497 413 523
							 | 
							leadd2dd | 
							   | 
						
						
							| 525 | 
							
								524
							 | 
							adantr | 
							   | 
						
						
							| 526 | 
							
								479 517 520 522 525
							 | 
							ltletrd | 
							   | 
						
						
							| 527 | 
							
								518
							 | 
							eqcomd | 
							   | 
						
						
							| 528 | 
							
								527
							 | 
							adantr | 
							   | 
						
						
							| 529 | 
							
								526 528
							 | 
							breqtrd | 
							   | 
						
						
							| 530 | 
							
								472 477 479 516 529
							 | 
							eliood | 
							   | 
						
						
							| 531 | 
							
								530
							 | 
							adantlr | 
							   | 
						
						
							| 532 | 
							
								
							 | 
							rspa | 
							   | 
						
						
							| 533 | 
							
								458 531 532
							 | 
							syl2anc | 
							   | 
						
						
							| 534 | 
							
								533
							 | 
							ex | 
							   | 
						
						
							| 535 | 
							
								457 534
							 | 
							ralrimi | 
							   | 
						
						
							| 536 | 
							
								535
							 | 
							ex | 
							   | 
						
						
							| 537 | 
							
								536
							 | 
							reximdv | 
							   | 
						
						
							| 538 | 
							
								454 537
							 | 
							mpd | 
							   | 
						
						
							| 539 | 
							
								448
							 | 
							raleqdv | 
							   | 
						
						
							| 540 | 
							
								539
							 | 
							rexbidv | 
							   | 
						
						
							| 541 | 
							
								444 540
							 | 
							imbi12d | 
							   | 
						
						
							| 542 | 
							
								541 10
							 | 
							vtoclg | 
							   | 
						
						
							| 543 | 
							
								440 442 542
							 | 
							sylc | 
							   | 
						
						
							| 544 | 
							
								
							 | 
							nfra1 | 
							   | 
						
						
							| 545 | 
							
								455 544
							 | 
							nfan | 
							   | 
						
						
							| 546 | 
							
								1 68
							 | 
							fssd | 
							   | 
						
						
							| 547 | 
							
								
							 | 
							ssid | 
							   | 
						
						
							| 548 | 
							
								547
							 | 
							a1i | 
							   | 
						
						
							| 549 | 
							
								
							 | 
							ioossre | 
							   | 
						
						
							| 550 | 
							
								549
							 | 
							a1i | 
							   | 
						
						
							| 551 | 
							
								50 405
							 | 
							dvres | 
							   | 
						
						
							| 552 | 
							
								68 546 548 550 551
							 | 
							syl22anc | 
							   | 
						
						
							| 553 | 
							
								
							 | 
							ioontr | 
							   | 
						
						
							| 554 | 
							
								553
							 | 
							reseq2i | 
							   | 
						
						
							| 555 | 
							
								554
							 | 
							a1i | 
							   | 
						
						
							| 556 | 
							
								552 555
							 | 
							eqtrd | 
							   | 
						
						
							| 557 | 
							
								556
							 | 
							fveq1d | 
							   | 
						
						
							| 558 | 
							
								
							 | 
							fvres | 
							   | 
						
						
							| 559 | 
							
								557 558
							 | 
							sylan9eq | 
							   | 
						
						
							| 560 | 
							
								559
							 | 
							ad4ant14 | 
							   | 
						
						
							| 561 | 
							
								560
							 | 
							fveq2d | 
							   | 
						
						
							| 562 | 
							
								561
							 | 
							adantlr | 
							   | 
						
						
							| 563 | 
							
								
							 | 
							simplr | 
							   | 
						
						
							| 564 | 
							
								530
							 | 
							adantlr | 
							   | 
						
						
							| 565 | 
							
								
							 | 
							rspa | 
							   | 
						
						
							| 566 | 
							
								563 564 565
							 | 
							syl2anc | 
							   | 
						
						
							| 567 | 
							
								562 566
							 | 
							eqbrtrd | 
							   | 
						
						
							| 568 | 
							
								567
							 | 
							ex | 
							   | 
						
						
							| 569 | 
							
								545 568
							 | 
							ralrimi | 
							   | 
						
						
							| 570 | 
							
								569
							 | 
							ex | 
							   | 
						
						
							| 571 | 
							
								570
							 | 
							reximdv | 
							   | 
						
						
							| 572 | 
							
								543 571
							 | 
							mpd | 
							   | 
						
						
							| 573 | 
							
								426
							 | 
							rexrd | 
							   | 
						
						
							| 574 | 
							
								573 328 322 428
							 | 
							fourierdlem8 | 
							   | 
						
						
							| 575 | 
							
								145
							 | 
							ad2antrr | 
							   | 
						
						
							| 576 | 
							
								170 320
							 | 
							fssd | 
							   | 
						
						
							| 577 | 
							
								576
							 | 
							ad2antrr | 
							   | 
						
						
							| 578 | 
							
								
							 | 
							simpr | 
							   | 
						
						
							| 579 | 
							
								171
							 | 
							eqcomd | 
							   | 
						
						
							| 580 | 
							
								172
							 | 
							eqcomd | 
							   | 
						
						
							| 581 | 
							
								579 580
							 | 
							oveq12d | 
							   | 
						
						
							| 582 | 
							
								581
							 | 
							adantr | 
							   | 
						
						
							| 583 | 
							
								578 582
							 | 
							eleqtrd | 
							   | 
						
						
							| 584 | 
							
								583
							 | 
							adantr | 
							   | 
						
						
							| 585 | 
							
								
							 | 
							simpr | 
							   | 
						
						
							| 586 | 
							
								
							 | 
							fveq2 | 
							   | 
						
						
							| 587 | 
							
								586
							 | 
							breq1d | 
							   | 
						
						
							| 588 | 
							
								587
							 | 
							cbvrabv | 
							   | 
						
						
							| 589 | 
							
								588
							 | 
							supeq1i | 
							   | 
						
						
							| 590 | 
							
								575 577 584 585 589
							 | 
							fourierdlem25 | 
							   | 
						
						
							| 591 | 
							
								554
							 | 
							a1i | 
							   | 
						
						
							| 592 | 
							
								546
							 | 
							ad2antrr | 
							   | 
						
						
							| 593 | 
							
								547
							 | 
							a1i | 
							   | 
						
						
							| 594 | 
							
								549
							 | 
							a1i | 
							   | 
						
						
							| 595 | 
							
								403 592 593 594 551
							 | 
							syl22anc | 
							   | 
						
						
							| 596 | 
							
								530
							 | 
							ralrimiva | 
							   | 
						
						
							| 597 | 
							
								
							 | 
							dfss3 | 
							   | 
						
						
							| 598 | 
							
								596 597
							 | 
							sylibr | 
							   | 
						
						
							| 599 | 
							
								598
							 | 
							resabs1d | 
							   | 
						
						
							| 600 | 
							
								591 595 599
							 | 
							3eqtr4rd | 
							   | 
						
						
							| 601 | 
							
								
							 | 
							simpr | 
							   | 
						
						
							| 602 | 
							
								
							 | 
							id | 
							   | 
						
						
							| 603 | 
							
								448
							 | 
							reseq2d | 
							   | 
						
						
							| 604 | 
							
								603 448
							 | 
							feq12d | 
							   | 
						
						
							| 605 | 
							
								444 604
							 | 
							imbi12d | 
							   | 
						
						
							| 606 | 
							
								
							 | 
							cncff | 
							   | 
						
						
							| 607 | 
							
								9 606
							 | 
							syl | 
							   | 
						
						
							| 608 | 
							
								605 607
							 | 
							vtoclg | 
							   | 
						
						
							| 609 | 
							
								601 602 608
							 | 
							sylc | 
							   | 
						
						
							| 610 | 
							
								442 609
							 | 
							syl | 
							   | 
						
						
							| 611 | 
							
								610 598
							 | 
							fssresd | 
							   | 
						
						
							| 612 | 
							
								600 611
							 | 
							feq1dd | 
							   | 
						
						
							| 613 | 
							
								379 390
							 | 
							oveq12d | 
							   | 
						
						
							| 614 | 
							
								613
							 | 
							cbvmptv | 
							   | 
						
						
							| 615 | 
							
								
							 | 
							biid | 
							   | 
						
						
							| 616 | 
							
								
							 | 
							fveq2 | 
							   | 
						
						
							| 617 | 
							
								616
							 | 
							fveq2d | 
							   | 
						
						
							| 618 | 
							
								617
							 | 
							breq1d | 
							   | 
						
						
							| 619 | 
							
								618
							 | 
							cbvralvw | 
							   | 
						
						
							| 620 | 
							
								615 619
							 | 
							anbi12i | 
							   | 
						
						
							| 621 | 
							
								
							 | 
							fveq2 | 
							   | 
						
						
							| 622 | 
							
								621
							 | 
							fveq2d | 
							   | 
						
						
							| 623 | 
							
								622
							 | 
							breq1d | 
							   | 
						
						
							| 624 | 
							
								623
							 | 
							cbvralvw | 
							   | 
						
						
							| 625 | 
							
								620 624
							 | 
							anbi12i | 
							   | 
						
						
							| 626 | 
							
								280 281 42 44 85 291 292 438 439 538 572 170 194 574 590 612 614 625
							 | 
							fourierdlem80 | 
							   | 
						
						
							| 627 | 
							
								370
							 | 
							mpteq2dva | 
							   | 
						
						
							| 628 | 
							
								277 627
							 | 
							eqtrd | 
							   | 
						
						
							| 629 | 
							
								628
							 | 
							oveq2d | 
							   | 
						
						
							| 630 | 
							
								629
							 | 
							dmeqd | 
							   | 
						
						
							| 631 | 
							
								
							 | 
							nfcv | 
							   | 
						
						
							| 632 | 
							
								
							 | 
							nfcv | 
							   | 
						
						
							| 633 | 
							
								
							 | 
							nfcv | 
							   | 
						
						
							| 634 | 
							
								
							 | 
							nfmpt1 | 
							   | 
						
						
							| 635 | 
							
								632 633 634
							 | 
							nfov | 
							   | 
						
						
							| 636 | 
							
								635
							 | 
							nfdm | 
							   | 
						
						
							| 637 | 
							
								631 636
							 | 
							raleqf | 
							   | 
						
						
							| 638 | 
							
								630 637
							 | 
							syl | 
							   | 
						
						
							| 639 | 
							
								629
							 | 
							fveq1d | 
							   | 
						
						
							| 640 | 
							
								639
							 | 
							fveq2d | 
							   | 
						
						
							| 641 | 
							
								640
							 | 
							breq1d | 
							   | 
						
						
							| 642 | 
							
								641
							 | 
							ralbidv | 
							   | 
						
						
							| 643 | 
							
								638 642
							 | 
							bitrd | 
							   | 
						
						
							| 644 | 
							
								643
							 | 
							rexbidv | 
							   | 
						
						
							| 645 | 
							
								626 644
							 | 
							mpbird | 
							   | 
						
						
							| 646 | 
							
								
							 | 
							eqid | 
							   | 
						
						
							| 647 | 
							
								
							 | 
							eqeq1 | 
							   | 
						
						
							| 648 | 
							
								
							 | 
							fveq2 | 
							   | 
						
						
							| 649 | 
							
								
							 | 
							oveq1 | 
							   | 
						
						
							| 650 | 
							
								649
							 | 
							fveq2d | 
							   | 
						
						
							| 651 | 
							
								648 650
							 | 
							oveq12d | 
							   | 
						
						
							| 652 | 
							
								651
							 | 
							sseq2d | 
							   | 
						
						
							| 653 | 
							
								652
							 | 
							cbvriotavw | 
							   | 
						
						
							| 654 | 
							
								653
							 | 
							fveq2i | 
							   | 
						
						
							| 655 | 
							
								654
							 | 
							eqeq2i | 
							   | 
						
						
							| 656 | 
							
								655
							 | 
							a1i | 
							   | 
						
						
							| 657 | 
							
								
							 | 
							csbeq1 | 
							   | 
						
						
							| 658 | 
							
								653 657
							 | 
							ax-mp | 
							   | 
						
						
							| 659 | 
							
								658
							 | 
							a1i | 
							   | 
						
						
							| 660 | 
							
								656 659
							 | 
							ifbieq1d | 
							   | 
						
						
							| 661 | 
							
								660
							 | 
							mptru | 
							   | 
						
						
							| 662 | 
							
								661
							 | 
							oveq1i | 
							   | 
						
						
							| 663 | 
							
								662
							 | 
							oveq1i | 
							   | 
						
						
							| 664 | 
							
								663
							 | 
							oveq1i | 
							   | 
						
						
							| 665 | 
							
								664
							 | 
							a1i | 
							   | 
						
						
							| 666 | 
							
								
							 | 
							eqeq1 | 
							   | 
						
						
							| 667 | 
							
								653
							 | 
							oveq1i | 
							   | 
						
						
							| 668 | 
							
								667
							 | 
							fveq2i | 
							   | 
						
						
							| 669 | 
							
								668
							 | 
							eqeq2i | 
							   | 
						
						
							| 670 | 
							
								669
							 | 
							a1i | 
							   | 
						
						
							| 671 | 
							
								
							 | 
							csbeq1 | 
							   | 
						
						
							| 672 | 
							
								653 671
							 | 
							ax-mp | 
							   | 
						
						
							| 673 | 
							
								672
							 | 
							a1i | 
							   | 
						
						
							| 674 | 
							
								670 673
							 | 
							ifbieq1d | 
							   | 
						
						
							| 675 | 
							
								674
							 | 
							mptru | 
							   | 
						
						
							| 676 | 
							
								675
							 | 
							oveq1i | 
							   | 
						
						
							| 677 | 
							
								676
							 | 
							oveq1i | 
							   | 
						
						
							| 678 | 
							
								677
							 | 
							oveq1i | 
							   | 
						
						
							| 679 | 
							
								678
							 | 
							a1i | 
							   | 
						
						
							| 680 | 
							
								
							 | 
							fveq2 | 
							   | 
						
						
							| 681 | 
							
								666 679 680
							 | 
							ifbieq12d | 
							   | 
						
						
							| 682 | 
							
								647 665 681
							 | 
							ifbieq12d | 
							   | 
						
						
							| 683 | 
							
								682
							 | 
							cbvmptv | 
							   | 
						
						
							| 684 | 
							
								42 44 89 145 170 171 172 194 304 310 313 314 437 645 646 683
							 | 
							fourierdlem73 | 
							   | 
						
						
							| 685 | 
							
								
							 | 
							breq2 | 
							   | 
						
						
							| 686 | 
							
								685
							 | 
							rexralbidv | 
							   | 
						
						
							| 687 | 
							
								686
							 | 
							cbvralvw | 
							   | 
						
						
							| 688 | 
							
								684 687
							 | 
							sylib | 
							   | 
						
						
							| 689 | 
							
								688
							 | 
							adantlr | 
							   | 
						
						
							| 690 | 
							
								
							 | 
							rphalfcl | 
							   | 
						
						
							| 691 | 
							
								690
							 | 
							ad2antlr | 
							   | 
						
						
							| 692 | 
							
								
							 | 
							breq2 | 
							   | 
						
						
							| 693 | 
							
								692
							 | 
							rexralbidv | 
							   | 
						
						
							| 694 | 
							
								693
							 | 
							rspccva | 
							   | 
						
						
							| 695 | 
							
								689 691 694
							 | 
							syl2anc | 
							   | 
						
						
							| 696 | 
							
								357
							 | 
							a1i | 
							   | 
						
						
							| 697 | 
							
								158
							 | 
							a1i | 
							   | 
						
						
							| 698 | 
							
								697
							 | 
							sselda | 
							   | 
						
						
							| 699 | 
							
								698 359
							 | 
							syl | 
							   | 
						
						
							| 700 | 
							
								696 699
							 | 
							eqtr2d | 
							   | 
						
						
							| 701 | 
							
								700
							 | 
							oveq1d | 
							   | 
						
						
							| 702 | 
							
								701
							 | 
							itgeq2dv | 
							   | 
						
						
							| 703 | 
							
								702
							 | 
							adantr | 
							   | 
						
						
							| 704 | 
							
								703
							 | 
							fveq2d | 
							   | 
						
						
							| 705 | 
							
								
							 | 
							simpr | 
							   | 
						
						
							| 706 | 
							
								704 705
							 | 
							eqbrtrd | 
							   | 
						
						
							| 707 | 
							
								706
							 | 
							ex | 
							   | 
						
						
							| 708 | 
							
								707
							 | 
							adantlr | 
							   | 
						
						
							| 709 | 
							
								708
							 | 
							ralimdv | 
							   | 
						
						
							| 710 | 
							
								709
							 | 
							reximdv | 
							   | 
						
						
							| 711 | 
							
								695 710
							 | 
							mpd | 
							   | 
						
						
							| 712 | 
							
								711
							 | 
							adantr | 
							   | 
						
						
							| 713 | 
							
								
							 | 
							nfv | 
							   | 
						
						
							| 714 | 
							
								
							 | 
							nfra1 | 
							   | 
						
						
							| 715 | 
							
								713 714
							 | 
							nfan | 
							   | 
						
						
							| 716 | 
							
								
							 | 
							nfv | 
							   | 
						
						
							| 717 | 
							
								715 716
							 | 
							nfan | 
							   | 
						
						
							| 718 | 
							
								
							 | 
							nfv | 
							   | 
						
						
							| 719 | 
							
								717 718
							 | 
							nfan | 
							   | 
						
						
							| 720 | 
							
								
							 | 
							simpll | 
							   | 
						
						
							| 721 | 
							
								
							 | 
							eluznn | 
							   | 
						
						
							| 722 | 
							
								721
							 | 
							adantll | 
							   | 
						
						
							| 723 | 
							
								720 722
							 | 
							jca | 
							   | 
						
						
							| 724 | 
							
								723
							 | 
							adantllr | 
							   | 
						
						
							| 725 | 
							
								
							 | 
							simpllr | 
							   | 
						
						
							| 726 | 
							
								721
							 | 
							adantll | 
							   | 
						
						
							| 727 | 
							
								
							 | 
							rspa | 
							   | 
						
						
							| 728 | 
							
								725 726 727
							 | 
							syl2anc | 
							   | 
						
						
							| 729 | 
							
								724 728
							 | 
							jca | 
							   | 
						
						
							| 730 | 
							
								729
							 | 
							adantlr | 
							   | 
						
						
							| 731 | 
							
								
							 | 
							nnre | 
							   | 
						
						
							| 732 | 
							
								731
							 | 
							rexrd | 
							   | 
						
						
							| 733 | 
							
								732
							 | 
							adantr | 
							   | 
						
						
							| 734 | 
							
								51
							 | 
							a1i | 
							   | 
						
						
							| 735 | 
							
								
							 | 
							eluzelre | 
							   | 
						
						
							| 736 | 
							
								
							 | 
							1re | 
							   | 
						
						
							| 737 | 
							
								736
							 | 
							rehalfcli | 
							   | 
						
						
							| 738 | 
							
								737
							 | 
							a1i | 
							   | 
						
						
							| 739 | 
							
								735 738
							 | 
							readdcld | 
							   | 
						
						
							| 740 | 
							
								739
							 | 
							adantl | 
							   | 
						
						
							| 741 | 
							
								731
							 | 
							adantr | 
							   | 
						
						
							| 742 | 
							
								735
							 | 
							adantl | 
							   | 
						
						
							| 743 | 
							
								
							 | 
							eluzle | 
							   | 
						
						
							| 744 | 
							
								743
							 | 
							adantl | 
							   | 
						
						
							| 745 | 
							
								
							 | 
							halfgt0 | 
							   | 
						
						
							| 746 | 
							
								745
							 | 
							a1i | 
							   | 
						
						
							| 747 | 
							
								737
							 | 
							a1i | 
							   | 
						
						
							| 748 | 
							
								747 742
							 | 
							ltaddposd | 
							   | 
						
						
							| 749 | 
							
								746 748
							 | 
							mpbid | 
							   | 
						
						
							| 750 | 
							
								741 742 740 744 749
							 | 
							lelttrd | 
							   | 
						
						
							| 751 | 
							
								740
							 | 
							ltpnfd | 
							   | 
						
						
							| 752 | 
							
								733 734 740 750 751
							 | 
							eliood | 
							   | 
						
						
							| 753 | 
							
								752
							 | 
							adantlr | 
							   | 
						
						
							| 754 | 
							
								
							 | 
							simplr | 
							   | 
						
						
							| 755 | 
							
								
							 | 
							oveq1 | 
							   | 
						
						
							| 756 | 
							
								755
							 | 
							fveq2d | 
							   | 
						
						
							| 757 | 
							
								756
							 | 
							oveq2d | 
							   | 
						
						
							| 758 | 
							
								757
							 | 
							adantr | 
							   | 
						
						
							| 759 | 
							
								758
							 | 
							itgeq2dv | 
							   | 
						
						
							| 760 | 
							
								759
							 | 
							fveq2d | 
							   | 
						
						
							| 761 | 
							
								760
							 | 
							breq1d | 
							   | 
						
						
							| 762 | 
							
								761
							 | 
							rspcv | 
							   | 
						
						
							| 763 | 
							
								753 754 762
							 | 
							sylc | 
							   | 
						
						
							| 764 | 
							
								763
							 | 
							adantlll | 
							   | 
						
						
							| 765 | 
							
								730 764
							 | 
							jca | 
							   | 
						
						
							| 766 | 
							
								765 31
							 | 
							sylibr | 
							   | 
						
						
							| 767 | 
							
								41
							 | 
							a1i | 
							   | 
						
						
							| 768 | 
							
								
							 | 
							0red | 
							   | 
						
						
							| 769 | 
							
								
							 | 
							ioossicc | 
							   | 
						
						
							| 770 | 
							
								31
							 | 
							biimpi | 
							   | 
						
						
							| 771 | 
							
								
							 | 
							simp-4r | 
							   | 
						
						
							| 772 | 
							
								770 771
							 | 
							syl | 
							   | 
						
						
							| 773 | 
							
								769 772
							 | 
							sselid | 
							   | 
						
						
							| 774 | 
							
								
							 | 
							simp-5l | 
							   | 
						
						
							| 775 | 
							
								770 774
							 | 
							syl | 
							   | 
						
						
							| 776 | 
							
								66
							 | 
							adantr | 
							   | 
						
						
							| 777 | 
							
								40
							 | 
							rexri | 
							   | 
						
						
							| 778 | 
							
								
							 | 
							0re | 
							   | 
						
						
							| 779 | 
							
								778 40 79
							 | 
							ltleii | 
							   | 
						
						
							| 780 | 
							
								
							 | 
							iooss2 | 
							   | 
						
						
							| 781 | 
							
								777 779 780
							 | 
							mp2an | 
							   | 
						
						
							| 782 | 
							
								
							 | 
							ioossicc | 
							   | 
						
						
							| 783 | 
							
								781 782
							 | 
							sstri | 
							   | 
						
						
							| 784 | 
							
								783
							 | 
							sseli | 
							   | 
						
						
							| 785 | 
							
								784
							 | 
							adantl | 
							   | 
						
						
							| 786 | 
							
								776 785
							 | 
							ffvelcdmd | 
							   | 
						
						
							| 787 | 
							
								775 786
							 | 
							sylan | 
							   | 
						
						
							| 788 | 
							
								
							 | 
							simpllr | 
							   | 
						
						
							| 789 | 
							
								770 788
							 | 
							syl | 
							   | 
						
						
							| 790 | 
							
								789
							 | 
							nnred | 
							   | 
						
						
							| 791 | 
							
								737
							 | 
							a1i | 
							   | 
						
						
							| 792 | 
							
								790 791
							 | 
							readdcld | 
							   | 
						
						
							| 793 | 
							
								792
							 | 
							adantr | 
							   | 
						
						
							| 794 | 
							
								
							 | 
							elioore | 
							   | 
						
						
							| 795 | 
							
								794
							 | 
							adantl | 
							   | 
						
						
							| 796 | 
							
								793 795
							 | 
							remulcld | 
							   | 
						
						
							| 797 | 
							
								796
							 | 
							resincld | 
							   | 
						
						
							| 798 | 
							
								787 797
							 | 
							remulcld | 
							   | 
						
						
							| 799 | 
							
								798
							 | 
							recnd | 
							   | 
						
						
							| 800 | 
							
								75
							 | 
							a1i | 
							   | 
						
						
							| 801 | 
							
								76
							 | 
							a1i | 
							   | 
						
						
							| 802 | 
							
								767
							 | 
							leidd | 
							   | 
						
						
							| 803 | 
							
								
							 | 
							ioossre | 
							   | 
						
						
							| 804 | 
							
								803 772
							 | 
							sselid | 
							   | 
						
						
							| 805 | 
							
								800 801 772 77
							 | 
							syl3anc | 
							   | 
						
						
							| 806 | 
							
								804 768 805
							 | 
							ltled | 
							   | 
						
						
							| 807 | 
							
								
							 | 
							ioossioo | 
							   | 
						
						
							| 808 | 
							
								800 801 802 806 807
							 | 
							syl22anc | 
							   | 
						
						
							| 809 | 
							
								
							 | 
							ioombl | 
							   | 
						
						
							| 810 | 
							
								809
							 | 
							a1i | 
							   | 
						
						
							| 811 | 
							
								
							 | 
							eleq1 | 
							   | 
						
						
							| 812 | 
							
								811
							 | 
							anbi2d | 
							   | 
						
						
							| 813 | 
							
								
							 | 
							simpl | 
							   | 
						
						
							| 814 | 
							
								813
							 | 
							oveq1d | 
							   | 
						
						
							| 815 | 
							
								814
							 | 
							oveq1d | 
							   | 
						
						
							| 816 | 
							
								815
							 | 
							fveq2d | 
							   | 
						
						
							| 817 | 
							
								816
							 | 
							oveq2d | 
							   | 
						
						
							| 818 | 
							
								817
							 | 
							mpteq2dva | 
							   | 
						
						
							| 819 | 
							
								818
							 | 
							eleq1d | 
							   | 
						
						
							| 820 | 
							
								812 819
							 | 
							imbi12d | 
							   | 
						
						
							| 821 | 
							
								783
							 | 
							a1i | 
							   | 
						
						
							| 822 | 
							
								
							 | 
							ioombl | 
							   | 
						
						
							| 823 | 
							
								822
							 | 
							a1i | 
							   | 
						
						
							| 824 | 
							
								66
							 | 
							ffvelcdmda | 
							   | 
						
						
							| 825 | 
							
								824
							 | 
							adantlr | 
							   | 
						
						
							| 826 | 
							
								
							 | 
							nnre | 
							   | 
						
						
							| 827 | 
							
								
							 | 
							readdcl | 
							   | 
						
						
							| 828 | 
							
								826 737 827
							 | 
							sylancl | 
							   | 
						
						
							| 829 | 
							
								828
							 | 
							adantr | 
							   | 
						
						
							| 830 | 
							
								
							 | 
							simpr | 
							   | 
						
						
							| 831 | 
							
								232 830
							 | 
							sselid | 
							   | 
						
						
							| 832 | 
							
								829 831
							 | 
							remulcld | 
							   | 
						
						
							| 833 | 
							
								832
							 | 
							resincld | 
							   | 
						
						
							| 834 | 
							
								833
							 | 
							adantll | 
							   | 
						
						
							| 835 | 
							
								825 834
							 | 
							remulcld | 
							   | 
						
						
							| 836 | 
							
								17
							 | 
							a1i | 
							   | 
						
						
							| 837 | 
							
								16
							 | 
							fvmpt2 | 
							   | 
						
						
							| 838 | 
							
								830 833 837
							 | 
							syl2anc | 
							   | 
						
						
							| 839 | 
							
								838
							 | 
							adantll | 
							   | 
						
						
							| 840 | 
							
								839
							 | 
							oveq2d | 
							   | 
						
						
							| 841 | 
							
								840
							 | 
							mpteq2dva | 
							   | 
						
						
							| 842 | 
							
								836 841
							 | 
							eqtr2d | 
							   | 
						
						
							| 843 | 
							
								1
							 | 
							adantr | 
							   | 
						
						
							| 844 | 
							
								6
							 | 
							adantr | 
							   | 
						
						
							| 845 | 
							
								20
							 | 
							adantr | 
							   | 
						
						
							| 846 | 
							
								21
							 | 
							adantr | 
							   | 
						
						
							| 847 | 
							
								826
							 | 
							adantl | 
							   | 
						
						
							| 848 | 
							
								4
							 | 
							adantr | 
							   | 
						
						
							| 849 | 
							
								5
							 | 
							adantr | 
							   | 
						
						
							| 850 | 
							
								7
							 | 
							adantlr | 
							   | 
						
						
							| 851 | 
							
								11
							 | 
							adantlr | 
							   | 
						
						
							| 852 | 
							
								12
							 | 
							adantlr | 
							   | 
						
						
							| 853 | 
							
								
							 | 
							eqid | 
							   | 
						
						
							| 854 | 
							
								
							 | 
							eqid | 
							   | 
						
						
							| 855 | 
							
								607
							 | 
							adantlr | 
							   | 
						
						
							| 856 | 
							
								22
							 | 
							adantr | 
							   | 
						
						
							| 857 | 
							
								23
							 | 
							adantr | 
							   | 
						
						
							| 858 | 
							
								3 843 844 845 846 13 14 15 847 16 17 848 849 850 851 852 29 853 854 855 856 857
							 | 
							fourierdlem88 | 
							   | 
						
						
							| 859 | 
							
								842 858
							 | 
							eqeltrd | 
							   | 
						
						
							| 860 | 
							
								821 823 835 859
							 | 
							iblss | 
							   | 
						
						
							| 861 | 
							
								820 860
							 | 
							chvarvv | 
							   | 
						
						
							| 862 | 
							
								775 789 861
							 | 
							syl2anc | 
							   | 
						
						
							| 863 | 
							
								808 810 798 862
							 | 
							iblss | 
							   | 
						
						
							| 864 | 
							
								772 125
							 | 
							syl | 
							   | 
						
						
							| 865 | 
							
								767 804 864
							 | 
							ltled | 
							   | 
						
						
							| 866 | 
							
								768
							 | 
							leidd | 
							   | 
						
						
							| 867 | 
							
								
							 | 
							ioossioo | 
							   | 
						
						
							| 868 | 
							
								800 801 865 866 867
							 | 
							syl22anc | 
							   | 
						
						
							| 869 | 
							
								
							 | 
							ioombl | 
							   | 
						
						
							| 870 | 
							
								869
							 | 
							a1i | 
							   | 
						
						
							| 871 | 
							
								868 870 798 862
							 | 
							iblss | 
							   | 
						
						
							| 872 | 
							
								767 768 773 799 863 871
							 | 
							itgsplitioo | 
							   | 
						
						
							| 873 | 
							
								808
							 | 
							sselda | 
							   | 
						
						
							| 874 | 
							
								873 798
							 | 
							syldan | 
							   | 
						
						
							| 875 | 
							
								874 863
							 | 
							itgcl | 
							   | 
						
						
							| 876 | 
							
								868
							 | 
							sselda | 
							   | 
						
						
							| 877 | 
							
								876 798
							 | 
							syldan | 
							   | 
						
						
							| 878 | 
							
								877 871
							 | 
							itgcl | 
							   | 
						
						
							| 879 | 
							
								875 878
							 | 
							addcomd | 
							   | 
						
						
							| 880 | 
							
								872 879
							 | 
							eqtrd | 
							   | 
						
						
							| 881 | 
							
								880
							 | 
							fveq2d | 
							   | 
						
						
							| 882 | 
							
								878 875
							 | 
							addcld | 
							   | 
						
						
							| 883 | 
							
								882
							 | 
							abscld | 
							   | 
						
						
							| 884 | 
							
								878
							 | 
							abscld | 
							   | 
						
						
							| 885 | 
							
								875
							 | 
							abscld | 
							   | 
						
						
							| 886 | 
							
								884 885
							 | 
							readdcld | 
							   | 
						
						
							| 887 | 
							
								
							 | 
							simp-5r | 
							   | 
						
						
							| 888 | 
							
								770 887
							 | 
							syl | 
							   | 
						
						
							| 889 | 
							
								888
							 | 
							rpred | 
							   | 
						
						
							| 890 | 
							
								878 875
							 | 
							abstrid | 
							   | 
						
						
							| 891 | 
							
								
							 | 
							simplr | 
							   | 
						
						
							| 892 | 
							
								770 891
							 | 
							syl | 
							   | 
						
						
							| 893 | 
							
								770
							 | 
							simprd | 
							   | 
						
						
							| 894 | 
							
								884 885 889 892 893
							 | 
							lt2halvesd | 
							   | 
						
						
							| 895 | 
							
								883 886 889 890 894
							 | 
							lelttrd | 
							   | 
						
						
							| 896 | 
							
								881 895
							 | 
							eqbrtrd | 
							   | 
						
						
							| 897 | 
							
								766 896
							 | 
							syl | 
							   | 
						
						
							| 898 | 
							
								897
							 | 
							ex | 
							   | 
						
						
							| 899 | 
							
								719 898
							 | 
							ralrimi | 
							   | 
						
						
							| 900 | 
							
								899
							 | 
							ex | 
							   | 
						
						
							| 901 | 
							
								900
							 | 
							reximdva | 
							   | 
						
						
							| 902 | 
							
								712 901
							 | 
							mpd | 
							   | 
						
						
							| 903 | 
							
								
							 | 
							negpilt0 | 
							   | 
						
						
							| 904 | 
							
								41 778 40
							 | 
							lttri | 
							   | 
						
						
							| 905 | 
							
								903 79 904
							 | 
							mp2an | 
							   | 
						
						
							| 906 | 
							
								41 40 905
							 | 
							ltleii | 
							   | 
						
						
							| 907 | 
							
								906
							 | 
							a1i | 
							   | 
						
						
							| 908 | 
							
								3
							 | 
							fourierdlem2 | 
							   | 
						
						
							| 909 | 
							
								4 908
							 | 
							syl | 
							   | 
						
						
							| 910 | 
							
								5 909
							 | 
							mpbid | 
							   | 
						
						
							| 911 | 
							
								910
							 | 
							simpld | 
							   | 
						
						
							| 912 | 
							
								
							 | 
							elmapi | 
							   | 
						
						
							| 913 | 
							
								911 912
							 | 
							syl | 
							   | 
						
						
							| 914 | 
							
								913
							 | 
							ffvelcdmda | 
							   | 
						
						
							| 915 | 
							
								2
							 | 
							adantr | 
							   | 
						
						
							| 916 | 
							
								914 915
							 | 
							resubcld | 
							   | 
						
						
							| 917 | 
							
								916 29
							 | 
							fmptd | 
							   | 
						
						
							| 918 | 
							
								29
							 | 
							a1i | 
							   | 
						
						
							| 919 | 
							
								
							 | 
							fveq2 | 
							   | 
						
						
							| 920 | 
							
								919
							 | 
							oveq1d | 
							   | 
						
						
							| 921 | 
							
								920
							 | 
							adantl | 
							   | 
						
						
							| 922 | 
							
								4
							 | 
							nnnn0d | 
							   | 
						
						
							| 923 | 
							
								
							 | 
							nn0uz | 
							   | 
						
						
							| 924 | 
							
								922 923
							 | 
							eleqtrdi | 
							   | 
						
						
							| 925 | 
							
								
							 | 
							eluzfz1 | 
							   | 
						
						
							| 926 | 
							
								924 925
							 | 
							syl | 
							   | 
						
						
							| 927 | 
							
								913 926
							 | 
							ffvelcdmd | 
							   | 
						
						
							| 928 | 
							
								927 2
							 | 
							resubcld | 
							   | 
						
						
							| 929 | 
							
								918 921 926 928
							 | 
							fvmptd | 
							   | 
						
						
							| 930 | 
							
								910
							 | 
							simprd | 
							   | 
						
						
							| 931 | 
							
								930
							 | 
							simpld | 
							   | 
						
						
							| 932 | 
							
								931
							 | 
							simpld | 
							   | 
						
						
							| 933 | 
							
								932
							 | 
							oveq1d | 
							   | 
						
						
							| 934 | 
							
								459
							 | 
							recnd | 
							   | 
						
						
							| 935 | 
							
								2
							 | 
							recnd | 
							   | 
						
						
							| 936 | 
							
								934 935
							 | 
							pncand | 
							   | 
						
						
							| 937 | 
							
								929 933 936
							 | 
							3eqtrd | 
							   | 
						
						
							| 938 | 
							
								459 461 2 3 853 4 5 29
							 | 
							fourierdlem14 | 
							   | 
						
						
							| 939 | 
							
								853
							 | 
							fourierdlem2 | 
							   | 
						
						
							| 940 | 
							
								4 939
							 | 
							syl | 
							   | 
						
						
							| 941 | 
							
								938 940
							 | 
							mpbid | 
							   | 
						
						
							| 942 | 
							
								941
							 | 
							simprd | 
							   | 
						
						
							| 943 | 
							
								942
							 | 
							simpld | 
							   | 
						
						
							| 944 | 
							
								943
							 | 
							simprd | 
							   | 
						
						
							| 945 | 
							
								942
							 | 
							simprd | 
							   | 
						
						
							| 946 | 
							
								945
							 | 
							r19.21bi | 
							   | 
						
						
							| 947 | 
							
								1
							 | 
							adantr | 
							   | 
						
						
							| 948 | 
							
								853 4 938
							 | 
							fourierdlem15 | 
							   | 
						
						
							| 949 | 
							
								948
							 | 
							adantr | 
							   | 
						
						
							| 950 | 
							
								
							 | 
							elfzofz | 
							   | 
						
						
							| 951 | 
							
								950
							 | 
							adantl | 
							   | 
						
						
							| 952 | 
							
								949 951
							 | 
							ffvelcdmd | 
							   | 
						
						
							| 953 | 
							
								
							 | 
							fzofzp1 | 
							   | 
						
						
							| 954 | 
							
								953
							 | 
							adantl | 
							   | 
						
						
							| 955 | 
							
								949 954
							 | 
							ffvelcdmd | 
							   | 
						
						
							| 956 | 
							
								2
							 | 
							adantr | 
							   | 
						
						
							| 957 | 
							
								
							 | 
							ffn | 
							   | 
						
						
							| 958 | 
							
								911 912 957
							 | 
							3syl | 
							   | 
						
						
							| 959 | 
							
								
							 | 
							fvelrnb | 
							   | 
						
						
							| 960 | 
							
								958 959
							 | 
							syl | 
							   | 
						
						
							| 961 | 
							
								6 960
							 | 
							mpbid | 
							   | 
						
						
							| 962 | 
							
								
							 | 
							oveq1 | 
							   | 
						
						
							| 963 | 
							
								962
							 | 
							adantl | 
							   | 
						
						
							| 964 | 
							
								935
							 | 
							subidd | 
							   | 
						
						
							| 965 | 
							
								964
							 | 
							ad2antrr | 
							   | 
						
						
							| 966 | 
							
								963 965
							 | 
							eqtr2d | 
							   | 
						
						
							| 967 | 
							
								966
							 | 
							ex | 
							   | 
						
						
							| 968 | 
							
								967
							 | 
							reximdva | 
							   | 
						
						
							| 969 | 
							
								961 968
							 | 
							mpd | 
							   | 
						
						
							| 970 | 
							
								29
							 | 
							elrnmpt | 
							   | 
						
						
							| 971 | 
							
								778 970
							 | 
							ax-mp | 
							   | 
						
						
							| 972 | 
							
								969 971
							 | 
							sylibr | 
							   | 
						
						
							| 973 | 
							
								853 4 938 972
							 | 
							fourierdlem12 | 
							   | 
						
						
							| 974 | 
							
								913
							 | 
							adantr | 
							   | 
						
						
							| 975 | 
							
								974 951
							 | 
							ffvelcdmd | 
							   | 
						
						
							| 976 | 
							
								975 956
							 | 
							resubcld | 
							   | 
						
						
							| 977 | 
							
								29
							 | 
							fvmpt2 | 
							   | 
						
						
							| 978 | 
							
								951 976 977
							 | 
							syl2anc | 
							   | 
						
						
							| 979 | 
							
								978
							 | 
							oveq1d | 
							   | 
						
						
							| 980 | 
							
								975
							 | 
							recnd | 
							   | 
						
						
							| 981 | 
							
								935
							 | 
							adantr | 
							   | 
						
						
							| 982 | 
							
								980 981
							 | 
							npcand | 
							   | 
						
						
							| 983 | 
							
								979 982
							 | 
							eqtrd | 
							   | 
						
						
							| 984 | 
							
								
							 | 
							fveq2 | 
							   | 
						
						
							| 985 | 
							
								984
							 | 
							oveq1d | 
							   | 
						
						
							| 986 | 
							
								985
							 | 
							cbvmptv | 
							   | 
						
						
							| 987 | 
							
								29 986
							 | 
							eqtr4i | 
							   | 
						
						
							| 988 | 
							
								987
							 | 
							a1i | 
							   | 
						
						
							| 989 | 
							
								
							 | 
							fveq2 | 
							   | 
						
						
							| 990 | 
							
								989
							 | 
							oveq1d | 
							   | 
						
						
							| 991 | 
							
								990
							 | 
							adantl | 
							   | 
						
						
							| 992 | 
							
								974 954
							 | 
							ffvelcdmd | 
							   | 
						
						
							| 993 | 
							
								992 956
							 | 
							resubcld | 
							   | 
						
						
							| 994 | 
							
								988 991 954 993
							 | 
							fvmptd | 
							   | 
						
						
							| 995 | 
							
								994
							 | 
							oveq1d | 
							   | 
						
						
							| 996 | 
							
								992
							 | 
							recnd | 
							   | 
						
						
							| 997 | 
							
								996 981
							 | 
							npcand | 
							   | 
						
						
							| 998 | 
							
								995 997
							 | 
							eqtrd | 
							   | 
						
						
							| 999 | 
							
								983 998
							 | 
							oveq12d | 
							   | 
						
						
							| 1000 | 
							
								999
							 | 
							reseq2d | 
							   | 
						
						
							| 1001 | 
							
								999
							 | 
							oveq1d | 
							   | 
						
						
							| 1002 | 
							
								7 1000 1001
							 | 
							3eltr4d | 
							   | 
						
						
							| 1003 | 
							
								55
							 | 
							adantr | 
							   | 
						
						
							| 1004 | 
							
								65
							 | 
							adantr | 
							   | 
						
						
							| 1005 | 
							
								947 952 955 956 973 1002 1003 1004 13
							 | 
							fourierdlem40 | 
							   | 
						
						
							| 1006 | 
							
								
							 | 
							id | 
							   | 
						
						
							| 1007 | 
							
								67
							 | 
							a1i | 
							   | 
						
						
							| 1008 | 
							
								1006 1007
							 | 
							fssd | 
							   | 
						
						
							| 1009 | 
							
								9 606 1008
							 | 
							3syl | 
							   | 
						
						
							| 1010 | 
							
								
							 | 
							eqid | 
							   | 
						
						
							| 1011 | 
							
								2 3 1 6 20 65 13 4 5 11 29 853 854 1009 23 1010
							 | 
							fourierdlem75 | 
							   | 
						
						
							| 1012 | 
							
								
							 | 
							eqid | 
							   | 
						
						
							| 1013 | 
							
								2 3 1 6 55 21 13 4 5 12 29 853 854 607 22 1012
							 | 
							fourierdlem74 | 
							   | 
						
						
							| 1014 | 
							
								
							 | 
							fveq2 | 
							   | 
						
						
							| 1015 | 
							
								
							 | 
							oveq1 | 
							   | 
						
						
							| 1016 | 
							
								1015
							 | 
							fveq2d | 
							   | 
						
						
							| 1017 | 
							
								1014 1016
							 | 
							oveq12d | 
							   | 
						
						
							| 1018 | 
							
								1017
							 | 
							cbvmptv | 
							   | 
						
						
							| 1019 | 
							
								459 461 907 198 4 917 937 944 946 1005 1011 1013 1018
							 | 
							fourierdlem70 | 
							   | 
						
						
							| 1020 | 
							
								
							 | 
							eqid | 
							   | 
						
						
							| 1021 | 
							
								
							 | 
							fveq2 | 
							   | 
						
						
							| 1022 | 
							
								1021
							 | 
							fveq2d | 
							   | 
						
						
							| 1023 | 
							
								1022
							 | 
							breq1d | 
							   | 
						
						
							| 1024 | 
							
								1023
							 | 
							cbvralvw | 
							   | 
						
						
							| 1025 | 
							
								1024
							 | 
							ralbii | 
							   | 
						
						
							| 1026 | 
							
								1025
							 | 
							3anbi3i | 
							   | 
						
						
							| 1027 | 
							
								1026
							 | 
							anbi1i | 
							   | 
						
						
							| 1028 | 
							
								1027
							 | 
							anbi1i | 
							   | 
						
						
							| 1029 | 
							
								1028
							 | 
							anbi1i | 
							   | 
						
						
							| 1030 | 
							
								1 2 55 65 13 14 15 16 17 1019 858 1020 1029
							 | 
							fourierdlem87 | 
							   | 
						
						
							| 1031 | 
							
								
							 | 
							iftrue | 
							   | 
						
						
							| 1032 | 
							
								1031
							 | 
							negeqd | 
							   | 
						
						
							| 1033 | 
							
								1032
							 | 
							adantl | 
							   | 
						
						
							| 1034 | 
							
								75
							 | 
							a1i | 
							   | 
						
						
							| 1035 | 
							
								76
							 | 
							a1i | 
							   | 
						
						
							| 1036 | 
							
								
							 | 
							rpre | 
							   | 
						
						
							| 1037 | 
							
								1036
							 | 
							renegcld | 
							   | 
						
						
							| 1038 | 
							
								1037
							 | 
							adantr | 
							   | 
						
						
							| 1039 | 
							
								1036
							 | 
							adantr | 
							   | 
						
						
							| 1040 | 
							
								40
							 | 
							rehalfcli | 
							   | 
						
						
							| 1041 | 
							
								1040
							 | 
							a1i | 
							   | 
						
						
							| 1042 | 
							
								40
							 | 
							a1i | 
							   | 
						
						
							| 1043 | 
							
								
							 | 
							simpr | 
							   | 
						
						
							| 1044 | 
							
								
							 | 
							halfpos | 
							   | 
						
						
							| 1045 | 
							
								40 1044
							 | 
							ax-mp | 
							   | 
						
						
							| 1046 | 
							
								79 1045
							 | 
							mpbi | 
							   | 
						
						
							| 1047 | 
							
								1046
							 | 
							a1i | 
							   | 
						
						
							| 1048 | 
							
								1039 1041 1042 1043 1047
							 | 
							lelttrd | 
							   | 
						
						
							| 1049 | 
							
								1039 1042
							 | 
							ltnegd | 
							   | 
						
						
							| 1050 | 
							
								1048 1049
							 | 
							mpbid | 
							   | 
						
						
							| 1051 | 
							
								
							 | 
							rpgt0 | 
							   | 
						
						
							| 1052 | 
							
								1036
							 | 
							lt0neg2d | 
							   | 
						
						
							| 1053 | 
							
								1051 1052
							 | 
							mpbid | 
							   | 
						
						
							| 1054 | 
							
								1053
							 | 
							adantr | 
							   | 
						
						
							| 1055 | 
							
								1034 1035 1038 1050 1054
							 | 
							eliood | 
							   | 
						
						
							| 1056 | 
							
								1033 1055
							 | 
							eqeltrd | 
							   | 
						
						
							| 1057 | 
							
								
							 | 
							iffalse | 
							   | 
						
						
							| 1058 | 
							
								1057
							 | 
							negeqd | 
							   | 
						
						
							| 1059 | 
							
								1040
							 | 
							renegcli | 
							   | 
						
						
							| 1060 | 
							
								1059
							 | 
							rexri | 
							   | 
						
						
							| 1061 | 
							
								75 76 1060
							 | 
							3pm3.2i | 
							   | 
						
						
							| 1062 | 
							
								1040 40
							 | 
							ltnegi | 
							   | 
						
						
							| 1063 | 
							
								1046 1062
							 | 
							mpbi | 
							   | 
						
						
							| 1064 | 
							
								
							 | 
							2pos | 
							   | 
						
						
							| 1065 | 
							
								40 120 79 1064
							 | 
							divgt0ii | 
							   | 
						
						
							| 1066 | 
							
								
							 | 
							lt0neg2 | 
							   | 
						
						
							| 1067 | 
							
								1040 1066
							 | 
							ax-mp | 
							   | 
						
						
							| 1068 | 
							
								1065 1067
							 | 
							mpbi | 
							   | 
						
						
							| 1069 | 
							
								1063 1068
							 | 
							pm3.2i | 
							   | 
						
						
							| 1070 | 
							
								
							 | 
							elioo3g | 
							   | 
						
						
							| 1071 | 
							
								1061 1069 1070
							 | 
							mpbir2an | 
							   | 
						
						
							| 1072 | 
							
								1071
							 | 
							a1i | 
							   | 
						
						
							| 1073 | 
							
								1058 1072
							 | 
							eqeltrd | 
							   | 
						
						
							| 1074 | 
							
								1073
							 | 
							adantl | 
							   | 
						
						
							| 1075 | 
							
								1056 1074
							 | 
							pm2.61dan | 
							   | 
						
						
							| 1076 | 
							
								1075
							 | 
							3ad2ant2 | 
							   | 
						
						
							| 1077 | 
							
								
							 | 
							ioombl | 
							   | 
						
						
							| 1078 | 
							
								1077
							 | 
							a1i | 
							   | 
						
						
							| 1079 | 
							
								
							 | 
							simpr | 
							   | 
						
						
							| 1080 | 
							
								1078 1079
							 | 
							jca | 
							   | 
						
						
							| 1081 | 
							
								
							 | 
							ioossicc | 
							   | 
						
						
							| 1082 | 
							
								1081
							 | 
							a1i | 
							   | 
						
						
							| 1083 | 
							
								41
							 | 
							a1i | 
							   | 
						
						
							| 1084 | 
							
								40
							 | 
							a1i | 
							   | 
						
						
							| 1085 | 
							
								1039 1042 1048
							 | 
							ltled | 
							   | 
						
						
							| 1086 | 
							
								1039 1042
							 | 
							lenegd | 
							   | 
						
						
							| 1087 | 
							
								1085 1086
							 | 
							mpbid | 
							   | 
						
						
							| 1088 | 
							
								1032
							 | 
							eqcomd | 
							   | 
						
						
							| 1089 | 
							
								1088
							 | 
							adantl | 
							   | 
						
						
							| 1090 | 
							
								1087 1089
							 | 
							breqtrd | 
							   | 
						
						
							| 1091 | 
							
								41 1059 1063
							 | 
							ltleii | 
							   | 
						
						
							| 1092 | 
							
								1091
							 | 
							a1i | 
							   | 
						
						
							| 1093 | 
							
								1058
							 | 
							eqcomd | 
							   | 
						
						
							| 1094 | 
							
								1093
							 | 
							adantl | 
							   | 
						
						
							| 1095 | 
							
								1092 1094
							 | 
							breqtrd | 
							   | 
						
						
							| 1096 | 
							
								1090 1095
							 | 
							pm2.61dan | 
							   | 
						
						
							| 1097 | 
							
								779
							 | 
							a1i | 
							   | 
						
						
							| 1098 | 
							
								
							 | 
							iccss | 
							   | 
						
						
							| 1099 | 
							
								1083 1084 1096 1097 1098
							 | 
							syl22anc | 
							   | 
						
						
							| 1100 | 
							
								1082 1099
							 | 
							sstrd | 
							   | 
						
						
							| 1101 | 
							
								803 1075
							 | 
							sselid | 
							   | 
						
						
							| 1102 | 
							
								
							 | 
							0red | 
							   | 
						
						
							| 1103 | 
							
								
							 | 
							rpge0 | 
							   | 
						
						
							| 1104 | 
							
								1103
							 | 
							adantr | 
							   | 
						
						
							| 1105 | 
							
								1043
							 | 
							iftrued | 
							   | 
						
						
							| 1106 | 
							
								1104 1105
							 | 
							breqtrrd | 
							   | 
						
						
							| 1107 | 
							
								778 1040 1065
							 | 
							ltleii | 
							   | 
						
						
							| 1108 | 
							
								
							 | 
							simpr | 
							   | 
						
						
							| 1109 | 
							
								1108
							 | 
							iffalsed | 
							   | 
						
						
							| 1110 | 
							
								1107 1109
							 | 
							breqtrrid | 
							   | 
						
						
							| 1111 | 
							
								1106 1110
							 | 
							pm2.61dan | 
							   | 
						
						
							| 1112 | 
							
								1040
							 | 
							a1i | 
							   | 
						
						
							| 1113 | 
							
								1036 1112
							 | 
							ifcld | 
							   | 
						
						
							| 1114 | 
							
								1113
							 | 
							le0neg2d | 
							   | 
						
						
							| 1115 | 
							
								1111 1114
							 | 
							mpbid | 
							   | 
						
						
							| 1116 | 
							
								
							 | 
							volioo | 
							   | 
						
						
							| 1117 | 
							
								1101 1102 1115 1116
							 | 
							syl3anc | 
							   | 
						
						
							| 1118 | 
							
								
							 | 
							0cn | 
							   | 
						
						
							| 1119 | 
							
								1118
							 | 
							a1i | 
							   | 
						
						
							| 1120 | 
							
								1113
							 | 
							recnd | 
							   | 
						
						
							| 1121 | 
							
								1119 1120
							 | 
							subnegd | 
							   | 
						
						
							| 1122 | 
							
								1120
							 | 
							addlidd | 
							   | 
						
						
							| 1123 | 
							
								1117 1121 1122
							 | 
							3eqtrd | 
							   | 
						
						
							| 1124 | 
							
								
							 | 
							min1 | 
							   | 
						
						
							| 1125 | 
							
								1036 1040 1124
							 | 
							sylancl | 
							   | 
						
						
							| 1126 | 
							
								1123 1125
							 | 
							eqbrtrd | 
							   | 
						
						
							| 1127 | 
							
								1100 1126
							 | 
							jca | 
							   | 
						
						
							| 1128 | 
							
								1127
							 | 
							adantr | 
							   | 
						
						
							| 1129 | 
							
								
							 | 
							sseq1 | 
							   | 
						
						
							| 1130 | 
							
								
							 | 
							fveq2 | 
							   | 
						
						
							| 1131 | 
							
								1130
							 | 
							breq1d | 
							   | 
						
						
							| 1132 | 
							
								1129 1131
							 | 
							anbi12d | 
							   | 
						
						
							| 1133 | 
							
								
							 | 
							itgeq1 | 
							   | 
						
						
							| 1134 | 
							
								1133
							 | 
							fveq2d | 
							   | 
						
						
							| 1135 | 
							
								1134
							 | 
							breq1d | 
							   | 
						
						
							| 1136 | 
							
								1135
							 | 
							ralbidv | 
							   | 
						
						
							| 1137 | 
							
								1132 1136
							 | 
							imbi12d | 
							   | 
						
						
							| 1138 | 
							
								1137
							 | 
							rspcva | 
							   | 
						
						
							| 1139 | 
							
								1080 1128 1138
							 | 
							sylc | 
							   | 
						
						
							| 1140 | 
							
								1139
							 | 
							3adant1 | 
							   | 
						
						
							| 1141 | 
							
								
							 | 
							oveq1 | 
							   | 
						
						
							| 1142 | 
							
								1141
							 | 
							itgeq1d | 
							   | 
						
						
							| 1143 | 
							
								1142
							 | 
							fveq2d | 
							   | 
						
						
							| 1144 | 
							
								1143
							 | 
							breq1d | 
							   | 
						
						
							| 1145 | 
							
								1144
							 | 
							ralbidv | 
							   | 
						
						
							| 1146 | 
							
								1145
							 | 
							rspcev | 
							   | 
						
						
							| 1147 | 
							
								1076 1140 1146
							 | 
							syl2anc | 
							   | 
						
						
							| 1148 | 
							
								1147
							 | 
							rexlimdv3a | 
							   | 
						
						
							| 1149 | 
							
								1030 1148
							 | 
							mpd | 
							   | 
						
						
							| 1150 | 
							
								902 1149
							 | 
							r19.29a | 
							   | 
						
						
							| 1151 | 
							
								1150
							 | 
							ralrimiva | 
							   | 
						
						
							| 1152 | 
							
								
							 | 
							nnex | 
							   | 
						
						
							| 1153 | 
							
								1152
							 | 
							mptex | 
							   | 
						
						
							| 1154 | 
							
								1153
							 | 
							a1i | 
							   | 
						
						
							| 1155 | 
							
								
							 | 
							eqidd | 
							   | 
						
						
							| 1156 | 
							
								784
							 | 
							adantl | 
							   | 
						
						
							| 1157 | 
							
								786
							 | 
							ad4ant14 | 
							   | 
						
						
							| 1158 | 
							
								784
							 | 
							adantl | 
							   | 
						
						
							| 1159 | 
							
								
							 | 
							simpr | 
							   | 
						
						
							| 1160 | 
							
								
							 | 
							simpl | 
							   | 
						
						
							| 1161 | 
							
								1159 1160
							 | 
							eqeltrd | 
							   | 
						
						
							| 1162 | 
							
								1161
							 | 
							nnred | 
							   | 
						
						
							| 1163 | 
							
								737
							 | 
							a1i | 
							   | 
						
						
							| 1164 | 
							
								1162 1163
							 | 
							readdcld | 
							   | 
						
						
							| 1165 | 
							
								1164
							 | 
							adantr | 
							   | 
						
						
							| 1166 | 
							
								232 1158
							 | 
							sselid | 
							   | 
						
						
							| 1167 | 
							
								1165 1166
							 | 
							remulcld | 
							   | 
						
						
							| 1168 | 
							
								1167
							 | 
							resincld | 
							   | 
						
						
							| 1169 | 
							
								1158 1168 837
							 | 
							syl2anc | 
							   | 
						
						
							| 1170 | 
							
								1169
							 | 
							adantlll | 
							   | 
						
						
							| 1171 | 
							
								1162
							 | 
							adantll | 
							   | 
						
						
							| 1172 | 
							
								1171
							 | 
							adantr | 
							   | 
						
						
							| 1173 | 
							
								
							 | 
							1red | 
							   | 
						
						
							| 1174 | 
							
								1173
							 | 
							rehalfcld | 
							   | 
						
						
							| 1175 | 
							
								1172 1174
							 | 
							readdcld | 
							   | 
						
						
							| 1176 | 
							
								232 1156
							 | 
							sselid | 
							   | 
						
						
							| 1177 | 
							
								1175 1176
							 | 
							remulcld | 
							   | 
						
						
							| 1178 | 
							
								1177
							 | 
							resincld | 
							   | 
						
						
							| 1179 | 
							
								1170 1178
							 | 
							eqeltrd | 
							   | 
						
						
							| 1180 | 
							
								1157 1179
							 | 
							remulcld | 
							   | 
						
						
							| 1181 | 
							
								17
							 | 
							fvmpt2 | 
							   | 
						
						
							| 1182 | 
							
								1156 1180 1181
							 | 
							syl2anc | 
							   | 
						
						
							| 1183 | 
							
								
							 | 
							oveq1 | 
							   | 
						
						
							| 1184 | 
							
								1183
							 | 
							oveq1d | 
							   | 
						
						
							| 1185 | 
							
								1184
							 | 
							fveq2d | 
							   | 
						
						
							| 1186 | 
							
								1185
							 | 
							ad2antlr | 
							   | 
						
						
							| 1187 | 
							
								1170 1186
							 | 
							eqtrd | 
							   | 
						
						
							| 1188 | 
							
								1187
							 | 
							oveq2d | 
							   | 
						
						
							| 1189 | 
							
								1182 1188
							 | 
							eqtrd | 
							   | 
						
						
							| 1190 | 
							
								1189
							 | 
							itgeq2dv | 
							   | 
						
						
							| 1191 | 
							
								
							 | 
							simpr | 
							   | 
						
						
							| 1192 | 
							
								817
							 | 
							itgeq2dv | 
							   | 
						
						
							| 1193 | 
							
								1192
							 | 
							eleq1d | 
							   | 
						
						
							| 1194 | 
							
								812 1193
							 | 
							imbi12d | 
							   | 
						
						
							| 1195 | 
							
								786
							 | 
							adantlr | 
							   | 
						
						
							| 1196 | 
							
								
							 | 
							simpr | 
							   | 
						
						
							| 1197 | 
							
								1196 784 833
							 | 
							syl2an | 
							   | 
						
						
							| 1198 | 
							
								1195 1197
							 | 
							remulcld | 
							   | 
						
						
							| 1199 | 
							
								1198 860
							 | 
							itgcl | 
							   | 
						
						
							| 1200 | 
							
								1194 1199
							 | 
							chvarvv | 
							   | 
						
						
							| 1201 | 
							
								1155 1190 1191 1200
							 | 
							fvmptd | 
							   | 
						
						
							| 1202 | 
							
								39 33 1154 1201 1200
							 | 
							clim0c | 
							   | 
						
						
							| 1203 | 
							
								1151 1202
							 | 
							mpbird | 
							   | 
						
						
							| 1204 | 
							
								1152
							 | 
							mptex | 
							   | 
						
						
							| 1205 | 
							
								19 1204
							 | 
							eqeltri | 
							   | 
						
						
							| 1206 | 
							
								1205
							 | 
							a1i | 
							   | 
						
						
							| 1207 | 
							
								1152
							 | 
							mptex | 
							   | 
						
						
							| 1208 | 
							
								1207
							 | 
							a1i | 
							   | 
						
						
							| 1209 | 
							
								
							 | 
							picn | 
							   | 
						
						
							| 1210 | 
							
								1209
							 | 
							a1i | 
							   | 
						
						
							| 1211 | 
							
								
							 | 
							eqidd | 
							   | 
						
						
							| 1212 | 
							
								
							 | 
							eqidd | 
							   | 
						
						
							| 1213 | 
							
								
							 | 
							id | 
							   | 
						
						
							| 1214 | 
							
								40
							 | 
							a1i | 
							   | 
						
						
							| 1215 | 
							
								1211 1212 1213 1214
							 | 
							fvmptd | 
							   | 
						
						
							| 1216 | 
							
								1215
							 | 
							adantl | 
							   | 
						
						
							| 1217 | 
							
								39 33 1208 1210 1216
							 | 
							climconst | 
							   | 
						
						
							| 1218 | 
							
								778 79
							 | 
							gtneii | 
							   | 
						
						
							| 1219 | 
							
								1218
							 | 
							a1i | 
							   | 
						
						
							| 1220 | 
							
								2
							 | 
							adantr | 
							   | 
						
						
							| 1221 | 
							
								55
							 | 
							adantr | 
							   | 
						
						
							| 1222 | 
							
								65
							 | 
							adantr | 
							   | 
						
						
							| 1223 | 
							
								843 1220 1221 1222 13 14 15 847 16 17
							 | 
							fourierdlem67 | 
							   | 
						
						
							| 1224 | 
							
								1223
							 | 
							adantr | 
							   | 
						
						
							| 1225 | 
							
								821
							 | 
							sselda | 
							   | 
						
						
							| 1226 | 
							
								1224 1225
							 | 
							ffvelcdmd | 
							   | 
						
						
							| 1227 | 
							
								1223
							 | 
							ffvelcdmda | 
							   | 
						
						
							| 1228 | 
							
								1223
							 | 
							feqmptd | 
							   | 
						
						
							| 1229 | 
							
								1228 858
							 | 
							eqeltrrd | 
							   | 
						
						
							| 1230 | 
							
								821 823 1227 1229
							 | 
							iblss | 
							   | 
						
						
							| 1231 | 
							
								1226 1230
							 | 
							itgcl | 
							   | 
						
						
							| 1232 | 
							
								
							 | 
							eqid | 
							   | 
						
						
							| 1233 | 
							
								1232
							 | 
							fvmpt2 | 
							   | 
						
						
							| 1234 | 
							
								1196 1231 1233
							 | 
							syl2anc | 
							   | 
						
						
							| 1235 | 
							
								1234 1231
							 | 
							eqeltrd | 
							   | 
						
						
							| 1236 | 
							
								
							 | 
							id | 
							   | 
						
						
							| 1237 | 
							
								
							 | 
							eqid | 
							   | 
						
						
							| 1238 | 
							
								1237
							 | 
							fvmpt2 | 
							   | 
						
						
							| 1239 | 
							
								1236 40 1238
							 | 
							sylancl | 
							   | 
						
						
							| 1240 | 
							
								1209
							 | 
							a1i | 
							   | 
						
						
							| 1241 | 
							
								1218
							 | 
							a1i | 
							   | 
						
						
							| 1242 | 
							
								1240 1241
							 | 
							jca | 
							   | 
						
						
							| 1243 | 
							
								
							 | 
							eldifsn | 
							   | 
						
						
							| 1244 | 
							
								1242 1243
							 | 
							sylibr | 
							   | 
						
						
							| 1245 | 
							
								1239 1244
							 | 
							eqeltrd | 
							   | 
						
						
							| 1246 | 
							
								1245
							 | 
							adantl | 
							   | 
						
						
							| 1247 | 
							
								1209
							 | 
							a1i | 
							   | 
						
						
							| 1248 | 
							
								1218
							 | 
							a1i | 
							   | 
						
						
							| 1249 | 
							
								1231 1247 1248
							 | 
							divcld | 
							   | 
						
						
							| 1250 | 
							
								19
							 | 
							fvmpt2 | 
							   | 
						
						
							| 1251 | 
							
								1196 1249 1250
							 | 
							syl2anc | 
							   | 
						
						
							| 1252 | 
							
								1234
							 | 
							eqcomd | 
							   | 
						
						
							| 1253 | 
							
								1239
							 | 
							eqcomd | 
							   | 
						
						
							| 1254 | 
							
								1253
							 | 
							adantl | 
							   | 
						
						
							| 1255 | 
							
								1252 1254
							 | 
							oveq12d | 
							   | 
						
						
							| 1256 | 
							
								1251 1255
							 | 
							eqtrd | 
							   | 
						
						
							| 1257 | 
							
								34 35 36 38 39 33 1203 1206 1217 1219 1235 1246 1256
							 | 
							climdivf | 
							   | 
						
						
							| 1258 | 
							
								1209 1218
							 | 
							div0i | 
							   | 
						
						
							| 1259 | 
							
								1258
							 | 
							a1i | 
							   | 
						
						
							| 1260 | 
							
								1257 1259
							 | 
							breqtrd | 
							   | 
						
						
							| 1261 | 
							
								1152
							 | 
							mptex | 
							   | 
						
						
							| 1262 | 
							
								18 1261
							 | 
							eqeltri | 
							   | 
						
						
							| 1263 | 
							
								1262
							 | 
							a1i | 
							   | 
						
						
							| 1264 | 
							
								1152
							 | 
							mptex | 
							   | 
						
						
							| 1265 | 
							
								1264
							 | 
							a1i | 
							   | 
						
						
							| 1266 | 
							
								
							 | 
							limccl | 
							   | 
						
						
							| 1267 | 
							
								1266 21
							 | 
							sselid | 
							   | 
						
						
							| 1268 | 
							
								1267
							 | 
							halfcld | 
							   | 
						
						
							| 1269 | 
							
								
							 | 
							eqidd | 
							   | 
						
						
							| 1270 | 
							
								
							 | 
							eqidd | 
							   | 
						
						
							| 1271 | 
							
								39
							 | 
							eqcomi | 
							   | 
						
						
							| 1272 | 
							
								1271
							 | 
							eleq2i | 
							   | 
						
						
							| 1273 | 
							
								1272
							 | 
							biimpi | 
							   | 
						
						
							| 1274 | 
							
								1273
							 | 
							adantl | 
							   | 
						
						
							| 1275 | 
							
								1268
							 | 
							adantr | 
							   | 
						
						
							| 1276 | 
							
								1269 1270 1274 1275
							 | 
							fvmptd | 
							   | 
						
						
							| 1277 | 
							
								32 33 1265 1268 1276
							 | 
							climconst | 
							   | 
						
						
							| 1278 | 
							
								1249 19
							 | 
							fmptd | 
							   | 
						
						
							| 1279 | 
							
								1278
							 | 
							adantr | 
							   | 
						
						
							| 1280 | 
							
								1279 1274
							 | 
							ffvelcdmd | 
							   | 
						
						
							| 1281 | 
							
								1276 1275
							 | 
							eqeltrd | 
							   | 
						
						
							| 1282 | 
							
								1276
							 | 
							oveq2d | 
							   | 
						
						
							| 1283 | 
							
								822
							 | 
							a1i | 
							   | 
						
						
							| 1284 | 
							
								75
							 | 
							a1i | 
							   | 
						
						
							| 1285 | 
							
								
							 | 
							0red | 
							   | 
						
						
							| 1286 | 
							
								1285
							 | 
							rexrd | 
							   | 
						
						
							| 1287 | 
							
								
							 | 
							id | 
							   | 
						
						
							| 1288 | 
							
								
							 | 
							iooltub | 
							   | 
						
						
							| 1289 | 
							
								1284 1286 1287 1288
							 | 
							syl3anc | 
							   | 
						
						
							| 1290 | 
							
								794 1289
							 | 
							ltned | 
							   | 
						
						
							| 1291 | 
							
								1290
							 | 
							neneqd | 
							   | 
						
						
							| 1292 | 
							
								
							 | 
							velsn | 
							   | 
						
						
							| 1293 | 
							
								1291 1292
							 | 
							sylnibr | 
							   | 
						
						
							| 1294 | 
							
								784 1293
							 | 
							eldifd | 
							   | 
						
						
							| 1295 | 
							
								1294
							 | 
							ssriv | 
							   | 
						
						
							| 1296 | 
							
								1295
							 | 
							a1i | 
							   | 
						
						
							| 1297 | 
							
								794
							 | 
							adantl | 
							   | 
						
						
							| 1298 | 
							
								
							 | 
							0red | 
							   | 
						
						
							| 1299 | 
							
								794 1285 1289
							 | 
							ltled | 
							   | 
						
						
							| 1300 | 
							
								1299
							 | 
							adantl | 
							   | 
						
						
							| 1301 | 
							
								1297 1298 1300
							 | 
							lensymd | 
							   | 
						
						
							| 1302 | 
							
								1301
							 | 
							iffalsed | 
							   | 
						
						
							| 1303 | 
							
								
							 | 
							eqid | 
							   | 
						
						
							| 1304 | 
							
								41
							 | 
							a1i | 
							   | 
						
						
							| 1305 | 
							
								
							 | 
							0red | 
							   | 
						
						
							| 1306 | 
							
								41 778 903
							 | 
							ltleii | 
							   | 
						
						
							| 1307 | 
							
								1306
							 | 
							a1i | 
							   | 
						
						
							| 1308 | 
							
								
							 | 
							eqid | 
							   | 
						
						
							| 1309 | 
							
								24 1196 1303 1304 1305 1307 1308
							 | 
							dirkeritg | 
							   | 
						
						
							| 1310 | 
							
								
							 | 
							ubicc2 | 
							   | 
						
						
							| 1311 | 
							
								75 76 1306 1310
							 | 
							mp3an | 
							   | 
						
						
							| 1312 | 
							
								
							 | 
							oveq1 | 
							   | 
						
						
							| 1313 | 
							
								257 262
							 | 
							div0i | 
							   | 
						
						
							| 1314 | 
							
								1313
							 | 
							a1i | 
							   | 
						
						
							| 1315 | 
							
								1312 1314
							 | 
							eqtrd | 
							   | 
						
						
							| 1316 | 
							
								
							 | 
							oveq2 | 
							   | 
						
						
							| 1317 | 
							
								
							 | 
							elfzelz | 
							   | 
						
						
							| 1318 | 
							
								1317
							 | 
							zcnd | 
							   | 
						
						
							| 1319 | 
							
								1318
							 | 
							mul01d | 
							   | 
						
						
							| 1320 | 
							
								1316 1319
							 | 
							sylan9eq | 
							   | 
						
						
							| 1321 | 
							
								1320
							 | 
							fveq2d | 
							   | 
						
						
							| 1322 | 
							
								
							 | 
							sin0 | 
							   | 
						
						
							| 1323 | 
							
								1322
							 | 
							a1i | 
							   | 
						
						
							| 1324 | 
							
								1321 1323
							 | 
							eqtrd | 
							   | 
						
						
							| 1325 | 
							
								1324
							 | 
							oveq1d | 
							   | 
						
						
							| 1326 | 
							
								
							 | 
							0red | 
							   | 
						
						
							| 1327 | 
							
								
							 | 
							1red | 
							   | 
						
						
							| 1328 | 
							
								1317
							 | 
							zred | 
							   | 
						
						
							| 1329 | 
							
								118
							 | 
							a1i | 
							   | 
						
						
							| 1330 | 
							
								
							 | 
							elfzle1 | 
							   | 
						
						
							| 1331 | 
							
								1326 1327 1328 1329 1330
							 | 
							ltletrd | 
							   | 
						
						
							| 1332 | 
							
								1331
							 | 
							gt0ne0d | 
							   | 
						
						
							| 1333 | 
							
								1318 1332
							 | 
							div0d | 
							   | 
						
						
							| 1334 | 
							
								1333
							 | 
							adantl | 
							   | 
						
						
							| 1335 | 
							
								1325 1334
							 | 
							eqtrd | 
							   | 
						
						
							| 1336 | 
							
								1335
							 | 
							sumeq2dv | 
							   | 
						
						
							| 1337 | 
							
								
							 | 
							fzfi | 
							   | 
						
						
							| 1338 | 
							
								1337
							 | 
							olci | 
							   | 
						
						
							| 1339 | 
							
								
							 | 
							sumz | 
							   | 
						
						
							| 1340 | 
							
								1338 1339
							 | 
							ax-mp | 
							   | 
						
						
							| 1341 | 
							
								1340
							 | 
							a1i | 
							   | 
						
						
							| 1342 | 
							
								1336 1341
							 | 
							eqtrd | 
							   | 
						
						
							| 1343 | 
							
								1315 1342
							 | 
							oveq12d | 
							   | 
						
						
							| 1344 | 
							
								
							 | 
							00id | 
							   | 
						
						
							| 1345 | 
							
								1344
							 | 
							a1i | 
							   | 
						
						
							| 1346 | 
							
								1343 1345
							 | 
							eqtrd | 
							   | 
						
						
							| 1347 | 
							
								1346
							 | 
							oveq1d | 
							   | 
						
						
							| 1348 | 
							
								1258
							 | 
							a1i | 
							   | 
						
						
							| 1349 | 
							
								1347 1348
							 | 
							eqtrd | 
							   | 
						
						
							| 1350 | 
							
								778
							 | 
							elexi | 
							   | 
						
						
							| 1351 | 
							
								1349 1308 1350
							 | 
							fvmpt | 
							   | 
						
						
							| 1352 | 
							
								1311 1351
							 | 
							ax-mp | 
							   | 
						
						
							| 1353 | 
							
								
							 | 
							lbicc2 | 
							   | 
						
						
							| 1354 | 
							
								75 76 1306 1353
							 | 
							mp3an | 
							   | 
						
						
							| 1355 | 
							
								
							 | 
							oveq1 | 
							   | 
						
						
							| 1356 | 
							
								
							 | 
							oveq2 | 
							   | 
						
						
							| 1357 | 
							
								1356
							 | 
							fveq2d | 
							   | 
						
						
							| 1358 | 
							
								1357
							 | 
							oveq1d | 
							   | 
						
						
							| 1359 | 
							
								1358
							 | 
							sumeq2sdv | 
							   | 
						
						
							| 1360 | 
							
								1355 1359
							 | 
							oveq12d | 
							   | 
						
						
							| 1361 | 
							
								1360
							 | 
							oveq1d | 
							   | 
						
						
							| 1362 | 
							
								
							 | 
							ovex | 
							   | 
						
						
							| 1363 | 
							
								1361 1308 1362
							 | 
							fvmpt | 
							   | 
						
						
							| 1364 | 
							
								1354 1363
							 | 
							ax-mp | 
							   | 
						
						
							| 1365 | 
							
								
							 | 
							mulneg12 | 
							   | 
						
						
							| 1366 | 
							
								1318 1209 1365
							 | 
							sylancl | 
							   | 
						
						
							| 1367 | 
							
								1366
							 | 
							eqcomd | 
							   | 
						
						
							| 1368 | 
							
								1367
							 | 
							oveq1d | 
							   | 
						
						
							| 1369 | 
							
								1318
							 | 
							negcld | 
							   | 
						
						
							| 1370 | 
							
								1209
							 | 
							a1i | 
							   | 
						
						
							| 1371 | 
							
								1218
							 | 
							a1i | 
							   | 
						
						
							| 1372 | 
							
								1369 1370 1371
							 | 
							divcan4d | 
							   | 
						
						
							| 1373 | 
							
								1368 1372
							 | 
							eqtrd | 
							   | 
						
						
							| 1374 | 
							
								1317
							 | 
							znegcld | 
							   | 
						
						
							| 1375 | 
							
								1373 1374
							 | 
							eqeltrd | 
							   | 
						
						
							| 1376 | 
							
								
							 | 
							negpicn | 
							   | 
						
						
							| 1377 | 
							
								1376
							 | 
							a1i | 
							   | 
						
						
							| 1378 | 
							
								1318 1377
							 | 
							mulcld | 
							   | 
						
						
							| 1379 | 
							
								
							 | 
							sineq0 | 
							   | 
						
						
							| 1380 | 
							
								1378 1379
							 | 
							syl | 
							   | 
						
						
							| 1381 | 
							
								1375 1380
							 | 
							mpbird | 
							   | 
						
						
							| 1382 | 
							
								1381
							 | 
							oveq1d | 
							   | 
						
						
							| 1383 | 
							
								1382 1333
							 | 
							eqtrd | 
							   | 
						
						
							| 1384 | 
							
								1383
							 | 
							sumeq2i | 
							   | 
						
						
							| 1385 | 
							
								1384 1340
							 | 
							eqtri | 
							   | 
						
						
							| 1386 | 
							
								1385
							 | 
							oveq2i | 
							   | 
						
						
							| 1387 | 
							
								1386
							 | 
							oveq1i | 
							   | 
						
						
							| 1388 | 
							
								1376 257 262
							 | 
							divcli | 
							   | 
						
						
							| 1389 | 
							
								1388
							 | 
							addridi | 
							   | 
						
						
							| 1390 | 
							
								
							 | 
							divneg | 
							   | 
						
						
							| 1391 | 
							
								1209 257 262 1390
							 | 
							mp3an | 
							   | 
						
						
							| 1392 | 
							
								1389 1391
							 | 
							eqtr4i | 
							   | 
						
						
							| 1393 | 
							
								1392
							 | 
							oveq1i | 
							   | 
						
						
							| 1394 | 
							
								1040
							 | 
							recni | 
							   | 
						
						
							| 1395 | 
							
								
							 | 
							divneg | 
							   | 
						
						
							| 1396 | 
							
								1394 1209 1218 1395
							 | 
							mp3an | 
							   | 
						
						
							| 1397 | 
							
								1396
							 | 
							eqcomi | 
							   | 
						
						
							| 1398 | 
							
								1209 257 1209 262 1218
							 | 
							divdiv32i | 
							   | 
						
						
							| 1399 | 
							
								1209 1218
							 | 
							dividi | 
							   | 
						
						
							| 1400 | 
							
								1399
							 | 
							oveq1i | 
							   | 
						
						
							| 1401 | 
							
								1398 1400
							 | 
							eqtri | 
							   | 
						
						
							| 1402 | 
							
								1401
							 | 
							negeqi | 
							   | 
						
						
							| 1403 | 
							
								1393 1397 1402
							 | 
							3eqtri | 
							   | 
						
						
							| 1404 | 
							
								1364 1387 1403
							 | 
							3eqtri | 
							   | 
						
						
							| 1405 | 
							
								1352 1404
							 | 
							oveq12i | 
							   | 
						
						
							| 1406 | 
							
								1405
							 | 
							a1i | 
							   | 
						
						
							| 1407 | 
							
								
							 | 
							halfcn | 
							   | 
						
						
							| 1408 | 
							
								1118 1407
							 | 
							subnegi | 
							   | 
						
						
							| 1409 | 
							
								1407
							 | 
							addlidi | 
							   | 
						
						
							| 1410 | 
							
								1408 1409
							 | 
							eqtri | 
							   | 
						
						
							| 1411 | 
							
								1410
							 | 
							a1i | 
							   | 
						
						
							| 1412 | 
							
								1309 1406 1411
							 | 
							3eqtrd | 
							   | 
						
						
							| 1413 | 
							
								1 2 3 4 5 6 7 11 12 13 14 15 16 17 854 607 22 23 20 21 1283 1296 19 24 65 1302 1412
							 | 
							fourierdlem95 | 
							   | 
						
						
							| 1414 | 
							
								1274 1413
							 | 
							syldan | 
							   | 
						
						
							| 1415 | 
							
								18
							 | 
							a1i | 
							   | 
						
						
							| 1416 | 
							
								
							 | 
							fveq2 | 
							   | 
						
						
							| 1417 | 
							
								1416
							 | 
							fveq1d | 
							   | 
						
						
							| 1418 | 
							
								1417
							 | 
							oveq2d | 
							   | 
						
						
							| 1419 | 
							
								1418
							 | 
							adantr | 
							   | 
						
						
							| 1420 | 
							
								1419
							 | 
							itgeq2dv | 
							   | 
						
						
							| 1421 | 
							
								1420
							 | 
							adantl | 
							   | 
						
						
							| 1422 | 
							
								1
							 | 
							adantr | 
							   | 
						
						
							| 1423 | 
							
								2
							 | 
							adantr | 
							   | 
						
						
							| 1424 | 
							
								1423 1297
							 | 
							readdcld | 
							   | 
						
						
							| 1425 | 
							
								1422 1424
							 | 
							ffvelcdmd | 
							   | 
						
						
							| 1426 | 
							
								1425
							 | 
							adantlr | 
							   | 
						
						
							| 1427 | 
							
								24
							 | 
							dirkerf | 
							   | 
						
						
							| 1428 | 
							
								1427
							 | 
							ad2antlr | 
							   | 
						
						
							| 1429 | 
							
								794
							 | 
							adantl | 
							   | 
						
						
							| 1430 | 
							
								1428 1429
							 | 
							ffvelcdmd | 
							   | 
						
						
							| 1431 | 
							
								1426 1430
							 | 
							remulcld | 
							   | 
						
						
							| 1432 | 
							
								1
							 | 
							adantr | 
							   | 
						
						
							| 1433 | 
							
								2
							 | 
							adantr | 
							   | 
						
						
							| 1434 | 
							
								232
							 | 
							sseli | 
							   | 
						
						
							| 1435 | 
							
								1434
							 | 
							adantl | 
							   | 
						
						
							| 1436 | 
							
								1433 1435
							 | 
							readdcld | 
							   | 
						
						
							| 1437 | 
							
								1432 1436
							 | 
							ffvelcdmd | 
							   | 
						
						
							| 1438 | 
							
								1437
							 | 
							adantlr | 
							   | 
						
						
							| 1439 | 
							
								1427
							 | 
							ad2antlr | 
							   | 
						
						
							| 1440 | 
							
								1434
							 | 
							adantl | 
							   | 
						
						
							| 1441 | 
							
								1439 1440
							 | 
							ffvelcdmd | 
							   | 
						
						
							| 1442 | 
							
								1438 1441
							 | 
							remulcld | 
							   | 
						
						
							| 1443 | 
							
								40
							 | 
							a1i | 
							   | 
						
						
							| 1444 | 
							
								24
							 | 
							dirkercncf | 
							   | 
						
						
							| 1445 | 
							
								1444
							 | 
							adantl | 
							   | 
						
						
							| 1446 | 
							
								
							 | 
							eqid | 
							   | 
						
						
							| 1447 | 
							
								1304 1443 843 1220 3 848 849 850 851 852 29 853 1445 1446
							 | 
							fourierdlem84 | 
							   | 
						
						
							| 1448 | 
							
								821 823 1442 1447
							 | 
							iblss | 
							   | 
						
						
							| 1449 | 
							
								1431 1448
							 | 
							itgrecl | 
							   | 
						
						
							| 1450 | 
							
								1415 1421 1196 1449
							 | 
							fvmptd | 
							   | 
						
						
							| 1451 | 
							
								1450
							 | 
							eqcomd | 
							   | 
						
						
							| 1452 | 
							
								1274 1451
							 | 
							syldan | 
							   | 
						
						
							| 1453 | 
							
								1282 1414 1452
							 | 
							3eqtrrd | 
							   | 
						
						
							| 1454 | 
							
								32 33 1260 1263 1277 1280 1281 1453
							 | 
							climadd | 
							   | 
						
						
							| 1455 | 
							
								1268
							 | 
							addlidd | 
							   | 
						
						
							| 1456 | 
							
								1454 1455
							 | 
							breqtrd | 
							   |