ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  gausslemma2dlem1a GIF version

Theorem gausslemma2dlem1a 15102
Description: Lemma for gausslemma2dlem1 15105. (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 4901 . . . 4 (𝑦 ∈ V → (𝑦 ∈ ran 𝑅 ↔ ∃𝑥 ∈ (1...𝐻)𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2)))))
32elv 2760 . . 3 (𝑦 ∈ ran 𝑅 ↔ ∃𝑥 ∈ (1...𝐻)𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))))
4 iftrue 3558 . . . . . . . . . 10 ((𝑥 · 2) < (𝑃 / 2) → if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) = (𝑥 · 2))
54eqeq2d 2201 . . . . . . . . 9 ((𝑥 · 2) < (𝑃 / 2) → (𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) ↔ 𝑦 = (𝑥 · 2)))
65adantr 276 . . . . . . . 8 (((𝑥 · 2) < (𝑃 / 2) ∧ (𝜑𝑥 ∈ (1...𝐻))) → (𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) ↔ 𝑦 = (𝑥 · 2)))
7 elfz1b 10142 . . . . . . . . . . . . 13 (𝑥 ∈ (1...𝐻) ↔ (𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥𝐻))
8 id 19 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℕ → 𝑥 ∈ ℕ)
9 2nn 9129 . . . . . . . . . . . . . . . . . . 19 2 ∈ ℕ
109a1i 9 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℕ → 2 ∈ ℕ)
118, 10nnmulcld 9017 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ℕ → (𝑥 · 2) ∈ ℕ)
12113ad2ant1 1020 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥𝐻) → (𝑥 · 2) ∈ ℕ)
13123ad2ant1 1020 . . . . . . . . . . . . . . 15 (((𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥𝐻) ∧ 𝜑 ∧ (𝑥 · 2) < (𝑃 / 2)) → (𝑥 · 2) ∈ ℕ)
14 gausslemma2d.h . . . . . . . . . . . . . . . . . . 19 𝐻 = ((𝑃 − 1) / 2)
1514eleq1i 2255 . . . . . . . . . . . . . . . . . 18 (𝐻 ∈ ℕ ↔ ((𝑃 − 1) / 2) ∈ ℕ)
1615biimpi 120 . . . . . . . . . . . . . . . . 17 (𝐻 ∈ ℕ → ((𝑃 − 1) / 2) ∈ ℕ)
17163ad2ant2 1021 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥𝐻) → ((𝑃 − 1) / 2) ∈ ℕ)
18173ad2ant1 1020 . . . . . . . . . . . . . . 15 (((𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥𝐻) ∧ 𝜑 ∧ (𝑥 · 2) < (𝑃 / 2)) → ((𝑃 − 1) / 2) ∈ ℕ)
19 gausslemma2d.p . . . . . . . . . . . . . . . . . . 19 (𝜑𝑃 ∈ (ℙ ∖ {2}))
20 nnoddn2prm 12372 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑃 ∈ (ℙ ∖ {2}) → (𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃))
21 nnz 9322 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑃 ∈ ℕ → 𝑃 ∈ ℤ)
2221anim1i 340 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) → (𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃))
2320, 22syl 14 . . . . . . . . . . . . . . . . . . . . . 22 (𝑃 ∈ (ℙ ∖ {2}) → (𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃))
24 nnz 9322 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 ∈ ℕ → 𝑥 ∈ ℤ)
25 2z 9331 . . . . . . . . . . . . . . . . . . . . . . . . 25 2 ∈ ℤ
2625a1i 9 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 ∈ ℕ → 2 ∈ ℤ)
2724, 26zmulcld 9431 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ ℕ → (𝑥 · 2) ∈ ℤ)
28273ad2ant1 1020 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥𝐻) → (𝑥 · 2) ∈ ℤ)
2923, 28anim12i 338 . . . . . . . . . . . . . . . . . . . . 21 ((𝑃 ∈ (ℙ ∖ {2}) ∧ (𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥𝐻)) → ((𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃) ∧ (𝑥 · 2) ∈ ℤ))
30 df-3an 982 . . . . . . . . . . . . . . . . . . . . 21 ((𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ∧ (𝑥 · 2) ∈ ℤ) ↔ ((𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃) ∧ (𝑥 · 2) ∈ ℤ))
3129, 30sylibr 134 . . . . . . . . . . . . . . . . . . . 20 ((𝑃 ∈ (ℙ ∖ {2}) ∧ (𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥𝐻)) → (𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ∧ (𝑥 · 2) ∈ ℤ))
3231ex 115 . . . . . . . . . . . . . . . . . . 19 (𝑃 ∈ (ℙ ∖ {2}) → ((𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥𝐻) → (𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ∧ (𝑥 · 2) ∈ ℤ)))
3319, 32syl 14 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥𝐻) → (𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ∧ (𝑥 · 2) ∈ ℤ)))
3433impcom 125 . . . . . . . . . . . . . . . . 17 (((𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥𝐻) ∧ 𝜑) → (𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ∧ (𝑥 · 2) ∈ ℤ))
35 ltoddhalfle 12008 . . . . . . . . . . . . . . . . 17 ((𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ∧ (𝑥 · 2) ∈ ℤ) → ((𝑥 · 2) < (𝑃 / 2) ↔ (𝑥 · 2) ≤ ((𝑃 − 1) / 2)))
3634, 35syl 14 . . . . . . . . . . . . . . . 16 (((𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥𝐻) ∧ 𝜑) → ((𝑥 · 2) < (𝑃 / 2) ↔ (𝑥 · 2) ≤ ((𝑃 − 1) / 2)))
3736biimp3a 1356 . . . . . . . . . . . . . . 15 (((𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥𝐻) ∧ 𝜑 ∧ (𝑥 · 2) < (𝑃 / 2)) → (𝑥 · 2) ≤ ((𝑃 − 1) / 2))
3813, 18, 373jca 1179 . . . . . . . . . . . . . 14 (((𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥𝐻) ∧ 𝜑 ∧ (𝑥 · 2) < (𝑃 / 2)) → ((𝑥 · 2) ∈ ℕ ∧ ((𝑃 − 1) / 2) ∈ ℕ ∧ (𝑥 · 2) ≤ ((𝑃 − 1) / 2)))
39383exp 1204 . . . . . . . . . . . . 13 ((𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥𝐻) → (𝜑 → ((𝑥 · 2) < (𝑃 / 2) → ((𝑥 · 2) ∈ ℕ ∧ ((𝑃 − 1) / 2) ∈ ℕ ∧ (𝑥 · 2) ≤ ((𝑃 − 1) / 2)))))
407, 39sylbi 121 . . . . . . . . . . . 12 (𝑥 ∈ (1...𝐻) → (𝜑 → ((𝑥 · 2) < (𝑃 / 2) → ((𝑥 · 2) ∈ ℕ ∧ ((𝑃 − 1) / 2) ∈ ℕ ∧ (𝑥 · 2) ≤ ((𝑃 − 1) / 2)))))
4140impcom 125 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (1...𝐻)) → ((𝑥 · 2) < (𝑃 / 2) → ((𝑥 · 2) ∈ ℕ ∧ ((𝑃 − 1) / 2) ∈ ℕ ∧ (𝑥 · 2) ≤ ((𝑃 − 1) / 2))))
4241impcom 125 . . . . . . . . . 10 (((𝑥 · 2) < (𝑃 / 2) ∧ (𝜑𝑥 ∈ (1...𝐻))) → ((𝑥 · 2) ∈ ℕ ∧ ((𝑃 − 1) / 2) ∈ ℕ ∧ (𝑥 · 2) ≤ ((𝑃 − 1) / 2)))
4314oveq2i 5917 . . . . . . . . . . . 12 (1...𝐻) = (1...((𝑃 − 1) / 2))
4443eleq2i 2256 . . . . . . . . . . 11 ((𝑥 · 2) ∈ (1...𝐻) ↔ (𝑥 · 2) ∈ (1...((𝑃 − 1) / 2)))
45 elfz1b 10142 . . . . . . . . . . 11 ((𝑥 · 2) ∈ (1...((𝑃 − 1) / 2)) ↔ ((𝑥 · 2) ∈ ℕ ∧ ((𝑃 − 1) / 2) ∈ ℕ ∧ (𝑥 · 2) ≤ ((𝑃 − 1) / 2)))
4644, 45bitri 184 . . . . . . . . . 10 ((𝑥 · 2) ∈ (1...𝐻) ↔ ((𝑥 · 2) ∈ ℕ ∧ ((𝑃 − 1) / 2) ∈ ℕ ∧ (𝑥 · 2) ≤ ((𝑃 − 1) / 2)))
4742, 46sylibr 134 . . . . . . . . 9 (((𝑥 · 2) < (𝑃 / 2) ∧ (𝜑𝑥 ∈ (1...𝐻))) → (𝑥 · 2) ∈ (1...𝐻))
48 eleq1 2252 . . . . . . . . 9 (𝑦 = (𝑥 · 2) → (𝑦 ∈ (1...𝐻) ↔ (𝑥 · 2) ∈ (1...𝐻)))
4947, 48syl5ibrcom 157 . . . . . . . 8 (((𝑥 · 2) < (𝑃 / 2) ∧ (𝜑𝑥 ∈ (1...𝐻))) → (𝑦 = (𝑥 · 2) → 𝑦 ∈ (1...𝐻)))
506, 49sylbid 150 . . . . . . 7 (((𝑥 · 2) < (𝑃 / 2) ∧ (𝜑𝑥 ∈ (1...𝐻))) → (𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) → 𝑦 ∈ (1...𝐻)))
5150ancoms 268 . . . . . 6 (((𝜑𝑥 ∈ (1...𝐻)) ∧ (𝑥 · 2) < (𝑃 / 2)) → (𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) → 𝑦 ∈ (1...𝐻)))
52 iffalse 3561 . . . . . . . . . 10 (¬ (𝑥 · 2) < (𝑃 / 2) → if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) = (𝑃 − (𝑥 · 2)))
5352eqeq2d 2201 . . . . . . . . 9 (¬ (𝑥 · 2) < (𝑃 / 2) → (𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) ↔ 𝑦 = (𝑃 − (𝑥 · 2))))
5453adantr 276 . . . . . . . 8 ((¬ (𝑥 · 2) < (𝑃 / 2) ∧ (𝜑𝑥 ∈ (1...𝐻))) → (𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) ↔ 𝑦 = (𝑃 − (𝑥 · 2))))
55 eldifi 3277 . . . . . . . . . . . . . 14 (𝑃 ∈ (ℙ ∖ {2}) → 𝑃 ∈ ℙ)
56 prmz 12223 . . . . . . . . . . . . . 14 (𝑃 ∈ ℙ → 𝑃 ∈ ℤ)
5719, 55, 563syl 17 . . . . . . . . . . . . 13 (𝜑𝑃 ∈ ℤ)
5857ad2antrl 490 . . . . . . . . . . . 12 ((¬ (𝑥 · 2) < (𝑃 / 2) ∧ (𝜑𝑥 ∈ (1...𝐻))) → 𝑃 ∈ ℤ)
59 elfzelz 10077 . . . . . . . . . . . . . 14 (𝑥 ∈ (1...𝐻) → 𝑥 ∈ ℤ)
6025a1i 9 . . . . . . . . . . . . . 14 (𝑥 ∈ (1...𝐻) → 2 ∈ ℤ)
6159, 60zmulcld 9431 . . . . . . . . . . . . 13 (𝑥 ∈ (1...𝐻) → (𝑥 · 2) ∈ ℤ)
6261ad2antll 491 . . . . . . . . . . . 12 ((¬ (𝑥 · 2) < (𝑃 / 2) ∧ (𝜑𝑥 ∈ (1...𝐻))) → (𝑥 · 2) ∈ ℤ)
6358, 62zsubcld 9430 . . . . . . . . . . 11 ((¬ (𝑥 · 2) < (𝑃 / 2) ∧ (𝜑𝑥 ∈ (1...𝐻))) → (𝑃 − (𝑥 · 2)) ∈ ℤ)
6456zred 9425 . . . . . . . . . . . . . 14 (𝑃 ∈ ℙ → 𝑃 ∈ ℝ)
6514breq2i 4033 . . . . . . . . . . . . . . . . . . . 20 (𝑥𝐻𝑥 ≤ ((𝑃 − 1) / 2))
66 nnre 8975 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ ℕ → 𝑥 ∈ ℝ)
6766adantr 276 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ) → 𝑥 ∈ ℝ)
68 peano2rem 8272 . . . . . . . . . . . . . . . . . . . . . 22 (𝑃 ∈ ℝ → (𝑃 − 1) ∈ ℝ)
6968adantl 277 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ) → (𝑃 − 1) ∈ ℝ)
70 2re 9038 . . . . . . . . . . . . . . . . . . . . . . 23 2 ∈ ℝ
71 2pos 9059 . . . . . . . . . . . . . . . . . . . . . . 23 0 < 2
7270, 71pm3.2i 272 . . . . . . . . . . . . . . . . . . . . . 22 (2 ∈ ℝ ∧ 0 < 2)
7372a1i 9 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ) → (2 ∈ ℝ ∧ 0 < 2))
74 lemuldiv 8886 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 ∈ ℝ ∧ (𝑃 − 1) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((𝑥 · 2) ≤ (𝑃 − 1) ↔ 𝑥 ≤ ((𝑃 − 1) / 2)))
7567, 69, 73, 74syl3anc 1249 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ) → ((𝑥 · 2) ≤ (𝑃 − 1) ↔ 𝑥 ≤ ((𝑃 − 1) / 2)))
7665, 75bitr4id 199 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ) → (𝑥𝐻 ↔ (𝑥 · 2) ≤ (𝑃 − 1)))
7711nnred 8981 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ ℕ → (𝑥 · 2) ∈ ℝ)
7877adantr 276 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ) → (𝑥 · 2) ∈ ℝ)
79 simpr 110 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ) → 𝑃 ∈ ℝ)
8078, 69, 79lesub2d 8558 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ) → ((𝑥 · 2) ≤ (𝑃 − 1) ↔ (𝑃 − (𝑃 − 1)) ≤ (𝑃 − (𝑥 · 2))))
81 recn 7991 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑃 ∈ ℝ → 𝑃 ∈ ℂ)
82 1cnd 8021 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑃 ∈ ℝ → 1 ∈ ℂ)
8381, 82nncand 8321 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑃 ∈ ℝ → (𝑃 − (𝑃 − 1)) = 1)
8483adantl 277 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ) → (𝑃 − (𝑃 − 1)) = 1)
8584breq1d 4035 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ) → ((𝑃 − (𝑃 − 1)) ≤ (𝑃 − (𝑥 · 2)) ↔ 1 ≤ (𝑃 − (𝑥 · 2))))
8685biimpd 144 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ) → ((𝑃 − (𝑃 − 1)) ≤ (𝑃 − (𝑥 · 2)) → 1 ≤ (𝑃 − (𝑥 · 2))))
8780, 86sylbid 150 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ) → ((𝑥 · 2) ≤ (𝑃 − 1) → 1 ≤ (𝑃 − (𝑥 · 2))))
8876, 87sylbid 150 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ) → (𝑥𝐻 → 1 ≤ (𝑃 − (𝑥 · 2))))
8988impancom 260 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ ℕ ∧ 𝑥𝐻) → (𝑃 ∈ ℝ → 1 ≤ (𝑃 − (𝑥 · 2))))
90893adant2 1018 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥𝐻) → (𝑃 ∈ ℝ → 1 ≤ (𝑃 − (𝑥 · 2))))
917, 90sylbi 121 . . . . . . . . . . . . . . 15 (𝑥 ∈ (1...𝐻) → (𝑃 ∈ ℝ → 1 ≤ (𝑃 − (𝑥 · 2))))
9291com12 30 . . . . . . . . . . . . . 14 (𝑃 ∈ ℝ → (𝑥 ∈ (1...𝐻) → 1 ≤ (𝑃 − (𝑥 · 2))))
9319, 55, 64, 924syl 18 . . . . . . . . . . . . 13 (𝜑 → (𝑥 ∈ (1...𝐻) → 1 ≤ (𝑃 − (𝑥 · 2))))
9493imp 124 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ (1...𝐻)) → 1 ≤ (𝑃 − (𝑥 · 2)))
9594adantl 277 . . . . . . . . . . 11 ((¬ (𝑥 · 2) < (𝑃 / 2) ∧ (𝜑𝑥 ∈ (1...𝐻))) → 1 ≤ (𝑃 − (𝑥 · 2)))
96 elnnz1 9326 . . . . . . . . . . 11 ((𝑃 − (𝑥 · 2)) ∈ ℕ ↔ ((𝑃 − (𝑥 · 2)) ∈ ℤ ∧ 1 ≤ (𝑃 − (𝑥 · 2))))
9763, 95, 96sylanbrc 417 . . . . . . . . . 10 ((¬ (𝑥 · 2) < (𝑃 / 2) ∧ (𝜑𝑥 ∈ (1...𝐻))) → (𝑃 − (𝑥 · 2)) ∈ ℕ)
987simp2bi 1015 . . . . . . . . . . 11 (𝑥 ∈ (1...𝐻) → 𝐻 ∈ ℕ)
9998ad2antll 491 . . . . . . . . . 10 ((¬ (𝑥 · 2) < (𝑃 / 2) ∧ (𝜑𝑥 ∈ (1...𝐻))) → 𝐻 ∈ ℕ)
100 nnre 8975 . . . . . . . . . . . . . . . . . 18 (𝑃 ∈ ℕ → 𝑃 ∈ ℝ)
101100rehalfcld 9215 . . . . . . . . . . . . . . . . 17 (𝑃 ∈ ℕ → (𝑃 / 2) ∈ ℝ)
102101adantr 276 . . . . . . . . . . . . . . . 16 ((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) → (𝑃 / 2) ∈ ℝ)
10361zred 9425 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (1...𝐻) → (𝑥 · 2) ∈ ℝ)
104 lenlt 8081 . . . . . . . . . . . . . . . 16 (((𝑃 / 2) ∈ ℝ ∧ (𝑥 · 2) ∈ ℝ) → ((𝑃 / 2) ≤ (𝑥 · 2) ↔ ¬ (𝑥 · 2) < (𝑃 / 2)))
105102, 103, 104syl2an 289 . . . . . . . . . . . . . . 15 (((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → ((𝑃 / 2) ≤ (𝑥 · 2) ↔ ¬ (𝑥 · 2) < (𝑃 / 2)))
10622, 61anim12i 338 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → ((𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃) ∧ (𝑥 · 2) ∈ ℤ))
107106, 30sylibr 134 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → (𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ∧ (𝑥 · 2) ∈ ℤ))
108 halfleoddlt 12009 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ∧ (𝑥 · 2) ∈ ℤ) → ((𝑃 / 2) ≤ (𝑥 · 2) ↔ (𝑃 / 2) < (𝑥 · 2)))
109107, 108syl 14 . . . . . . . . . . . . . . . . . . . . 21 (((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → ((𝑃 / 2) ≤ (𝑥 · 2) ↔ (𝑃 / 2) < (𝑥 · 2)))
110109biimpa 296 . . . . . . . . . . . . . . . . . . . 20 ((((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) ∧ (𝑃 / 2) ≤ (𝑥 · 2)) → (𝑃 / 2) < (𝑥 · 2))
111 nncn 8976 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑃 ∈ ℕ → 𝑃 ∈ ℂ)
112 subhalfhalf 9203 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑃 ∈ ℂ → (𝑃 − (𝑃 / 2)) = (𝑃 / 2))
113111, 112syl 14 . . . . . . . . . . . . . . . . . . . . . 22 (𝑃 ∈ ℕ → (𝑃 − (𝑃 / 2)) = (𝑃 / 2))
114113breq1d 4035 . . . . . . . . . . . . . . . . . . . . 21 (𝑃 ∈ ℕ → ((𝑃 − (𝑃 / 2)) < (𝑥 · 2) ↔ (𝑃 / 2) < (𝑥 · 2)))
115114ad3antrrr 492 . . . . . . . . . . . . . . . . . . . 20 ((((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) ∧ (𝑃 / 2) ≤ (𝑥 · 2)) → ((𝑃 − (𝑃 / 2)) < (𝑥 · 2) ↔ (𝑃 / 2) < (𝑥 · 2)))
116110, 115mpbird 167 . . . . . . . . . . . . . . . . . . 19 ((((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) ∧ (𝑃 / 2) ≤ (𝑥 · 2)) → (𝑃 − (𝑃 / 2)) < (𝑥 · 2))
117100ad2antrr 488 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → 𝑃 ∈ ℝ)
118101ad2antrr 488 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → (𝑃 / 2) ∈ ℝ)
119103adantl 277 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → (𝑥 · 2) ∈ ℝ)
120117, 118, 1193jca 1179 . . . . . . . . . . . . . . . . . . . . 21 (((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → (𝑃 ∈ ℝ ∧ (𝑃 / 2) ∈ ℝ ∧ (𝑥 · 2) ∈ ℝ))
121120adantr 276 . . . . . . . . . . . . . . . . . . . 20 ((((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) ∧ (𝑃 / 2) ≤ (𝑥 · 2)) → (𝑃 ∈ ℝ ∧ (𝑃 / 2) ∈ ℝ ∧ (𝑥 · 2) ∈ ℝ))
122 ltsub23 8447 . . . . . . . . . . . . . . . . . . . 20 ((𝑃 ∈ ℝ ∧ (𝑃 / 2) ∈ ℝ ∧ (𝑥 · 2) ∈ ℝ) → ((𝑃 − (𝑃 / 2)) < (𝑥 · 2) ↔ (𝑃 − (𝑥 · 2)) < (𝑃 / 2)))
123121, 122syl 14 . . . . . . . . . . . . . . . . . . 19 ((((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) ∧ (𝑃 / 2) ≤ (𝑥 · 2)) → ((𝑃 − (𝑃 / 2)) < (𝑥 · 2) ↔ (𝑃 − (𝑥 · 2)) < (𝑃 / 2)))
124116, 123mpbid 147 . . . . . . . . . . . . . . . . . 18 ((((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) ∧ (𝑃 / 2) ≤ (𝑥 · 2)) → (𝑃 − (𝑥 · 2)) < (𝑃 / 2))
12521ad2antrr 488 . . . . . . . . . . . . . . . . . . . . 21 (((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → 𝑃 ∈ ℤ)
126 simplr 528 . . . . . . . . . . . . . . . . . . . . 21 (((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → ¬ 2 ∥ 𝑃)
12761adantl 277 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → (𝑥 · 2) ∈ ℤ)
128125, 127zsubcld 9430 . . . . . . . . . . . . . . . . . . . . 21 (((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → (𝑃 − (𝑥 · 2)) ∈ ℤ)
129125, 126, 1283jca 1179 . . . . . . . . . . . . . . . . . . . 20 (((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → (𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ∧ (𝑃 − (𝑥 · 2)) ∈ ℤ))
130129adantr 276 . . . . . . . . . . . . . . . . . . 19 ((((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) ∧ (𝑃 / 2) ≤ (𝑥 · 2)) → (𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ∧ (𝑃 − (𝑥 · 2)) ∈ ℤ))
131 ltoddhalfle 12008 . . . . . . . . . . . . . . . . . . 19 ((𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ∧ (𝑃 − (𝑥 · 2)) ∈ ℤ) → ((𝑃 − (𝑥 · 2)) < (𝑃 / 2) ↔ (𝑃 − (𝑥 · 2)) ≤ ((𝑃 − 1) / 2)))
132130, 131syl 14 . . . . . . . . . . . . . . . . . 18 ((((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) ∧ (𝑃 / 2) ≤ (𝑥 · 2)) → ((𝑃 − (𝑥 · 2)) < (𝑃 / 2) ↔ (𝑃 − (𝑥 · 2)) ≤ ((𝑃 − 1) / 2)))
133124, 132mpbid 147 . . . . . . . . . . . . . . . . 17 ((((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) ∧ (𝑃 / 2) ≤ (𝑥 · 2)) → (𝑃 − (𝑥 · 2)) ≤ ((𝑃 − 1) / 2))
134133ex 115 . . . . . . . . . . . . . . . 16 (((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → ((𝑃 / 2) ≤ (𝑥 · 2) → (𝑃 − (𝑥 · 2)) ≤ ((𝑃 − 1) / 2)))
13514breq2i 4033 . . . . . . . . . . . . . . . 16 ((𝑃 − (𝑥 · 2)) ≤ 𝐻 ↔ (𝑃 − (𝑥 · 2)) ≤ ((𝑃 − 1) / 2))
136134, 135imbitrrdi 162 . . . . . . . . . . . . . . 15 (((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → ((𝑃 / 2) ≤ (𝑥 · 2) → (𝑃 − (𝑥 · 2)) ≤ 𝐻))
137105, 136sylbird 170 . . . . . . . . . . . . . 14 (((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → (¬ (𝑥 · 2) < (𝑃 / 2) → (𝑃 − (𝑥 · 2)) ≤ 𝐻))
138137ex 115 . . . . . . . . . . . . 13 ((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) → (𝑥 ∈ (1...𝐻) → (¬ (𝑥 · 2) < (𝑃 / 2) → (𝑃 − (𝑥 · 2)) ≤ 𝐻)))
13919, 20, 1383syl 17 . . . . . . . . . . . 12 (𝜑 → (𝑥 ∈ (1...𝐻) → (¬ (𝑥 · 2) < (𝑃 / 2) → (𝑃 − (𝑥 · 2)) ≤ 𝐻)))
140139imp 124 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (1...𝐻)) → (¬ (𝑥 · 2) < (𝑃 / 2) → (𝑃 − (𝑥 · 2)) ≤ 𝐻))
141140impcom 125 . . . . . . . . . 10 ((¬ (𝑥 · 2) < (𝑃 / 2) ∧ (𝜑𝑥 ∈ (1...𝐻))) → (𝑃 − (𝑥 · 2)) ≤ 𝐻)
142 elfz1b 10142 . . . . . . . . . 10 ((𝑃 − (𝑥 · 2)) ∈ (1...𝐻) ↔ ((𝑃 − (𝑥 · 2)) ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ (𝑃 − (𝑥 · 2)) ≤ 𝐻))
14397, 99, 141, 142syl3anbrc 1183 . . . . . . . . 9 ((¬ (𝑥 · 2) < (𝑃 / 2) ∧ (𝜑𝑥 ∈ (1...𝐻))) → (𝑃 − (𝑥 · 2)) ∈ (1...𝐻))
144 eleq1 2252 . . . . . . . . 9 (𝑦 = (𝑃 − (𝑥 · 2)) → (𝑦 ∈ (1...𝐻) ↔ (𝑃 − (𝑥 · 2)) ∈ (1...𝐻)))
145143, 144syl5ibrcom 157 . . . . . . . 8 ((¬ (𝑥 · 2) < (𝑃 / 2) ∧ (𝜑𝑥 ∈ (1...𝐻))) → (𝑦 = (𝑃 − (𝑥 · 2)) → 𝑦 ∈ (1...𝐻)))
14654, 145sylbid 150 . . . . . . 7 ((¬ (𝑥 · 2) < (𝑃 / 2) ∧ (𝜑𝑥 ∈ (1...𝐻))) → (𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) → 𝑦 ∈ (1...𝐻)))
147146ancoms 268 . . . . . 6 (((𝜑𝑥 ∈ (1...𝐻)) ∧ ¬ (𝑥 · 2) < (𝑃 / 2)) → (𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) → 𝑦 ∈ (1...𝐻)))
14861adantl 277 . . . . . . . . 9 ((𝜑𝑥 ∈ (1...𝐻)) → (𝑥 · 2) ∈ ℤ)
149 zq 9677 . . . . . . . . 9 ((𝑥 · 2) ∈ ℤ → (𝑥 · 2) ∈ ℚ)
150148, 149syl 14 . . . . . . . 8 ((𝜑𝑥 ∈ (1...𝐻)) → (𝑥 · 2) ∈ ℚ)
15157adantr 276 . . . . . . . . 9 ((𝜑𝑥 ∈ (1...𝐻)) → 𝑃 ∈ ℤ)
152 znq 9675 . . . . . . . . 9 ((𝑃 ∈ ℤ ∧ 2 ∈ ℕ) → (𝑃 / 2) ∈ ℚ)
153151, 9, 152sylancl 413 . . . . . . . 8 ((𝜑𝑥 ∈ (1...𝐻)) → (𝑃 / 2) ∈ ℚ)
154 qdclt 10301 . . . . . . . 8 (((𝑥 · 2) ∈ ℚ ∧ (𝑃 / 2) ∈ ℚ) → DECID (𝑥 · 2) < (𝑃 / 2))
155150, 153, 154syl2anc 411 . . . . . . 7 ((𝜑𝑥 ∈ (1...𝐻)) → DECID (𝑥 · 2) < (𝑃 / 2))
156 exmiddc 837 . . . . . . 7 (DECID (𝑥 · 2) < (𝑃 / 2) → ((𝑥 · 2) < (𝑃 / 2) ∨ ¬ (𝑥 · 2) < (𝑃 / 2)))
157155, 156syl 14 . . . . . 6 ((𝜑𝑥 ∈ (1...𝐻)) → ((𝑥 · 2) < (𝑃 / 2) ∨ ¬ (𝑥 · 2) < (𝑃 / 2)))
15851, 147, 157mpjaodan 799 . . . . 5 ((𝜑𝑥 ∈ (1...𝐻)) → (𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) → 𝑦 ∈ (1...𝐻)))
159158rexlimdva 2607 . . . 4 (𝜑 → (∃𝑥 ∈ (1...𝐻)𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) → 𝑦 ∈ (1...𝐻)))
160 elfz1b 10142 . . . . . . . . . . . 12 (𝑦 ∈ (1...𝐻) ↔ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦𝐻))
161 simp1 999 . . . . . . . . . . . . . . 15 ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦𝐻) → 𝑦 ∈ ℕ)
162 simpl 109 . . . . . . . . . . . . . . 15 ((2 ∥ 𝑦𝜑) → 2 ∥ 𝑦)
163 nnehalf 12019 . . . . . . . . . . . . . . 15 ((𝑦 ∈ ℕ ∧ 2 ∥ 𝑦) → (𝑦 / 2) ∈ ℕ)
164161, 162, 163syl2anr 290 . . . . . . . . . . . . . 14 (((2 ∥ 𝑦𝜑) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦𝐻)) → (𝑦 / 2) ∈ ℕ)
165 simpr2 1006 . . . . . . . . . . . . . 14 (((2 ∥ 𝑦𝜑) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦𝐻)) → 𝐻 ∈ ℕ)
166 nnre 8975 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ ℕ → 𝑦 ∈ ℝ)
167166ad2antrr 488 . . . . . . . . . . . . . . . . . . 19 (((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) ∧ (2 ∥ 𝑦𝜑)) → 𝑦 ∈ ℝ)
168 nnrp 9715 . . . . . . . . . . . . . . . . . . . . 21 (𝐻 ∈ ℕ → 𝐻 ∈ ℝ+)
169168adantl 277 . . . . . . . . . . . . . . . . . . . 20 ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) → 𝐻 ∈ ℝ+)
170169adantr 276 . . . . . . . . . . . . . . . . . . 19 (((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) ∧ (2 ∥ 𝑦𝜑)) → 𝐻 ∈ ℝ+)
171 2rp 9710 . . . . . . . . . . . . . . . . . . . . 21 2 ∈ ℝ+
172 1le2 9176 . . . . . . . . . . . . . . . . . . . . 21 1 ≤ 2
173171, 172pm3.2i 272 . . . . . . . . . . . . . . . . . . . 20 (2 ∈ ℝ+ ∧ 1 ≤ 2)
174173a1i 9 . . . . . . . . . . . . . . . . . . 19 (((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) ∧ (2 ∥ 𝑦𝜑)) → (2 ∈ ℝ+ ∧ 1 ≤ 2))
175 ledivge1le 9778 . . . . . . . . . . . . . . . . . . 19 ((𝑦 ∈ ℝ ∧ 𝐻 ∈ ℝ+ ∧ (2 ∈ ℝ+ ∧ 1 ≤ 2)) → (𝑦𝐻 → (𝑦 / 2) ≤ 𝐻))
176167, 170, 174, 175syl3anc 1249 . . . . . . . . . . . . . . . . . 18 (((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) ∧ (2 ∥ 𝑦𝜑)) → (𝑦𝐻 → (𝑦 / 2) ≤ 𝐻))
177176ex 115 . . . . . . . . . . . . . . . . 17 ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) → ((2 ∥ 𝑦𝜑) → (𝑦𝐻 → (𝑦 / 2) ≤ 𝐻)))
178177com23 78 . . . . . . . . . . . . . . . 16 ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) → (𝑦𝐻 → ((2 ∥ 𝑦𝜑) → (𝑦 / 2) ≤ 𝐻)))
1791783impia 1202 . . . . . . . . . . . . . . 15 ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦𝐻) → ((2 ∥ 𝑦𝜑) → (𝑦 / 2) ≤ 𝐻))
180179impcom 125 . . . . . . . . . . . . . 14 (((2 ∥ 𝑦𝜑) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦𝐻)) → (𝑦 / 2) ≤ 𝐻)
181164, 165, 1803jca 1179 . . . . . . . . . . . . 13 (((2 ∥ 𝑦𝜑) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦𝐻)) → ((𝑦 / 2) ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ (𝑦 / 2) ≤ 𝐻))
182181ex 115 . . . . . . . . . . . 12 ((2 ∥ 𝑦𝜑) → ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦𝐻) → ((𝑦 / 2) ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ (𝑦 / 2) ≤ 𝐻)))
183160, 182biimtrid 152 . . . . . . . . . . 11 ((2 ∥ 𝑦𝜑) → (𝑦 ∈ (1...𝐻) → ((𝑦 / 2) ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ (𝑦 / 2) ≤ 𝐻)))
1841833impia 1202 . . . . . . . . . 10 ((2 ∥ 𝑦𝜑𝑦 ∈ (1...𝐻)) → ((𝑦 / 2) ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ (𝑦 / 2) ≤ 𝐻))
185 elfz1b 10142 . . . . . . . . . 10 ((𝑦 / 2) ∈ (1...𝐻) ↔ ((𝑦 / 2) ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ (𝑦 / 2) ≤ 𝐻))
186184, 185sylibr 134 . . . . . . . . 9 ((2 ∥ 𝑦𝜑𝑦 ∈ (1...𝐻)) → (𝑦 / 2) ∈ (1...𝐻))
187 oveq1 5913 . . . . . . . . . . . . 13 (𝑥 = (𝑦 / 2) → (𝑥 · 2) = ((𝑦 / 2) · 2))
188187breq1d 4035 . . . . . . . . . . . 12 (𝑥 = (𝑦 / 2) → ((𝑥 · 2) < (𝑃 / 2) ↔ ((𝑦 / 2) · 2) < (𝑃 / 2)))
189187oveq2d 5922 . . . . . . . . . . . 12 (𝑥 = (𝑦 / 2) → (𝑃 − (𝑥 · 2)) = (𝑃 − ((𝑦 / 2) · 2)))
190188, 187, 189ifbieq12d 3579 . . . . . . . . . . 11 (𝑥 = (𝑦 / 2) → if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) = if(((𝑦 / 2) · 2) < (𝑃 / 2), ((𝑦 / 2) · 2), (𝑃 − ((𝑦 / 2) · 2))))
191190eqeq2d 2201 . . . . . . . . . 10 (𝑥 = (𝑦 / 2) → (𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) ↔ 𝑦 = if(((𝑦 / 2) · 2) < (𝑃 / 2), ((𝑦 / 2) · 2), (𝑃 − ((𝑦 / 2) · 2)))))
192191adantl 277 . . . . . . . . 9 (((2 ∥ 𝑦𝜑𝑦 ∈ (1...𝐻)) ∧ 𝑥 = (𝑦 / 2)) → (𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) ↔ 𝑦 = if(((𝑦 / 2) · 2) < (𝑃 / 2), ((𝑦 / 2) · 2), (𝑃 − ((𝑦 / 2) · 2)))))
193 elfzelz 10077 . . . . . . . . . . . . . . 15 (𝑦 ∈ (1...𝐻) → 𝑦 ∈ ℤ)
194193zcnd 9426 . . . . . . . . . . . . . 14 (𝑦 ∈ (1...𝐻) → 𝑦 ∈ ℂ)
1951943ad2ant3 1022 . . . . . . . . . . . . 13 ((2 ∥ 𝑦𝜑𝑦 ∈ (1...𝐻)) → 𝑦 ∈ ℂ)
196 2cnd 9041 . . . . . . . . . . . . 13 ((2 ∥ 𝑦𝜑𝑦 ∈ (1...𝐻)) → 2 ∈ ℂ)
197 2ap0 9061 . . . . . . . . . . . . . 14 2 # 0
198197a1i 9 . . . . . . . . . . . . 13 ((2 ∥ 𝑦𝜑𝑦 ∈ (1...𝐻)) → 2 # 0)
199195, 196, 198divcanap1d 8796 . . . . . . . . . . . 12 ((2 ∥ 𝑦𝜑𝑦 ∈ (1...𝐻)) → ((𝑦 / 2) · 2) = 𝑦)
20014breq2i 4033 . . . . . . . . . . . . . . . . . 18 (𝑦𝐻𝑦 ≤ ((𝑃 − 1) / 2))
201 nnz 9322 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ ℕ → 𝑦 ∈ ℤ)
20219, 20, 223syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃))
203202adantl 277 . . . . . . . . . . . . . . . . . . . . . . 23 ((2 ∥ 𝑦𝜑) → (𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃))
204201, 203anim12ci 339 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑦 ∈ ℕ ∧ (2 ∥ 𝑦𝜑)) → ((𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃) ∧ 𝑦 ∈ ℤ))
205 df-3an 982 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃𝑦 ∈ ℤ) ↔ ((𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃) ∧ 𝑦 ∈ ℤ))
206204, 205sylibr 134 . . . . . . . . . . . . . . . . . . . . 21 ((𝑦 ∈ ℕ ∧ (2 ∥ 𝑦𝜑)) → (𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃𝑦 ∈ ℤ))
207 ltoddhalfle 12008 . . . . . . . . . . . . . . . . . . . . 21 ((𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃𝑦 ∈ ℤ) → (𝑦 < (𝑃 / 2) ↔ 𝑦 ≤ ((𝑃 − 1) / 2)))
208206, 207syl 14 . . . . . . . . . . . . . . . . . . . 20 ((𝑦 ∈ ℕ ∧ (2 ∥ 𝑦𝜑)) → (𝑦 < (𝑃 / 2) ↔ 𝑦 ≤ ((𝑃 − 1) / 2)))
209208exbiri 382 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ ℕ → ((2 ∥ 𝑦𝜑) → (𝑦 ≤ ((𝑃 − 1) / 2) → 𝑦 < (𝑃 / 2))))
210209com23 78 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ ℕ → (𝑦 ≤ ((𝑃 − 1) / 2) → ((2 ∥ 𝑦𝜑) → 𝑦 < (𝑃 / 2))))
211200, 210biimtrid 152 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ℕ → (𝑦𝐻 → ((2 ∥ 𝑦𝜑) → 𝑦 < (𝑃 / 2))))
212211a1d 22 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℕ → (𝐻 ∈ ℕ → (𝑦𝐻 → ((2 ∥ 𝑦𝜑) → 𝑦 < (𝑃 / 2)))))
2132123imp 1195 . . . . . . . . . . . . . . 15 ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦𝐻) → ((2 ∥ 𝑦𝜑) → 𝑦 < (𝑃 / 2)))
214160, 213sylbi 121 . . . . . . . . . . . . . 14 (𝑦 ∈ (1...𝐻) → ((2 ∥ 𝑦𝜑) → 𝑦 < (𝑃 / 2)))
215214com12 30 . . . . . . . . . . . . 13 ((2 ∥ 𝑦𝜑) → (𝑦 ∈ (1...𝐻) → 𝑦 < (𝑃 / 2)))
2162153impia 1202 . . . . . . . . . . . 12 ((2 ∥ 𝑦𝜑𝑦 ∈ (1...𝐻)) → 𝑦 < (𝑃 / 2))
217199, 216eqbrtrd 4047 . . . . . . . . . . 11 ((2 ∥ 𝑦𝜑𝑦 ∈ (1...𝐻)) → ((𝑦 / 2) · 2) < (𝑃 / 2))
218217iftrued 3560 . . . . . . . . . 10 ((2 ∥ 𝑦𝜑𝑦 ∈ (1...𝐻)) → if(((𝑦 / 2) · 2) < (𝑃 / 2), ((𝑦 / 2) · 2), (𝑃 − ((𝑦 / 2) · 2))) = ((𝑦 / 2) · 2))
219218, 199eqtr2d 2223 . . . . . . . . 9 ((2 ∥ 𝑦𝜑𝑦 ∈ (1...𝐻)) → 𝑦 = if(((𝑦 / 2) · 2) < (𝑃 / 2), ((𝑦 / 2) · 2), (𝑃 − ((𝑦 / 2) · 2))))
220186, 192, 219rspcedvd 2866 . . . . . . . 8 ((2 ∥ 𝑦𝜑𝑦 ∈ (1...𝐻)) → ∃𝑥 ∈ (1...𝐻)𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))))
2212203expb 1206 . . . . . . 7 ((2 ∥ 𝑦 ∧ (𝜑𝑦 ∈ (1...𝐻))) → ∃𝑥 ∈ (1...𝐻)𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))))
222221ancoms 268 . . . . . 6 (((𝜑𝑦 ∈ (1...𝐻)) ∧ 2 ∥ 𝑦) → ∃𝑥 ∈ (1...𝐻)𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))))
22355, 56syl 14 . . . . . . . . . . . . . . . . . . 19 (𝑃 ∈ (ℙ ∖ {2}) → 𝑃 ∈ ℤ)
224223ad2antrr 488 . . . . . . . . . . . . . . . . . 18 (((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦𝐻)) → 𝑃 ∈ ℤ)
2252013ad2ant1 1020 . . . . . . . . . . . . . . . . . . 19 ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦𝐻) → 𝑦 ∈ ℤ)
226225adantl 277 . . . . . . . . . . . . . . . . . 18 (((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦𝐻)) → 𝑦 ∈ ℤ)
227224, 226zsubcld 9430 . . . . . . . . . . . . . . . . 17 (((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦𝐻)) → (𝑃𝑦) ∈ ℤ)
228166ad2antrl 490 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑃 ∈ ℝ ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ)) → 𝑦 ∈ ℝ)
22968rehalfcld 9215 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑃 ∈ ℝ → ((𝑃 − 1) / 2) ∈ ℝ)
230229adantr 276 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑃 ∈ ℝ ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ)) → ((𝑃 − 1) / 2) ∈ ℝ)
231 simpl 109 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑃 ∈ ℝ ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ)) → 𝑃 ∈ ℝ)
232228, 230, 2313jca 1179 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑃 ∈ ℝ ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ)) → (𝑦 ∈ ℝ ∧ ((𝑃 − 1) / 2) ∈ ℝ ∧ 𝑃 ∈ ℝ))
233232ex 115 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑃 ∈ ℝ → ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) → (𝑦 ∈ ℝ ∧ ((𝑃 − 1) / 2) ∈ ℝ ∧ 𝑃 ∈ ℝ)))
23455, 64, 2333syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑃 ∈ (ℙ ∖ {2}) → ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) → (𝑦 ∈ ℝ ∧ ((𝑃 − 1) / 2) ∈ ℝ ∧ 𝑃 ∈ ℝ)))
235234adantr 276 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) → ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) → (𝑦 ∈ ℝ ∧ ((𝑃 − 1) / 2) ∈ ℝ ∧ 𝑃 ∈ ℝ)))
236235impcom 125 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) ∧ (𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦)) → (𝑦 ∈ ℝ ∧ ((𝑃 − 1) / 2) ∈ ℝ ∧ 𝑃 ∈ ℝ))
237 lesub2 8462 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑦 ∈ ℝ ∧ ((𝑃 − 1) / 2) ∈ ℝ ∧ 𝑃 ∈ ℝ) → (𝑦 ≤ ((𝑃 − 1) / 2) ↔ (𝑃 − ((𝑃 − 1) / 2)) ≤ (𝑃𝑦)))
238236, 237syl 14 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) ∧ (𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦)) → (𝑦 ≤ ((𝑃 − 1) / 2) ↔ (𝑃 − ((𝑃 − 1) / 2)) ≤ (𝑃𝑦)))
23956zcnd 9426 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑃 ∈ ℙ → 𝑃 ∈ ℂ)
240 id 19 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑃 ∈ ℂ → 𝑃 ∈ ℂ)
241 1cnd 8021 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑃 ∈ ℂ → 1 ∈ ℂ)
242 2cnd 9041 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑃 ∈ ℂ → 2 ∈ ℂ)
243197a1i 9 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑃 ∈ ℂ → 2 # 0)
244240, 241, 242, 243divsubdirapd 8835 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑃 ∈ ℂ → ((𝑃 − 1) / 2) = ((𝑃 / 2) − (1 / 2)))
245244oveq2d 5922 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑃 ∈ ℂ → (𝑃 − ((𝑃 − 1) / 2)) = (𝑃 − ((𝑃 / 2) − (1 / 2))))
246 halfcl 9194 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑃 ∈ ℂ → (𝑃 / 2) ∈ ℂ)
247 halfcn 9182 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (1 / 2) ∈ ℂ
248247a1i 9 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑃 ∈ ℂ → (1 / 2) ∈ ℂ)
249240, 246, 248subsubd 8344 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑃 ∈ ℂ → (𝑃 − ((𝑃 / 2) − (1 / 2))) = ((𝑃 − (𝑃 / 2)) + (1 / 2)))
250112oveq1d 5921 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑃 ∈ ℂ → ((𝑃 − (𝑃 / 2)) + (1 / 2)) = ((𝑃 / 2) + (1 / 2)))
251245, 249, 2503eqtrd 2226 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑃 ∈ ℂ → (𝑃 − ((𝑃 − 1) / 2)) = ((𝑃 / 2) + (1 / 2)))
25255, 239, 2513syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑃 ∈ (ℙ ∖ {2}) → (𝑃 − ((𝑃 − 1) / 2)) = ((𝑃 / 2) + (1 / 2)))
253252ad2antrl 490 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) ∧ (𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦)) → (𝑃 − ((𝑃 − 1) / 2)) = ((𝑃 / 2) + (1 / 2)))
254253breq1d 4035 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) ∧ (𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦)) → ((𝑃 − ((𝑃 − 1) / 2)) ≤ (𝑃𝑦) ↔ ((𝑃 / 2) + (1 / 2)) ≤ (𝑃𝑦)))
255 prmnn 12222 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
256 halfre 9181 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (1 / 2) ∈ ℝ
257256a1i 9 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑃 ∈ ℕ → (1 / 2) ∈ ℝ)
258 nngt0 8993 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑃 ∈ ℕ → 0 < 𝑃)
25972a1i 9 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑃 ∈ ℕ → (2 ∈ ℝ ∧ 0 < 2))
260 divgt0 8877 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑃 ∈ ℝ ∧ 0 < 𝑃) ∧ (2 ∈ ℝ ∧ 0 < 2)) → 0 < (𝑃 / 2))
261100, 258, 259, 260syl21anc 1248 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑃 ∈ ℕ → 0 < (𝑃 / 2))
262 halfgt0 9183 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 0 < (1 / 2)
263262a1i 9 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑃 ∈ ℕ → 0 < (1 / 2))
264101, 257, 261, 263addgt0d 8526 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑃 ∈ ℕ → 0 < ((𝑃 / 2) + (1 / 2)))
26555, 255, 2643syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑃 ∈ (ℙ ∖ {2}) → 0 < ((𝑃 / 2) + (1 / 2)))
266265ad2antrl 490 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) ∧ (𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦)) → 0 < ((𝑃 / 2) + (1 / 2)))
267 0red 8006 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → 0 ∈ ℝ)
268 simpr 110 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → 𝑃 ∈ ℝ)
269268rehalfcld 9215 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → (𝑃 / 2) ∈ ℝ)
270256a1i 9 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → (1 / 2) ∈ ℝ)
271269, 270readdcld 8035 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → ((𝑃 / 2) + (1 / 2)) ∈ ℝ)
272 resubcl 8269 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑃 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑃𝑦) ∈ ℝ)
273272ancoms 268 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → (𝑃𝑦) ∈ ℝ)
274267, 271, 2733jca 1179 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → (0 ∈ ℝ ∧ ((𝑃 / 2) + (1 / 2)) ∈ ℝ ∧ (𝑃𝑦) ∈ ℝ))
275274ex 115 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑦 ∈ ℝ → (𝑃 ∈ ℝ → (0 ∈ ℝ ∧ ((𝑃 / 2) + (1 / 2)) ∈ ℝ ∧ (𝑃𝑦) ∈ ℝ)))
276166, 275syl 14 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑦 ∈ ℕ → (𝑃 ∈ ℝ → (0 ∈ ℝ ∧ ((𝑃 / 2) + (1 / 2)) ∈ ℝ ∧ (𝑃𝑦) ∈ ℝ)))
277276adantr 276 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) → (𝑃 ∈ ℝ → (0 ∈ ℝ ∧ ((𝑃 / 2) + (1 / 2)) ∈ ℝ ∧ (𝑃𝑦) ∈ ℝ)))
278277com12 30 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑃 ∈ ℝ → ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) → (0 ∈ ℝ ∧ ((𝑃 / 2) + (1 / 2)) ∈ ℝ ∧ (𝑃𝑦) ∈ ℝ)))
27955, 64, 2783syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑃 ∈ (ℙ ∖ {2}) → ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) → (0 ∈ ℝ ∧ ((𝑃 / 2) + (1 / 2)) ∈ ℝ ∧ (𝑃𝑦) ∈ ℝ)))
280279adantr 276 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) → ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) → (0 ∈ ℝ ∧ ((𝑃 / 2) + (1 / 2)) ∈ ℝ ∧ (𝑃𝑦) ∈ ℝ)))
281280impcom 125 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) ∧ (𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦)) → (0 ∈ ℝ ∧ ((𝑃 / 2) + (1 / 2)) ∈ ℝ ∧ (𝑃𝑦) ∈ ℝ))
282 ltletr 8095 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((0 ∈ ℝ ∧ ((𝑃 / 2) + (1 / 2)) ∈ ℝ ∧ (𝑃𝑦) ∈ ℝ) → ((0 < ((𝑃 / 2) + (1 / 2)) ∧ ((𝑃 / 2) + (1 / 2)) ≤ (𝑃𝑦)) → 0 < (𝑃𝑦)))
283281, 282syl 14 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) ∧ (𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦)) → ((0 < ((𝑃 / 2) + (1 / 2)) ∧ ((𝑃 / 2) + (1 / 2)) ≤ (𝑃𝑦)) → 0 < (𝑃𝑦)))
284266, 283mpand 429 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) ∧ (𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦)) → (((𝑃 / 2) + (1 / 2)) ≤ (𝑃𝑦) → 0 < (𝑃𝑦)))
285254, 284sylbid 150 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) ∧ (𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦)) → ((𝑃 − ((𝑃 − 1) / 2)) ≤ (𝑃𝑦) → 0 < (𝑃𝑦)))
286238, 285sylbid 150 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) ∧ (𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦)) → (𝑦 ≤ ((𝑃 − 1) / 2) → 0 < (𝑃𝑦)))
287286ex 115 . . . . . . . . . . . . . . . . . . . . 21 ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) → ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) → (𝑦 ≤ ((𝑃 − 1) / 2) → 0 < (𝑃𝑦))))
288287com23 78 . . . . . . . . . . . . . . . . . . . 20 ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) → (𝑦 ≤ ((𝑃 − 1) / 2) → ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) → 0 < (𝑃𝑦))))
289200, 288biimtrid 152 . . . . . . . . . . . . . . . . . . 19 ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) → (𝑦𝐻 → ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) → 0 < (𝑃𝑦))))
2902893impia 1202 . . . . . . . . . . . . . . . . . 18 ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦𝐻) → ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) → 0 < (𝑃𝑦)))
291290impcom 125 . . . . . . . . . . . . . . . . 17 (((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦𝐻)) → 0 < (𝑃𝑦))
292 elnnz 9313 . . . . . . . . . . . . . . . . 17 ((𝑃𝑦) ∈ ℕ ↔ ((𝑃𝑦) ∈ ℤ ∧ 0 < (𝑃𝑦)))
293227, 291, 292sylanbrc 417 . . . . . . . . . . . . . . . 16 (((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦𝐻)) → (𝑃𝑦) ∈ ℕ)
29423adantr 276 . . . . . . . . . . . . . . . . 17 ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) → (𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃))
295 simpr 110 . . . . . . . . . . . . . . . . . 18 ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) → ¬ 2 ∥ 𝑦)
296295, 225anim12ci 339 . . . . . . . . . . . . . . . . 17 (((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦𝐻)) → (𝑦 ∈ ℤ ∧ ¬ 2 ∥ 𝑦))
297 omoe 12011 . . . . . . . . . . . . . . . . 17 (((𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃) ∧ (𝑦 ∈ ℤ ∧ ¬ 2 ∥ 𝑦)) → 2 ∥ (𝑃𝑦))
298294, 296, 297syl2an2r 595 . . . . . . . . . . . . . . . 16 (((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦𝐻)) → 2 ∥ (𝑃𝑦))
299 nnehalf 12019 . . . . . . . . . . . . . . . 16 (((𝑃𝑦) ∈ ℕ ∧ 2 ∥ (𝑃𝑦)) → ((𝑃𝑦) / 2) ∈ ℕ)
300293, 298, 299syl2anc 411 . . . . . . . . . . . . . . 15 (((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦𝐻)) → ((𝑃𝑦) / 2) ∈ ℕ)
301 simpr2 1006 . . . . . . . . . . . . . . 15 (((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦𝐻)) → 𝐻 ∈ ℕ)
302 1red 8020 . . . . . . . . . . . . . . . . . 18 (((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦𝐻)) → 1 ∈ ℝ)
3031663ad2ant1 1020 . . . . . . . . . . . . . . . . . . 19 ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦𝐻) → 𝑦 ∈ ℝ)
304303adantl 277 . . . . . . . . . . . . . . . . . 18 (((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦𝐻)) → 𝑦 ∈ ℝ)
30555, 64syl 14 . . . . . . . . . . . . . . . . . . 19 (𝑃 ∈ (ℙ ∖ {2}) → 𝑃 ∈ ℝ)
306305ad2antrr 488 . . . . . . . . . . . . . . . . . 18 (((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦𝐻)) → 𝑃 ∈ ℝ)
307 nnge1 8991 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ ℕ → 1 ≤ 𝑦)
3083073ad2ant1 1020 . . . . . . . . . . . . . . . . . . 19 ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦𝐻) → 1 ≤ 𝑦)
309308adantl 277 . . . . . . . . . . . . . . . . . 18 (((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦𝐻)) → 1 ≤ 𝑦)
310302, 304, 306, 309lesub2dd 8567 . . . . . . . . . . . . . . . . 17 (((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦𝐻)) → (𝑃𝑦) ≤ (𝑃 − 1))
311306, 304resubcld 8386 . . . . . . . . . . . . . . . . . 18 (((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦𝐻)) → (𝑃𝑦) ∈ ℝ)
31255, 64, 683syl 17 . . . . . . . . . . . . . . . . . . 19 (𝑃 ∈ (ℙ ∖ {2}) → (𝑃 − 1) ∈ ℝ)
313312ad2antrr 488 . . . . . . . . . . . . . . . . . 18 (((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦𝐻)) → (𝑃 − 1) ∈ ℝ)
31472a1i 9 . . . . . . . . . . . . . . . . . 18 (((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦𝐻)) → (2 ∈ ℝ ∧ 0 < 2))
315 lediv1 8874 . . . . . . . . . . . . . . . . . 18 (((𝑃𝑦) ∈ ℝ ∧ (𝑃 − 1) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((𝑃𝑦) ≤ (𝑃 − 1) ↔ ((𝑃𝑦) / 2) ≤ ((𝑃 − 1) / 2)))
316311, 313, 314, 315syl3anc 1249 . . . . . . . . . . . . . . . . 17 (((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦𝐻)) → ((𝑃𝑦) ≤ (𝑃 − 1) ↔ ((𝑃𝑦) / 2) ≤ ((𝑃 − 1) / 2)))
317310, 316mpbid 147 . . . . . . . . . . . . . . . 16 (((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦𝐻)) → ((𝑃𝑦) / 2) ≤ ((𝑃 − 1) / 2))
31814breq2i 4033 . . . . . . . . . . . . . . . 16 (((𝑃𝑦) / 2) ≤ 𝐻 ↔ ((𝑃𝑦) / 2) ≤ ((𝑃 − 1) / 2))
319317, 318sylibr 134 . . . . . . . . . . . . . . 15 (((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦𝐻)) → ((𝑃𝑦) / 2) ≤ 𝐻)
320300, 301, 3193jca 1179 . . . . . . . . . . . . . 14 (((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦𝐻)) → (((𝑃𝑦) / 2) ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ ((𝑃𝑦) / 2) ≤ 𝐻))
321320ex 115 . . . . . . . . . . . . 13 ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) → ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦𝐻) → (((𝑃𝑦) / 2) ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ ((𝑃𝑦) / 2) ≤ 𝐻)))
322 elfz1b 10142 . . . . . . . . . . . . 13 (((𝑃𝑦) / 2) ∈ (1...𝐻) ↔ (((𝑃𝑦) / 2) ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ ((𝑃𝑦) / 2) ≤ 𝐻))
323321, 160, 3223imtr4g 205 . . . . . . . . . . . 12 ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) → (𝑦 ∈ (1...𝐻) → ((𝑃𝑦) / 2) ∈ (1...𝐻)))
324323ex 115 . . . . . . . . . . 11 (𝑃 ∈ (ℙ ∖ {2}) → (¬ 2 ∥ 𝑦 → (𝑦 ∈ (1...𝐻) → ((𝑃𝑦) / 2) ∈ (1...𝐻))))
32519, 324syl 14 . . . . . . . . . 10 (𝜑 → (¬ 2 ∥ 𝑦 → (𝑦 ∈ (1...𝐻) → ((𝑃𝑦) / 2) ∈ (1...𝐻))))
3263253imp21 1200 . . . . . . . . 9 ((¬ 2 ∥ 𝑦𝜑𝑦 ∈ (1...𝐻)) → ((𝑃𝑦) / 2) ∈ (1...𝐻))
327 oveq1 5913 . . . . . . . . . . . . 13 (𝑥 = ((𝑃𝑦) / 2) → (𝑥 · 2) = (((𝑃𝑦) / 2) · 2))
328327breq1d 4035 . . . . . . . . . . . 12 (𝑥 = ((𝑃𝑦) / 2) → ((𝑥 · 2) < (𝑃 / 2) ↔ (((𝑃𝑦) / 2) · 2) < (𝑃 / 2)))
329327oveq2d 5922 . . . . . . . . . . . 12 (𝑥 = ((𝑃𝑦) / 2) → (𝑃 − (𝑥 · 2)) = (𝑃 − (((𝑃𝑦) / 2) · 2)))
330328, 327, 329ifbieq12d 3579 . . . . . . . . . . 11 (𝑥 = ((𝑃𝑦) / 2) → if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) = if((((𝑃𝑦) / 2) · 2) < (𝑃 / 2), (((𝑃𝑦) / 2) · 2), (𝑃 − (((𝑃𝑦) / 2) · 2))))
331330eqeq2d 2201 . . . . . . . . . 10 (𝑥 = ((𝑃𝑦) / 2) → (𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) ↔ 𝑦 = if((((𝑃𝑦) / 2) · 2) < (𝑃 / 2), (((𝑃𝑦) / 2) · 2), (𝑃 − (((𝑃𝑦) / 2) · 2)))))
332331adantl 277 . . . . . . . . 9 (((¬ 2 ∥ 𝑦𝜑𝑦 ∈ (1...𝐻)) ∧ 𝑥 = ((𝑃𝑦) / 2)) → (𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) ↔ 𝑦 = if((((𝑃𝑦) / 2) · 2) < (𝑃 / 2), (((𝑃𝑦) / 2) · 2), (𝑃 − (((𝑃𝑦) / 2) · 2)))))
33319, 55, 2393syl 17 . . . . . . . . . . . . . . 15 (𝜑𝑃 ∈ ℂ)
3343333ad2ant2 1021 . . . . . . . . . . . . . 14 ((¬ 2 ∥ 𝑦𝜑𝑦 ∈ (1...𝐻)) → 𝑃 ∈ ℂ)
3351943ad2ant3 1022 . . . . . . . . . . . . . 14 ((¬ 2 ∥ 𝑦𝜑𝑦 ∈ (1...𝐻)) → 𝑦 ∈ ℂ)
336334, 335subcld 8316 . . . . . . . . . . . . 13 ((¬ 2 ∥ 𝑦𝜑𝑦 ∈ (1...𝐻)) → (𝑃𝑦) ∈ ℂ)
337 2cnd 9041 . . . . . . . . . . . . 13 ((¬ 2 ∥ 𝑦𝜑𝑦 ∈ (1...𝐻)) → 2 ∈ ℂ)
338197a1i 9 . . . . . . . . . . . . 13 ((¬ 2 ∥ 𝑦𝜑𝑦 ∈ (1...𝐻)) → 2 # 0)
339336, 337, 338divcanap1d 8796 . . . . . . . . . . . 12 ((¬ 2 ∥ 𝑦𝜑𝑦 ∈ (1...𝐻)) → (((𝑃𝑦) / 2) · 2) = (𝑃𝑦))
340 zre 9307 . . . . . . . . . . . . . . . . . . . . . 22 (𝑃 ∈ ℤ → 𝑃 ∈ ℝ)
341 halfge0 9184 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 0 ≤ (1 / 2)
342 rehalfcl 9195 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑃 ∈ ℝ → (𝑃 / 2) ∈ ℝ)
343342adantl 277 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → (𝑃 / 2) ∈ ℝ)
344343, 270subge02d 8542 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → (0 ≤ (1 / 2) ↔ ((𝑃 / 2) − (1 / 2)) ≤ (𝑃 / 2)))
345341, 344mpbii 148 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → ((𝑃 / 2) − (1 / 2)) ≤ (𝑃 / 2))
346 simpl 109 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → 𝑦 ∈ ℝ)
347256a1i 9 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑃 ∈ ℝ → (1 / 2) ∈ ℝ)
348342, 347resubcld 8386 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑃 ∈ ℝ → ((𝑃 / 2) − (1 / 2)) ∈ ℝ)
349348adantl 277 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → ((𝑃 / 2) − (1 / 2)) ∈ ℝ)
350 letr 8088 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑦 ∈ ℝ ∧ ((𝑃 / 2) − (1 / 2)) ∈ ℝ ∧ (𝑃 / 2) ∈ ℝ) → ((𝑦 ≤ ((𝑃 / 2) − (1 / 2)) ∧ ((𝑃 / 2) − (1 / 2)) ≤ (𝑃 / 2)) → 𝑦 ≤ (𝑃 / 2)))
351346, 349, 343, 350syl3anc 1249 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → ((𝑦 ≤ ((𝑃 / 2) − (1 / 2)) ∧ ((𝑃 / 2) − (1 / 2)) ≤ (𝑃 / 2)) → 𝑦 ≤ (𝑃 / 2)))
352345, 351mpan2d 428 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → (𝑦 ≤ ((𝑃 / 2) − (1 / 2)) → 𝑦 ≤ (𝑃 / 2)))
35381adantl 277 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → 𝑃 ∈ ℂ)
354353, 244syl 14 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → ((𝑃 − 1) / 2) = ((𝑃 / 2) − (1 / 2)))
355354breq2d 4037 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → (𝑦 ≤ ((𝑃 − 1) / 2) ↔ 𝑦 ≤ ((𝑃 / 2) − (1 / 2))))
356 lesub 8446 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝑃 / 2) ∈ ℝ ∧ 𝑃 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((𝑃 / 2) ≤ (𝑃𝑦) ↔ 𝑦 ≤ (𝑃 − (𝑃 / 2))))
357343, 268, 346, 356syl3anc 1249 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → ((𝑃 / 2) ≤ (𝑃𝑦) ↔ 𝑦 ≤ (𝑃 − (𝑃 / 2))))
358269, 273lenltd 8123 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → ((𝑃 / 2) ≤ (𝑃𝑦) ↔ ¬ (𝑃𝑦) < (𝑃 / 2)))
359 2cnd 9041 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑃 ∈ ℝ → 2 ∈ ℂ)
360197a1i 9 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑃 ∈ ℝ → 2 # 0)
36181, 359, 360divcanap1d 8796 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑃 ∈ ℝ → ((𝑃 / 2) · 2) = 𝑃)
362361eqcomd 2195 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑃 ∈ ℝ → 𝑃 = ((𝑃 / 2) · 2))
363362oveq1d 5921 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑃 ∈ ℝ → (𝑃 − (𝑃 / 2)) = (((𝑃 / 2) · 2) − (𝑃 / 2)))
364342recnd 8034 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑃 ∈ ℝ → (𝑃 / 2) ∈ ℂ)
365364, 359mulcomd 8027 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑃 ∈ ℝ → ((𝑃 / 2) · 2) = (2 · (𝑃 / 2)))
366365oveq1d 5921 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑃 ∈ ℝ → (((𝑃 / 2) · 2) − (𝑃 / 2)) = ((2 · (𝑃 / 2)) − (𝑃 / 2)))
367359, 364mulsubfacd 8423 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑃 ∈ ℝ → ((2 · (𝑃 / 2)) − (𝑃 / 2)) = ((2 − 1) · (𝑃 / 2)))
368 2m1e1 9086 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (2 − 1) = 1
369368a1i 9 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑃 ∈ ℝ → (2 − 1) = 1)
370369oveq1d 5921 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑃 ∈ ℝ → ((2 − 1) · (𝑃 / 2)) = (1 · (𝑃 / 2)))
371364mullidd 8023 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑃 ∈ ℝ → (1 · (𝑃 / 2)) = (𝑃 / 2))
372367, 370, 3713eqtrd 2226 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑃 ∈ ℝ → ((2 · (𝑃 / 2)) − (𝑃 / 2)) = (𝑃 / 2))
373363, 366, 3723eqtrd 2226 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑃 ∈ ℝ → (𝑃 − (𝑃 / 2)) = (𝑃 / 2))
374373adantl 277 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → (𝑃 − (𝑃 / 2)) = (𝑃 / 2))
375374breq2d 4037 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → (𝑦 ≤ (𝑃 − (𝑃 / 2)) ↔ 𝑦 ≤ (𝑃 / 2)))
376357, 358, 3753bitr3d 218 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → (¬ (𝑃𝑦) < (𝑃 / 2) ↔ 𝑦 ≤ (𝑃 / 2)))
377352, 355, 3763imtr4d 203 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → (𝑦 ≤ ((𝑃 − 1) / 2) → ¬ (𝑃𝑦) < (𝑃 / 2)))
378377ex 115 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 ∈ ℝ → (𝑃 ∈ ℝ → (𝑦 ≤ ((𝑃 − 1) / 2) → ¬ (𝑃𝑦) < (𝑃 / 2))))
379166, 378syl 14 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ ℕ → (𝑃 ∈ ℝ → (𝑦 ≤ ((𝑃 − 1) / 2) → ¬ (𝑃𝑦) < (𝑃 / 2))))
380379com3l 81 . . . . . . . . . . . . . . . . . . . . . 22 (𝑃 ∈ ℝ → (𝑦 ≤ ((𝑃 − 1) / 2) → (𝑦 ∈ ℕ → ¬ (𝑃𝑦) < (𝑃 / 2))))
381340, 380syl 14 . . . . . . . . . . . . . . . . . . . . 21 (𝑃 ∈ ℤ → (𝑦 ≤ ((𝑃 − 1) / 2) → (𝑦 ∈ ℕ → ¬ (𝑃𝑦) < (𝑃 / 2))))
38219, 55, 56, 3814syl 18 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑦 ≤ ((𝑃 − 1) / 2) → (𝑦 ∈ ℕ → ¬ (𝑃𝑦) < (𝑃 / 2))))
383382adantl 277 . . . . . . . . . . . . . . . . . . 19 ((¬ 2 ∥ 𝑦𝜑) → (𝑦 ≤ ((𝑃 − 1) / 2) → (𝑦 ∈ ℕ → ¬ (𝑃𝑦) < (𝑃 / 2))))
384383com13 80 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ ℕ → (𝑦 ≤ ((𝑃 − 1) / 2) → ((¬ 2 ∥ 𝑦𝜑) → ¬ (𝑃𝑦) < (𝑃 / 2))))
385200, 384biimtrid 152 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ℕ → (𝑦𝐻 → ((¬ 2 ∥ 𝑦𝜑) → ¬ (𝑃𝑦) < (𝑃 / 2))))
386385a1d 22 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℕ → (𝐻 ∈ ℕ → (𝑦𝐻 → ((¬ 2 ∥ 𝑦𝜑) → ¬ (𝑃𝑦) < (𝑃 / 2)))))
3873863imp 1195 . . . . . . . . . . . . . . 15 ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦𝐻) → ((¬ 2 ∥ 𝑦𝜑) → ¬ (𝑃𝑦) < (𝑃 / 2)))
388387com12 30 . . . . . . . . . . . . . 14 ((¬ 2 ∥ 𝑦𝜑) → ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦𝐻) → ¬ (𝑃𝑦) < (𝑃 / 2)))
389160, 388biimtrid 152 . . . . . . . . . . . . 13 ((¬ 2 ∥ 𝑦𝜑) → (𝑦 ∈ (1...𝐻) → ¬ (𝑃𝑦) < (𝑃 / 2)))
3903893impia 1202 . . . . . . . . . . . 12 ((¬ 2 ∥ 𝑦𝜑𝑦 ∈ (1...𝐻)) → ¬ (𝑃𝑦) < (𝑃 / 2))
391339, 390eqnbrtrd 4043 . . . . . . . . . . 11 ((¬ 2 ∥ 𝑦𝜑𝑦 ∈ (1...𝐻)) → ¬ (((𝑃𝑦) / 2) · 2) < (𝑃 / 2))
392391iffalsed 3563 . . . . . . . . . 10 ((¬ 2 ∥ 𝑦𝜑𝑦 ∈ (1...𝐻)) → if((((𝑃𝑦) / 2) · 2) < (𝑃 / 2), (((𝑃𝑦) / 2) · 2), (𝑃 − (((𝑃𝑦) / 2) · 2))) = (𝑃 − (((𝑃𝑦) / 2) · 2)))
393339oveq2d 5922 . . . . . . . . . 10 ((¬ 2 ∥ 𝑦𝜑𝑦 ∈ (1...𝐻)) → (𝑃 − (((𝑃𝑦) / 2) · 2)) = (𝑃 − (𝑃𝑦)))
394333, 194anim12i 338 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ (1...𝐻)) → (𝑃 ∈ ℂ ∧ 𝑦 ∈ ℂ))
3953943adant1 1017 . . . . . . . . . . 11 ((¬ 2 ∥ 𝑦𝜑𝑦 ∈ (1...𝐻)) → (𝑃 ∈ ℂ ∧ 𝑦 ∈ ℂ))
396 nncan 8234 . . . . . . . . . . 11 ((𝑃 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑃 − (𝑃𝑦)) = 𝑦)
397395, 396syl 14 . . . . . . . . . 10 ((¬ 2 ∥ 𝑦𝜑𝑦 ∈ (1...𝐻)) → (𝑃 − (𝑃𝑦)) = 𝑦)
398392, 393, 3973eqtrrd 2227 . . . . . . . . 9 ((¬ 2 ∥ 𝑦𝜑𝑦 ∈ (1...𝐻)) → 𝑦 = if((((𝑃𝑦) / 2) · 2) < (𝑃 / 2), (((𝑃𝑦) / 2) · 2), (𝑃 − (((𝑃𝑦) / 2) · 2))))
399326, 332, 398rspcedvd 2866 . . . . . . . 8 ((¬ 2 ∥ 𝑦𝜑𝑦 ∈ (1...𝐻)) → ∃𝑥 ∈ (1...𝐻)𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))))
4003993expb 1206 . . . . . . 7 ((¬ 2 ∥ 𝑦 ∧ (𝜑𝑦 ∈ (1...𝐻))) → ∃𝑥 ∈ (1...𝐻)𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))))
401400ancoms 268 . . . . . 6 (((𝜑𝑦 ∈ (1...𝐻)) ∧ ¬ 2 ∥ 𝑦) → ∃𝑥 ∈ (1...𝐻)𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))))
4029a1i 9 . . . . . . . 8 ((𝜑𝑦 ∈ (1...𝐻)) → 2 ∈ ℕ)
403193adantl 277 . . . . . . . 8 ((𝜑𝑦 ∈ (1...𝐻)) → 𝑦 ∈ ℤ)
404 dvdsdc 11915 . . . . . . . 8 ((2 ∈ ℕ ∧ 𝑦 ∈ ℤ) → DECID 2 ∥ 𝑦)
405402, 403, 404syl2anc 411 . . . . . . 7 ((𝜑𝑦 ∈ (1...𝐻)) → DECID 2 ∥ 𝑦)
406 exmiddc 837 . . . . . . 7 (DECID 2 ∥ 𝑦 → (2 ∥ 𝑦 ∨ ¬ 2 ∥ 𝑦))
407405, 406syl 14 . . . . . 6 ((𝜑𝑦 ∈ (1...𝐻)) → (2 ∥ 𝑦 ∨ ¬ 2 ∥ 𝑦))
408222, 401, 407mpjaodan 799 . . . . 5 ((𝜑𝑦 ∈ (1...𝐻)) → ∃𝑥 ∈ (1...𝐻)𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))))
409408ex 115 . . . 4 (𝜑 → (𝑦 ∈ (1...𝐻) → ∃𝑥 ∈ (1...𝐻)𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2)))))
410159, 409impbid 129 . . 3 (𝜑 → (∃𝑥 ∈ (1...𝐻)𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) ↔ 𝑦 ∈ (1...𝐻)))
4113, 410bitrid 192 . 2 (𝜑 → (𝑦 ∈ ran 𝑅𝑦 ∈ (1...𝐻)))
412411eqrdv 2187 1 (𝜑 → ran 𝑅 = (1...𝐻))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 104  wb 105  wo 709  DECID wdc 835  w3a 980   = wceq 1364  wcel 2160  wrex 2469  Vcvv 2756  cdif 3146  ifcif 3553  {csn 3614   class class class wbr 4025  cmpt 4086  ran crn 4652  (class class class)co 5906  cc 7856  cr 7857  0cc0 7858  1c1 7859   + caddc 7861   · cmul 7863   < clt 8040  cle 8041  cmin 8176   # cap 8586   / cdiv 8677  cn 8968  2c2 9019  cz 9303  cq 9670  +crp 9705  ...cfz 10060  cdvds 11904  cprime 12219
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-13 2162  ax-14 2163  ax-ext 2171  ax-coll 4140  ax-sep 4143  ax-nul 4151  ax-pow 4199  ax-pr 4234  ax-un 4458  ax-setind 4561  ax-iinf 4612  ax-cnex 7949  ax-resscn 7950  ax-1cn 7951  ax-1re 7952  ax-icn 7953  ax-addcl 7954  ax-addrcl 7955  ax-mulcl 7956  ax-mulrcl 7957  ax-addcom 7958  ax-mulcom 7959  ax-addass 7960  ax-mulass 7961  ax-distr 7962  ax-i2m1 7963  ax-0lt1 7964  ax-1rid 7965  ax-0id 7966  ax-rnegex 7967  ax-precex 7968  ax-cnre 7969  ax-pre-ltirr 7970  ax-pre-ltwlin 7971  ax-pre-lttrn 7972  ax-pre-apti 7973  ax-pre-ltadd 7974  ax-pre-mulgt0 7975  ax-pre-mulext 7976  ax-arch 7977  ax-caucvg 7978
This theorem depends on definitions:  df-bi 117  df-dc 836  df-3or 981  df-3an 982  df-tru 1367  df-fal 1370  df-xor 1387  df-nf 1472  df-sb 1774  df-eu 2041  df-mo 2042  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-ne 2361  df-nel 2456  df-ral 2473  df-rex 2474  df-reu 2475  df-rmo 2476  df-rab 2477  df-v 2758  df-sbc 2982  df-csb 3077  df-dif 3151  df-un 3153  df-in 3155  df-ss 3162  df-nul 3443  df-if 3554  df-pw 3599  df-sn 3620  df-pr 3621  df-op 3623  df-uni 3832  df-int 3867  df-iun 3910  df-br 4026  df-opab 4087  df-mpt 4088  df-tr 4124  df-id 4318  df-po 4321  df-iso 4322  df-iord 4391  df-on 4393  df-ilim 4394  df-suc 4396  df-iom 4615  df-xp 4657  df-rel 4658  df-cnv 4659  df-co 4660  df-dm 4661  df-rn 4662  df-res 4663  df-ima 4664  df-iota 5203  df-fun 5244  df-fn 5245  df-f 5246  df-f1 5247  df-fo 5248  df-f1o 5249  df-fv 5250  df-riota 5861  df-ov 5909  df-oprab 5910  df-mpo 5911  df-1st 6180  df-2nd 6181  df-recs 6345  df-frec 6431  df-1o 6456  df-2o 6457  df-er 6574  df-en 6782  df-pnf 8042  df-mnf 8043  df-xr 8044  df-ltxr 8045  df-le 8046  df-sub 8178  df-neg 8179  df-reap 8580  df-ap 8587  df-div 8678  df-inn 8969  df-2 9027  df-3 9028  df-4 9029  df-n0 9227  df-z 9304  df-uz 9579  df-q 9671  df-rp 9706  df-ioo 9944  df-fz 10061  df-fl 10325  df-mod 10380  df-seqfrec 10505  df-exp 10584  df-cj 10960  df-re 10961  df-im 10962  df-rsqrt 11116  df-abs 11117  df-dvds 11905  df-prm 12220
This theorem is referenced by:  gausslemma2dlem1f1o  15104
  Copyright terms: Public domain W3C validator