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

Theorem gausslemma2dlem1a 25071
Description: Lemma for gausslemma2dlem1 25072. (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 vex 3198 . . . 4 𝑦 ∈ V
2 gausslemma2d.r . . . . 5 𝑅 = (𝑥 ∈ (1...𝐻) ↦ if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))))
32elrnmpt 5361 . . . 4 (𝑦 ∈ V → (𝑦 ∈ ran 𝑅 ↔ ∃𝑥 ∈ (1...𝐻)𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2)))))
41, 3ax-mp 5 . . 3 (𝑦 ∈ ran 𝑅 ↔ ∃𝑥 ∈ (1...𝐻)𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))))
5 iftrue 4083 . . . . . . . . 9 ((𝑥 · 2) < (𝑃 / 2) → if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) = (𝑥 · 2))
65eqeq2d 2630 . . . . . . . 8 ((𝑥 · 2) < (𝑃 / 2) → (𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) ↔ 𝑦 = (𝑥 · 2)))
76adantr 481 . . . . . . 7 (((𝑥 · 2) < (𝑃 / 2) ∧ (𝜑𝑥 ∈ (1...𝐻))) → (𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) ↔ 𝑦 = (𝑥 · 2)))
8 elfz1b 12394 . . . . . . . . . . . 12 (𝑥 ∈ (1...𝐻) ↔ (𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥𝐻))
9 id 22 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ℕ → 𝑥 ∈ ℕ)
10 2nn 11170 . . . . . . . . . . . . . . . . . 18 2 ∈ ℕ
1110a1i 11 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ℕ → 2 ∈ ℕ)
129, 11nnmulcld 11053 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℕ → (𝑥 · 2) ∈ ℕ)
13123ad2ant1 1080 . . . . . . . . . . . . . . 15 ((𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥𝐻) → (𝑥 · 2) ∈ ℕ)
14133ad2ant1 1080 . . . . . . . . . . . . . 14 (((𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥𝐻) ∧ 𝜑 ∧ (𝑥 · 2) < (𝑃 / 2)) → (𝑥 · 2) ∈ ℕ)
15 gausslemma2d.h . . . . . . . . . . . . . . . . . 18 𝐻 = ((𝑃 − 1) / 2)
1615eleq1i 2690 . . . . . . . . . . . . . . . . 17 (𝐻 ∈ ℕ ↔ ((𝑃 − 1) / 2) ∈ ℕ)
1716biimpi 206 . . . . . . . . . . . . . . . 16 (𝐻 ∈ ℕ → ((𝑃 − 1) / 2) ∈ ℕ)
18173ad2ant2 1081 . . . . . . . . . . . . . . 15 ((𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥𝐻) → ((𝑃 − 1) / 2) ∈ ℕ)
19183ad2ant1 1080 . . . . . . . . . . . . . 14 (((𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥𝐻) ∧ 𝜑 ∧ (𝑥 · 2) < (𝑃 / 2)) → ((𝑃 − 1) / 2) ∈ ℕ)
20 gausslemma2d.p . . . . . . . . . . . . . . . . . 18 (𝜑𝑃 ∈ (ℙ ∖ {2}))
21 nnoddn2prm 15497 . . . . . . . . . . . . . . . . . . . . . 22 (𝑃 ∈ (ℙ ∖ {2}) → (𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃))
22 nnz 11384 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑃 ∈ ℕ → 𝑃 ∈ ℤ)
2322anim1i 591 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) → (𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃))
2421, 23syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝑃 ∈ (ℙ ∖ {2}) → (𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃))
25 nnz 11384 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ ℕ → 𝑥 ∈ ℤ)
26 2z 11394 . . . . . . . . . . . . . . . . . . . . . . . 24 2 ∈ ℤ
2726a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ ℕ → 2 ∈ ℤ)
2825, 27zmulcld 11473 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ ℕ → (𝑥 · 2) ∈ ℤ)
29283ad2ant1 1080 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥𝐻) → (𝑥 · 2) ∈ ℤ)
3024, 29anim12i 589 . . . . . . . . . . . . . . . . . . . 20 ((𝑃 ∈ (ℙ ∖ {2}) ∧ (𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥𝐻)) → ((𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃) ∧ (𝑥 · 2) ∈ ℤ))
31 df-3an 1038 . . . . . . . . . . . . . . . . . . . 20 ((𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ∧ (𝑥 · 2) ∈ ℤ) ↔ ((𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃) ∧ (𝑥 · 2) ∈ ℤ))
3230, 31sylibr 224 . . . . . . . . . . . . . . . . . . 19 ((𝑃 ∈ (ℙ ∖ {2}) ∧ (𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥𝐻)) → (𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ∧ (𝑥 · 2) ∈ ℤ))
3332ex 450 . . . . . . . . . . . . . . . . . 18 (𝑃 ∈ (ℙ ∖ {2}) → ((𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥𝐻) → (𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ∧ (𝑥 · 2) ∈ ℤ)))
3420, 33syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥𝐻) → (𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ∧ (𝑥 · 2) ∈ ℤ)))
3534impcom 446 . . . . . . . . . . . . . . . 16 (((𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥𝐻) ∧ 𝜑) → (𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ∧ (𝑥 · 2) ∈ ℤ))
36 ltoddhalfle 15066 . . . . . . . . . . . . . . . 16 ((𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ∧ (𝑥 · 2) ∈ ℤ) → ((𝑥 · 2) < (𝑃 / 2) ↔ (𝑥 · 2) ≤ ((𝑃 − 1) / 2)))
3735, 36syl 17 . . . . . . . . . . . . . . 15 (((𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥𝐻) ∧ 𝜑) → ((𝑥 · 2) < (𝑃 / 2) ↔ (𝑥 · 2) ≤ ((𝑃 − 1) / 2)))
3837biimp3a 1430 . . . . . . . . . . . . . 14 (((𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥𝐻) ∧ 𝜑 ∧ (𝑥 · 2) < (𝑃 / 2)) → (𝑥 · 2) ≤ ((𝑃 − 1) / 2))
3914, 19, 383jca 1240 . . . . . . . . . . . . 13 (((𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥𝐻) ∧ 𝜑 ∧ (𝑥 · 2) < (𝑃 / 2)) → ((𝑥 · 2) ∈ ℕ ∧ ((𝑃 − 1) / 2) ∈ ℕ ∧ (𝑥 · 2) ≤ ((𝑃 − 1) / 2)))
40393exp 1262 . . . . . . . . . . . 12 ((𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥𝐻) → (𝜑 → ((𝑥 · 2) < (𝑃 / 2) → ((𝑥 · 2) ∈ ℕ ∧ ((𝑃 − 1) / 2) ∈ ℕ ∧ (𝑥 · 2) ≤ ((𝑃 − 1) / 2)))))
418, 40sylbi 207 . . . . . . . . . . 11 (𝑥 ∈ (1...𝐻) → (𝜑 → ((𝑥 · 2) < (𝑃 / 2) → ((𝑥 · 2) ∈ ℕ ∧ ((𝑃 − 1) / 2) ∈ ℕ ∧ (𝑥 · 2) ≤ ((𝑃 − 1) / 2)))))
4241impcom 446 . . . . . . . . . 10 ((𝜑𝑥 ∈ (1...𝐻)) → ((𝑥 · 2) < (𝑃 / 2) → ((𝑥 · 2) ∈ ℕ ∧ ((𝑃 − 1) / 2) ∈ ℕ ∧ (𝑥 · 2) ≤ ((𝑃 − 1) / 2))))
4342impcom 446 . . . . . . . . 9 (((𝑥 · 2) < (𝑃 / 2) ∧ (𝜑𝑥 ∈ (1...𝐻))) → ((𝑥 · 2) ∈ ℕ ∧ ((𝑃 − 1) / 2) ∈ ℕ ∧ (𝑥 · 2) ≤ ((𝑃 − 1) / 2)))
4415oveq2i 6646 . . . . . . . . . . 11 (1...𝐻) = (1...((𝑃 − 1) / 2))
4544eleq2i 2691 . . . . . . . . . 10 ((𝑥 · 2) ∈ (1...𝐻) ↔ (𝑥 · 2) ∈ (1...((𝑃 − 1) / 2)))
46 elfz1b 12394 . . . . . . . . . 10 ((𝑥 · 2) ∈ (1...((𝑃 − 1) / 2)) ↔ ((𝑥 · 2) ∈ ℕ ∧ ((𝑃 − 1) / 2) ∈ ℕ ∧ (𝑥 · 2) ≤ ((𝑃 − 1) / 2)))
4745, 46bitri 264 . . . . . . . . 9 ((𝑥 · 2) ∈ (1...𝐻) ↔ ((𝑥 · 2) ∈ ℕ ∧ ((𝑃 − 1) / 2) ∈ ℕ ∧ (𝑥 · 2) ≤ ((𝑃 − 1) / 2)))
4843, 47sylibr 224 . . . . . . . 8 (((𝑥 · 2) < (𝑃 / 2) ∧ (𝜑𝑥 ∈ (1...𝐻))) → (𝑥 · 2) ∈ (1...𝐻))
49 eleq1 2687 . . . . . . . 8 (𝑦 = (𝑥 · 2) → (𝑦 ∈ (1...𝐻) ↔ (𝑥 · 2) ∈ (1...𝐻)))
5048, 49syl5ibrcom 237 . . . . . . 7 (((𝑥 · 2) < (𝑃 / 2) ∧ (𝜑𝑥 ∈ (1...𝐻))) → (𝑦 = (𝑥 · 2) → 𝑦 ∈ (1...𝐻)))
517, 50sylbid 230 . . . . . 6 (((𝑥 · 2) < (𝑃 / 2) ∧ (𝜑𝑥 ∈ (1...𝐻))) → (𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) → 𝑦 ∈ (1...𝐻)))
52 iffalse 4086 . . . . . . . . 9 (¬ (𝑥 · 2) < (𝑃 / 2) → if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) = (𝑃 − (𝑥 · 2)))
5352eqeq2d 2630 . . . . . . . 8 (¬ (𝑥 · 2) < (𝑃 / 2) → (𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) ↔ 𝑦 = (𝑃 − (𝑥 · 2))))
5453adantr 481 . . . . . . 7 ((¬ (𝑥 · 2) < (𝑃 / 2) ∧ (𝜑𝑥 ∈ (1...𝐻))) → (𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) ↔ 𝑦 = (𝑃 − (𝑥 · 2))))
55 eldifi 3724 . . . . . . . . . . . . 13 (𝑃 ∈ (ℙ ∖ {2}) → 𝑃 ∈ ℙ)
56 prmz 15370 . . . . . . . . . . . . 13 (𝑃 ∈ ℙ → 𝑃 ∈ ℤ)
5720, 55, 563syl 18 . . . . . . . . . . . 12 (𝜑𝑃 ∈ ℤ)
5857ad2antrl 763 . . . . . . . . . . 11 ((¬ (𝑥 · 2) < (𝑃 / 2) ∧ (𝜑𝑥 ∈ (1...𝐻))) → 𝑃 ∈ ℤ)
59 elfzelz 12327 . . . . . . . . . . . . 13 (𝑥 ∈ (1...𝐻) → 𝑥 ∈ ℤ)
6026a1i 11 . . . . . . . . . . . . 13 (𝑥 ∈ (1...𝐻) → 2 ∈ ℤ)
6159, 60zmulcld 11473 . . . . . . . . . . . 12 (𝑥 ∈ (1...𝐻) → (𝑥 · 2) ∈ ℤ)
6261ad2antll 764 . . . . . . . . . . 11 ((¬ (𝑥 · 2) < (𝑃 / 2) ∧ (𝜑𝑥 ∈ (1...𝐻))) → (𝑥 · 2) ∈ ℤ)
6358, 62zsubcld 11472 . . . . . . . . . 10 ((¬ (𝑥 · 2) < (𝑃 / 2) ∧ (𝜑𝑥 ∈ (1...𝐻))) → (𝑃 − (𝑥 · 2)) ∈ ℤ)
6456zred 11467 . . . . . . . . . . . . . 14 (𝑃 ∈ ℙ → 𝑃 ∈ ℝ)
65 nnre 11012 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ ℕ → 𝑥 ∈ ℝ)
6665adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ) → 𝑥 ∈ ℝ)
67 peano2rem 10333 . . . . . . . . . . . . . . . . . . . . . 22 (𝑃 ∈ ℝ → (𝑃 − 1) ∈ ℝ)
6867adantl 482 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ) → (𝑃 − 1) ∈ ℝ)
69 2re 11075 . . . . . . . . . . . . . . . . . . . . . . 23 2 ∈ ℝ
70 2pos 11097 . . . . . . . . . . . . . . . . . . . . . . 23 0 < 2
7169, 70pm3.2i 471 . . . . . . . . . . . . . . . . . . . . . 22 (2 ∈ ℝ ∧ 0 < 2)
7271a1i 11 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ) → (2 ∈ ℝ ∧ 0 < 2))
73 lemuldiv 10888 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 ∈ ℝ ∧ (𝑃 − 1) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((𝑥 · 2) ≤ (𝑃 − 1) ↔ 𝑥 ≤ ((𝑃 − 1) / 2)))
7466, 68, 72, 73syl3anc 1324 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ) → ((𝑥 · 2) ≤ (𝑃 − 1) ↔ 𝑥 ≤ ((𝑃 − 1) / 2)))
7515breq2i 4652 . . . . . . . . . . . . . . . . . . . 20 (𝑥𝐻𝑥 ≤ ((𝑃 − 1) / 2))
7674, 75syl6rbbr 279 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ) → (𝑥𝐻 ↔ (𝑥 · 2) ≤ (𝑃 − 1)))
7712nnred 11020 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ ℕ → (𝑥 · 2) ∈ ℝ)
7877adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ) → (𝑥 · 2) ∈ ℝ)
79 simpr 477 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ) → 𝑃 ∈ ℝ)
8078, 68, 79lesub2d 10620 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ) → ((𝑥 · 2) ≤ (𝑃 − 1) ↔ (𝑃 − (𝑃 − 1)) ≤ (𝑃 − (𝑥 · 2))))
81 recn 10011 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑃 ∈ ℝ → 𝑃 ∈ ℂ)
82 1cnd 10041 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑃 ∈ ℝ → 1 ∈ ℂ)
8381, 82nncand 10382 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑃 ∈ ℝ → (𝑃 − (𝑃 − 1)) = 1)
8483adantl 482 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ) → (𝑃 − (𝑃 − 1)) = 1)
8584breq1d 4654 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ) → ((𝑃 − (𝑃 − 1)) ≤ (𝑃 − (𝑥 · 2)) ↔ 1 ≤ (𝑃 − (𝑥 · 2))))
8685biimpd 219 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ) → ((𝑃 − (𝑃 − 1)) ≤ (𝑃 − (𝑥 · 2)) → 1 ≤ (𝑃 − (𝑥 · 2))))
8780, 86sylbid 230 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ) → ((𝑥 · 2) ≤ (𝑃 − 1) → 1 ≤ (𝑃 − (𝑥 · 2))))
8876, 87sylbid 230 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ) → (𝑥𝐻 → 1 ≤ (𝑃 − (𝑥 · 2))))
8988impancom 456 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ ℕ ∧ 𝑥𝐻) → (𝑃 ∈ ℝ → 1 ≤ (𝑃 − (𝑥 · 2))))
90893adant2 1078 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥𝐻) → (𝑃 ∈ ℝ → 1 ≤ (𝑃 − (𝑥 · 2))))
918, 90sylbi 207 . . . . . . . . . . . . . . 15 (𝑥 ∈ (1...𝐻) → (𝑃 ∈ ℝ → 1 ≤ (𝑃 − (𝑥 · 2))))
9291com12 32 . . . . . . . . . . . . . 14 (𝑃 ∈ ℝ → (𝑥 ∈ (1...𝐻) → 1 ≤ (𝑃 − (𝑥 · 2))))
9364, 92syl 17 . . . . . . . . . . . . 13 (𝑃 ∈ ℙ → (𝑥 ∈ (1...𝐻) → 1 ≤ (𝑃 − (𝑥 · 2))))
9420, 55, 933syl 18 . . . . . . . . . . . 12 (𝜑 → (𝑥 ∈ (1...𝐻) → 1 ≤ (𝑃 − (𝑥 · 2))))
9594imp 445 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (1...𝐻)) → 1 ≤ (𝑃 − (𝑥 · 2)))
9695adantl 482 . . . . . . . . . 10 ((¬ (𝑥 · 2) < (𝑃 / 2) ∧ (𝜑𝑥 ∈ (1...𝐻))) → 1 ≤ (𝑃 − (𝑥 · 2)))
97 elnnz1 11388 . . . . . . . . . 10 ((𝑃 − (𝑥 · 2)) ∈ ℕ ↔ ((𝑃 − (𝑥 · 2)) ∈ ℤ ∧ 1 ≤ (𝑃 − (𝑥 · 2))))
9863, 96, 97sylanbrc 697 . . . . . . . . 9 ((¬ (𝑥 · 2) < (𝑃 / 2) ∧ (𝜑𝑥 ∈ (1...𝐻))) → (𝑃 − (𝑥 · 2)) ∈ ℕ)
998simp2bi 1075 . . . . . . . . . 10 (𝑥 ∈ (1...𝐻) → 𝐻 ∈ ℕ)
10099ad2antll 764 . . . . . . . . 9 ((¬ (𝑥 · 2) < (𝑃 / 2) ∧ (𝜑𝑥 ∈ (1...𝐻))) → 𝐻 ∈ ℕ)
101 nnre 11012 . . . . . . . . . . . . . . . . 17 (𝑃 ∈ ℕ → 𝑃 ∈ ℝ)
102101rehalfcld 11264 . . . . . . . . . . . . . . . 16 (𝑃 ∈ ℕ → (𝑃 / 2) ∈ ℝ)
103102adantr 481 . . . . . . . . . . . . . . 15 ((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) → (𝑃 / 2) ∈ ℝ)
10461zred 11467 . . . . . . . . . . . . . . 15 (𝑥 ∈ (1...𝐻) → (𝑥 · 2) ∈ ℝ)
105 lenlt 10101 . . . . . . . . . . . . . . 15 (((𝑃 / 2) ∈ ℝ ∧ (𝑥 · 2) ∈ ℝ) → ((𝑃 / 2) ≤ (𝑥 · 2) ↔ ¬ (𝑥 · 2) < (𝑃 / 2)))
106103, 104, 105syl2an 494 . . . . . . . . . . . . . 14 (((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → ((𝑃 / 2) ≤ (𝑥 · 2) ↔ ¬ (𝑥 · 2) < (𝑃 / 2)))
10723, 61anim12i 589 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → ((𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃) ∧ (𝑥 · 2) ∈ ℤ))
108107, 31sylibr 224 . . . . . . . . . . . . . . . . . . . . 21 (((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → (𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ∧ (𝑥 · 2) ∈ ℤ))
109 halfleoddlt 15067 . . . . . . . . . . . . . . . . . . . . 21 ((𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ∧ (𝑥 · 2) ∈ ℤ) → ((𝑃 / 2) ≤ (𝑥 · 2) ↔ (𝑃 / 2) < (𝑥 · 2)))
110108, 109syl 17 . . . . . . . . . . . . . . . . . . . 20 (((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → ((𝑃 / 2) ≤ (𝑥 · 2) ↔ (𝑃 / 2) < (𝑥 · 2)))
111110biimpa 501 . . . . . . . . . . . . . . . . . . 19 ((((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) ∧ (𝑃 / 2) ≤ (𝑥 · 2)) → (𝑃 / 2) < (𝑥 · 2))
112 nncn 11013 . . . . . . . . . . . . . . . . . . . . . 22 (𝑃 ∈ ℕ → 𝑃 ∈ ℂ)
113 subhalfhalf 11251 . . . . . . . . . . . . . . . . . . . . . 22 (𝑃 ∈ ℂ → (𝑃 − (𝑃 / 2)) = (𝑃 / 2))
114112, 113syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝑃 ∈ ℕ → (𝑃 − (𝑃 / 2)) = (𝑃 / 2))
115114breq1d 4654 . . . . . . . . . . . . . . . . . . . 20 (𝑃 ∈ ℕ → ((𝑃 − (𝑃 / 2)) < (𝑥 · 2) ↔ (𝑃 / 2) < (𝑥 · 2)))
116115ad3antrrr 765 . . . . . . . . . . . . . . . . . . 19 ((((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) ∧ (𝑃 / 2) ≤ (𝑥 · 2)) → ((𝑃 − (𝑃 / 2)) < (𝑥 · 2) ↔ (𝑃 / 2) < (𝑥 · 2)))
117111, 116mpbird 247 . . . . . . . . . . . . . . . . . 18 ((((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) ∧ (𝑃 / 2) ≤ (𝑥 · 2)) → (𝑃 − (𝑃 / 2)) < (𝑥 · 2))
118101ad2antrr 761 . . . . . . . . . . . . . . . . . . . . 21 (((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → 𝑃 ∈ ℝ)
119102ad2antrr 761 . . . . . . . . . . . . . . . . . . . . 21 (((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → (𝑃 / 2) ∈ ℝ)
120104adantl 482 . . . . . . . . . . . . . . . . . . . . 21 (((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → (𝑥 · 2) ∈ ℝ)
121118, 119, 1203jca 1240 . . . . . . . . . . . . . . . . . . . 20 (((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → (𝑃 ∈ ℝ ∧ (𝑃 / 2) ∈ ℝ ∧ (𝑥 · 2) ∈ ℝ))
122121adantr 481 . . . . . . . . . . . . . . . . . . 19 ((((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) ∧ (𝑃 / 2) ≤ (𝑥 · 2)) → (𝑃 ∈ ℝ ∧ (𝑃 / 2) ∈ ℝ ∧ (𝑥 · 2) ∈ ℝ))
123 ltsub23 10493 . . . . . . . . . . . . . . . . . . 19 ((𝑃 ∈ ℝ ∧ (𝑃 / 2) ∈ ℝ ∧ (𝑥 · 2) ∈ ℝ) → ((𝑃 − (𝑃 / 2)) < (𝑥 · 2) ↔ (𝑃 − (𝑥 · 2)) < (𝑃 / 2)))
124122, 123syl 17 . . . . . . . . . . . . . . . . . 18 ((((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) ∧ (𝑃 / 2) ≤ (𝑥 · 2)) → ((𝑃 − (𝑃 / 2)) < (𝑥 · 2) ↔ (𝑃 − (𝑥 · 2)) < (𝑃 / 2)))
125117, 124mpbid 222 . . . . . . . . . . . . . . . . 17 ((((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) ∧ (𝑃 / 2) ≤ (𝑥 · 2)) → (𝑃 − (𝑥 · 2)) < (𝑃 / 2))
12622ad2antrr 761 . . . . . . . . . . . . . . . . . . . 20 (((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → 𝑃 ∈ ℤ)
127 simplr 791 . . . . . . . . . . . . . . . . . . . 20 (((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → ¬ 2 ∥ 𝑃)
12861adantl 482 . . . . . . . . . . . . . . . . . . . . 21 (((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → (𝑥 · 2) ∈ ℤ)
129126, 128zsubcld 11472 . . . . . . . . . . . . . . . . . . . 20 (((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → (𝑃 − (𝑥 · 2)) ∈ ℤ)
130126, 127, 1293jca 1240 . . . . . . . . . . . . . . . . . . 19 (((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → (𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ∧ (𝑃 − (𝑥 · 2)) ∈ ℤ))
131130adantr 481 . . . . . . . . . . . . . . . . . 18 ((((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) ∧ (𝑃 / 2) ≤ (𝑥 · 2)) → (𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ∧ (𝑃 − (𝑥 · 2)) ∈ ℤ))
132 ltoddhalfle 15066 . . . . . . . . . . . . . . . . . 18 ((𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ∧ (𝑃 − (𝑥 · 2)) ∈ ℤ) → ((𝑃 − (𝑥 · 2)) < (𝑃 / 2) ↔ (𝑃 − (𝑥 · 2)) ≤ ((𝑃 − 1) / 2)))
133131, 132syl 17 . . . . . . . . . . . . . . . . 17 ((((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) ∧ (𝑃 / 2) ≤ (𝑥 · 2)) → ((𝑃 − (𝑥 · 2)) < (𝑃 / 2) ↔ (𝑃 − (𝑥 · 2)) ≤ ((𝑃 − 1) / 2)))
134125, 133mpbid 222 . . . . . . . . . . . . . . . 16 ((((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) ∧ (𝑃 / 2) ≤ (𝑥 · 2)) → (𝑃 − (𝑥 · 2)) ≤ ((𝑃 − 1) / 2))
135134ex 450 . . . . . . . . . . . . . . 15 (((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → ((𝑃 / 2) ≤ (𝑥 · 2) → (𝑃 − (𝑥 · 2)) ≤ ((𝑃 − 1) / 2)))
13615breq2i 4652 . . . . . . . . . . . . . . 15 ((𝑃 − (𝑥 · 2)) ≤ 𝐻 ↔ (𝑃 − (𝑥 · 2)) ≤ ((𝑃 − 1) / 2))
137135, 136syl6ibr 242 . . . . . . . . . . . . . 14 (((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → ((𝑃 / 2) ≤ (𝑥 · 2) → (𝑃 − (𝑥 · 2)) ≤ 𝐻))
138106, 137sylbird 250 . . . . . . . . . . . . 13 (((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → (¬ (𝑥 · 2) < (𝑃 / 2) → (𝑃 − (𝑥 · 2)) ≤ 𝐻))
139138ex 450 . . . . . . . . . . . 12 ((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) → (𝑥 ∈ (1...𝐻) → (¬ (𝑥 · 2) < (𝑃 / 2) → (𝑃 − (𝑥 · 2)) ≤ 𝐻)))
14020, 21, 1393syl 18 . . . . . . . . . . 11 (𝜑 → (𝑥 ∈ (1...𝐻) → (¬ (𝑥 · 2) < (𝑃 / 2) → (𝑃 − (𝑥 · 2)) ≤ 𝐻)))
141140imp 445 . . . . . . . . . 10 ((𝜑𝑥 ∈ (1...𝐻)) → (¬ (𝑥 · 2) < (𝑃 / 2) → (𝑃 − (𝑥 · 2)) ≤ 𝐻))
142141impcom 446 . . . . . . . . 9 ((¬ (𝑥 · 2) < (𝑃 / 2) ∧ (𝜑𝑥 ∈ (1...𝐻))) → (𝑃 − (𝑥 · 2)) ≤ 𝐻)
143 elfz1b 12394 . . . . . . . . 9 ((𝑃 − (𝑥 · 2)) ∈ (1...𝐻) ↔ ((𝑃 − (𝑥 · 2)) ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ (𝑃 − (𝑥 · 2)) ≤ 𝐻))
14498, 100, 142, 143syl3anbrc 1244 . . . . . . . 8 ((¬ (𝑥 · 2) < (𝑃 / 2) ∧ (𝜑𝑥 ∈ (1...𝐻))) → (𝑃 − (𝑥 · 2)) ∈ (1...𝐻))
145 eleq1 2687 . . . . . . . 8 (𝑦 = (𝑃 − (𝑥 · 2)) → (𝑦 ∈ (1...𝐻) ↔ (𝑃 − (𝑥 · 2)) ∈ (1...𝐻)))
146144, 145syl5ibrcom 237 . . . . . . 7 ((¬ (𝑥 · 2) < (𝑃 / 2) ∧ (𝜑𝑥 ∈ (1...𝐻))) → (𝑦 = (𝑃 − (𝑥 · 2)) → 𝑦 ∈ (1...𝐻)))
14754, 146sylbid 230 . . . . . 6 ((¬ (𝑥 · 2) < (𝑃 / 2) ∧ (𝜑𝑥 ∈ (1...𝐻))) → (𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) → 𝑦 ∈ (1...𝐻)))
14851, 147pm2.61ian 830 . . . . 5 ((𝜑𝑥 ∈ (1...𝐻)) → (𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) → 𝑦 ∈ (1...𝐻)))
149148rexlimdva 3027 . . . 4 (𝜑 → (∃𝑥 ∈ (1...𝐻)𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) → 𝑦 ∈ (1...𝐻)))
150 elfz1b 12394 . . . . . . . . . 10 (𝑦 ∈ (1...𝐻) ↔ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦𝐻))
151 simp1 1059 . . . . . . . . . . . . 13 ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦𝐻) → 𝑦 ∈ ℕ)
152 simpl 473 . . . . . . . . . . . . 13 ((2 ∥ 𝑦𝜑) → 2 ∥ 𝑦)
153 nnehalf 15077 . . . . . . . . . . . . 13 ((𝑦 ∈ ℕ ∧ 2 ∥ 𝑦) → (𝑦 / 2) ∈ ℕ)
154151, 152, 153syl2anr 495 . . . . . . . . . . . 12 (((2 ∥ 𝑦𝜑) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦𝐻)) → (𝑦 / 2) ∈ ℕ)
155 simpr2 1066 . . . . . . . . . . . 12 (((2 ∥ 𝑦𝜑) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦𝐻)) → 𝐻 ∈ ℕ)
156 nnre 11012 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ ℕ → 𝑦 ∈ ℝ)
157156ad2antrr 761 . . . . . . . . . . . . . . . . 17 (((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) ∧ (2 ∥ 𝑦𝜑)) → 𝑦 ∈ ℝ)
158 nnrp 11827 . . . . . . . . . . . . . . . . . . 19 (𝐻 ∈ ℕ → 𝐻 ∈ ℝ+)
159158adantl 482 . . . . . . . . . . . . . . . . . 18 ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) → 𝐻 ∈ ℝ+)
160159adantr 481 . . . . . . . . . . . . . . . . 17 (((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) ∧ (2 ∥ 𝑦𝜑)) → 𝐻 ∈ ℝ+)
161 2rp 11822 . . . . . . . . . . . . . . . . . . 19 2 ∈ ℝ+
162 1le2 11226 . . . . . . . . . . . . . . . . . . 19 1 ≤ 2
163161, 162pm3.2i 471 . . . . . . . . . . . . . . . . . 18 (2 ∈ ℝ+ ∧ 1 ≤ 2)
164163a1i 11 . . . . . . . . . . . . . . . . 17 (((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) ∧ (2 ∥ 𝑦𝜑)) → (2 ∈ ℝ+ ∧ 1 ≤ 2))
165 ledivge1le 11886 . . . . . . . . . . . . . . . . 17 ((𝑦 ∈ ℝ ∧ 𝐻 ∈ ℝ+ ∧ (2 ∈ ℝ+ ∧ 1 ≤ 2)) → (𝑦𝐻 → (𝑦 / 2) ≤ 𝐻))
166157, 160, 164, 165syl3anc 1324 . . . . . . . . . . . . . . . 16 (((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) ∧ (2 ∥ 𝑦𝜑)) → (𝑦𝐻 → (𝑦 / 2) ≤ 𝐻))
167166ex 450 . . . . . . . . . . . . . . 15 ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) → ((2 ∥ 𝑦𝜑) → (𝑦𝐻 → (𝑦 / 2) ≤ 𝐻)))
168167com23 86 . . . . . . . . . . . . . 14 ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) → (𝑦𝐻 → ((2 ∥ 𝑦𝜑) → (𝑦 / 2) ≤ 𝐻)))
1691683impia 1259 . . . . . . . . . . . . 13 ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦𝐻) → ((2 ∥ 𝑦𝜑) → (𝑦 / 2) ≤ 𝐻))
170169impcom 446 . . . . . . . . . . . 12 (((2 ∥ 𝑦𝜑) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦𝐻)) → (𝑦 / 2) ≤ 𝐻)
171154, 155, 1703jca 1240 . . . . . . . . . . 11 (((2 ∥ 𝑦𝜑) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦𝐻)) → ((𝑦 / 2) ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ (𝑦 / 2) ≤ 𝐻))
172171ex 450 . . . . . . . . . 10 ((2 ∥ 𝑦𝜑) → ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦𝐻) → ((𝑦 / 2) ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ (𝑦 / 2) ≤ 𝐻)))
173150, 172syl5bi 232 . . . . . . . . 9 ((2 ∥ 𝑦𝜑) → (𝑦 ∈ (1...𝐻) → ((𝑦 / 2) ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ (𝑦 / 2) ≤ 𝐻)))
1741733impia 1259 . . . . . . . 8 ((2 ∥ 𝑦𝜑𝑦 ∈ (1...𝐻)) → ((𝑦 / 2) ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ (𝑦 / 2) ≤ 𝐻))
175 elfz1b 12394 . . . . . . . 8 ((𝑦 / 2) ∈ (1...𝐻) ↔ ((𝑦 / 2) ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ (𝑦 / 2) ≤ 𝐻))
176174, 175sylibr 224 . . . . . . 7 ((2 ∥ 𝑦𝜑𝑦 ∈ (1...𝐻)) → (𝑦 / 2) ∈ (1...𝐻))
177 oveq1 6642 . . . . . . . . . . 11 (𝑥 = (𝑦 / 2) → (𝑥 · 2) = ((𝑦 / 2) · 2))
178177breq1d 4654 . . . . . . . . . 10 (𝑥 = (𝑦 / 2) → ((𝑥 · 2) < (𝑃 / 2) ↔ ((𝑦 / 2) · 2) < (𝑃 / 2)))
179177oveq2d 6651 . . . . . . . . . 10 (𝑥 = (𝑦 / 2) → (𝑃 − (𝑥 · 2)) = (𝑃 − ((𝑦 / 2) · 2)))
180178, 177, 179ifbieq12d 4104 . . . . . . . . 9 (𝑥 = (𝑦 / 2) → if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) = if(((𝑦 / 2) · 2) < (𝑃 / 2), ((𝑦 / 2) · 2), (𝑃 − ((𝑦 / 2) · 2))))
181180eqeq2d 2630 . . . . . . . 8 (𝑥 = (𝑦 / 2) → (𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) ↔ 𝑦 = if(((𝑦 / 2) · 2) < (𝑃 / 2), ((𝑦 / 2) · 2), (𝑃 − ((𝑦 / 2) · 2)))))
182181adantl 482 . . . . . . 7 (((2 ∥ 𝑦𝜑𝑦 ∈ (1...𝐻)) ∧ 𝑥 = (𝑦 / 2)) → (𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) ↔ 𝑦 = if(((𝑦 / 2) · 2) < (𝑃 / 2), ((𝑦 / 2) · 2), (𝑃 − ((𝑦 / 2) · 2)))))
183 elfzelz 12327 . . . . . . . . . . . . 13 (𝑦 ∈ (1...𝐻) → 𝑦 ∈ ℤ)
184183zcnd 11468 . . . . . . . . . . . 12 (𝑦 ∈ (1...𝐻) → 𝑦 ∈ ℂ)
1851843ad2ant3 1082 . . . . . . . . . . 11 ((2 ∥ 𝑦𝜑𝑦 ∈ (1...𝐻)) → 𝑦 ∈ ℂ)
186 2cnd 11078 . . . . . . . . . . 11 ((2 ∥ 𝑦𝜑𝑦 ∈ (1...𝐻)) → 2 ∈ ℂ)
187 2ne0 11098 . . . . . . . . . . . 12 2 ≠ 0
188187a1i 11 . . . . . . . . . . 11 ((2 ∥ 𝑦𝜑𝑦 ∈ (1...𝐻)) → 2 ≠ 0)
189185, 186, 188divcan1d 10787 . . . . . . . . . 10 ((2 ∥ 𝑦𝜑𝑦 ∈ (1...𝐻)) → ((𝑦 / 2) · 2) = 𝑦)
19015breq2i 4652 . . . . . . . . . . . . . . . 16 (𝑦𝐻𝑦 ≤ ((𝑃 − 1) / 2))
191 nnz 11384 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ ℕ → 𝑦 ∈ ℤ)
19220, 21, 233syl 18 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃))
193192adantl 482 . . . . . . . . . . . . . . . . . . . . 21 ((2 ∥ 𝑦𝜑) → (𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃))
194191, 193anim12ci 590 . . . . . . . . . . . . . . . . . . . 20 ((𝑦 ∈ ℕ ∧ (2 ∥ 𝑦𝜑)) → ((𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃) ∧ 𝑦 ∈ ℤ))
195 df-3an 1038 . . . . . . . . . . . . . . . . . . . 20 ((𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃𝑦 ∈ ℤ) ↔ ((𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃) ∧ 𝑦 ∈ ℤ))
196194, 195sylibr 224 . . . . . . . . . . . . . . . . . . 19 ((𝑦 ∈ ℕ ∧ (2 ∥ 𝑦𝜑)) → (𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃𝑦 ∈ ℤ))
197 ltoddhalfle 15066 . . . . . . . . . . . . . . . . . . 19 ((𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃𝑦 ∈ ℤ) → (𝑦 < (𝑃 / 2) ↔ 𝑦 ≤ ((𝑃 − 1) / 2)))
198196, 197syl 17 . . . . . . . . . . . . . . . . . 18 ((𝑦 ∈ ℕ ∧ (2 ∥ 𝑦𝜑)) → (𝑦 < (𝑃 / 2) ↔ 𝑦 ≤ ((𝑃 − 1) / 2)))
199198exbiri 651 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ℕ → ((2 ∥ 𝑦𝜑) → (𝑦 ≤ ((𝑃 − 1) / 2) → 𝑦 < (𝑃 / 2))))
200199com23 86 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℕ → (𝑦 ≤ ((𝑃 − 1) / 2) → ((2 ∥ 𝑦𝜑) → 𝑦 < (𝑃 / 2))))
201190, 200syl5bi 232 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → (𝑦𝐻 → ((2 ∥ 𝑦𝜑) → 𝑦 < (𝑃 / 2))))
202201a1d 25 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → (𝐻 ∈ ℕ → (𝑦𝐻 → ((2 ∥ 𝑦𝜑) → 𝑦 < (𝑃 / 2)))))
2032023imp 1254 . . . . . . . . . . . . 13 ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦𝐻) → ((2 ∥ 𝑦𝜑) → 𝑦 < (𝑃 / 2)))
204150, 203sylbi 207 . . . . . . . . . . . 12 (𝑦 ∈ (1...𝐻) → ((2 ∥ 𝑦𝜑) → 𝑦 < (𝑃 / 2)))
205204com12 32 . . . . . . . . . . 11 ((2 ∥ 𝑦𝜑) → (𝑦 ∈ (1...𝐻) → 𝑦 < (𝑃 / 2)))
2062053impia 1259 . . . . . . . . . 10 ((2 ∥ 𝑦𝜑𝑦 ∈ (1...𝐻)) → 𝑦 < (𝑃 / 2))
207189, 206eqbrtrd 4666 . . . . . . . . 9 ((2 ∥ 𝑦𝜑𝑦 ∈ (1...𝐻)) → ((𝑦 / 2) · 2) < (𝑃 / 2))
208207iftrued 4085 . . . . . . . 8 ((2 ∥ 𝑦𝜑𝑦 ∈ (1...𝐻)) → if(((𝑦 / 2) · 2) < (𝑃 / 2), ((𝑦 / 2) · 2), (𝑃 − ((𝑦 / 2) · 2))) = ((𝑦 / 2) · 2))
209208, 189eqtr2d 2655 . . . . . . 7 ((2 ∥ 𝑦𝜑𝑦 ∈ (1...𝐻)) → 𝑦 = if(((𝑦 / 2) · 2) < (𝑃 / 2), ((𝑦 / 2) · 2), (𝑃 − ((𝑦 / 2) · 2))))
210176, 182, 209rspcedvd 3312 . . . . . 6 ((2 ∥ 𝑦𝜑𝑦 ∈ (1...𝐻)) → ∃𝑥 ∈ (1...𝐻)𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))))
2112103exp 1262 . . . . 5 (2 ∥ 𝑦 → (𝜑 → (𝑦 ∈ (1...𝐻) → ∃𝑥 ∈ (1...𝐻)𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))))))
21255, 56syl 17 . . . . . . . . . . . . . . . . 17 (𝑃 ∈ (ℙ ∖ {2}) → 𝑃 ∈ ℤ)
213212ad2antrr 761 . . . . . . . . . . . . . . . 16 (((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦𝐻)) → 𝑃 ∈ ℤ)
2141913ad2ant1 1080 . . . . . . . . . . . . . . . . 17 ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦𝐻) → 𝑦 ∈ ℤ)
215214adantl 482 . . . . . . . . . . . . . . . 16 (((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦𝐻)) → 𝑦 ∈ ℤ)
216213, 215zsubcld 11472 . . . . . . . . . . . . . . 15 (((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦𝐻)) → (𝑃𝑦) ∈ ℤ)
217156ad2antrl 763 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑃 ∈ ℝ ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ)) → 𝑦 ∈ ℝ)
21867rehalfcld 11264 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑃 ∈ ℝ → ((𝑃 − 1) / 2) ∈ ℝ)
219218adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑃 ∈ ℝ ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ)) → ((𝑃 − 1) / 2) ∈ ℝ)
220 simpl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑃 ∈ ℝ ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ)) → 𝑃 ∈ ℝ)
221217, 219, 2203jca 1240 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑃 ∈ ℝ ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ)) → (𝑦 ∈ ℝ ∧ ((𝑃 − 1) / 2) ∈ ℝ ∧ 𝑃 ∈ ℝ))
222221ex 450 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑃 ∈ ℝ → ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) → (𝑦 ∈ ℝ ∧ ((𝑃 − 1) / 2) ∈ ℝ ∧ 𝑃 ∈ ℝ)))
22355, 64, 2223syl 18 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑃 ∈ (ℙ ∖ {2}) → ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) → (𝑦 ∈ ℝ ∧ ((𝑃 − 1) / 2) ∈ ℝ ∧ 𝑃 ∈ ℝ)))
224223adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) → ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) → (𝑦 ∈ ℝ ∧ ((𝑃 − 1) / 2) ∈ ℝ ∧ 𝑃 ∈ ℝ)))
225224impcom 446 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) ∧ (𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦)) → (𝑦 ∈ ℝ ∧ ((𝑃 − 1) / 2) ∈ ℝ ∧ 𝑃 ∈ ℝ))
226 lesub2 10508 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑦 ∈ ℝ ∧ ((𝑃 − 1) / 2) ∈ ℝ ∧ 𝑃 ∈ ℝ) → (𝑦 ≤ ((𝑃 − 1) / 2) ↔ (𝑃 − ((𝑃 − 1) / 2)) ≤ (𝑃𝑦)))
227225, 226syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) ∧ (𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦)) → (𝑦 ≤ ((𝑃 − 1) / 2) ↔ (𝑃 − ((𝑃 − 1) / 2)) ≤ (𝑃𝑦)))
22856zcnd 11468 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑃 ∈ ℙ → 𝑃 ∈ ℂ)
229 1cnd 10041 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑃 ∈ ℂ → 1 ∈ ℂ)
230 2cnne0 11227 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (2 ∈ ℂ ∧ 2 ≠ 0)
231230a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑃 ∈ ℂ → (2 ∈ ℂ ∧ 2 ≠ 0))
232 divsubdir 10706 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑃 ∈ ℂ ∧ 1 ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → ((𝑃 − 1) / 2) = ((𝑃 / 2) − (1 / 2)))
233229, 231, 232mpd3an23 1424 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑃 ∈ ℂ → ((𝑃 − 1) / 2) = ((𝑃 / 2) − (1 / 2)))
234233oveq2d 6651 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑃 ∈ ℂ → (𝑃 − ((𝑃 − 1) / 2)) = (𝑃 − ((𝑃 / 2) − (1 / 2))))
235 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑃 ∈ ℂ → 𝑃 ∈ ℂ)
236 halfcl 11242 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑃 ∈ ℂ → (𝑃 / 2) ∈ ℂ)
237 halfcn 11232 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (1 / 2) ∈ ℂ
238237a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑃 ∈ ℂ → (1 / 2) ∈ ℂ)
239235, 236, 238subsubd 10405 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑃 ∈ ℂ → (𝑃 − ((𝑃 / 2) − (1 / 2))) = ((𝑃 − (𝑃 / 2)) + (1 / 2)))
240113oveq1d 6650 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑃 ∈ ℂ → ((𝑃 − (𝑃 / 2)) + (1 / 2)) = ((𝑃 / 2) + (1 / 2)))
241234, 239, 2403eqtrd 2658 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑃 ∈ ℂ → (𝑃 − ((𝑃 − 1) / 2)) = ((𝑃 / 2) + (1 / 2)))
24255, 228, 2413syl 18 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑃 ∈ (ℙ ∖ {2}) → (𝑃 − ((𝑃 − 1) / 2)) = ((𝑃 / 2) + (1 / 2)))
243242ad2antrl 763 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) ∧ (𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦)) → (𝑃 − ((𝑃 − 1) / 2)) = ((𝑃 / 2) + (1 / 2)))
244243breq1d 4654 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) ∧ (𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦)) → ((𝑃 − ((𝑃 − 1) / 2)) ≤ (𝑃𝑦) ↔ ((𝑃 / 2) + (1 / 2)) ≤ (𝑃𝑦)))
245 prmnn 15369 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
246 halfre 11231 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (1 / 2) ∈ ℝ
247246a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑃 ∈ ℕ → (1 / 2) ∈ ℝ)
248 nngt0 11034 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑃 ∈ ℕ → 0 < 𝑃)
24971a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑃 ∈ ℕ → (2 ∈ ℝ ∧ 0 < 2))
250 divgt0 10876 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑃 ∈ ℝ ∧ 0 < 𝑃) ∧ (2 ∈ ℝ ∧ 0 < 2)) → 0 < (𝑃 / 2))
251101, 248, 249, 250syl21anc 1323 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑃 ∈ ℕ → 0 < (𝑃 / 2))
252 halfgt0 11233 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 0 < (1 / 2)
253252a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑃 ∈ ℕ → 0 < (1 / 2))
254102, 247, 251, 253addgt0d 10587 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑃 ∈ ℕ → 0 < ((𝑃 / 2) + (1 / 2)))
25555, 245, 2543syl 18 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑃 ∈ (ℙ ∖ {2}) → 0 < ((𝑃 / 2) + (1 / 2)))
256255ad2antrl 763 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) ∧ (𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦)) → 0 < ((𝑃 / 2) + (1 / 2)))
257 0red 10026 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → 0 ∈ ℝ)
258 simpr 477 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → 𝑃 ∈ ℝ)
259258rehalfcld 11264 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → (𝑃 / 2) ∈ ℝ)
260246a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → (1 / 2) ∈ ℝ)
261259, 260readdcld 10054 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → ((𝑃 / 2) + (1 / 2)) ∈ ℝ)
262 resubcl 10330 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑃 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑃𝑦) ∈ ℝ)
263262ancoms 469 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → (𝑃𝑦) ∈ ℝ)
264257, 261, 2633jca 1240 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → (0 ∈ ℝ ∧ ((𝑃 / 2) + (1 / 2)) ∈ ℝ ∧ (𝑃𝑦) ∈ ℝ))
265264ex 450 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑦 ∈ ℝ → (𝑃 ∈ ℝ → (0 ∈ ℝ ∧ ((𝑃 / 2) + (1 / 2)) ∈ ℝ ∧ (𝑃𝑦) ∈ ℝ)))
266156, 265syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑦 ∈ ℕ → (𝑃 ∈ ℝ → (0 ∈ ℝ ∧ ((𝑃 / 2) + (1 / 2)) ∈ ℝ ∧ (𝑃𝑦) ∈ ℝ)))
267266adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) → (𝑃 ∈ ℝ → (0 ∈ ℝ ∧ ((𝑃 / 2) + (1 / 2)) ∈ ℝ ∧ (𝑃𝑦) ∈ ℝ)))
268267com12 32 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑃 ∈ ℝ → ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) → (0 ∈ ℝ ∧ ((𝑃 / 2) + (1 / 2)) ∈ ℝ ∧ (𝑃𝑦) ∈ ℝ)))
26955, 64, 2683syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑃 ∈ (ℙ ∖ {2}) → ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) → (0 ∈ ℝ ∧ ((𝑃 / 2) + (1 / 2)) ∈ ℝ ∧ (𝑃𝑦) ∈ ℝ)))
270269adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) → ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) → (0 ∈ ℝ ∧ ((𝑃 / 2) + (1 / 2)) ∈ ℝ ∧ (𝑃𝑦) ∈ ℝ)))
271270impcom 446 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) ∧ (𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦)) → (0 ∈ ℝ ∧ ((𝑃 / 2) + (1 / 2)) ∈ ℝ ∧ (𝑃𝑦) ∈ ℝ))
272 ltletr 10114 . . . . . . . . . . . . . . . . . . . . . . . 24 ((0 ∈ ℝ ∧ ((𝑃 / 2) + (1 / 2)) ∈ ℝ ∧ (𝑃𝑦) ∈ ℝ) → ((0 < ((𝑃 / 2) + (1 / 2)) ∧ ((𝑃 / 2) + (1 / 2)) ≤ (𝑃𝑦)) → 0 < (𝑃𝑦)))
273271, 272syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) ∧ (𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦)) → ((0 < ((𝑃 / 2) + (1 / 2)) ∧ ((𝑃 / 2) + (1 / 2)) ≤ (𝑃𝑦)) → 0 < (𝑃𝑦)))
274256, 273mpand 710 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) ∧ (𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦)) → (((𝑃 / 2) + (1 / 2)) ≤ (𝑃𝑦) → 0 < (𝑃𝑦)))
275244, 274sylbid 230 . . . . . . . . . . . . . . . . . . . . 21 (((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) ∧ (𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦)) → ((𝑃 − ((𝑃 − 1) / 2)) ≤ (𝑃𝑦) → 0 < (𝑃𝑦)))
276227, 275sylbid 230 . . . . . . . . . . . . . . . . . . . 20 (((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) ∧ (𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦)) → (𝑦 ≤ ((𝑃 − 1) / 2) → 0 < (𝑃𝑦)))
277276ex 450 . . . . . . . . . . . . . . . . . . 19 ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) → ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) → (𝑦 ≤ ((𝑃 − 1) / 2) → 0 < (𝑃𝑦))))
278277com23 86 . . . . . . . . . . . . . . . . . 18 ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) → (𝑦 ≤ ((𝑃 − 1) / 2) → ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) → 0 < (𝑃𝑦))))
279190, 278syl5bi 232 . . . . . . . . . . . . . . . . 17 ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) → (𝑦𝐻 → ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) → 0 < (𝑃𝑦))))
2802793impia 1259 . . . . . . . . . . . . . . . 16 ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦𝐻) → ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) → 0 < (𝑃𝑦)))
281280impcom 446 . . . . . . . . . . . . . . 15 (((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦𝐻)) → 0 < (𝑃𝑦))
282 elnnz 11372 . . . . . . . . . . . . . . 15 ((𝑃𝑦) ∈ ℕ ↔ ((𝑃𝑦) ∈ ℤ ∧ 0 < (𝑃𝑦)))
283216, 281, 282sylanbrc 697 . . . . . . . . . . . . . 14 (((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦𝐻)) → (𝑃𝑦) ∈ ℕ)
28424adantr 481 . . . . . . . . . . . . . . 15 ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) → (𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃))
285 simpr 477 . . . . . . . . . . . . . . . 16 ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) → ¬ 2 ∥ 𝑦)
286285, 214anim12ci 590 . . . . . . . . . . . . . . 15 (((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦𝐻)) → (𝑦 ∈ ℤ ∧ ¬ 2 ∥ 𝑦))
287 omoe 15069 . . . . . . . . . . . . . . 15 (((𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃) ∧ (𝑦 ∈ ℤ ∧ ¬ 2 ∥ 𝑦)) → 2 ∥ (𝑃𝑦))
288284, 286, 287syl2an2r 875 . . . . . . . . . . . . . 14 (((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦𝐻)) → 2 ∥ (𝑃𝑦))
289 nnehalf 15077 . . . . . . . . . . . . . 14 (((𝑃𝑦) ∈ ℕ ∧ 2 ∥ (𝑃𝑦)) → ((𝑃𝑦) / 2) ∈ ℕ)
290283, 288, 289syl2anc 692 . . . . . . . . . . . . 13 (((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦𝐻)) → ((𝑃𝑦) / 2) ∈ ℕ)
291 simpr2 1066 . . . . . . . . . . . . 13 (((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦𝐻)) → 𝐻 ∈ ℕ)
292 1red 10040 . . . . . . . . . . . . . . . 16 (((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦𝐻)) → 1 ∈ ℝ)
2931563ad2ant1 1080 . . . . . . . . . . . . . . . . 17 ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦𝐻) → 𝑦 ∈ ℝ)
294293adantl 482 . . . . . . . . . . . . . . . 16 (((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦𝐻)) → 𝑦 ∈ ℝ)
29555, 64syl 17 . . . . . . . . . . . . . . . . 17 (𝑃 ∈ (ℙ ∖ {2}) → 𝑃 ∈ ℝ)
296295ad2antrr 761 . . . . . . . . . . . . . . . 16 (((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦𝐻)) → 𝑃 ∈ ℝ)
297 nnge1 11031 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ ℕ → 1 ≤ 𝑦)
2982973ad2ant1 1080 . . . . . . . . . . . . . . . . 17 ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦𝐻) → 1 ≤ 𝑦)
299298adantl 482 . . . . . . . . . . . . . . . 16 (((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦𝐻)) → 1 ≤ 𝑦)
300292, 294, 296, 299lesub2dd 10629 . . . . . . . . . . . . . . 15 (((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦𝐻)) → (𝑃𝑦) ≤ (𝑃 − 1))
301296, 294resubcld 10443 . . . . . . . . . . . . . . . 16 (((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦𝐻)) → (𝑃𝑦) ∈ ℝ)
30255, 64, 673syl 18 . . . . . . . . . . . . . . . . 17 (𝑃 ∈ (ℙ ∖ {2}) → (𝑃 − 1) ∈ ℝ)
303302ad2antrr 761 . . . . . . . . . . . . . . . 16 (((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦𝐻)) → (𝑃 − 1) ∈ ℝ)
30471a1i 11 . . . . . . . . . . . . . . . 16 (((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦𝐻)) → (2 ∈ ℝ ∧ 0 < 2))
305 lediv1 10873 . . . . . . . . . . . . . . . 16 (((𝑃𝑦) ∈ ℝ ∧ (𝑃 − 1) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((𝑃𝑦) ≤ (𝑃 − 1) ↔ ((𝑃𝑦) / 2) ≤ ((𝑃 − 1) / 2)))
306301, 303, 304, 305syl3anc 1324 . . . . . . . . . . . . . . 15 (((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦𝐻)) → ((𝑃𝑦) ≤ (𝑃 − 1) ↔ ((𝑃𝑦) / 2) ≤ ((𝑃 − 1) / 2)))
307300, 306mpbid 222 . . . . . . . . . . . . . 14 (((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦𝐻)) → ((𝑃𝑦) / 2) ≤ ((𝑃 − 1) / 2))
30815breq2i 4652 . . . . . . . . . . . . . 14 (((𝑃𝑦) / 2) ≤ 𝐻 ↔ ((𝑃𝑦) / 2) ≤ ((𝑃 − 1) / 2))
309307, 308sylibr 224 . . . . . . . . . . . . 13 (((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦𝐻)) → ((𝑃𝑦) / 2) ≤ 𝐻)
310290, 291, 3093jca 1240 . . . . . . . . . . . 12 (((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦𝐻)) → (((𝑃𝑦) / 2) ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ ((𝑃𝑦) / 2) ≤ 𝐻))
311310ex 450 . . . . . . . . . . 11 ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) → ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦𝐻) → (((𝑃𝑦) / 2) ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ ((𝑃𝑦) / 2) ≤ 𝐻)))
312 elfz1b 12394 . . . . . . . . . . 11 (((𝑃𝑦) / 2) ∈ (1...𝐻) ↔ (((𝑃𝑦) / 2) ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ ((𝑃𝑦) / 2) ≤ 𝐻))
313311, 150, 3123imtr4g 285 . . . . . . . . . 10 ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) → (𝑦 ∈ (1...𝐻) → ((𝑃𝑦) / 2) ∈ (1...𝐻)))
314313ex 450 . . . . . . . . 9 (𝑃 ∈ (ℙ ∖ {2}) → (¬ 2 ∥ 𝑦 → (𝑦 ∈ (1...𝐻) → ((𝑃𝑦) / 2) ∈ (1...𝐻))))
31520, 314syl 17 . . . . . . . 8 (𝜑 → (¬ 2 ∥ 𝑦 → (𝑦 ∈ (1...𝐻) → ((𝑃𝑦) / 2) ∈ (1...𝐻))))
3163153imp21 1275 . . . . . . 7 ((¬ 2 ∥ 𝑦𝜑𝑦 ∈ (1...𝐻)) → ((𝑃𝑦) / 2) ∈ (1...𝐻))
317 oveq1 6642 . . . . . . . . . . 11 (𝑥 = ((𝑃𝑦) / 2) → (𝑥 · 2) = (((𝑃𝑦) / 2) · 2))
318317breq1d 4654 . . . . . . . . . 10 (𝑥 = ((𝑃𝑦) / 2) → ((𝑥 · 2) < (𝑃 / 2) ↔ (((𝑃𝑦) / 2) · 2) < (𝑃 / 2)))
319317oveq2d 6651 . . . . . . . . . 10 (𝑥 = ((𝑃𝑦) / 2) → (𝑃 − (𝑥 · 2)) = (𝑃 − (((𝑃𝑦) / 2) · 2)))
320318, 317, 319ifbieq12d 4104 . . . . . . . . 9 (𝑥 = ((𝑃𝑦) / 2) → if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) = if((((𝑃𝑦) / 2) · 2) < (𝑃 / 2), (((𝑃𝑦) / 2) · 2), (𝑃 − (((𝑃𝑦) / 2) · 2))))
321320eqeq2d 2630 . . . . . . . 8 (𝑥 = ((𝑃𝑦) / 2) → (𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) ↔ 𝑦 = if((((𝑃𝑦) / 2) · 2) < (𝑃 / 2), (((𝑃𝑦) / 2) · 2), (𝑃 − (((𝑃𝑦) / 2) · 2)))))
322321adantl 482 . . . . . . 7 (((¬ 2 ∥ 𝑦𝜑𝑦 ∈ (1...𝐻)) ∧ 𝑥 = ((𝑃𝑦) / 2)) → (𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) ↔ 𝑦 = if((((𝑃𝑦) / 2) · 2) < (𝑃 / 2), (((𝑃𝑦) / 2) · 2), (𝑃 − (((𝑃𝑦) / 2) · 2)))))
32320, 55, 2283syl 18 . . . . . . . . . . . . 13 (𝜑𝑃 ∈ ℂ)
3243233ad2ant2 1081 . . . . . . . . . . . 12 ((¬ 2 ∥ 𝑦𝜑𝑦 ∈ (1...𝐻)) → 𝑃 ∈ ℂ)
3251843ad2ant3 1082 . . . . . . . . . . . 12 ((¬ 2 ∥ 𝑦𝜑𝑦 ∈ (1...𝐻)) → 𝑦 ∈ ℂ)
326324, 325subcld 10377 . . . . . . . . . . 11 ((¬ 2 ∥ 𝑦𝜑𝑦 ∈ (1...𝐻)) → (𝑃𝑦) ∈ ℂ)
327 2cnd 11078 . . . . . . . . . . 11 ((¬ 2 ∥ 𝑦𝜑𝑦 ∈ (1...𝐻)) → 2 ∈ ℂ)
328187a1i 11 . . . . . . . . . . 11 ((¬ 2 ∥ 𝑦𝜑𝑦 ∈ (1...𝐻)) → 2 ≠ 0)
329326, 327, 328divcan1d 10787 . . . . . . . . . 10 ((¬ 2 ∥ 𝑦𝜑𝑦 ∈ (1...𝐻)) → (((𝑃𝑦) / 2) · 2) = (𝑃𝑦))
330 zre 11366 . . . . . . . . . . . . . . . . . . . . 21 (𝑃 ∈ ℤ → 𝑃 ∈ ℝ)
331 halfge0 11234 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 0 ≤ (1 / 2)
332 rehalfcl 11243 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑃 ∈ ℝ → (𝑃 / 2) ∈ ℝ)
333332adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → (𝑃 / 2) ∈ ℝ)
334333, 260subge02d 10604 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → (0 ≤ (1 / 2) ↔ ((𝑃 / 2) − (1 / 2)) ≤ (𝑃 / 2)))
335331, 334mpbii 223 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → ((𝑃 / 2) − (1 / 2)) ≤ (𝑃 / 2))
336 simpl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → 𝑦 ∈ ℝ)
337246a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑃 ∈ ℝ → (1 / 2) ∈ ℝ)
338332, 337resubcld 10443 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑃 ∈ ℝ → ((𝑃 / 2) − (1 / 2)) ∈ ℝ)
339338adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → ((𝑃 / 2) − (1 / 2)) ∈ ℝ)
340 letr 10116 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑦 ∈ ℝ ∧ ((𝑃 / 2) − (1 / 2)) ∈ ℝ ∧ (𝑃 / 2) ∈ ℝ) → ((𝑦 ≤ ((𝑃 / 2) − (1 / 2)) ∧ ((𝑃 / 2) − (1 / 2)) ≤ (𝑃 / 2)) → 𝑦 ≤ (𝑃 / 2)))
341336, 339, 333, 340syl3anc 1324 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → ((𝑦 ≤ ((𝑃 / 2) − (1 / 2)) ∧ ((𝑃 / 2) − (1 / 2)) ≤ (𝑃 / 2)) → 𝑦 ≤ (𝑃 / 2)))
342335, 341mpan2d 709 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → (𝑦 ≤ ((𝑃 / 2) − (1 / 2)) → 𝑦 ≤ (𝑃 / 2)))
34381adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → 𝑃 ∈ ℂ)
344 1cnd 10041 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → 1 ∈ ℂ)
345230a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → (2 ∈ ℂ ∧ 2 ≠ 0))
346343, 344, 345, 232syl3anc 1324 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → ((𝑃 − 1) / 2) = ((𝑃 / 2) − (1 / 2)))
347346breq2d 4656 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → (𝑦 ≤ ((𝑃 − 1) / 2) ↔ 𝑦 ≤ ((𝑃 / 2) − (1 / 2))))
348 lesub 10492 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑃 / 2) ∈ ℝ ∧ 𝑃 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((𝑃 / 2) ≤ (𝑃𝑦) ↔ 𝑦 ≤ (𝑃 − (𝑃 / 2))))
349333, 258, 336, 348syl3anc 1324 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → ((𝑃 / 2) ≤ (𝑃𝑦) ↔ 𝑦 ≤ (𝑃 − (𝑃 / 2))))
350259, 263lenltd 10168 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → ((𝑃 / 2) ≤ (𝑃𝑦) ↔ ¬ (𝑃𝑦) < (𝑃 / 2)))
351 2cnd 11078 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑃 ∈ ℝ → 2 ∈ ℂ)
352187a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑃 ∈ ℝ → 2 ≠ 0)
35381, 351, 352divcan1d 10787 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑃 ∈ ℝ → ((𝑃 / 2) · 2) = 𝑃)
354353eqcomd 2626 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑃 ∈ ℝ → 𝑃 = ((𝑃 / 2) · 2))
355354oveq1d 6650 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑃 ∈ ℝ → (𝑃 − (𝑃 / 2)) = (((𝑃 / 2) · 2) − (𝑃 / 2)))
356332recnd 10053 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑃 ∈ ℝ → (𝑃 / 2) ∈ ℂ)
357356, 351mulcomd 10046 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑃 ∈ ℝ → ((𝑃 / 2) · 2) = (2 · (𝑃 / 2)))
358357oveq1d 6650 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑃 ∈ ℝ → (((𝑃 / 2) · 2) − (𝑃 / 2)) = ((2 · (𝑃 / 2)) − (𝑃 / 2)))
359351, 356mulsubfacd 10477 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑃 ∈ ℝ → ((2 · (𝑃 / 2)) − (𝑃 / 2)) = ((2 − 1) · (𝑃 / 2)))
360 2m1e1 11120 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (2 − 1) = 1
361360a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑃 ∈ ℝ → (2 − 1) = 1)
362361oveq1d 6650 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑃 ∈ ℝ → ((2 − 1) · (𝑃 / 2)) = (1 · (𝑃 / 2)))
363356mulid2d 10043 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑃 ∈ ℝ → (1 · (𝑃 / 2)) = (𝑃 / 2))
364359, 362, 3633eqtrd 2658 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑃 ∈ ℝ → ((2 · (𝑃 / 2)) − (𝑃 / 2)) = (𝑃 / 2))
365355, 358, 3643eqtrd 2658 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑃 ∈ ℝ → (𝑃 − (𝑃 / 2)) = (𝑃 / 2))
366365adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → (𝑃 − (𝑃 / 2)) = (𝑃 / 2))
367366breq2d 4656 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → (𝑦 ≤ (𝑃 − (𝑃 / 2)) ↔ 𝑦 ≤ (𝑃 / 2)))
368349, 350, 3673bitr3d 298 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → (¬ (𝑃𝑦) < (𝑃 / 2) ↔ 𝑦 ≤ (𝑃 / 2)))
369342, 347, 3683imtr4d 283 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → (𝑦 ≤ ((𝑃 − 1) / 2) → ¬ (𝑃𝑦) < (𝑃 / 2)))
370369ex 450 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ ℝ → (𝑃 ∈ ℝ → (𝑦 ≤ ((𝑃 − 1) / 2) → ¬ (𝑃𝑦) < (𝑃 / 2))))
371156, 370syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 ∈ ℕ → (𝑃 ∈ ℝ → (𝑦 ≤ ((𝑃 − 1) / 2) → ¬ (𝑃𝑦) < (𝑃 / 2))))
372371com3l 89 . . . . . . . . . . . . . . . . . . . . 21 (𝑃 ∈ ℝ → (𝑦 ≤ ((𝑃 − 1) / 2) → (𝑦 ∈ ℕ → ¬ (𝑃𝑦) < (𝑃 / 2))))
373330, 372syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝑃 ∈ ℤ → (𝑦 ≤ ((𝑃 − 1) / 2) → (𝑦 ∈ ℕ → ¬ (𝑃𝑦) < (𝑃 / 2))))
37455, 56, 3733syl 18 . . . . . . . . . . . . . . . . . . 19 (𝑃 ∈ (ℙ ∖ {2}) → (𝑦 ≤ ((𝑃 − 1) / 2) → (𝑦 ∈ ℕ → ¬ (𝑃𝑦) < (𝑃 / 2))))
37520, 374syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑦 ≤ ((𝑃 − 1) / 2) → (𝑦 ∈ ℕ → ¬ (𝑃𝑦) < (𝑃 / 2))))
376375adantl 482 . . . . . . . . . . . . . . . . 17 ((¬ 2 ∥ 𝑦𝜑) → (𝑦 ≤ ((𝑃 − 1) / 2) → (𝑦 ∈ ℕ → ¬ (𝑃𝑦) < (𝑃 / 2))))
377376com13 88 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℕ → (𝑦 ≤ ((𝑃 − 1) / 2) → ((¬ 2 ∥ 𝑦𝜑) → ¬ (𝑃𝑦) < (𝑃 / 2))))
378190, 377syl5bi 232 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → (𝑦𝐻 → ((¬ 2 ∥ 𝑦𝜑) → ¬ (𝑃𝑦) < (𝑃 / 2))))
379378a1d 25 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → (𝐻 ∈ ℕ → (𝑦𝐻 → ((¬ 2 ∥ 𝑦𝜑) → ¬ (𝑃𝑦) < (𝑃 / 2)))))
3803793imp 1254 . . . . . . . . . . . . 13 ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦𝐻) → ((¬ 2 ∥ 𝑦𝜑) → ¬ (𝑃𝑦) < (𝑃 / 2)))
381380com12 32 . . . . . . . . . . . 12 ((¬ 2 ∥ 𝑦𝜑) → ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦𝐻) → ¬ (𝑃𝑦) < (𝑃 / 2)))
382150, 381syl5bi 232 . . . . . . . . . . 11 ((¬ 2 ∥ 𝑦𝜑) → (𝑦 ∈ (1...𝐻) → ¬ (𝑃𝑦) < (𝑃 / 2)))
3833823impia 1259 . . . . . . . . . 10 ((¬ 2 ∥ 𝑦𝜑𝑦 ∈ (1...𝐻)) → ¬ (𝑃𝑦) < (𝑃 / 2))
384329, 383eqnbrtrd 4662 . . . . . . . . 9 ((¬ 2 ∥ 𝑦𝜑𝑦 ∈ (1...𝐻)) → ¬ (((𝑃𝑦) / 2) · 2) < (𝑃 / 2))
385384iffalsed 4088 . . . . . . . 8 ((¬ 2 ∥ 𝑦𝜑𝑦 ∈ (1...𝐻)) → if((((𝑃𝑦) / 2) · 2) < (𝑃 / 2), (((𝑃𝑦) / 2) · 2), (𝑃 − (((𝑃𝑦) / 2) · 2))) = (𝑃 − (((𝑃𝑦) / 2) · 2)))
386329oveq2d 6651 . . . . . . . 8 ((¬ 2 ∥ 𝑦𝜑𝑦 ∈ (1...𝐻)) → (𝑃 − (((𝑃𝑦) / 2) · 2)) = (𝑃 − (𝑃𝑦)))
387323, 184anim12i 589 . . . . . . . . . 10 ((𝜑𝑦 ∈ (1...𝐻)) → (𝑃 ∈ ℂ ∧ 𝑦 ∈ ℂ))
3883873adant1 1077 . . . . . . . . 9 ((¬ 2 ∥ 𝑦𝜑𝑦 ∈ (1...𝐻)) → (𝑃 ∈ ℂ ∧ 𝑦 ∈ ℂ))
389 nncan 10295 . . . . . . . . 9 ((𝑃 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑃 − (𝑃𝑦)) = 𝑦)
390388, 389syl 17 . . . . . . . 8 ((¬ 2 ∥ 𝑦𝜑𝑦 ∈ (1...𝐻)) → (𝑃 − (𝑃𝑦)) = 𝑦)
391385, 386, 3903eqtrrd 2659 . . . . . . 7 ((¬ 2 ∥ 𝑦𝜑𝑦 ∈ (1...𝐻)) → 𝑦 = if((((𝑃𝑦) / 2) · 2) < (𝑃 / 2), (((𝑃𝑦) / 2) · 2), (𝑃 − (((𝑃𝑦) / 2) · 2))))
392316, 322, 391rspcedvd 3312 . . . . . 6 ((¬ 2 ∥ 𝑦𝜑𝑦 ∈ (1...𝐻)) → ∃𝑥 ∈ (1...𝐻)𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))))
3933923exp 1262 . . . . 5 (¬ 2 ∥ 𝑦 → (𝜑 → (𝑦 ∈ (1...𝐻) → ∃𝑥 ∈ (1...𝐻)𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))))))
394211, 393pm2.61i 176 . . . 4 (𝜑 → (𝑦 ∈ (1...𝐻) → ∃𝑥 ∈ (1...𝐻)𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2)))))
395149, 394impbid 202 . . 3 (𝜑 → (∃𝑥 ∈ (1...𝐻)𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) ↔ 𝑦 ∈ (1...𝐻)))
3964, 395syl5bb 272 . 2 (𝜑 → (𝑦 ∈ ran 𝑅𝑦 ∈ (1...𝐻)))
397396eqrdv 2618 1 (𝜑 → ran 𝑅 = (1...𝐻))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 384  w3a 1036   = wceq 1481  wcel 1988  wne 2791  wrex 2910  Vcvv 3195  cdif 3564  ifcif 4077  {csn 4168   class class class wbr 4644  cmpt 4720  ran crn 5105  (class class class)co 6635  cc 9919  cr 9920  0cc0 9921  1c1 9922   + caddc 9924   · cmul 9926   < clt 10059  cle 10060  cmin 10251   / cdiv 10669  cn 11005  2c2 11055  cz 11362  +crp 11817  ...cfz 12311  cdvds 14964  cprime 15366
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-8 1990  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-sep 4772  ax-nul 4780  ax-pow 4834  ax-pr 4897  ax-un 6934  ax-cnex 9977  ax-resscn 9978  ax-1cn 9979  ax-icn 9980  ax-addcl 9981  ax-addrcl 9982  ax-mulcl 9983  ax-mulrcl 9984  ax-mulcom 9985  ax-addass 9986  ax-mulass 9987  ax-distr 9988  ax-i2m1 9989  ax-1ne0 9990  ax-1rid 9991  ax-rnegex 9992  ax-rrecex 9993  ax-cnre 9994  ax-pre-lttri 9995  ax-pre-lttrn 9996  ax-pre-ltadd 9997  ax-pre-mulgt0 9998  ax-pre-sup 9999
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ne 2792  df-nel 2895  df-ral 2914  df-rex 2915  df-reu 2916  df-rmo 2917  df-rab 2918  df-v 3197  df-sbc 3430  df-csb 3527  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-pss 3583  df-nul 3908  df-if 4078  df-pw 4151  df-sn 4169  df-pr 4171  df-tp 4173  df-op 4175  df-uni 4428  df-int 4467  df-iun 4513  df-br 4645  df-opab 4704  df-mpt 4721  df-tr 4744  df-id 5014  df-eprel 5019  df-po 5025  df-so 5026  df-fr 5063  df-we 5065  df-xp 5110  df-rel 5111  df-cnv 5112  df-co 5113  df-dm 5114  df-rn 5115  df-res 5116  df-ima 5117  df-pred 5668  df-ord 5714  df-on 5715  df-lim 5716  df-suc 5717  df-iota 5839  df-fun 5878  df-fn 5879  df-f 5880  df-f1 5881  df-fo 5882  df-f1o 5883  df-fv 5884  df-riota 6596  df-ov 6638  df-oprab 6639  df-mpt2 6640  df-om 7051  df-1st 7153  df-2nd 7154  df-wrecs 7392  df-recs 7453  df-rdg 7491  df-1o 7545  df-2o 7546  df-oadd 7549  df-er 7727  df-en 7941  df-dom 7942  df-sdom 7943  df-fin 7944  df-sup 8333  df-pnf 10061  df-mnf 10062  df-xr 10063  df-ltxr 10064  df-le 10065  df-sub 10253  df-neg 10254  df-div 10670  df-nn 11006  df-2 11064  df-3 11065  df-n0 11278  df-z 11363  df-uz 11673  df-rp 11818  df-ioo 12164  df-fz 12312  df-seq 12785  df-exp 12844  df-cj 13820  df-re 13821  df-im 13822  df-sqrt 13956  df-abs 13957  df-dvds 14965  df-prm 15367
This theorem is referenced by:  gausslemma2dlem1  25072
  Copyright terms: Public domain W3C validator