Theorem gausslemma2dlem1a

Description: Lemma for gausslemma2dlem1 . (Contributed by AV, 1-Jul-2021)

	Ref	Expression
Hypotheses	gausslemma2d.p	⊢ ( 𝜑 → 𝑃 ∈ ( ℙ ∖ { 2 } ) )
	gausslemma2d.h	⊢ 𝐻 = ( ( 𝑃 − 1 ) / 2 )
	gausslemma2d.r	⊢ 𝑅 = ( 𝑥 ∈ ( 1 ... 𝐻 ) ↦ if ( ( 𝑥 · 2 ) < ( 𝑃 / 2 ) , ( 𝑥 · 2 ) , ( 𝑃 − ( 𝑥 · 2 ) ) ) )
Assertion	gausslemma2dlem1a	⊢ ( 𝜑 → ran 𝑅 = ( 1 ... 𝐻 ) )

Proof

Step	Hyp	Ref	Expression
1		gausslemma2d.p	⊢ ( 𝜑 → 𝑃 ∈ ( ℙ ∖ { 2 } ) )
2		gausslemma2d.h	⊢ 𝐻 = ( ( 𝑃 − 1 ) / 2 )
3		gausslemma2d.r	⊢ 𝑅 = ( 𝑥 ∈ ( 1 ... 𝐻 ) ↦ if ( ( 𝑥 · 2 ) < ( 𝑃 / 2 ) , ( 𝑥 · 2 ) , ( 𝑃 − ( 𝑥 · 2 ) ) ) )
4	3	elrnmpt	⊢ ( 𝑦 ∈ V → ( 𝑦 ∈ ran 𝑅 ↔ ∃ 𝑥 ∈ ( 1 ... 𝐻 ) 𝑦 = if ( ( 𝑥 · 2 ) < ( 𝑃 / 2 ) , ( 𝑥 · 2 ) , ( 𝑃 − ( 𝑥 · 2 ) ) ) ) )
5	4	elv	⊢ ( 𝑦 ∈ ran 𝑅 ↔ ∃ 𝑥 ∈ ( 1 ... 𝐻 ) 𝑦 = if ( ( 𝑥 · 2 ) < ( 𝑃 / 2 ) , ( 𝑥 · 2 ) , ( 𝑃 − ( 𝑥 · 2 ) ) ) )
6		iftrue	⊢ ( ( 𝑥 · 2 ) < ( 𝑃 / 2 ) → if ( ( 𝑥 · 2 ) < ( 𝑃 / 2 ) , ( 𝑥 · 2 ) , ( 𝑃 − ( 𝑥 · 2 ) ) ) = ( 𝑥 · 2 ) )
7	6	eqeq2d	⊢ ( ( 𝑥 · 2 ) < ( 𝑃 / 2 ) → ( 𝑦 = if ( ( 𝑥 · 2 ) < ( 𝑃 / 2 ) , ( 𝑥 · 2 ) , ( 𝑃 − ( 𝑥 · 2 ) ) ) ↔ 𝑦 = ( 𝑥 · 2 ) ) )
8	7	adantr	⊢ ( ( ( 𝑥 · 2 ) < ( 𝑃 / 2 ) ∧ ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝐻 ) ) ) → ( 𝑦 = if ( ( 𝑥 · 2 ) < ( 𝑃 / 2 ) , ( 𝑥 · 2 ) , ( 𝑃 − ( 𝑥 · 2 ) ) ) ↔ 𝑦 = ( 𝑥 · 2 ) ) )
9		elfz1b	⊢ ( 𝑥 ∈ ( 1 ... 𝐻 ) ↔ ( 𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻 ) )
10		id	⊢ ( 𝑥 ∈ ℕ → 𝑥 ∈ ℕ )
11		2nn	⊢ 2 ∈ ℕ
12	11	a1i	⊢ ( 𝑥 ∈ ℕ → 2 ∈ ℕ )
13	10 12	nnmulcld	⊢ ( 𝑥 ∈ ℕ → ( 𝑥 · 2 ) ∈ ℕ )
14	13	3ad2ant1	⊢ ( ( 𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻 ) → ( 𝑥 · 2 ) ∈ ℕ )
15	14	3ad2ant1	⊢ ( ( ( 𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻 ) ∧ 𝜑 ∧ ( 𝑥 · 2 ) < ( 𝑃 / 2 ) ) → ( 𝑥 · 2 ) ∈ ℕ )
16	2	eleq1i	⊢ ( 𝐻 ∈ ℕ ↔ ( ( 𝑃 − 1 ) / 2 ) ∈ ℕ )
17	16	biimpi	⊢ ( 𝐻 ∈ ℕ → ( ( 𝑃 − 1 ) / 2 ) ∈ ℕ )
18	17	3ad2ant2	⊢ ( ( 𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻 ) → ( ( 𝑃 − 1 ) / 2 ) ∈ ℕ )
19	18	3ad2ant1	⊢ ( ( ( 𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻 ) ∧ 𝜑 ∧ ( 𝑥 · 2 ) < ( 𝑃 / 2 ) ) → ( ( 𝑃 − 1 ) / 2 ) ∈ ℕ )
20		nnoddn2prm	⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → ( 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) )
21		nnz	⊢ ( 𝑃 ∈ ℕ → 𝑃 ∈ ℤ )
22	21	anim1i	⊢ ( ( 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) → ( 𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ) )
23	20 22	syl	⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → ( 𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ) )
24		nnz	⊢ ( 𝑥 ∈ ℕ → 𝑥 ∈ ℤ )
25		2z	⊢ 2 ∈ ℤ
26	25	a1i	⊢ ( 𝑥 ∈ ℕ → 2 ∈ ℤ )
27	24 26	zmulcld	⊢ ( 𝑥 ∈ ℕ → ( 𝑥 · 2 ) ∈ ℤ )
28	27	3ad2ant1	⊢ ( ( 𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻 ) → ( 𝑥 · 2 ) ∈ ℤ )
29	23 28	anim12i	⊢ ( ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ( 𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻 ) ) → ( ( 𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ) ∧ ( 𝑥 · 2 ) ∈ ℤ ) )
30		df-3an	⊢ ( ( 𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ∧ ( 𝑥 · 2 ) ∈ ℤ ) ↔ ( ( 𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ) ∧ ( 𝑥 · 2 ) ∈ ℤ ) )
31	29 30	sylibr	⊢ ( ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ( 𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻 ) ) → ( 𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ∧ ( 𝑥 · 2 ) ∈ ℤ ) )
32	31	ex	⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → ( ( 𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻 ) → ( 𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ∧ ( 𝑥 · 2 ) ∈ ℤ ) ) )
33	1 32	syl	⊢ ( 𝜑 → ( ( 𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻 ) → ( 𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ∧ ( 𝑥 · 2 ) ∈ ℤ ) ) )
34	33	impcom	⊢ ( ( ( 𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻 ) ∧ 𝜑 ) → ( 𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ∧ ( 𝑥 · 2 ) ∈ ℤ ) )
35		ltoddhalfle	⊢ ( ( 𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ∧ ( 𝑥 · 2 ) ∈ ℤ ) → ( ( 𝑥 · 2 ) < ( 𝑃 / 2 ) ↔ ( 𝑥 · 2 ) ≤ ( ( 𝑃 − 1 ) / 2 ) ) )
36	34 35	syl	⊢ ( ( ( 𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻 ) ∧ 𝜑 ) → ( ( 𝑥 · 2 ) < ( 𝑃 / 2 ) ↔ ( 𝑥 · 2 ) ≤ ( ( 𝑃 − 1 ) / 2 ) ) )
37	36	biimp3a	⊢ ( ( ( 𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻 ) ∧ 𝜑 ∧ ( 𝑥 · 2 ) < ( 𝑃 / 2 ) ) → ( 𝑥 · 2 ) ≤ ( ( 𝑃 − 1 ) / 2 ) )
38	15 19 37	3jca	⊢ ( ( ( 𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻 ) ∧ 𝜑 ∧ ( 𝑥 · 2 ) < ( 𝑃 / 2 ) ) → ( ( 𝑥 · 2 ) ∈ ℕ ∧ ( ( 𝑃 − 1 ) / 2 ) ∈ ℕ ∧ ( 𝑥 · 2 ) ≤ ( ( 𝑃 − 1 ) / 2 ) ) )
39	38	3exp	⊢ ( ( 𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻 ) → ( 𝜑 → ( ( 𝑥 · 2 ) < ( 𝑃 / 2 ) → ( ( 𝑥 · 2 ) ∈ ℕ ∧ ( ( 𝑃 − 1 ) / 2 ) ∈ ℕ ∧ ( 𝑥 · 2 ) ≤ ( ( 𝑃 − 1 ) / 2 ) ) ) ) )
40	9 39	sylbi	⊢ ( 𝑥 ∈ ( 1 ... 𝐻 ) → ( 𝜑 → ( ( 𝑥 · 2 ) < ( 𝑃 / 2 ) → ( ( 𝑥 · 2 ) ∈ ℕ ∧ ( ( 𝑃 − 1 ) / 2 ) ∈ ℕ ∧ ( 𝑥 · 2 ) ≤ ( ( 𝑃 − 1 ) / 2 ) ) ) ) )
41	40	impcom	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝐻 ) ) → ( ( 𝑥 · 2 ) < ( 𝑃 / 2 ) → ( ( 𝑥 · 2 ) ∈ ℕ ∧ ( ( 𝑃 − 1 ) / 2 ) ∈ ℕ ∧ ( 𝑥 · 2 ) ≤ ( ( 𝑃 − 1 ) / 2 ) ) ) )
42	41	impcom	⊢ ( ( ( 𝑥 · 2 ) < ( 𝑃 / 2 ) ∧ ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝐻 ) ) ) → ( ( 𝑥 · 2 ) ∈ ℕ ∧ ( ( 𝑃 − 1 ) / 2 ) ∈ ℕ ∧ ( 𝑥 · 2 ) ≤ ( ( 𝑃 − 1 ) / 2 ) ) )
43	2	oveq2i	⊢ ( 1 ... 𝐻 ) = ( 1 ... ( ( 𝑃 − 1 ) / 2 ) )
44	43	eleq2i	⊢ ( ( 𝑥 · 2 ) ∈ ( 1 ... 𝐻 ) ↔ ( 𝑥 · 2 ) ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) )
45		elfz1b	⊢ ( ( 𝑥 · 2 ) ∈ ( 1 ... ( ( 𝑃 − 1 ) / 2 ) ) ↔ ( ( 𝑥 · 2 ) ∈ ℕ ∧ ( ( 𝑃 − 1 ) / 2 ) ∈ ℕ ∧ ( 𝑥 · 2 ) ≤ ( ( 𝑃 − 1 ) / 2 ) ) )
46	44 45	bitri	⊢ ( ( 𝑥 · 2 ) ∈ ( 1 ... 𝐻 ) ↔ ( ( 𝑥 · 2 ) ∈ ℕ ∧ ( ( 𝑃 − 1 ) / 2 ) ∈ ℕ ∧ ( 𝑥 · 2 ) ≤ ( ( 𝑃 − 1 ) / 2 ) ) )
47	42 46	sylibr	⊢ ( ( ( 𝑥 · 2 ) < ( 𝑃 / 2 ) ∧ ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝐻 ) ) ) → ( 𝑥 · 2 ) ∈ ( 1 ... 𝐻 ) )
48		eleq1	⊢ ( 𝑦 = ( 𝑥 · 2 ) → ( 𝑦 ∈ ( 1 ... 𝐻 ) ↔ ( 𝑥 · 2 ) ∈ ( 1 ... 𝐻 ) ) )
49	47 48	syl5ibrcom	⊢ ( ( ( 𝑥 · 2 ) < ( 𝑃 / 2 ) ∧ ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝐻 ) ) ) → ( 𝑦 = ( 𝑥 · 2 ) → 𝑦 ∈ ( 1 ... 𝐻 ) ) )
50	8 49	sylbid	⊢ ( ( ( 𝑥 · 2 ) < ( 𝑃 / 2 ) ∧ ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝐻 ) ) ) → ( 𝑦 = if ( ( 𝑥 · 2 ) < ( 𝑃 / 2 ) , ( 𝑥 · 2 ) , ( 𝑃 − ( 𝑥 · 2 ) ) ) → 𝑦 ∈ ( 1 ... 𝐻 ) ) )
51		iffalse	⊢ ( ¬ ( 𝑥 · 2 ) < ( 𝑃 / 2 ) → if ( ( 𝑥 · 2 ) < ( 𝑃 / 2 ) , ( 𝑥 · 2 ) , ( 𝑃 − ( 𝑥 · 2 ) ) ) = ( 𝑃 − ( 𝑥 · 2 ) ) )
52	51	eqeq2d	⊢ ( ¬ ( 𝑥 · 2 ) < ( 𝑃 / 2 ) → ( 𝑦 = if ( ( 𝑥 · 2 ) < ( 𝑃 / 2 ) , ( 𝑥 · 2 ) , ( 𝑃 − ( 𝑥 · 2 ) ) ) ↔ 𝑦 = ( 𝑃 − ( 𝑥 · 2 ) ) ) )
53	52	adantr	⊢ ( ( ¬ ( 𝑥 · 2 ) < ( 𝑃 / 2 ) ∧ ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝐻 ) ) ) → ( 𝑦 = if ( ( 𝑥 · 2 ) < ( 𝑃 / 2 ) , ( 𝑥 · 2 ) , ( 𝑃 − ( 𝑥 · 2 ) ) ) ↔ 𝑦 = ( 𝑃 − ( 𝑥 · 2 ) ) ) )
54		eldifi	⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → 𝑃 ∈ ℙ )
55		prmz	⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℤ )
56	1 54 55	3syl	⊢ ( 𝜑 → 𝑃 ∈ ℤ )
57	56	ad2antrl	⊢ ( ( ¬ ( 𝑥 · 2 ) < ( 𝑃 / 2 ) ∧ ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝐻 ) ) ) → 𝑃 ∈ ℤ )
58		elfzelz	⊢ ( 𝑥 ∈ ( 1 ... 𝐻 ) → 𝑥 ∈ ℤ )
59	25	a1i	⊢ ( 𝑥 ∈ ( 1 ... 𝐻 ) → 2 ∈ ℤ )
60	58 59	zmulcld	⊢ ( 𝑥 ∈ ( 1 ... 𝐻 ) → ( 𝑥 · 2 ) ∈ ℤ )
61	60	ad2antll	⊢ ( ( ¬ ( 𝑥 · 2 ) < ( 𝑃 / 2 ) ∧ ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝐻 ) ) ) → ( 𝑥 · 2 ) ∈ ℤ )
62	57 61	zsubcld	⊢ ( ( ¬ ( 𝑥 · 2 ) < ( 𝑃 / 2 ) ∧ ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝐻 ) ) ) → ( 𝑃 − ( 𝑥 · 2 ) ) ∈ ℤ )
63	55	zred	⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℝ )
64	2	breq2i	⊢ ( 𝑥 ≤ 𝐻 ↔ 𝑥 ≤ ( ( 𝑃 − 1 ) / 2 ) )
65		nnre	⊢ ( 𝑥 ∈ ℕ → 𝑥 ∈ ℝ )
66	65	adantr	⊢ ( ( 𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ ) → 𝑥 ∈ ℝ )
67		peano2rem	⊢ ( 𝑃 ∈ ℝ → ( 𝑃 − 1 ) ∈ ℝ )
68	67	adantl	⊢ ( ( 𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ ) → ( 𝑃 − 1 ) ∈ ℝ )
69		2re	⊢ 2 ∈ ℝ
70		2pos	⊢ 0 < 2
71	69 70	pm3.2i	⊢ ( 2 ∈ ℝ ∧ 0 < 2 )
72	71	a1i	⊢ ( ( 𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ ) → ( 2 ∈ ℝ ∧ 0 < 2 ) )
73		lemuldiv	⊢ ( ( 𝑥 ∈ ℝ ∧ ( 𝑃 − 1 ) ∈ ℝ ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) → ( ( 𝑥 · 2 ) ≤ ( 𝑃 − 1 ) ↔ 𝑥 ≤ ( ( 𝑃 − 1 ) / 2 ) ) )
74	66 68 72 73	syl3anc	⊢ ( ( 𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ ) → ( ( 𝑥 · 2 ) ≤ ( 𝑃 − 1 ) ↔ 𝑥 ≤ ( ( 𝑃 − 1 ) / 2 ) ) )
75	64 74	bitr4id	⊢ ( ( 𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ ) → ( 𝑥 ≤ 𝐻 ↔ ( 𝑥 · 2 ) ≤ ( 𝑃 − 1 ) ) )
76	13	nnred	⊢ ( 𝑥 ∈ ℕ → ( 𝑥 · 2 ) ∈ ℝ )
77	76	adantr	⊢ ( ( 𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ ) → ( 𝑥 · 2 ) ∈ ℝ )
78		simpr	⊢ ( ( 𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ ) → 𝑃 ∈ ℝ )
79	77 68 78	lesub2d	⊢ ( ( 𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ ) → ( ( 𝑥 · 2 ) ≤ ( 𝑃 − 1 ) ↔ ( 𝑃 − ( 𝑃 − 1 ) ) ≤ ( 𝑃 − ( 𝑥 · 2 ) ) ) )
80		recn	⊢ ( 𝑃 ∈ ℝ → 𝑃 ∈ ℂ )
81		1cnd	⊢ ( 𝑃 ∈ ℝ → 1 ∈ ℂ )
82	80 81	nncand	⊢ ( 𝑃 ∈ ℝ → ( 𝑃 − ( 𝑃 − 1 ) ) = 1 )
83	82	adantl	⊢ ( ( 𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ ) → ( 𝑃 − ( 𝑃 − 1 ) ) = 1 )
84	83	breq1d	⊢ ( ( 𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ ) → ( ( 𝑃 − ( 𝑃 − 1 ) ) ≤ ( 𝑃 − ( 𝑥 · 2 ) ) ↔ 1 ≤ ( 𝑃 − ( 𝑥 · 2 ) ) ) )
85	84	biimpd	⊢ ( ( 𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ ) → ( ( 𝑃 − ( 𝑃 − 1 ) ) ≤ ( 𝑃 − ( 𝑥 · 2 ) ) → 1 ≤ ( 𝑃 − ( 𝑥 · 2 ) ) ) )
86	79 85	sylbid	⊢ ( ( 𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ ) → ( ( 𝑥 · 2 ) ≤ ( 𝑃 − 1 ) → 1 ≤ ( 𝑃 − ( 𝑥 · 2 ) ) ) )
87	75 86	sylbid	⊢ ( ( 𝑥 ∈ ℕ ∧ 𝑃 ∈ ℝ ) → ( 𝑥 ≤ 𝐻 → 1 ≤ ( 𝑃 − ( 𝑥 · 2 ) ) ) )
88	87	impancom	⊢ ( ( 𝑥 ∈ ℕ ∧ 𝑥 ≤ 𝐻 ) → ( 𝑃 ∈ ℝ → 1 ≤ ( 𝑃 − ( 𝑥 · 2 ) ) ) )
89	88	3adant2	⊢ ( ( 𝑥 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑥 ≤ 𝐻 ) → ( 𝑃 ∈ ℝ → 1 ≤ ( 𝑃 − ( 𝑥 · 2 ) ) ) )
90	9 89	sylbi	⊢ ( 𝑥 ∈ ( 1 ... 𝐻 ) → ( 𝑃 ∈ ℝ → 1 ≤ ( 𝑃 − ( 𝑥 · 2 ) ) ) )
91	90	com12	⊢ ( 𝑃 ∈ ℝ → ( 𝑥 ∈ ( 1 ... 𝐻 ) → 1 ≤ ( 𝑃 − ( 𝑥 · 2 ) ) ) )
92	63 91	syl	⊢ ( 𝑃 ∈ ℙ → ( 𝑥 ∈ ( 1 ... 𝐻 ) → 1 ≤ ( 𝑃 − ( 𝑥 · 2 ) ) ) )
93	1 54 92	3syl	⊢ ( 𝜑 → ( 𝑥 ∈ ( 1 ... 𝐻 ) → 1 ≤ ( 𝑃 − ( 𝑥 · 2 ) ) ) )
94	93	imp	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝐻 ) ) → 1 ≤ ( 𝑃 − ( 𝑥 · 2 ) ) )
95	94	adantl	⊢ ( ( ¬ ( 𝑥 · 2 ) < ( 𝑃 / 2 ) ∧ ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝐻 ) ) ) → 1 ≤ ( 𝑃 − ( 𝑥 · 2 ) ) )
96		elnnz1	⊢ ( ( 𝑃 − ( 𝑥 · 2 ) ) ∈ ℕ ↔ ( ( 𝑃 − ( 𝑥 · 2 ) ) ∈ ℤ ∧ 1 ≤ ( 𝑃 − ( 𝑥 · 2 ) ) ) )
97	62 95 96	sylanbrc	⊢ ( ( ¬ ( 𝑥 · 2 ) < ( 𝑃 / 2 ) ∧ ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝐻 ) ) ) → ( 𝑃 − ( 𝑥 · 2 ) ) ∈ ℕ )
98	9	simp2bi	⊢ ( 𝑥 ∈ ( 1 ... 𝐻 ) → 𝐻 ∈ ℕ )
99	98	ad2antll	⊢ ( ( ¬ ( 𝑥 · 2 ) < ( 𝑃 / 2 ) ∧ ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝐻 ) ) ) → 𝐻 ∈ ℕ )
100		nnre	⊢ ( 𝑃 ∈ ℕ → 𝑃 ∈ ℝ )
101	100	rehalfcld	⊢ ( 𝑃 ∈ ℕ → ( 𝑃 / 2 ) ∈ ℝ )
102	101	adantr	⊢ ( ( 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) → ( 𝑃 / 2 ) ∈ ℝ )
103	60	zred	⊢ ( 𝑥 ∈ ( 1 ... 𝐻 ) → ( 𝑥 · 2 ) ∈ ℝ )
104		lenlt	⊢ ( ( ( 𝑃 / 2 ) ∈ ℝ ∧ ( 𝑥 · 2 ) ∈ ℝ ) → ( ( 𝑃 / 2 ) ≤ ( 𝑥 · 2 ) ↔ ¬ ( 𝑥 · 2 ) < ( 𝑃 / 2 ) ) )
105	102 103 104	syl2an	⊢ ( ( ( 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) ∧ 𝑥 ∈ ( 1 ... 𝐻 ) ) → ( ( 𝑃 / 2 ) ≤ ( 𝑥 · 2 ) ↔ ¬ ( 𝑥 · 2 ) < ( 𝑃 / 2 ) ) )
106	22 60	anim12i	⊢ ( ( ( 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) ∧ 𝑥 ∈ ( 1 ... 𝐻 ) ) → ( ( 𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ) ∧ ( 𝑥 · 2 ) ∈ ℤ ) )
107	106 30	sylibr	⊢ ( ( ( 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) ∧ 𝑥 ∈ ( 1 ... 𝐻 ) ) → ( 𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ∧ ( 𝑥 · 2 ) ∈ ℤ ) )
108		halfleoddlt	⊢ ( ( 𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ∧ ( 𝑥 · 2 ) ∈ ℤ ) → ( ( 𝑃 / 2 ) ≤ ( 𝑥 · 2 ) ↔ ( 𝑃 / 2 ) < ( 𝑥 · 2 ) ) )
109	107 108	syl	⊢ ( ( ( 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) ∧ 𝑥 ∈ ( 1 ... 𝐻 ) ) → ( ( 𝑃 / 2 ) ≤ ( 𝑥 · 2 ) ↔ ( 𝑃 / 2 ) < ( 𝑥 · 2 ) ) )
110	109	biimpa	⊢ ( ( ( ( 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) ∧ 𝑥 ∈ ( 1 ... 𝐻 ) ) ∧ ( 𝑃 / 2 ) ≤ ( 𝑥 · 2 ) ) → ( 𝑃 / 2 ) < ( 𝑥 · 2 ) )
111		nncn	⊢ ( 𝑃 ∈ ℕ → 𝑃 ∈ ℂ )
112		subhalfhalf	⊢ ( 𝑃 ∈ ℂ → ( 𝑃 − ( 𝑃 / 2 ) ) = ( 𝑃 / 2 ) )
113	111 112	syl	⊢ ( 𝑃 ∈ ℕ → ( 𝑃 − ( 𝑃 / 2 ) ) = ( 𝑃 / 2 ) )
114	113	breq1d	⊢ ( 𝑃 ∈ ℕ → ( ( 𝑃 − ( 𝑃 / 2 ) ) < ( 𝑥 · 2 ) ↔ ( 𝑃 / 2 ) < ( 𝑥 · 2 ) ) )
115	114	ad3antrrr	⊢ ( ( ( ( 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) ∧ 𝑥 ∈ ( 1 ... 𝐻 ) ) ∧ ( 𝑃 / 2 ) ≤ ( 𝑥 · 2 ) ) → ( ( 𝑃 − ( 𝑃 / 2 ) ) < ( 𝑥 · 2 ) ↔ ( 𝑃 / 2 ) < ( 𝑥 · 2 ) ) )
116	110 115	mpbird	⊢ ( ( ( ( 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) ∧ 𝑥 ∈ ( 1 ... 𝐻 ) ) ∧ ( 𝑃 / 2 ) ≤ ( 𝑥 · 2 ) ) → ( 𝑃 − ( 𝑃 / 2 ) ) < ( 𝑥 · 2 ) )
117	100	ad2antrr	⊢ ( ( ( 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) ∧ 𝑥 ∈ ( 1 ... 𝐻 ) ) → 𝑃 ∈ ℝ )
118	101	ad2antrr	⊢ ( ( ( 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) ∧ 𝑥 ∈ ( 1 ... 𝐻 ) ) → ( 𝑃 / 2 ) ∈ ℝ )
119	103	adantl	⊢ ( ( ( 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) ∧ 𝑥 ∈ ( 1 ... 𝐻 ) ) → ( 𝑥 · 2 ) ∈ ℝ )
120	117 118 119	3jca	⊢ ( ( ( 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) ∧ 𝑥 ∈ ( 1 ... 𝐻 ) ) → ( 𝑃 ∈ ℝ ∧ ( 𝑃 / 2 ) ∈ ℝ ∧ ( 𝑥 · 2 ) ∈ ℝ ) )
121	120	adantr	⊢ ( ( ( ( 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) ∧ 𝑥 ∈ ( 1 ... 𝐻 ) ) ∧ ( 𝑃 / 2 ) ≤ ( 𝑥 · 2 ) ) → ( 𝑃 ∈ ℝ ∧ ( 𝑃 / 2 ) ∈ ℝ ∧ ( 𝑥 · 2 ) ∈ ℝ ) )
122		ltsub23	⊢ ( ( 𝑃 ∈ ℝ ∧ ( 𝑃 / 2 ) ∈ ℝ ∧ ( 𝑥 · 2 ) ∈ ℝ ) → ( ( 𝑃 − ( 𝑃 / 2 ) ) < ( 𝑥 · 2 ) ↔ ( 𝑃 − ( 𝑥 · 2 ) ) < ( 𝑃 / 2 ) ) )
123	121 122	syl	⊢ ( ( ( ( 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) ∧ 𝑥 ∈ ( 1 ... 𝐻 ) ) ∧ ( 𝑃 / 2 ) ≤ ( 𝑥 · 2 ) ) → ( ( 𝑃 − ( 𝑃 / 2 ) ) < ( 𝑥 · 2 ) ↔ ( 𝑃 − ( 𝑥 · 2 ) ) < ( 𝑃 / 2 ) ) )
124	116 123	mpbid	⊢ ( ( ( ( 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) ∧ 𝑥 ∈ ( 1 ... 𝐻 ) ) ∧ ( 𝑃 / 2 ) ≤ ( 𝑥 · 2 ) ) → ( 𝑃 − ( 𝑥 · 2 ) ) < ( 𝑃 / 2 ) )
125	21	ad2antrr	⊢ ( ( ( 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) ∧ 𝑥 ∈ ( 1 ... 𝐻 ) ) → 𝑃 ∈ ℤ )
126		simplr	⊢ ( ( ( 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) ∧ 𝑥 ∈ ( 1 ... 𝐻 ) ) → ¬ 2 ∥ 𝑃 )
127	60	adantl	⊢ ( ( ( 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) ∧ 𝑥 ∈ ( 1 ... 𝐻 ) ) → ( 𝑥 · 2 ) ∈ ℤ )
128	125 127	zsubcld	⊢ ( ( ( 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) ∧ 𝑥 ∈ ( 1 ... 𝐻 ) ) → ( 𝑃 − ( 𝑥 · 2 ) ) ∈ ℤ )
129	125 126 128	3jca	⊢ ( ( ( 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) ∧ 𝑥 ∈ ( 1 ... 𝐻 ) ) → ( 𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ∧ ( 𝑃 − ( 𝑥 · 2 ) ) ∈ ℤ ) )
130	129	adantr	⊢ ( ( ( ( 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) ∧ 𝑥 ∈ ( 1 ... 𝐻 ) ) ∧ ( 𝑃 / 2 ) ≤ ( 𝑥 · 2 ) ) → ( 𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ∧ ( 𝑃 − ( 𝑥 · 2 ) ) ∈ ℤ ) )
131		ltoddhalfle	⊢ ( ( 𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ∧ ( 𝑃 − ( 𝑥 · 2 ) ) ∈ ℤ ) → ( ( 𝑃 − ( 𝑥 · 2 ) ) < ( 𝑃 / 2 ) ↔ ( 𝑃 − ( 𝑥 · 2 ) ) ≤ ( ( 𝑃 − 1 ) / 2 ) ) )
132	130 131	syl	⊢ ( ( ( ( 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) ∧ 𝑥 ∈ ( 1 ... 𝐻 ) ) ∧ ( 𝑃 / 2 ) ≤ ( 𝑥 · 2 ) ) → ( ( 𝑃 − ( 𝑥 · 2 ) ) < ( 𝑃 / 2 ) ↔ ( 𝑃 − ( 𝑥 · 2 ) ) ≤ ( ( 𝑃 − 1 ) / 2 ) ) )
133	124 132	mpbid	⊢ ( ( ( ( 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) ∧ 𝑥 ∈ ( 1 ... 𝐻 ) ) ∧ ( 𝑃 / 2 ) ≤ ( 𝑥 · 2 ) ) → ( 𝑃 − ( 𝑥 · 2 ) ) ≤ ( ( 𝑃 − 1 ) / 2 ) )
134	133	ex	⊢ ( ( ( 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) ∧ 𝑥 ∈ ( 1 ... 𝐻 ) ) → ( ( 𝑃 / 2 ) ≤ ( 𝑥 · 2 ) → ( 𝑃 − ( 𝑥 · 2 ) ) ≤ ( ( 𝑃 − 1 ) / 2 ) ) )
135	2	breq2i	⊢ ( ( 𝑃 − ( 𝑥 · 2 ) ) ≤ 𝐻 ↔ ( 𝑃 − ( 𝑥 · 2 ) ) ≤ ( ( 𝑃 − 1 ) / 2 ) )
136	134 135	imbitrrdi	⊢ ( ( ( 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) ∧ 𝑥 ∈ ( 1 ... 𝐻 ) ) → ( ( 𝑃 / 2 ) ≤ ( 𝑥 · 2 ) → ( 𝑃 − ( 𝑥 · 2 ) ) ≤ 𝐻 ) )
137	105 136	sylbird	⊢ ( ( ( 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) ∧ 𝑥 ∈ ( 1 ... 𝐻 ) ) → ( ¬ ( 𝑥 · 2 ) < ( 𝑃 / 2 ) → ( 𝑃 − ( 𝑥 · 2 ) ) ≤ 𝐻 ) )
138	137	ex	⊢ ( ( 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) → ( 𝑥 ∈ ( 1 ... 𝐻 ) → ( ¬ ( 𝑥 · 2 ) < ( 𝑃 / 2 ) → ( 𝑃 − ( 𝑥 · 2 ) ) ≤ 𝐻 ) ) )
139	1 20 138	3syl	⊢ ( 𝜑 → ( 𝑥 ∈ ( 1 ... 𝐻 ) → ( ¬ ( 𝑥 · 2 ) < ( 𝑃 / 2 ) → ( 𝑃 − ( 𝑥 · 2 ) ) ≤ 𝐻 ) ) )
140	139	imp	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝐻 ) ) → ( ¬ ( 𝑥 · 2 ) < ( 𝑃 / 2 ) → ( 𝑃 − ( 𝑥 · 2 ) ) ≤ 𝐻 ) )
141	140	impcom	⊢ ( ( ¬ ( 𝑥 · 2 ) < ( 𝑃 / 2 ) ∧ ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝐻 ) ) ) → ( 𝑃 − ( 𝑥 · 2 ) ) ≤ 𝐻 )
142		elfz1b	⊢ ( ( 𝑃 − ( 𝑥 · 2 ) ) ∈ ( 1 ... 𝐻 ) ↔ ( ( 𝑃 − ( 𝑥 · 2 ) ) ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ ( 𝑃 − ( 𝑥 · 2 ) ) ≤ 𝐻 ) )
143	97 99 141 142	syl3anbrc	⊢ ( ( ¬ ( 𝑥 · 2 ) < ( 𝑃 / 2 ) ∧ ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝐻 ) ) ) → ( 𝑃 − ( 𝑥 · 2 ) ) ∈ ( 1 ... 𝐻 ) )
144		eleq1	⊢ ( 𝑦 = ( 𝑃 − ( 𝑥 · 2 ) ) → ( 𝑦 ∈ ( 1 ... 𝐻 ) ↔ ( 𝑃 − ( 𝑥 · 2 ) ) ∈ ( 1 ... 𝐻 ) ) )
145	143 144	syl5ibrcom	⊢ ( ( ¬ ( 𝑥 · 2 ) < ( 𝑃 / 2 ) ∧ ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝐻 ) ) ) → ( 𝑦 = ( 𝑃 − ( 𝑥 · 2 ) ) → 𝑦 ∈ ( 1 ... 𝐻 ) ) )
146	53 145	sylbid	⊢ ( ( ¬ ( 𝑥 · 2 ) < ( 𝑃 / 2 ) ∧ ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝐻 ) ) ) → ( 𝑦 = if ( ( 𝑥 · 2 ) < ( 𝑃 / 2 ) , ( 𝑥 · 2 ) , ( 𝑃 − ( 𝑥 · 2 ) ) ) → 𝑦 ∈ ( 1 ... 𝐻 ) ) )
147	50 146	pm2.61ian	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 ... 𝐻 ) ) → ( 𝑦 = if ( ( 𝑥 · 2 ) < ( 𝑃 / 2 ) , ( 𝑥 · 2 ) , ( 𝑃 − ( 𝑥 · 2 ) ) ) → 𝑦 ∈ ( 1 ... 𝐻 ) ) )
148	147	rexlimdva	⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ( 1 ... 𝐻 ) 𝑦 = if ( ( 𝑥 · 2 ) < ( 𝑃 / 2 ) , ( 𝑥 · 2 ) , ( 𝑃 − ( 𝑥 · 2 ) ) ) → 𝑦 ∈ ( 1 ... 𝐻 ) ) )
149		elfz1b	⊢ ( 𝑦 ∈ ( 1 ... 𝐻 ) ↔ ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻 ) )
150		simp1	⊢ ( ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻 ) → 𝑦 ∈ ℕ )
151		simpl	⊢ ( ( 2 ∥ 𝑦 ∧ 𝜑 ) → 2 ∥ 𝑦 )
152		nnehalf	⊢ ( ( 𝑦 ∈ ℕ ∧ 2 ∥ 𝑦 ) → ( 𝑦 / 2 ) ∈ ℕ )
153	150 151 152	syl2anr	⊢ ( ( ( 2 ∥ 𝑦 ∧ 𝜑 ) ∧ ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻 ) ) → ( 𝑦 / 2 ) ∈ ℕ )
154		simpr2	⊢ ( ( ( 2 ∥ 𝑦 ∧ 𝜑 ) ∧ ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻 ) ) → 𝐻 ∈ ℕ )
155		nnre	⊢ ( 𝑦 ∈ ℕ → 𝑦 ∈ ℝ )
156	155	ad2antrr	⊢ ( ( ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ) ∧ ( 2 ∥ 𝑦 ∧ 𝜑 ) ) → 𝑦 ∈ ℝ )
157		nnrp	⊢ ( 𝐻 ∈ ℕ → 𝐻 ∈ ℝ+ )
158	157	adantl	⊢ ( ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ) → 𝐻 ∈ ℝ+ )
159	158	adantr	⊢ ( ( ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ) ∧ ( 2 ∥ 𝑦 ∧ 𝜑 ) ) → 𝐻 ∈ ℝ+ )
160		2rp	⊢ 2 ∈ ℝ+
161		1le2	⊢ 1 ≤ 2
162	160 161	pm3.2i	⊢ ( 2 ∈ ℝ+ ∧ 1 ≤ 2 )
163	162	a1i	⊢ ( ( ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ) ∧ ( 2 ∥ 𝑦 ∧ 𝜑 ) ) → ( 2 ∈ ℝ+ ∧ 1 ≤ 2 ) )
164		ledivge1le	⊢ ( ( 𝑦 ∈ ℝ ∧ 𝐻 ∈ ℝ+ ∧ ( 2 ∈ ℝ+ ∧ 1 ≤ 2 ) ) → ( 𝑦 ≤ 𝐻 → ( 𝑦 / 2 ) ≤ 𝐻 ) )
165	156 159 163 164	syl3anc	⊢ ( ( ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ) ∧ ( 2 ∥ 𝑦 ∧ 𝜑 ) ) → ( 𝑦 ≤ 𝐻 → ( 𝑦 / 2 ) ≤ 𝐻 ) )
166	165	ex	⊢ ( ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ) → ( ( 2 ∥ 𝑦 ∧ 𝜑 ) → ( 𝑦 ≤ 𝐻 → ( 𝑦 / 2 ) ≤ 𝐻 ) ) )
167	166	com23	⊢ ( ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ) → ( 𝑦 ≤ 𝐻 → ( ( 2 ∥ 𝑦 ∧ 𝜑 ) → ( 𝑦 / 2 ) ≤ 𝐻 ) ) )
168	167	3impia	⊢ ( ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻 ) → ( ( 2 ∥ 𝑦 ∧ 𝜑 ) → ( 𝑦 / 2 ) ≤ 𝐻 ) )
169	168	impcom	⊢ ( ( ( 2 ∥ 𝑦 ∧ 𝜑 ) ∧ ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻 ) ) → ( 𝑦 / 2 ) ≤ 𝐻 )
170	153 154 169	3jca	⊢ ( ( ( 2 ∥ 𝑦 ∧ 𝜑 ) ∧ ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻 ) ) → ( ( 𝑦 / 2 ) ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ ( 𝑦 / 2 ) ≤ 𝐻 ) )
171	170	ex	⊢ ( ( 2 ∥ 𝑦 ∧ 𝜑 ) → ( ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻 ) → ( ( 𝑦 / 2 ) ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ ( 𝑦 / 2 ) ≤ 𝐻 ) ) )
172	149 171	biimtrid	⊢ ( ( 2 ∥ 𝑦 ∧ 𝜑 ) → ( 𝑦 ∈ ( 1 ... 𝐻 ) → ( ( 𝑦 / 2 ) ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ ( 𝑦 / 2 ) ≤ 𝐻 ) ) )
173	172	3impia	⊢ ( ( 2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ ( 1 ... 𝐻 ) ) → ( ( 𝑦 / 2 ) ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ ( 𝑦 / 2 ) ≤ 𝐻 ) )
174		elfz1b	⊢ ( ( 𝑦 / 2 ) ∈ ( 1 ... 𝐻 ) ↔ ( ( 𝑦 / 2 ) ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ ( 𝑦 / 2 ) ≤ 𝐻 ) )
175	173 174	sylibr	⊢ ( ( 2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ ( 1 ... 𝐻 ) ) → ( 𝑦 / 2 ) ∈ ( 1 ... 𝐻 ) )
176		oveq1	⊢ ( 𝑥 = ( 𝑦 / 2 ) → ( 𝑥 · 2 ) = ( ( 𝑦 / 2 ) · 2 ) )
177	176	breq1d	⊢ ( 𝑥 = ( 𝑦 / 2 ) → ( ( 𝑥 · 2 ) < ( 𝑃 / 2 ) ↔ ( ( 𝑦 / 2 ) · 2 ) < ( 𝑃 / 2 ) ) )
178	176	oveq2d	⊢ ( 𝑥 = ( 𝑦 / 2 ) → ( 𝑃 − ( 𝑥 · 2 ) ) = ( 𝑃 − ( ( 𝑦 / 2 ) · 2 ) ) )
179	177 176 178	ifbieq12d	⊢ ( 𝑥 = ( 𝑦 / 2 ) → if ( ( 𝑥 · 2 ) < ( 𝑃 / 2 ) , ( 𝑥 · 2 ) , ( 𝑃 − ( 𝑥 · 2 ) ) ) = if ( ( ( 𝑦 / 2 ) · 2 ) < ( 𝑃 / 2 ) , ( ( 𝑦 / 2 ) · 2 ) , ( 𝑃 − ( ( 𝑦 / 2 ) · 2 ) ) ) )
180	179	eqeq2d	⊢ ( 𝑥 = ( 𝑦 / 2 ) → ( 𝑦 = if ( ( 𝑥 · 2 ) < ( 𝑃 / 2 ) , ( 𝑥 · 2 ) , ( 𝑃 − ( 𝑥 · 2 ) ) ) ↔ 𝑦 = if ( ( ( 𝑦 / 2 ) · 2 ) < ( 𝑃 / 2 ) , ( ( 𝑦 / 2 ) · 2 ) , ( 𝑃 − ( ( 𝑦 / 2 ) · 2 ) ) ) ) )
181	180	adantl	⊢ ( ( ( 2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ ( 1 ... 𝐻 ) ) ∧ 𝑥 = ( 𝑦 / 2 ) ) → ( 𝑦 = if ( ( 𝑥 · 2 ) < ( 𝑃 / 2 ) , ( 𝑥 · 2 ) , ( 𝑃 − ( 𝑥 · 2 ) ) ) ↔ 𝑦 = if ( ( ( 𝑦 / 2 ) · 2 ) < ( 𝑃 / 2 ) , ( ( 𝑦 / 2 ) · 2 ) , ( 𝑃 − ( ( 𝑦 / 2 ) · 2 ) ) ) ) )
182		elfzelz	⊢ ( 𝑦 ∈ ( 1 ... 𝐻 ) → 𝑦 ∈ ℤ )
183	182	zcnd	⊢ ( 𝑦 ∈ ( 1 ... 𝐻 ) → 𝑦 ∈ ℂ )
184	183	3ad2ant3	⊢ ( ( 2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ ( 1 ... 𝐻 ) ) → 𝑦 ∈ ℂ )
185		2cnd	⊢ ( ( 2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ ( 1 ... 𝐻 ) ) → 2 ∈ ℂ )
186		2ne0	⊢ 2 ≠ 0
187	186	a1i	⊢ ( ( 2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ ( 1 ... 𝐻 ) ) → 2 ≠ 0 )
188	184 185 187	divcan1d	⊢ ( ( 2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ ( 1 ... 𝐻 ) ) → ( ( 𝑦 / 2 ) · 2 ) = 𝑦 )
189	2	breq2i	⊢ ( 𝑦 ≤ 𝐻 ↔ 𝑦 ≤ ( ( 𝑃 − 1 ) / 2 ) )
190		nnz	⊢ ( 𝑦 ∈ ℕ → 𝑦 ∈ ℤ )
191	1 20 22	3syl	⊢ ( 𝜑 → ( 𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ) )
192	191	adantl	⊢ ( ( 2 ∥ 𝑦 ∧ 𝜑 ) → ( 𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ) )
193	190 192	anim12ci	⊢ ( ( 𝑦 ∈ ℕ ∧ ( 2 ∥ 𝑦 ∧ 𝜑 ) ) → ( ( 𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ) ∧ 𝑦 ∈ ℤ ) )
194		df-3an	⊢ ( ( 𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ∧ 𝑦 ∈ ℤ ) ↔ ( ( 𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ) ∧ 𝑦 ∈ ℤ ) )
195	193 194	sylibr	⊢ ( ( 𝑦 ∈ ℕ ∧ ( 2 ∥ 𝑦 ∧ 𝜑 ) ) → ( 𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ∧ 𝑦 ∈ ℤ ) )
196		ltoddhalfle	⊢ ( ( 𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ∧ 𝑦 ∈ ℤ ) → ( 𝑦 < ( 𝑃 / 2 ) ↔ 𝑦 ≤ ( ( 𝑃 − 1 ) / 2 ) ) )
197	195 196	syl	⊢ ( ( 𝑦 ∈ ℕ ∧ ( 2 ∥ 𝑦 ∧ 𝜑 ) ) → ( 𝑦 < ( 𝑃 / 2 ) ↔ 𝑦 ≤ ( ( 𝑃 − 1 ) / 2 ) ) )
198	197	exbiri	⊢ ( 𝑦 ∈ ℕ → ( ( 2 ∥ 𝑦 ∧ 𝜑 ) → ( 𝑦 ≤ ( ( 𝑃 − 1 ) / 2 ) → 𝑦 < ( 𝑃 / 2 ) ) ) )
199	198	com23	⊢ ( 𝑦 ∈ ℕ → ( 𝑦 ≤ ( ( 𝑃 − 1 ) / 2 ) → ( ( 2 ∥ 𝑦 ∧ 𝜑 ) → 𝑦 < ( 𝑃 / 2 ) ) ) )
200	189 199	biimtrid	⊢ ( 𝑦 ∈ ℕ → ( 𝑦 ≤ 𝐻 → ( ( 2 ∥ 𝑦 ∧ 𝜑 ) → 𝑦 < ( 𝑃 / 2 ) ) ) )
201	200	a1d	⊢ ( 𝑦 ∈ ℕ → ( 𝐻 ∈ ℕ → ( 𝑦 ≤ 𝐻 → ( ( 2 ∥ 𝑦 ∧ 𝜑 ) → 𝑦 < ( 𝑃 / 2 ) ) ) ) )
202	201	3imp	⊢ ( ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻 ) → ( ( 2 ∥ 𝑦 ∧ 𝜑 ) → 𝑦 < ( 𝑃 / 2 ) ) )
203	149 202	sylbi	⊢ ( 𝑦 ∈ ( 1 ... 𝐻 ) → ( ( 2 ∥ 𝑦 ∧ 𝜑 ) → 𝑦 < ( 𝑃 / 2 ) ) )
204	203	com12	⊢ ( ( 2 ∥ 𝑦 ∧ 𝜑 ) → ( 𝑦 ∈ ( 1 ... 𝐻 ) → 𝑦 < ( 𝑃 / 2 ) ) )
205	204	3impia	⊢ ( ( 2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ ( 1 ... 𝐻 ) ) → 𝑦 < ( 𝑃 / 2 ) )
206	188 205	eqbrtrd	⊢ ( ( 2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ ( 1 ... 𝐻 ) ) → ( ( 𝑦 / 2 ) · 2 ) < ( 𝑃 / 2 ) )
207	206	iftrued	⊢ ( ( 2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ ( 1 ... 𝐻 ) ) → if ( ( ( 𝑦 / 2 ) · 2 ) < ( 𝑃 / 2 ) , ( ( 𝑦 / 2 ) · 2 ) , ( 𝑃 − ( ( 𝑦 / 2 ) · 2 ) ) ) = ( ( 𝑦 / 2 ) · 2 ) )
208	207 188	eqtr2d	⊢ ( ( 2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ ( 1 ... 𝐻 ) ) → 𝑦 = if ( ( ( 𝑦 / 2 ) · 2 ) < ( 𝑃 / 2 ) , ( ( 𝑦 / 2 ) · 2 ) , ( 𝑃 − ( ( 𝑦 / 2 ) · 2 ) ) ) )
209	175 181 208	rspcedvd	⊢ ( ( 2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ ( 1 ... 𝐻 ) ) → ∃ 𝑥 ∈ ( 1 ... 𝐻 ) 𝑦 = if ( ( 𝑥 · 2 ) < ( 𝑃 / 2 ) , ( 𝑥 · 2 ) , ( 𝑃 − ( 𝑥 · 2 ) ) ) )
210	209	3exp	⊢ ( 2 ∥ 𝑦 → ( 𝜑 → ( 𝑦 ∈ ( 1 ... 𝐻 ) → ∃ 𝑥 ∈ ( 1 ... 𝐻 ) 𝑦 = if ( ( 𝑥 · 2 ) < ( 𝑃 / 2 ) , ( 𝑥 · 2 ) , ( 𝑃 − ( 𝑥 · 2 ) ) ) ) ) )
211	54 55	syl	⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → 𝑃 ∈ ℤ )
212	211	ad2antrr	⊢ ( ( ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 2 ∥ 𝑦 ) ∧ ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻 ) ) → 𝑃 ∈ ℤ )
213	190	3ad2ant1	⊢ ( ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻 ) → 𝑦 ∈ ℤ )
214	213	adantl	⊢ ( ( ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 2 ∥ 𝑦 ) ∧ ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻 ) ) → 𝑦 ∈ ℤ )
215	212 214	zsubcld	⊢ ( ( ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 2 ∥ 𝑦 ) ∧ ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻 ) ) → ( 𝑃 − 𝑦 ) ∈ ℤ )
216	155	ad2antrl	⊢ ( ( 𝑃 ∈ ℝ ∧ ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ) ) → 𝑦 ∈ ℝ )
217	67	rehalfcld	⊢ ( 𝑃 ∈ ℝ → ( ( 𝑃 − 1 ) / 2 ) ∈ ℝ )
218	217	adantr	⊢ ( ( 𝑃 ∈ ℝ ∧ ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ) ) → ( ( 𝑃 − 1 ) / 2 ) ∈ ℝ )
219		simpl	⊢ ( ( 𝑃 ∈ ℝ ∧ ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ) ) → 𝑃 ∈ ℝ )
220	216 218 219	3jca	⊢ ( ( 𝑃 ∈ ℝ ∧ ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ) ) → ( 𝑦 ∈ ℝ ∧ ( ( 𝑃 − 1 ) / 2 ) ∈ ℝ ∧ 𝑃 ∈ ℝ ) )
221	220	ex	⊢ ( 𝑃 ∈ ℝ → ( ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ) → ( 𝑦 ∈ ℝ ∧ ( ( 𝑃 − 1 ) / 2 ) ∈ ℝ ∧ 𝑃 ∈ ℝ ) ) )
222	54 63 221	3syl	⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → ( ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ) → ( 𝑦 ∈ ℝ ∧ ( ( 𝑃 − 1 ) / 2 ) ∈ ℝ ∧ 𝑃 ∈ ℝ ) ) )
223	222	adantr	⊢ ( ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 2 ∥ 𝑦 ) → ( ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ) → ( 𝑦 ∈ ℝ ∧ ( ( 𝑃 − 1 ) / 2 ) ∈ ℝ ∧ 𝑃 ∈ ℝ ) ) )
224	223	impcom	⊢ ( ( ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ) ∧ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 2 ∥ 𝑦 ) ) → ( 𝑦 ∈ ℝ ∧ ( ( 𝑃 − 1 ) / 2 ) ∈ ℝ ∧ 𝑃 ∈ ℝ ) )
225		lesub2	⊢ ( ( 𝑦 ∈ ℝ ∧ ( ( 𝑃 − 1 ) / 2 ) ∈ ℝ ∧ 𝑃 ∈ ℝ ) → ( 𝑦 ≤ ( ( 𝑃 − 1 ) / 2 ) ↔ ( 𝑃 − ( ( 𝑃 − 1 ) / 2 ) ) ≤ ( 𝑃 − 𝑦 ) ) )
226	224 225	syl	⊢ ( ( ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ) ∧ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 2 ∥ 𝑦 ) ) → ( 𝑦 ≤ ( ( 𝑃 − 1 ) / 2 ) ↔ ( 𝑃 − ( ( 𝑃 − 1 ) / 2 ) ) ≤ ( 𝑃 − 𝑦 ) ) )
227	55	zcnd	⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℂ )
228		1cnd	⊢ ( 𝑃 ∈ ℂ → 1 ∈ ℂ )
229		2cnne0	⊢ ( 2 ∈ ℂ ∧ 2 ≠ 0 )
230	229	a1i	⊢ ( 𝑃 ∈ ℂ → ( 2 ∈ ℂ ∧ 2 ≠ 0 ) )
231		divsubdir	⊢ ( ( 𝑃 ∈ ℂ ∧ 1 ∈ ℂ ∧ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ) → ( ( 𝑃 − 1 ) / 2 ) = ( ( 𝑃 / 2 ) − ( 1 / 2 ) ) )
232	228 230 231	mpd3an23	⊢ ( 𝑃 ∈ ℂ → ( ( 𝑃 − 1 ) / 2 ) = ( ( 𝑃 / 2 ) − ( 1 / 2 ) ) )
233	232	oveq2d	⊢ ( 𝑃 ∈ ℂ → ( 𝑃 − ( ( 𝑃 − 1 ) / 2 ) ) = ( 𝑃 − ( ( 𝑃 / 2 ) − ( 1 / 2 ) ) ) )
234		id	⊢ ( 𝑃 ∈ ℂ → 𝑃 ∈ ℂ )
235		halfcl	⊢ ( 𝑃 ∈ ℂ → ( 𝑃 / 2 ) ∈ ℂ )
236		halfcn	⊢ ( 1 / 2 ) ∈ ℂ
237	236	a1i	⊢ ( 𝑃 ∈ ℂ → ( 1 / 2 ) ∈ ℂ )
238	234 235 237	subsubd	⊢ ( 𝑃 ∈ ℂ → ( 𝑃 − ( ( 𝑃 / 2 ) − ( 1 / 2 ) ) ) = ( ( 𝑃 − ( 𝑃 / 2 ) ) + ( 1 / 2 ) ) )
239	112	oveq1d	⊢ ( 𝑃 ∈ ℂ → ( ( 𝑃 − ( 𝑃 / 2 ) ) + ( 1 / 2 ) ) = ( ( 𝑃 / 2 ) + ( 1 / 2 ) ) )
240	233 238 239	3eqtrd	⊢ ( 𝑃 ∈ ℂ → ( 𝑃 − ( ( 𝑃 − 1 ) / 2 ) ) = ( ( 𝑃 / 2 ) + ( 1 / 2 ) ) )
241	54 227 240	3syl	⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → ( 𝑃 − ( ( 𝑃 − 1 ) / 2 ) ) = ( ( 𝑃 / 2 ) + ( 1 / 2 ) ) )
242	241	ad2antrl	⊢ ( ( ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ) ∧ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 2 ∥ 𝑦 ) ) → ( 𝑃 − ( ( 𝑃 − 1 ) / 2 ) ) = ( ( 𝑃 / 2 ) + ( 1 / 2 ) ) )
243	242	breq1d	⊢ ( ( ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ) ∧ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 2 ∥ 𝑦 ) ) → ( ( 𝑃 − ( ( 𝑃 − 1 ) / 2 ) ) ≤ ( 𝑃 − 𝑦 ) ↔ ( ( 𝑃 / 2 ) + ( 1 / 2 ) ) ≤ ( 𝑃 − 𝑦 ) ) )
244		prmnn	⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
245		halfre	⊢ ( 1 / 2 ) ∈ ℝ
246	245	a1i	⊢ ( 𝑃 ∈ ℕ → ( 1 / 2 ) ∈ ℝ )
247		nngt0	⊢ ( 𝑃 ∈ ℕ → 0 < 𝑃 )
248	71	a1i	⊢ ( 𝑃 ∈ ℕ → ( 2 ∈ ℝ ∧ 0 < 2 ) )
249		divgt0	⊢ ( ( ( 𝑃 ∈ ℝ ∧ 0 < 𝑃 ) ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) → 0 < ( 𝑃 / 2 ) )
250	100 247 248 249	syl21anc	⊢ ( 𝑃 ∈ ℕ → 0 < ( 𝑃 / 2 ) )
251		halfgt0	⊢ 0 < ( 1 / 2 )
252	251	a1i	⊢ ( 𝑃 ∈ ℕ → 0 < ( 1 / 2 ) )
253	101 246 250 252	addgt0d	⊢ ( 𝑃 ∈ ℕ → 0 < ( ( 𝑃 / 2 ) + ( 1 / 2 ) ) )
254	54 244 253	3syl	⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → 0 < ( ( 𝑃 / 2 ) + ( 1 / 2 ) ) )
255	254	ad2antrl	⊢ ( ( ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ) ∧ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 2 ∥ 𝑦 ) ) → 0 < ( ( 𝑃 / 2 ) + ( 1 / 2 ) ) )
256		0red	⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ ) → 0 ∈ ℝ )
257		simpr	⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ ) → 𝑃 ∈ ℝ )
258	257	rehalfcld	⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ ) → ( 𝑃 / 2 ) ∈ ℝ )
259	245	a1i	⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ ) → ( 1 / 2 ) ∈ ℝ )
260	258 259	readdcld	⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ ) → ( ( 𝑃 / 2 ) + ( 1 / 2 ) ) ∈ ℝ )
261		resubcl	⊢ ( ( 𝑃 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑃 − 𝑦 ) ∈ ℝ )
262	261	ancoms	⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ ) → ( 𝑃 − 𝑦 ) ∈ ℝ )
263	256 260 262	3jca	⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ ) → ( 0 ∈ ℝ ∧ ( ( 𝑃 / 2 ) + ( 1 / 2 ) ) ∈ ℝ ∧ ( 𝑃 − 𝑦 ) ∈ ℝ ) )
264	263	ex	⊢ ( 𝑦 ∈ ℝ → ( 𝑃 ∈ ℝ → ( 0 ∈ ℝ ∧ ( ( 𝑃 / 2 ) + ( 1 / 2 ) ) ∈ ℝ ∧ ( 𝑃 − 𝑦 ) ∈ ℝ ) ) )
265	155 264	syl	⊢ ( 𝑦 ∈ ℕ → ( 𝑃 ∈ ℝ → ( 0 ∈ ℝ ∧ ( ( 𝑃 / 2 ) + ( 1 / 2 ) ) ∈ ℝ ∧ ( 𝑃 − 𝑦 ) ∈ ℝ ) ) )
266	265	adantr	⊢ ( ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ) → ( 𝑃 ∈ ℝ → ( 0 ∈ ℝ ∧ ( ( 𝑃 / 2 ) + ( 1 / 2 ) ) ∈ ℝ ∧ ( 𝑃 − 𝑦 ) ∈ ℝ ) ) )
267	266	com12	⊢ ( 𝑃 ∈ ℝ → ( ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ) → ( 0 ∈ ℝ ∧ ( ( 𝑃 / 2 ) + ( 1 / 2 ) ) ∈ ℝ ∧ ( 𝑃 − 𝑦 ) ∈ ℝ ) ) )
268	54 63 267	3syl	⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → ( ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ) → ( 0 ∈ ℝ ∧ ( ( 𝑃 / 2 ) + ( 1 / 2 ) ) ∈ ℝ ∧ ( 𝑃 − 𝑦 ) ∈ ℝ ) ) )
269	268	adantr	⊢ ( ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 2 ∥ 𝑦 ) → ( ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ) → ( 0 ∈ ℝ ∧ ( ( 𝑃 / 2 ) + ( 1 / 2 ) ) ∈ ℝ ∧ ( 𝑃 − 𝑦 ) ∈ ℝ ) ) )
270	269	impcom	⊢ ( ( ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ) ∧ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 2 ∥ 𝑦 ) ) → ( 0 ∈ ℝ ∧ ( ( 𝑃 / 2 ) + ( 1 / 2 ) ) ∈ ℝ ∧ ( 𝑃 − 𝑦 ) ∈ ℝ ) )
271		ltletr	⊢ ( ( 0 ∈ ℝ ∧ ( ( 𝑃 / 2 ) + ( 1 / 2 ) ) ∈ ℝ ∧ ( 𝑃 − 𝑦 ) ∈ ℝ ) → ( ( 0 < ( ( 𝑃 / 2 ) + ( 1 / 2 ) ) ∧ ( ( 𝑃 / 2 ) + ( 1 / 2 ) ) ≤ ( 𝑃 − 𝑦 ) ) → 0 < ( 𝑃 − 𝑦 ) ) )
272	270 271	syl	⊢ ( ( ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ) ∧ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 2 ∥ 𝑦 ) ) → ( ( 0 < ( ( 𝑃 / 2 ) + ( 1 / 2 ) ) ∧ ( ( 𝑃 / 2 ) + ( 1 / 2 ) ) ≤ ( 𝑃 − 𝑦 ) ) → 0 < ( 𝑃 − 𝑦 ) ) )
273	255 272	mpand	⊢ ( ( ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ) ∧ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 2 ∥ 𝑦 ) ) → ( ( ( 𝑃 / 2 ) + ( 1 / 2 ) ) ≤ ( 𝑃 − 𝑦 ) → 0 < ( 𝑃 − 𝑦 ) ) )
274	243 273	sylbid	⊢ ( ( ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ) ∧ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 2 ∥ 𝑦 ) ) → ( ( 𝑃 − ( ( 𝑃 − 1 ) / 2 ) ) ≤ ( 𝑃 − 𝑦 ) → 0 < ( 𝑃 − 𝑦 ) ) )
275	226 274	sylbid	⊢ ( ( ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ) ∧ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 2 ∥ 𝑦 ) ) → ( 𝑦 ≤ ( ( 𝑃 − 1 ) / 2 ) → 0 < ( 𝑃 − 𝑦 ) ) )
276	275	ex	⊢ ( ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ) → ( ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 2 ∥ 𝑦 ) → ( 𝑦 ≤ ( ( 𝑃 − 1 ) / 2 ) → 0 < ( 𝑃 − 𝑦 ) ) ) )
277	276	com23	⊢ ( ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ) → ( 𝑦 ≤ ( ( 𝑃 − 1 ) / 2 ) → ( ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 2 ∥ 𝑦 ) → 0 < ( 𝑃 − 𝑦 ) ) ) )
278	189 277	biimtrid	⊢ ( ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ) → ( 𝑦 ≤ 𝐻 → ( ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 2 ∥ 𝑦 ) → 0 < ( 𝑃 − 𝑦 ) ) ) )
279	278	3impia	⊢ ( ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻 ) → ( ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 2 ∥ 𝑦 ) → 0 < ( 𝑃 − 𝑦 ) ) )
280	279	impcom	⊢ ( ( ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 2 ∥ 𝑦 ) ∧ ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻 ) ) → 0 < ( 𝑃 − 𝑦 ) )
281		elnnz	⊢ ( ( 𝑃 − 𝑦 ) ∈ ℕ ↔ ( ( 𝑃 − 𝑦 ) ∈ ℤ ∧ 0 < ( 𝑃 − 𝑦 ) ) )
282	215 280 281	sylanbrc	⊢ ( ( ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 2 ∥ 𝑦 ) ∧ ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻 ) ) → ( 𝑃 − 𝑦 ) ∈ ℕ )
283	23	adantr	⊢ ( ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 2 ∥ 𝑦 ) → ( 𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ) )
284		simpr	⊢ ( ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 2 ∥ 𝑦 ) → ¬ 2 ∥ 𝑦 )
285	284 213	anim12ci	⊢ ( ( ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 2 ∥ 𝑦 ) ∧ ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻 ) ) → ( 𝑦 ∈ ℤ ∧ ¬ 2 ∥ 𝑦 ) )
286		omoe	⊢ ( ( ( 𝑃 ∈ ℤ ∧ ¬ 2 ∥ 𝑃 ) ∧ ( 𝑦 ∈ ℤ ∧ ¬ 2 ∥ 𝑦 ) ) → 2 ∥ ( 𝑃 − 𝑦 ) )
287	283 285 286	syl2an2r	⊢ ( ( ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 2 ∥ 𝑦 ) ∧ ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻 ) ) → 2 ∥ ( 𝑃 − 𝑦 ) )
288		nnehalf	⊢ ( ( ( 𝑃 − 𝑦 ) ∈ ℕ ∧ 2 ∥ ( 𝑃 − 𝑦 ) ) → ( ( 𝑃 − 𝑦 ) / 2 ) ∈ ℕ )
289	282 287 288	syl2anc	⊢ ( ( ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 2 ∥ 𝑦 ) ∧ ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻 ) ) → ( ( 𝑃 − 𝑦 ) / 2 ) ∈ ℕ )
290		simpr2	⊢ ( ( ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 2 ∥ 𝑦 ) ∧ ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻 ) ) → 𝐻 ∈ ℕ )
291		1red	⊢ ( ( ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 2 ∥ 𝑦 ) ∧ ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻 ) ) → 1 ∈ ℝ )
292	155	3ad2ant1	⊢ ( ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻 ) → 𝑦 ∈ ℝ )
293	292	adantl	⊢ ( ( ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 2 ∥ 𝑦 ) ∧ ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻 ) ) → 𝑦 ∈ ℝ )
294	54 63	syl	⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → 𝑃 ∈ ℝ )
295	294	ad2antrr	⊢ ( ( ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 2 ∥ 𝑦 ) ∧ ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻 ) ) → 𝑃 ∈ ℝ )
296		nnge1	⊢ ( 𝑦 ∈ ℕ → 1 ≤ 𝑦 )
297	296	3ad2ant1	⊢ ( ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻 ) → 1 ≤ 𝑦 )
298	297	adantl	⊢ ( ( ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 2 ∥ 𝑦 ) ∧ ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻 ) ) → 1 ≤ 𝑦 )
299	291 293 295 298	lesub2dd	⊢ ( ( ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 2 ∥ 𝑦 ) ∧ ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻 ) ) → ( 𝑃 − 𝑦 ) ≤ ( 𝑃 − 1 ) )
300	295 293	resubcld	⊢ ( ( ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 2 ∥ 𝑦 ) ∧ ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻 ) ) → ( 𝑃 − 𝑦 ) ∈ ℝ )
301	54 63 67	3syl	⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → ( 𝑃 − 1 ) ∈ ℝ )
302	301	ad2antrr	⊢ ( ( ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 2 ∥ 𝑦 ) ∧ ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻 ) ) → ( 𝑃 − 1 ) ∈ ℝ )
303	71	a1i	⊢ ( ( ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 2 ∥ 𝑦 ) ∧ ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻 ) ) → ( 2 ∈ ℝ ∧ 0 < 2 ) )
304		lediv1	⊢ ( ( ( 𝑃 − 𝑦 ) ∈ ℝ ∧ ( 𝑃 − 1 ) ∈ ℝ ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) → ( ( 𝑃 − 𝑦 ) ≤ ( 𝑃 − 1 ) ↔ ( ( 𝑃 − 𝑦 ) / 2 ) ≤ ( ( 𝑃 − 1 ) / 2 ) ) )
305	300 302 303 304	syl3anc	⊢ ( ( ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 2 ∥ 𝑦 ) ∧ ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻 ) ) → ( ( 𝑃 − 𝑦 ) ≤ ( 𝑃 − 1 ) ↔ ( ( 𝑃 − 𝑦 ) / 2 ) ≤ ( ( 𝑃 − 1 ) / 2 ) ) )
306	299 305	mpbid	⊢ ( ( ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 2 ∥ 𝑦 ) ∧ ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻 ) ) → ( ( 𝑃 − 𝑦 ) / 2 ) ≤ ( ( 𝑃 − 1 ) / 2 ) )
307	2	breq2i	⊢ ( ( ( 𝑃 − 𝑦 ) / 2 ) ≤ 𝐻 ↔ ( ( 𝑃 − 𝑦 ) / 2 ) ≤ ( ( 𝑃 − 1 ) / 2 ) )
308	306 307	sylibr	⊢ ( ( ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 2 ∥ 𝑦 ) ∧ ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻 ) ) → ( ( 𝑃 − 𝑦 ) / 2 ) ≤ 𝐻 )
309	289 290 308	3jca	⊢ ( ( ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 2 ∥ 𝑦 ) ∧ ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻 ) ) → ( ( ( 𝑃 − 𝑦 ) / 2 ) ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ ( ( 𝑃 − 𝑦 ) / 2 ) ≤ 𝐻 ) )
310	309	ex	⊢ ( ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 2 ∥ 𝑦 ) → ( ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻 ) → ( ( ( 𝑃 − 𝑦 ) / 2 ) ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ ( ( 𝑃 − 𝑦 ) / 2 ) ≤ 𝐻 ) ) )
311		elfz1b	⊢ ( ( ( 𝑃 − 𝑦 ) / 2 ) ∈ ( 1 ... 𝐻 ) ↔ ( ( ( 𝑃 − 𝑦 ) / 2 ) ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ ( ( 𝑃 − 𝑦 ) / 2 ) ≤ 𝐻 ) )
312	310 149 311	3imtr4g	⊢ ( ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ¬ 2 ∥ 𝑦 ) → ( 𝑦 ∈ ( 1 ... 𝐻 ) → ( ( 𝑃 − 𝑦 ) / 2 ) ∈ ( 1 ... 𝐻 ) ) )
313	312	ex	⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → ( ¬ 2 ∥ 𝑦 → ( 𝑦 ∈ ( 1 ... 𝐻 ) → ( ( 𝑃 − 𝑦 ) / 2 ) ∈ ( 1 ... 𝐻 ) ) ) )
314	1 313	syl	⊢ ( 𝜑 → ( ¬ 2 ∥ 𝑦 → ( 𝑦 ∈ ( 1 ... 𝐻 ) → ( ( 𝑃 − 𝑦 ) / 2 ) ∈ ( 1 ... 𝐻 ) ) ) )
315	314	3imp21	⊢ ( ( ¬ 2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ ( 1 ... 𝐻 ) ) → ( ( 𝑃 − 𝑦 ) / 2 ) ∈ ( 1 ... 𝐻 ) )
316		oveq1	⊢ ( 𝑥 = ( ( 𝑃 − 𝑦 ) / 2 ) → ( 𝑥 · 2 ) = ( ( ( 𝑃 − 𝑦 ) / 2 ) · 2 ) )
317	316	breq1d	⊢ ( 𝑥 = ( ( 𝑃 − 𝑦 ) / 2 ) → ( ( 𝑥 · 2 ) < ( 𝑃 / 2 ) ↔ ( ( ( 𝑃 − 𝑦 ) / 2 ) · 2 ) < ( 𝑃 / 2 ) ) )
318	316	oveq2d	⊢ ( 𝑥 = ( ( 𝑃 − 𝑦 ) / 2 ) → ( 𝑃 − ( 𝑥 · 2 ) ) = ( 𝑃 − ( ( ( 𝑃 − 𝑦 ) / 2 ) · 2 ) ) )
319	317 316 318	ifbieq12d	⊢ ( 𝑥 = ( ( 𝑃 − 𝑦 ) / 2 ) → if ( ( 𝑥 · 2 ) < ( 𝑃 / 2 ) , ( 𝑥 · 2 ) , ( 𝑃 − ( 𝑥 · 2 ) ) ) = if ( ( ( ( 𝑃 − 𝑦 ) / 2 ) · 2 ) < ( 𝑃 / 2 ) , ( ( ( 𝑃 − 𝑦 ) / 2 ) · 2 ) , ( 𝑃 − ( ( ( 𝑃 − 𝑦 ) / 2 ) · 2 ) ) ) )
320	319	eqeq2d	⊢ ( 𝑥 = ( ( 𝑃 − 𝑦 ) / 2 ) → ( 𝑦 = if ( ( 𝑥 · 2 ) < ( 𝑃 / 2 ) , ( 𝑥 · 2 ) , ( 𝑃 − ( 𝑥 · 2 ) ) ) ↔ 𝑦 = if ( ( ( ( 𝑃 − 𝑦 ) / 2 ) · 2 ) < ( 𝑃 / 2 ) , ( ( ( 𝑃 − 𝑦 ) / 2 ) · 2 ) , ( 𝑃 − ( ( ( 𝑃 − 𝑦 ) / 2 ) · 2 ) ) ) ) )
321	320	adantl	⊢ ( ( ( ¬ 2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ ( 1 ... 𝐻 ) ) ∧ 𝑥 = ( ( 𝑃 − 𝑦 ) / 2 ) ) → ( 𝑦 = if ( ( 𝑥 · 2 ) < ( 𝑃 / 2 ) , ( 𝑥 · 2 ) , ( 𝑃 − ( 𝑥 · 2 ) ) ) ↔ 𝑦 = if ( ( ( ( 𝑃 − 𝑦 ) / 2 ) · 2 ) < ( 𝑃 / 2 ) , ( ( ( 𝑃 − 𝑦 ) / 2 ) · 2 ) , ( 𝑃 − ( ( ( 𝑃 − 𝑦 ) / 2 ) · 2 ) ) ) ) )
322	1 54 227	3syl	⊢ ( 𝜑 → 𝑃 ∈ ℂ )
323	322	3ad2ant2	⊢ ( ( ¬ 2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ ( 1 ... 𝐻 ) ) → 𝑃 ∈ ℂ )
324	183	3ad2ant3	⊢ ( ( ¬ 2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ ( 1 ... 𝐻 ) ) → 𝑦 ∈ ℂ )
325	323 324	subcld	⊢ ( ( ¬ 2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ ( 1 ... 𝐻 ) ) → ( 𝑃 − 𝑦 ) ∈ ℂ )
326		2cnd	⊢ ( ( ¬ 2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ ( 1 ... 𝐻 ) ) → 2 ∈ ℂ )
327	186	a1i	⊢ ( ( ¬ 2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ ( 1 ... 𝐻 ) ) → 2 ≠ 0 )
328	325 326 327	divcan1d	⊢ ( ( ¬ 2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ ( 1 ... 𝐻 ) ) → ( ( ( 𝑃 − 𝑦 ) / 2 ) · 2 ) = ( 𝑃 − 𝑦 ) )
329		zre	⊢ ( 𝑃 ∈ ℤ → 𝑃 ∈ ℝ )
330		halfge0	⊢ 0 ≤ ( 1 / 2 )
331		rehalfcl	⊢ ( 𝑃 ∈ ℝ → ( 𝑃 / 2 ) ∈ ℝ )
332	331	adantl	⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ ) → ( 𝑃 / 2 ) ∈ ℝ )
333	332 259	subge02d	⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ ) → ( 0 ≤ ( 1 / 2 ) ↔ ( ( 𝑃 / 2 ) − ( 1 / 2 ) ) ≤ ( 𝑃 / 2 ) ) )
334	330 333	mpbii	⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ ) → ( ( 𝑃 / 2 ) − ( 1 / 2 ) ) ≤ ( 𝑃 / 2 ) )
335		simpl	⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ ) → 𝑦 ∈ ℝ )
336	245	a1i	⊢ ( 𝑃 ∈ ℝ → ( 1 / 2 ) ∈ ℝ )
337	331 336	resubcld	⊢ ( 𝑃 ∈ ℝ → ( ( 𝑃 / 2 ) − ( 1 / 2 ) ) ∈ ℝ )
338	337	adantl	⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ ) → ( ( 𝑃 / 2 ) − ( 1 / 2 ) ) ∈ ℝ )
339		letr	⊢ ( ( 𝑦 ∈ ℝ ∧ ( ( 𝑃 / 2 ) − ( 1 / 2 ) ) ∈ ℝ ∧ ( 𝑃 / 2 ) ∈ ℝ ) → ( ( 𝑦 ≤ ( ( 𝑃 / 2 ) − ( 1 / 2 ) ) ∧ ( ( 𝑃 / 2 ) − ( 1 / 2 ) ) ≤ ( 𝑃 / 2 ) ) → 𝑦 ≤ ( 𝑃 / 2 ) ) )
340	335 338 332 339	syl3anc	⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ ) → ( ( 𝑦 ≤ ( ( 𝑃 / 2 ) − ( 1 / 2 ) ) ∧ ( ( 𝑃 / 2 ) − ( 1 / 2 ) ) ≤ ( 𝑃 / 2 ) ) → 𝑦 ≤ ( 𝑃 / 2 ) ) )
341	334 340	mpan2d	⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ ) → ( 𝑦 ≤ ( ( 𝑃 / 2 ) − ( 1 / 2 ) ) → 𝑦 ≤ ( 𝑃 / 2 ) ) )
342	80	adantl	⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ ) → 𝑃 ∈ ℂ )
343		1cnd	⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ ) → 1 ∈ ℂ )
344	229	a1i	⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ ) → ( 2 ∈ ℂ ∧ 2 ≠ 0 ) )
345	342 343 344 231	syl3anc	⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ ) → ( ( 𝑃 − 1 ) / 2 ) = ( ( 𝑃 / 2 ) − ( 1 / 2 ) ) )
346	345	breq2d	⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ ) → ( 𝑦 ≤ ( ( 𝑃 − 1 ) / 2 ) ↔ 𝑦 ≤ ( ( 𝑃 / 2 ) − ( 1 / 2 ) ) ) )
347		lesub	⊢ ( ( ( 𝑃 / 2 ) ∈ ℝ ∧ 𝑃 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( 𝑃 / 2 ) ≤ ( 𝑃 − 𝑦 ) ↔ 𝑦 ≤ ( 𝑃 − ( 𝑃 / 2 ) ) ) )
348	332 257 335 347	syl3anc	⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ ) → ( ( 𝑃 / 2 ) ≤ ( 𝑃 − 𝑦 ) ↔ 𝑦 ≤ ( 𝑃 − ( 𝑃 / 2 ) ) ) )
349	258 262	lenltd	⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ ) → ( ( 𝑃 / 2 ) ≤ ( 𝑃 − 𝑦 ) ↔ ¬ ( 𝑃 − 𝑦 ) < ( 𝑃 / 2 ) ) )
350		2cnd	⊢ ( 𝑃 ∈ ℝ → 2 ∈ ℂ )
351	186	a1i	⊢ ( 𝑃 ∈ ℝ → 2 ≠ 0 )
352	80 350 351	divcan1d	⊢ ( 𝑃 ∈ ℝ → ( ( 𝑃 / 2 ) · 2 ) = 𝑃 )
353	352	eqcomd	⊢ ( 𝑃 ∈ ℝ → 𝑃 = ( ( 𝑃 / 2 ) · 2 ) )
354	353	oveq1d	⊢ ( 𝑃 ∈ ℝ → ( 𝑃 − ( 𝑃 / 2 ) ) = ( ( ( 𝑃 / 2 ) · 2 ) − ( 𝑃 / 2 ) ) )
355	331	recnd	⊢ ( 𝑃 ∈ ℝ → ( 𝑃 / 2 ) ∈ ℂ )
356	355 350	mulcomd	⊢ ( 𝑃 ∈ ℝ → ( ( 𝑃 / 2 ) · 2 ) = ( 2 · ( 𝑃 / 2 ) ) )
357	356	oveq1d	⊢ ( 𝑃 ∈ ℝ → ( ( ( 𝑃 / 2 ) · 2 ) − ( 𝑃 / 2 ) ) = ( ( 2 · ( 𝑃 / 2 ) ) − ( 𝑃 / 2 ) ) )
358	350 355	mulsubfacd	⊢ ( 𝑃 ∈ ℝ → ( ( 2 · ( 𝑃 / 2 ) ) − ( 𝑃 / 2 ) ) = ( ( 2 − 1 ) · ( 𝑃 / 2 ) ) )
359		2m1e1	⊢ ( 2 − 1 ) = 1
360	359	a1i	⊢ ( 𝑃 ∈ ℝ → ( 2 − 1 ) = 1 )
361	360	oveq1d	⊢ ( 𝑃 ∈ ℝ → ( ( 2 − 1 ) · ( 𝑃 / 2 ) ) = ( 1 · ( 𝑃 / 2 ) ) )
362	355	mullidd	⊢ ( 𝑃 ∈ ℝ → ( 1 · ( 𝑃 / 2 ) ) = ( 𝑃 / 2 ) )
363	358 361 362	3eqtrd	⊢ ( 𝑃 ∈ ℝ → ( ( 2 · ( 𝑃 / 2 ) ) − ( 𝑃 / 2 ) ) = ( 𝑃 / 2 ) )
364	354 357 363	3eqtrd	⊢ ( 𝑃 ∈ ℝ → ( 𝑃 − ( 𝑃 / 2 ) ) = ( 𝑃 / 2 ) )
365	364	adantl	⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ ) → ( 𝑃 − ( 𝑃 / 2 ) ) = ( 𝑃 / 2 ) )
366	365	breq2d	⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ ) → ( 𝑦 ≤ ( 𝑃 − ( 𝑃 / 2 ) ) ↔ 𝑦 ≤ ( 𝑃 / 2 ) ) )
367	348 349 366	3bitr3d	⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ ) → ( ¬ ( 𝑃 − 𝑦 ) < ( 𝑃 / 2 ) ↔ 𝑦 ≤ ( 𝑃 / 2 ) ) )
368	341 346 367	3imtr4d	⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑃 ∈ ℝ ) → ( 𝑦 ≤ ( ( 𝑃 − 1 ) / 2 ) → ¬ ( 𝑃 − 𝑦 ) < ( 𝑃 / 2 ) ) )
369	368	ex	⊢ ( 𝑦 ∈ ℝ → ( 𝑃 ∈ ℝ → ( 𝑦 ≤ ( ( 𝑃 − 1 ) / 2 ) → ¬ ( 𝑃 − 𝑦 ) < ( 𝑃 / 2 ) ) ) )
370	155 369	syl	⊢ ( 𝑦 ∈ ℕ → ( 𝑃 ∈ ℝ → ( 𝑦 ≤ ( ( 𝑃 − 1 ) / 2 ) → ¬ ( 𝑃 − 𝑦 ) < ( 𝑃 / 2 ) ) ) )
371	370	com3l	⊢ ( 𝑃 ∈ ℝ → ( 𝑦 ≤ ( ( 𝑃 − 1 ) / 2 ) → ( 𝑦 ∈ ℕ → ¬ ( 𝑃 − 𝑦 ) < ( 𝑃 / 2 ) ) ) )
372	329 371	syl	⊢ ( 𝑃 ∈ ℤ → ( 𝑦 ≤ ( ( 𝑃 − 1 ) / 2 ) → ( 𝑦 ∈ ℕ → ¬ ( 𝑃 − 𝑦 ) < ( 𝑃 / 2 ) ) ) )
373	54 55 372	3syl	⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → ( 𝑦 ≤ ( ( 𝑃 − 1 ) / 2 ) → ( 𝑦 ∈ ℕ → ¬ ( 𝑃 − 𝑦 ) < ( 𝑃 / 2 ) ) ) )
374	1 373	syl	⊢ ( 𝜑 → ( 𝑦 ≤ ( ( 𝑃 − 1 ) / 2 ) → ( 𝑦 ∈ ℕ → ¬ ( 𝑃 − 𝑦 ) < ( 𝑃 / 2 ) ) ) )
375	374	adantl	⊢ ( ( ¬ 2 ∥ 𝑦 ∧ 𝜑 ) → ( 𝑦 ≤ ( ( 𝑃 − 1 ) / 2 ) → ( 𝑦 ∈ ℕ → ¬ ( 𝑃 − 𝑦 ) < ( 𝑃 / 2 ) ) ) )
376	375	com13	⊢ ( 𝑦 ∈ ℕ → ( 𝑦 ≤ ( ( 𝑃 − 1 ) / 2 ) → ( ( ¬ 2 ∥ 𝑦 ∧ 𝜑 ) → ¬ ( 𝑃 − 𝑦 ) < ( 𝑃 / 2 ) ) ) )
377	189 376	biimtrid	⊢ ( 𝑦 ∈ ℕ → ( 𝑦 ≤ 𝐻 → ( ( ¬ 2 ∥ 𝑦 ∧ 𝜑 ) → ¬ ( 𝑃 − 𝑦 ) < ( 𝑃 / 2 ) ) ) )
378	377	a1d	⊢ ( 𝑦 ∈ ℕ → ( 𝐻 ∈ ℕ → ( 𝑦 ≤ 𝐻 → ( ( ¬ 2 ∥ 𝑦 ∧ 𝜑 ) → ¬ ( 𝑃 − 𝑦 ) < ( 𝑃 / 2 ) ) ) ) )
379	378	3imp	⊢ ( ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻 ) → ( ( ¬ 2 ∥ 𝑦 ∧ 𝜑 ) → ¬ ( 𝑃 − 𝑦 ) < ( 𝑃 / 2 ) ) )
380	379	com12	⊢ ( ( ¬ 2 ∥ 𝑦 ∧ 𝜑 ) → ( ( 𝑦 ∈ ℕ ∧ 𝐻 ∈ ℕ ∧ 𝑦 ≤ 𝐻 ) → ¬ ( 𝑃 − 𝑦 ) < ( 𝑃 / 2 ) ) )
381	149 380	biimtrid	⊢ ( ( ¬ 2 ∥ 𝑦 ∧ 𝜑 ) → ( 𝑦 ∈ ( 1 ... 𝐻 ) → ¬ ( 𝑃 − 𝑦 ) < ( 𝑃 / 2 ) ) )
382	381	3impia	⊢ ( ( ¬ 2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ ( 1 ... 𝐻 ) ) → ¬ ( 𝑃 − 𝑦 ) < ( 𝑃 / 2 ) )
383	328 382	eqnbrtrd	⊢ ( ( ¬ 2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ ( 1 ... 𝐻 ) ) → ¬ ( ( ( 𝑃 − 𝑦 ) / 2 ) · 2 ) < ( 𝑃 / 2 ) )
384	383	iffalsed	⊢ ( ( ¬ 2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ ( 1 ... 𝐻 ) ) → if ( ( ( ( 𝑃 − 𝑦 ) / 2 ) · 2 ) < ( 𝑃 / 2 ) , ( ( ( 𝑃 − 𝑦 ) / 2 ) · 2 ) , ( 𝑃 − ( ( ( 𝑃 − 𝑦 ) / 2 ) · 2 ) ) ) = ( 𝑃 − ( ( ( 𝑃 − 𝑦 ) / 2 ) · 2 ) ) )
385	328	oveq2d	⊢ ( ( ¬ 2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ ( 1 ... 𝐻 ) ) → ( 𝑃 − ( ( ( 𝑃 − 𝑦 ) / 2 ) · 2 ) ) = ( 𝑃 − ( 𝑃 − 𝑦 ) ) )
386	322 183	anim12i	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 1 ... 𝐻 ) ) → ( 𝑃 ∈ ℂ ∧ 𝑦 ∈ ℂ ) )
387	386	3adant1	⊢ ( ( ¬ 2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ ( 1 ... 𝐻 ) ) → ( 𝑃 ∈ ℂ ∧ 𝑦 ∈ ℂ ) )
388		nncan	⊢ ( ( 𝑃 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑃 − ( 𝑃 − 𝑦 ) ) = 𝑦 )
389	387 388	syl	⊢ ( ( ¬ 2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ ( 1 ... 𝐻 ) ) → ( 𝑃 − ( 𝑃 − 𝑦 ) ) = 𝑦 )
390	384 385 389	3eqtrrd	⊢ ( ( ¬ 2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ ( 1 ... 𝐻 ) ) → 𝑦 = if ( ( ( ( 𝑃 − 𝑦 ) / 2 ) · 2 ) < ( 𝑃 / 2 ) , ( ( ( 𝑃 − 𝑦 ) / 2 ) · 2 ) , ( 𝑃 − ( ( ( 𝑃 − 𝑦 ) / 2 ) · 2 ) ) ) )
391	315 321 390	rspcedvd	⊢ ( ( ¬ 2 ∥ 𝑦 ∧ 𝜑 ∧ 𝑦 ∈ ( 1 ... 𝐻 ) ) → ∃ 𝑥 ∈ ( 1 ... 𝐻 ) 𝑦 = if ( ( 𝑥 · 2 ) < ( 𝑃 / 2 ) , ( 𝑥 · 2 ) , ( 𝑃 − ( 𝑥 · 2 ) ) ) )
392	391	3exp	⊢ ( ¬ 2 ∥ 𝑦 → ( 𝜑 → ( 𝑦 ∈ ( 1 ... 𝐻 ) → ∃ 𝑥 ∈ ( 1 ... 𝐻 ) 𝑦 = if ( ( 𝑥 · 2 ) < ( 𝑃 / 2 ) , ( 𝑥 · 2 ) , ( 𝑃 − ( 𝑥 · 2 ) ) ) ) ) )
393	210 392	pm2.61i	⊢ ( 𝜑 → ( 𝑦 ∈ ( 1 ... 𝐻 ) → ∃ 𝑥 ∈ ( 1 ... 𝐻 ) 𝑦 = if ( ( 𝑥 · 2 ) < ( 𝑃 / 2 ) , ( 𝑥 · 2 ) , ( 𝑃 − ( 𝑥 · 2 ) ) ) ) )
394	148 393	impbid	⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ( 1 ... 𝐻 ) 𝑦 = if ( ( 𝑥 · 2 ) < ( 𝑃 / 2 ) , ( 𝑥 · 2 ) , ( 𝑃 − ( 𝑥 · 2 ) ) ) ↔ 𝑦 ∈ ( 1 ... 𝐻 ) ) )
395	5 394	bitrid	⊢ ( 𝜑 → ( 𝑦 ∈ ran 𝑅 ↔ 𝑦 ∈ ( 1 ... 𝐻 ) ) )
396	395	eqrdv	⊢ ( 𝜑 → ran 𝑅 = ( 1 ... 𝐻 ) )