MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  gausslemma2dlem1a Structured version   Visualization version   GIF version

Theorem gausslemma2dlem1a 26636
Description: Lemma for gausslemma2dlem1 26637. (Contributed by AV, 1-Jul-2021.)
Hypotheses
Ref Expression
gausslemma2d.p (๐œ‘ โ†’ ๐‘ƒ โˆˆ (โ„™ โˆ– {2}))
gausslemma2d.h ๐ป = ((๐‘ƒ โˆ’ 1) / 2)
gausslemma2d.r ๐‘… = (๐‘ฅ โˆˆ (1...๐ป) โ†ฆ if((๐‘ฅ ยท 2) < (๐‘ƒ / 2), (๐‘ฅ ยท 2), (๐‘ƒ โˆ’ (๐‘ฅ ยท 2))))
Assertion
Ref Expression
gausslemma2dlem1a (๐œ‘ โ†’ ran ๐‘… = (1...๐ป))
Distinct variable groups:   ๐‘ฅ,๐ป   ๐‘ฅ,๐‘ƒ   ๐œ‘,๐‘ฅ
Allowed substitution hint:   ๐‘…(๐‘ฅ)

Proof of Theorem gausslemma2dlem1a
Dummy variable ๐‘ฆ is distinct from all other variables.
StepHypRef Expression
1 gausslemma2d.r . . . . 5 ๐‘… = (๐‘ฅ โˆˆ (1...๐ป) โ†ฆ if((๐‘ฅ ยท 2) < (๐‘ƒ / 2), (๐‘ฅ ยท 2), (๐‘ƒ โˆ’ (๐‘ฅ ยท 2))))
21elrnmpt 5908 . . . 4 (๐‘ฆ โˆˆ V โ†’ (๐‘ฆ โˆˆ ran ๐‘… โ†” โˆƒ๐‘ฅ โˆˆ (1...๐ป)๐‘ฆ = if((๐‘ฅ ยท 2) < (๐‘ƒ / 2), (๐‘ฅ ยท 2), (๐‘ƒ โˆ’ (๐‘ฅ ยท 2)))))
32elv 3450 . . 3 (๐‘ฆ โˆˆ ran ๐‘… โ†” โˆƒ๐‘ฅ โˆˆ (1...๐ป)๐‘ฆ = if((๐‘ฅ ยท 2) < (๐‘ƒ / 2), (๐‘ฅ ยท 2), (๐‘ƒ โˆ’ (๐‘ฅ ยท 2))))
4 iftrue 4491 . . . . . . . . 9 ((๐‘ฅ ยท 2) < (๐‘ƒ / 2) โ†’ if((๐‘ฅ ยท 2) < (๐‘ƒ / 2), (๐‘ฅ ยท 2), (๐‘ƒ โˆ’ (๐‘ฅ ยท 2))) = (๐‘ฅ ยท 2))
54eqeq2d 2749 . . . . . . . 8 ((๐‘ฅ ยท 2) < (๐‘ƒ / 2) โ†’ (๐‘ฆ = if((๐‘ฅ ยท 2) < (๐‘ƒ / 2), (๐‘ฅ ยท 2), (๐‘ƒ โˆ’ (๐‘ฅ ยท 2))) โ†” ๐‘ฆ = (๐‘ฅ ยท 2)))
65adantr 482 . . . . . . 7 (((๐‘ฅ ยท 2) < (๐‘ƒ / 2) โˆง (๐œ‘ โˆง ๐‘ฅ โˆˆ (1...๐ป))) โ†’ (๐‘ฆ = if((๐‘ฅ ยท 2) < (๐‘ƒ / 2), (๐‘ฅ ยท 2), (๐‘ƒ โˆ’ (๐‘ฅ ยท 2))) โ†” ๐‘ฆ = (๐‘ฅ ยท 2)))
7 elfz1b 13439 . . . . . . . . . . . 12 (๐‘ฅ โˆˆ (1...๐ป) โ†” (๐‘ฅ โˆˆ โ„• โˆง ๐ป โˆˆ โ„• โˆง ๐‘ฅ โ‰ค ๐ป))
8 id 22 . . . . . . . . . . . . . . . . 17 (๐‘ฅ โˆˆ โ„• โ†’ ๐‘ฅ โˆˆ โ„•)
9 2nn 12160 . . . . . . . . . . . . . . . . . 18 2 โˆˆ โ„•
109a1i 11 . . . . . . . . . . . . . . . . 17 (๐‘ฅ โˆˆ โ„• โ†’ 2 โˆˆ โ„•)
118, 10nnmulcld 12140 . . . . . . . . . . . . . . . 16 (๐‘ฅ โˆˆ โ„• โ†’ (๐‘ฅ ยท 2) โˆˆ โ„•)
12113ad2ant1 1134 . . . . . . . . . . . . . . 15 ((๐‘ฅ โˆˆ โ„• โˆง ๐ป โˆˆ โ„• โˆง ๐‘ฅ โ‰ค ๐ป) โ†’ (๐‘ฅ ยท 2) โˆˆ โ„•)
13123ad2ant1 1134 . . . . . . . . . . . . . 14 (((๐‘ฅ โˆˆ โ„• โˆง ๐ป โˆˆ โ„• โˆง ๐‘ฅ โ‰ค ๐ป) โˆง ๐œ‘ โˆง (๐‘ฅ ยท 2) < (๐‘ƒ / 2)) โ†’ (๐‘ฅ ยท 2) โˆˆ โ„•)
14 gausslemma2d.h . . . . . . . . . . . . . . . . . 18 ๐ป = ((๐‘ƒ โˆ’ 1) / 2)
1514eleq1i 2829 . . . . . . . . . . . . . . . . 17 (๐ป โˆˆ โ„• โ†” ((๐‘ƒ โˆ’ 1) / 2) โˆˆ โ„•)
1615biimpi 215 . . . . . . . . . . . . . . . 16 (๐ป โˆˆ โ„• โ†’ ((๐‘ƒ โˆ’ 1) / 2) โˆˆ โ„•)
17163ad2ant2 1135 . . . . . . . . . . . . . . 15 ((๐‘ฅ โˆˆ โ„• โˆง ๐ป โˆˆ โ„• โˆง ๐‘ฅ โ‰ค ๐ป) โ†’ ((๐‘ƒ โˆ’ 1) / 2) โˆˆ โ„•)
18173ad2ant1 1134 . . . . . . . . . . . . . 14 (((๐‘ฅ โˆˆ โ„• โˆง ๐ป โˆˆ โ„• โˆง ๐‘ฅ โ‰ค ๐ป) โˆง ๐œ‘ โˆง (๐‘ฅ ยท 2) < (๐‘ƒ / 2)) โ†’ ((๐‘ƒ โˆ’ 1) / 2) โˆˆ โ„•)
19 gausslemma2d.p . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ ๐‘ƒ โˆˆ (โ„™ โˆ– {2}))
20 nnoddn2prm 16618 . . . . . . . . . . . . . . . . . . . . . 22 (๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โ†’ (๐‘ƒ โˆˆ โ„• โˆง ยฌ 2 โˆฅ ๐‘ƒ))
21 nnz 12456 . . . . . . . . . . . . . . . . . . . . . . 23 (๐‘ƒ โˆˆ โ„• โ†’ ๐‘ƒ โˆˆ โ„ค)
2221anim1i 616 . . . . . . . . . . . . . . . . . . . . . 22 ((๐‘ƒ โˆˆ โ„• โˆง ยฌ 2 โˆฅ ๐‘ƒ) โ†’ (๐‘ƒ โˆˆ โ„ค โˆง ยฌ 2 โˆฅ ๐‘ƒ))
2320, 22syl 17 . . . . . . . . . . . . . . . . . . . . 21 (๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โ†’ (๐‘ƒ โˆˆ โ„ค โˆง ยฌ 2 โˆฅ ๐‘ƒ))
24 nnz 12456 . . . . . . . . . . . . . . . . . . . . . . 23 (๐‘ฅ โˆˆ โ„• โ†’ ๐‘ฅ โˆˆ โ„ค)
25 2z 12466 . . . . . . . . . . . . . . . . . . . . . . . 24 2 โˆˆ โ„ค
2625a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (๐‘ฅ โˆˆ โ„• โ†’ 2 โˆˆ โ„ค)
2724, 26zmulcld 12546 . . . . . . . . . . . . . . . . . . . . . 22 (๐‘ฅ โˆˆ โ„• โ†’ (๐‘ฅ ยท 2) โˆˆ โ„ค)
28273ad2ant1 1134 . . . . . . . . . . . . . . . . . . . . 21 ((๐‘ฅ โˆˆ โ„• โˆง ๐ป โˆˆ โ„• โˆง ๐‘ฅ โ‰ค ๐ป) โ†’ (๐‘ฅ ยท 2) โˆˆ โ„ค)
2923, 28anim12i 614 . . . . . . . . . . . . . . . . . . . 20 ((๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โˆง (๐‘ฅ โˆˆ โ„• โˆง ๐ป โˆˆ โ„• โˆง ๐‘ฅ โ‰ค ๐ป)) โ†’ ((๐‘ƒ โˆˆ โ„ค โˆง ยฌ 2 โˆฅ ๐‘ƒ) โˆง (๐‘ฅ ยท 2) โˆˆ โ„ค))
30 df-3an 1090 . . . . . . . . . . . . . . . . . . . 20 ((๐‘ƒ โˆˆ โ„ค โˆง ยฌ 2 โˆฅ ๐‘ƒ โˆง (๐‘ฅ ยท 2) โˆˆ โ„ค) โ†” ((๐‘ƒ โˆˆ โ„ค โˆง ยฌ 2 โˆฅ ๐‘ƒ) โˆง (๐‘ฅ ยท 2) โˆˆ โ„ค))
3129, 30sylibr 233 . . . . . . . . . . . . . . . . . . 19 ((๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โˆง (๐‘ฅ โˆˆ โ„• โˆง ๐ป โˆˆ โ„• โˆง ๐‘ฅ โ‰ค ๐ป)) โ†’ (๐‘ƒ โˆˆ โ„ค โˆง ยฌ 2 โˆฅ ๐‘ƒ โˆง (๐‘ฅ ยท 2) โˆˆ โ„ค))
3231ex 414 . . . . . . . . . . . . . . . . . 18 (๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โ†’ ((๐‘ฅ โˆˆ โ„• โˆง ๐ป โˆˆ โ„• โˆง ๐‘ฅ โ‰ค ๐ป) โ†’ (๐‘ƒ โˆˆ โ„ค โˆง ยฌ 2 โˆฅ ๐‘ƒ โˆง (๐‘ฅ ยท 2) โˆˆ โ„ค)))
3319, 32syl 17 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ ((๐‘ฅ โˆˆ โ„• โˆง ๐ป โˆˆ โ„• โˆง ๐‘ฅ โ‰ค ๐ป) โ†’ (๐‘ƒ โˆˆ โ„ค โˆง ยฌ 2 โˆฅ ๐‘ƒ โˆง (๐‘ฅ ยท 2) โˆˆ โ„ค)))
3433impcom 409 . . . . . . . . . . . . . . . 16 (((๐‘ฅ โˆˆ โ„• โˆง ๐ป โˆˆ โ„• โˆง ๐‘ฅ โ‰ค ๐ป) โˆง ๐œ‘) โ†’ (๐‘ƒ โˆˆ โ„ค โˆง ยฌ 2 โˆฅ ๐‘ƒ โˆง (๐‘ฅ ยท 2) โˆˆ โ„ค))
35 ltoddhalfle 16178 . . . . . . . . . . . . . . . 16 ((๐‘ƒ โˆˆ โ„ค โˆง ยฌ 2 โˆฅ ๐‘ƒ โˆง (๐‘ฅ ยท 2) โˆˆ โ„ค) โ†’ ((๐‘ฅ ยท 2) < (๐‘ƒ / 2) โ†” (๐‘ฅ ยท 2) โ‰ค ((๐‘ƒ โˆ’ 1) / 2)))
3634, 35syl 17 . . . . . . . . . . . . . . 15 (((๐‘ฅ โˆˆ โ„• โˆง ๐ป โˆˆ โ„• โˆง ๐‘ฅ โ‰ค ๐ป) โˆง ๐œ‘) โ†’ ((๐‘ฅ ยท 2) < (๐‘ƒ / 2) โ†” (๐‘ฅ ยท 2) โ‰ค ((๐‘ƒ โˆ’ 1) / 2)))
3736biimp3a 1470 . . . . . . . . . . . . . 14 (((๐‘ฅ โˆˆ โ„• โˆง ๐ป โˆˆ โ„• โˆง ๐‘ฅ โ‰ค ๐ป) โˆง ๐œ‘ โˆง (๐‘ฅ ยท 2) < (๐‘ƒ / 2)) โ†’ (๐‘ฅ ยท 2) โ‰ค ((๐‘ƒ โˆ’ 1) / 2))
3813, 18, 373jca 1129 . . . . . . . . . . . . 13 (((๐‘ฅ โˆˆ โ„• โˆง ๐ป โˆˆ โ„• โˆง ๐‘ฅ โ‰ค ๐ป) โˆง ๐œ‘ โˆง (๐‘ฅ ยท 2) < (๐‘ƒ / 2)) โ†’ ((๐‘ฅ ยท 2) โˆˆ โ„• โˆง ((๐‘ƒ โˆ’ 1) / 2) โˆˆ โ„• โˆง (๐‘ฅ ยท 2) โ‰ค ((๐‘ƒ โˆ’ 1) / 2)))
39383exp 1120 . . . . . . . . . . . 12 ((๐‘ฅ โˆˆ โ„• โˆง ๐ป โˆˆ โ„• โˆง ๐‘ฅ โ‰ค ๐ป) โ†’ (๐œ‘ โ†’ ((๐‘ฅ ยท 2) < (๐‘ƒ / 2) โ†’ ((๐‘ฅ ยท 2) โˆˆ โ„• โˆง ((๐‘ƒ โˆ’ 1) / 2) โˆˆ โ„• โˆง (๐‘ฅ ยท 2) โ‰ค ((๐‘ƒ โˆ’ 1) / 2)))))
407, 39sylbi 216 . . . . . . . . . . 11 (๐‘ฅ โˆˆ (1...๐ป) โ†’ (๐œ‘ โ†’ ((๐‘ฅ ยท 2) < (๐‘ƒ / 2) โ†’ ((๐‘ฅ ยท 2) โˆˆ โ„• โˆง ((๐‘ƒ โˆ’ 1) / 2) โˆˆ โ„• โˆง (๐‘ฅ ยท 2) โ‰ค ((๐‘ƒ โˆ’ 1) / 2)))))
4140impcom 409 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1...๐ป)) โ†’ ((๐‘ฅ ยท 2) < (๐‘ƒ / 2) โ†’ ((๐‘ฅ ยท 2) โˆˆ โ„• โˆง ((๐‘ƒ โˆ’ 1) / 2) โˆˆ โ„• โˆง (๐‘ฅ ยท 2) โ‰ค ((๐‘ƒ โˆ’ 1) / 2))))
4241impcom 409 . . . . . . . . 9 (((๐‘ฅ ยท 2) < (๐‘ƒ / 2) โˆง (๐œ‘ โˆง ๐‘ฅ โˆˆ (1...๐ป))) โ†’ ((๐‘ฅ ยท 2) โˆˆ โ„• โˆง ((๐‘ƒ โˆ’ 1) / 2) โˆˆ โ„• โˆง (๐‘ฅ ยท 2) โ‰ค ((๐‘ƒ โˆ’ 1) / 2)))
4314oveq2i 7361 . . . . . . . . . . 11 (1...๐ป) = (1...((๐‘ƒ โˆ’ 1) / 2))
4443eleq2i 2830 . . . . . . . . . 10 ((๐‘ฅ ยท 2) โˆˆ (1...๐ป) โ†” (๐‘ฅ ยท 2) โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)))
45 elfz1b 13439 . . . . . . . . . 10 ((๐‘ฅ ยท 2) โˆˆ (1...((๐‘ƒ โˆ’ 1) / 2)) โ†” ((๐‘ฅ ยท 2) โˆˆ โ„• โˆง ((๐‘ƒ โˆ’ 1) / 2) โˆˆ โ„• โˆง (๐‘ฅ ยท 2) โ‰ค ((๐‘ƒ โˆ’ 1) / 2)))
4644, 45bitri 275 . . . . . . . . 9 ((๐‘ฅ ยท 2) โˆˆ (1...๐ป) โ†” ((๐‘ฅ ยท 2) โˆˆ โ„• โˆง ((๐‘ƒ โˆ’ 1) / 2) โˆˆ โ„• โˆง (๐‘ฅ ยท 2) โ‰ค ((๐‘ƒ โˆ’ 1) / 2)))
4742, 46sylibr 233 . . . . . . . 8 (((๐‘ฅ ยท 2) < (๐‘ƒ / 2) โˆง (๐œ‘ โˆง ๐‘ฅ โˆˆ (1...๐ป))) โ†’ (๐‘ฅ ยท 2) โˆˆ (1...๐ป))
48 eleq1 2826 . . . . . . . 8 (๐‘ฆ = (๐‘ฅ ยท 2) โ†’ (๐‘ฆ โˆˆ (1...๐ป) โ†” (๐‘ฅ ยท 2) โˆˆ (1...๐ป)))
4947, 48syl5ibrcom 247 . . . . . . 7 (((๐‘ฅ ยท 2) < (๐‘ƒ / 2) โˆง (๐œ‘ โˆง ๐‘ฅ โˆˆ (1...๐ป))) โ†’ (๐‘ฆ = (๐‘ฅ ยท 2) โ†’ ๐‘ฆ โˆˆ (1...๐ป)))
506, 49sylbid 239 . . . . . 6 (((๐‘ฅ ยท 2) < (๐‘ƒ / 2) โˆง (๐œ‘ โˆง ๐‘ฅ โˆˆ (1...๐ป))) โ†’ (๐‘ฆ = if((๐‘ฅ ยท 2) < (๐‘ƒ / 2), (๐‘ฅ ยท 2), (๐‘ƒ โˆ’ (๐‘ฅ ยท 2))) โ†’ ๐‘ฆ โˆˆ (1...๐ป)))
51 iffalse 4494 . . . . . . . . 9 (ยฌ (๐‘ฅ ยท 2) < (๐‘ƒ / 2) โ†’ if((๐‘ฅ ยท 2) < (๐‘ƒ / 2), (๐‘ฅ ยท 2), (๐‘ƒ โˆ’ (๐‘ฅ ยท 2))) = (๐‘ƒ โˆ’ (๐‘ฅ ยท 2)))
5251eqeq2d 2749 . . . . . . . 8 (ยฌ (๐‘ฅ ยท 2) < (๐‘ƒ / 2) โ†’ (๐‘ฆ = if((๐‘ฅ ยท 2) < (๐‘ƒ / 2), (๐‘ฅ ยท 2), (๐‘ƒ โˆ’ (๐‘ฅ ยท 2))) โ†” ๐‘ฆ = (๐‘ƒ โˆ’ (๐‘ฅ ยท 2))))
5352adantr 482 . . . . . . 7 ((ยฌ (๐‘ฅ ยท 2) < (๐‘ƒ / 2) โˆง (๐œ‘ โˆง ๐‘ฅ โˆˆ (1...๐ป))) โ†’ (๐‘ฆ = if((๐‘ฅ ยท 2) < (๐‘ƒ / 2), (๐‘ฅ ยท 2), (๐‘ƒ โˆ’ (๐‘ฅ ยท 2))) โ†” ๐‘ฆ = (๐‘ƒ โˆ’ (๐‘ฅ ยท 2))))
54 eldifi 4085 . . . . . . . . . . . . 13 (๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โ†’ ๐‘ƒ โˆˆ โ„™)
55 prmz 16486 . . . . . . . . . . . . 13 (๐‘ƒ โˆˆ โ„™ โ†’ ๐‘ƒ โˆˆ โ„ค)
5619, 54, 553syl 18 . . . . . . . . . . . 12 (๐œ‘ โ†’ ๐‘ƒ โˆˆ โ„ค)
5756ad2antrl 727 . . . . . . . . . . 11 ((ยฌ (๐‘ฅ ยท 2) < (๐‘ƒ / 2) โˆง (๐œ‘ โˆง ๐‘ฅ โˆˆ (1...๐ป))) โ†’ ๐‘ƒ โˆˆ โ„ค)
58 elfzelz 13370 . . . . . . . . . . . . 13 (๐‘ฅ โˆˆ (1...๐ป) โ†’ ๐‘ฅ โˆˆ โ„ค)
5925a1i 11 . . . . . . . . . . . . 13 (๐‘ฅ โˆˆ (1...๐ป) โ†’ 2 โˆˆ โ„ค)
6058, 59zmulcld 12546 . . . . . . . . . . . 12 (๐‘ฅ โˆˆ (1...๐ป) โ†’ (๐‘ฅ ยท 2) โˆˆ โ„ค)
6160ad2antll 728 . . . . . . . . . . 11 ((ยฌ (๐‘ฅ ยท 2) < (๐‘ƒ / 2) โˆง (๐œ‘ โˆง ๐‘ฅ โˆˆ (1...๐ป))) โ†’ (๐‘ฅ ยท 2) โˆˆ โ„ค)
6257, 61zsubcld 12545 . . . . . . . . . 10 ((ยฌ (๐‘ฅ ยท 2) < (๐‘ƒ / 2) โˆง (๐œ‘ โˆง ๐‘ฅ โˆˆ (1...๐ป))) โ†’ (๐‘ƒ โˆ’ (๐‘ฅ ยท 2)) โˆˆ โ„ค)
6355zred 12540 . . . . . . . . . . . . . 14 (๐‘ƒ โˆˆ โ„™ โ†’ ๐‘ƒ โˆˆ โ„)
6414breq2i 5112 . . . . . . . . . . . . . . . . . . . 20 (๐‘ฅ โ‰ค ๐ป โ†” ๐‘ฅ โ‰ค ((๐‘ƒ โˆ’ 1) / 2))
65 nnre 12094 . . . . . . . . . . . . . . . . . . . . . 22 (๐‘ฅ โˆˆ โ„• โ†’ ๐‘ฅ โˆˆ โ„)
6665adantr 482 . . . . . . . . . . . . . . . . . . . . 21 ((๐‘ฅ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ โ„) โ†’ ๐‘ฅ โˆˆ โ„)
67 peano2rem 11402 . . . . . . . . . . . . . . . . . . . . . 22 (๐‘ƒ โˆˆ โ„ โ†’ (๐‘ƒ โˆ’ 1) โˆˆ โ„)
6867adantl 483 . . . . . . . . . . . . . . . . . . . . 21 ((๐‘ฅ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ โ„) โ†’ (๐‘ƒ โˆ’ 1) โˆˆ โ„)
69 2re 12161 . . . . . . . . . . . . . . . . . . . . . . 23 2 โˆˆ โ„
70 2pos 12190 . . . . . . . . . . . . . . . . . . . . . . 23 0 < 2
7169, 70pm3.2i 472 . . . . . . . . . . . . . . . . . . . . . 22 (2 โˆˆ โ„ โˆง 0 < 2)
7271a1i 11 . . . . . . . . . . . . . . . . . . . . 21 ((๐‘ฅ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ โ„) โ†’ (2 โˆˆ โ„ โˆง 0 < 2))
73 lemuldiv 11969 . . . . . . . . . . . . . . . . . . . . 21 ((๐‘ฅ โˆˆ โ„ โˆง (๐‘ƒ โˆ’ 1) โˆˆ โ„ โˆง (2 โˆˆ โ„ โˆง 0 < 2)) โ†’ ((๐‘ฅ ยท 2) โ‰ค (๐‘ƒ โˆ’ 1) โ†” ๐‘ฅ โ‰ค ((๐‘ƒ โˆ’ 1) / 2)))
7466, 68, 72, 73syl3anc 1372 . . . . . . . . . . . . . . . . . . . 20 ((๐‘ฅ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ โ„) โ†’ ((๐‘ฅ ยท 2) โ‰ค (๐‘ƒ โˆ’ 1) โ†” ๐‘ฅ โ‰ค ((๐‘ƒ โˆ’ 1) / 2)))
7564, 74bitr4id 290 . . . . . . . . . . . . . . . . . . 19 ((๐‘ฅ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ โ„) โ†’ (๐‘ฅ โ‰ค ๐ป โ†” (๐‘ฅ ยท 2) โ‰ค (๐‘ƒ โˆ’ 1)))
7611nnred 12102 . . . . . . . . . . . . . . . . . . . . . 22 (๐‘ฅ โˆˆ โ„• โ†’ (๐‘ฅ ยท 2) โˆˆ โ„)
7776adantr 482 . . . . . . . . . . . . . . . . . . . . 21 ((๐‘ฅ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ โ„) โ†’ (๐‘ฅ ยท 2) โˆˆ โ„)
78 simpr 486 . . . . . . . . . . . . . . . . . . . . 21 ((๐‘ฅ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ โ„) โ†’ ๐‘ƒ โˆˆ โ„)
7977, 68, 78lesub2d 11697 . . . . . . . . . . . . . . . . . . . 20 ((๐‘ฅ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ โ„) โ†’ ((๐‘ฅ ยท 2) โ‰ค (๐‘ƒ โˆ’ 1) โ†” (๐‘ƒ โˆ’ (๐‘ƒ โˆ’ 1)) โ‰ค (๐‘ƒ โˆ’ (๐‘ฅ ยท 2))))
80 recn 11075 . . . . . . . . . . . . . . . . . . . . . . . 24 (๐‘ƒ โˆˆ โ„ โ†’ ๐‘ƒ โˆˆ โ„‚)
81 1cnd 11084 . . . . . . . . . . . . . . . . . . . . . . . 24 (๐‘ƒ โˆˆ โ„ โ†’ 1 โˆˆ โ„‚)
8280, 81nncand 11451 . . . . . . . . . . . . . . . . . . . . . . 23 (๐‘ƒ โˆˆ โ„ โ†’ (๐‘ƒ โˆ’ (๐‘ƒ โˆ’ 1)) = 1)
8382adantl 483 . . . . . . . . . . . . . . . . . . . . . 22 ((๐‘ฅ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ โ„) โ†’ (๐‘ƒ โˆ’ (๐‘ƒ โˆ’ 1)) = 1)
8483breq1d 5114 . . . . . . . . . . . . . . . . . . . . 21 ((๐‘ฅ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ โ„) โ†’ ((๐‘ƒ โˆ’ (๐‘ƒ โˆ’ 1)) โ‰ค (๐‘ƒ โˆ’ (๐‘ฅ ยท 2)) โ†” 1 โ‰ค (๐‘ƒ โˆ’ (๐‘ฅ ยท 2))))
8584biimpd 228 . . . . . . . . . . . . . . . . . . . 20 ((๐‘ฅ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ โ„) โ†’ ((๐‘ƒ โˆ’ (๐‘ƒ โˆ’ 1)) โ‰ค (๐‘ƒ โˆ’ (๐‘ฅ ยท 2)) โ†’ 1 โ‰ค (๐‘ƒ โˆ’ (๐‘ฅ ยท 2))))
8679, 85sylbid 239 . . . . . . . . . . . . . . . . . . 19 ((๐‘ฅ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ โ„) โ†’ ((๐‘ฅ ยท 2) โ‰ค (๐‘ƒ โˆ’ 1) โ†’ 1 โ‰ค (๐‘ƒ โˆ’ (๐‘ฅ ยท 2))))
8775, 86sylbid 239 . . . . . . . . . . . . . . . . . 18 ((๐‘ฅ โˆˆ โ„• โˆง ๐‘ƒ โˆˆ โ„) โ†’ (๐‘ฅ โ‰ค ๐ป โ†’ 1 โ‰ค (๐‘ƒ โˆ’ (๐‘ฅ ยท 2))))
8887impancom 453 . . . . . . . . . . . . . . . . 17 ((๐‘ฅ โˆˆ โ„• โˆง ๐‘ฅ โ‰ค ๐ป) โ†’ (๐‘ƒ โˆˆ โ„ โ†’ 1 โ‰ค (๐‘ƒ โˆ’ (๐‘ฅ ยท 2))))
89883adant2 1132 . . . . . . . . . . . . . . . 16 ((๐‘ฅ โˆˆ โ„• โˆง ๐ป โˆˆ โ„• โˆง ๐‘ฅ โ‰ค ๐ป) โ†’ (๐‘ƒ โˆˆ โ„ โ†’ 1 โ‰ค (๐‘ƒ โˆ’ (๐‘ฅ ยท 2))))
907, 89sylbi 216 . . . . . . . . . . . . . . 15 (๐‘ฅ โˆˆ (1...๐ป) โ†’ (๐‘ƒ โˆˆ โ„ โ†’ 1 โ‰ค (๐‘ƒ โˆ’ (๐‘ฅ ยท 2))))
9190com12 32 . . . . . . . . . . . . . 14 (๐‘ƒ โˆˆ โ„ โ†’ (๐‘ฅ โˆˆ (1...๐ป) โ†’ 1 โ‰ค (๐‘ƒ โˆ’ (๐‘ฅ ยท 2))))
9263, 91syl 17 . . . . . . . . . . . . 13 (๐‘ƒ โˆˆ โ„™ โ†’ (๐‘ฅ โˆˆ (1...๐ป) โ†’ 1 โ‰ค (๐‘ƒ โˆ’ (๐‘ฅ ยท 2))))
9319, 54, 923syl 18 . . . . . . . . . . . 12 (๐œ‘ โ†’ (๐‘ฅ โˆˆ (1...๐ป) โ†’ 1 โ‰ค (๐‘ƒ โˆ’ (๐‘ฅ ยท 2))))
9493imp 408 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1...๐ป)) โ†’ 1 โ‰ค (๐‘ƒ โˆ’ (๐‘ฅ ยท 2)))
9594adantl 483 . . . . . . . . . 10 ((ยฌ (๐‘ฅ ยท 2) < (๐‘ƒ / 2) โˆง (๐œ‘ โˆง ๐‘ฅ โˆˆ (1...๐ป))) โ†’ 1 โ‰ค (๐‘ƒ โˆ’ (๐‘ฅ ยท 2)))
96 elnnz1 12460 . . . . . . . . . 10 ((๐‘ƒ โˆ’ (๐‘ฅ ยท 2)) โˆˆ โ„• โ†” ((๐‘ƒ โˆ’ (๐‘ฅ ยท 2)) โˆˆ โ„ค โˆง 1 โ‰ค (๐‘ƒ โˆ’ (๐‘ฅ ยท 2))))
9762, 95, 96sylanbrc 584 . . . . . . . . 9 ((ยฌ (๐‘ฅ ยท 2) < (๐‘ƒ / 2) โˆง (๐œ‘ โˆง ๐‘ฅ โˆˆ (1...๐ป))) โ†’ (๐‘ƒ โˆ’ (๐‘ฅ ยท 2)) โˆˆ โ„•)
987simp2bi 1147 . . . . . . . . . 10 (๐‘ฅ โˆˆ (1...๐ป) โ†’ ๐ป โˆˆ โ„•)
9998ad2antll 728 . . . . . . . . 9 ((ยฌ (๐‘ฅ ยท 2) < (๐‘ƒ / 2) โˆง (๐œ‘ โˆง ๐‘ฅ โˆˆ (1...๐ป))) โ†’ ๐ป โˆˆ โ„•)
100 nnre 12094 . . . . . . . . . . . . . . . . 17 (๐‘ƒ โˆˆ โ„• โ†’ ๐‘ƒ โˆˆ โ„)
101100rehalfcld 12334 . . . . . . . . . . . . . . . 16 (๐‘ƒ โˆˆ โ„• โ†’ (๐‘ƒ / 2) โˆˆ โ„)
102101adantr 482 . . . . . . . . . . . . . . 15 ((๐‘ƒ โˆˆ โ„• โˆง ยฌ 2 โˆฅ ๐‘ƒ) โ†’ (๐‘ƒ / 2) โˆˆ โ„)
10360zred 12540 . . . . . . . . . . . . . . 15 (๐‘ฅ โˆˆ (1...๐ป) โ†’ (๐‘ฅ ยท 2) โˆˆ โ„)
104 lenlt 11167 . . . . . . . . . . . . . . 15 (((๐‘ƒ / 2) โˆˆ โ„ โˆง (๐‘ฅ ยท 2) โˆˆ โ„) โ†’ ((๐‘ƒ / 2) โ‰ค (๐‘ฅ ยท 2) โ†” ยฌ (๐‘ฅ ยท 2) < (๐‘ƒ / 2)))
105102, 103, 104syl2an 597 . . . . . . . . . . . . . 14 (((๐‘ƒ โˆˆ โ„• โˆง ยฌ 2 โˆฅ ๐‘ƒ) โˆง ๐‘ฅ โˆˆ (1...๐ป)) โ†’ ((๐‘ƒ / 2) โ‰ค (๐‘ฅ ยท 2) โ†” ยฌ (๐‘ฅ ยท 2) < (๐‘ƒ / 2)))
10622, 60anim12i 614 . . . . . . . . . . . . . . . . . . . . . 22 (((๐‘ƒ โˆˆ โ„• โˆง ยฌ 2 โˆฅ ๐‘ƒ) โˆง ๐‘ฅ โˆˆ (1...๐ป)) โ†’ ((๐‘ƒ โˆˆ โ„ค โˆง ยฌ 2 โˆฅ ๐‘ƒ) โˆง (๐‘ฅ ยท 2) โˆˆ โ„ค))
107106, 30sylibr 233 . . . . . . . . . . . . . . . . . . . . 21 (((๐‘ƒ โˆˆ โ„• โˆง ยฌ 2 โˆฅ ๐‘ƒ) โˆง ๐‘ฅ โˆˆ (1...๐ป)) โ†’ (๐‘ƒ โˆˆ โ„ค โˆง ยฌ 2 โˆฅ ๐‘ƒ โˆง (๐‘ฅ ยท 2) โˆˆ โ„ค))
108 halfleoddlt 16179 . . . . . . . . . . . . . . . . . . . . 21 ((๐‘ƒ โˆˆ โ„ค โˆง ยฌ 2 โˆฅ ๐‘ƒ โˆง (๐‘ฅ ยท 2) โˆˆ โ„ค) โ†’ ((๐‘ƒ / 2) โ‰ค (๐‘ฅ ยท 2) โ†” (๐‘ƒ / 2) < (๐‘ฅ ยท 2)))
109107, 108syl 17 . . . . . . . . . . . . . . . . . . . 20 (((๐‘ƒ โˆˆ โ„• โˆง ยฌ 2 โˆฅ ๐‘ƒ) โˆง ๐‘ฅ โˆˆ (1...๐ป)) โ†’ ((๐‘ƒ / 2) โ‰ค (๐‘ฅ ยท 2) โ†” (๐‘ƒ / 2) < (๐‘ฅ ยท 2)))
110109biimpa 478 . . . . . . . . . . . . . . . . . . 19 ((((๐‘ƒ โˆˆ โ„• โˆง ยฌ 2 โˆฅ ๐‘ƒ) โˆง ๐‘ฅ โˆˆ (1...๐ป)) โˆง (๐‘ƒ / 2) โ‰ค (๐‘ฅ ยท 2)) โ†’ (๐‘ƒ / 2) < (๐‘ฅ ยท 2))
111 nncn 12095 . . . . . . . . . . . . . . . . . . . . . 22 (๐‘ƒ โˆˆ โ„• โ†’ ๐‘ƒ โˆˆ โ„‚)
112 subhalfhalf 12321 . . . . . . . . . . . . . . . . . . . . . 22 (๐‘ƒ โˆˆ โ„‚ โ†’ (๐‘ƒ โˆ’ (๐‘ƒ / 2)) = (๐‘ƒ / 2))
113111, 112syl 17 . . . . . . . . . . . . . . . . . . . . 21 (๐‘ƒ โˆˆ โ„• โ†’ (๐‘ƒ โˆ’ (๐‘ƒ / 2)) = (๐‘ƒ / 2))
114113breq1d 5114 . . . . . . . . . . . . . . . . . . . 20 (๐‘ƒ โˆˆ โ„• โ†’ ((๐‘ƒ โˆ’ (๐‘ƒ / 2)) < (๐‘ฅ ยท 2) โ†” (๐‘ƒ / 2) < (๐‘ฅ ยท 2)))
115114ad3antrrr 729 . . . . . . . . . . . . . . . . . . 19 ((((๐‘ƒ โˆˆ โ„• โˆง ยฌ 2 โˆฅ ๐‘ƒ) โˆง ๐‘ฅ โˆˆ (1...๐ป)) โˆง (๐‘ƒ / 2) โ‰ค (๐‘ฅ ยท 2)) โ†’ ((๐‘ƒ โˆ’ (๐‘ƒ / 2)) < (๐‘ฅ ยท 2) โ†” (๐‘ƒ / 2) < (๐‘ฅ ยท 2)))
116110, 115mpbird 257 . . . . . . . . . . . . . . . . . 18 ((((๐‘ƒ โˆˆ โ„• โˆง ยฌ 2 โˆฅ ๐‘ƒ) โˆง ๐‘ฅ โˆˆ (1...๐ป)) โˆง (๐‘ƒ / 2) โ‰ค (๐‘ฅ ยท 2)) โ†’ (๐‘ƒ โˆ’ (๐‘ƒ / 2)) < (๐‘ฅ ยท 2))
117100ad2antrr 725 . . . . . . . . . . . . . . . . . . . . 21 (((๐‘ƒ โˆˆ โ„• โˆง ยฌ 2 โˆฅ ๐‘ƒ) โˆง ๐‘ฅ โˆˆ (1...๐ป)) โ†’ ๐‘ƒ โˆˆ โ„)
118101ad2antrr 725 . . . . . . . . . . . . . . . . . . . . 21 (((๐‘ƒ โˆˆ โ„• โˆง ยฌ 2 โˆฅ ๐‘ƒ) โˆง ๐‘ฅ โˆˆ (1...๐ป)) โ†’ (๐‘ƒ / 2) โˆˆ โ„)
119103adantl 483 . . . . . . . . . . . . . . . . . . . . 21 (((๐‘ƒ โˆˆ โ„• โˆง ยฌ 2 โˆฅ ๐‘ƒ) โˆง ๐‘ฅ โˆˆ (1...๐ป)) โ†’ (๐‘ฅ ยท 2) โˆˆ โ„)
120117, 118, 1193jca 1129 . . . . . . . . . . . . . . . . . . . 20 (((๐‘ƒ โˆˆ โ„• โˆง ยฌ 2 โˆฅ ๐‘ƒ) โˆง ๐‘ฅ โˆˆ (1...๐ป)) โ†’ (๐‘ƒ โˆˆ โ„ โˆง (๐‘ƒ / 2) โˆˆ โ„ โˆง (๐‘ฅ ยท 2) โˆˆ โ„))
121120adantr 482 . . . . . . . . . . . . . . . . . . 19 ((((๐‘ƒ โˆˆ โ„• โˆง ยฌ 2 โˆฅ ๐‘ƒ) โˆง ๐‘ฅ โˆˆ (1...๐ป)) โˆง (๐‘ƒ / 2) โ‰ค (๐‘ฅ ยท 2)) โ†’ (๐‘ƒ โˆˆ โ„ โˆง (๐‘ƒ / 2) โˆˆ โ„ โˆง (๐‘ฅ ยท 2) โˆˆ โ„))
122 ltsub23 11569 . . . . . . . . . . . . . . . . . . 19 ((๐‘ƒ โˆˆ โ„ โˆง (๐‘ƒ / 2) โˆˆ โ„ โˆง (๐‘ฅ ยท 2) โˆˆ โ„) โ†’ ((๐‘ƒ โˆ’ (๐‘ƒ / 2)) < (๐‘ฅ ยท 2) โ†” (๐‘ƒ โˆ’ (๐‘ฅ ยท 2)) < (๐‘ƒ / 2)))
123121, 122syl 17 . . . . . . . . . . . . . . . . . 18 ((((๐‘ƒ โˆˆ โ„• โˆง ยฌ 2 โˆฅ ๐‘ƒ) โˆง ๐‘ฅ โˆˆ (1...๐ป)) โˆง (๐‘ƒ / 2) โ‰ค (๐‘ฅ ยท 2)) โ†’ ((๐‘ƒ โˆ’ (๐‘ƒ / 2)) < (๐‘ฅ ยท 2) โ†” (๐‘ƒ โˆ’ (๐‘ฅ ยท 2)) < (๐‘ƒ / 2)))
124116, 123mpbid 231 . . . . . . . . . . . . . . . . 17 ((((๐‘ƒ โˆˆ โ„• โˆง ยฌ 2 โˆฅ ๐‘ƒ) โˆง ๐‘ฅ โˆˆ (1...๐ป)) โˆง (๐‘ƒ / 2) โ‰ค (๐‘ฅ ยท 2)) โ†’ (๐‘ƒ โˆ’ (๐‘ฅ ยท 2)) < (๐‘ƒ / 2))
12521ad2antrr 725 . . . . . . . . . . . . . . . . . . . 20 (((๐‘ƒ โˆˆ โ„• โˆง ยฌ 2 โˆฅ ๐‘ƒ) โˆง ๐‘ฅ โˆˆ (1...๐ป)) โ†’ ๐‘ƒ โˆˆ โ„ค)
126 simplr 768 . . . . . . . . . . . . . . . . . . . 20 (((๐‘ƒ โˆˆ โ„• โˆง ยฌ 2 โˆฅ ๐‘ƒ) โˆง ๐‘ฅ โˆˆ (1...๐ป)) โ†’ ยฌ 2 โˆฅ ๐‘ƒ)
12760adantl 483 . . . . . . . . . . . . . . . . . . . . 21 (((๐‘ƒ โˆˆ โ„• โˆง ยฌ 2 โˆฅ ๐‘ƒ) โˆง ๐‘ฅ โˆˆ (1...๐ป)) โ†’ (๐‘ฅ ยท 2) โˆˆ โ„ค)
128125, 127zsubcld 12545 . . . . . . . . . . . . . . . . . . . 20 (((๐‘ƒ โˆˆ โ„• โˆง ยฌ 2 โˆฅ ๐‘ƒ) โˆง ๐‘ฅ โˆˆ (1...๐ป)) โ†’ (๐‘ƒ โˆ’ (๐‘ฅ ยท 2)) โˆˆ โ„ค)
129125, 126, 1283jca 1129 . . . . . . . . . . . . . . . . . . 19 (((๐‘ƒ โˆˆ โ„• โˆง ยฌ 2 โˆฅ ๐‘ƒ) โˆง ๐‘ฅ โˆˆ (1...๐ป)) โ†’ (๐‘ƒ โˆˆ โ„ค โˆง ยฌ 2 โˆฅ ๐‘ƒ โˆง (๐‘ƒ โˆ’ (๐‘ฅ ยท 2)) โˆˆ โ„ค))
130129adantr 482 . . . . . . . . . . . . . . . . . 18 ((((๐‘ƒ โˆˆ โ„• โˆง ยฌ 2 โˆฅ ๐‘ƒ) โˆง ๐‘ฅ โˆˆ (1...๐ป)) โˆง (๐‘ƒ / 2) โ‰ค (๐‘ฅ ยท 2)) โ†’ (๐‘ƒ โˆˆ โ„ค โˆง ยฌ 2 โˆฅ ๐‘ƒ โˆง (๐‘ƒ โˆ’ (๐‘ฅ ยท 2)) โˆˆ โ„ค))
131 ltoddhalfle 16178 . . . . . . . . . . . . . . . . . 18 ((๐‘ƒ โˆˆ โ„ค โˆง ยฌ 2 โˆฅ ๐‘ƒ โˆง (๐‘ƒ โˆ’ (๐‘ฅ ยท 2)) โˆˆ โ„ค) โ†’ ((๐‘ƒ โˆ’ (๐‘ฅ ยท 2)) < (๐‘ƒ / 2) โ†” (๐‘ƒ โˆ’ (๐‘ฅ ยท 2)) โ‰ค ((๐‘ƒ โˆ’ 1) / 2)))
132130, 131syl 17 . . . . . . . . . . . . . . . . 17 ((((๐‘ƒ โˆˆ โ„• โˆง ยฌ 2 โˆฅ ๐‘ƒ) โˆง ๐‘ฅ โˆˆ (1...๐ป)) โˆง (๐‘ƒ / 2) โ‰ค (๐‘ฅ ยท 2)) โ†’ ((๐‘ƒ โˆ’ (๐‘ฅ ยท 2)) < (๐‘ƒ / 2) โ†” (๐‘ƒ โˆ’ (๐‘ฅ ยท 2)) โ‰ค ((๐‘ƒ โˆ’ 1) / 2)))
133124, 132mpbid 231 . . . . . . . . . . . . . . . 16 ((((๐‘ƒ โˆˆ โ„• โˆง ยฌ 2 โˆฅ ๐‘ƒ) โˆง ๐‘ฅ โˆˆ (1...๐ป)) โˆง (๐‘ƒ / 2) โ‰ค (๐‘ฅ ยท 2)) โ†’ (๐‘ƒ โˆ’ (๐‘ฅ ยท 2)) โ‰ค ((๐‘ƒ โˆ’ 1) / 2))
134133ex 414 . . . . . . . . . . . . . . 15 (((๐‘ƒ โˆˆ โ„• โˆง ยฌ 2 โˆฅ ๐‘ƒ) โˆง ๐‘ฅ โˆˆ (1...๐ป)) โ†’ ((๐‘ƒ / 2) โ‰ค (๐‘ฅ ยท 2) โ†’ (๐‘ƒ โˆ’ (๐‘ฅ ยท 2)) โ‰ค ((๐‘ƒ โˆ’ 1) / 2)))
13514breq2i 5112 . . . . . . . . . . . . . . 15 ((๐‘ƒ โˆ’ (๐‘ฅ ยท 2)) โ‰ค ๐ป โ†” (๐‘ƒ โˆ’ (๐‘ฅ ยท 2)) โ‰ค ((๐‘ƒ โˆ’ 1) / 2))
136134, 135syl6ibr 252 . . . . . . . . . . . . . 14 (((๐‘ƒ โˆˆ โ„• โˆง ยฌ 2 โˆฅ ๐‘ƒ) โˆง ๐‘ฅ โˆˆ (1...๐ป)) โ†’ ((๐‘ƒ / 2) โ‰ค (๐‘ฅ ยท 2) โ†’ (๐‘ƒ โˆ’ (๐‘ฅ ยท 2)) โ‰ค ๐ป))
137105, 136sylbird 260 . . . . . . . . . . . . 13 (((๐‘ƒ โˆˆ โ„• โˆง ยฌ 2 โˆฅ ๐‘ƒ) โˆง ๐‘ฅ โˆˆ (1...๐ป)) โ†’ (ยฌ (๐‘ฅ ยท 2) < (๐‘ƒ / 2) โ†’ (๐‘ƒ โˆ’ (๐‘ฅ ยท 2)) โ‰ค ๐ป))
138137ex 414 . . . . . . . . . . . 12 ((๐‘ƒ โˆˆ โ„• โˆง ยฌ 2 โˆฅ ๐‘ƒ) โ†’ (๐‘ฅ โˆˆ (1...๐ป) โ†’ (ยฌ (๐‘ฅ ยท 2) < (๐‘ƒ / 2) โ†’ (๐‘ƒ โˆ’ (๐‘ฅ ยท 2)) โ‰ค ๐ป)))
13919, 20, 1383syl 18 . . . . . . . . . . 11 (๐œ‘ โ†’ (๐‘ฅ โˆˆ (1...๐ป) โ†’ (ยฌ (๐‘ฅ ยท 2) < (๐‘ƒ / 2) โ†’ (๐‘ƒ โˆ’ (๐‘ฅ ยท 2)) โ‰ค ๐ป)))
140139imp 408 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1...๐ป)) โ†’ (ยฌ (๐‘ฅ ยท 2) < (๐‘ƒ / 2) โ†’ (๐‘ƒ โˆ’ (๐‘ฅ ยท 2)) โ‰ค ๐ป))
141140impcom 409 . . . . . . . . 9 ((ยฌ (๐‘ฅ ยท 2) < (๐‘ƒ / 2) โˆง (๐œ‘ โˆง ๐‘ฅ โˆˆ (1...๐ป))) โ†’ (๐‘ƒ โˆ’ (๐‘ฅ ยท 2)) โ‰ค ๐ป)
142 elfz1b 13439 . . . . . . . . 9 ((๐‘ƒ โˆ’ (๐‘ฅ ยท 2)) โˆˆ (1...๐ป) โ†” ((๐‘ƒ โˆ’ (๐‘ฅ ยท 2)) โˆˆ โ„• โˆง ๐ป โˆˆ โ„• โˆง (๐‘ƒ โˆ’ (๐‘ฅ ยท 2)) โ‰ค ๐ป))
14397, 99, 141, 142syl3anbrc 1344 . . . . . . . 8 ((ยฌ (๐‘ฅ ยท 2) < (๐‘ƒ / 2) โˆง (๐œ‘ โˆง ๐‘ฅ โˆˆ (1...๐ป))) โ†’ (๐‘ƒ โˆ’ (๐‘ฅ ยท 2)) โˆˆ (1...๐ป))
144 eleq1 2826 . . . . . . . 8 (๐‘ฆ = (๐‘ƒ โˆ’ (๐‘ฅ ยท 2)) โ†’ (๐‘ฆ โˆˆ (1...๐ป) โ†” (๐‘ƒ โˆ’ (๐‘ฅ ยท 2)) โˆˆ (1...๐ป)))
145143, 144syl5ibrcom 247 . . . . . . 7 ((ยฌ (๐‘ฅ ยท 2) < (๐‘ƒ / 2) โˆง (๐œ‘ โˆง ๐‘ฅ โˆˆ (1...๐ป))) โ†’ (๐‘ฆ = (๐‘ƒ โˆ’ (๐‘ฅ ยท 2)) โ†’ ๐‘ฆ โˆˆ (1...๐ป)))
14653, 145sylbid 239 . . . . . 6 ((ยฌ (๐‘ฅ ยท 2) < (๐‘ƒ / 2) โˆง (๐œ‘ โˆง ๐‘ฅ โˆˆ (1...๐ป))) โ†’ (๐‘ฆ = if((๐‘ฅ ยท 2) < (๐‘ƒ / 2), (๐‘ฅ ยท 2), (๐‘ƒ โˆ’ (๐‘ฅ ยท 2))) โ†’ ๐‘ฆ โˆˆ (1...๐ป)))
14750, 146pm2.61ian 811 . . . . 5 ((๐œ‘ โˆง ๐‘ฅ โˆˆ (1...๐ป)) โ†’ (๐‘ฆ = if((๐‘ฅ ยท 2) < (๐‘ƒ / 2), (๐‘ฅ ยท 2), (๐‘ƒ โˆ’ (๐‘ฅ ยท 2))) โ†’ ๐‘ฆ โˆˆ (1...๐ป)))
148147rexlimdva 3151 . . . 4 (๐œ‘ โ†’ (โˆƒ๐‘ฅ โˆˆ (1...๐ป)๐‘ฆ = if((๐‘ฅ ยท 2) < (๐‘ƒ / 2), (๐‘ฅ ยท 2), (๐‘ƒ โˆ’ (๐‘ฅ ยท 2))) โ†’ ๐‘ฆ โˆˆ (1...๐ป)))
149 elfz1b 13439 . . . . . . . . . 10 (๐‘ฆ โˆˆ (1...๐ป) โ†” (๐‘ฆ โˆˆ โ„• โˆง ๐ป โˆˆ โ„• โˆง ๐‘ฆ โ‰ค ๐ป))
150 simp1 1137 . . . . . . . . . . . . 13 ((๐‘ฆ โˆˆ โ„• โˆง ๐ป โˆˆ โ„• โˆง ๐‘ฆ โ‰ค ๐ป) โ†’ ๐‘ฆ โˆˆ โ„•)
151 simpl 484 . . . . . . . . . . . . 13 ((2 โˆฅ ๐‘ฆ โˆง ๐œ‘) โ†’ 2 โˆฅ ๐‘ฆ)
152 nnehalf 16196 . . . . . . . . . . . . 13 ((๐‘ฆ โˆˆ โ„• โˆง 2 โˆฅ ๐‘ฆ) โ†’ (๐‘ฆ / 2) โˆˆ โ„•)
153150, 151, 152syl2anr 598 . . . . . . . . . . . 12 (((2 โˆฅ ๐‘ฆ โˆง ๐œ‘) โˆง (๐‘ฆ โˆˆ โ„• โˆง ๐ป โˆˆ โ„• โˆง ๐‘ฆ โ‰ค ๐ป)) โ†’ (๐‘ฆ / 2) โˆˆ โ„•)
154 simpr2 1196 . . . . . . . . . . . 12 (((2 โˆฅ ๐‘ฆ โˆง ๐œ‘) โˆง (๐‘ฆ โˆˆ โ„• โˆง ๐ป โˆˆ โ„• โˆง ๐‘ฆ โ‰ค ๐ป)) โ†’ ๐ป โˆˆ โ„•)
155 nnre 12094 . . . . . . . . . . . . . . . . . 18 (๐‘ฆ โˆˆ โ„• โ†’ ๐‘ฆ โˆˆ โ„)
156155ad2antrr 725 . . . . . . . . . . . . . . . . 17 (((๐‘ฆ โˆˆ โ„• โˆง ๐ป โˆˆ โ„•) โˆง (2 โˆฅ ๐‘ฆ โˆง ๐œ‘)) โ†’ ๐‘ฆ โˆˆ โ„)
157 nnrp 12855 . . . . . . . . . . . . . . . . . . 19 (๐ป โˆˆ โ„• โ†’ ๐ป โˆˆ โ„+)
158157adantl 483 . . . . . . . . . . . . . . . . . 18 ((๐‘ฆ โˆˆ โ„• โˆง ๐ป โˆˆ โ„•) โ†’ ๐ป โˆˆ โ„+)
159158adantr 482 . . . . . . . . . . . . . . . . 17 (((๐‘ฆ โˆˆ โ„• โˆง ๐ป โˆˆ โ„•) โˆง (2 โˆฅ ๐‘ฆ โˆง ๐œ‘)) โ†’ ๐ป โˆˆ โ„+)
160 2rp 12849 . . . . . . . . . . . . . . . . . . 19 2 โˆˆ โ„+
161 1le2 12296 . . . . . . . . . . . . . . . . . . 19 1 โ‰ค 2
162160, 161pm3.2i 472 . . . . . . . . . . . . . . . . . 18 (2 โˆˆ โ„+ โˆง 1 โ‰ค 2)
163162a1i 11 . . . . . . . . . . . . . . . . 17 (((๐‘ฆ โˆˆ โ„• โˆง ๐ป โˆˆ โ„•) โˆง (2 โˆฅ ๐‘ฆ โˆง ๐œ‘)) โ†’ (2 โˆˆ โ„+ โˆง 1 โ‰ค 2))
164 ledivge1le 12915 . . . . . . . . . . . . . . . . 17 ((๐‘ฆ โˆˆ โ„ โˆง ๐ป โˆˆ โ„+ โˆง (2 โˆˆ โ„+ โˆง 1 โ‰ค 2)) โ†’ (๐‘ฆ โ‰ค ๐ป โ†’ (๐‘ฆ / 2) โ‰ค ๐ป))
165156, 159, 163, 164syl3anc 1372 . . . . . . . . . . . . . . . 16 (((๐‘ฆ โˆˆ โ„• โˆง ๐ป โˆˆ โ„•) โˆง (2 โˆฅ ๐‘ฆ โˆง ๐œ‘)) โ†’ (๐‘ฆ โ‰ค ๐ป โ†’ (๐‘ฆ / 2) โ‰ค ๐ป))
166165ex 414 . . . . . . . . . . . . . . 15 ((๐‘ฆ โˆˆ โ„• โˆง ๐ป โˆˆ โ„•) โ†’ ((2 โˆฅ ๐‘ฆ โˆง ๐œ‘) โ†’ (๐‘ฆ โ‰ค ๐ป โ†’ (๐‘ฆ / 2) โ‰ค ๐ป)))
167166com23 86 . . . . . . . . . . . . . 14 ((๐‘ฆ โˆˆ โ„• โˆง ๐ป โˆˆ โ„•) โ†’ (๐‘ฆ โ‰ค ๐ป โ†’ ((2 โˆฅ ๐‘ฆ โˆง ๐œ‘) โ†’ (๐‘ฆ / 2) โ‰ค ๐ป)))
1681673impia 1118 . . . . . . . . . . . . 13 ((๐‘ฆ โˆˆ โ„• โˆง ๐ป โˆˆ โ„• โˆง ๐‘ฆ โ‰ค ๐ป) โ†’ ((2 โˆฅ ๐‘ฆ โˆง ๐œ‘) โ†’ (๐‘ฆ / 2) โ‰ค ๐ป))
169168impcom 409 . . . . . . . . . . . 12 (((2 โˆฅ ๐‘ฆ โˆง ๐œ‘) โˆง (๐‘ฆ โˆˆ โ„• โˆง ๐ป โˆˆ โ„• โˆง ๐‘ฆ โ‰ค ๐ป)) โ†’ (๐‘ฆ / 2) โ‰ค ๐ป)
170153, 154, 1693jca 1129 . . . . . . . . . . 11 (((2 โˆฅ ๐‘ฆ โˆง ๐œ‘) โˆง (๐‘ฆ โˆˆ โ„• โˆง ๐ป โˆˆ โ„• โˆง ๐‘ฆ โ‰ค ๐ป)) โ†’ ((๐‘ฆ / 2) โˆˆ โ„• โˆง ๐ป โˆˆ โ„• โˆง (๐‘ฆ / 2) โ‰ค ๐ป))
171170ex 414 . . . . . . . . . 10 ((2 โˆฅ ๐‘ฆ โˆง ๐œ‘) โ†’ ((๐‘ฆ โˆˆ โ„• โˆง ๐ป โˆˆ โ„• โˆง ๐‘ฆ โ‰ค ๐ป) โ†’ ((๐‘ฆ / 2) โˆˆ โ„• โˆง ๐ป โˆˆ โ„• โˆง (๐‘ฆ / 2) โ‰ค ๐ป)))
172149, 171biimtrid 241 . . . . . . . . 9 ((2 โˆฅ ๐‘ฆ โˆง ๐œ‘) โ†’ (๐‘ฆ โˆˆ (1...๐ป) โ†’ ((๐‘ฆ / 2) โˆˆ โ„• โˆง ๐ป โˆˆ โ„• โˆง (๐‘ฆ / 2) โ‰ค ๐ป)))
1731723impia 1118 . . . . . . . 8 ((2 โˆฅ ๐‘ฆ โˆง ๐œ‘ โˆง ๐‘ฆ โˆˆ (1...๐ป)) โ†’ ((๐‘ฆ / 2) โˆˆ โ„• โˆง ๐ป โˆˆ โ„• โˆง (๐‘ฆ / 2) โ‰ค ๐ป))
174 elfz1b 13439 . . . . . . . 8 ((๐‘ฆ / 2) โˆˆ (1...๐ป) โ†” ((๐‘ฆ / 2) โˆˆ โ„• โˆง ๐ป โˆˆ โ„• โˆง (๐‘ฆ / 2) โ‰ค ๐ป))
175173, 174sylibr 233 . . . . . . 7 ((2 โˆฅ ๐‘ฆ โˆง ๐œ‘ โˆง ๐‘ฆ โˆˆ (1...๐ป)) โ†’ (๐‘ฆ / 2) โˆˆ (1...๐ป))
176 oveq1 7357 . . . . . . . . . . 11 (๐‘ฅ = (๐‘ฆ / 2) โ†’ (๐‘ฅ ยท 2) = ((๐‘ฆ / 2) ยท 2))
177176breq1d 5114 . . . . . . . . . 10 (๐‘ฅ = (๐‘ฆ / 2) โ†’ ((๐‘ฅ ยท 2) < (๐‘ƒ / 2) โ†” ((๐‘ฆ / 2) ยท 2) < (๐‘ƒ / 2)))
178176oveq2d 7366 . . . . . . . . . 10 (๐‘ฅ = (๐‘ฆ / 2) โ†’ (๐‘ƒ โˆ’ (๐‘ฅ ยท 2)) = (๐‘ƒ โˆ’ ((๐‘ฆ / 2) ยท 2)))
179177, 176, 178ifbieq12d 4513 . . . . . . . . 9 (๐‘ฅ = (๐‘ฆ / 2) โ†’ if((๐‘ฅ ยท 2) < (๐‘ƒ / 2), (๐‘ฅ ยท 2), (๐‘ƒ โˆ’ (๐‘ฅ ยท 2))) = if(((๐‘ฆ / 2) ยท 2) < (๐‘ƒ / 2), ((๐‘ฆ / 2) ยท 2), (๐‘ƒ โˆ’ ((๐‘ฆ / 2) ยท 2))))
180179eqeq2d 2749 . . . . . . . 8 (๐‘ฅ = (๐‘ฆ / 2) โ†’ (๐‘ฆ = if((๐‘ฅ ยท 2) < (๐‘ƒ / 2), (๐‘ฅ ยท 2), (๐‘ƒ โˆ’ (๐‘ฅ ยท 2))) โ†” ๐‘ฆ = if(((๐‘ฆ / 2) ยท 2) < (๐‘ƒ / 2), ((๐‘ฆ / 2) ยท 2), (๐‘ƒ โˆ’ ((๐‘ฆ / 2) ยท 2)))))
181180adantl 483 . . . . . . 7 (((2 โˆฅ ๐‘ฆ โˆง ๐œ‘ โˆง ๐‘ฆ โˆˆ (1...๐ป)) โˆง ๐‘ฅ = (๐‘ฆ / 2)) โ†’ (๐‘ฆ = if((๐‘ฅ ยท 2) < (๐‘ƒ / 2), (๐‘ฅ ยท 2), (๐‘ƒ โˆ’ (๐‘ฅ ยท 2))) โ†” ๐‘ฆ = if(((๐‘ฆ / 2) ยท 2) < (๐‘ƒ / 2), ((๐‘ฆ / 2) ยท 2), (๐‘ƒ โˆ’ ((๐‘ฆ / 2) ยท 2)))))
182 elfzelz 13370 . . . . . . . . . . . . 13 (๐‘ฆ โˆˆ (1...๐ป) โ†’ ๐‘ฆ โˆˆ โ„ค)
183182zcnd 12541 . . . . . . . . . . . 12 (๐‘ฆ โˆˆ (1...๐ป) โ†’ ๐‘ฆ โˆˆ โ„‚)
1841833ad2ant3 1136 . . . . . . . . . . 11 ((2 โˆฅ ๐‘ฆ โˆง ๐œ‘ โˆง ๐‘ฆ โˆˆ (1...๐ป)) โ†’ ๐‘ฆ โˆˆ โ„‚)
185 2cnd 12165 . . . . . . . . . . 11 ((2 โˆฅ ๐‘ฆ โˆง ๐œ‘ โˆง ๐‘ฆ โˆˆ (1...๐ป)) โ†’ 2 โˆˆ โ„‚)
186 2ne0 12191 . . . . . . . . . . . 12 2 โ‰  0
187186a1i 11 . . . . . . . . . . 11 ((2 โˆฅ ๐‘ฆ โˆง ๐œ‘ โˆง ๐‘ฆ โˆˆ (1...๐ป)) โ†’ 2 โ‰  0)
188184, 185, 187divcan1d 11866 . . . . . . . . . 10 ((2 โˆฅ ๐‘ฆ โˆง ๐œ‘ โˆง ๐‘ฆ โˆˆ (1...๐ป)) โ†’ ((๐‘ฆ / 2) ยท 2) = ๐‘ฆ)
18914breq2i 5112 . . . . . . . . . . . . . . . 16 (๐‘ฆ โ‰ค ๐ป โ†” ๐‘ฆ โ‰ค ((๐‘ƒ โˆ’ 1) / 2))
190 nnz 12456 . . . . . . . . . . . . . . . . . . . . 21 (๐‘ฆ โˆˆ โ„• โ†’ ๐‘ฆ โˆˆ โ„ค)
19119, 20, 223syl 18 . . . . . . . . . . . . . . . . . . . . . 22 (๐œ‘ โ†’ (๐‘ƒ โˆˆ โ„ค โˆง ยฌ 2 โˆฅ ๐‘ƒ))
192191adantl 483 . . . . . . . . . . . . . . . . . . . . 21 ((2 โˆฅ ๐‘ฆ โˆง ๐œ‘) โ†’ (๐‘ƒ โˆˆ โ„ค โˆง ยฌ 2 โˆฅ ๐‘ƒ))
193190, 192anim12ci 615 . . . . . . . . . . . . . . . . . . . 20 ((๐‘ฆ โˆˆ โ„• โˆง (2 โˆฅ ๐‘ฆ โˆง ๐œ‘)) โ†’ ((๐‘ƒ โˆˆ โ„ค โˆง ยฌ 2 โˆฅ ๐‘ƒ) โˆง ๐‘ฆ โˆˆ โ„ค))
194 df-3an 1090 . . . . . . . . . . . . . . . . . . . 20 ((๐‘ƒ โˆˆ โ„ค โˆง ยฌ 2 โˆฅ ๐‘ƒ โˆง ๐‘ฆ โˆˆ โ„ค) โ†” ((๐‘ƒ โˆˆ โ„ค โˆง ยฌ 2 โˆฅ ๐‘ƒ) โˆง ๐‘ฆ โˆˆ โ„ค))
195193, 194sylibr 233 . . . . . . . . . . . . . . . . . . 19 ((๐‘ฆ โˆˆ โ„• โˆง (2 โˆฅ ๐‘ฆ โˆง ๐œ‘)) โ†’ (๐‘ƒ โˆˆ โ„ค โˆง ยฌ 2 โˆฅ ๐‘ƒ โˆง ๐‘ฆ โˆˆ โ„ค))
196 ltoddhalfle 16178 . . . . . . . . . . . . . . . . . . 19 ((๐‘ƒ โˆˆ โ„ค โˆง ยฌ 2 โˆฅ ๐‘ƒ โˆง ๐‘ฆ โˆˆ โ„ค) โ†’ (๐‘ฆ < (๐‘ƒ / 2) โ†” ๐‘ฆ โ‰ค ((๐‘ƒ โˆ’ 1) / 2)))
197195, 196syl 17 . . . . . . . . . . . . . . . . . 18 ((๐‘ฆ โˆˆ โ„• โˆง (2 โˆฅ ๐‘ฆ โˆง ๐œ‘)) โ†’ (๐‘ฆ < (๐‘ƒ / 2) โ†” ๐‘ฆ โ‰ค ((๐‘ƒ โˆ’ 1) / 2)))
198197exbiri 810 . . . . . . . . . . . . . . . . 17 (๐‘ฆ โˆˆ โ„• โ†’ ((2 โˆฅ ๐‘ฆ โˆง ๐œ‘) โ†’ (๐‘ฆ โ‰ค ((๐‘ƒ โˆ’ 1) / 2) โ†’ ๐‘ฆ < (๐‘ƒ / 2))))
199198com23 86 . . . . . . . . . . . . . . . 16 (๐‘ฆ โˆˆ โ„• โ†’ (๐‘ฆ โ‰ค ((๐‘ƒ โˆ’ 1) / 2) โ†’ ((2 โˆฅ ๐‘ฆ โˆง ๐œ‘) โ†’ ๐‘ฆ < (๐‘ƒ / 2))))
200189, 199biimtrid 241 . . . . . . . . . . . . . . 15 (๐‘ฆ โˆˆ โ„• โ†’ (๐‘ฆ โ‰ค ๐ป โ†’ ((2 โˆฅ ๐‘ฆ โˆง ๐œ‘) โ†’ ๐‘ฆ < (๐‘ƒ / 2))))
201200a1d 25 . . . . . . . . . . . . . 14 (๐‘ฆ โˆˆ โ„• โ†’ (๐ป โˆˆ โ„• โ†’ (๐‘ฆ โ‰ค ๐ป โ†’ ((2 โˆฅ ๐‘ฆ โˆง ๐œ‘) โ†’ ๐‘ฆ < (๐‘ƒ / 2)))))
2022013imp 1112 . . . . . . . . . . . . 13 ((๐‘ฆ โˆˆ โ„• โˆง ๐ป โˆˆ โ„• โˆง ๐‘ฆ โ‰ค ๐ป) โ†’ ((2 โˆฅ ๐‘ฆ โˆง ๐œ‘) โ†’ ๐‘ฆ < (๐‘ƒ / 2)))
203149, 202sylbi 216 . . . . . . . . . . . 12 (๐‘ฆ โˆˆ (1...๐ป) โ†’ ((2 โˆฅ ๐‘ฆ โˆง ๐œ‘) โ†’ ๐‘ฆ < (๐‘ƒ / 2)))
204203com12 32 . . . . . . . . . . 11 ((2 โˆฅ ๐‘ฆ โˆง ๐œ‘) โ†’ (๐‘ฆ โˆˆ (1...๐ป) โ†’ ๐‘ฆ < (๐‘ƒ / 2)))
2052043impia 1118 . . . . . . . . . 10 ((2 โˆฅ ๐‘ฆ โˆง ๐œ‘ โˆง ๐‘ฆ โˆˆ (1...๐ป)) โ†’ ๐‘ฆ < (๐‘ƒ / 2))
206188, 205eqbrtrd 5126 . . . . . . . . 9 ((2 โˆฅ ๐‘ฆ โˆง ๐œ‘ โˆง ๐‘ฆ โˆˆ (1...๐ป)) โ†’ ((๐‘ฆ / 2) ยท 2) < (๐‘ƒ / 2))
207206iftrued 4493 . . . . . . . 8 ((2 โˆฅ ๐‘ฆ โˆง ๐œ‘ โˆง ๐‘ฆ โˆˆ (1...๐ป)) โ†’ if(((๐‘ฆ / 2) ยท 2) < (๐‘ƒ / 2), ((๐‘ฆ / 2) ยท 2), (๐‘ƒ โˆ’ ((๐‘ฆ / 2) ยท 2))) = ((๐‘ฆ / 2) ยท 2))
208207, 188eqtr2d 2779 . . . . . . 7 ((2 โˆฅ ๐‘ฆ โˆง ๐œ‘ โˆง ๐‘ฆ โˆˆ (1...๐ป)) โ†’ ๐‘ฆ = if(((๐‘ฆ / 2) ยท 2) < (๐‘ƒ / 2), ((๐‘ฆ / 2) ยท 2), (๐‘ƒ โˆ’ ((๐‘ฆ / 2) ยท 2))))
209175, 181, 208rspcedvd 3582 . . . . . 6 ((2 โˆฅ ๐‘ฆ โˆง ๐œ‘ โˆง ๐‘ฆ โˆˆ (1...๐ป)) โ†’ โˆƒ๐‘ฅ โˆˆ (1...๐ป)๐‘ฆ = if((๐‘ฅ ยท 2) < (๐‘ƒ / 2), (๐‘ฅ ยท 2), (๐‘ƒ โˆ’ (๐‘ฅ ยท 2))))
2102093exp 1120 . . . . 5 (2 โˆฅ ๐‘ฆ โ†’ (๐œ‘ โ†’ (๐‘ฆ โˆˆ (1...๐ป) โ†’ โˆƒ๐‘ฅ โˆˆ (1...๐ป)๐‘ฆ = if((๐‘ฅ ยท 2) < (๐‘ƒ / 2), (๐‘ฅ ยท 2), (๐‘ƒ โˆ’ (๐‘ฅ ยท 2))))))
21154, 55syl 17 . . . . . . . . . . . . . . . . 17 (๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โ†’ ๐‘ƒ โˆˆ โ„ค)
212211ad2antrr 725 . . . . . . . . . . . . . . . 16 (((๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โˆง ยฌ 2 โˆฅ ๐‘ฆ) โˆง (๐‘ฆ โˆˆ โ„• โˆง ๐ป โˆˆ โ„• โˆง ๐‘ฆ โ‰ค ๐ป)) โ†’ ๐‘ƒ โˆˆ โ„ค)
2131903ad2ant1 1134 . . . . . . . . . . . . . . . . 17 ((๐‘ฆ โˆˆ โ„• โˆง ๐ป โˆˆ โ„• โˆง ๐‘ฆ โ‰ค ๐ป) โ†’ ๐‘ฆ โˆˆ โ„ค)
214213adantl 483 . . . . . . . . . . . . . . . 16 (((๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โˆง ยฌ 2 โˆฅ ๐‘ฆ) โˆง (๐‘ฆ โˆˆ โ„• โˆง ๐ป โˆˆ โ„• โˆง ๐‘ฆ โ‰ค ๐ป)) โ†’ ๐‘ฆ โˆˆ โ„ค)
215212, 214zsubcld 12545 . . . . . . . . . . . . . . 15 (((๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โˆง ยฌ 2 โˆฅ ๐‘ฆ) โˆง (๐‘ฆ โˆˆ โ„• โˆง ๐ป โˆˆ โ„• โˆง ๐‘ฆ โ‰ค ๐ป)) โ†’ (๐‘ƒ โˆ’ ๐‘ฆ) โˆˆ โ„ค)
216155ad2antrl 727 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((๐‘ƒ โˆˆ โ„ โˆง (๐‘ฆ โˆˆ โ„• โˆง ๐ป โˆˆ โ„•)) โ†’ ๐‘ฆ โˆˆ โ„)
21767rehalfcld 12334 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (๐‘ƒ โˆˆ โ„ โ†’ ((๐‘ƒ โˆ’ 1) / 2) โˆˆ โ„)
218217adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((๐‘ƒ โˆˆ โ„ โˆง (๐‘ฆ โˆˆ โ„• โˆง ๐ป โˆˆ โ„•)) โ†’ ((๐‘ƒ โˆ’ 1) / 2) โˆˆ โ„)
219 simpl 484 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((๐‘ƒ โˆˆ โ„ โˆง (๐‘ฆ โˆˆ โ„• โˆง ๐ป โˆˆ โ„•)) โ†’ ๐‘ƒ โˆˆ โ„)
220216, 218, 2193jca 1129 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((๐‘ƒ โˆˆ โ„ โˆง (๐‘ฆ โˆˆ โ„• โˆง ๐ป โˆˆ โ„•)) โ†’ (๐‘ฆ โˆˆ โ„ โˆง ((๐‘ƒ โˆ’ 1) / 2) โˆˆ โ„ โˆง ๐‘ƒ โˆˆ โ„))
221220ex 414 . . . . . . . . . . . . . . . . . . . . . . . . 25 (๐‘ƒ โˆˆ โ„ โ†’ ((๐‘ฆ โˆˆ โ„• โˆง ๐ป โˆˆ โ„•) โ†’ (๐‘ฆ โˆˆ โ„ โˆง ((๐‘ƒ โˆ’ 1) / 2) โˆˆ โ„ โˆง ๐‘ƒ โˆˆ โ„)))
22254, 63, 2213syl 18 . . . . . . . . . . . . . . . . . . . . . . . 24 (๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โ†’ ((๐‘ฆ โˆˆ โ„• โˆง ๐ป โˆˆ โ„•) โ†’ (๐‘ฆ โˆˆ โ„ โˆง ((๐‘ƒ โˆ’ 1) / 2) โˆˆ โ„ โˆง ๐‘ƒ โˆˆ โ„)))
223222adantr 482 . . . . . . . . . . . . . . . . . . . . . . 23 ((๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โˆง ยฌ 2 โˆฅ ๐‘ฆ) โ†’ ((๐‘ฆ โˆˆ โ„• โˆง ๐ป โˆˆ โ„•) โ†’ (๐‘ฆ โˆˆ โ„ โˆง ((๐‘ƒ โˆ’ 1) / 2) โˆˆ โ„ โˆง ๐‘ƒ โˆˆ โ„)))
224223impcom 409 . . . . . . . . . . . . . . . . . . . . . 22 (((๐‘ฆ โˆˆ โ„• โˆง ๐ป โˆˆ โ„•) โˆง (๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โˆง ยฌ 2 โˆฅ ๐‘ฆ)) โ†’ (๐‘ฆ โˆˆ โ„ โˆง ((๐‘ƒ โˆ’ 1) / 2) โˆˆ โ„ โˆง ๐‘ƒ โˆˆ โ„))
225 lesub2 11584 . . . . . . . . . . . . . . . . . . . . . 22 ((๐‘ฆ โˆˆ โ„ โˆง ((๐‘ƒ โˆ’ 1) / 2) โˆˆ โ„ โˆง ๐‘ƒ โˆˆ โ„) โ†’ (๐‘ฆ โ‰ค ((๐‘ƒ โˆ’ 1) / 2) โ†” (๐‘ƒ โˆ’ ((๐‘ƒ โˆ’ 1) / 2)) โ‰ค (๐‘ƒ โˆ’ ๐‘ฆ)))
226224, 225syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((๐‘ฆ โˆˆ โ„• โˆง ๐ป โˆˆ โ„•) โˆง (๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โˆง ยฌ 2 โˆฅ ๐‘ฆ)) โ†’ (๐‘ฆ โ‰ค ((๐‘ƒ โˆ’ 1) / 2) โ†” (๐‘ƒ โˆ’ ((๐‘ƒ โˆ’ 1) / 2)) โ‰ค (๐‘ƒ โˆ’ ๐‘ฆ)))
22755zcnd 12541 . . . . . . . . . . . . . . . . . . . . . . . . 25 (๐‘ƒ โˆˆ โ„™ โ†’ ๐‘ƒ โˆˆ โ„‚)
228 1cnd 11084 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (๐‘ƒ โˆˆ โ„‚ โ†’ 1 โˆˆ โ„‚)
229 2cnne0 12297 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (2 โˆˆ โ„‚ โˆง 2 โ‰  0)
230229a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (๐‘ƒ โˆˆ โ„‚ โ†’ (2 โˆˆ โ„‚ โˆง 2 โ‰  0))
231 divsubdir 11783 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((๐‘ƒ โˆˆ โ„‚ โˆง 1 โˆˆ โ„‚ โˆง (2 โˆˆ โ„‚ โˆง 2 โ‰  0)) โ†’ ((๐‘ƒ โˆ’ 1) / 2) = ((๐‘ƒ / 2) โˆ’ (1 / 2)))
232228, 230, 231mpd3an23 1464 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (๐‘ƒ โˆˆ โ„‚ โ†’ ((๐‘ƒ โˆ’ 1) / 2) = ((๐‘ƒ / 2) โˆ’ (1 / 2)))
233232oveq2d 7366 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (๐‘ƒ โˆˆ โ„‚ โ†’ (๐‘ƒ โˆ’ ((๐‘ƒ โˆ’ 1) / 2)) = (๐‘ƒ โˆ’ ((๐‘ƒ / 2) โˆ’ (1 / 2))))
234 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (๐‘ƒ โˆˆ โ„‚ โ†’ ๐‘ƒ โˆˆ โ„‚)
235 halfcl 12312 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (๐‘ƒ โˆˆ โ„‚ โ†’ (๐‘ƒ / 2) โˆˆ โ„‚)
236 halfcn 12302 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (1 / 2) โˆˆ โ„‚
237236a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (๐‘ƒ โˆˆ โ„‚ โ†’ (1 / 2) โˆˆ โ„‚)
238234, 235, 237subsubd 11474 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (๐‘ƒ โˆˆ โ„‚ โ†’ (๐‘ƒ โˆ’ ((๐‘ƒ / 2) โˆ’ (1 / 2))) = ((๐‘ƒ โˆ’ (๐‘ƒ / 2)) + (1 / 2)))
239112oveq1d 7365 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (๐‘ƒ โˆˆ โ„‚ โ†’ ((๐‘ƒ โˆ’ (๐‘ƒ / 2)) + (1 / 2)) = ((๐‘ƒ / 2) + (1 / 2)))
240233, 238, 2393eqtrd 2782 . . . . . . . . . . . . . . . . . . . . . . . . 25 (๐‘ƒ โˆˆ โ„‚ โ†’ (๐‘ƒ โˆ’ ((๐‘ƒ โˆ’ 1) / 2)) = ((๐‘ƒ / 2) + (1 / 2)))
24154, 227, 2403syl 18 . . . . . . . . . . . . . . . . . . . . . . . 24 (๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โ†’ (๐‘ƒ โˆ’ ((๐‘ƒ โˆ’ 1) / 2)) = ((๐‘ƒ / 2) + (1 / 2)))
242241ad2antrl 727 . . . . . . . . . . . . . . . . . . . . . . 23 (((๐‘ฆ โˆˆ โ„• โˆง ๐ป โˆˆ โ„•) โˆง (๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โˆง ยฌ 2 โˆฅ ๐‘ฆ)) โ†’ (๐‘ƒ โˆ’ ((๐‘ƒ โˆ’ 1) / 2)) = ((๐‘ƒ / 2) + (1 / 2)))
243242breq1d 5114 . . . . . . . . . . . . . . . . . . . . . 22 (((๐‘ฆ โˆˆ โ„• โˆง ๐ป โˆˆ โ„•) โˆง (๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โˆง ยฌ 2 โˆฅ ๐‘ฆ)) โ†’ ((๐‘ƒ โˆ’ ((๐‘ƒ โˆ’ 1) / 2)) โ‰ค (๐‘ƒ โˆ’ ๐‘ฆ) โ†” ((๐‘ƒ / 2) + (1 / 2)) โ‰ค (๐‘ƒ โˆ’ ๐‘ฆ)))
244 prmnn 16485 . . . . . . . . . . . . . . . . . . . . . . . . 25 (๐‘ƒ โˆˆ โ„™ โ†’ ๐‘ƒ โˆˆ โ„•)
245 halfre 12301 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (1 / 2) โˆˆ โ„
246245a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (๐‘ƒ โˆˆ โ„• โ†’ (1 / 2) โˆˆ โ„)
247 nngt0 12118 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (๐‘ƒ โˆˆ โ„• โ†’ 0 < ๐‘ƒ)
24871a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (๐‘ƒ โˆˆ โ„• โ†’ (2 โˆˆ โ„ โˆง 0 < 2))
249 divgt0 11957 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((๐‘ƒ โˆˆ โ„ โˆง 0 < ๐‘ƒ) โˆง (2 โˆˆ โ„ โˆง 0 < 2)) โ†’ 0 < (๐‘ƒ / 2))
250100, 247, 248, 249syl21anc 837 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (๐‘ƒ โˆˆ โ„• โ†’ 0 < (๐‘ƒ / 2))
251 halfgt0 12303 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 0 < (1 / 2)
252251a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (๐‘ƒ โˆˆ โ„• โ†’ 0 < (1 / 2))
253101, 246, 250, 252addgt0d 11664 . . . . . . . . . . . . . . . . . . . . . . . . 25 (๐‘ƒ โˆˆ โ„• โ†’ 0 < ((๐‘ƒ / 2) + (1 / 2)))
25454, 244, 2533syl 18 . . . . . . . . . . . . . . . . . . . . . . . 24 (๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โ†’ 0 < ((๐‘ƒ / 2) + (1 / 2)))
255254ad2antrl 727 . . . . . . . . . . . . . . . . . . . . . . 23 (((๐‘ฆ โˆˆ โ„• โˆง ๐ป โˆˆ โ„•) โˆง (๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โˆง ยฌ 2 โˆฅ ๐‘ฆ)) โ†’ 0 < ((๐‘ƒ / 2) + (1 / 2)))
256 0red 11092 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((๐‘ฆ โˆˆ โ„ โˆง ๐‘ƒ โˆˆ โ„) โ†’ 0 โˆˆ โ„)
257 simpr 486 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((๐‘ฆ โˆˆ โ„ โˆง ๐‘ƒ โˆˆ โ„) โ†’ ๐‘ƒ โˆˆ โ„)
258257rehalfcld 12334 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((๐‘ฆ โˆˆ โ„ โˆง ๐‘ƒ โˆˆ โ„) โ†’ (๐‘ƒ / 2) โˆˆ โ„)
259245a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((๐‘ฆ โˆˆ โ„ โˆง ๐‘ƒ โˆˆ โ„) โ†’ (1 / 2) โˆˆ โ„)
260258, 259readdcld 11118 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((๐‘ฆ โˆˆ โ„ โˆง ๐‘ƒ โˆˆ โ„) โ†’ ((๐‘ƒ / 2) + (1 / 2)) โˆˆ โ„)
261 resubcl 11399 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((๐‘ƒ โˆˆ โ„ โˆง ๐‘ฆ โˆˆ โ„) โ†’ (๐‘ƒ โˆ’ ๐‘ฆ) โˆˆ โ„)
262261ancoms 460 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((๐‘ฆ โˆˆ โ„ โˆง ๐‘ƒ โˆˆ โ„) โ†’ (๐‘ƒ โˆ’ ๐‘ฆ) โˆˆ โ„)
263256, 260, 2623jca 1129 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((๐‘ฆ โˆˆ โ„ โˆง ๐‘ƒ โˆˆ โ„) โ†’ (0 โˆˆ โ„ โˆง ((๐‘ƒ / 2) + (1 / 2)) โˆˆ โ„ โˆง (๐‘ƒ โˆ’ ๐‘ฆ) โˆˆ โ„))
264263ex 414 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (๐‘ฆ โˆˆ โ„ โ†’ (๐‘ƒ โˆˆ โ„ โ†’ (0 โˆˆ โ„ โˆง ((๐‘ƒ / 2) + (1 / 2)) โˆˆ โ„ โˆง (๐‘ƒ โˆ’ ๐‘ฆ) โˆˆ โ„)))
265155, 264syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (๐‘ฆ โˆˆ โ„• โ†’ (๐‘ƒ โˆˆ โ„ โ†’ (0 โˆˆ โ„ โˆง ((๐‘ƒ / 2) + (1 / 2)) โˆˆ โ„ โˆง (๐‘ƒ โˆ’ ๐‘ฆ) โˆˆ โ„)))
266265adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((๐‘ฆ โˆˆ โ„• โˆง ๐ป โˆˆ โ„•) โ†’ (๐‘ƒ โˆˆ โ„ โ†’ (0 โˆˆ โ„ โˆง ((๐‘ƒ / 2) + (1 / 2)) โˆˆ โ„ โˆง (๐‘ƒ โˆ’ ๐‘ฆ) โˆˆ โ„)))
267266com12 32 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (๐‘ƒ โˆˆ โ„ โ†’ ((๐‘ฆ โˆˆ โ„• โˆง ๐ป โˆˆ โ„•) โ†’ (0 โˆˆ โ„ โˆง ((๐‘ƒ / 2) + (1 / 2)) โˆˆ โ„ โˆง (๐‘ƒ โˆ’ ๐‘ฆ) โˆˆ โ„)))
26854, 63, 2673syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โ†’ ((๐‘ฆ โˆˆ โ„• โˆง ๐ป โˆˆ โ„•) โ†’ (0 โˆˆ โ„ โˆง ((๐‘ƒ / 2) + (1 / 2)) โˆˆ โ„ โˆง (๐‘ƒ โˆ’ ๐‘ฆ) โˆˆ โ„)))
269268adantr 482 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โˆง ยฌ 2 โˆฅ ๐‘ฆ) โ†’ ((๐‘ฆ โˆˆ โ„• โˆง ๐ป โˆˆ โ„•) โ†’ (0 โˆˆ โ„ โˆง ((๐‘ƒ / 2) + (1 / 2)) โˆˆ โ„ โˆง (๐‘ƒ โˆ’ ๐‘ฆ) โˆˆ โ„)))
270269impcom 409 . . . . . . . . . . . . . . . . . . . . . . . 24 (((๐‘ฆ โˆˆ โ„• โˆง ๐ป โˆˆ โ„•) โˆง (๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โˆง ยฌ 2 โˆฅ ๐‘ฆ)) โ†’ (0 โˆˆ โ„ โˆง ((๐‘ƒ / 2) + (1 / 2)) โˆˆ โ„ โˆง (๐‘ƒ โˆ’ ๐‘ฆ) โˆˆ โ„))
271 ltletr 11181 . . . . . . . . . . . . . . . . . . . . . . . 24 ((0 โˆˆ โ„ โˆง ((๐‘ƒ / 2) + (1 / 2)) โˆˆ โ„ โˆง (๐‘ƒ โˆ’ ๐‘ฆ) โˆˆ โ„) โ†’ ((0 < ((๐‘ƒ / 2) + (1 / 2)) โˆง ((๐‘ƒ / 2) + (1 / 2)) โ‰ค (๐‘ƒ โˆ’ ๐‘ฆ)) โ†’ 0 < (๐‘ƒ โˆ’ ๐‘ฆ)))
272270, 271syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (((๐‘ฆ โˆˆ โ„• โˆง ๐ป โˆˆ โ„•) โˆง (๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โˆง ยฌ 2 โˆฅ ๐‘ฆ)) โ†’ ((0 < ((๐‘ƒ / 2) + (1 / 2)) โˆง ((๐‘ƒ / 2) + (1 / 2)) โ‰ค (๐‘ƒ โˆ’ ๐‘ฆ)) โ†’ 0 < (๐‘ƒ โˆ’ ๐‘ฆ)))
273255, 272mpand 694 . . . . . . . . . . . . . . . . . . . . . 22 (((๐‘ฆ โˆˆ โ„• โˆง ๐ป โˆˆ โ„•) โˆง (๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โˆง ยฌ 2 โˆฅ ๐‘ฆ)) โ†’ (((๐‘ƒ / 2) + (1 / 2)) โ‰ค (๐‘ƒ โˆ’ ๐‘ฆ) โ†’ 0 < (๐‘ƒ โˆ’ ๐‘ฆ)))
274243, 273sylbid 239 . . . . . . . . . . . . . . . . . . . . 21 (((๐‘ฆ โˆˆ โ„• โˆง ๐ป โˆˆ โ„•) โˆง (๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โˆง ยฌ 2 โˆฅ ๐‘ฆ)) โ†’ ((๐‘ƒ โˆ’ ((๐‘ƒ โˆ’ 1) / 2)) โ‰ค (๐‘ƒ โˆ’ ๐‘ฆ) โ†’ 0 < (๐‘ƒ โˆ’ ๐‘ฆ)))
275226, 274sylbid 239 . . . . . . . . . . . . . . . . . . . 20 (((๐‘ฆ โˆˆ โ„• โˆง ๐ป โˆˆ โ„•) โˆง (๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โˆง ยฌ 2 โˆฅ ๐‘ฆ)) โ†’ (๐‘ฆ โ‰ค ((๐‘ƒ โˆ’ 1) / 2) โ†’ 0 < (๐‘ƒ โˆ’ ๐‘ฆ)))
276275ex 414 . . . . . . . . . . . . . . . . . . 19 ((๐‘ฆ โˆˆ โ„• โˆง ๐ป โˆˆ โ„•) โ†’ ((๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โˆง ยฌ 2 โˆฅ ๐‘ฆ) โ†’ (๐‘ฆ โ‰ค ((๐‘ƒ โˆ’ 1) / 2) โ†’ 0 < (๐‘ƒ โˆ’ ๐‘ฆ))))
277276com23 86 . . . . . . . . . . . . . . . . . 18 ((๐‘ฆ โˆˆ โ„• โˆง ๐ป โˆˆ โ„•) โ†’ (๐‘ฆ โ‰ค ((๐‘ƒ โˆ’ 1) / 2) โ†’ ((๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โˆง ยฌ 2 โˆฅ ๐‘ฆ) โ†’ 0 < (๐‘ƒ โˆ’ ๐‘ฆ))))
278189, 277biimtrid 241 . . . . . . . . . . . . . . . . 17 ((๐‘ฆ โˆˆ โ„• โˆง ๐ป โˆˆ โ„•) โ†’ (๐‘ฆ โ‰ค ๐ป โ†’ ((๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โˆง ยฌ 2 โˆฅ ๐‘ฆ) โ†’ 0 < (๐‘ƒ โˆ’ ๐‘ฆ))))
2792783impia 1118 . . . . . . . . . . . . . . . 16 ((๐‘ฆ โˆˆ โ„• โˆง ๐ป โˆˆ โ„• โˆง ๐‘ฆ โ‰ค ๐ป) โ†’ ((๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โˆง ยฌ 2 โˆฅ ๐‘ฆ) โ†’ 0 < (๐‘ƒ โˆ’ ๐‘ฆ)))
280279impcom 409 . . . . . . . . . . . . . . 15 (((๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โˆง ยฌ 2 โˆฅ ๐‘ฆ) โˆง (๐‘ฆ โˆˆ โ„• โˆง ๐ป โˆˆ โ„• โˆง ๐‘ฆ โ‰ค ๐ป)) โ†’ 0 < (๐‘ƒ โˆ’ ๐‘ฆ))
281 elnnz 12443 . . . . . . . . . . . . . . 15 ((๐‘ƒ โˆ’ ๐‘ฆ) โˆˆ โ„• โ†” ((๐‘ƒ โˆ’ ๐‘ฆ) โˆˆ โ„ค โˆง 0 < (๐‘ƒ โˆ’ ๐‘ฆ)))
282215, 280, 281sylanbrc 584 . . . . . . . . . . . . . 14 (((๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โˆง ยฌ 2 โˆฅ ๐‘ฆ) โˆง (๐‘ฆ โˆˆ โ„• โˆง ๐ป โˆˆ โ„• โˆง ๐‘ฆ โ‰ค ๐ป)) โ†’ (๐‘ƒ โˆ’ ๐‘ฆ) โˆˆ โ„•)
28323adantr 482 . . . . . . . . . . . . . . 15 ((๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โˆง ยฌ 2 โˆฅ ๐‘ฆ) โ†’ (๐‘ƒ โˆˆ โ„ค โˆง ยฌ 2 โˆฅ ๐‘ƒ))
284 simpr 486 . . . . . . . . . . . . . . . 16 ((๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โˆง ยฌ 2 โˆฅ ๐‘ฆ) โ†’ ยฌ 2 โˆฅ ๐‘ฆ)
285284, 213anim12ci 615 . . . . . . . . . . . . . . 15 (((๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โˆง ยฌ 2 โˆฅ ๐‘ฆ) โˆง (๐‘ฆ โˆˆ โ„• โˆง ๐ป โˆˆ โ„• โˆง ๐‘ฆ โ‰ค ๐ป)) โ†’ (๐‘ฆ โˆˆ โ„ค โˆง ยฌ 2 โˆฅ ๐‘ฆ))
286 omoe 16181 . . . . . . . . . . . . . . 15 (((๐‘ƒ โˆˆ โ„ค โˆง ยฌ 2 โˆฅ ๐‘ƒ) โˆง (๐‘ฆ โˆˆ โ„ค โˆง ยฌ 2 โˆฅ ๐‘ฆ)) โ†’ 2 โˆฅ (๐‘ƒ โˆ’ ๐‘ฆ))
287283, 285, 286syl2an2r 684 . . . . . . . . . . . . . 14 (((๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โˆง ยฌ 2 โˆฅ ๐‘ฆ) โˆง (๐‘ฆ โˆˆ โ„• โˆง ๐ป โˆˆ โ„• โˆง ๐‘ฆ โ‰ค ๐ป)) โ†’ 2 โˆฅ (๐‘ƒ โˆ’ ๐‘ฆ))
288 nnehalf 16196 . . . . . . . . . . . . . 14 (((๐‘ƒ โˆ’ ๐‘ฆ) โˆˆ โ„• โˆง 2 โˆฅ (๐‘ƒ โˆ’ ๐‘ฆ)) โ†’ ((๐‘ƒ โˆ’ ๐‘ฆ) / 2) โˆˆ โ„•)
289282, 287, 288syl2anc 585 . . . . . . . . . . . . 13 (((๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โˆง ยฌ 2 โˆฅ ๐‘ฆ) โˆง (๐‘ฆ โˆˆ โ„• โˆง ๐ป โˆˆ โ„• โˆง ๐‘ฆ โ‰ค ๐ป)) โ†’ ((๐‘ƒ โˆ’ ๐‘ฆ) / 2) โˆˆ โ„•)
290 simpr2 1196 . . . . . . . . . . . . 13 (((๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โˆง ยฌ 2 โˆฅ ๐‘ฆ) โˆง (๐‘ฆ โˆˆ โ„• โˆง ๐ป โˆˆ โ„• โˆง ๐‘ฆ โ‰ค ๐ป)) โ†’ ๐ป โˆˆ โ„•)
291 1red 11090 . . . . . . . . . . . . . . . 16 (((๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โˆง ยฌ 2 โˆฅ ๐‘ฆ) โˆง (๐‘ฆ โˆˆ โ„• โˆง ๐ป โˆˆ โ„• โˆง ๐‘ฆ โ‰ค ๐ป)) โ†’ 1 โˆˆ โ„)
2921553ad2ant1 1134 . . . . . . . . . . . . . . . . 17 ((๐‘ฆ โˆˆ โ„• โˆง ๐ป โˆˆ โ„• โˆง ๐‘ฆ โ‰ค ๐ป) โ†’ ๐‘ฆ โˆˆ โ„)
293292adantl 483 . . . . . . . . . . . . . . . 16 (((๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โˆง ยฌ 2 โˆฅ ๐‘ฆ) โˆง (๐‘ฆ โˆˆ โ„• โˆง ๐ป โˆˆ โ„• โˆง ๐‘ฆ โ‰ค ๐ป)) โ†’ ๐‘ฆ โˆˆ โ„)
29454, 63syl 17 . . . . . . . . . . . . . . . . 17 (๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โ†’ ๐‘ƒ โˆˆ โ„)
295294ad2antrr 725 . . . . . . . . . . . . . . . 16 (((๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โˆง ยฌ 2 โˆฅ ๐‘ฆ) โˆง (๐‘ฆ โˆˆ โ„• โˆง ๐ป โˆˆ โ„• โˆง ๐‘ฆ โ‰ค ๐ป)) โ†’ ๐‘ƒ โˆˆ โ„)
296 nnge1 12115 . . . . . . . . . . . . . . . . . 18 (๐‘ฆ โˆˆ โ„• โ†’ 1 โ‰ค ๐‘ฆ)
2972963ad2ant1 1134 . . . . . . . . . . . . . . . . 17 ((๐‘ฆ โˆˆ โ„• โˆง ๐ป โˆˆ โ„• โˆง ๐‘ฆ โ‰ค ๐ป) โ†’ 1 โ‰ค ๐‘ฆ)
298297adantl 483 . . . . . . . . . . . . . . . 16 (((๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โˆง ยฌ 2 โˆฅ ๐‘ฆ) โˆง (๐‘ฆ โˆˆ โ„• โˆง ๐ป โˆˆ โ„• โˆง ๐‘ฆ โ‰ค ๐ป)) โ†’ 1 โ‰ค ๐‘ฆ)
299291, 293, 295, 298lesub2dd 11706 . . . . . . . . . . . . . . 15 (((๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โˆง ยฌ 2 โˆฅ ๐‘ฆ) โˆง (๐‘ฆ โˆˆ โ„• โˆง ๐ป โˆˆ โ„• โˆง ๐‘ฆ โ‰ค ๐ป)) โ†’ (๐‘ƒ โˆ’ ๐‘ฆ) โ‰ค (๐‘ƒ โˆ’ 1))
300295, 293resubcld 11517 . . . . . . . . . . . . . . . 16 (((๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โˆง ยฌ 2 โˆฅ ๐‘ฆ) โˆง (๐‘ฆ โˆˆ โ„• โˆง ๐ป โˆˆ โ„• โˆง ๐‘ฆ โ‰ค ๐ป)) โ†’ (๐‘ƒ โˆ’ ๐‘ฆ) โˆˆ โ„)
30154, 63, 673syl 18 . . . . . . . . . . . . . . . . 17 (๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โ†’ (๐‘ƒ โˆ’ 1) โˆˆ โ„)
302301ad2antrr 725 . . . . . . . . . . . . . . . 16 (((๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โˆง ยฌ 2 โˆฅ ๐‘ฆ) โˆง (๐‘ฆ โˆˆ โ„• โˆง ๐ป โˆˆ โ„• โˆง ๐‘ฆ โ‰ค ๐ป)) โ†’ (๐‘ƒ โˆ’ 1) โˆˆ โ„)
30371a1i 11 . . . . . . . . . . . . . . . 16 (((๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โˆง ยฌ 2 โˆฅ ๐‘ฆ) โˆง (๐‘ฆ โˆˆ โ„• โˆง ๐ป โˆˆ โ„• โˆง ๐‘ฆ โ‰ค ๐ป)) โ†’ (2 โˆˆ โ„ โˆง 0 < 2))
304 lediv1 11954 . . . . . . . . . . . . . . . 16 (((๐‘ƒ โˆ’ ๐‘ฆ) โˆˆ โ„ โˆง (๐‘ƒ โˆ’ 1) โˆˆ โ„ โˆง (2 โˆˆ โ„ โˆง 0 < 2)) โ†’ ((๐‘ƒ โˆ’ ๐‘ฆ) โ‰ค (๐‘ƒ โˆ’ 1) โ†” ((๐‘ƒ โˆ’ ๐‘ฆ) / 2) โ‰ค ((๐‘ƒ โˆ’ 1) / 2)))
305300, 302, 303, 304syl3anc 1372 . . . . . . . . . . . . . . 15 (((๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โˆง ยฌ 2 โˆฅ ๐‘ฆ) โˆง (๐‘ฆ โˆˆ โ„• โˆง ๐ป โˆˆ โ„• โˆง ๐‘ฆ โ‰ค ๐ป)) โ†’ ((๐‘ƒ โˆ’ ๐‘ฆ) โ‰ค (๐‘ƒ โˆ’ 1) โ†” ((๐‘ƒ โˆ’ ๐‘ฆ) / 2) โ‰ค ((๐‘ƒ โˆ’ 1) / 2)))
306299, 305mpbid 231 . . . . . . . . . . . . . 14 (((๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โˆง ยฌ 2 โˆฅ ๐‘ฆ) โˆง (๐‘ฆ โˆˆ โ„• โˆง ๐ป โˆˆ โ„• โˆง ๐‘ฆ โ‰ค ๐ป)) โ†’ ((๐‘ƒ โˆ’ ๐‘ฆ) / 2) โ‰ค ((๐‘ƒ โˆ’ 1) / 2))
30714breq2i 5112 . . . . . . . . . . . . . 14 (((๐‘ƒ โˆ’ ๐‘ฆ) / 2) โ‰ค ๐ป โ†” ((๐‘ƒ โˆ’ ๐‘ฆ) / 2) โ‰ค ((๐‘ƒ โˆ’ 1) / 2))
308306, 307sylibr 233 . . . . . . . . . . . . 13 (((๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โˆง ยฌ 2 โˆฅ ๐‘ฆ) โˆง (๐‘ฆ โˆˆ โ„• โˆง ๐ป โˆˆ โ„• โˆง ๐‘ฆ โ‰ค ๐ป)) โ†’ ((๐‘ƒ โˆ’ ๐‘ฆ) / 2) โ‰ค ๐ป)
309289, 290, 3083jca 1129 . . . . . . . . . . . 12 (((๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โˆง ยฌ 2 โˆฅ ๐‘ฆ) โˆง (๐‘ฆ โˆˆ โ„• โˆง ๐ป โˆˆ โ„• โˆง ๐‘ฆ โ‰ค ๐ป)) โ†’ (((๐‘ƒ โˆ’ ๐‘ฆ) / 2) โˆˆ โ„• โˆง ๐ป โˆˆ โ„• โˆง ((๐‘ƒ โˆ’ ๐‘ฆ) / 2) โ‰ค ๐ป))
310309ex 414 . . . . . . . . . . 11 ((๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โˆง ยฌ 2 โˆฅ ๐‘ฆ) โ†’ ((๐‘ฆ โˆˆ โ„• โˆง ๐ป โˆˆ โ„• โˆง ๐‘ฆ โ‰ค ๐ป) โ†’ (((๐‘ƒ โˆ’ ๐‘ฆ) / 2) โˆˆ โ„• โˆง ๐ป โˆˆ โ„• โˆง ((๐‘ƒ โˆ’ ๐‘ฆ) / 2) โ‰ค ๐ป)))
311 elfz1b 13439 . . . . . . . . . . 11 (((๐‘ƒ โˆ’ ๐‘ฆ) / 2) โˆˆ (1...๐ป) โ†” (((๐‘ƒ โˆ’ ๐‘ฆ) / 2) โˆˆ โ„• โˆง ๐ป โˆˆ โ„• โˆง ((๐‘ƒ โˆ’ ๐‘ฆ) / 2) โ‰ค ๐ป))
312310, 149, 3113imtr4g 296 . . . . . . . . . 10 ((๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โˆง ยฌ 2 โˆฅ ๐‘ฆ) โ†’ (๐‘ฆ โˆˆ (1...๐ป) โ†’ ((๐‘ƒ โˆ’ ๐‘ฆ) / 2) โˆˆ (1...๐ป)))
313312ex 414 . . . . . . . . 9 (๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โ†’ (ยฌ 2 โˆฅ ๐‘ฆ โ†’ (๐‘ฆ โˆˆ (1...๐ป) โ†’ ((๐‘ƒ โˆ’ ๐‘ฆ) / 2) โˆˆ (1...๐ป))))
31419, 313syl 17 . . . . . . . 8 (๐œ‘ โ†’ (ยฌ 2 โˆฅ ๐‘ฆ โ†’ (๐‘ฆ โˆˆ (1...๐ป) โ†’ ((๐‘ƒ โˆ’ ๐‘ฆ) / 2) โˆˆ (1...๐ป))))
3153143imp21 1115 . . . . . . 7 ((ยฌ 2 โˆฅ ๐‘ฆ โˆง ๐œ‘ โˆง ๐‘ฆ โˆˆ (1...๐ป)) โ†’ ((๐‘ƒ โˆ’ ๐‘ฆ) / 2) โˆˆ (1...๐ป))
316 oveq1 7357 . . . . . . . . . . 11 (๐‘ฅ = ((๐‘ƒ โˆ’ ๐‘ฆ) / 2) โ†’ (๐‘ฅ ยท 2) = (((๐‘ƒ โˆ’ ๐‘ฆ) / 2) ยท 2))
317316breq1d 5114 . . . . . . . . . 10 (๐‘ฅ = ((๐‘ƒ โˆ’ ๐‘ฆ) / 2) โ†’ ((๐‘ฅ ยท 2) < (๐‘ƒ / 2) โ†” (((๐‘ƒ โˆ’ ๐‘ฆ) / 2) ยท 2) < (๐‘ƒ / 2)))
318316oveq2d 7366 . . . . . . . . . 10 (๐‘ฅ = ((๐‘ƒ โˆ’ ๐‘ฆ) / 2) โ†’ (๐‘ƒ โˆ’ (๐‘ฅ ยท 2)) = (๐‘ƒ โˆ’ (((๐‘ƒ โˆ’ ๐‘ฆ) / 2) ยท 2)))
319317, 316, 318ifbieq12d 4513 . . . . . . . . 9 (๐‘ฅ = ((๐‘ƒ โˆ’ ๐‘ฆ) / 2) โ†’ if((๐‘ฅ ยท 2) < (๐‘ƒ / 2), (๐‘ฅ ยท 2), (๐‘ƒ โˆ’ (๐‘ฅ ยท 2))) = if((((๐‘ƒ โˆ’ ๐‘ฆ) / 2) ยท 2) < (๐‘ƒ / 2), (((๐‘ƒ โˆ’ ๐‘ฆ) / 2) ยท 2), (๐‘ƒ โˆ’ (((๐‘ƒ โˆ’ ๐‘ฆ) / 2) ยท 2))))
320319eqeq2d 2749 . . . . . . . 8 (๐‘ฅ = ((๐‘ƒ โˆ’ ๐‘ฆ) / 2) โ†’ (๐‘ฆ = if((๐‘ฅ ยท 2) < (๐‘ƒ / 2), (๐‘ฅ ยท 2), (๐‘ƒ โˆ’ (๐‘ฅ ยท 2))) โ†” ๐‘ฆ = if((((๐‘ƒ โˆ’ ๐‘ฆ) / 2) ยท 2) < (๐‘ƒ / 2), (((๐‘ƒ โˆ’ ๐‘ฆ) / 2) ยท 2), (๐‘ƒ โˆ’ (((๐‘ƒ โˆ’ ๐‘ฆ) / 2) ยท 2)))))
321320adantl 483 . . . . . . 7 (((ยฌ 2 โˆฅ ๐‘ฆ โˆง ๐œ‘ โˆง ๐‘ฆ โˆˆ (1...๐ป)) โˆง ๐‘ฅ = ((๐‘ƒ โˆ’ ๐‘ฆ) / 2)) โ†’ (๐‘ฆ = if((๐‘ฅ ยท 2) < (๐‘ƒ / 2), (๐‘ฅ ยท 2), (๐‘ƒ โˆ’ (๐‘ฅ ยท 2))) โ†” ๐‘ฆ = if((((๐‘ƒ โˆ’ ๐‘ฆ) / 2) ยท 2) < (๐‘ƒ / 2), (((๐‘ƒ โˆ’ ๐‘ฆ) / 2) ยท 2), (๐‘ƒ โˆ’ (((๐‘ƒ โˆ’ ๐‘ฆ) / 2) ยท 2)))))
32219, 54, 2273syl 18 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ๐‘ƒ โˆˆ โ„‚)
3233223ad2ant2 1135 . . . . . . . . . . . 12 ((ยฌ 2 โˆฅ ๐‘ฆ โˆง ๐œ‘ โˆง ๐‘ฆ โˆˆ (1...๐ป)) โ†’ ๐‘ƒ โˆˆ โ„‚)
3241833ad2ant3 1136 . . . . . . . . . . . 12 ((ยฌ 2 โˆฅ ๐‘ฆ โˆง ๐œ‘ โˆง ๐‘ฆ โˆˆ (1...๐ป)) โ†’ ๐‘ฆ โˆˆ โ„‚)
325323, 324subcld 11446 . . . . . . . . . . 11 ((ยฌ 2 โˆฅ ๐‘ฆ โˆง ๐œ‘ โˆง ๐‘ฆ โˆˆ (1...๐ป)) โ†’ (๐‘ƒ โˆ’ ๐‘ฆ) โˆˆ โ„‚)
326 2cnd 12165 . . . . . . . . . . 11 ((ยฌ 2 โˆฅ ๐‘ฆ โˆง ๐œ‘ โˆง ๐‘ฆ โˆˆ (1...๐ป)) โ†’ 2 โˆˆ โ„‚)
327186a1i 11 . . . . . . . . . . 11 ((ยฌ 2 โˆฅ ๐‘ฆ โˆง ๐œ‘ โˆง ๐‘ฆ โˆˆ (1...๐ป)) โ†’ 2 โ‰  0)
328325, 326, 327divcan1d 11866 . . . . . . . . . 10 ((ยฌ 2 โˆฅ ๐‘ฆ โˆง ๐œ‘ โˆง ๐‘ฆ โˆˆ (1...๐ป)) โ†’ (((๐‘ƒ โˆ’ ๐‘ฆ) / 2) ยท 2) = (๐‘ƒ โˆ’ ๐‘ฆ))
329 zre 12437 . . . . . . . . . . . . . . . . . . . . 21 (๐‘ƒ โˆˆ โ„ค โ†’ ๐‘ƒ โˆˆ โ„)
330 halfge0 12304 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 0 โ‰ค (1 / 2)
331 rehalfcl 12313 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (๐‘ƒ โˆˆ โ„ โ†’ (๐‘ƒ / 2) โˆˆ โ„)
332331adantl 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((๐‘ฆ โˆˆ โ„ โˆง ๐‘ƒ โˆˆ โ„) โ†’ (๐‘ƒ / 2) โˆˆ โ„)
333332, 259subge02d 11681 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((๐‘ฆ โˆˆ โ„ โˆง ๐‘ƒ โˆˆ โ„) โ†’ (0 โ‰ค (1 / 2) โ†” ((๐‘ƒ / 2) โˆ’ (1 / 2)) โ‰ค (๐‘ƒ / 2)))
334330, 333mpbii 232 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((๐‘ฆ โˆˆ โ„ โˆง ๐‘ƒ โˆˆ โ„) โ†’ ((๐‘ƒ / 2) โˆ’ (1 / 2)) โ‰ค (๐‘ƒ / 2))
335 simpl 484 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((๐‘ฆ โˆˆ โ„ โˆง ๐‘ƒ โˆˆ โ„) โ†’ ๐‘ฆ โˆˆ โ„)
336245a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (๐‘ƒ โˆˆ โ„ โ†’ (1 / 2) โˆˆ โ„)
337331, 336resubcld 11517 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (๐‘ƒ โˆˆ โ„ โ†’ ((๐‘ƒ / 2) โˆ’ (1 / 2)) โˆˆ โ„)
338337adantl 483 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((๐‘ฆ โˆˆ โ„ โˆง ๐‘ƒ โˆˆ โ„) โ†’ ((๐‘ƒ / 2) โˆ’ (1 / 2)) โˆˆ โ„)
339 letr 11183 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((๐‘ฆ โˆˆ โ„ โˆง ((๐‘ƒ / 2) โˆ’ (1 / 2)) โˆˆ โ„ โˆง (๐‘ƒ / 2) โˆˆ โ„) โ†’ ((๐‘ฆ โ‰ค ((๐‘ƒ / 2) โˆ’ (1 / 2)) โˆง ((๐‘ƒ / 2) โˆ’ (1 / 2)) โ‰ค (๐‘ƒ / 2)) โ†’ ๐‘ฆ โ‰ค (๐‘ƒ / 2)))
340335, 338, 332, 339syl3anc 1372 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((๐‘ฆ โˆˆ โ„ โˆง ๐‘ƒ โˆˆ โ„) โ†’ ((๐‘ฆ โ‰ค ((๐‘ƒ / 2) โˆ’ (1 / 2)) โˆง ((๐‘ƒ / 2) โˆ’ (1 / 2)) โ‰ค (๐‘ƒ / 2)) โ†’ ๐‘ฆ โ‰ค (๐‘ƒ / 2)))
341334, 340mpan2d 693 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((๐‘ฆ โˆˆ โ„ โˆง ๐‘ƒ โˆˆ โ„) โ†’ (๐‘ฆ โ‰ค ((๐‘ƒ / 2) โˆ’ (1 / 2)) โ†’ ๐‘ฆ โ‰ค (๐‘ƒ / 2)))
34280adantl 483 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((๐‘ฆ โˆˆ โ„ โˆง ๐‘ƒ โˆˆ โ„) โ†’ ๐‘ƒ โˆˆ โ„‚)
343 1cnd 11084 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((๐‘ฆ โˆˆ โ„ โˆง ๐‘ƒ โˆˆ โ„) โ†’ 1 โˆˆ โ„‚)
344229a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((๐‘ฆ โˆˆ โ„ โˆง ๐‘ƒ โˆˆ โ„) โ†’ (2 โˆˆ โ„‚ โˆง 2 โ‰  0))
345342, 343, 344, 231syl3anc 1372 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((๐‘ฆ โˆˆ โ„ โˆง ๐‘ƒ โˆˆ โ„) โ†’ ((๐‘ƒ โˆ’ 1) / 2) = ((๐‘ƒ / 2) โˆ’ (1 / 2)))
346345breq2d 5116 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((๐‘ฆ โˆˆ โ„ โˆง ๐‘ƒ โˆˆ โ„) โ†’ (๐‘ฆ โ‰ค ((๐‘ƒ โˆ’ 1) / 2) โ†” ๐‘ฆ โ‰ค ((๐‘ƒ / 2) โˆ’ (1 / 2))))
347 lesub 11568 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((๐‘ƒ / 2) โˆˆ โ„ โˆง ๐‘ƒ โˆˆ โ„ โˆง ๐‘ฆ โˆˆ โ„) โ†’ ((๐‘ƒ / 2) โ‰ค (๐‘ƒ โˆ’ ๐‘ฆ) โ†” ๐‘ฆ โ‰ค (๐‘ƒ โˆ’ (๐‘ƒ / 2))))
348332, 257, 335, 347syl3anc 1372 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((๐‘ฆ โˆˆ โ„ โˆง ๐‘ƒ โˆˆ โ„) โ†’ ((๐‘ƒ / 2) โ‰ค (๐‘ƒ โˆ’ ๐‘ฆ) โ†” ๐‘ฆ โ‰ค (๐‘ƒ โˆ’ (๐‘ƒ / 2))))
349258, 262lenltd 11235 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((๐‘ฆ โˆˆ โ„ โˆง ๐‘ƒ โˆˆ โ„) โ†’ ((๐‘ƒ / 2) โ‰ค (๐‘ƒ โˆ’ ๐‘ฆ) โ†” ยฌ (๐‘ƒ โˆ’ ๐‘ฆ) < (๐‘ƒ / 2)))
350 2cnd 12165 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (๐‘ƒ โˆˆ โ„ โ†’ 2 โˆˆ โ„‚)
351186a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (๐‘ƒ โˆˆ โ„ โ†’ 2 โ‰  0)
35280, 350, 351divcan1d 11866 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (๐‘ƒ โˆˆ โ„ โ†’ ((๐‘ƒ / 2) ยท 2) = ๐‘ƒ)
353352eqcomd 2744 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (๐‘ƒ โˆˆ โ„ โ†’ ๐‘ƒ = ((๐‘ƒ / 2) ยท 2))
354353oveq1d 7365 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (๐‘ƒ โˆˆ โ„ โ†’ (๐‘ƒ โˆ’ (๐‘ƒ / 2)) = (((๐‘ƒ / 2) ยท 2) โˆ’ (๐‘ƒ / 2)))
355331recnd 11117 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (๐‘ƒ โˆˆ โ„ โ†’ (๐‘ƒ / 2) โˆˆ โ„‚)
356355, 350mulcomd 11110 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (๐‘ƒ โˆˆ โ„ โ†’ ((๐‘ƒ / 2) ยท 2) = (2 ยท (๐‘ƒ / 2)))
357356oveq1d 7365 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (๐‘ƒ โˆˆ โ„ โ†’ (((๐‘ƒ / 2) ยท 2) โˆ’ (๐‘ƒ / 2)) = ((2 ยท (๐‘ƒ / 2)) โˆ’ (๐‘ƒ / 2)))
358350, 355mulsubfacd 11550 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (๐‘ƒ โˆˆ โ„ โ†’ ((2 ยท (๐‘ƒ / 2)) โˆ’ (๐‘ƒ / 2)) = ((2 โˆ’ 1) ยท (๐‘ƒ / 2)))
359 2m1e1 12213 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (2 โˆ’ 1) = 1
360359a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (๐‘ƒ โˆˆ โ„ โ†’ (2 โˆ’ 1) = 1)
361360oveq1d 7365 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (๐‘ƒ โˆˆ โ„ โ†’ ((2 โˆ’ 1) ยท (๐‘ƒ / 2)) = (1 ยท (๐‘ƒ / 2)))
362355mulid2d 11107 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (๐‘ƒ โˆˆ โ„ โ†’ (1 ยท (๐‘ƒ / 2)) = (๐‘ƒ / 2))
363358, 361, 3623eqtrd 2782 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (๐‘ƒ โˆˆ โ„ โ†’ ((2 ยท (๐‘ƒ / 2)) โˆ’ (๐‘ƒ / 2)) = (๐‘ƒ / 2))
364354, 357, 3633eqtrd 2782 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (๐‘ƒ โˆˆ โ„ โ†’ (๐‘ƒ โˆ’ (๐‘ƒ / 2)) = (๐‘ƒ / 2))
365364adantl 483 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((๐‘ฆ โˆˆ โ„ โˆง ๐‘ƒ โˆˆ โ„) โ†’ (๐‘ƒ โˆ’ (๐‘ƒ / 2)) = (๐‘ƒ / 2))
366365breq2d 5116 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((๐‘ฆ โˆˆ โ„ โˆง ๐‘ƒ โˆˆ โ„) โ†’ (๐‘ฆ โ‰ค (๐‘ƒ โˆ’ (๐‘ƒ / 2)) โ†” ๐‘ฆ โ‰ค (๐‘ƒ / 2)))
367348, 349, 3663bitr3d 309 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((๐‘ฆ โˆˆ โ„ โˆง ๐‘ƒ โˆˆ โ„) โ†’ (ยฌ (๐‘ƒ โˆ’ ๐‘ฆ) < (๐‘ƒ / 2) โ†” ๐‘ฆ โ‰ค (๐‘ƒ / 2)))
368341, 346, 3673imtr4d 294 . . . . . . . . . . . . . . . . . . . . . . . 24 ((๐‘ฆ โˆˆ โ„ โˆง ๐‘ƒ โˆˆ โ„) โ†’ (๐‘ฆ โ‰ค ((๐‘ƒ โˆ’ 1) / 2) โ†’ ยฌ (๐‘ƒ โˆ’ ๐‘ฆ) < (๐‘ƒ / 2)))
369368ex 414 . . . . . . . . . . . . . . . . . . . . . . 23 (๐‘ฆ โˆˆ โ„ โ†’ (๐‘ƒ โˆˆ โ„ โ†’ (๐‘ฆ โ‰ค ((๐‘ƒ โˆ’ 1) / 2) โ†’ ยฌ (๐‘ƒ โˆ’ ๐‘ฆ) < (๐‘ƒ / 2))))
370155, 369syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (๐‘ฆ โˆˆ โ„• โ†’ (๐‘ƒ โˆˆ โ„ โ†’ (๐‘ฆ โ‰ค ((๐‘ƒ โˆ’ 1) / 2) โ†’ ยฌ (๐‘ƒ โˆ’ ๐‘ฆ) < (๐‘ƒ / 2))))
371370com3l 89 . . . . . . . . . . . . . . . . . . . . 21 (๐‘ƒ โˆˆ โ„ โ†’ (๐‘ฆ โ‰ค ((๐‘ƒ โˆ’ 1) / 2) โ†’ (๐‘ฆ โˆˆ โ„• โ†’ ยฌ (๐‘ƒ โˆ’ ๐‘ฆ) < (๐‘ƒ / 2))))
372329, 371syl 17 . . . . . . . . . . . . . . . . . . . 20 (๐‘ƒ โˆˆ โ„ค โ†’ (๐‘ฆ โ‰ค ((๐‘ƒ โˆ’ 1) / 2) โ†’ (๐‘ฆ โˆˆ โ„• โ†’ ยฌ (๐‘ƒ โˆ’ ๐‘ฆ) < (๐‘ƒ / 2))))
37354, 55, 3723syl 18 . . . . . . . . . . . . . . . . . . 19 (๐‘ƒ โˆˆ (โ„™ โˆ– {2}) โ†’ (๐‘ฆ โ‰ค ((๐‘ƒ โˆ’ 1) / 2) โ†’ (๐‘ฆ โˆˆ โ„• โ†’ ยฌ (๐‘ƒ โˆ’ ๐‘ฆ) < (๐‘ƒ / 2))))
37419, 373syl 17 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ (๐‘ฆ โ‰ค ((๐‘ƒ โˆ’ 1) / 2) โ†’ (๐‘ฆ โˆˆ โ„• โ†’ ยฌ (๐‘ƒ โˆ’ ๐‘ฆ) < (๐‘ƒ / 2))))
375374adantl 483 . . . . . . . . . . . . . . . . 17 ((ยฌ 2 โˆฅ ๐‘ฆ โˆง ๐œ‘) โ†’ (๐‘ฆ โ‰ค ((๐‘ƒ โˆ’ 1) / 2) โ†’ (๐‘ฆ โˆˆ โ„• โ†’ ยฌ (๐‘ƒ โˆ’ ๐‘ฆ) < (๐‘ƒ / 2))))
376375com13 88 . . . . . . . . . . . . . . . 16 (๐‘ฆ โˆˆ โ„• โ†’ (๐‘ฆ โ‰ค ((๐‘ƒ โˆ’ 1) / 2) โ†’ ((ยฌ 2 โˆฅ ๐‘ฆ โˆง ๐œ‘) โ†’ ยฌ (๐‘ƒ โˆ’ ๐‘ฆ) < (๐‘ƒ / 2))))
377189, 376biimtrid 241 . . . . . . . . . . . . . . 15 (๐‘ฆ โˆˆ โ„• โ†’ (๐‘ฆ โ‰ค ๐ป โ†’ ((ยฌ 2 โˆฅ ๐‘ฆ โˆง ๐œ‘) โ†’ ยฌ (๐‘ƒ โˆ’ ๐‘ฆ) < (๐‘ƒ / 2))))
378377a1d 25 . . . . . . . . . . . . . 14 (๐‘ฆ โˆˆ โ„• โ†’ (๐ป โˆˆ โ„• โ†’ (๐‘ฆ โ‰ค ๐ป โ†’ ((ยฌ 2 โˆฅ ๐‘ฆ โˆง ๐œ‘) โ†’ ยฌ (๐‘ƒ โˆ’ ๐‘ฆ) < (๐‘ƒ / 2)))))
3793783imp 1112 . . . . . . . . . . . . 13 ((๐‘ฆ โˆˆ โ„• โˆง ๐ป โˆˆ โ„• โˆง ๐‘ฆ โ‰ค ๐ป) โ†’ ((ยฌ 2 โˆฅ ๐‘ฆ โˆง ๐œ‘) โ†’ ยฌ (๐‘ƒ โˆ’ ๐‘ฆ) < (๐‘ƒ / 2)))
380379com12 32 . . . . . . . . . . . 12 ((ยฌ 2 โˆฅ ๐‘ฆ โˆง ๐œ‘) โ†’ ((๐‘ฆ โˆˆ โ„• โˆง ๐ป โˆˆ โ„• โˆง ๐‘ฆ โ‰ค ๐ป) โ†’ ยฌ (๐‘ƒ โˆ’ ๐‘ฆ) < (๐‘ƒ / 2)))
381149, 380biimtrid 241 . . . . . . . . . . 11 ((ยฌ 2 โˆฅ ๐‘ฆ โˆง ๐œ‘) โ†’ (๐‘ฆ โˆˆ (1...๐ป) โ†’ ยฌ (๐‘ƒ โˆ’ ๐‘ฆ) < (๐‘ƒ / 2)))
3823813impia 1118 . . . . . . . . . 10 ((ยฌ 2 โˆฅ ๐‘ฆ โˆง ๐œ‘ โˆง ๐‘ฆ โˆˆ (1...๐ป)) โ†’ ยฌ (๐‘ƒ โˆ’ ๐‘ฆ) < (๐‘ƒ / 2))
383328, 382eqnbrtrd 5122 . . . . . . . . 9 ((ยฌ 2 โˆฅ ๐‘ฆ โˆง ๐œ‘ โˆง ๐‘ฆ โˆˆ (1...๐ป)) โ†’ ยฌ (((๐‘ƒ โˆ’ ๐‘ฆ) / 2) ยท 2) < (๐‘ƒ / 2))
384383iffalsed 4496 . . . . . . . 8 ((ยฌ 2 โˆฅ ๐‘ฆ โˆง ๐œ‘ โˆง ๐‘ฆ โˆˆ (1...๐ป)) โ†’ if((((๐‘ƒ โˆ’ ๐‘ฆ) / 2) ยท 2) < (๐‘ƒ / 2), (((๐‘ƒ โˆ’ ๐‘ฆ) / 2) ยท 2), (๐‘ƒ โˆ’ (((๐‘ƒ โˆ’ ๐‘ฆ) / 2) ยท 2))) = (๐‘ƒ โˆ’ (((๐‘ƒ โˆ’ ๐‘ฆ) / 2) ยท 2)))
385328oveq2d 7366 . . . . . . . 8 ((ยฌ 2 โˆฅ ๐‘ฆ โˆง ๐œ‘ โˆง ๐‘ฆ โˆˆ (1...๐ป)) โ†’ (๐‘ƒ โˆ’ (((๐‘ƒ โˆ’ ๐‘ฆ) / 2) ยท 2)) = (๐‘ƒ โˆ’ (๐‘ƒ โˆ’ ๐‘ฆ)))
386322, 183anim12i 614 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘ฆ โˆˆ (1...๐ป)) โ†’ (๐‘ƒ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‚))
3873863adant1 1131 . . . . . . . . 9 ((ยฌ 2 โˆฅ ๐‘ฆ โˆง ๐œ‘ โˆง ๐‘ฆ โˆˆ (1...๐ป)) โ†’ (๐‘ƒ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‚))
388 nncan 11364 . . . . . . . . 9 ((๐‘ƒ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‚) โ†’ (๐‘ƒ โˆ’ (๐‘ƒ โˆ’ ๐‘ฆ)) = ๐‘ฆ)
389387, 388syl 17 . . . . . . . 8 ((ยฌ 2 โˆฅ ๐‘ฆ โˆง ๐œ‘ โˆง ๐‘ฆ โˆˆ (1...๐ป)) โ†’ (๐‘ƒ โˆ’ (๐‘ƒ โˆ’ ๐‘ฆ)) = ๐‘ฆ)
390384, 385, 3893eqtrrd 2783 . . . . . . 7 ((ยฌ 2 โˆฅ ๐‘ฆ โˆง ๐œ‘ โˆง ๐‘ฆ โˆˆ (1...๐ป)) โ†’ ๐‘ฆ = if((((๐‘ƒ โˆ’ ๐‘ฆ) / 2) ยท 2) < (๐‘ƒ / 2), (((๐‘ƒ โˆ’ ๐‘ฆ) / 2) ยท 2), (๐‘ƒ โˆ’ (((๐‘ƒ โˆ’ ๐‘ฆ) / 2) ยท 2))))
391315, 321, 390rspcedvd 3582 . . . . . 6 ((ยฌ 2 โˆฅ ๐‘ฆ โˆง ๐œ‘ โˆง ๐‘ฆ โˆˆ (1...๐ป)) โ†’ โˆƒ๐‘ฅ โˆˆ (1...๐ป)๐‘ฆ = if((๐‘ฅ ยท 2) < (๐‘ƒ / 2), (๐‘ฅ ยท 2), (๐‘ƒ โˆ’ (๐‘ฅ ยท 2))))
3923913exp 1120 . . . . 5 (ยฌ 2 โˆฅ ๐‘ฆ โ†’ (๐œ‘ โ†’ (๐‘ฆ โˆˆ (1...๐ป) โ†’ โˆƒ๐‘ฅ โˆˆ (1...๐ป)๐‘ฆ = if((๐‘ฅ ยท 2) < (๐‘ƒ / 2), (๐‘ฅ ยท 2), (๐‘ƒ โˆ’ (๐‘ฅ ยท 2))))))
393210, 392pm2.61i 182 . . . 4 (๐œ‘ โ†’ (๐‘ฆ โˆˆ (1...๐ป) โ†’ โˆƒ๐‘ฅ โˆˆ (1...๐ป)๐‘ฆ = if((๐‘ฅ ยท 2) < (๐‘ƒ / 2), (๐‘ฅ ยท 2), (๐‘ƒ โˆ’ (๐‘ฅ ยท 2)))))
394148, 393impbid 211 . . 3 (๐œ‘ โ†’ (โˆƒ๐‘ฅ โˆˆ (1...๐ป)๐‘ฆ = if((๐‘ฅ ยท 2) < (๐‘ƒ / 2), (๐‘ฅ ยท 2), (๐‘ƒ โˆ’ (๐‘ฅ ยท 2))) โ†” ๐‘ฆ โˆˆ (1...๐ป)))
3953, 394bitrid 283 . 2 (๐œ‘ โ†’ (๐‘ฆ โˆˆ ran ๐‘… โ†” ๐‘ฆ โˆˆ (1...๐ป)))
396395eqrdv 2736 1 (๐œ‘ โ†’ ran ๐‘… = (1...๐ป))
Colors of variables: wff setvar class
Syntax hints:  ยฌ wn 3   โ†’ wi 4   โ†” wb 205   โˆง wa 397   โˆง w3a 1088   = wceq 1542   โˆˆ wcel 2107   โ‰  wne 2942  โˆƒwrex 3072  Vcvv 3444   โˆ– cdif 3906  ifcif 4485  {csn 4585   class class class wbr 5104   โ†ฆ cmpt 5187  ran crn 5632  (class class class)co 7350  โ„‚cc 10983  โ„cr 10984  0cc0 10985  1c1 10986   + caddc 10988   ยท cmul 10990   < clt 11123   โ‰ค cle 11124   โˆ’ cmin 11319   / cdiv 11746  โ„•cn 12087  2c2 12142  โ„คcz 12433  โ„+crp 12844  ...cfz 13353   โˆฅ cdvds 16071  โ„™cprime 16482
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2709  ax-sep 5255  ax-nul 5262  ax-pow 5319  ax-pr 5383  ax-un 7663  ax-cnex 11041  ax-resscn 11042  ax-1cn 11043  ax-icn 11044  ax-addcl 11045  ax-addrcl 11046  ax-mulcl 11047  ax-mulrcl 11048  ax-mulcom 11049  ax-addass 11050  ax-mulass 11051  ax-distr 11052  ax-i2m1 11053  ax-1ne0 11054  ax-1rid 11055  ax-rnegex 11056  ax-rrecex 11057  ax-cnre 11058  ax-pre-lttri 11059  ax-pre-lttrn 11060  ax-pre-ltadd 11061  ax-pre-mulgt0 11062  ax-pre-sup 11063
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2888  df-ne 2943  df-nel 3049  df-ral 3064  df-rex 3073  df-rmo 3352  df-reu 3353  df-rab 3407  df-v 3446  df-sbc 3739  df-csb 3855  df-dif 3912  df-un 3914  df-in 3916  df-ss 3926  df-pss 3928  df-nul 4282  df-if 4486  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4865  df-iun 4955  df-br 5105  df-opab 5167  df-mpt 5188  df-tr 5222  df-id 5529  df-eprel 5535  df-po 5543  df-so 5544  df-fr 5586  df-we 5588  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6250  df-ord 6317  df-on 6318  df-lim 6319  df-suc 6320  df-iota 6444  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-riota 7306  df-ov 7353  df-oprab 7354  df-mpo 7355  df-om 7794  df-1st 7912  df-2nd 7913  df-frecs 8180  df-wrecs 8211  df-recs 8285  df-rdg 8324  df-1o 8380  df-2o 8381  df-er 8582  df-en 8818  df-dom 8819  df-sdom 8820  df-fin 8821  df-sup 9312  df-pnf 11125  df-mnf 11126  df-xr 11127  df-ltxr 11128  df-le 11129  df-sub 11321  df-neg 11322  df-div 11747  df-nn 12088  df-2 12150  df-3 12151  df-n0 12348  df-z 12434  df-uz 12697  df-rp 12845  df-ioo 13197  df-fz 13354  df-seq 13836  df-exp 13897  df-cj 14918  df-re 14919  df-im 14920  df-sqrt 15054  df-abs 15055  df-dvds 16072  df-prm 16483
This theorem is referenced by:  gausslemma2dlem1  26637
  Copyright terms: Public domain W3C validator