Theorem gausslemma2dlem1a 15299

Description: Lemma for gausslemma2dlem1 15302. (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		gausslemma2d.r	. . . . 5 ⊢ 𝑅 = (𝑥 ∈ (1...𝐻) ↦ if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))))
2	1	elrnmpt 4915	. . . 4 ⊢ (𝑦 ∈ V → (𝑦 ∈ ran 𝑅 ↔ ∃𝑥 ∈ (1...𝐻)𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2)))))
3	2	elv 2767	. . 3 ⊢ (𝑦 ∈ ran 𝑅 ↔ ∃𝑥 ∈ (1...𝐻)𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))))
4		iftrue 3566	. . . . . . . . . 10 ⊢ ((𝑥 · 2) < (𝑃 / 2) → if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) = (𝑥 · 2))
5	4	eqeq2d 2208	. . . . . . . . 9 ⊢ ((𝑥 · 2) < (𝑃 / 2) → (𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) ↔ 𝑦 = (𝑥 · 2)))
6	5	adantr 276	. . . . . . . 8 ⊢ (((𝑥 · 2) < (𝑃 / 2) ∧ (𝜑 ∧ 𝑥 ∈ (1...𝐻))) → (𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) ↔ 𝑦 = (𝑥 · 2)))
7		elfz1b 10165	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (1...𝐻) ↔ (𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻))
8		id 19	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ℕ → 𝑥 ∈ ℕ)
9		2nn 9152	. . . . . . . . . . . . . . . . . . 19 ⊢ 2 ∈ ℕ
10	9	a1i 9	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ℕ → 2 ∈ ℕ)
11	8, 10	nnmulcld 9039	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ℕ → (𝑥 · 2) ∈ ℕ)
12	11	3ad2ant1 1020	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻) → (𝑥 · 2) ∈ ℕ)
13	12	3ad2ant1 1020	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻) ∧ 𝜑 ∧ (𝑥 · 2) < (𝑃 / 2)) → (𝑥 · 2) ∈ ℕ)
14		gausslemma2d.h	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝐻 = ((𝑃 − 1) / 2)
15	14	eleq1i 2262	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐻 ∈ ℕ ↔ ((𝑃 − 1) / 2) ∈ ℕ)
16	15	biimpi 120	. . . . . . . . . . . . . . . . 17 ⊢ (𝐻 ∈ ℕ → ((𝑃 − 1) / 2) ∈ ℕ)
17	16	3ad2ant2 1021	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻) → ((𝑃 − 1) / 2) ∈ ℕ)
18	17	3ad2ant1 1020	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻) ∧ 𝜑 ∧ (𝑥 · 2) < (𝑃 / 2)) → ((𝑃 − 1) / 2) ∈ ℕ)
19		gausslemma2d.p	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑃 ∈ (ℙ ∖ {2}))
20		nnoddn2prm 12429	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃))
21		nnz 9345	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑃 ∈ ℕ → 𝑃 ∈ ℤ)
22	21	anim1i 340	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) → (𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃))
23	20, 22	syl 14	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃))
24		nnz 9345	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 ∈ ℕ → 𝑥 ∈ ℤ)
25		2z 9354	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 2 ∈ ℤ
26	25	a1i 9	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 ∈ ℕ → 2 ∈ ℤ)
27	24, 26	zmulcld 9454	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 ∈ ℕ → (𝑥 · 2) ∈ ℤ)
28	27	3ad2ant1 1020	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻) → (𝑥 · 2) ∈ ℤ)
29	23, 28	anim12i 338	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ (𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻)) → ((𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃) ∧ (𝑥 · 2) ∈ ℤ))
30		df-3an 982	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ∧ (𝑥 · 2) ∈ ℤ) ↔ ((𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃) ∧ (𝑥 · 2) ∈ ℤ))
31	29, 30	sylibr 134	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ (𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻)) → (𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ∧ (𝑥 · 2) ∈ ℤ))
32	31	ex 115	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → ((𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻) → (𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ∧ (𝑥 · 2) ∈ ℤ)))
33	19, 32	syl 14	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻) → (𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ∧ (𝑥 · 2) ∈ ℤ)))
34	33	impcom 125	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻) ∧ 𝜑) → (𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ∧ (𝑥 · 2) ∈ ℤ))
35		ltoddhalfle 12058	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ∧ (𝑥 · 2) ∈ ℤ) → ((𝑥 · 2) < (𝑃 / 2) ↔ (𝑥 · 2) ≤ ((𝑃 − 1) / 2)))
36	34, 35	syl 14	. . . . . . . . . . . . . . . 16 ⊢ (((𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻) ∧ 𝜑) → ((𝑥 · 2) < (𝑃 / 2) ↔ (𝑥 · 2) ≤ ((𝑃 − 1) / 2)))
37	36	biimp3a 1356	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻) ∧ 𝜑 ∧ (𝑥 · 2) < (𝑃 / 2)) → (𝑥 · 2) ≤ ((𝑃 − 1) / 2))
38	13, 18, 37	3jca 1179	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻) ∧ 𝜑 ∧ (𝑥 · 2) < (𝑃 / 2)) → ((𝑥 · 2) ∈ ℕ ∧ ((𝑃 − 1) / 2) ∈ ℕ ∧ (𝑥 · 2) ≤ ((𝑃 − 1) / 2)))
39	38	3exp 1204	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻) → (𝜑 → ((𝑥 · 2) < (𝑃 / 2) → ((𝑥 · 2) ∈ ℕ ∧ ((𝑃 − 1) / 2) ∈ ℕ ∧ (𝑥 · 2) ≤ ((𝑃 − 1) / 2)))))
40	7, 39	sylbi 121	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (1...𝐻) → (𝜑 → ((𝑥 · 2) < (𝑃 / 2) → ((𝑥 · 2) ∈ ℕ ∧ ((𝑃 − 1) / 2) ∈ ℕ ∧ (𝑥 · 2) ≤ ((𝑃 − 1) / 2)))))
41	40	impcom 125	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝐻)) → ((𝑥 · 2) < (𝑃 / 2) → ((𝑥 · 2) ∈ ℕ ∧ ((𝑃 − 1) / 2) ∈ ℕ ∧ (𝑥 · 2) ≤ ((𝑃 − 1) / 2))))
42	41	impcom 125	. . . . . . . . . 10 ⊢ (((𝑥 · 2) < (𝑃 / 2) ∧ (𝜑 ∧ 𝑥 ∈ (1...𝐻))) → ((𝑥 · 2) ∈ ℕ ∧ ((𝑃 − 1) / 2) ∈ ℕ ∧ (𝑥 · 2) ≤ ((𝑃 − 1) / 2)))
43	14	oveq2i 5933	. . . . . . . . . . . 12 ⊢ (1...𝐻) = (1...((𝑃 − 1) / 2))
44	43	eleq2i 2263	. . . . . . . . . . 11 ⊢ ((𝑥 · 2) ∈ (1...𝐻) ↔ (𝑥 · 2) ∈ (1...((𝑃 − 1) / 2)))
45		elfz1b 10165	. . . . . . . . . . 11 ⊢ ((𝑥 · 2) ∈ (1...((𝑃 − 1) / 2)) ↔ ((𝑥 · 2) ∈ ℕ ∧ ((𝑃 − 1) / 2) ∈ ℕ ∧ (𝑥 · 2) ≤ ((𝑃 − 1) / 2)))
46	44, 45	bitri 184	. . . . . . . . . 10 ⊢ ((𝑥 · 2) ∈ (1...𝐻) ↔ ((𝑥 · 2) ∈ ℕ ∧ ((𝑃 − 1) / 2) ∈ ℕ ∧ (𝑥 · 2) ≤ ((𝑃 − 1) / 2)))
47	42, 46	sylibr 134	. . . . . . . . 9 ⊢ (((𝑥 · 2) < (𝑃 / 2) ∧ (𝜑 ∧ 𝑥 ∈ (1...𝐻))) → (𝑥 · 2) ∈ (1...𝐻))
48		eleq1 2259	. . . . . . . . 9 ⊢ (𝑦 = (𝑥 · 2) → (𝑦 ∈ (1...𝐻) ↔ (𝑥 · 2) ∈ (1...𝐻)))
49	47, 48	syl5ibrcom 157	. . . . . . . 8 ⊢ (((𝑥 · 2) < (𝑃 / 2) ∧ (𝜑 ∧ 𝑥 ∈ (1...𝐻))) → (𝑦 = (𝑥 · 2) → 𝑦 ∈ (1...𝐻)))
50	6, 49	sylbid 150	. . . . . . 7 ⊢ (((𝑥 · 2) < (𝑃 / 2) ∧ (𝜑 ∧ 𝑥 ∈ (1...𝐻))) → (𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) → 𝑦 ∈ (1...𝐻)))
51	50	ancoms 268	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝐻)) ∧ (𝑥 · 2) < (𝑃 / 2)) → (𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) → 𝑦 ∈ (1...𝐻)))
52		iffalse 3569	. . . . . . . . . 10 ⊢ (¬ (𝑥 · 2) < (𝑃 / 2) → if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) = (𝑃 − (𝑥 · 2)))
53	52	eqeq2d 2208	. . . . . . . . 9 ⊢ (¬ (𝑥 · 2) < (𝑃 / 2) → (𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) ↔ 𝑦 = (𝑃 − (𝑥 · 2))))
54	53	adantr 276	. . . . . . . 8 ⊢ ((¬ (𝑥 · 2) < (𝑃 / 2) ∧ (𝜑 ∧ 𝑥 ∈ (1...𝐻))) → (𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) ↔ 𝑦 = (𝑃 − (𝑥 · 2))))
55		eldifi 3285	. . . . . . . . . . . . . 14 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 𝑃 ∈ ℙ)
56		prmz 12279	. . . . . . . . . . . . . 14 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℤ)
57	19, 55, 56	3syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑃 ∈ ℤ)
58	57	ad2antrl 490	. . . . . . . . . . . 12 ⊢ ((¬ (𝑥 · 2) < (𝑃 / 2) ∧ (𝜑 ∧ 𝑥 ∈ (1...𝐻))) → 𝑃 ∈ ℤ)
59		elfzelz 10100	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (1...𝐻) → 𝑥 ∈ ℤ)
60	25	a1i 9	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (1...𝐻) → 2 ∈ ℤ)
61	59, 60	zmulcld 9454	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (1...𝐻) → (𝑥 · 2) ∈ ℤ)
62	61	ad2antll 491	. . . . . . . . . . . 12 ⊢ ((¬ (𝑥 · 2) < (𝑃 / 2) ∧ (𝜑 ∧ 𝑥 ∈ (1...𝐻))) → (𝑥 · 2) ∈ ℤ)
63	58, 62	zsubcld 9453	. . . . . . . . . . 11 ⊢ ((¬ (𝑥 · 2) < (𝑃 / 2) ∧ (𝜑 ∧ 𝑥 ∈ (1...𝐻))) → (𝑃 − (𝑥 · 2)) ∈ ℤ)
64	56	zred 9448	. . . . . . . . . . . . . 14 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℝ)
65	14	breq2i 4041	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ≤ 𝐻 ↔ 𝑥 ≤ ((𝑃 − 1) / 2))
66		nnre 8997	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ ℕ → 𝑥 ∈ ℝ)
67	66	adantr 276	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ) → 𝑥 ∈ ℝ)
68		peano2rem 8293	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑃 ∈ ℝ → (𝑃 − 1) ∈ ℝ)
69	68	adantl 277	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ) → (𝑃 − 1) ∈ ℝ)
70		2re 9060	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 2 ∈ ℝ
71		2pos 9081	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 0 < 2
72	70, 71	pm3.2i 272	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (2 ∈ ℝ ∧ 0 < 2)
73	72	a1i 9	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ) → (2 ∈ ℝ ∧ 0 < 2))
74		lemuldiv 8908	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ ℝ ∧ (𝑃 − 1) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((𝑥 · 2) ≤ (𝑃 − 1) ↔ 𝑥 ≤ ((𝑃 − 1) / 2)))
75	67, 69, 73, 74	syl3anc 1249	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ) → ((𝑥 · 2) ≤ (𝑃 − 1) ↔ 𝑥 ≤ ((𝑃 − 1) / 2)))
76	65, 75	bitr4id 199	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ) → (𝑥 ≤ 𝐻 ↔ (𝑥 · 2) ≤ (𝑃 − 1)))
77	11	nnred 9003	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ ℕ → (𝑥 · 2) ∈ ℝ)
78	77	adantr 276	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ) → (𝑥 · 2) ∈ ℝ)
79		simpr 110	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ) → 𝑃 ∈ ℝ)
80	78, 69, 79	lesub2d 8580	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ) → ((𝑥 · 2) ≤ (𝑃 − 1) ↔ (𝑃 − (𝑃 − 1)) ≤ (𝑃 − (𝑥 · 2))))
81		recn 8012	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑃 ∈ ℝ → 𝑃 ∈ ℂ)
82		1cnd 8042	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑃 ∈ ℝ → 1 ∈ ℂ)
83	81, 82	nncand 8342	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑃 ∈ ℝ → (𝑃 − (𝑃 − 1)) = 1)
84	83	adantl 277	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ) → (𝑃 − (𝑃 − 1)) = 1)
85	84	breq1d 4043	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ) → ((𝑃 − (𝑃 − 1)) ≤ (𝑃 − (𝑥 · 2)) ↔ 1 ≤ (𝑃 − (𝑥 · 2))))
86	85	biimpd 144	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ) → ((𝑃 − (𝑃 − 1)) ≤ (𝑃 − (𝑥 · 2)) → 1 ≤ (𝑃 − (𝑥 · 2))))
87	80, 86	sylbid 150	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ) → ((𝑥 · 2) ≤ (𝑃 − 1) → 1 ≤ (𝑃 − (𝑥 · 2))))
88	76, 87	sylbid 150	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ) → (𝑥 ≤ 𝐻 → 1 ≤ (𝑃 − (𝑥 · 2))))
89	88	impancom 260	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℕ ∧ 𝑥 ≤ 𝐻) → (𝑃 ∈ ℝ → 1 ≤ (𝑃 − (𝑥 · 2))))
90	89	3adant2 1018	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻) → (𝑃 ∈ ℝ → 1 ≤ (𝑃 − (𝑥 · 2))))
91	7, 90	sylbi 121	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (1...𝐻) → (𝑃 ∈ ℝ → 1 ≤ (𝑃 − (𝑥 · 2))))
92	91	com12 30	. . . . . . . . . . . . . 14 ⊢ (𝑃 ∈ ℝ → (𝑥 ∈ (1...𝐻) → 1 ≤ (𝑃 − (𝑥 · 2))))
93	19, 55, 64, 92	4syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑥 ∈ (1...𝐻) → 1 ≤ (𝑃 − (𝑥 · 2))))
94	93	imp 124	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝐻)) → 1 ≤ (𝑃 − (𝑥 · 2)))
95	94	adantl 277	. . . . . . . . . . 11 ⊢ ((¬ (𝑥 · 2) < (𝑃 / 2) ∧ (𝜑 ∧ 𝑥 ∈ (1...𝐻))) → 1 ≤ (𝑃 − (𝑥 · 2)))
96		elnnz1 9349	. . . . . . . . . . 11 ⊢ ((𝑃 − (𝑥 · 2)) ∈ ℕ ↔ ((𝑃 − (𝑥 · 2)) ∈ ℤ ∧ 1 ≤ (𝑃 − (𝑥 · 2))))
97	63, 95, 96	sylanbrc 417	. . . . . . . . . 10 ⊢ ((¬ (𝑥 · 2) < (𝑃 / 2) ∧ (𝜑 ∧ 𝑥 ∈ (1...𝐻))) → (𝑃 − (𝑥 · 2)) ∈ ℕ)
98	7	simp2bi 1015	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (1...𝐻) → 𝐻 ∈ ℕ)
99	98	ad2antll 491	. . . . . . . . . 10 ⊢ ((¬ (𝑥 · 2) < (𝑃 / 2) ∧ (𝜑 ∧ 𝑥 ∈ (1...𝐻))) → 𝐻 ∈ ℕ)
100		nnre 8997	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑃 ∈ ℕ → 𝑃 ∈ ℝ)
101	100	rehalfcld 9238	. . . . . . . . . . . . . . . . 17 ⊢ (𝑃 ∈ ℕ → (𝑃 / 2) ∈ ℝ)
102	101	adantr 276	. . . . . . . . . . . . . . . 16 ⊢ ((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) → (𝑃 / 2) ∈ ℝ)
103	61	zred 9448	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (1...𝐻) → (𝑥 · 2) ∈ ℝ)
104		lenlt 8102	. . . . . . . . . . . . . . . 16 ⊢ (((𝑃 / 2) ∈ ℝ ∧ (𝑥 · 2) ∈ ℝ) → ((𝑃 / 2) ≤ (𝑥 · 2) ↔ ¬ (𝑥 · 2) < (𝑃 / 2)))
105	102, 103, 104	syl2an 289	. . . . . . . . . . . . . . 15 ⊢ (((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → ((𝑃 / 2) ≤ (𝑥 · 2) ↔ ¬ (𝑥 · 2) < (𝑃 / 2)))
106	22, 61	anim12i 338	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → ((𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃) ∧ (𝑥 · 2) ∈ ℤ))
107	106, 30	sylibr 134	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → (𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ∧ (𝑥 · 2) ∈ ℤ))
108		halfleoddlt 12059	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ∧ (𝑥 · 2) ∈ ℤ) → ((𝑃 / 2) ≤ (𝑥 · 2) ↔ (𝑃 / 2) < (𝑥 · 2)))
109	107, 108	syl 14	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → ((𝑃 / 2) ≤ (𝑥 · 2) ↔ (𝑃 / 2) < (𝑥 · 2)))
110	109	biimpa 296	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) ∧ (𝑃 / 2) ≤ (𝑥 · 2)) → (𝑃 / 2) < (𝑥 · 2))
111		nncn 8998	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑃 ∈ ℕ → 𝑃 ∈ ℂ)
112		subhalfhalf 9226	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑃 ∈ ℂ → (𝑃 − (𝑃 / 2)) = (𝑃 / 2))
113	111, 112	syl 14	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑃 ∈ ℕ → (𝑃 − (𝑃 / 2)) = (𝑃 / 2))
114	113	breq1d 4043	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑃 ∈ ℕ → ((𝑃 − (𝑃 / 2)) < (𝑥 · 2) ↔ (𝑃 / 2) < (𝑥 · 2)))
115	114	ad3antrrr 492	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) ∧ (𝑃 / 2) ≤ (𝑥 · 2)) → ((𝑃 − (𝑃 / 2)) < (𝑥 · 2) ↔ (𝑃 / 2) < (𝑥 · 2)))
116	110, 115	mpbird 167	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) ∧ (𝑃 / 2) ≤ (𝑥 · 2)) → (𝑃 − (𝑃 / 2)) < (𝑥 · 2))
117	100	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → 𝑃 ∈ ℝ)
118	101	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → (𝑃 / 2) ∈ ℝ)
119	103	adantl 277	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → (𝑥 · 2) ∈ ℝ)
120	117, 118, 119	3jca 1179	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → (𝑃 ∈ ℝ ∧ (𝑃 / 2) ∈ ℝ ∧ (𝑥 · 2) ∈ ℝ))
121	120	adantr 276	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) ∧ (𝑃 / 2) ≤ (𝑥 · 2)) → (𝑃 ∈ ℝ ∧ (𝑃 / 2) ∈ ℝ ∧ (𝑥 · 2) ∈ ℝ))
122		ltsub23 8469	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑃 ∈ ℝ ∧ (𝑃 / 2) ∈ ℝ ∧ (𝑥 · 2) ∈ ℝ) → ((𝑃 − (𝑃 / 2)) < (𝑥 · 2) ↔ (𝑃 − (𝑥 · 2)) < (𝑃 / 2)))
123	121, 122	syl 14	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) ∧ (𝑃 / 2) ≤ (𝑥 · 2)) → ((𝑃 − (𝑃 / 2)) < (𝑥 · 2) ↔ (𝑃 − (𝑥 · 2)) < (𝑃 / 2)))
124	116, 123	mpbid 147	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) ∧ (𝑃 / 2) ≤ (𝑥 · 2)) → (𝑃 − (𝑥 · 2)) < (𝑃 / 2))
125	21	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → 𝑃 ∈ ℤ)
126		simplr 528	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → ¬ 2 ∥ 𝑃)
127	61	adantl 277	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → (𝑥 · 2) ∈ ℤ)
128	125, 127	zsubcld 9453	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → (𝑃 − (𝑥 · 2)) ∈ ℤ)
129	125, 126, 128	3jca 1179	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → (𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ∧ (𝑃 − (𝑥 · 2)) ∈ ℤ))
130	129	adantr 276	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) ∧ (𝑃 / 2) ≤ (𝑥 · 2)) → (𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ∧ (𝑃 − (𝑥 · 2)) ∈ ℤ))
131		ltoddhalfle 12058	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ∧ (𝑃 − (𝑥 · 2)) ∈ ℤ) → ((𝑃 − (𝑥 · 2)) < (𝑃 / 2) ↔ (𝑃 − (𝑥 · 2)) ≤ ((𝑃 − 1) / 2)))
132	130, 131	syl 14	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) ∧ (𝑃 / 2) ≤ (𝑥 · 2)) → ((𝑃 − (𝑥 · 2)) < (𝑃 / 2) ↔ (𝑃 − (𝑥 · 2)) ≤ ((𝑃 − 1) / 2)))
133	124, 132	mpbid 147	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) ∧ (𝑃 / 2) ≤ (𝑥 · 2)) → (𝑃 − (𝑥 · 2)) ≤ ((𝑃 − 1) / 2))
134	133	ex 115	. . . . . . . . . . . . . . . 16 ⊢ (((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → ((𝑃 / 2) ≤ (𝑥 · 2) → (𝑃 − (𝑥 · 2)) ≤ ((𝑃 − 1) / 2)))
135	14	breq2i 4041	. . . . . . . . . . . . . . . 16 ⊢ ((𝑃 − (𝑥 · 2)) ≤ 𝐻 ↔ (𝑃 − (𝑥 · 2)) ≤ ((𝑃 − 1) / 2))
136	134, 135	imbitrrdi 162	. . . . . . . . . . . . . . 15 ⊢ (((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → ((𝑃 / 2) ≤ (𝑥 · 2) → (𝑃 − (𝑥 · 2)) ≤ 𝐻))
137	105, 136	sylbird 170	. . . . . . . . . . . . . 14 ⊢ (((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) ∧ 𝑥 ∈ (1...𝐻)) → (¬ (𝑥 · 2) < (𝑃 / 2) → (𝑃 − (𝑥 · 2)) ≤ 𝐻))
138	137	ex 115	. . . . . . . . . . . . 13 ⊢ ((𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃) → (𝑥 ∈ (1...𝐻) → (¬ (𝑥 · 2) < (𝑃 / 2) → (𝑃 − (𝑥 · 2)) ≤ 𝐻)))
139	19, 20, 138	3syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑥 ∈ (1...𝐻) → (¬ (𝑥 · 2) < (𝑃 / 2) → (𝑃 − (𝑥 · 2)) ≤ 𝐻)))
140	139	imp 124	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝐻)) → (¬ (𝑥 · 2) < (𝑃 / 2) → (𝑃 − (𝑥 · 2)) ≤ 𝐻))
141	140	impcom 125	. . . . . . . . . 10 ⊢ ((¬ (𝑥 · 2) < (𝑃 / 2) ∧ (𝜑 ∧ 𝑥 ∈ (1...𝐻))) → (𝑃 − (𝑥 · 2)) ≤ 𝐻)
142		elfz1b 10165	. . . . . . . . . 10 ⊢ ((𝑃 − (𝑥 · 2)) ∈ (1...𝐻) ↔ ((𝑃 − (𝑥 · 2)) ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ (𝑃 − (𝑥 · 2)) ≤ 𝐻))
143	97, 99, 141, 142	syl3anbrc 1183	. . . . . . . . 9 ⊢ ((¬ (𝑥 · 2) < (𝑃 / 2) ∧ (𝜑 ∧ 𝑥 ∈ (1...𝐻))) → (𝑃 − (𝑥 · 2)) ∈ (1...𝐻))
144		eleq1 2259	. . . . . . . . 9 ⊢ (𝑦 = (𝑃 − (𝑥 · 2)) → (𝑦 ∈ (1...𝐻) ↔ (𝑃 − (𝑥 · 2)) ∈ (1...𝐻)))
145	143, 144	syl5ibrcom 157	. . . . . . . 8 ⊢ ((¬ (𝑥 · 2) < (𝑃 / 2) ∧ (𝜑 ∧ 𝑥 ∈ (1...𝐻))) → (𝑦 = (𝑃 − (𝑥 · 2)) → 𝑦 ∈ (1...𝐻)))
146	54, 145	sylbid 150	. . . . . . 7 ⊢ ((¬ (𝑥 · 2) < (𝑃 / 2) ∧ (𝜑 ∧ 𝑥 ∈ (1...𝐻))) → (𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) → 𝑦 ∈ (1...𝐻)))
147	146	ancoms 268	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝐻)) ∧ ¬ (𝑥 · 2) < (𝑃 / 2)) → (𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) → 𝑦 ∈ (1...𝐻)))
148	61	adantl 277	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝐻)) → (𝑥 · 2) ∈ ℤ)
149		zq 9700	. . . . . . . . 9 ⊢ ((𝑥 · 2) ∈ ℤ → (𝑥 · 2) ∈ ℚ)
150	148, 149	syl 14	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝐻)) → (𝑥 · 2) ∈ ℚ)
151	57	adantr 276	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝐻)) → 𝑃 ∈ ℤ)
152		znq 9698	. . . . . . . . 9 ⊢ ((𝑃 ∈ ℤ ∧ 2 ∈ ℕ) → (𝑃 / 2) ∈ ℚ)
153	151, 9, 152	sylancl 413	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝐻)) → (𝑃 / 2) ∈ ℚ)
154		qdclt 10335	. . . . . . . 8 ⊢ (((𝑥 · 2) ∈ ℚ ∧ (𝑃 / 2) ∈ ℚ) → DECID (𝑥 · 2) < (𝑃 / 2))
155	150, 153, 154	syl2anc 411	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝐻)) → DECID (𝑥 · 2) < (𝑃 / 2))
156		exmiddc 837	. . . . . . 7 ⊢ (DECID (𝑥 · 2) < (𝑃 / 2) → ((𝑥 · 2) < (𝑃 / 2) ∨ ¬ (𝑥 · 2) < (𝑃 / 2)))
157	155, 156	syl 14	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝐻)) → ((𝑥 · 2) < (𝑃 / 2) ∨ ¬ (𝑥 · 2) < (𝑃 / 2)))
158	51, 147, 157	mpjaodan 799	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝐻)) → (𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) → 𝑦 ∈ (1...𝐻)))
159	158	rexlimdva 2614	. . . 4 ⊢ (𝜑 → (∃𝑥 ∈ (1...𝐻)𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) → 𝑦 ∈ (1...𝐻)))
160		elfz1b 10165	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ (1...𝐻) ↔ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻))
161		simp1 999	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻) → 𝑦 ∈ ℕ)
162		simpl 109	. . . . . . . . . . . . . . 15 ⊢ ((2 ∥ 𝑦 ∧ 𝜑) → 2 ∥ 𝑦)
163		nnehalf 12069	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 ∈ ℕ ∧ 2 ∥ 𝑦) → (𝑦 / 2) ∈ ℕ)
164	161, 162, 163	syl2anr 290	. . . . . . . . . . . . . 14 ⊢ (((2 ∥ 𝑦 ∧ 𝜑) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻)) → (𝑦 / 2) ∈ ℕ)
165		simpr2 1006	. . . . . . . . . . . . . 14 ⊢ (((2 ∥ 𝑦 ∧ 𝜑) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻)) → 𝐻 ∈ ℕ)
166		nnre 8997	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ ℕ → 𝑦 ∈ ℝ)
167	166	ad2antrr 488	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) ∧ (2 ∥ 𝑦 ∧ 𝜑)) → 𝑦 ∈ ℝ)
168		nnrp 9738	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐻 ∈ ℕ → 𝐻 ∈ ℝ+)
169	168	adantl 277	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) → 𝐻 ∈ ℝ+)
170	169	adantr 276	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) ∧ (2 ∥ 𝑦 ∧ 𝜑)) → 𝐻 ∈ ℝ+)
171		2rp 9733	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 2 ∈ ℝ+
172		1le2 9199	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 1 ≤ 2
173	171, 172	pm3.2i 272	. . . . . . . . . . . . . . . . . . . 20 ⊢ (2 ∈ ℝ+ ∧ 1 ≤ 2)
174	173	a1i 9	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) ∧ (2 ∥ 𝑦 ∧ 𝜑)) → (2 ∈ ℝ+ ∧ 1 ≤ 2))
175		ledivge1le 9801	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑦 ∈ ℝ ∧ 𝐻 ∈ ℝ+ ∧ (2 ∈ ℝ+ ∧ 1 ≤ 2)) → (𝑦 ≤ 𝐻 → (𝑦 / 2) ≤ 𝐻))
176	167, 170, 174, 175	syl3anc 1249	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) ∧ (2 ∥ 𝑦 ∧ 𝜑)) → (𝑦 ≤ 𝐻 → (𝑦 / 2) ≤ 𝐻))
177	176	ex 115	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) → ((2 ∥ 𝑦 ∧ 𝜑) → (𝑦 ≤ 𝐻 → (𝑦 / 2) ≤ 𝐻)))
178	177	com23 78	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) → (𝑦 ≤ 𝐻 → ((2 ∥ 𝑦 ∧ 𝜑) → (𝑦 / 2) ≤ 𝐻)))
179	178	3impia 1202	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻) → ((2 ∥ 𝑦 ∧ 𝜑) → (𝑦 / 2) ≤ 𝐻))
180	179	impcom 125	. . . . . . . . . . . . . 14 ⊢ (((2 ∥ 𝑦 ∧ 𝜑) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻)) → (𝑦 / 2) ≤ 𝐻)
181	164, 165, 180	3jca 1179	. . . . . . . . . . . . 13 ⊢ (((2 ∥ 𝑦 ∧ 𝜑) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻)) → ((𝑦 / 2) ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ (𝑦 / 2) ≤ 𝐻))
182	181	ex 115	. . . . . . . . . . . 12 ⊢ ((2 ∥ 𝑦 ∧ 𝜑) → ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻) → ((𝑦 / 2) ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ (𝑦 / 2) ≤ 𝐻)))
183	160, 182	biimtrid 152	. . . . . . . . . . 11 ⊢ ((2 ∥ 𝑦 ∧ 𝜑) → (𝑦 ∈ (1...𝐻) → ((𝑦 / 2) ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ (𝑦 / 2) ≤ 𝐻)))
184	183	3impia 1202	. . . . . . . . . 10 ⊢ ((2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → ((𝑦 / 2) ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ (𝑦 / 2) ≤ 𝐻))
185		elfz1b 10165	. . . . . . . . . 10 ⊢ ((𝑦 / 2) ∈ (1...𝐻) ↔ ((𝑦 / 2) ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ (𝑦 / 2) ≤ 𝐻))
186	184, 185	sylibr 134	. . . . . . . . 9 ⊢ ((2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → (𝑦 / 2) ∈ (1...𝐻))
187		oveq1 5929	. . . . . . . . . . . . 13 ⊢ (𝑥 = (𝑦 / 2) → (𝑥 · 2) = ((𝑦 / 2) · 2))
188	187	breq1d 4043	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝑦 / 2) → ((𝑥 · 2) < (𝑃 / 2) ↔ ((𝑦 / 2) · 2) < (𝑃 / 2)))
189	187	oveq2d 5938	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝑦 / 2) → (𝑃 − (𝑥 · 2)) = (𝑃 − ((𝑦 / 2) · 2)))
190	188, 187, 189	ifbieq12d 3587	. . . . . . . . . . 11 ⊢ (𝑥 = (𝑦 / 2) → if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) = if(((𝑦 / 2) · 2) < (𝑃 / 2), ((𝑦 / 2) · 2), (𝑃 − ((𝑦 / 2) · 2))))
191	190	eqeq2d 2208	. . . . . . . . . 10 ⊢ (𝑥 = (𝑦 / 2) → (𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) ↔ 𝑦 = if(((𝑦 / 2) · 2) < (𝑃 / 2), ((𝑦 / 2) · 2), (𝑃 − ((𝑦 / 2) · 2)))))
192	191	adantl 277	. . . . . . . . 9 ⊢ (((2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) ∧ 𝑥 = (𝑦 / 2)) → (𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) ↔ 𝑦 = if(((𝑦 / 2) · 2) < (𝑃 / 2), ((𝑦 / 2) · 2), (𝑃 − ((𝑦 / 2) · 2)))))
193		elfzelz 10100	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ (1...𝐻) → 𝑦 ∈ ℤ)
194	193	zcnd 9449	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ (1...𝐻) → 𝑦 ∈ ℂ)
195	194	3ad2ant3 1022	. . . . . . . . . . . . 13 ⊢ ((2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → 𝑦 ∈ ℂ)
196		2cnd 9063	. . . . . . . . . . . . 13 ⊢ ((2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → 2 ∈ ℂ)
197		2ap0 9083	. . . . . . . . . . . . . 14 ⊢ 2 # 0
198	197	a1i 9	. . . . . . . . . . . . 13 ⊢ ((2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → 2 # 0)
199	195, 196, 198	divcanap1d 8818	. . . . . . . . . . . 12 ⊢ ((2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → ((𝑦 / 2) · 2) = 𝑦)
200	14	breq2i 4041	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ≤ 𝐻 ↔ 𝑦 ≤ ((𝑃 − 1) / 2))
201		nnz 9345	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ ℕ → 𝑦 ∈ ℤ)
202	19, 20, 22	3syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃))
203	202	adantl 277	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((2 ∥ 𝑦 ∧ 𝜑) → (𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃))
204	201, 203	anim12ci 339	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑦 ∈ ℕ ∧ (2 ∥ 𝑦 ∧ 𝜑)) → ((𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃) ∧ 𝑦 ∈ ℤ))
205		df-3an 982	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ∧ 𝑦 ∈ ℤ) ↔ ((𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃) ∧ 𝑦 ∈ ℤ))
206	204, 205	sylibr 134	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑦 ∈ ℕ ∧ (2 ∥ 𝑦 ∧ 𝜑)) → (𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ∧ 𝑦 ∈ ℤ))
207		ltoddhalfle 12058	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ∧ 𝑦 ∈ ℤ) → (𝑦 < (𝑃 / 2) ↔ 𝑦 ≤ ((𝑃 − 1) / 2)))
208	206, 207	syl 14	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑦 ∈ ℕ ∧ (2 ∥ 𝑦 ∧ 𝜑)) → (𝑦 < (𝑃 / 2) ↔ 𝑦 ≤ ((𝑃 − 1) / 2)))
209	208	exbiri 382	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ ℕ → ((2 ∥ 𝑦 ∧ 𝜑) → (𝑦 ≤ ((𝑃 − 1) / 2) → 𝑦 < (𝑃 / 2))))
210	209	com23 78	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ ℕ → (𝑦 ≤ ((𝑃 − 1) / 2) → ((2 ∥ 𝑦 ∧ 𝜑) → 𝑦 < (𝑃 / 2))))
211	200, 210	biimtrid 152	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ ℕ → (𝑦 ≤ 𝐻 → ((2 ∥ 𝑦 ∧ 𝜑) → 𝑦 < (𝑃 / 2))))
212	211	a1d 22	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ℕ → (𝐻 ∈ ℕ → (𝑦 ≤ 𝐻 → ((2 ∥ 𝑦 ∧ 𝜑) → 𝑦 < (𝑃 / 2)))))
213	212	3imp 1195	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻) → ((2 ∥ 𝑦 ∧ 𝜑) → 𝑦 < (𝑃 / 2)))
214	160, 213	sylbi 121	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ (1...𝐻) → ((2 ∥ 𝑦 ∧ 𝜑) → 𝑦 < (𝑃 / 2)))
215	214	com12 30	. . . . . . . . . . . . 13 ⊢ ((2 ∥ 𝑦 ∧ 𝜑) → (𝑦 ∈ (1...𝐻) → 𝑦 < (𝑃 / 2)))
216	215	3impia 1202	. . . . . . . . . . . 12 ⊢ ((2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → 𝑦 < (𝑃 / 2))
217	199, 216	eqbrtrd 4055	. . . . . . . . . . 11 ⊢ ((2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → ((𝑦 / 2) · 2) < (𝑃 / 2))
218	217	iftrued 3568	. . . . . . . . . 10 ⊢ ((2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → if(((𝑦 / 2) · 2) < (𝑃 / 2), ((𝑦 / 2) · 2), (𝑃 − ((𝑦 / 2) · 2))) = ((𝑦 / 2) · 2))
219	218, 199	eqtr2d 2230	. . . . . . . . 9 ⊢ ((2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → 𝑦 = if(((𝑦 / 2) · 2) < (𝑃 / 2), ((𝑦 / 2) · 2), (𝑃 − ((𝑦 / 2) · 2))))
220	186, 192, 219	rspcedvd 2874	. . . . . . . 8 ⊢ ((2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → ∃𝑥 ∈ (1...𝐻)𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))))
221	220	3expb 1206	. . . . . . 7 ⊢ ((2 ∥ 𝑦 ∧ (𝜑 ∧ 𝑦 ∈ (1...𝐻))) → ∃𝑥 ∈ (1...𝐻)𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))))
222	221	ancoms 268	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ (1...𝐻)) ∧ 2 ∥ 𝑦) → ∃𝑥 ∈ (1...𝐻)𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))))
223	55, 56	syl 14	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 𝑃 ∈ ℤ)
224	223	ad2antrr 488	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻)) → 𝑃 ∈ ℤ)
225	201	3ad2ant1 1020	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻) → 𝑦 ∈ ℤ)
226	225	adantl 277	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻)) → 𝑦 ∈ ℤ)
227	224, 226	zsubcld 9453	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻)) → (𝑃 − 𝑦) ∈ ℤ)
228	166	ad2antrl 490	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑃 ∈ ℝ ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ)) → 𝑦 ∈ ℝ)
229	68	rehalfcld 9238	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑃 ∈ ℝ → ((𝑃 − 1) / 2) ∈ ℝ)
230	229	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑃 ∈ ℝ ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ)) → ((𝑃 − 1) / 2) ∈ ℝ)
231		simpl 109	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑃 ∈ ℝ ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ)) → 𝑃 ∈ ℝ)
232	228, 230, 231	3jca 1179	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑃 ∈ ℝ ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ)) → (𝑦 ∈ ℝ ∧ ((𝑃 − 1) / 2) ∈ ℝ ∧ 𝑃 ∈ ℝ))
233	232	ex 115	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑃 ∈ ℝ → ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) → (𝑦 ∈ ℝ ∧ ((𝑃 − 1) / 2) ∈ ℝ ∧ 𝑃 ∈ ℝ)))
234	55, 64, 233	3syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) → (𝑦 ∈ ℝ ∧ ((𝑃 − 1) / 2) ∈ ℝ ∧ 𝑃 ∈ ℝ)))
235	234	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) → ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) → (𝑦 ∈ ℝ ∧ ((𝑃 − 1) / 2) ∈ ℝ ∧ 𝑃 ∈ ℝ)))
236	235	impcom 125	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) ∧ (𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦)) → (𝑦 ∈ ℝ ∧ ((𝑃 − 1) / 2) ∈ ℝ ∧ 𝑃 ∈ ℝ))
237		lesub2 8484	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑦 ∈ ℝ ∧ ((𝑃 − 1) / 2) ∈ ℝ ∧ 𝑃 ∈ ℝ) → (𝑦 ≤ ((𝑃 − 1) / 2) ↔ (𝑃 − ((𝑃 − 1) / 2)) ≤ (𝑃 − 𝑦)))
238	236, 237	syl 14	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) ∧ (𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦)) → (𝑦 ≤ ((𝑃 − 1) / 2) ↔ (𝑃 − ((𝑃 − 1) / 2)) ≤ (𝑃 − 𝑦)))
239	56	zcnd 9449	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℂ)
240		id 19	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑃 ∈ ℂ → 𝑃 ∈ ℂ)
241		1cnd 8042	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑃 ∈ ℂ → 1 ∈ ℂ)
242		2cnd 9063	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑃 ∈ ℂ → 2 ∈ ℂ)
243	197	a1i 9	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑃 ∈ ℂ → 2 # 0)
244	240, 241, 242, 243	divsubdirapd 8857	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑃 ∈ ℂ → ((𝑃 − 1) / 2) = ((𝑃 / 2) − (1 / 2)))
245	244	oveq2d 5938	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑃 ∈ ℂ → (𝑃 − ((𝑃 − 1) / 2)) = (𝑃 − ((𝑃 / 2) − (1 / 2))))
246		halfcl 9217	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑃 ∈ ℂ → (𝑃 / 2) ∈ ℂ)
247		halfcn 9205	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (1 / 2) ∈ ℂ
248	247	a1i 9	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑃 ∈ ℂ → (1 / 2) ∈ ℂ)
249	240, 246, 248	subsubd 8365	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑃 ∈ ℂ → (𝑃 − ((𝑃 / 2) − (1 / 2))) = ((𝑃 − (𝑃 / 2)) + (1 / 2)))
250	112	oveq1d 5937	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑃 ∈ ℂ → ((𝑃 − (𝑃 / 2)) + (1 / 2)) = ((𝑃 / 2) + (1 / 2)))
251	245, 249, 250	3eqtrd 2233	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑃 ∈ ℂ → (𝑃 − ((𝑃 − 1) / 2)) = ((𝑃 / 2) + (1 / 2)))
252	55, 239, 251	3syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (𝑃 − ((𝑃 − 1) / 2)) = ((𝑃 / 2) + (1 / 2)))
253	252	ad2antrl 490	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) ∧ (𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦)) → (𝑃 − ((𝑃 − 1) / 2)) = ((𝑃 / 2) + (1 / 2)))
254	253	breq1d 4043	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) ∧ (𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦)) → ((𝑃 − ((𝑃 − 1) / 2)) ≤ (𝑃 − 𝑦) ↔ ((𝑃 / 2) + (1 / 2)) ≤ (𝑃 − 𝑦)))
255		prmnn 12278	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
256		halfre 9204	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (1 / 2) ∈ ℝ
257	256	a1i 9	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑃 ∈ ℕ → (1 / 2) ∈ ℝ)
258		nngt0 9015	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑃 ∈ ℕ → 0 < 𝑃)
259	72	a1i 9	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑃 ∈ ℕ → (2 ∈ ℝ ∧ 0 < 2))
260		divgt0 8899	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝑃 ∈ ℝ ∧ 0 < 𝑃) ∧ (2 ∈ ℝ ∧ 0 < 2)) → 0 < (𝑃 / 2))
261	100, 258, 259, 260	syl21anc 1248	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑃 ∈ ℕ → 0 < (𝑃 / 2))
262		halfgt0 9206	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ 0 < (1 / 2)
263	262	a1i 9	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑃 ∈ ℕ → 0 < (1 / 2))
264	101, 257, 261, 263	addgt0d 8548	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑃 ∈ ℕ → 0 < ((𝑃 / 2) + (1 / 2)))
265	55, 255, 264	3syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 0 < ((𝑃 / 2) + (1 / 2)))
266	265	ad2antrl 490	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) ∧ (𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦)) → 0 < ((𝑃 / 2) + (1 / 2)))
267		0red 8027	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → 0 ∈ ℝ)
268		simpr 110	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → 𝑃 ∈ ℝ)
269	268	rehalfcld 9238	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → (𝑃 / 2) ∈ ℝ)
270	256	a1i 9	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → (1 / 2) ∈ ℝ)
271	269, 270	readdcld 8056	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → ((𝑃 / 2) + (1 / 2)) ∈ ℝ)
272		resubcl 8290	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝑃 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑃 − 𝑦) ∈ ℝ)
273	272	ancoms 268	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → (𝑃 − 𝑦) ∈ ℝ)
274	267, 271, 273	3jca 1179	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → (0 ∈ ℝ ∧ ((𝑃 / 2) + (1 / 2)) ∈ ℝ ∧ (𝑃 − 𝑦) ∈ ℝ))
275	274	ex 115	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑦 ∈ ℝ → (𝑃 ∈ ℝ → (0 ∈ ℝ ∧ ((𝑃 / 2) + (1 / 2)) ∈ ℝ ∧ (𝑃 − 𝑦) ∈ ℝ)))
276	166, 275	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑦 ∈ ℕ → (𝑃 ∈ ℝ → (0 ∈ ℝ ∧ ((𝑃 / 2) + (1 / 2)) ∈ ℝ ∧ (𝑃 − 𝑦) ∈ ℝ)))
277	276	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) → (𝑃 ∈ ℝ → (0 ∈ ℝ ∧ ((𝑃 / 2) + (1 / 2)) ∈ ℝ ∧ (𝑃 − 𝑦) ∈ ℝ)))
278	277	com12 30	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑃 ∈ ℝ → ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) → (0 ∈ ℝ ∧ ((𝑃 / 2) + (1 / 2)) ∈ ℝ ∧ (𝑃 − 𝑦) ∈ ℝ)))
279	55, 64, 278	3syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) → (0 ∈ ℝ ∧ ((𝑃 / 2) + (1 / 2)) ∈ ℝ ∧ (𝑃 − 𝑦) ∈ ℝ)))
280	279	adantr 276	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) → ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) → (0 ∈ ℝ ∧ ((𝑃 / 2) + (1 / 2)) ∈ ℝ ∧ (𝑃 − 𝑦) ∈ ℝ)))
281	280	impcom 125	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) ∧ (𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦)) → (0 ∈ ℝ ∧ ((𝑃 / 2) + (1 / 2)) ∈ ℝ ∧ (𝑃 − 𝑦) ∈ ℝ))
282		ltletr 8116	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((0 ∈ ℝ ∧ ((𝑃 / 2) + (1 / 2)) ∈ ℝ ∧ (𝑃 − 𝑦) ∈ ℝ) → ((0 < ((𝑃 / 2) + (1 / 2)) ∧ ((𝑃 / 2) + (1 / 2)) ≤ (𝑃 − 𝑦)) → 0 < (𝑃 − 𝑦)))
283	281, 282	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) ∧ (𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦)) → ((0 < ((𝑃 / 2) + (1 / 2)) ∧ ((𝑃 / 2) + (1 / 2)) ≤ (𝑃 − 𝑦)) → 0 < (𝑃 − 𝑦)))
284	266, 283	mpand 429	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) ∧ (𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦)) → (((𝑃 / 2) + (1 / 2)) ≤ (𝑃 − 𝑦) → 0 < (𝑃 − 𝑦)))
285	254, 284	sylbid 150	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) ∧ (𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦)) → ((𝑃 − ((𝑃 − 1) / 2)) ≤ (𝑃 − 𝑦) → 0 < (𝑃 − 𝑦)))
286	238, 285	sylbid 150	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) ∧ (𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦)) → (𝑦 ≤ ((𝑃 − 1) / 2) → 0 < (𝑃 − 𝑦)))
287	286	ex 115	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) → ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) → (𝑦 ≤ ((𝑃 − 1) / 2) → 0 < (𝑃 − 𝑦))))
288	287	com23 78	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) → (𝑦 ≤ ((𝑃 − 1) / 2) → ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) → 0 < (𝑃 − 𝑦))))
289	200, 288	biimtrid 152	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ) → (𝑦 ≤ 𝐻 → ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) → 0 < (𝑃 − 𝑦))))
290	289	3impia 1202	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻) → ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) → 0 < (𝑃 − 𝑦)))
291	290	impcom 125	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻)) → 0 < (𝑃 − 𝑦))
292		elnnz 9336	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑃 − 𝑦) ∈ ℕ ↔ ((𝑃 − 𝑦) ∈ ℤ ∧ 0 < (𝑃 − 𝑦)))
293	227, 291, 292	sylanbrc 417	. . . . . . . . . . . . . . . 16 ⊢ (((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻)) → (𝑃 − 𝑦) ∈ ℕ)
294	23	adantr 276	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) → (𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃))
295		simpr 110	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) → ¬ 2 ∥ 𝑦)
296	295, 225	anim12ci 339	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻)) → (𝑦 ∈ ℤ ∧ ¬ 2 ∥ 𝑦))
297		omoe 12061	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃) ∧ (𝑦 ∈ ℤ ∧ ¬ 2 ∥ 𝑦)) → 2 ∥ (𝑃 − 𝑦))
298	294, 296, 297	syl2an2r 595	. . . . . . . . . . . . . . . 16 ⊢ (((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻)) → 2 ∥ (𝑃 − 𝑦))
299		nnehalf 12069	. . . . . . . . . . . . . . . 16 ⊢ (((𝑃 − 𝑦) ∈ ℕ ∧ 2 ∥ (𝑃 − 𝑦)) → ((𝑃 − 𝑦) / 2) ∈ ℕ)
300	293, 298, 299	syl2anc 411	. . . . . . . . . . . . . . 15 ⊢ (((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻)) → ((𝑃 − 𝑦) / 2) ∈ ℕ)
301		simpr2 1006	. . . . . . . . . . . . . . 15 ⊢ (((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻)) → 𝐻 ∈ ℕ)
302		1red 8041	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻)) → 1 ∈ ℝ)
303	166	3ad2ant1 1020	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻) → 𝑦 ∈ ℝ)
304	303	adantl 277	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻)) → 𝑦 ∈ ℝ)
305	55, 64	syl 14	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → 𝑃 ∈ ℝ)
306	305	ad2antrr 488	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻)) → 𝑃 ∈ ℝ)
307		nnge1 9013	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ ℕ → 1 ≤ 𝑦)
308	307	3ad2ant1 1020	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻) → 1 ≤ 𝑦)
309	308	adantl 277	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻)) → 1 ≤ 𝑦)
310	302, 304, 306, 309	lesub2dd 8589	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻)) → (𝑃 − 𝑦) ≤ (𝑃 − 1))
311	306, 304	resubcld 8407	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻)) → (𝑃 − 𝑦) ∈ ℝ)
312	55, 64, 68	3syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (𝑃 − 1) ∈ ℝ)
313	312	ad2antrr 488	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻)) → (𝑃 − 1) ∈ ℝ)
314	72	a1i 9	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻)) → (2 ∈ ℝ ∧ 0 < 2))
315		lediv1 8896	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑃 − 𝑦) ∈ ℝ ∧ (𝑃 − 1) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((𝑃 − 𝑦) ≤ (𝑃 − 1) ↔ ((𝑃 − 𝑦) / 2) ≤ ((𝑃 − 1) / 2)))
316	311, 313, 314, 315	syl3anc 1249	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻)) → ((𝑃 − 𝑦) ≤ (𝑃 − 1) ↔ ((𝑃 − 𝑦) / 2) ≤ ((𝑃 − 1) / 2)))
317	310, 316	mpbid 147	. . . . . . . . . . . . . . . 16 ⊢ (((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻)) → ((𝑃 − 𝑦) / 2) ≤ ((𝑃 − 1) / 2))
318	14	breq2i 4041	. . . . . . . . . . . . . . . 16 ⊢ (((𝑃 − 𝑦) / 2) ≤ 𝐻 ↔ ((𝑃 − 𝑦) / 2) ≤ ((𝑃 − 1) / 2))
319	317, 318	sylibr 134	. . . . . . . . . . . . . . 15 ⊢ (((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻)) → ((𝑃 − 𝑦) / 2) ≤ 𝐻)
320	300, 301, 319	3jca 1179	. . . . . . . . . . . . . 14 ⊢ (((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) ∧ (𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻)) → (((𝑃 − 𝑦) / 2) ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ ((𝑃 − 𝑦) / 2) ≤ 𝐻))
321	320	ex 115	. . . . . . . . . . . . 13 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) → ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻) → (((𝑃 − 𝑦) / 2) ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ ((𝑃 − 𝑦) / 2) ≤ 𝐻)))
322		elfz1b 10165	. . . . . . . . . . . . 13 ⊢ (((𝑃 − 𝑦) / 2) ∈ (1...𝐻) ↔ (((𝑃 − 𝑦) / 2) ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ ((𝑃 − 𝑦) / 2) ≤ 𝐻))
323	321, 160, 322	3imtr4g 205	. . . . . . . . . . . 12 ⊢ ((𝑃 ∈ (ℙ ∖ {2}) ∧ ¬ 2 ∥ 𝑦) → (𝑦 ∈ (1...𝐻) → ((𝑃 − 𝑦) / 2) ∈ (1...𝐻)))
324	323	ex 115	. . . . . . . . . . 11 ⊢ (𝑃 ∈ (ℙ ∖ {2}) → (¬ 2 ∥ 𝑦 → (𝑦 ∈ (1...𝐻) → ((𝑃 − 𝑦) / 2) ∈ (1...𝐻))))
325	19, 324	syl 14	. . . . . . . . . 10 ⊢ (𝜑 → (¬ 2 ∥ 𝑦 → (𝑦 ∈ (1...𝐻) → ((𝑃 − 𝑦) / 2) ∈ (1...𝐻))))
326	325	3imp21 1200	. . . . . . . . 9 ⊢ ((¬ 2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → ((𝑃 − 𝑦) / 2) ∈ (1...𝐻))
327		oveq1 5929	. . . . . . . . . . . . 13 ⊢ (𝑥 = ((𝑃 − 𝑦) / 2) → (𝑥 · 2) = (((𝑃 − 𝑦) / 2) · 2))
328	327	breq1d 4043	. . . . . . . . . . . 12 ⊢ (𝑥 = ((𝑃 − 𝑦) / 2) → ((𝑥 · 2) < (𝑃 / 2) ↔ (((𝑃 − 𝑦) / 2) · 2) < (𝑃 / 2)))
329	327	oveq2d 5938	. . . . . . . . . . . 12 ⊢ (𝑥 = ((𝑃 − 𝑦) / 2) → (𝑃 − (𝑥 · 2)) = (𝑃 − (((𝑃 − 𝑦) / 2) · 2)))
330	328, 327, 329	ifbieq12d 3587	. . . . . . . . . . 11 ⊢ (𝑥 = ((𝑃 − 𝑦) / 2) → if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) = if((((𝑃 − 𝑦) / 2) · 2) < (𝑃 / 2), (((𝑃 − 𝑦) / 2) · 2), (𝑃 − (((𝑃 − 𝑦) / 2) · 2))))
331	330	eqeq2d 2208	. . . . . . . . . 10 ⊢ (𝑥 = ((𝑃 − 𝑦) / 2) → (𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) ↔ 𝑦 = if((((𝑃 − 𝑦) / 2) · 2) < (𝑃 / 2), (((𝑃 − 𝑦) / 2) · 2), (𝑃 − (((𝑃 − 𝑦) / 2) · 2)))))
332	331	adantl 277	. . . . . . . . 9 ⊢ (((¬ 2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) ∧ 𝑥 = ((𝑃 − 𝑦) / 2)) → (𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) ↔ 𝑦 = if((((𝑃 − 𝑦) / 2) · 2) < (𝑃 / 2), (((𝑃 − 𝑦) / 2) · 2), (𝑃 − (((𝑃 − 𝑦) / 2) · 2)))))
333	19, 55, 239	3syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑃 ∈ ℂ)
334	333	3ad2ant2 1021	. . . . . . . . . . . . . 14 ⊢ ((¬ 2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → 𝑃 ∈ ℂ)
335	194	3ad2ant3 1022	. . . . . . . . . . . . . 14 ⊢ ((¬ 2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → 𝑦 ∈ ℂ)
336	334, 335	subcld 8337	. . . . . . . . . . . . 13 ⊢ ((¬ 2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → (𝑃 − 𝑦) ∈ ℂ)
337		2cnd 9063	. . . . . . . . . . . . 13 ⊢ ((¬ 2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → 2 ∈ ℂ)
338	197	a1i 9	. . . . . . . . . . . . 13 ⊢ ((¬ 2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → 2 # 0)
339	336, 337, 338	divcanap1d 8818	. . . . . . . . . . . 12 ⊢ ((¬ 2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → (((𝑃 − 𝑦) / 2) · 2) = (𝑃 − 𝑦))
340		zre 9330	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑃 ∈ ℤ → 𝑃 ∈ ℝ)
341		halfge0 9207	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ 0 ≤ (1 / 2)
342		rehalfcl 9218	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑃 ∈ ℝ → (𝑃 / 2) ∈ ℝ)
343	342	adantl 277	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → (𝑃 / 2) ∈ ℝ)
344	343, 270	subge02d 8564	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → (0 ≤ (1 / 2) ↔ ((𝑃 / 2) − (1 / 2)) ≤ (𝑃 / 2)))
345	341, 344	mpbii 148	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → ((𝑃 / 2) − (1 / 2)) ≤ (𝑃 / 2))
346		simpl 109	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → 𝑦 ∈ ℝ)
347	256	a1i 9	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑃 ∈ ℝ → (1 / 2) ∈ ℝ)
348	342, 347	resubcld 8407	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑃 ∈ ℝ → ((𝑃 / 2) − (1 / 2)) ∈ ℝ)
349	348	adantl 277	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → ((𝑃 / 2) − (1 / 2)) ∈ ℝ)
350		letr 8109	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑦 ∈ ℝ ∧ ((𝑃 / 2) − (1 / 2)) ∈ ℝ ∧ (𝑃 / 2) ∈ ℝ) → ((𝑦 ≤ ((𝑃 / 2) − (1 / 2)) ∧ ((𝑃 / 2) − (1 / 2)) ≤ (𝑃 / 2)) → 𝑦 ≤ (𝑃 / 2)))
351	346, 349, 343, 350	syl3anc 1249	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → ((𝑦 ≤ ((𝑃 / 2) − (1 / 2)) ∧ ((𝑃 / 2) − (1 / 2)) ≤ (𝑃 / 2)) → 𝑦 ≤ (𝑃 / 2)))
352	345, 351	mpan2d 428	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → (𝑦 ≤ ((𝑃 / 2) − (1 / 2)) → 𝑦 ≤ (𝑃 / 2)))
353	81	adantl 277	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → 𝑃 ∈ ℂ)
354	353, 244	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → ((𝑃 − 1) / 2) = ((𝑃 / 2) − (1 / 2)))
355	354	breq2d 4045	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → (𝑦 ≤ ((𝑃 − 1) / 2) ↔ 𝑦 ≤ ((𝑃 / 2) − (1 / 2))))
356		lesub 8468	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝑃 / 2) ∈ ℝ ∧ 𝑃 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((𝑃 / 2) ≤ (𝑃 − 𝑦) ↔ 𝑦 ≤ (𝑃 − (𝑃 / 2))))
357	343, 268, 346, 356	syl3anc 1249	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → ((𝑃 / 2) ≤ (𝑃 − 𝑦) ↔ 𝑦 ≤ (𝑃 − (𝑃 / 2))))
358	269, 273	lenltd 8144	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → ((𝑃 / 2) ≤ (𝑃 − 𝑦) ↔ ¬ (𝑃 − 𝑦) < (𝑃 / 2)))
359		2cnd 9063	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑃 ∈ ℝ → 2 ∈ ℂ)
360	197	a1i 9	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑃 ∈ ℝ → 2 # 0)
361	81, 359, 360	divcanap1d 8818	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑃 ∈ ℝ → ((𝑃 / 2) · 2) = 𝑃)
362	361	eqcomd 2202	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑃 ∈ ℝ → 𝑃 = ((𝑃 / 2) · 2))
363	362	oveq1d 5937	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑃 ∈ ℝ → (𝑃 − (𝑃 / 2)) = (((𝑃 / 2) · 2) − (𝑃 / 2)))
364	342	recnd 8055	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑃 ∈ ℝ → (𝑃 / 2) ∈ ℂ)
365	364, 359	mulcomd 8048	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑃 ∈ ℝ → ((𝑃 / 2) · 2) = (2 · (𝑃 / 2)))
366	365	oveq1d 5937	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑃 ∈ ℝ → (((𝑃 / 2) · 2) − (𝑃 / 2)) = ((2 · (𝑃 / 2)) − (𝑃 / 2)))
367	359, 364	mulsubfacd 8445	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑃 ∈ ℝ → ((2 · (𝑃 / 2)) − (𝑃 / 2)) = ((2 − 1) · (𝑃 / 2)))
368		2m1e1 9108	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (2 − 1) = 1
369	368	a1i 9	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑃 ∈ ℝ → (2 − 1) = 1)
370	369	oveq1d 5937	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑃 ∈ ℝ → ((2 − 1) · (𝑃 / 2)) = (1 · (𝑃 / 2)))
371	364	mullidd 8044	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑃 ∈ ℝ → (1 · (𝑃 / 2)) = (𝑃 / 2))
372	367, 370, 371	3eqtrd 2233	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑃 ∈ ℝ → ((2 · (𝑃 / 2)) − (𝑃 / 2)) = (𝑃 / 2))
373	363, 366, 372	3eqtrd 2233	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑃 ∈ ℝ → (𝑃 − (𝑃 / 2)) = (𝑃 / 2))
374	373	adantl 277	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → (𝑃 − (𝑃 / 2)) = (𝑃 / 2))
375	374	breq2d 4045	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → (𝑦 ≤ (𝑃 − (𝑃 / 2)) ↔ 𝑦 ≤ (𝑃 / 2)))
376	357, 358, 375	3bitr3d 218	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → (¬ (𝑃 − 𝑦) < (𝑃 / 2) ↔ 𝑦 ≤ (𝑃 / 2)))
377	352, 355, 376	3imtr4d 203	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ) → (𝑦 ≤ ((𝑃 − 1) / 2) → ¬ (𝑃 − 𝑦) < (𝑃 / 2)))
378	377	ex 115	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ∈ ℝ → (𝑃 ∈ ℝ → (𝑦 ≤ ((𝑃 − 1) / 2) → ¬ (𝑃 − 𝑦) < (𝑃 / 2))))
379	166, 378	syl 14	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ ℕ → (𝑃 ∈ ℝ → (𝑦 ≤ ((𝑃 − 1) / 2) → ¬ (𝑃 − 𝑦) < (𝑃 / 2))))
380	379	com3l 81	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑃 ∈ ℝ → (𝑦 ≤ ((𝑃 − 1) / 2) → (𝑦 ∈ ℕ → ¬ (𝑃 − 𝑦) < (𝑃 / 2))))
381	340, 380	syl 14	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑃 ∈ ℤ → (𝑦 ≤ ((𝑃 − 1) / 2) → (𝑦 ∈ ℕ → ¬ (𝑃 − 𝑦) < (𝑃 / 2))))
382	19, 55, 56, 381	4syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑦 ≤ ((𝑃 − 1) / 2) → (𝑦 ∈ ℕ → ¬ (𝑃 − 𝑦) < (𝑃 / 2))))
383	382	adantl 277	. . . . . . . . . . . . . . . . . . 19 ⊢ ((¬ 2 ∥ 𝑦 ∧ 𝜑) → (𝑦 ≤ ((𝑃 − 1) / 2) → (𝑦 ∈ ℕ → ¬ (𝑃 − 𝑦) < (𝑃 / 2))))
384	383	com13 80	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ ℕ → (𝑦 ≤ ((𝑃 − 1) / 2) → ((¬ 2 ∥ 𝑦 ∧ 𝜑) → ¬ (𝑃 − 𝑦) < (𝑃 / 2))))
385	200, 384	biimtrid 152	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ ℕ → (𝑦 ≤ 𝐻 → ((¬ 2 ∥ 𝑦 ∧ 𝜑) → ¬ (𝑃 − 𝑦) < (𝑃 / 2))))
386	385	a1d 22	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ℕ → (𝐻 ∈ ℕ → (𝑦 ≤ 𝐻 → ((¬ 2 ∥ 𝑦 ∧ 𝜑) → ¬ (𝑃 − 𝑦) < (𝑃 / 2)))))
387	386	3imp 1195	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻) → ((¬ 2 ∥ 𝑦 ∧ 𝜑) → ¬ (𝑃 − 𝑦) < (𝑃 / 2)))
388	387	com12 30	. . . . . . . . . . . . . 14 ⊢ ((¬ 2 ∥ 𝑦 ∧ 𝜑) → ((𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻) → ¬ (𝑃 − 𝑦) < (𝑃 / 2)))
389	160, 388	biimtrid 152	. . . . . . . . . . . . 13 ⊢ ((¬ 2 ∥ 𝑦 ∧ 𝜑) → (𝑦 ∈ (1...𝐻) → ¬ (𝑃 − 𝑦) < (𝑃 / 2)))
390	389	3impia 1202	. . . . . . . . . . . 12 ⊢ ((¬ 2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → ¬ (𝑃 − 𝑦) < (𝑃 / 2))
391	339, 390	eqnbrtrd 4051	. . . . . . . . . . 11 ⊢ ((¬ 2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → ¬ (((𝑃 − 𝑦) / 2) · 2) < (𝑃 / 2))
392	391	iffalsed 3571	. . . . . . . . . 10 ⊢ ((¬ 2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → if((((𝑃 − 𝑦) / 2) · 2) < (𝑃 / 2), (((𝑃 − 𝑦) / 2) · 2), (𝑃 − (((𝑃 − 𝑦) / 2) · 2))) = (𝑃 − (((𝑃 − 𝑦) / 2) · 2)))
393	339	oveq2d 5938	. . . . . . . . . 10 ⊢ ((¬ 2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → (𝑃 − (((𝑃 − 𝑦) / 2) · 2)) = (𝑃 − (𝑃 − 𝑦)))
394	333, 194	anim12i 338	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...𝐻)) → (𝑃 ∈ ℂ ∧ 𝑦 ∈ ℂ))
395	394	3adant1 1017	. . . . . . . . . . 11 ⊢ ((¬ 2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → (𝑃 ∈ ℂ ∧ 𝑦 ∈ ℂ))
396		nncan 8255	. . . . . . . . . . 11 ⊢ ((𝑃 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑃 − (𝑃 − 𝑦)) = 𝑦)
397	395, 396	syl 14	. . . . . . . . . 10 ⊢ ((¬ 2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → (𝑃 − (𝑃 − 𝑦)) = 𝑦)
398	392, 393, 397	3eqtrrd 2234	. . . . . . . . 9 ⊢ ((¬ 2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → 𝑦 = if((((𝑃 − 𝑦) / 2) · 2) < (𝑃 / 2), (((𝑃 − 𝑦) / 2) · 2), (𝑃 − (((𝑃 − 𝑦) / 2) · 2))))
399	326, 332, 398	rspcedvd 2874	. . . . . . . 8 ⊢ ((¬ 2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ (1...𝐻)) → ∃𝑥 ∈ (1...𝐻)𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))))
400	399	3expb 1206	. . . . . . 7 ⊢ ((¬ 2 ∥ 𝑦 ∧ (𝜑 ∧ 𝑦 ∈ (1...𝐻))) → ∃𝑥 ∈ (1...𝐻)𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))))
401	400	ancoms 268	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ (1...𝐻)) ∧ ¬ 2 ∥ 𝑦) → ∃𝑥 ∈ (1...𝐻)𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))))
402	9	a1i 9	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...𝐻)) → 2 ∈ ℕ)
403	193	adantl 277	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...𝐻)) → 𝑦 ∈ ℤ)
404		dvdsdc 11963	. . . . . . . 8 ⊢ ((2 ∈ ℕ ∧ 𝑦 ∈ ℤ) → DECID 2 ∥ 𝑦)
405	402, 403, 404	syl2anc 411	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...𝐻)) → DECID 2 ∥ 𝑦)
406		exmiddc 837	. . . . . . 7 ⊢ (DECID 2 ∥ 𝑦 → (2 ∥ 𝑦 ∨ ¬ 2 ∥ 𝑦))
407	405, 406	syl 14	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...𝐻)) → (2 ∥ 𝑦 ∨ ¬ 2 ∥ 𝑦))
408	222, 401, 407	mpjaodan 799	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ (1...𝐻)) → ∃𝑥 ∈ (1...𝐻)𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))))
409	408	ex 115	. . . 4 ⊢ (𝜑 → (𝑦 ∈ (1...𝐻) → ∃𝑥 ∈ (1...𝐻)𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2)))))
410	159, 409	impbid 129	. . 3 ⊢ (𝜑 → (∃𝑥 ∈ (1...𝐻)𝑦 = if((𝑥 · 2) < (𝑃 / 2), (𝑥 · 2), (𝑃 − (𝑥 · 2))) ↔ 𝑦 ∈ (1...𝐻)))
411	3, 410	bitrid 192	. 2 ⊢ (𝜑 → (𝑦 ∈ ran 𝑅 ↔ 𝑦 ∈ (1...𝐻)))
412	411	eqrdv 2194	1 ⊢ (𝜑 → ran 𝑅 = (1...𝐻))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 104   ↔ wb 105   ∨ wo 709  DECID wdc 835   ∧ w3a 980   = wceq 1364   ∈ wcel 2167  ∃wrex 2476  Vcvv 2763   ∖ cdif 3154  ifcif 3561  {csn 3622   class class class wbr 4033   ↦ cmpt 4094  ran crn 4664  (class class class)co 5922  ℂcc 7877  ℝcr 7878  0cc0 7879  1c1 7880   + caddc 7882   · cmul 7884   < clt 8061   ≤ cle 8062   − cmin 8197   # cap 8608   / cdiv 8699  ℕcn 8990  2c2 9041  ℤcz 9326  ℚcq 9693  ℝ⁺crp 9728  ...cfz 10083   ∥ cdvds 11952  ℙcprime 12275

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-13 2169  ax-14 2170  ax-ext 2178  ax-coll 4148  ax-sep 4151  ax-nul 4159  ax-pow 4207  ax-pr 4242  ax-un 4468  ax-setind 4573  ax-iinf 4624  ax-cnex 7970  ax-resscn 7971  ax-1cn 7972  ax-1re 7973  ax-icn 7974  ax-addcl 7975  ax-addrcl 7976  ax-mulcl 7977  ax-mulrcl 7978  ax-addcom 7979  ax-mulcom 7980  ax-addass 7981  ax-mulass 7982  ax-distr 7983  ax-i2m1 7984  ax-0lt1 7985  ax-1rid 7986  ax-0id 7987  ax-rnegex 7988  ax-precex 7989  ax-cnre 7990  ax-pre-ltirr 7991  ax-pre-ltwlin 7992  ax-pre-lttrn 7993  ax-pre-apti 7994  ax-pre-ltadd 7995  ax-pre-mulgt0 7996  ax-pre-mulext 7997  ax-arch 7998  ax-caucvg 7999

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 1475  df-sb 1777  df-eu 2048  df-mo 2049  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-ne 2368  df-nel 2463  df-ral 2480  df-rex 2481  df-reu 2482  df-rmo 2483  df-rab 2484  df-v 2765  df-sbc 2990  df-csb 3085  df-dif 3159  df-un 3161  df-in 3163  df-ss 3170  df-nul 3451  df-if 3562  df-pw 3607  df-sn 3628  df-pr 3629  df-op 3631  df-uni 3840  df-int 3875  df-iun 3918  df-br 4034  df-opab 4095  df-mpt 4096  df-tr 4132  df-id 4328  df-po 4331  df-iso 4332  df-iord 4401  df-on 4403  df-ilim 4404  df-suc 4406  df-iom 4627  df-xp 4669  df-rel 4670  df-cnv 4671  df-co 4672  df-dm 4673  df-rn 4674  df-res 4675  df-ima 4676  df-iota 5219  df-fun 5260  df-fn 5261  df-f 5262  df-f1 5263  df-fo 5264  df-f1o 5265  df-fv 5266  df-riota 5877  df-ov 5925  df-oprab 5926  df-mpo 5927  df-1st 6198  df-2nd 6199  df-recs 6363  df-frec 6449  df-1o 6474  df-2o 6475  df-er 6592  df-en 6800  df-pnf 8063  df-mnf 8064  df-xr 8065  df-ltxr 8066  df-le 8067  df-sub 8199  df-neg 8200  df-reap 8602  df-ap 8609  df-div 8700  df-inn 8991  df-2 9049  df-3 9050  df-4 9051  df-n0 9250  df-z 9327  df-uz 9602  df-q 9694  df-rp 9729  df-ioo 9967  df-fz 10084  df-fl 10360  df-mod 10415  df-seqfrec 10540  df-exp 10631  df-cj 11007  df-re 11008  df-im 11009  df-rsqrt 11163  df-abs 11164  df-dvds 11953  df-prm 12276

This theorem is referenced by:  gausslemma2dlem1f1o  15301