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 63 91 syl P x 1 H 1 P x 2
93 1 54 92 3syl φ x 1 H 1 P x 2
94 93 imp φ x 1 H 1 P x 2
95 94 adantl ¬ x 2 < P 2 φ x 1 H 1 P x 2
96 elnnz1 P x 2 P x 2 1 P x 2
97 62 95 96 sylanbrc ¬ x 2 < P 2 φ x 1 H P x 2
98 9 simp2bi x 1 H H
99 98 ad2antll ¬ x 2 < P 2 φ x 1 H H
100 nnre P P
101 100 rehalfcld P P 2
102 101 adantr P ¬ 2 P P 2
103 60 zred x 1 H x 2
104 lenlt P 2 x 2 P 2 x 2 ¬ x 2 < P 2
105 102 103 104 syl2an P ¬ 2 P x 1 H P 2 x 2 ¬ x 2 < P 2
106 22 60 anim12i P ¬ 2 P x 1 H P ¬ 2 P x 2
107 106 30 sylibr P ¬ 2 P x 1 H P ¬ 2 P x 2
108 halfleoddlt P ¬ 2 P x 2 P 2 x 2 P 2 < x 2
109 107 108 syl P ¬ 2 P x 1 H P 2 x 2 P 2 < x 2
110 109 biimpa P ¬ 2 P x 1 H P 2 x 2 P 2 < x 2
111 nncn P P
112 subhalfhalf P P P 2 = P 2
113 111 112 syl P P P 2 = P 2
114 113 breq1d P P P 2 < x 2 P 2 < x 2
115 114 ad3antrrr P ¬ 2 P x 1 H P 2 x 2 P P 2 < x 2 P 2 < x 2
116 110 115 mpbird P ¬ 2 P x 1 H P 2 x 2 P P 2 < x 2
117 100 ad2antrr P ¬ 2 P x 1 H P
118 101 ad2antrr P ¬ 2 P x 1 H P 2
119 103 adantl P ¬ 2 P x 1 H x 2
120 117 118 119 3jca P ¬ 2 P x 1 H P P 2 x 2
121 120 adantr P ¬ 2 P x 1 H P 2 x 2 P P 2 x 2
122 ltsub23 P P 2 x 2 P P 2 < x 2 P x 2 < P 2
123 121 122 syl P ¬ 2 P x 1 H P 2 x 2 P P 2 < x 2 P x 2 < P 2
124 116 123 mpbid P ¬ 2 P x 1 H P 2 x 2 P x 2 < P 2
125 21 ad2antrr P ¬ 2 P x 1 H P
126 simplr P ¬ 2 P x 1 H ¬ 2 P
127 60 adantl P ¬ 2 P x 1 H x 2
128 125 127 zsubcld P ¬ 2 P x 1 H P x 2
129 125 126 128 3jca P ¬ 2 P x 1 H P ¬ 2 P P x 2
130 129 adantr P ¬ 2 P x 1 H P 2 x 2 P ¬ 2 P P x 2
131 ltoddhalfle P ¬ 2 P P x 2 P x 2 < P 2 P x 2 P 1 2
132 130 131 syl P ¬ 2 P x 1 H P 2 x 2 P x 2 < P 2 P x 2 P 1 2
133 124 132 mpbid P ¬ 2 P x 1 H P 2 x 2 P x 2 P 1 2
134 133 ex P ¬ 2 P x 1 H P 2 x 2 P x 2 P 1 2
135 2 breq2i P x 2 H P x 2 P 1 2
136 134 135 syl6ibr P ¬ 2 P x 1 H P 2 x 2 P x 2 H
137 105 136 sylbird P ¬ 2 P x 1 H ¬ x 2 < P 2 P x 2 H
138 137 ex P ¬ 2 P x 1 H ¬ x 2 < P 2 P x 2 H
139 1 20 138 3syl φ x 1 H ¬ x 2 < P 2 P x 2 H
140 139 imp φ x 1 H ¬ x 2 < P 2 P x 2 H
141 140 impcom ¬ x 2 < P 2 φ x 1 H P x 2 H
142 elfz1b P x 2 1 H P x 2 H P x 2 H
143 97 99 141 142 syl3anbrc ¬ x 2 < P 2 φ x 1 H P x 2 1 H
144 eleq1 y = P x 2 y 1 H P x 2 1 H
145 143 144 syl5ibrcom ¬ x 2 < P 2 φ x 1 H y = P x 2 y 1 H
146 53 145 sylbid ¬ x 2 < P 2 φ x 1 H y = if x 2 < P 2 x 2 P x 2 y 1 H
147 50 146 pm2.61ian φ x 1 H y = if x 2 < P 2 x 2 P x 2 y 1 H
148 147 rexlimdva φ x 1 H y = if x 2 < P 2 x 2 P x 2 y 1 H
149 elfz1b y 1 H y H y H
150 simp1 y H y H y
151 simpl 2 y φ 2 y
152 nnehalf y 2 y y 2
153 150 151 152 syl2anr 2 y φ y H y H y 2
154 simpr2 2 y φ y H y H H
155 nnre y y
156 155 ad2antrr y H 2 y φ y
157 nnrp H H +
158 157 adantl y H H +
159 158 adantr y H 2 y φ H +
160 2rp 2 +
161 1le2 1 2
162 160 161 pm3.2i 2 + 1 2
163 162 a1i y H 2 y φ 2 + 1 2
164 ledivge1le y H + 2 + 1 2 y H y 2 H
165 156 159 163 164 syl3anc y H 2 y φ y H y 2 H
166 165 ex y H 2 y φ y H y 2 H
167 166 com23 y H y H 2 y φ y 2 H
168 167 3impia y H y H 2 y φ y 2 H
169 168 impcom 2 y φ y H y H y 2 H
170 153 154 169 3jca 2 y φ y H y H y 2 H y 2 H
171 170 ex 2 y φ y H y H y 2 H y 2 H
172 149 171 syl5bi 2 y φ y 1 H y 2 H y 2 H
173 172 3impia 2 y φ y 1 H y 2 H y 2 H
174 elfz1b y 2 1 H y 2 H y 2 H
175 173 174 sylibr 2 y φ y 1 H y 2 1 H
176 oveq1 x = y 2 x 2 = y 2 2
177 176 breq1d x = y 2 x 2 < P 2 y 2 2 < P 2
178 176 oveq2d x = y 2 P x 2 = P y 2 2
179 177 176 178 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
180 179 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
181 180 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
182 elfzelz y 1 H y
183 182 zcnd y 1 H y
184 183 3ad2ant3 2 y φ y 1 H y
185 2cnd 2 y φ y 1 H 2
186 2ne0 2 0
187 186 a1i 2 y φ y 1 H 2 0
188 184 185 187 divcan1d 2 y φ y 1 H y 2 2 = y
189 2 breq2i y H y P 1 2
190 nnz y y
191 1 20 22 3syl φ P ¬ 2 P
192 191 adantl 2 y φ P ¬ 2 P
193 190 192 anim12ci y 2 y φ P ¬ 2 P y
194 df-3an P ¬ 2 P y P ¬ 2 P y
195 193 194 sylibr y 2 y φ P ¬ 2 P y
196 ltoddhalfle P ¬ 2 P y y < P 2 y P 1 2
197 195 196 syl y 2 y φ y < P 2 y P 1 2
198 197 exbiri y 2 y φ y P 1 2 y < P 2
199 198 com23 y y P 1 2 2 y φ y < P 2
200 189 199 syl5bi y y H 2 y φ y < P 2
201 200 a1d y H y H 2 y φ y < P 2
202 201 3imp y H y H 2 y φ y < P 2
203 149 202 sylbi y 1 H 2 y φ y < P 2
204 203 com12 2 y φ y 1 H y < P 2
205 204 3impia 2 y φ y 1 H y < P 2
206 188 205 eqbrtrd 2 y φ y 1 H y 2 2 < P 2
207 206 iftrued 2 y φ y 1 H if y 2 2 < P 2 y 2 2 P y 2 2 = y 2 2
208 207 188 eqtr2d 2 y φ y 1 H y = if y 2 2 < P 2 y 2 2 P y 2 2
209 175 181 208 rspcedvd 2 y φ y 1 H x 1 H y = if x 2 < P 2 x 2 P x 2
210 209 3exp 2 y φ y 1 H x 1 H y = if x 2 < P 2 x 2 P x 2
211 54 55 syl P 2 P
212 211 ad2antrr P 2 ¬ 2 y y H y H P
213 190 3ad2ant1 y H y H y
214 213 adantl P 2 ¬ 2 y y H y H y
215 212 214 zsubcld P 2 ¬ 2 y y H y H P y
216 155 ad2antrl P y H y
217 67 rehalfcld P P 1 2
218 217 adantr P y H P 1 2
219 simpl P y H P
220 216 218 219 3jca P y H y P 1 2 P
221 220 ex P y H y P 1 2 P
222 54 63 221 3syl P 2 y H y P 1 2 P
223 222 adantr P 2 ¬ 2 y y H y P 1 2 P
224 223 impcom y H P 2 ¬ 2 y y P 1 2 P
225 lesub2 y P 1 2 P y P 1 2 P P 1 2 P y
226 224 225 syl y H P 2 ¬ 2 y y P 1 2 P P 1 2 P y
227 55 zcnd P P
228 1cnd P 1
229 2cnne0 2 2 0
230 229 a1i P 2 2 0
231 divsubdir P 1 2 2 0 P 1 2 = P 2 1 2
232 228 230 231 mpd3an23 P P 1 2 = P 2 1 2
233 232 oveq2d P P P 1 2 = P P 2 1 2
234 id P P
235 halfcl P P 2
236 halfcn 1 2
237 236 a1i P 1 2
238 234 235 237 subsubd P P P 2 1 2 = P - P 2 + 1 2
239 112 oveq1d P P - P 2 + 1 2 = P 2 + 1 2
240 233 238 239 3eqtrd P P P 1 2 = P 2 + 1 2
241 54 227 240 3syl P 2 P P 1 2 = P 2 + 1 2
242 241 ad2antrl y H P 2 ¬ 2 y P P 1 2 = P 2 + 1 2
243 242 breq1d y H P 2 ¬ 2 y P P 1 2 P y P 2 + 1 2 P y
244 prmnn P P
245 halfre 1 2
246 245 a1i P 1 2
247 nngt0 P 0 < P
248 71 a1i P 2 0 < 2
249 divgt0 P 0 < P 2 0 < 2 0 < P 2
250 100 247 248 249 syl21anc P 0 < P 2
251 halfgt0 0 < 1 2
252 251 a1i P 0 < 1 2
253 101 246 250 252 addgt0d P 0 < P 2 + 1 2
254 54 244 253 3syl P 2 0 < P 2 + 1 2
255 254 ad2antrl y H P 2 ¬ 2 y 0 < P 2 + 1 2
256 0red y P 0
257 simpr y P P
258 257 rehalfcld y P P 2
259 245 a1i y P 1 2
260 258 259 readdcld y P P 2 + 1 2
261 resubcl P y P y
262 261 ancoms y P P y
263 256 260 262 3jca y P 0 P 2 + 1 2 P y
264 263 ex y P 0 P 2 + 1 2 P y
265 155 264 syl y P 0 P 2 + 1 2 P y
266 265 adantr y H P 0 P 2 + 1 2 P y
267 266 com12 P y H 0 P 2 + 1 2 P y
268 54 63 267 3syl P 2 y H 0 P 2 + 1 2 P y
269 268 adantr P 2 ¬ 2 y y H 0 P 2 + 1 2 P y
270 269 impcom y H P 2 ¬ 2 y 0 P 2 + 1 2 P y
271 ltletr 0 P 2 + 1 2 P y 0 < P 2 + 1 2 P 2 + 1 2 P y 0 < P y
272 270 271 syl y H P 2 ¬ 2 y 0 < P 2 + 1 2 P 2 + 1 2 P y 0 < P y
273 255 272 mpand y H P 2 ¬ 2 y P 2 + 1 2 P y 0 < P y
274 243 273 sylbid y H P 2 ¬ 2 y P P 1 2 P y 0 < P y
275 226 274 sylbid y H P 2 ¬ 2 y y P 1 2 0 < P y
276 275 ex y H P 2 ¬ 2 y y P 1 2 0 < P y
277 276 com23 y H y P 1 2 P 2 ¬ 2 y 0 < P y
278 189 277 syl5bi y H y H P 2 ¬ 2 y 0 < P y
279 278 3impia y H y H P 2 ¬ 2 y 0 < P y
280 279 impcom P 2 ¬ 2 y y H y H 0 < P y
281 elnnz P y P y 0 < P y
282 215 280 281 sylanbrc P 2 ¬ 2 y y H y H P y
283 23 adantr P 2 ¬ 2 y P ¬ 2 P
284 simpr P 2 ¬ 2 y ¬ 2 y
285 284 213 anim12ci P 2 ¬ 2 y y H y H y ¬ 2 y
286 omoe P ¬ 2 P y ¬ 2 y 2 P y
287 283 285 286 syl2an2r P 2 ¬ 2 y y H y H 2 P y
288 nnehalf P y 2 P y P y 2
289 282 287 288 syl2anc P 2 ¬ 2 y y H y H P y 2
290 simpr2 P 2 ¬ 2 y y H y H H
291 1red P 2 ¬ 2 y y H y H 1
292 155 3ad2ant1 y H y H y
293 292 adantl P 2 ¬ 2 y y H y H y
294 54 63 syl P 2 P
295 294 ad2antrr P 2 ¬ 2 y y H y H P
296 nnge1 y 1 y
297 296 3ad2ant1 y H y H 1 y
298 297 adantl P 2 ¬ 2 y y H y H 1 y
299 291 293 295 298 lesub2dd P 2 ¬ 2 y y H y H P y P 1
300 295 293 resubcld P 2 ¬ 2 y y H y H P y
301 54 63 67 3syl P 2 P 1
302 301 ad2antrr P 2 ¬ 2 y y H y H P 1
303 71 a1i P 2 ¬ 2 y y H y H 2 0 < 2
304 lediv1 P y P 1 2 0 < 2 P y P 1 P y 2 P 1 2
305 300 302 303 304 syl3anc P 2 ¬ 2 y y H y H P y P 1 P y 2 P 1 2
306 299 305 mpbid P 2 ¬ 2 y y H y H P y 2 P 1 2
307 2 breq2i P y 2 H P y 2 P 1 2
308 306 307 sylibr P 2 ¬ 2 y y H y H P y 2 H
309 289 290 308 3jca P 2 ¬ 2 y y H y H P y 2 H P y 2 H
310 309 ex P 2 ¬ 2 y y H y H P y 2 H P y 2 H
311 elfz1b P y 2 1 H P y 2 H P y 2 H
312 310 149 311 3imtr4g P 2 ¬ 2 y y 1 H P y 2 1 H
313 312 ex P 2 ¬ 2 y y 1 H P y 2 1 H
314 1 313 syl φ ¬ 2 y y 1 H P y 2 1 H
315 314 3imp21 ¬ 2 y φ y 1 H P y 2 1 H
316 oveq1 x = P y 2 x 2 = P y 2 2
317 316 breq1d x = P y 2 x 2 < P 2 P y 2 2 < P 2
318 316 oveq2d x = P y 2 P x 2 = P P y 2 2
319 317 316 318 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
320 319 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
321 320 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
322 1 54 227 3syl φ P
323 322 3ad2ant2 ¬ 2 y φ y 1 H P
324 183 3ad2ant3 ¬ 2 y φ y 1 H y
325 323 324 subcld ¬ 2 y φ y 1 H P y
326 2cnd ¬ 2 y φ y 1 H 2
327 186 a1i ¬ 2 y φ y 1 H 2 0
328 325 326 327 divcan1d ¬ 2 y φ y 1 H P y 2 2 = P y
329 zre P P
330 halfge0 0 1 2
331 rehalfcl P P 2
332 331 adantl y P P 2
333 332 259 subge02d y P 0 1 2 P 2 1 2 P 2
334 330 333 mpbii y P P 2 1 2 P 2
335 simpl y P y
336 245 a1i P 1 2
337 331 336 resubcld P P 2 1 2
338 337 adantl y P P 2 1 2
339 letr y P 2 1 2 P 2 y P 2 1 2 P 2 1 2 P 2 y P 2
340 335 338 332 339 syl3anc y P y P 2 1 2 P 2 1 2 P 2 y P 2
341 334 340 mpan2d y P y P 2 1 2 y P 2
342 80 adantl y P P
343 1cnd y P 1
344 229 a1i y P 2 2 0
345 342 343 344 231 syl3anc y P P 1 2 = P 2 1 2
346 345 breq2d y P y P 1 2 y P 2 1 2
347 lesub P 2 P y P 2 P y y P P 2
348 332 257 335 347 syl3anc y P P 2 P y y P P 2
349 258 262 lenltd y P P 2 P y ¬ P y < P 2
350 2cnd P 2
351 186 a1i P 2 0
352 80 350 351 divcan1d P P 2 2 = P
353 352 eqcomd P P = P 2 2
354 353 oveq1d P P P 2 = P 2 2 P 2
355 331 recnd P P 2
356 355 350 mulcomd P P 2 2 = 2 P 2
357 356 oveq1d P P 2 2 P 2 = 2 P 2 P 2
358 350 355 mulsubfacd P 2 P 2 P 2 = 2 1 P 2
359 2m1e1 2 1 = 1
360 359 a1i P 2 1 = 1
361 360 oveq1d P 2 1 P 2 = 1 P 2
362 355 mulid2d P 1 P 2 = P 2
363 358 361 362 3eqtrd P 2 P 2 P 2 = P 2
364 354 357 363 3eqtrd P P P 2 = P 2
365 364 adantl y P P P 2 = P 2
366 365 breq2d y P y P P 2 y P 2
367 348 349 366 3bitr3d y P ¬ P y < P 2 y P 2
368 341 346 367 3imtr4d y P y P 1 2 ¬ P y < P 2
369 368 ex y P y P 1 2 ¬ P y < P 2
370 155 369 syl y P y P 1 2 ¬ P y < P 2
371 370 com3l P y P 1 2 y ¬ P y < P 2
372 329 371 syl P y P 1 2 y ¬ P y < P 2
373 54 55 372 3syl P 2 y P 1 2 y ¬ P y < P 2
374 1 373 syl φ y P 1 2 y ¬ P y < P 2
375 374 adantl ¬ 2 y φ y P 1 2 y ¬ P y < P 2
376 375 com13 y y P 1 2 ¬ 2 y φ ¬ P y < P 2
377 189 376 syl5bi y y H ¬ 2 y φ ¬ P y < P 2
378 377 a1d y H y H ¬ 2 y φ ¬ P y < P 2
379 378 3imp y H y H ¬ 2 y φ ¬ P y < P 2
380 379 com12 ¬ 2 y φ y H y H ¬ P y < P 2
381 149 380 syl5bi ¬ 2 y φ y 1 H ¬ P y < P 2
382 381 3impia ¬ 2 y φ y 1 H ¬ P y < P 2
383 328 382 eqnbrtrd ¬ 2 y φ y 1 H ¬ P y 2 2 < P 2
384 383 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
385 328 oveq2d ¬ 2 y φ y 1 H P P y 2 2 = P P y
386 322 183 anim12i φ y 1 H P y
387 386 3adant1 ¬ 2 y φ y 1 H P y
388 nncan P y P P y = y
389 387 388 syl ¬ 2 y φ y 1 H P P y = y
390 384 385 389 3eqtrrd ¬ 2 y φ y 1 H y = if P y 2 2 < P 2 P y 2 2 P P y 2 2
391 315 321 390 rspcedvd ¬ 2 y φ y 1 H x 1 H y = if x 2 < P 2 x 2 P x 2
392 391 3exp ¬ 2 y φ y 1 H x 1 H y = if x 2 < P 2 x 2 P x 2
393 210 392 pm2.61i φ y 1 H x 1 H y = if x 2 < P 2 x 2 P x 2
394 148 393 impbid φ x 1 H y = if x 2 < P 2 x 2 P x 2 y 1 H
395 5 394 syl5bb φ y ran R y 1 H
396 395 eqrdv φ ran R = 1 H