Theorem gausslemma2dlem1a 25381

Description: Lemma for gausslemma2dlem1 25382. (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.

Step	Hyp	Ref	Expression
1		vex 3353	. . . 4 ⊢ 𝑦 ∈ V
2		gausslemma2d.r	. . . . 5 ⊢ 𝑅 = (𝑥 ∈ (1...𝐻) ↦ if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))))
3	2	elrnmpt 5541	. . . 4 ⊢ (𝑦 ∈ V → (𝑦 ∈ ran 𝑅 ↔ ∃𝑥 ∈ (1...𝐻)𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2)))))
4	1, 3	ax-mp 5	. . 3 ⊢ (𝑦 ∈ ran 𝑅 ↔ ∃𝑥 ∈ (1...𝐻)𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))))
5		iftrue 4249	. . . . . . . . 9 ⊢ ((𝑥 · 2) < (𝑃 / 2) → if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) = (𝑥 · 2))
6	5	eqeq2d 2775	. . . . . . . 8 ⊢ ((𝑥 · 2) < (𝑃 / 2) → (𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) ↔ 𝑦 = (𝑥 · 2)))
7	6	adantr 472	. . . . . . 7 ⊢ (((𝑥 · 2) < (𝑃 / 2) ∧ (𝜑 ∧ 𝑥 ∈ (1...𝐻))) → (𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) ↔ 𝑦 = (𝑥 · 2)))
8		elfz1b 12616	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (1...𝐻) ↔ (𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻))
9		id 22	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ℕ → 𝑥 ∈ ℕ)
10		2nn 11345	. . . . . . . . . . . . . . . . . 18 ⊢ 2 ∈ ℕ
11	10	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ℕ → 2 ∈ ℕ)
12	9, 11	nnmulcld 11325	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℕ → (𝑥 · 2) ∈ ℕ)
13	12	3ad2ant1 1163	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻) → (𝑥 · 2) ∈ ℕ)
14	13	3ad2ant1 1163	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻) ∧ 𝜑 ∧ (𝑥 · 2) < (𝑃 / 2)) → (𝑥 · 2) ∈ ℕ)
15		gausslemma2d.h	. . . . . . . . . . . . . . . . . 18 ⊢ 𝐻 = ((𝑃 − 1) / 2)
16	15	eleq1i 2835	. . . . . . . . . . . . . . . . 17 ⊢ (𝐻 ∈ ℕ ↔ ((𝑃 − 1) / 2) ∈ ℕ)
17	16	biimpi 207	. . . . . . . . . . . . . . . 16 ⊢ (𝐻 ∈ ℕ → ((𝑃 − 1) / 2) ∈ ℕ)
18	17	3ad2ant2 1164	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻) → ((𝑃 − 1) / 2) ∈ ℕ)
19	18	3ad2ant1 1163	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻) ∧ 𝜑 ∧ (𝑥 · 2) < (𝑃 / 2)) → ((𝑃 − 1) / 2) ∈ ℕ)
20		gausslemma2d.p	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2}))
21		nnoddn2prm 15797	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃))
22		nnz 11646	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑃 ∈ ℕ → 𝑃 ∈ ℤ)
23	22	anim1i 608	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) → (𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃))
24	21, 23	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃))
25		nnz 11646	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 ∈ ℕ → 𝑥 ∈ ℤ)
26		2z 11656	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 2 ∈ ℤ
27	26	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 ∈ ℕ → 2 ∈ ℤ)
28	25, 27	zmulcld 11735	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ ℕ → (𝑥 · 2) ∈ ℤ)
29	28	3ad2ant1 1163	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻) → (𝑥 · 2) ∈ ℤ)
30	24, 29	anim12i 606	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ (𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻)) → ((𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃) ∧ (𝑥 · 2) ∈ ℤ))
31		df-3an 1109	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ∧ (𝑥 · 2) ∈ ℤ) ↔ ((𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃) ∧ (𝑥 · 2) ∈ ℤ))
32	30, 31	sylibr 225	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ (𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻)) → (𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ∧ (𝑥 · 2) ∈ ℤ))
33	32	ex 401	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → ((𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻) → (𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ∧ (𝑥 · 2) ∈ ℤ)))
34	20, 33	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻) → (𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ∧ (𝑥 · 2) ∈ ℤ)))
35	34	impcom 396	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻) ∧ 𝜑) → (𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ∧ (𝑥 · 2) ∈ ℤ))
36		ltoddhalfle 15369	. . . . . . . . . . . . . . . 16 ⊢ ((𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ∧ (𝑥 · 2) ∈ ℤ) → ((𝑥 · 2) < (𝑃 / 2) ↔ (𝑥 · 2) ≤ ((𝑃 − 1) / 2)))
37	35, 36	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻) ∧ 𝜑) → ((𝑥 · 2) < (𝑃 / 2) ↔ (𝑥 · 2) ≤ ((𝑃 − 1) / 2)))
38	37	biimp3a 1593	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻) ∧ 𝜑 ∧ (𝑥 · 2) < (𝑃 / 2)) → (𝑥 · 2) ≤ ((𝑃 − 1) / 2))
39	14, 19, 38	3jca 1158	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻) ∧ 𝜑 ∧ (𝑥 · 2) < (𝑃 / 2)) → ((𝑥 · 2) ∈ ℕ ∧ ((𝑃 − 1) / 2) ∈ ℕ ∧ (𝑥 · 2) ≤ ((𝑃 − 1) / 2)))
40	39	3exp 1148	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻) → (𝜑 → ((𝑥 · 2) < (𝑃 / 2) → ((𝑥 · 2) ∈ ℕ ∧ ((𝑃 − 1) / 2) ∈ ℕ ∧ (𝑥 · 2) ≤ ((𝑃 − 1) / 2)))))
41	8, 40	sylbi 208	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (1...𝐻) → (𝜑 → ((𝑥 · 2) < (𝑃 / 2) → ((𝑥 · 2) ∈ ℕ ∧ ((𝑃 − 1) / 2) ∈ ℕ ∧ (𝑥 · 2) ≤ ((𝑃 − 1) / 2)))))
42	41	impcom 396	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝐻)) → ((𝑥 · 2) < (𝑃 / 2) → ((𝑥 · 2) ∈ ℕ ∧ ((𝑃 − 1) / 2) ∈ ℕ ∧ (𝑥 · 2) ≤ ((𝑃 − 1) / 2))))
43	42	impcom 396	. . . . . . . . 9 ⊢ (((𝑥 · 2) < (𝑃 / 2) ∧ (𝜑 ∧ 𝑥 ∈ (1...𝐻))) → ((𝑥 · 2) ∈ ℕ ∧ ((𝑃 − 1) / 2) ∈ ℕ ∧ (𝑥 · 2) ≤ ((𝑃 − 1) / 2)))
44	15	oveq2i 6853	. . . . . . . . . . 11 ⊢ (1...𝐻) = (1...((𝑃 − 1) / 2))
45	44	eleq2i 2836	. . . . . . . . . 10 ⊢ ((𝑥 · 2) ∈ (1...𝐻) ↔ (𝑥 · 2) ∈ (1...((𝑃 − 1) / 2)))
46		elfz1b 12616	. . . . . . . . . 10 ⊢ ((𝑥 · 2) ∈ (1...((𝑃 − 1) / 2)) ↔ ((𝑥 · 2) ∈ ℕ ∧ ((𝑃 − 1) / 2) ∈ ℕ ∧ (𝑥 · 2) ≤ ((𝑃 − 1) / 2)))
47	45, 46	bitri 266	. . . . . . . . 9 ⊢ ((𝑥 · 2) ∈ (1...𝐻) ↔ ((𝑥 · 2) ∈ ℕ ∧ ((𝑃 − 1) / 2) ∈ ℕ ∧ (𝑥 · 2) ≤ ((𝑃 − 1) / 2)))
48	43, 47	sylibr 225	. . . . . . . 8 ⊢ (((𝑥 · 2) < (𝑃 / 2) ∧ (𝜑 ∧ 𝑥 ∈ (1...𝐻))) → (𝑥 · 2) ∈ (1...𝐻))
49		eleq1 2832	. . . . . . . 8 ⊢ (𝑦 = (𝑥 · 2) → (𝑦 ∈ (1...𝐻) ↔ (𝑥 · 2) ∈ (1...𝐻)))
50	48, 49	syl5ibrcom 238	. . . . . . 7 ⊢ (((𝑥 · 2) < (𝑃 / 2) ∧ (𝜑 ∧ 𝑥 ∈ (1...𝐻))) → (𝑦 = (𝑥 · 2) → 𝑦 ∈ (1...𝐻)))
51	7, 50	sylbid 231	. . . . . 6 ⊢ (((𝑥 · 2) < (𝑃 / 2) ∧ (𝜑 ∧ 𝑥 ∈ (1...𝐻))) → (𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) → 𝑦 ∈ (1...𝐻)))
52		iffalse 4252	. . . . . . . . 9 ⊢ (¬ (𝑥 · 2) < (𝑃 / 2) → if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) = (𝑃 − (𝑥 · 2)))
53	52	eqeq2d 2775	. . . . . . . 8 ⊢ (¬ (𝑥 · 2) < (𝑃 / 2) → (𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) ↔ 𝑦 = (𝑃 − (𝑥 · 2))))
54	53	adantr 472	. . . . . . 7 ⊢ ((¬ (𝑥 · 2) < (𝑃 / 2) ∧ (𝜑 ∧ 𝑥 ∈ (1...𝐻))) → (𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) ↔ 𝑦 = (𝑃 − (𝑥 · 2))))
55		eldifi 3894	. . . . . . . . . . . . 13 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 𝑃 ∈ ℙ)
56		prmz 15671	. . . . . . . . . . . . 13 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℤ)
57	20, 55, 56	3syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑃 ∈ ℤ)
58	57	ad2antrl 719	. . . . . . . . . . 11 ⊢ ((¬ (𝑥 · 2) < (𝑃 / 2) ∧ (𝜑 ∧ 𝑥 ∈ (1...𝐻))) → 𝑃 ∈ ℤ)
59		elfzelz 12549	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (1...𝐻) → 𝑥 ∈ ℤ)
60	26	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (1...𝐻) → 2 ∈ ℤ)
61	59, 60	zmulcld 11735	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (1...𝐻) → (𝑥 · 2) ∈ ℤ)
62	61	ad2antll 720	. . . . . . . . . . 11 ⊢ ((¬ (𝑥 · 2) < (𝑃 / 2) ∧ (𝜑 ∧ 𝑥 ∈ (1...𝐻))) → (𝑥 · 2) ∈ ℤ)
63	58, 62	zsubcld 11734	. . . . . . . . . 10 ⊢ ((¬ (𝑥 · 2) < (𝑃 / 2) ∧ (𝜑 ∧ 𝑥 ∈ (1...𝐻))) → (𝑃 − (𝑥 · 2)) ∈ ℤ)
64	56	zred 11729	. . . . . . . . . . . . . 14 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℝ)
65		nnre 11282	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ ℕ → 𝑥 ∈ ℝ)
66	65	adantr 472	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ) → 𝑥 ∈ ℝ)
67		peano2rem 10602	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑃 ∈ ℝ → (𝑃 − 1) ∈ ℝ)
68	67	adantl 473	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ) → (𝑃 − 1) ∈ ℝ)
69		2re 11346	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 2 ∈ ℝ
70		2pos 11382	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 0 < 2
71	69, 70	pm3.2i 462	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (2 ∈ ℝ ∧ 0 < 2)
72	71	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ) → (2 ∈ ℝ ∧ 0 < 2))
73		lemuldiv 11157	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ ℝ ∧ (𝑃 − 1) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((𝑥 · 2) ≤ (𝑃 − 1) ↔ 𝑥 ≤ ((𝑃 − 1) / 2)))
74	66, 68, 72, 73	syl3anc 1490	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ) → ((𝑥 · 2) ≤ (𝑃 − 1) ↔ 𝑥 ≤ ((𝑃 − 1) / 2)))
75	15	breq2i 4817	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ≤ 𝐻 ↔ 𝑥 ≤ ((𝑃 − 1) / 2))
76	74, 75	syl6rbbr 281	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ) → (𝑥 ≤ 𝐻 ↔ (𝑥 · 2) ≤ (𝑃 − 1)))
77	12	nnred 11291	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ ℕ → (𝑥 · 2) ∈ ℝ)
78	77	adantr 472	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ) → (𝑥 · 2) ∈ ℝ)
79		simpr 477	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ) → 𝑃 ∈ ℝ)
80	78, 68, 79	lesub2d 10889	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ) → ((𝑥 · 2) ≤ (𝑃 − 1) ↔ (𝑃 − (𝑃 − 1)) ≤ (𝑃 − (𝑥 · 2))))
81		recn 10279	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑃 ∈ ℝ → 𝑃 ∈ ℂ)
82		1cnd 10288	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑃 ∈ ℝ → 1 ∈ ℂ)
83	81, 82	nncand 10651	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑃 ∈ ℝ → (𝑃 − (𝑃 − 1)) = 1)
84	83	adantl 473	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ) → (𝑃 − (𝑃 − 1)) = 1)
85	84	breq1d 4819	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ) → ((𝑃 − (𝑃 − 1)) ≤ (𝑃 − (𝑥 · 2)) ↔ 1 ≤ (𝑃 − (𝑥 · 2))))
86	85	biimpd 220	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ) → ((𝑃 − (𝑃 − 1)) ≤ (𝑃 − (𝑥 · 2)) → 1 ≤ (𝑃 − (𝑥 · 2))))
87	80, 86	sylbid 231	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ) → ((𝑥 · 2) ≤ (𝑃 − 1) → 1 ≤ (𝑃 − (𝑥 · 2))))
88	76, 87	sylbid 231	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ) → (𝑥 ≤ 𝐻 → 1 ≤ (𝑃 − (𝑥 · 2))))
89	88	impancom 443	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℕ ∧ 𝑥 ≤ 𝐻) → (𝑃 ∈ ℝ → 1 ≤ (𝑃 − (𝑥 · 2))))
90	89	3adant2 1161	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻) → (𝑃 ∈ ℝ → 1 ≤ (𝑃 − (𝑥 · 2))))
91	8, 90	sylbi 208	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (1...𝐻) → (𝑃 ∈ ℝ → 1 ≤ (𝑃 − (𝑥 · 2))))
92	91	com12 32	. . . . . . . . . . . . . 14 ⊢ (𝑃 ∈ ℝ → (𝑥 ∈ (1...𝐻) → 1 ≤ (𝑃 − (𝑥 · 2))))
93	64, 92	syl 17	. . . . . . . . . . . . 13 ⊢ (𝑃 ∈ ℙ → (𝑥 ∈ (1...𝐻) → 1 ≤ (𝑃 − (𝑥 · 2))))
94	20, 55, 93	3syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑥 ∈ (1...𝐻) → 1 ≤ (𝑃 − (𝑥 · 2))))
95	94	imp 395	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝐻)) → 1 ≤ (𝑃 − (𝑥 · 2)))
96	95	adantl 473	. . . . . . . . . 10 ⊢ ((¬ (𝑥 · 2) < (𝑃 / 2) ∧ (𝜑 ∧ 𝑥 ∈ (1...𝐻))) → 1 ≤ (𝑃 − (𝑥 · 2)))
97		elnnz1 11650	. . . . . . . . . 10 ⊢ ((𝑃 − (𝑥 · 2)) ∈ ℕ ↔ ((𝑃 − (𝑥 · 2)) ∈ ℤ ∧ 1 ≤ (𝑃 − (𝑥 · 2))))
98	63, 96, 97	sylanbrc 578	. . . . . . . . 9 ⊢ ((¬ (𝑥 · 2) < (𝑃 / 2) ∧ (𝜑 ∧ 𝑥 ∈ (1...𝐻))) → (𝑃 − (𝑥 · 2)) ∈ ℕ)
99	8	simp2bi 1176	. . . . . . . . . 10 ⊢ (𝑥 ∈ (1...𝐻) → 𝐻 ∈ ℕ)
100	99	ad2antll 720	. . . . . . . . 9 ⊢ ((¬ (𝑥 · 2) < (𝑃 / 2) ∧ (𝜑 ∧ 𝑥 ∈ (1...𝐻))) → 𝐻 ∈ ℕ)
101		nnre 11282	. . . . . . . . . . . . . . . . 17 ⊢ (𝑃 ∈ ℕ → 𝑃 ∈ ℝ)
102	101	rehalfcld 11525	. . . . . . . . . . . . . . . 16 ⊢ (𝑃 ∈ ℕ → (𝑃 / 2) ∈ ℝ)
103	102	adantr 472	. . . . . . . . . . . . . . 15 ⊢ ((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) → (𝑃 / 2) ∈ ℝ)
104	61	zred 11729	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (1...𝐻) → (𝑥 · 2) ∈ ℝ)
105		lenlt 10370	. . . . . . . . . . . . . . 15 ⊢ (((𝑃 / 2) ∈ ℝ ∧ (𝑥 · 2) ∈ ℝ) → ((𝑃 / 2) ≤ (𝑥 · 2) ↔ ¬ (𝑥 · 2) < (𝑃 / 2)))
106	103, 104, 105	syl2an 589	. . . . . . . . . . . . . 14 ⊢ (((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → ((𝑃 / 2) ≤ (𝑥 · 2) ↔ ¬ (𝑥 · 2) < (𝑃 / 2)))
107	23, 61	anim12i 606	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → ((𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃) ∧ (𝑥 · 2) ∈ ℤ))
108	107, 31	sylibr 225	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → (𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ∧ (𝑥 · 2) ∈ ℤ))
109		halfleoddlt 15370	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ∧ (𝑥 · 2) ∈ ℤ) → ((𝑃 / 2) ≤ (𝑥 · 2) ↔ (𝑃 / 2) < (𝑥 · 2)))
110	108, 109	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → ((𝑃 / 2) ≤ (𝑥 · 2) ↔ (𝑃 / 2) < (𝑥 · 2)))
111	110	biimpa 468	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) ∧ (𝑃 / 2) ≤ (𝑥 · 2)) → (𝑃 / 2) < (𝑥 · 2))
112		nncn 11283	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑃 ∈ ℕ → 𝑃 ∈ ℂ)
113		subhalfhalf 11512	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑃 ∈ ℂ → (𝑃 − (𝑃 / 2)) = (𝑃 / 2))
114	112, 113	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑃 ∈ ℕ → (𝑃 − (𝑃 / 2)) = (𝑃 / 2))
115	114	breq1d 4819	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑃 ∈ ℕ → ((𝑃 − (𝑃 / 2)) < (𝑥 · 2) ↔ (𝑃 / 2) < (𝑥 · 2)))
116	115	ad3antrrr 721	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) ∧ (𝑃 / 2) ≤ (𝑥 · 2)) → ((𝑃 − (𝑃 / 2)) < (𝑥 · 2) ↔ (𝑃 / 2) < (𝑥 · 2)))
117	111, 116	mpbird 248	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) ∧ (𝑃 / 2) ≤ (𝑥 · 2)) → (𝑃 − (𝑃 / 2)) < (𝑥 · 2))
118	101	ad2antrr 717	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → 𝑃 ∈ ℝ)
119	102	ad2antrr 717	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → (𝑃 / 2) ∈ ℝ)
120	104	adantl 473	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → (𝑥 · 2) ∈ ℝ)
121	118, 119, 120	3jca 1158	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → (𝑃 ∈ ℝ ∧ (𝑃 / 2) ∈ ℝ ∧ (𝑥 · 2) ∈ ℝ))
122	121	adantr 472	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) ∧ (𝑃 / 2) ≤ (𝑥 · 2)) → (𝑃 ∈ ℝ ∧ (𝑃 / 2) ∈ ℝ ∧ (𝑥 · 2) ∈ ℝ))
123		ltsub23 10762	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑃 ∈ ℝ ∧ (𝑃 / 2) ∈ ℝ ∧ (𝑥 · 2) ∈ ℝ) → ((𝑃 − (𝑃 / 2)) < (𝑥 · 2) ↔ (𝑃 − (𝑥 · 2)) < (𝑃 / 2)))
124	122, 123	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) ∧ (𝑃 / 2) ≤ (𝑥 · 2)) → ((𝑃 − (𝑃 / 2)) < (𝑥 · 2) ↔ (𝑃 − (𝑥 · 2)) < (𝑃 / 2)))
125	117, 124	mpbid 223	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) ∧ (𝑃 / 2) ≤ (𝑥 · 2)) → (𝑃 − (𝑥 · 2)) < (𝑃 / 2))
126	22	ad2antrr 717	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → 𝑃 ∈ ℤ)
127		simplr 785	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → ¬ 2 ∥ 𝑃)
128	61	adantl 473	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → (𝑥 · 2) ∈ ℤ)
129	126, 128	zsubcld 11734	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → (𝑃 − (𝑥 · 2)) ∈ ℤ)
130	126, 127, 129	3jca 1158	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → (𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ∧ (𝑃 − (𝑥 · 2)) ∈ ℤ))
131	130	adantr 472	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) ∧ (𝑃 / 2) ≤ (𝑥 · 2)) → (𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ∧ (𝑃 − (𝑥 · 2)) ∈ ℤ))
132		ltoddhalfle 15369	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ∧ (𝑃 − (𝑥 · 2)) ∈ ℤ) → ((𝑃 − (𝑥 · 2)) < (𝑃 / 2) ↔ (𝑃 − (𝑥 · 2)) ≤ ((𝑃 − 1) / 2)))
133	131, 132	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) ∧ (𝑃 / 2) ≤ (𝑥 · 2)) → ((𝑃 − (𝑥 · 2)) < (𝑃 / 2) ↔ (𝑃 − (𝑥 · 2)) ≤ ((𝑃 − 1) / 2)))
134	125, 133	mpbid 223	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) ∧ (𝑃 / 2) ≤ (𝑥 · 2)) → (𝑃 − (𝑥 · 2)) ≤ ((𝑃 − 1) / 2))
135	134	ex 401	. . . . . . . . . . . . . . 15 ⊢ (((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → ((𝑃 / 2) ≤ (𝑥 · 2) → (𝑃 − (𝑥 · 2)) ≤ ((𝑃 − 1) / 2)))
136	15	breq2i 4817	. . . . . . . . . . . . . . 15 ⊢ ((𝑃 − (𝑥 · 2)) ≤ 𝐻 ↔ (𝑃 − (𝑥 · 2)) ≤ ((𝑃 − 1) / 2))
137	135, 136	syl6ibr 243	. . . . . . . . . . . . . 14 ⊢ (((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → ((𝑃 / 2) ≤ (𝑥 · 2) → (𝑃 − (𝑥 · 2)) ≤ 𝐻))
138	106, 137	sylbird 251	. . . . . . . . . . . . 13 ⊢ (((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → (¬ (𝑥 · 2) < (𝑃 / 2) → (𝑃 − (𝑥 · 2)) ≤ 𝐻))
139	138	ex 401	. . . . . . . . . . . 12 ⊢ ((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) → (𝑥 ∈ (1...𝐻) → (¬ (𝑥 · 2) < (𝑃 / 2) → (𝑃 − (𝑥 · 2)) ≤ 𝐻)))
140	20, 21, 139	3syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ∈ (1...𝐻) → (¬ (𝑥 · 2) < (𝑃 / 2) → (𝑃 − (𝑥 · 2)) ≤ 𝐻)))
141	140	imp 395	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝐻)) → (¬ (𝑥 · 2) < (𝑃 / 2) → (𝑃 − (𝑥 · 2)) ≤ 𝐻))
142	141	impcom 396	. . . . . . . . 9 ⊢ ((¬ (𝑥 · 2) < (𝑃 / 2) ∧ (𝜑 ∧ 𝑥 ∈ (1...𝐻))) → (𝑃 − (𝑥 · 2)) ≤ 𝐻)
143		elfz1b 12616	. . . . . . . . 9 ⊢ ((𝑃 − (𝑥 · 2)) ∈ (1...𝐻) ↔ ((𝑃 − (𝑥 · 2)) ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ (𝑃 − (𝑥 · 2)) ≤ 𝐻))
144	98, 100, 142, 143	syl3anbrc 1443	. . . . . . . 8 ⊢ ((¬ (𝑥 · 2) < (𝑃 / 2) ∧ (𝜑 ∧ 𝑥 ∈ (1...𝐻))) → (𝑃 − (𝑥 · 2)) ∈ (1...𝐻))
145		eleq1 2832	. . . . . . . 8 ⊢ (𝑦 = (𝑃 − (𝑥 · 2)) → (𝑦 ∈ (1...𝐻) ↔ (𝑃 − (𝑥 · 2)) ∈ (1...𝐻)))
146	144, 145	syl5ibrcom 238	. . . . . . 7 ⊢ ((¬ (𝑥 · 2) < (𝑃 / 2) ∧ (𝜑 ∧ 𝑥 ∈ (1...𝐻))) → (𝑦 = (𝑃 − (𝑥 · 2)) → 𝑦 ∈ (1...𝐻)))
147	54, 146	sylbid 231	. . . . . 6 ⊢ ((¬ (𝑥 · 2) < (𝑃 / 2) ∧ (𝜑 ∧ 𝑥 ∈ (1...𝐻))) → (𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) → 𝑦 ∈ (1...𝐻)))
148	51, 147	pm2.61ian 846	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝐻)) → (𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) → 𝑦 ∈ (1...𝐻)))
149	148	rexlimdva 3178	. . . 4 ⊢ (𝜑 → (∃𝑥 ∈ (1...𝐻)𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) → 𝑦 ∈ (1...𝐻)))
150		elfz1b 12616	. . . . . . . . . 10 ⊢ (𝑦 ∈ (1...𝐻) ↔ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻))
151		simp1 1166	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻) → 𝑦 ∈ ℕ)
152		simpl 474	. . . . . . . . . . . . 13 ⊢ ((2 ∥ 𝑦 ∧ 𝜑) → 2 ∥ 𝑦)
153		nnehalf 15380	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ ℕ ∧ 2 ∥ 𝑦) → (𝑦 / 2) ∈ ℕ)
154	151, 152, 153	syl2anr 590	. . . . . . . . . . . 12 ⊢ (((2 ∥ 𝑦 ∧ 𝜑) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻)) → (𝑦 / 2) ∈ ℕ)
155		simpr2 1250	. . . . . . . . . . . 12 ⊢ (((2 ∥ 𝑦 ∧ 𝜑) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻)) → 𝐻 ∈ ℕ)
156		nnre 11282	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ ℕ → 𝑦 ∈ ℝ)
157	156	ad2antrr 717	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) ∧ (2 ∥ 𝑦 ∧ 𝜑)) → 𝑦 ∈ ℝ)
158		nnrp 12041	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐻 ∈ ℕ → 𝐻 ∈ ℝ+)
159	158	adantl 473	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) → 𝐻 ∈ ℝ+)
160	159	adantr 472	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) ∧ (2 ∥ 𝑦 ∧ 𝜑)) → 𝐻 ∈ ℝ+)
161		2rp 12033	. . . . . . . . . . . . . . . . . . 19 ⊢ 2 ∈ ℝ+
162		1le2 11487	. . . . . . . . . . . . . . . . . . 19 ⊢ 1 ≤ 2
163	161, 162	pm3.2i 462	. . . . . . . . . . . . . . . . . 18 ⊢ (2 ∈ ℝ+ ∧ 1 ≤ 2)
164	163	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) ∧ (2 ∥ 𝑦 ∧ 𝜑)) → (2 ∈ ℝ+ ∧ 1 ≤ 2))
165		ledivge1le 12099	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑦 ∈ ℝ ∧ 𝐻 ∈ ℝ+ ∧ (2 ∈ ℝ+ ∧ 1 ≤ 2)) → (𝑦 ≤ 𝐻 → (𝑦 / 2) ≤ 𝐻))
166	157, 160, 164, 165	syl3anc 1490	. . . . . . . . . . . . . . . 16 ⊢ (((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) ∧ (2 ∥ 𝑦 ∧ 𝜑)) → (𝑦 ≤ 𝐻 → (𝑦 / 2) ≤ 𝐻))
167	166	ex 401	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) → ((2 ∥ 𝑦 ∧ 𝜑) → (𝑦 ≤ 𝐻 → (𝑦 / 2) ≤ 𝐻)))
168	167	com23 86	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) → (𝑦 ≤ 𝐻 → ((2 ∥ 𝑦 ∧ 𝜑) → (𝑦 / 2) ≤ 𝐻)))
169	168	3impia 1145	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻) → ((2 ∥ 𝑦 ∧ 𝜑) → (𝑦 / 2) ≤ 𝐻))
170	169	impcom 396	. . . . . . . . . . . 12 ⊢ (((2 ∥ 𝑦 ∧ 𝜑) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻)) → (𝑦 / 2) ≤ 𝐻)
171	154, 155, 170	3jca 1158	. . . . . . . . . . 11 ⊢ (((2 ∥ 𝑦 ∧ 𝜑) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻)) → ((𝑦 / 2) ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ (𝑦 / 2) ≤ 𝐻))
172	171	ex 401	. . . . . . . . . 10 ⊢ ((2 ∥ 𝑦 ∧ 𝜑) → ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻) → ((𝑦 / 2) ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ (𝑦 / 2) ≤ 𝐻)))
173	150, 172	syl5bi 233	. . . . . . . . 9 ⊢ ((2 ∥ 𝑦 ∧ 𝜑) → (𝑦 ∈ (1...𝐻) → ((𝑦 / 2) ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ (𝑦 / 2) ≤ 𝐻)))
174	173	3impia 1145	. . . . . . . 8 ⊢ ((2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → ((𝑦 / 2) ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ (𝑦 / 2) ≤ 𝐻))
175		elfz1b 12616	. . . . . . . 8 ⊢ ((𝑦 / 2) ∈ (1...𝐻) ↔ ((𝑦 / 2) ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ (𝑦 / 2) ≤ 𝐻))
176	174, 175	sylibr 225	. . . . . . 7 ⊢ ((2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → (𝑦 / 2) ∈ (1...𝐻))
177		oveq1 6849	. . . . . . . . . . 11 ⊢ (𝑥 = (𝑦 / 2) → (𝑥 · 2) = ((𝑦 / 2) · 2))
178	177	breq1d 4819	. . . . . . . . . 10 ⊢ (𝑥 = (𝑦 / 2) → ((𝑥 · 2) < (𝑃 / 2) ↔ ((𝑦 / 2) · 2) < (𝑃 / 2)))
179	177	oveq2d 6858	. . . . . . . . . 10 ⊢ (𝑥 = (𝑦 / 2) → (𝑃 − (𝑥 · 2)) = (𝑃 − ((𝑦 / 2) · 2)))
180	178, 177, 179	ifbieq12d 4270	. . . . . . . . 9 ⊢ (𝑥 = (𝑦 / 2) → if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) = if(((𝑦 / 2) · 2) < (𝑃 / 2), ((𝑦 / 2) · 2), (𝑃 − ((𝑦 / 2) · 2))))
181	180	eqeq2d 2775	. . . . . . . 8 ⊢ (𝑥 = (𝑦 / 2) → (𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) ↔ 𝑦 = if(((𝑦 / 2) · 2) < (𝑃 / 2), ((𝑦 / 2) · 2), (𝑃 − ((𝑦 / 2) · 2)))))
182	181	adantl 473	. . . . . . 7 ⊢ (((2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) ∧ 𝑥 = (𝑦 / 2)) → (𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) ↔ 𝑦 = if(((𝑦 / 2) · 2) < (𝑃 / 2), ((𝑦 / 2) · 2), (𝑃 − ((𝑦 / 2) · 2)))))
183		elfzelz 12549	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ (1...𝐻) → 𝑦 ∈ ℤ)
184	183	zcnd 11730	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ (1...𝐻) → 𝑦 ∈ ℂ)
185	184	3ad2ant3 1165	. . . . . . . . . . 11 ⊢ ((2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → 𝑦 ∈ ℂ)
186		2cnd 11350	. . . . . . . . . . 11 ⊢ ((2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → 2 ∈ ℂ)
187		2ne0 11383	. . . . . . . . . . . 12 ⊢ 2 ≠ 0
188	187	a1i 11	. . . . . . . . . . 11 ⊢ ((2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → 2 ≠ 0)
189	185, 186, 188	divcan1d 11056	. . . . . . . . . 10 ⊢ ((2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → ((𝑦 / 2) · 2) = 𝑦)
190	15	breq2i 4817	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ≤ 𝐻 ↔ 𝑦 ≤ ((𝑃 − 1) / 2))
191		nnz 11646	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 ∈ ℕ → 𝑦 ∈ ℤ)
192	20, 21, 23	3syl 18	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃))
193	192	adantl 473	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((2 ∥ 𝑦 ∧ 𝜑) → (𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃))
194	191, 193	anim12ci 607	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑦 ∈ ℕ ∧ (2 ∥ 𝑦 ∧ 𝜑)) → ((𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃) ∧ 𝑦 ∈ ℤ))
195		df-3an 1109	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ∧ 𝑦 ∈ ℤ) ↔ ((𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃) ∧ 𝑦 ∈ ℤ))
196	194, 195	sylibr 225	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑦 ∈ ℕ ∧ (2 ∥ 𝑦 ∧ 𝜑)) → (𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ∧ 𝑦 ∈ ℤ))
197		ltoddhalfle 15369	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ∧ 𝑦 ∈ ℤ) → (𝑦 < (𝑃 / 2) ↔ 𝑦 ≤ ((𝑃 − 1) / 2)))
198	196, 197	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑦 ∈ ℕ ∧ (2 ∥ 𝑦 ∧ 𝜑)) → (𝑦 < (𝑃 / 2) ↔ 𝑦 ≤ ((𝑃 − 1) / 2)))
199	198	exbiri 845	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ ℕ → ((2 ∥ 𝑦 ∧ 𝜑) → (𝑦 ≤ ((𝑃 − 1) / 2) → 𝑦 < (𝑃 / 2))))
200	199	com23 86	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ℕ → (𝑦 ≤ ((𝑃 − 1) / 2) → ((2 ∥ 𝑦 ∧ 𝜑) → 𝑦 < (𝑃 / 2))))
201	190, 200	syl5bi 233	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → (𝑦 ≤ 𝐻 → ((2 ∥ 𝑦 ∧ 𝜑) → 𝑦 < (𝑃 / 2))))
202	201	a1d 25	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → (𝐻 ∈ ℕ → (𝑦 ≤ 𝐻 → ((2 ∥ 𝑦 ∧ 𝜑) → 𝑦 < (𝑃 / 2)))))
203	202	3imp 1137	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻) → ((2 ∥ 𝑦 ∧ 𝜑) → 𝑦 < (𝑃 / 2)))
204	150, 203	sylbi 208	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ (1...𝐻) → ((2 ∥ 𝑦 ∧ 𝜑) → 𝑦 < (𝑃 / 2)))
205	204	com12 32	. . . . . . . . . . 11 ⊢ ((2 ∥ 𝑦 ∧ 𝜑) → (𝑦 ∈ (1...𝐻) → 𝑦 < (𝑃 / 2)))
206	205	3impia 1145	. . . . . . . . . 10 ⊢ ((2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → 𝑦 < (𝑃 / 2))
207	189, 206	eqbrtrd 4831	. . . . . . . . 9 ⊢ ((2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → ((𝑦 / 2) · 2) < (𝑃 / 2))
208	207	iftrued 4251	. . . . . . . 8 ⊢ ((2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → if(((𝑦 / 2) · 2) < (𝑃 / 2), ((𝑦 / 2) · 2), (𝑃 − ((𝑦 / 2) · 2))) = ((𝑦 / 2) · 2))
209	208, 189	eqtr2d 2800	. . . . . . 7 ⊢ ((2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → 𝑦 = if(((𝑦 / 2) · 2) < (𝑃 / 2), ((𝑦 / 2) · 2), (𝑃 − ((𝑦 / 2) · 2))))
210	176, 182, 209	rspcedvd 3468	. . . . . 6 ⊢ ((2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → ∃𝑥 ∈ (1...𝐻)𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))))
211	210	3exp 1148	. . . . 5 ⊢ (2 ∥ 𝑦 → (𝜑 → (𝑦 ∈ (1...𝐻) → ∃𝑥 ∈ (1...𝐻)𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))))))
212	55, 56	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 𝑃 ∈ ℤ)
213	212	ad2antrr 717	. . . . . . . . . . . . . . . 16 ⊢ (((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻)) → 𝑃 ∈ ℤ)
214	191	3ad2ant1 1163	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻) → 𝑦 ∈ ℤ)
215	214	adantl 473	. . . . . . . . . . . . . . . 16 ⊢ (((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻)) → 𝑦 ∈ ℤ)
216	213, 215	zsubcld 11734	. . . . . . . . . . . . . . 15 ⊢ (((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻)) → (𝑃 − 𝑦) ∈ ℤ)
217	156	ad2antrl 719	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑃 ∈ ℝ ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ)) → 𝑦 ∈ ℝ)
218	67	rehalfcld 11525	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑃 ∈ ℝ → ((𝑃 − 1) / 2) ∈ ℝ)
219	218	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑃 ∈ ℝ ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ)) → ((𝑃 − 1) / 2) ∈ ℝ)
220		simpl 474	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑃 ∈ ℝ ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ)) → 𝑃 ∈ ℝ)
221	217, 219, 220	3jca 1158	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑃 ∈ ℝ ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ)) → (𝑦 ∈ ℝ ∧ ((𝑃 − 1) / 2) ∈ ℝ ∧ 𝑃 ∈ ℝ))
222	221	ex 401	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑃 ∈ ℝ → ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) → (𝑦 ∈ ℝ ∧ ((𝑃 − 1) / 2) ∈ ℝ ∧ 𝑃 ∈ ℝ)))
223	55, 64, 222	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) → (𝑦 ∈ ℝ ∧ ((𝑃 − 1) / 2) ∈ ℝ ∧ 𝑃 ∈ ℝ)))
224	223	adantr 472	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) → ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) → (𝑦 ∈ ℝ ∧ ((𝑃 − 1) / 2) ∈ ℝ ∧ 𝑃 ∈ ℝ)))
225	224	impcom 396	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) ∧ (𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦)) → (𝑦 ∈ ℝ ∧ ((𝑃 − 1) / 2) ∈ ℝ ∧ 𝑃 ∈ ℝ))
226		lesub2 10777	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑦 ∈ ℝ ∧ ((𝑃 − 1) / 2) ∈ ℝ ∧ 𝑃 ∈ ℝ) → (𝑦 ≤ ((𝑃 − 1) / 2) ↔ (𝑃 − ((𝑃 − 1) / 2)) ≤ (𝑃 − 𝑦)))
227	225, 226	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) ∧ (𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦)) → (𝑦 ≤ ((𝑃 − 1) / 2) ↔ (𝑃 − ((𝑃 − 1) / 2)) ≤ (𝑃 − 𝑦)))
228	56	zcnd 11730	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℂ)
229		1cnd 10288	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑃 ∈ ℂ → 1 ∈ ℂ)
230		2cnne0 11488	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (2 ∈ ℂ ∧ 2 ≠ 0)
231	230	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑃 ∈ ℂ → (2 ∈ ℂ ∧ 2 ≠ 0))
232		divsubdir 10975	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑃 ∈ ℂ ∧ 1 ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → ((𝑃 − 1) / 2) = ((𝑃 / 2) − (1 / 2)))
233	229, 231, 232	mpd3an23 1587	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑃 ∈ ℂ → ((𝑃 − 1) / 2) = ((𝑃 / 2) − (1 / 2)))
234	233	oveq2d 6858	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑃 ∈ ℂ → (𝑃 − ((𝑃 − 1) / 2)) = (𝑃 − ((𝑃 / 2) − (1 / 2))))
235		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑃 ∈ ℂ → 𝑃 ∈ ℂ)
236		halfcl 11503	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑃 ∈ ℂ → (𝑃 / 2) ∈ ℂ)
237		halfcn 11493	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (1 / 2) ∈ ℂ
238	237	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑃 ∈ ℂ → (1 / 2) ∈ ℂ)
239	235, 236, 238	subsubd 10674	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑃 ∈ ℂ → (𝑃 − ((𝑃 / 2) − (1 / 2))) = ((𝑃 − (𝑃 / 2)) + (1 / 2)))
240	113	oveq1d 6857	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑃 ∈ ℂ → ((𝑃 − (𝑃 / 2)) + (1 / 2)) = ((𝑃 / 2) + (1 / 2)))
241	234, 239, 240	3eqtrd 2803	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑃 ∈ ℂ → (𝑃 − ((𝑃 − 1) / 2)) = ((𝑃 / 2) + (1 / 2)))
242	55, 228, 241	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (𝑃 − ((𝑃 − 1) / 2)) = ((𝑃 / 2) + (1 / 2)))
243	242	ad2antrl 719	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) ∧ (𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦)) → (𝑃 − ((𝑃 − 1) / 2)) = ((𝑃 / 2) + (1 / 2)))
244	243	breq1d 4819	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) ∧ (𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦)) → ((𝑃 − ((𝑃 − 1) / 2)) ≤ (𝑃 − 𝑦) ↔ ((𝑃 / 2) + (1 / 2)) ≤ (𝑃 − 𝑦)))
245		prmnn 15670	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
246		halfre 11492	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (1 / 2) ∈ ℝ
247	246	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑃 ∈ ℕ → (1 / 2) ∈ ℝ)
248		nngt0 11306	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑃 ∈ ℕ → 0 < 𝑃)
249	71	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑃 ∈ ℕ → (2 ∈ ℝ ∧ 0 < 2))
250		divgt0 11145	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑃 ∈ ℝ ∧ 0 < 𝑃) ∧ (2 ∈ ℝ ∧ 0 < 2)) → 0 < (𝑃 / 2))
251	101, 248, 249, 250	syl21anc 866	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑃 ∈ ℕ → 0 < (𝑃 / 2))
252		halfgt0 11494	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 0 < (1 / 2)
253	252	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑃 ∈ ℕ → 0 < (1 / 2))
254	102, 247, 251, 253	addgt0d 10856	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑃 ∈ ℕ → 0 < ((𝑃 / 2) + (1 / 2)))
255	55, 245, 254	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 0 < ((𝑃 / 2) + (1 / 2)))
256	255	ad2antrl 719	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) ∧ (𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦)) → 0 < ((𝑃 / 2) + (1 / 2)))
257		0red 10297	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → 0 ∈ ℝ)
258		simpr 477	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → 𝑃 ∈ ℝ)
259	258	rehalfcld 11525	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → (𝑃 / 2) ∈ ℝ)
260	246	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → (1 / 2) ∈ ℝ)
261	259, 260	readdcld 10323	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → ((𝑃 / 2) + (1 / 2)) ∈ ℝ)
262		resubcl 10599	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑃 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑃 − 𝑦) ∈ ℝ)
263	262	ancoms 450	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → (𝑃 − 𝑦) ∈ ℝ)
264	257, 261, 263	3jca 1158	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → (0 ∈ ℝ ∧ ((𝑃 / 2) + (1 / 2)) ∈ ℝ ∧ (𝑃 − 𝑦) ∈ ℝ))
265	264	ex 401	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑦 ∈ ℝ → (𝑃 ∈ ℝ → (0 ∈ ℝ ∧ ((𝑃 / 2) + (1 / 2)) ∈ ℝ ∧ (𝑃 − 𝑦) ∈ ℝ)))
266	156, 265	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑦 ∈ ℕ → (𝑃 ∈ ℝ → (0 ∈ ℝ ∧ ((𝑃 / 2) + (1 / 2)) ∈ ℝ ∧ (𝑃 − 𝑦) ∈ ℝ)))
267	266	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) → (𝑃 ∈ ℝ → (0 ∈ ℝ ∧ ((𝑃 / 2) + (1 / 2)) ∈ ℝ ∧ (𝑃 − 𝑦) ∈ ℝ)))
268	267	com12 32	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑃 ∈ ℝ → ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) → (0 ∈ ℝ ∧ ((𝑃 / 2) + (1 / 2)) ∈ ℝ ∧ (𝑃 − 𝑦) ∈ ℝ)))
269	55, 64, 268	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) → (0 ∈ ℝ ∧ ((𝑃 / 2) + (1 / 2)) ∈ ℝ ∧ (𝑃 − 𝑦) ∈ ℝ)))
270	269	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) → ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) → (0 ∈ ℝ ∧ ((𝑃 / 2) + (1 / 2)) ∈ ℝ ∧ (𝑃 − 𝑦) ∈ ℝ)))
271	270	impcom 396	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) ∧ (𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦)) → (0 ∈ ℝ ∧ ((𝑃 / 2) + (1 / 2)) ∈ ℝ ∧ (𝑃 − 𝑦) ∈ ℝ))
272		ltletr 10383	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((0 ∈ ℝ ∧ ((𝑃 / 2) + (1 / 2)) ∈ ℝ ∧ (𝑃 − 𝑦) ∈ ℝ) → ((0 < ((𝑃 / 2) + (1 / 2)) ∧ ((𝑃 / 2) + (1 / 2)) ≤ (𝑃 − 𝑦)) → 0 < (𝑃 − 𝑦)))
273	271, 272	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) ∧ (𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦)) → ((0 < ((𝑃 / 2) + (1 / 2)) ∧ ((𝑃 / 2) + (1 / 2)) ≤ (𝑃 − 𝑦)) → 0 < (𝑃 − 𝑦)))
274	256, 273	mpand 686	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) ∧ (𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦)) → (((𝑃 / 2) + (1 / 2)) ≤ (𝑃 − 𝑦) → 0 < (𝑃 − 𝑦)))
275	244, 274	sylbid 231	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) ∧ (𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦)) → ((𝑃 − ((𝑃 − 1) / 2)) ≤ (𝑃 − 𝑦) → 0 < (𝑃 − 𝑦)))
276	227, 275	sylbid 231	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) ∧ (𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦)) → (𝑦 ≤ ((𝑃 − 1) / 2) → 0 < (𝑃 − 𝑦)))
277	276	ex 401	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) → ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) → (𝑦 ≤ ((𝑃 − 1) / 2) → 0 < (𝑃 − 𝑦))))
278	277	com23 86	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) → (𝑦 ≤ ((𝑃 − 1) / 2) → ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) → 0 < (𝑃 − 𝑦))))
279	190, 278	syl5bi 233	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) → (𝑦 ≤ 𝐻 → ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) → 0 < (𝑃 − 𝑦))))
280	279	3impia 1145	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻) → ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) → 0 < (𝑃 − 𝑦)))
281	280	impcom 396	. . . . . . . . . . . . . . 15 ⊢ (((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻)) → 0 < (𝑃 − 𝑦))
282		elnnz 11634	. . . . . . . . . . . . . . 15 ⊢ ((𝑃 − 𝑦) ∈ ℕ ↔ ((𝑃 − 𝑦) ∈ ℤ ∧ 0 < (𝑃 − 𝑦)))
283	216, 281, 282	sylanbrc 578	. . . . . . . . . . . . . 14 ⊢ (((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻)) → (𝑃 − 𝑦) ∈ ℕ)
284	24	adantr 472	. . . . . . . . . . . . . . 15 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) → (𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃))
285		simpr 477	. . . . . . . . . . . . . . . 16 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) → ¬ 2 ∥ 𝑦)
286	285, 214	anim12ci 607	. . . . . . . . . . . . . . 15 ⊢ (((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻)) → (𝑦 ∈ ℤ ∧ ¬ 2 ∥ 𝑦))
287		omoe 15372	. . . . . . . . . . . . . . 15 ⊢ (((𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃) ∧ (𝑦 ∈ ℤ ∧ ¬ 2 ∥ 𝑦)) → 2 ∥ (𝑃 − 𝑦))
288	284, 286, 287	syl2an2r 675	. . . . . . . . . . . . . 14 ⊢ (((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻)) → 2 ∥ (𝑃 − 𝑦))
289		nnehalf 15380	. . . . . . . . . . . . . 14 ⊢ (((𝑃 − 𝑦) ∈ ℕ ∧ 2 ∥ (𝑃 − 𝑦)) → ((𝑃 − 𝑦) / 2) ∈ ℕ)
290	283, 288, 289	syl2anc 579	. . . . . . . . . . . . 13 ⊢ (((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻)) → ((𝑃 − 𝑦) / 2) ∈ ℕ)
291		simpr2 1250	. . . . . . . . . . . . 13 ⊢ (((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻)) → 𝐻 ∈ ℕ)
292		1red 10294	. . . . . . . . . . . . . . . 16 ⊢ (((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻)) → 1 ∈ ℝ)
293	156	3ad2ant1 1163	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻) → 𝑦 ∈ ℝ)
294	293	adantl 473	. . . . . . . . . . . . . . . 16 ⊢ (((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻)) → 𝑦 ∈ ℝ)
295	55, 64	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 𝑃 ∈ ℝ)
296	295	ad2antrr 717	. . . . . . . . . . . . . . . 16 ⊢ (((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻)) → 𝑃 ∈ ℝ)
297		nnge1 11303	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ ℕ → 1 ≤ 𝑦)
298	297	3ad2ant1 1163	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻) → 1 ≤ 𝑦)
299	298	adantl 473	. . . . . . . . . . . . . . . 16 ⊢ (((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻)) → 1 ≤ 𝑦)
300	292, 294, 296, 299	lesub2dd 10898	. . . . . . . . . . . . . . 15 ⊢ (((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻)) → (𝑃 − 𝑦) ≤ (𝑃 − 1))
301	296, 294	resubcld 10712	. . . . . . . . . . . . . . . 16 ⊢ (((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻)) → (𝑃 − 𝑦) ∈ ℝ)
302	55, 64, 67	3syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (𝑃 − 1) ∈ ℝ)
303	302	ad2antrr 717	. . . . . . . . . . . . . . . 16 ⊢ (((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻)) → (𝑃 − 1) ∈ ℝ)
304	71	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻)) → (2 ∈ ℝ ∧ 0 < 2))
305		lediv1 11142	. . . . . . . . . . . . . . . 16 ⊢ (((𝑃 − 𝑦) ∈ ℝ ∧ (𝑃 − 1) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((𝑃 − 𝑦) ≤ (𝑃 − 1) ↔ ((𝑃 − 𝑦) / 2) ≤ ((𝑃 − 1) / 2)))
306	301, 303, 304, 305	syl3anc 1490	. . . . . . . . . . . . . . 15 ⊢ (((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻)) → ((𝑃 − 𝑦) ≤ (𝑃 − 1) ↔ ((𝑃 − 𝑦) / 2) ≤ ((𝑃 − 1) / 2)))
307	300, 306	mpbid 223	. . . . . . . . . . . . . 14 ⊢ (((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻)) → ((𝑃 − 𝑦) / 2) ≤ ((𝑃 − 1) / 2))
308	15	breq2i 4817	. . . . . . . . . . . . . 14 ⊢ (((𝑃 − 𝑦) / 2) ≤ 𝐻 ↔ ((𝑃 − 𝑦) / 2) ≤ ((𝑃 − 1) / 2))
309	307, 308	sylibr 225	. . . . . . . . . . . . 13 ⊢ (((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻)) → ((𝑃 − 𝑦) / 2) ≤ 𝐻)
310	290, 291, 309	3jca 1158	. . . . . . . . . . . 12 ⊢ (((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻)) → (((𝑃 − 𝑦) / 2) ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ ((𝑃 − 𝑦) / 2) ≤ 𝐻))
311	310	ex 401	. . . . . . . . . . 11 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) → ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻) → (((𝑃 − 𝑦) / 2) ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ ((𝑃 − 𝑦) / 2) ≤ 𝐻)))
312		elfz1b 12616	. . . . . . . . . . 11 ⊢ (((𝑃 − 𝑦) / 2) ∈ (1...𝐻) ↔ (((𝑃 − 𝑦) / 2) ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ ((𝑃 − 𝑦) / 2) ≤ 𝐻))
313	311, 150, 312	3imtr4g 287	. . . . . . . . . 10 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) → (𝑦 ∈ (1...𝐻) → ((𝑃 − 𝑦) / 2) ∈ (1...𝐻)))
314	313	ex 401	. . . . . . . . 9 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (¬ 2 ∥ 𝑦 → (𝑦 ∈ (1...𝐻) → ((𝑃 − 𝑦) / 2) ∈ (1...𝐻))))
315	20, 314	syl 17	. . . . . . . 8 ⊢ (𝜑 → (¬ 2 ∥ 𝑦 → (𝑦 ∈ (1...𝐻) → ((𝑃 − 𝑦) / 2) ∈ (1...𝐻))))
316	315	3imp21 1141	. . . . . . 7 ⊢ ((¬ 2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → ((𝑃 − 𝑦) / 2) ∈ (1...𝐻))
317		oveq1 6849	. . . . . . . . . . 11 ⊢ (𝑥 = ((𝑃 − 𝑦) / 2) → (𝑥 · 2) = (((𝑃 − 𝑦) / 2) · 2))
318	317	breq1d 4819	. . . . . . . . . 10 ⊢ (𝑥 = ((𝑃 − 𝑦) / 2) → ((𝑥 · 2) < (𝑃 / 2) ↔ (((𝑃 − 𝑦) / 2) · 2) < (𝑃 / 2)))
319	317	oveq2d 6858	. . . . . . . . . 10 ⊢ (𝑥 = ((𝑃 − 𝑦) / 2) → (𝑃 − (𝑥 · 2)) = (𝑃 − (((𝑃 − 𝑦) / 2) · 2)))
320	318, 317, 319	ifbieq12d 4270	. . . . . . . . 9 ⊢ (𝑥 = ((𝑃 − 𝑦) / 2) → if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) = if((((𝑃 − 𝑦) / 2) · 2) < (𝑃 / 2), (((𝑃 − 𝑦) / 2) · 2), (𝑃 − (((𝑃 − 𝑦) / 2) · 2))))
321	320	eqeq2d 2775	. . . . . . . 8 ⊢ (𝑥 = ((𝑃 − 𝑦) / 2) → (𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) ↔ 𝑦 = if((((𝑃 − 𝑦) / 2) · 2) < (𝑃 / 2), (((𝑃 − 𝑦) / 2) · 2), (𝑃 − (((𝑃 − 𝑦) / 2) · 2)))))
322	321	adantl 473	. . . . . . 7 ⊢ (((¬ 2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) ∧ 𝑥 = ((𝑃 − 𝑦) / 2)) → (𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) ↔ 𝑦 = if((((𝑃 − 𝑦) / 2) · 2) < (𝑃 / 2), (((𝑃 − 𝑦) / 2) · 2), (𝑃 − (((𝑃 − 𝑦) / 2) · 2)))))
323	20, 55, 228	3syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑃 ∈ ℂ)
324	323	3ad2ant2 1164	. . . . . . . . . . . 12 ⊢ ((¬ 2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → 𝑃 ∈ ℂ)
325	184	3ad2ant3 1165	. . . . . . . . . . . 12 ⊢ ((¬ 2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → 𝑦 ∈ ℂ)
326	324, 325	subcld 10646	. . . . . . . . . . 11 ⊢ ((¬ 2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → (𝑃 − 𝑦) ∈ ℂ)
327		2cnd 11350	. . . . . . . . . . 11 ⊢ ((¬ 2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → 2 ∈ ℂ)
328	187	a1i 11	. . . . . . . . . . 11 ⊢ ((¬ 2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → 2 ≠ 0)
329	326, 327, 328	divcan1d 11056	. . . . . . . . . 10 ⊢ ((¬ 2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → (((𝑃 − 𝑦) / 2) · 2) = (𝑃 − 𝑦))
330		zre 11628	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑃 ∈ ℤ → 𝑃 ∈ ℝ)
331		halfge0 11495	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 0 ≤ (1 / 2)
332		rehalfcl 11504	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑃 ∈ ℝ → (𝑃 / 2) ∈ ℝ)
333	332	adantl 473	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → (𝑃 / 2) ∈ ℝ)
334	333, 260	subge02d 10873	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → (0 ≤ (1 / 2) ↔ ((𝑃 / 2) − (1 / 2)) ≤ (𝑃 / 2)))
335	331, 334	mpbii 224	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → ((𝑃 / 2) − (1 / 2)) ≤ (𝑃 / 2))
336		simpl 474	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → 𝑦 ∈ ℝ)
337	246	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑃 ∈ ℝ → (1 / 2) ∈ ℝ)
338	332, 337	resubcld 10712	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑃 ∈ ℝ → ((𝑃 / 2) − (1 / 2)) ∈ ℝ)
339	338	adantl 473	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → ((𝑃 / 2) − (1 / 2)) ∈ ℝ)
340		letr 10385	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑦 ∈ ℝ ∧ ((𝑃 / 2) − (1 / 2)) ∈ ℝ ∧ (𝑃 / 2) ∈ ℝ) → ((𝑦 ≤ ((𝑃 / 2) − (1 / 2)) ∧ ((𝑃 / 2) − (1 / 2)) ≤ (𝑃 / 2)) → 𝑦 ≤ (𝑃 / 2)))
341	336, 339, 333, 340	syl3anc 1490	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → ((𝑦 ≤ ((𝑃 / 2) − (1 / 2)) ∧ ((𝑃 / 2) − (1 / 2)) ≤ (𝑃 / 2)) → 𝑦 ≤ (𝑃 / 2)))
342	335, 341	mpan2d 685	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → (𝑦 ≤ ((𝑃 / 2) − (1 / 2)) → 𝑦 ≤ (𝑃 / 2)))
343	81	adantl 473	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → 𝑃 ∈ ℂ)
344		1cnd 10288	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → 1 ∈ ℂ)
345	230	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → (2 ∈ ℂ ∧ 2 ≠ 0))
346	343, 344, 345, 232	syl3anc 1490	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → ((𝑃 − 1) / 2) = ((𝑃 / 2) − (1 / 2)))
347	346	breq2d 4821	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → (𝑦 ≤ ((𝑃 − 1) / 2) ↔ 𝑦 ≤ ((𝑃 / 2) − (1 / 2))))
348		lesub 10761	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑃 / 2) ∈ ℝ ∧ 𝑃 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((𝑃 / 2) ≤ (𝑃 − 𝑦) ↔ 𝑦 ≤ (𝑃 − (𝑃 / 2))))
349	333, 258, 336, 348	syl3anc 1490	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → ((𝑃 / 2) ≤ (𝑃 − 𝑦) ↔ 𝑦 ≤ (𝑃 − (𝑃 / 2))))
350	259, 263	lenltd 10437	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → ((𝑃 / 2) ≤ (𝑃 − 𝑦) ↔ ¬ (𝑃 − 𝑦) < (𝑃 / 2)))
351		2cnd 11350	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑃 ∈ ℝ → 2 ∈ ℂ)
352	187	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑃 ∈ ℝ → 2 ≠ 0)
353	81, 351, 352	divcan1d 11056	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑃 ∈ ℝ → ((𝑃 / 2) · 2) = 𝑃)
354	353	eqcomd 2771	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑃 ∈ ℝ → 𝑃 = ((𝑃 / 2) · 2))
355	354	oveq1d 6857	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑃 ∈ ℝ → (𝑃 − (𝑃 / 2)) = (((𝑃 / 2) · 2) − (𝑃 / 2)))
356	332	recnd 10322	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑃 ∈ ℝ → (𝑃 / 2) ∈ ℂ)
357	356, 351	mulcomd 10315	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑃 ∈ ℝ → ((𝑃 / 2) · 2) = (2 · (𝑃 / 2)))
358	357	oveq1d 6857	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑃 ∈ ℝ → (((𝑃 / 2) · 2) − (𝑃 / 2)) = ((2 · (𝑃 / 2)) − (𝑃 / 2)))
359	351, 356	mulsubfacd 10746	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑃 ∈ ℝ → ((2 · (𝑃 / 2)) − (𝑃 / 2)) = ((2 − 1) · (𝑃 / 2)))
360		2m1e1 11405	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (2 − 1) = 1
361	360	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑃 ∈ ℝ → (2 − 1) = 1)
362	361	oveq1d 6857	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑃 ∈ ℝ → ((2 − 1) · (𝑃 / 2)) = (1 · (𝑃 / 2)))
363	356	mulid2d 10312	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑃 ∈ ℝ → (1 · (𝑃 / 2)) = (𝑃 / 2))
364	359, 362, 363	3eqtrd 2803	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑃 ∈ ℝ → ((2 · (𝑃 / 2)) − (𝑃 / 2)) = (𝑃 / 2))
365	355, 358, 364	3eqtrd 2803	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑃 ∈ ℝ → (𝑃 − (𝑃 / 2)) = (𝑃 / 2))
366	365	adantl 473	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → (𝑃 − (𝑃 / 2)) = (𝑃 / 2))
367	366	breq2d 4821	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → (𝑦 ≤ (𝑃 − (𝑃 / 2)) ↔ 𝑦 ≤ (𝑃 / 2)))
368	349, 350, 367	3bitr3d 300	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → (¬ (𝑃 − 𝑦) < (𝑃 / 2) ↔ 𝑦 ≤ (𝑃 / 2)))
369	342, 347, 368	3imtr4d 285	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → (𝑦 ≤ ((𝑃 − 1) / 2) → ¬ (𝑃 − 𝑦) < (𝑃 / 2)))
370	369	ex 401	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ ℝ → (𝑃 ∈ ℝ → (𝑦 ≤ ((𝑃 − 1) / 2) → ¬ (𝑃 − 𝑦) < (𝑃 / 2))))
371	156, 370	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ ℕ → (𝑃 ∈ ℝ → (𝑦 ≤ ((𝑃 − 1) / 2) → ¬ (𝑃 − 𝑦) < (𝑃 / 2))))
372	371	com3l 89	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑃 ∈ ℝ → (𝑦 ≤ ((𝑃 − 1) / 2) → (𝑦 ∈ ℕ → ¬ (𝑃 − 𝑦) < (𝑃 / 2))))
373	330, 372	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑃 ∈ ℤ → (𝑦 ≤ ((𝑃 − 1) / 2) → (𝑦 ∈ ℕ → ¬ (𝑃 − 𝑦) < (𝑃 / 2))))
374	55, 56, 373	3syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (𝑦 ≤ ((𝑃 − 1) / 2) → (𝑦 ∈ ℕ → ¬ (𝑃 − 𝑦) < (𝑃 / 2))))
375	20, 374	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑦 ≤ ((𝑃 − 1) / 2) → (𝑦 ∈ ℕ → ¬ (𝑃 − 𝑦) < (𝑃 / 2))))
376	375	adantl 473	. . . . . . . . . . . . . . . . 17 ⊢ ((¬ 2 ∥ 𝑦 ∧ 𝜑) → (𝑦 ≤ ((𝑃 − 1) / 2) → (𝑦 ∈ ℕ → ¬ (𝑃 − 𝑦) < (𝑃 / 2))))
377	376	com13 88	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ℕ → (𝑦 ≤ ((𝑃 − 1) / 2) → ((¬ 2 ∥ 𝑦 ∧ 𝜑) → ¬ (𝑃 − 𝑦) < (𝑃 / 2))))
378	190, 377	syl5bi 233	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → (𝑦 ≤ 𝐻 → ((¬ 2 ∥ 𝑦 ∧ 𝜑) → ¬ (𝑃 − 𝑦) < (𝑃 / 2))))
379	378	a1d 25	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → (𝐻 ∈ ℕ → (𝑦 ≤ 𝐻 → ((¬ 2 ∥ 𝑦 ∧ 𝜑) → ¬ (𝑃 − 𝑦) < (𝑃 / 2)))))
380	379	3imp 1137	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻) → ((¬ 2 ∥ 𝑦 ∧ 𝜑) → ¬ (𝑃 − 𝑦) < (𝑃 / 2)))
381	380	com12 32	. . . . . . . . . . . 12 ⊢ ((¬ 2 ∥ 𝑦 ∧ 𝜑) → ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻) → ¬ (𝑃 − 𝑦) < (𝑃 / 2)))
382	150, 381	syl5bi 233	. . . . . . . . . . 11 ⊢ ((¬ 2 ∥ 𝑦 ∧ 𝜑) → (𝑦 ∈ (1...𝐻) → ¬ (𝑃 − 𝑦) < (𝑃 / 2)))
383	382	3impia 1145	. . . . . . . . . 10 ⊢ ((¬ 2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → ¬ (𝑃 − 𝑦) < (𝑃 / 2))
384	329, 383	eqnbrtrd 4827	. . . . . . . . 9 ⊢ ((¬ 2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → ¬ (((𝑃 − 𝑦) / 2) · 2) < (𝑃 / 2))
385	384	iffalsed 4254	. . . . . . . 8 ⊢ ((¬ 2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → if((((𝑃 − 𝑦) / 2) · 2) < (𝑃 / 2), (((𝑃 − 𝑦) / 2) · 2), (𝑃 − (((𝑃 − 𝑦) / 2) · 2))) = (𝑃 − (((𝑃 − 𝑦) / 2) · 2)))
386	329	oveq2d 6858	. . . . . . . 8 ⊢ ((¬ 2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → (𝑃 − (((𝑃 − 𝑦) / 2) · 2)) = (𝑃 − (𝑃 − 𝑦)))
387	323, 184	anim12i 606	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...𝐻)) → (𝑃 ∈ ℂ ∧ 𝑦 ∈ ℂ))
388	387	3adant1 1160	. . . . . . . . 9 ⊢ ((¬ 2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → (𝑃 ∈ ℂ ∧ 𝑦 ∈ ℂ))
389		nncan 10564	. . . . . . . . 9 ⊢ ((𝑃 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑃 − (𝑃 − 𝑦)) = 𝑦)
390	388, 389	syl 17	. . . . . . . 8 ⊢ ((¬ 2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → (𝑃 − (𝑃 − 𝑦)) = 𝑦)
391	385, 386, 390	3eqtrrd 2804	. . . . . . 7 ⊢ ((¬ 2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → 𝑦 = if((((𝑃 − 𝑦) / 2) · 2) < (𝑃 / 2), (((𝑃 − 𝑦) / 2) · 2), (𝑃 − (((𝑃 − 𝑦) / 2) · 2))))
392	316, 322, 391	rspcedvd 3468	. . . . . 6 ⊢ ((¬ 2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → ∃𝑥 ∈ (1...𝐻)𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))))
393	392	3exp 1148	. . . . 5 ⊢ (¬ 2 ∥ 𝑦 → (𝜑 → (𝑦 ∈ (1...𝐻) → ∃𝑥 ∈ (1...𝐻)𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))))))
394	211, 393	pm2.61i 176	. . . 4 ⊢ (𝜑 → (𝑦 ∈ (1...𝐻) → ∃𝑥 ∈ (1...𝐻)𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2)))))
395	149, 394	impbid 203	. . 3 ⊢ (𝜑 → (∃𝑥 ∈ (1...𝐻)𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) ↔ 𝑦 ∈ (1...𝐻)))
396	4, 395	syl5bb 274	. 2 ⊢ (𝜑 → (𝑦 ∈ ran 𝑅 ↔ 𝑦 ∈ (1...𝐻)))
397	396	eqrdv 2763	1 ⊢ (𝜑 → ran 𝑅 = (1...𝐻))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 197   ∧ wa 384   ∧ w3a 1107   = wceq 1652   ∈ wcel 2155   ≠ wne 2937  ∃wrex 3056  Vcvv 3350   ∖ cdif 3729  ifcif 4243  {csn 4334   class class class wbr 4809   ↦ cmpt 4888  ran crn 5278  (class class class)co 6842  ℂcc 10187  ℝcr 10188  0cc0 10189  1c1 10190   + caddc 10192   · cmul 10194   < clt 10328   ≤ cle 10329   − cmin 10520   / cdiv 10938  ℕcn 11274  2c2 11327  ℤcz 11624  ℝ⁺crp 12028  ...cfz 12533   ∥ cdvds 15267  ℙcprime 15667

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-sep 4941  ax-nul 4949  ax-pow 5001  ax-pr 5062  ax-un 7147  ax-cnex 10245  ax-resscn 10246  ax-1cn 10247  ax-icn 10248  ax-addcl 10249  ax-addrcl 10250  ax-mulcl 10251  ax-mulrcl 10252  ax-mulcom 10253  ax-addass 10254  ax-mulass 10255  ax-distr 10256  ax-i2m1 10257  ax-1ne0 10258  ax-1rid 10259  ax-rnegex 10260  ax-rrecex 10261  ax-cnre 10262  ax-pre-lttri 10263  ax-pre-lttrn 10264  ax-pre-ltadd 10265  ax-pre-mulgt0 10266  ax-pre-sup 10267

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-nel 3041  df-ral 3060  df-rex 3061  df-reu 3062  df-rmo 3063  df-rab 3064  df-v 3352  df-sbc 3597  df-csb 3692  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-pss 3748  df-nul 4080  df-if 4244  df-pw 4317  df-sn 4335  df-pr 4337  df-tp 4339  df-op 4341  df-uni 4595  df-iun 4678  df-br 4810  df-opab 4872  df-mpt 4889  df-tr 4912  df-id 5185  df-eprel 5190  df-po 5198  df-so 5199  df-fr 5236  df-we 5238  df-xp 5283  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-rn 5288  df-res 5289  df-ima 5290  df-pred 5865  df-ord 5911  df-on 5912  df-lim 5913  df-suc 5914  df-iota 6031  df-fun 6070  df-fn 6071  df-f 6072  df-f1 6073  df-fo 6074  df-f1o 6075  df-fv 6076  df-riota 6803  df-ov 6845  df-oprab 6846  df-mpt2 6847  df-om 7264  df-1st 7366  df-2nd 7367  df-wrecs 7610  df-recs 7672  df-rdg 7710  df-1o 7764  df-2o 7765  df-er 7947  df-en 8161  df-dom 8162  df-sdom 8163  df-fin 8164  df-sup 8555  df-pnf 10330  df-mnf 10331  df-xr 10332  df-ltxr 10333  df-le 10334  df-sub 10522  df-neg 10523  df-div 10939  df-nn 11275  df-2 11335  df-3 11336  df-n0 11539  df-z 11625  df-uz 11887  df-rp 12029  df-ioo 12381  df-fz 12534  df-seq 13009  df-exp 13068  df-cj 14126  df-re 14127  df-im 14128  df-sqrt 14262  df-abs 14263  df-dvds 15268  df-prm 15668

This theorem is referenced by:  gausslemma2dlem1  25382