gausslemma2dlem1a

	Ref	Expression
Hypotheses	gausslemma2d.p	$⊢ φ \to P \in (ℙ ∖ \{2\})$
	gausslemma2d.h	$⊢ H = \frac{P - 1}{2}$
	gausslemma2d.r	$⊢ R = (x \in (1 \dots H) ⟼ if (x \cdot 2 < \frac{P}{2}, x \cdot 2, P - x \cdot 2))$
Assertion	gausslemma2dlem1a	$⊢ φ \to ran R = (1 \dots H)$

Proof

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

Metamath Proof Explorer

Theorem gausslemma2dlem1a

Proof