Metamath Proof Explorer


Theorem gausslemma2dlem1a

Description: Lemma for gausslemma2dlem1 . (Contributed by AV, 1-Jul-2021)

Ref Expression
Hypotheses gausslemma2d.p φ P 2
gausslemma2d.h H = P 1 2
gausslemma2d.r R = x 1 H if x 2 < P 2 x 2 P x 2
Assertion gausslemma2dlem1a φ ran R = 1 H

Proof

Step Hyp Ref Expression
1 gausslemma2d.p φ P 2
2 gausslemma2d.h H = P 1 2
3 gausslemma2d.r R = x 1 H if x 2 < P 2 x 2 P x 2
4 3 elrnmpt y V y ran R x 1 H y = if x 2 < P 2 x 2 P x 2
5 4 elv y ran R x 1 H y = if x 2 < P 2 x 2 P x 2
6 iftrue x 2 < P 2 if x 2 < P 2 x 2 P x 2 = x 2
7 6 eqeq2d x 2 < P 2 y = if x 2 < P 2 x 2 P x 2 y = x 2
8 7 adantr x 2 < P 2 φ x 1 H y = if x 2 < P 2 x 2 P x 2 y = x 2
9 elfz1b x 1 H x H x H
10 id x x
11 2nn 2
12 11 a1i x 2
13 10 12 nnmulcld x x 2
14 13 3ad2ant1 x H x H x 2
15 14 3ad2ant1 x H x H φ x 2 < P 2 x 2
16 2 eleq1i H P 1 2
17 16 biimpi H P 1 2
18 17 3ad2ant2 x H x H P 1 2
19 18 3ad2ant1 x H x H φ x 2 < P 2 P 1 2
20 nnoddn2prm P 2 P ¬ 2 P
21 nnz P P
22 21 anim1i P ¬ 2 P P ¬ 2 P
23 20 22 syl P 2 P ¬ 2 P
24 nnz x x
25 2z 2
26 25 a1i x 2
27 24 26 zmulcld x x 2
28 27 3ad2ant1 x H x H x 2
29 23 28 anim12i P 2 x H x H P ¬ 2 P x 2
30 df-3an P ¬ 2 P x 2 P ¬ 2 P x 2
31 29 30 sylibr P 2 x H x H P ¬ 2 P x 2
32 31 ex P 2 x H x H P ¬ 2 P x 2
33 1 32 syl φ x H x H P ¬ 2 P x 2
34 33 impcom x H x H φ P ¬ 2 P x 2
35 ltoddhalfle P ¬ 2 P x 2 x 2 < P 2 x 2 P 1 2
36 34 35 syl x H x H φ x 2 < P 2 x 2 P 1 2
37 36 biimp3a x H x H φ x 2 < P 2 x 2 P 1 2
38 15 19 37 3jca x H x H φ x 2 < P 2 x 2 P 1 2 x 2 P 1 2
39 38 3exp x H x H φ x 2 < P 2 x 2 P 1 2 x 2 P 1 2
40 9 39 sylbi x 1 H φ x 2 < P 2 x 2 P 1 2 x 2 P 1 2
41 40 impcom φ x 1 H x 2 < P 2 x 2 P 1 2 x 2 P 1 2
42 41 impcom x 2 < P 2 φ x 1 H x 2 P 1 2 x 2 P 1 2
43 2 oveq2i 1 H = 1 P 1 2
44 43 eleq2i x 2 1 H x 2 1 P 1 2
45 elfz1b x 2 1 P 1 2 x 2 P 1 2 x 2 P 1 2
46 44 45 bitri x 2 1 H x 2 P 1 2 x 2 P 1 2
47 42 46 sylibr x 2 < P 2 φ x 1 H x 2 1 H
48 eleq1 y = x 2 y 1 H x 2 1 H
49 47 48 syl5ibrcom x 2 < P 2 φ x 1 H y = x 2 y 1 H
50 8 49 sylbid x 2 < P 2 φ x 1 H y = if x 2 < P 2 x 2 P x 2 y 1 H
51 iffalse ¬ x 2 < P 2 if x 2 < P 2 x 2 P x 2 = P x 2
52 51 eqeq2d ¬ x 2 < P 2 y = if x 2 < P 2 x 2 P x 2 y = P x 2
53 52 adantr ¬ x 2 < P 2 φ x 1 H y = if x 2 < P 2 x 2 P x 2 y = P x 2
54 eldifi P 2 P
55 prmz P P
56 1 54 55 3syl φ P
57 56 ad2antrl ¬ x 2 < P 2 φ x 1 H P
58 elfzelz x 1 H x
59 25 a1i x 1 H 2
60 58 59 zmulcld x 1 H x 2
61 60 ad2antll ¬ x 2 < P 2 φ x 1 H x 2
62 57 61 zsubcld ¬ x 2 < P 2 φ x 1 H P x 2
63 55 zred P P
64 2 breq2i x H x P 1 2
65 nnre x x
66 65 adantr x P x
67 peano2rem P P 1
68 67 adantl x P P 1
69 2re 2
70 2pos 0 < 2
71 69 70 pm3.2i 2 0 < 2
72 71 a1i x P 2 0 < 2
73 lemuldiv x P 1 2 0 < 2 x 2 P 1 x P 1 2
74 66 68 72 73 syl3anc x P x 2 P 1 x P 1 2
75 64 74 bitr4id x P x H x 2 P 1
76 13 nnred x x 2
77 76 adantr x P x 2
78 simpr x P P
79 77 68 78 lesub2d x P x 2 P 1 P P 1 P x 2
80 recn P P
81 1cnd P 1
82 80 81 nncand P P P 1 = 1
83 82 adantl x P P P 1 = 1
84 83 breq1d x P P P 1 P x 2 1 P x 2
85 84 biimpd x P P P 1 P x 2 1 P x 2
86 79 85 sylbid x P x 2 P 1 1 P x 2
87 75 86 sylbid x P x H 1 P x 2
88 87 impancom x x H P 1 P x 2
89 88 3adant2 x H x H P 1 P x 2
90 9 89 sylbi x 1 H P 1 P x 2
91 90 com12 P x 1 H 1 P x 2
92 1 54 63 91 4syl φ x 1 H 1 P x 2
93 92 imp φ x 1 H 1 P x 2
94 93 adantl ¬ x 2 < P 2 φ x 1 H 1 P x 2
95 elnnz1 P x 2 P x 2 1 P x 2
96 62 94 95 sylanbrc ¬ x 2 < P 2 φ x 1 H P x 2
97 9 simp2bi x 1 H H
98 97 ad2antll ¬ x 2 < P 2 φ x 1 H H
99 nnre P P
100 99 rehalfcld P P 2
101 100 adantr P ¬ 2 P P 2
102 60 zred x 1 H x 2
103 lenlt P 2 x 2 P 2 x 2 ¬ x 2 < P 2
104 101 102 103 syl2an P ¬ 2 P x 1 H P 2 x 2 ¬ x 2 < P 2
105 22 60 anim12i P ¬ 2 P x 1 H P ¬ 2 P x 2
106 105 30 sylibr P ¬ 2 P x 1 H P ¬ 2 P x 2
107 halfleoddlt P ¬ 2 P x 2 P 2 x 2 P 2 < x 2
108 106 107 syl P ¬ 2 P x 1 H P 2 x 2 P 2 < x 2
109 108 biimpa P ¬ 2 P x 1 H P 2 x 2 P 2 < x 2
110 nncn P P
111 subhalfhalf P P P 2 = P 2
112 110 111 syl P P P 2 = P 2
113 112 breq1d P P P 2 < x 2 P 2 < x 2
114 113 ad3antrrr P ¬ 2 P x 1 H P 2 x 2 P P 2 < x 2 P 2 < x 2
115 109 114 mpbird P ¬ 2 P x 1 H P 2 x 2 P P 2 < x 2
116 99 ad2antrr P ¬ 2 P x 1 H P
117 100 ad2antrr P ¬ 2 P x 1 H P 2
118 102 adantl P ¬ 2 P x 1 H x 2
119 116 117 118 3jca P ¬ 2 P x 1 H P P 2 x 2
120 119 adantr P ¬ 2 P x 1 H P 2 x 2 P P 2 x 2
121 ltsub23 P P 2 x 2 P P 2 < x 2 P x 2 < P 2
122 120 121 syl P ¬ 2 P x 1 H P 2 x 2 P P 2 < x 2 P x 2 < P 2
123 115 122 mpbid P ¬ 2 P x 1 H P 2 x 2 P x 2 < P 2
124 21 ad2antrr P ¬ 2 P x 1 H P
125 simplr P ¬ 2 P x 1 H ¬ 2 P
126 60 adantl P ¬ 2 P x 1 H x 2
127 124 126 zsubcld P ¬ 2 P x 1 H P x 2
128 124 125 127 3jca P ¬ 2 P x 1 H P ¬ 2 P P x 2
129 128 adantr P ¬ 2 P x 1 H P 2 x 2 P ¬ 2 P P x 2
130 ltoddhalfle P ¬ 2 P P x 2 P x 2 < P 2 P x 2 P 1 2
131 129 130 syl P ¬ 2 P x 1 H P 2 x 2 P x 2 < P 2 P x 2 P 1 2
132 123 131 mpbid P ¬ 2 P x 1 H P 2 x 2 P x 2 P 1 2
133 132 ex P ¬ 2 P x 1 H P 2 x 2 P x 2 P 1 2
134 2 breq2i P x 2 H P x 2 P 1 2
135 133 134 imbitrrdi P ¬ 2 P x 1 H P 2 x 2 P x 2 H
136 104 135 sylbird P ¬ 2 P x 1 H ¬ x 2 < P 2 P x 2 H
137 136 ex P ¬ 2 P x 1 H ¬ x 2 < P 2 P x 2 H
138 1 20 137 3syl φ x 1 H ¬ x 2 < P 2 P x 2 H
139 138 imp φ x 1 H ¬ x 2 < P 2 P x 2 H
140 139 impcom ¬ x 2 < P 2 φ x 1 H P x 2 H
141 elfz1b P x 2 1 H P x 2 H P x 2 H
142 96 98 140 141 syl3anbrc ¬ x 2 < P 2 φ x 1 H P x 2 1 H
143 eleq1 y = P x 2 y 1 H P x 2 1 H
144 142 143 syl5ibrcom ¬ x 2 < P 2 φ x 1 H y = P x 2 y 1 H
145 53 144 sylbid ¬ x 2 < P 2 φ x 1 H y = if x 2 < P 2 x 2 P x 2 y 1 H
146 50 145 pm2.61ian φ x 1 H y = if x 2 < P 2 x 2 P x 2 y 1 H
147 146 rexlimdva φ x 1 H y = if x 2 < P 2 x 2 P x 2 y 1 H
148 elfz1b y 1 H y H y H
149 simp1 y H y H y
150 simpl 2 y φ 2 y
151 nnehalf y 2 y y 2
152 149 150 151 syl2anr 2 y φ y H y H y 2
153 simpr2 2 y φ y H y H H
154 nnre y y
155 154 ad2antrr y H 2 y φ y
156 nnrp H H +
157 156 adantl y H H +
158 157 adantr y H 2 y φ H +
159 2rp 2 +
160 1le2 1 2
161 159 160 pm3.2i 2 + 1 2
162 161 a1i y H 2 y φ 2 + 1 2
163 ledivge1le y H + 2 + 1 2 y H y 2 H
164 155 158 162 163 syl3anc y H 2 y φ y H y 2 H
165 164 ex y H 2 y φ y H y 2 H
166 165 com23 y H y H 2 y φ y 2 H
167 166 3impia y H y H 2 y φ y 2 H
168 167 impcom 2 y φ y H y H y 2 H
169 152 153 168 3jca 2 y φ y H y H y 2 H y 2 H
170 169 ex 2 y φ y H y H y 2 H y 2 H
171 148 170 biimtrid 2 y φ y 1 H y 2 H y 2 H
172 171 3impia 2 y φ y 1 H y 2 H y 2 H
173 elfz1b y 2 1 H y 2 H y 2 H
174 172 173 sylibr 2 y φ y 1 H y 2 1 H
175 oveq1 x = y 2 x 2 = y 2 2
176 175 breq1d x = y 2 x 2 < P 2 y 2 2 < P 2
177 175 oveq2d x = y 2 P x 2 = P y 2 2
178 176 175 177 ifbieq12d x = y 2 if x 2 < P 2 x 2 P x 2 = if y 2 2 < P 2 y 2 2 P y 2 2
179 178 eqeq2d x = y 2 y = if x 2 < P 2 x 2 P x 2 y = if y 2 2 < P 2 y 2 2 P y 2 2
180 179 adantl 2 y φ y 1 H x = y 2 y = if x 2 < P 2 x 2 P x 2 y = if y 2 2 < P 2 y 2 2 P y 2 2
181 elfzelz y 1 H y
182 181 zcnd y 1 H y
183 182 3ad2ant3 2 y φ y 1 H y
184 2cnd 2 y φ y 1 H 2
185 2ne0 2 0
186 185 a1i 2 y φ y 1 H 2 0
187 183 184 186 divcan1d 2 y φ y 1 H y 2 2 = y
188 2 breq2i y H y P 1 2
189 nnz y y
190 1 20 22 3syl φ P ¬ 2 P
191 190 adantl 2 y φ P ¬ 2 P
192 189 191 anim12ci y 2 y φ P ¬ 2 P y
193 df-3an P ¬ 2 P y P ¬ 2 P y
194 192 193 sylibr y 2 y φ P ¬ 2 P y
195 ltoddhalfle P ¬ 2 P y y < P 2 y P 1 2
196 194 195 syl y 2 y φ y < P 2 y P 1 2
197 196 exbiri y 2 y φ y P 1 2 y < P 2
198 197 com23 y y P 1 2 2 y φ y < P 2
199 188 198 biimtrid y y H 2 y φ y < P 2
200 199 a1d y H y H 2 y φ y < P 2
201 200 3imp y H y H 2 y φ y < P 2
202 148 201 sylbi y 1 H 2 y φ y < P 2
203 202 com12 2 y φ y 1 H y < P 2
204 203 3impia 2 y φ y 1 H y < P 2
205 187 204 eqbrtrd 2 y φ y 1 H y 2 2 < P 2
206 205 iftrued 2 y φ y 1 H if y 2 2 < P 2 y 2 2 P y 2 2 = y 2 2
207 206 187 eqtr2d 2 y φ y 1 H y = if y 2 2 < P 2 y 2 2 P y 2 2
208 174 180 207 rspcedvd 2 y φ y 1 H x 1 H y = if x 2 < P 2 x 2 P x 2
209 208 3exp 2 y φ y 1 H x 1 H y = if x 2 < P 2 x 2 P x 2
210 54 55 syl P 2 P
211 210 ad2antrr P 2 ¬ 2 y y H y H P
212 189 3ad2ant1 y H y H y
213 212 adantl P 2 ¬ 2 y y H y H y
214 211 213 zsubcld P 2 ¬ 2 y y H y H P y
215 154 ad2antrl P y H y
216 67 rehalfcld P P 1 2
217 216 adantr P y H P 1 2
218 simpl P y H P
219 215 217 218 3jca P y H y P 1 2 P
220 219 ex P y H y P 1 2 P
221 54 63 220 3syl P 2 y H y P 1 2 P
222 221 adantr P 2 ¬ 2 y y H y P 1 2 P
223 222 impcom y H P 2 ¬ 2 y y P 1 2 P
224 lesub2 y P 1 2 P y P 1 2 P P 1 2 P y
225 223 224 syl y H P 2 ¬ 2 y y P 1 2 P P 1 2 P y
226 55 zcnd P P
227 1cnd P 1
228 2cnne0 2 2 0
229 228 a1i P 2 2 0
230 divsubdir P 1 2 2 0 P 1 2 = P 2 1 2
231 227 229 230 mpd3an23 P P 1 2 = P 2 1 2
232 231 oveq2d P P P 1 2 = P P 2 1 2
233 id P P
234 halfcl P P 2
235 halfcn 1 2
236 235 a1i P 1 2
237 233 234 236 subsubd P P P 2 1 2 = P - P 2 + 1 2
238 111 oveq1d P P - P 2 + 1 2 = P 2 + 1 2
239 232 237 238 3eqtrd P P P 1 2 = P 2 + 1 2
240 54 226 239 3syl P 2 P P 1 2 = P 2 + 1 2
241 240 ad2antrl y H P 2 ¬ 2 y P P 1 2 = P 2 + 1 2
242 241 breq1d y H P 2 ¬ 2 y P P 1 2 P y P 2 + 1 2 P y
243 prmnn P P
244 halfre 1 2
245 244 a1i P 1 2
246 nngt0 P 0 < P
247 71 a1i P 2 0 < 2
248 divgt0 P 0 < P 2 0 < 2 0 < P 2
249 99 246 247 248 syl21anc P 0 < P 2
250 halfgt0 0 < 1 2
251 250 a1i P 0 < 1 2
252 100 245 249 251 addgt0d P 0 < P 2 + 1 2
253 54 243 252 3syl P 2 0 < P 2 + 1 2
254 253 ad2antrl y H P 2 ¬ 2 y 0 < P 2 + 1 2
255 0red y P 0
256 simpr y P P
257 256 rehalfcld y P P 2
258 244 a1i y P 1 2
259 257 258 readdcld y P P 2 + 1 2
260 resubcl P y P y
261 260 ancoms y P P y
262 255 259 261 3jca y P 0 P 2 + 1 2 P y
263 262 ex y P 0 P 2 + 1 2 P y
264 154 263 syl y P 0 P 2 + 1 2 P y
265 264 adantr y H P 0 P 2 + 1 2 P y
266 265 com12 P y H 0 P 2 + 1 2 P y
267 54 63 266 3syl P 2 y H 0 P 2 + 1 2 P y
268 267 adantr P 2 ¬ 2 y y H 0 P 2 + 1 2 P y
269 268 impcom y H P 2 ¬ 2 y 0 P 2 + 1 2 P y
270 ltletr 0 P 2 + 1 2 P y 0 < P 2 + 1 2 P 2 + 1 2 P y 0 < P y
271 269 270 syl y H P 2 ¬ 2 y 0 < P 2 + 1 2 P 2 + 1 2 P y 0 < P y
272 254 271 mpand y H P 2 ¬ 2 y P 2 + 1 2 P y 0 < P y
273 242 272 sylbid y H P 2 ¬ 2 y P P 1 2 P y 0 < P y
274 225 273 sylbid y H P 2 ¬ 2 y y P 1 2 0 < P y
275 274 ex y H P 2 ¬ 2 y y P 1 2 0 < P y
276 275 com23 y H y P 1 2 P 2 ¬ 2 y 0 < P y
277 188 276 biimtrid y H y H P 2 ¬ 2 y 0 < P y
278 277 3impia y H y H P 2 ¬ 2 y 0 < P y
279 278 impcom P 2 ¬ 2 y y H y H 0 < P y
280 elnnz P y P y 0 < P y
281 214 279 280 sylanbrc P 2 ¬ 2 y y H y H P y
282 23 adantr P 2 ¬ 2 y P ¬ 2 P
283 simpr P 2 ¬ 2 y ¬ 2 y
284 283 212 anim12ci P 2 ¬ 2 y y H y H y ¬ 2 y
285 omoe P ¬ 2 P y ¬ 2 y 2 P y
286 282 284 285 syl2an2r P 2 ¬ 2 y y H y H 2 P y
287 nnehalf P y 2 P y P y 2
288 281 286 287 syl2anc P 2 ¬ 2 y y H y H P y 2
289 simpr2 P 2 ¬ 2 y y H y H H
290 1red P 2 ¬ 2 y y H y H 1
291 154 3ad2ant1 y H y H y
292 291 adantl P 2 ¬ 2 y y H y H y
293 54 63 syl P 2 P
294 293 ad2antrr P 2 ¬ 2 y y H y H P
295 nnge1 y 1 y
296 295 3ad2ant1 y H y H 1 y
297 296 adantl P 2 ¬ 2 y y H y H 1 y
298 290 292 294 297 lesub2dd P 2 ¬ 2 y y H y H P y P 1
299 294 292 resubcld P 2 ¬ 2 y y H y H P y
300 54 63 67 3syl P 2 P 1
301 300 ad2antrr P 2 ¬ 2 y y H y H P 1
302 71 a1i P 2 ¬ 2 y y H y H 2 0 < 2
303 lediv1 P y P 1 2 0 < 2 P y P 1 P y 2 P 1 2
304 299 301 302 303 syl3anc P 2 ¬ 2 y y H y H P y P 1 P y 2 P 1 2
305 298 304 mpbid P 2 ¬ 2 y y H y H P y 2 P 1 2
306 2 breq2i P y 2 H P y 2 P 1 2
307 305 306 sylibr P 2 ¬ 2 y y H y H P y 2 H
308 288 289 307 3jca P 2 ¬ 2 y y H y H P y 2 H P y 2 H
309 308 ex P 2 ¬ 2 y y H y H P y 2 H P y 2 H
310 elfz1b P y 2 1 H P y 2 H P y 2 H
311 309 148 310 3imtr4g P 2 ¬ 2 y y 1 H P y 2 1 H
312 311 ex P 2 ¬ 2 y y 1 H P y 2 1 H
313 1 312 syl φ ¬ 2 y y 1 H P y 2 1 H
314 313 3imp21 ¬ 2 y φ y 1 H P y 2 1 H
315 oveq1 x = P y 2 x 2 = P y 2 2
316 315 breq1d x = P y 2 x 2 < P 2 P y 2 2 < P 2
317 315 oveq2d x = P y 2 P x 2 = P P y 2 2
318 316 315 317 ifbieq12d x = P y 2 if x 2 < P 2 x 2 P x 2 = if P y 2 2 < P 2 P y 2 2 P P y 2 2
319 318 eqeq2d x = P y 2 y = if x 2 < P 2 x 2 P x 2 y = if P y 2 2 < P 2 P y 2 2 P P y 2 2
320 319 adantl ¬ 2 y φ y 1 H x = P y 2 y = if x 2 < P 2 x 2 P x 2 y = if P y 2 2 < P 2 P y 2 2 P P y 2 2
321 1 54 226 3syl φ P
322 321 3ad2ant2 ¬ 2 y φ y 1 H P
323 182 3ad2ant3 ¬ 2 y φ y 1 H y
324 322 323 subcld ¬ 2 y φ y 1 H P y
325 2cnd ¬ 2 y φ y 1 H 2
326 185 a1i ¬ 2 y φ y 1 H 2 0
327 324 325 326 divcan1d ¬ 2 y φ y 1 H P y 2 2 = P y
328 zre P P
329 halfge0 0 1 2
330 rehalfcl P P 2
331 330 adantl y P P 2
332 331 258 subge02d y P 0 1 2 P 2 1 2 P 2
333 329 332 mpbii y P P 2 1 2 P 2
334 simpl y P y
335 244 a1i P 1 2
336 330 335 resubcld P P 2 1 2
337 336 adantl y P P 2 1 2
338 letr y P 2 1 2 P 2 y P 2 1 2 P 2 1 2 P 2 y P 2
339 334 337 331 338 syl3anc y P y P 2 1 2 P 2 1 2 P 2 y P 2
340 333 339 mpan2d y P y P 2 1 2 y P 2
341 80 adantl y P P
342 1cnd y P 1
343 228 a1i y P 2 2 0
344 341 342 343 230 syl3anc y P P 1 2 = P 2 1 2
345 344 breq2d y P y P 1 2 y P 2 1 2
346 lesub P 2 P y P 2 P y y P P 2
347 331 256 334 346 syl3anc y P P 2 P y y P P 2
348 257 261 lenltd y P P 2 P y ¬ P y < P 2
349 2cnd P 2
350 185 a1i P 2 0
351 80 349 350 divcan1d P P 2 2 = P
352 351 eqcomd P P = P 2 2
353 352 oveq1d P P P 2 = P 2 2 P 2
354 330 recnd P P 2
355 354 349 mulcomd P P 2 2 = 2 P 2
356 355 oveq1d P P 2 2 P 2 = 2 P 2 P 2
357 349 354 mulsubfacd P 2 P 2 P 2 = 2 1 P 2
358 2m1e1 2 1 = 1
359 358 a1i P 2 1 = 1
360 359 oveq1d P 2 1 P 2 = 1 P 2
361 354 mullidd P 1 P 2 = P 2
362 357 360 361 3eqtrd P 2 P 2 P 2 = P 2
363 353 356 362 3eqtrd P P P 2 = P 2
364 363 adantl y P P P 2 = P 2
365 364 breq2d y P y P P 2 y P 2
366 347 348 365 3bitr3d y P ¬ P y < P 2 y P 2
367 340 345 366 3imtr4d y P y P 1 2 ¬ P y < P 2
368 367 ex y P y P 1 2 ¬ P y < P 2
369 154 368 syl y P y P 1 2 ¬ P y < P 2
370 369 com3l P y P 1 2 y ¬ P y < P 2
371 328 370 syl P y P 1 2 y ¬ P y < P 2
372 1 54 55 371 4syl φ y P 1 2 y ¬ P y < P 2
373 372 adantl ¬ 2 y φ y P 1 2 y ¬ P y < P 2
374 373 com13 y y P 1 2 ¬ 2 y φ ¬ P y < P 2
375 188 374 biimtrid y y H ¬ 2 y φ ¬ P y < P 2
376 375 a1d y H y H ¬ 2 y φ ¬ P y < P 2
377 376 3imp y H y H ¬ 2 y φ ¬ P y < P 2
378 377 com12 ¬ 2 y φ y H y H ¬ P y < P 2
379 148 378 biimtrid ¬ 2 y φ y 1 H ¬ P y < P 2
380 379 3impia ¬ 2 y φ y 1 H ¬ P y < P 2
381 327 380 eqnbrtrd ¬ 2 y φ y 1 H ¬ P y 2 2 < P 2
382 381 iffalsed ¬ 2 y φ y 1 H if P y 2 2 < P 2 P y 2 2 P P y 2 2 = P P y 2 2
383 327 oveq2d ¬ 2 y φ y 1 H P P y 2 2 = P P y
384 321 182 anim12i φ y 1 H P y
385 384 3adant1 ¬ 2 y φ y 1 H P y
386 nncan P y P P y = y
387 385 386 syl ¬ 2 y φ y 1 H P P y = y
388 382 383 387 3eqtrrd ¬ 2 y φ y 1 H y = if P y 2 2 < P 2 P y 2 2 P P y 2 2
389 314 320 388 rspcedvd ¬ 2 y φ y 1 H x 1 H y = if x 2 < P 2 x 2 P x 2
390 389 3exp ¬ 2 y φ y 1 H x 1 H y = if x 2 < P 2 x 2 P x 2
391 209 390 pm2.61i φ y 1 H x 1 H y = if x 2 < P 2 x 2 P x 2
392 147 391 impbid φ x 1 H y = if x 2 < P 2 x 2 P x 2 y 1 H
393 5 392 bitrid φ y ran R y 1 H
394 393 eqrdv φ ran R = 1 H