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	63 91	syl	$⊢ P \in ℙ \to (x \in (1 \dots H) \to 1 \leq P - x \cdot 2)$
93	1 54 92	3syl	$⊢ φ \to (x \in (1 \dots H) \to 1 \leq P - x \cdot 2)$
94	93	imp	$⊢ (φ \land x \in (1 \dots H)) \to 1 \leq P - x \cdot 2$
95	94	adantl	$⊢ (\neg x \cdot 2 < \frac{P}{2} \land (φ \land x \in (1 \dots H))) \to 1 \leq P - x \cdot 2$
96		elnnz1	$⊢ P - x \cdot 2 \in ℕ \leftrightarrow (P - x \cdot 2 \in ℤ \land 1 \leq P - x \cdot 2)$
97	62 95 96	sylanbrc	$⊢ (\neg x \cdot 2 < \frac{P}{2} \land (φ \land x \in (1 \dots H))) \to P - x \cdot 2 \in ℕ$
98	9	simp2bi	$⊢ x \in (1 \dots H) \to H \in ℕ$
99	98	ad2antll	$⊢ (\neg x \cdot 2 < \frac{P}{2} \land (φ \land x \in (1 \dots H))) \to H \in ℕ$
100		nnre	$⊢ P \in ℕ \to P \in ℝ$
101	100	rehalfcld	$⊢ P \in ℕ \to \frac{P}{2} \in ℝ$
102	101	adantr	$⊢ (P \in ℕ \land \neg 2 ∥ P) \to \frac{P}{2} \in ℝ$
103	60	zred	$⊢ x \in (1 \dots H) \to x \cdot 2 \in ℝ$
104		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})$
105	102 103 104	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})$
106	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 ℤ)$
107	106 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 ℤ)$
108		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)$
109	107 108	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)$
110	109	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$
111		nncn	$⊢ P \in ℕ \to P \in ℂ$
112		subhalfhalf	$⊢ P \in ℂ \to P - (\frac{P}{2}) = \frac{P}{2}$
113	111 112	syl	$⊢ P \in ℕ \to P - (\frac{P}{2}) = \frac{P}{2}$
114	113	breq1d	$⊢ P \in ℕ \to (P - (\frac{P}{2}) < x \cdot 2 \leftrightarrow \frac{P}{2} < x \cdot 2)$
115	114	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)$
116	110 115	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$
117	100	ad2antrr	$⊢ ((P \in ℕ \land \neg 2 ∥ P) \land x \in (1 \dots H)) \to P \in ℝ$
118	101	ad2antrr	$⊢ ((P \in ℕ \land \neg 2 ∥ P) \land x \in (1 \dots H)) \to \frac{P}{2} \in ℝ$
119	103	adantl	$⊢ ((P \in ℕ \land \neg 2 ∥ P) \land x \in (1 \dots H)) \to x \cdot 2 \in ℝ$
120	117 118 119	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 ℝ)$
121	120	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 ℝ)$
122		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})$
123	121 122	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})$
124	116 123	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}$
125	21	ad2antrr	$⊢ ((P \in ℕ \land \neg 2 ∥ P) \land x \in (1 \dots H)) \to P \in ℤ$
126		simplr	$⊢ ((P \in ℕ \land \neg 2 ∥ P) \land x \in (1 \dots H)) \to \neg 2 ∥ P$
127	60	adantl	$⊢ ((P \in ℕ \land \neg 2 ∥ P) \land x \in (1 \dots H)) \to x \cdot 2 \in ℤ$
128	125 127	zsubcld	$⊢ ((P \in ℕ \land \neg 2 ∥ P) \land x \in (1 \dots H)) \to P - x \cdot 2 \in ℤ$
129	125 126 128	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 ℤ)$
130	129	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 ℤ)$
131		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})$
132	130 131	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})$
133	124 132	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}$
134	133	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})$
135	2	breq2i	$⊢ P - x \cdot 2 \leq H \leftrightarrow P - x \cdot 2 \leq \frac{P - 1}{2}$
136	134 135	syl6ibr	$⊢ ((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)$
137	105 136	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)$
138	137	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))$
139	1 20 138	3syl	$⊢ φ \to (x \in (1 \dots H) \to (\neg x \cdot 2 < \frac{P}{2} \to P - x \cdot 2 \leq H))$
140	139	imp	$⊢ (φ \land x \in (1 \dots H)) \to (\neg x \cdot 2 < \frac{P}{2} \to P - x \cdot 2 \leq H)$
141	140	impcom	$⊢ (\neg x \cdot 2 < \frac{P}{2} \land (φ \land x \in (1 \dots H))) \to P - x \cdot 2 \leq H$
142		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)$
143	97 99 141 142	syl3anbrc	$⊢ (\neg x \cdot 2 < \frac{P}{2} \land (φ \land x \in (1 \dots H))) \to P - x \cdot 2 \in (1 \dots H)$
144		eleq1	$⊢ y = P - x \cdot 2 \to (y \in (1 \dots H) \leftrightarrow P - x \cdot 2 \in (1 \dots H))$
145	143 144	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))$
146	53 145	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))$
147	50 146	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))$
148	147	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))$
149		elfz1b	$⊢ y \in (1 \dots H) \leftrightarrow (y \in ℕ \land H \in ℕ \land y \leq H)$
150		simp1	$⊢ (y \in ℕ \land H \in ℕ \land y \leq H) \to y \in ℕ$
151		simpl	$⊢ (2 ∥ y \land φ) \to 2 ∥ y$
152		nnehalf	$⊢ (y \in ℕ \land 2 ∥ y) \to \frac{y}{2} \in ℕ$
153	150 151 152	syl2anr	$⊢ ((2 ∥ y \land φ) \land (y \in ℕ \land H \in ℕ \land y \leq H)) \to \frac{y}{2} \in ℕ$
154		simpr2	$⊢ ((2 ∥ y \land φ) \land (y \in ℕ \land H \in ℕ \land y \leq H)) \to H \in ℕ$
155		nnre	$⊢ y \in ℕ \to y \in ℝ$
156	155	ad2antrr	$⊢ ((y \in ℕ \land H \in ℕ) \land (2 ∥ y \land φ)) \to y \in ℝ$
157		nnrp	$⊢ H \in ℕ \to H \in ℝ^{+}$
158	157	adantl	$⊢ (y \in ℕ \land H \in ℕ) \to H \in ℝ^{+}$
159	158	adantr	$⊢ ((y \in ℕ \land H \in ℕ) \land (2 ∥ y \land φ)) \to H \in ℝ^{+}$
160		2rp	$⊢ 2 \in ℝ^{+}$
161		1le2	$⊢ 1 \leq 2$
162	160 161	pm3.2i	$⊢ (2 \in ℝ^{+} \land 1 \leq 2)$
163	162	a1i	$⊢ ((y \in ℕ \land H \in ℕ) \land (2 ∥ y \land φ)) \to (2 \in ℝ^{+} \land 1 \leq 2)$
164		ledivge1le	$⊢ (y \in ℝ \land H \in ℝ^{+} \land (2 \in ℝ^{+} \land 1 \leq 2)) \to (y \leq H \to \frac{y}{2} \leq H)$
165	156 159 163 164	syl3anc	$⊢ ((y \in ℕ \land H \in ℕ) \land (2 ∥ y \land φ)) \to (y \leq H \to \frac{y}{2} \leq H)$
166	165	ex	$⊢ (y \in ℕ \land H \in ℕ) \to ((2 ∥ y \land φ) \to (y \leq H \to \frac{y}{2} \leq H))$
167	166	com23	$⊢ (y \in ℕ \land H \in ℕ) \to (y \leq H \to ((2 ∥ y \land φ) \to \frac{y}{2} \leq H))$
168	167	3impia	$⊢ (y \in ℕ \land H \in ℕ \land y \leq H) \to ((2 ∥ y \land φ) \to \frac{y}{2} \leq H)$
169	168	impcom	$⊢ ((2 ∥ y \land φ) \land (y \in ℕ \land H \in ℕ \land y \leq H)) \to \frac{y}{2} \leq H$
170	153 154 169	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)$
171	170	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))$
172	149 171	biimtrid	$⊢ (2 ∥ y \land φ) \to (y \in (1 \dots H) \to (\frac{y}{2} \in ℕ \land H \in ℕ \land \frac{y}{2} \leq H))$
173	172	3impia	$⊢ (2 ∥ y \land φ \land y \in (1 \dots H)) \to (\frac{y}{2} \in ℕ \land H \in ℕ \land \frac{y}{2} \leq H)$
174		elfz1b	$⊢ \frac{y}{2} \in (1 \dots H) \leftrightarrow (\frac{y}{2} \in ℕ \land H \in ℕ \land \frac{y}{2} \leq H)$
175	173 174	sylibr	$⊢ (2 ∥ y \land φ \land y \in (1 \dots H)) \to \frac{y}{2} \in (1 \dots H)$
176		oveq1	$⊢ x = \frac{y}{2} \to x \cdot 2 = (\frac{y}{2}) \cdot 2$
177	176	breq1d	$⊢ x = \frac{y}{2} \to (x \cdot 2 < \frac{P}{2} \leftrightarrow (\frac{y}{2}) \cdot 2 < \frac{P}{2})$
178	176	oveq2d	$⊢ x = \frac{y}{2} \to P - x \cdot 2 = P - (\frac{y}{2}) \cdot 2$
179	177 176 178	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)$
180	179	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))$
181	180	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))$
182		elfzelz	$⊢ y \in (1 \dots H) \to y \in ℤ$
183	182	zcnd	$⊢ y \in (1 \dots H) \to y \in ℂ$
184	183	3ad2ant3	$⊢ (2 ∥ y \land φ \land y \in (1 \dots H)) \to y \in ℂ$
185		2cnd	$⊢ (2 ∥ y \land φ \land y \in (1 \dots H)) \to 2 \in ℂ$
186		2ne0	$⊢ 2 \neq 0$
187	186	a1i	$⊢ (2 ∥ y \land φ \land y \in (1 \dots H)) \to 2 \neq 0$
188	184 185 187	divcan1d	$⊢ (2 ∥ y \land φ \land y \in (1 \dots H)) \to (\frac{y}{2}) \cdot 2 = y$
189	2	breq2i	$⊢ y \leq H \leftrightarrow y \leq \frac{P - 1}{2}$
190		nnz	$⊢ y \in ℕ \to y \in ℤ$
191	1 20 22	3syl	$⊢ φ \to (P \in ℤ \land \neg 2 ∥ P)$
192	191	adantl	$⊢ (2 ∥ y \land φ) \to (P \in ℤ \land \neg 2 ∥ P)$
193	190 192	anim12ci	$⊢ (y \in ℕ \land (2 ∥ y \land φ)) \to ((P \in ℤ \land \neg 2 ∥ P) \land y \in ℤ)$
194		df-3an	$⊢ (P \in ℤ \land \neg 2 ∥ P \land y \in ℤ) \leftrightarrow ((P \in ℤ \land \neg 2 ∥ P) \land y \in ℤ)$
195	193 194	sylibr	$⊢ (y \in ℕ \land (2 ∥ y \land φ)) \to (P \in ℤ \land \neg 2 ∥ P \land y \in ℤ)$
196		ltoddhalfle	$⊢ (P \in ℤ \land \neg 2 ∥ P \land y \in ℤ) \to (y < \frac{P}{2} \leftrightarrow y \leq \frac{P - 1}{2})$
197	195 196	syl	$⊢ (y \in ℕ \land (2 ∥ y \land φ)) \to (y < \frac{P}{2} \leftrightarrow y \leq \frac{P - 1}{2})$
198	197	exbiri	$⊢ y \in ℕ \to ((2 ∥ y \land φ) \to (y \leq \frac{P - 1}{2} \to y < \frac{P}{2}))$
199	198	com23	$⊢ y \in ℕ \to (y \leq \frac{P - 1}{2} \to ((2 ∥ y \land φ) \to y < \frac{P}{2}))$
200	189 199	biimtrid	$⊢ y \in ℕ \to (y \leq H \to ((2 ∥ y \land φ) \to y < \frac{P}{2}))$
201	200	a1d	$⊢ y \in ℕ \to (H \in ℕ \to (y \leq H \to ((2 ∥ y \land φ) \to y < \frac{P}{2})))$
202	201	3imp	$⊢ (y \in ℕ \land H \in ℕ \land y \leq H) \to ((2 ∥ y \land φ) \to y < \frac{P}{2})$
203	149 202	sylbi	$⊢ y \in (1 \dots H) \to ((2 ∥ y \land φ) \to y < \frac{P}{2})$
204	203	com12	$⊢ (2 ∥ y \land φ) \to (y \in (1 \dots H) \to y < \frac{P}{2})$
205	204	3impia	$⊢ (2 ∥ y \land φ \land y \in (1 \dots H)) \to y < \frac{P}{2}$
206	188 205	eqbrtrd	$⊢ (2 ∥ y \land φ \land y \in (1 \dots H)) \to (\frac{y}{2}) \cdot 2 < \frac{P}{2}$
207	206	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$
208	207 188	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)$
209	175 181 208	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)$
210	209	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)))$
211	54 55	syl	$⊢ P \in (ℙ ∖ \{2\}) \to P \in ℤ$
212	211	ad2antrr	$⊢ ((P \in (ℙ ∖ \{2\}) \land \neg 2 ∥ y) \land (y \in ℕ \land H \in ℕ \land y \leq H)) \to P \in ℤ$
213	190	3ad2ant1	$⊢ (y \in ℕ \land H \in ℕ \land y \leq H) \to y \in ℤ$
214	213	adantl	$⊢ ((P \in (ℙ ∖ \{2\}) \land \neg 2 ∥ y) \land (y \in ℕ \land H \in ℕ \land y \leq H)) \to y \in ℤ$
215	212 214	zsubcld	$⊢ ((P \in (ℙ ∖ \{2\}) \land \neg 2 ∥ y) \land (y \in ℕ \land H \in ℕ \land y \leq H)) \to P - y \in ℤ$
216	155	ad2antrl	$⊢ (P \in ℝ \land (y \in ℕ \land H \in ℕ)) \to y \in ℝ$
217	67	rehalfcld	$⊢ P \in ℝ \to \frac{P - 1}{2} \in ℝ$
218	217	adantr	$⊢ (P \in ℝ \land (y \in ℕ \land H \in ℕ)) \to \frac{P - 1}{2} \in ℝ$
219		simpl	$⊢ (P \in ℝ \land (y \in ℕ \land H \in ℕ)) \to P \in ℝ$
220	216 218 219	3jca	$⊢ (P \in ℝ \land (y \in ℕ \land H \in ℕ)) \to (y \in ℝ \land \frac{P - 1}{2} \in ℝ \land P \in ℝ)$
221	220	ex	$⊢ P \in ℝ \to ((y \in ℕ \land H \in ℕ) \to (y \in ℝ \land \frac{P - 1}{2} \in ℝ \land P \in ℝ))$
222	54 63 221	3syl	$⊢ P \in (ℙ ∖ \{2\}) \to ((y \in ℕ \land H \in ℕ) \to (y \in ℝ \land \frac{P - 1}{2} \in ℝ \land P \in ℝ))$
223	222	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 ℝ))$
224	223	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 ℝ)$
225		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)$
226	224 225	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)$
227	55	zcnd	$⊢ P \in ℙ \to P \in ℂ$
228		1cnd	$⊢ P \in ℂ \to 1 \in ℂ$
229		2cnne0	$⊢ (2 \in ℂ \land 2 \neq 0)$
230	229	a1i	$⊢ P \in ℂ \to (2 \in ℂ \land 2 \neq 0)$
231		divsubdir	$⊢ (P \in ℂ \land 1 \in ℂ \land (2 \in ℂ \land 2 \neq 0)) \to \frac{P - 1}{2} = (\frac{P}{2}) - (\frac{1}{2})$
232	228 230 231	mpd3an23	$⊢ P \in ℂ \to \frac{P - 1}{2} = (\frac{P}{2}) - (\frac{1}{2})$
233	232	oveq2d	$⊢ P \in ℂ \to P - (\frac{P - 1}{2}) = P - ((\frac{P}{2}) - (\frac{1}{2}))$
234		id	$⊢ P \in ℂ \to P \in ℂ$
235		halfcl	$⊢ P \in ℂ \to \frac{P}{2} \in ℂ$
236		halfcn	$⊢ \frac{1}{2} \in ℂ$
237	236	a1i	$⊢ P \in ℂ \to \frac{1}{2} \in ℂ$
238	234 235 237	subsubd	$⊢ P \in ℂ \to P - ((\frac{P}{2}) - (\frac{1}{2})) = P - (\frac{P}{2}) + (\frac{1}{2})$
239	112	oveq1d	$⊢ P \in ℂ \to P - (\frac{P}{2}) + (\frac{1}{2}) = (\frac{P}{2}) + (\frac{1}{2})$
240	233 238 239	3eqtrd	$⊢ P \in ℂ \to P - (\frac{P - 1}{2}) = (\frac{P}{2}) + (\frac{1}{2})$
241	54 227 240	3syl	$⊢ P \in (ℙ ∖ \{2\}) \to P - (\frac{P - 1}{2}) = (\frac{P}{2}) + (\frac{1}{2})$
242	241	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})$
243	242	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)$
244		prmnn	$⊢ P \in ℙ \to P \in ℕ$
245		halfre	$⊢ \frac{1}{2} \in ℝ$
246	245	a1i	$⊢ P \in ℕ \to \frac{1}{2} \in ℝ$
247		nngt0	$⊢ P \in ℕ \to 0 < P$
248	71	a1i	$⊢ P \in ℕ \to (2 \in ℝ \land 0 < 2)$
249		divgt0	$⊢ ((P \in ℝ \land 0 < P) \land (2 \in ℝ \land 0 < 2)) \to 0 < \frac{P}{2}$
250	100 247 248 249	syl21anc	$⊢ P \in ℕ \to 0 < \frac{P}{2}$
251		halfgt0	$⊢ 0 < \frac{1}{2}$
252	251	a1i	$⊢ P \in ℕ \to 0 < \frac{1}{2}$
253	101 246 250 252	addgt0d	$⊢ P \in ℕ \to 0 < (\frac{P}{2}) + (\frac{1}{2})$
254	54 244 253	3syl	$⊢ P \in (ℙ ∖ \{2\}) \to 0 < (\frac{P}{2}) + (\frac{1}{2})$
255	254	ad2antrl	$⊢ ((y \in ℕ \land H \in ℕ) \land (P \in (ℙ ∖ \{2\}) \land \neg 2 ∥ y)) \to 0 < (\frac{P}{2}) + (\frac{1}{2})$
256		0red	$⊢ (y \in ℝ \land P \in ℝ) \to 0 \in ℝ$
257		simpr	$⊢ (y \in ℝ \land P \in ℝ) \to P \in ℝ$
258	257	rehalfcld	$⊢ (y \in ℝ \land P \in ℝ) \to \frac{P}{2} \in ℝ$
259	245	a1i	$⊢ (y \in ℝ \land P \in ℝ) \to \frac{1}{2} \in ℝ$
260	258 259	readdcld	$⊢ (y \in ℝ \land P \in ℝ) \to (\frac{P}{2}) + (\frac{1}{2}) \in ℝ$
261		resubcl	$⊢ (P \in ℝ \land y \in ℝ) \to P - y \in ℝ$
262	261	ancoms	$⊢ (y \in ℝ \land P \in ℝ) \to P - y \in ℝ$
263	256 260 262	3jca	$⊢ (y \in ℝ \land P \in ℝ) \to (0 \in ℝ \land (\frac{P}{2}) + (\frac{1}{2}) \in ℝ \land P - y \in ℝ)$
264	263	ex	$⊢ y \in ℝ \to (P \in ℝ \to (0 \in ℝ \land (\frac{P}{2}) + (\frac{1}{2}) \in ℝ \land P - y \in ℝ))$
265	155 264	syl	$⊢ y \in ℕ \to (P \in ℝ \to (0 \in ℝ \land (\frac{P}{2}) + (\frac{1}{2}) \in ℝ \land P - y \in ℝ))$
266	265	adantr	$⊢ (y \in ℕ \land H \in ℕ) \to (P \in ℝ \to (0 \in ℝ \land (\frac{P}{2}) + (\frac{1}{2}) \in ℝ \land P - y \in ℝ))$
267	266	com12	$⊢ P \in ℝ \to ((y \in ℕ \land H \in ℕ) \to (0 \in ℝ \land (\frac{P}{2}) + (\frac{1}{2}) \in ℝ \land P - y \in ℝ))$
268	54 63 267	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 ℝ))$
269	268	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 ℝ))$
270	269	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 ℝ)$
271		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)$
272	270 271	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)$
273	255 272	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)$
274	243 273	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)$
275	226 274	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)$
276	275	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))$
277	276	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))$
278	189 277	biimtrid	$⊢ (y \in ℕ \land H \in ℕ) \to (y \leq H \to ((P \in (ℙ ∖ \{2\}) \land \neg 2 ∥ y) \to 0 < P - y))$
279	278	3impia	$⊢ (y \in ℕ \land H \in ℕ \land y \leq H) \to ((P \in (ℙ ∖ \{2\}) \land \neg 2 ∥ y) \to 0 < P - y)$
280	279	impcom	$⊢ ((P \in (ℙ ∖ \{2\}) \land \neg 2 ∥ y) \land (y \in ℕ \land H \in ℕ \land y \leq H)) \to 0 < P - y$
281		elnnz	$⊢ P - y \in ℕ \leftrightarrow (P - y \in ℤ \land 0 < P - y)$
282	215 280 281	sylanbrc	$⊢ ((P \in (ℙ ∖ \{2\}) \land \neg 2 ∥ y) \land (y \in ℕ \land H \in ℕ \land y \leq H)) \to P - y \in ℕ$
283	23	adantr	$⊢ (P \in (ℙ ∖ \{2\}) \land \neg 2 ∥ y) \to (P \in ℤ \land \neg 2 ∥ P)$
284		simpr	$⊢ (P \in (ℙ ∖ \{2\}) \land \neg 2 ∥ y) \to \neg 2 ∥ y$
285	284 213	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)$
286		omoe	$⊢ ((P \in ℤ \land \neg 2 ∥ P) \land (y \in ℤ \land \neg 2 ∥ y)) \to 2 ∥ (P - y)$
287	283 285 286	syl2an2r	$⊢ ((P \in (ℙ ∖ \{2\}) \land \neg 2 ∥ y) \land (y \in ℕ \land H \in ℕ \land y \leq H)) \to 2 ∥ (P - y)$
288		nnehalf	$⊢ (P - y \in ℕ \land 2 ∥ (P - y)) \to \frac{P - y}{2} \in ℕ$
289	282 287 288	syl2anc	$⊢ ((P \in (ℙ ∖ \{2\}) \land \neg 2 ∥ y) \land (y \in ℕ \land H \in ℕ \land y \leq H)) \to \frac{P - y}{2} \in ℕ$
290		simpr2	$⊢ ((P \in (ℙ ∖ \{2\}) \land \neg 2 ∥ y) \land (y \in ℕ \land H \in ℕ \land y \leq H)) \to H \in ℕ$
291		1red	$⊢ ((P \in (ℙ ∖ \{2\}) \land \neg 2 ∥ y) \land (y \in ℕ \land H \in ℕ \land y \leq H)) \to 1 \in ℝ$
292	155	3ad2ant1	$⊢ (y \in ℕ \land H \in ℕ \land y \leq H) \to y \in ℝ$
293	292	adantl	$⊢ ((P \in (ℙ ∖ \{2\}) \land \neg 2 ∥ y) \land (y \in ℕ \land H \in ℕ \land y \leq H)) \to y \in ℝ$
294	54 63	syl	$⊢ P \in (ℙ ∖ \{2\}) \to P \in ℝ$
295	294	ad2antrr	$⊢ ((P \in (ℙ ∖ \{2\}) \land \neg 2 ∥ y) \land (y \in ℕ \land H \in ℕ \land y \leq H)) \to P \in ℝ$
296		nnge1	$⊢ y \in ℕ \to 1 \leq y$
297	296	3ad2ant1	$⊢ (y \in ℕ \land H \in ℕ \land y \leq H) \to 1 \leq y$
298	297	adantl	$⊢ ((P \in (ℙ ∖ \{2\}) \land \neg 2 ∥ y) \land (y \in ℕ \land H \in ℕ \land y \leq H)) \to 1 \leq y$
299	291 293 295 298	lesub2dd	$⊢ ((P \in (ℙ ∖ \{2\}) \land \neg 2 ∥ y) \land (y \in ℕ \land H \in ℕ \land y \leq H)) \to P - y \leq P - 1$
300	295 293	resubcld	$⊢ ((P \in (ℙ ∖ \{2\}) \land \neg 2 ∥ y) \land (y \in ℕ \land H \in ℕ \land y \leq H)) \to P - y \in ℝ$
301	54 63 67	3syl	$⊢ P \in (ℙ ∖ \{2\}) \to P - 1 \in ℝ$
302	301	ad2antrr	$⊢ ((P \in (ℙ ∖ \{2\}) \land \neg 2 ∥ y) \land (y \in ℕ \land H \in ℕ \land y \leq H)) \to P - 1 \in ℝ$
303	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)$
304		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})$
305	300 302 303 304	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})$
306	299 305	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}$
307	2	breq2i	$⊢ \frac{P - y}{2} \leq H \leftrightarrow \frac{P - y}{2} \leq \frac{P - 1}{2}$
308	306 307	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$
309	289 290 308	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)$
310	309	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))$
311		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)$
312	310 149 311	3imtr4g	$⊢ (P \in (ℙ ∖ \{2\}) \land \neg 2 ∥ y) \to (y \in (1 \dots H) \to \frac{P - y}{2} \in (1 \dots H))$
313	312	ex	$⊢ P \in (ℙ ∖ \{2\}) \to (\neg 2 ∥ y \to (y \in (1 \dots H) \to \frac{P - y}{2} \in (1 \dots H)))$
314	1 313	syl	$⊢ φ \to (\neg 2 ∥ y \to (y \in (1 \dots H) \to \frac{P - y}{2} \in (1 \dots H)))$
315	314	3imp21	$⊢ (\neg 2 ∥ y \land φ \land y \in (1 \dots H)) \to \frac{P - y}{2} \in (1 \dots H)$
316		oveq1	$⊢ x = \frac{P - y}{2} \to x \cdot 2 = (\frac{P - y}{2}) \cdot 2$
317	316	breq1d	$⊢ x = \frac{P - y}{2} \to (x \cdot 2 < \frac{P}{2} \leftrightarrow (\frac{P - y}{2}) \cdot 2 < \frac{P}{2})$
318	316	oveq2d	$⊢ x = \frac{P - y}{2} \to P - x \cdot 2 = P - (\frac{P - y}{2}) \cdot 2$
319	317 316 318	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)$
320	319	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))$
321	320	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))$
322	1 54 227	3syl	$⊢ φ \to P \in ℂ$
323	322	3ad2ant2	$⊢ (\neg 2 ∥ y \land φ \land y \in (1 \dots H)) \to P \in ℂ$
324	183	3ad2ant3	$⊢ (\neg 2 ∥ y \land φ \land y \in (1 \dots H)) \to y \in ℂ$
325	323 324	subcld	$⊢ (\neg 2 ∥ y \land φ \land y \in (1 \dots H)) \to P - y \in ℂ$
326		2cnd	$⊢ (\neg 2 ∥ y \land φ \land y \in (1 \dots H)) \to 2 \in ℂ$
327	186	a1i	$⊢ (\neg 2 ∥ y \land φ \land y \in (1 \dots H)) \to 2 \neq 0$
328	325 326 327	divcan1d	$⊢ (\neg 2 ∥ y \land φ \land y \in (1 \dots H)) \to (\frac{P - y}{2}) \cdot 2 = P - y$
329		zre	$⊢ P \in ℤ \to P \in ℝ$
330		halfge0	$⊢ 0 \leq \frac{1}{2}$
331		rehalfcl	$⊢ P \in ℝ \to \frac{P}{2} \in ℝ$
332	331	adantl	$⊢ (y \in ℝ \land P \in ℝ) \to \frac{P}{2} \in ℝ$
333	332 259	subge02d	$⊢ (y \in ℝ \land P \in ℝ) \to (0 \leq \frac{1}{2} \leftrightarrow (\frac{P}{2}) - (\frac{1}{2}) \leq \frac{P}{2})$
334	330 333	mpbii	$⊢ (y \in ℝ \land P \in ℝ) \to (\frac{P}{2}) - (\frac{1}{2}) \leq \frac{P}{2}$
335		simpl	$⊢ (y \in ℝ \land P \in ℝ) \to y \in ℝ$
336	245	a1i	$⊢ P \in ℝ \to \frac{1}{2} \in ℝ$
337	331 336	resubcld	$⊢ P \in ℝ \to (\frac{P}{2}) - (\frac{1}{2}) \in ℝ$
338	337	adantl	$⊢ (y \in ℝ \land P \in ℝ) \to (\frac{P}{2}) - (\frac{1}{2}) \in ℝ$
339		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})$
340	335 338 332 339	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})$
341	334 340	mpan2d	$⊢ (y \in ℝ \land P \in ℝ) \to (y \leq (\frac{P}{2}) - (\frac{1}{2}) \to y \leq \frac{P}{2})$
342	80	adantl	$⊢ (y \in ℝ \land P \in ℝ) \to P \in ℂ$
343		1cnd	$⊢ (y \in ℝ \land P \in ℝ) \to 1 \in ℂ$
344	229	a1i	$⊢ (y \in ℝ \land P \in ℝ) \to (2 \in ℂ \land 2 \neq 0)$
345	342 343 344 231	syl3anc	$⊢ (y \in ℝ \land P \in ℝ) \to \frac{P - 1}{2} = (\frac{P}{2}) - (\frac{1}{2})$
346	345	breq2d	$⊢ (y \in ℝ \land P \in ℝ) \to (y \leq \frac{P - 1}{2} \leftrightarrow y \leq (\frac{P}{2}) - (\frac{1}{2}))$
347		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}))$
348	332 257 335 347	syl3anc	$⊢ (y \in ℝ \land P \in ℝ) \to (\frac{P}{2} \leq P - y \leftrightarrow y \leq P - (\frac{P}{2}))$
349	258 262	lenltd	$⊢ (y \in ℝ \land P \in ℝ) \to (\frac{P}{2} \leq P - y \leftrightarrow \neg P - y < \frac{P}{2})$
350		2cnd	$⊢ P \in ℝ \to 2 \in ℂ$
351	186	a1i	$⊢ P \in ℝ \to 2 \neq 0$
352	80 350 351	divcan1d	$⊢ P \in ℝ \to (\frac{P}{2}) \cdot 2 = P$
353	352	eqcomd	$⊢ P \in ℝ \to P = (\frac{P}{2}) \cdot 2$
354	353	oveq1d	$⊢ P \in ℝ \to P - (\frac{P}{2}) = (\frac{P}{2}) \cdot 2 - (\frac{P}{2})$
355	331	recnd	$⊢ P \in ℝ \to \frac{P}{2} \in ℂ$
356	355 350	mulcomd	$⊢ P \in ℝ \to (\frac{P}{2}) \cdot 2 = 2 (\frac{P}{2})$
357	356	oveq1d	$⊢ P \in ℝ \to (\frac{P}{2}) \cdot 2 - (\frac{P}{2}) = 2 (\frac{P}{2}) - (\frac{P}{2})$
358	350 355	mulsubfacd	$⊢ P \in ℝ \to 2 (\frac{P}{2}) - (\frac{P}{2}) = (2 - 1) (\frac{P}{2})$
359		2m1e1	$⊢ 2 - 1 = 1$
360	359	a1i	$⊢ P \in ℝ \to 2 - 1 = 1$
361	360	oveq1d	$⊢ P \in ℝ \to (2 - 1) (\frac{P}{2}) = 1 (\frac{P}{2})$
362	355	mullidd	$⊢ P \in ℝ \to 1 (\frac{P}{2}) = \frac{P}{2}$
363	358 361 362	3eqtrd	$⊢ P \in ℝ \to 2 (\frac{P}{2}) - (\frac{P}{2}) = \frac{P}{2}$
364	354 357 363	3eqtrd	$⊢ P \in ℝ \to P - (\frac{P}{2}) = \frac{P}{2}$
365	364	adantl	$⊢ (y \in ℝ \land P \in ℝ) \to P - (\frac{P}{2}) = \frac{P}{2}$
366	365	breq2d	$⊢ (y \in ℝ \land P \in ℝ) \to (y \leq P - (\frac{P}{2}) \leftrightarrow y \leq \frac{P}{2})$
367	348 349 366	3bitr3d	$⊢ (y \in ℝ \land P \in ℝ) \to (\neg P - y < \frac{P}{2} \leftrightarrow y \leq \frac{P}{2})$
368	341 346 367	3imtr4d	$⊢ (y \in ℝ \land P \in ℝ) \to (y \leq \frac{P - 1}{2} \to \neg P - y < \frac{P}{2})$
369	368	ex	$⊢ y \in ℝ \to (P \in ℝ \to (y \leq \frac{P - 1}{2} \to \neg P - y < \frac{P}{2}))$
370	155 369	syl	$⊢ y \in ℕ \to (P \in ℝ \to (y \leq \frac{P - 1}{2} \to \neg P - y < \frac{P}{2}))$
371	370	com3l	$⊢ P \in ℝ \to (y \leq \frac{P - 1}{2} \to (y \in ℕ \to \neg P - y < \frac{P}{2}))$
372	329 371	syl	$⊢ P \in ℤ \to (y \leq \frac{P - 1}{2} \to (y \in ℕ \to \neg P - y < \frac{P}{2}))$
373	54 55 372	3syl	$⊢ P \in (ℙ ∖ \{2\}) \to (y \leq \frac{P - 1}{2} \to (y \in ℕ \to \neg P - y < \frac{P}{2}))$
374	1 373	syl	$⊢ φ \to (y \leq \frac{P - 1}{2} \to (y \in ℕ \to \neg P - y < \frac{P}{2}))$
375	374	adantl	$⊢ (\neg 2 ∥ y \land φ) \to (y \leq \frac{P - 1}{2} \to (y \in ℕ \to \neg P - y < \frac{P}{2}))$
376	375	com13	$⊢ y \in ℕ \to (y \leq \frac{P - 1}{2} \to ((\neg 2 ∥ y \land φ) \to \neg P - y < \frac{P}{2}))$
377	189 376	biimtrid	$⊢ y \in ℕ \to (y \leq H \to ((\neg 2 ∥ y \land φ) \to \neg P - y < \frac{P}{2}))$
378	377	a1d	$⊢ y \in ℕ \to (H \in ℕ \to (y \leq H \to ((\neg 2 ∥ y \land φ) \to \neg P - y < \frac{P}{2})))$
379	378	3imp	$⊢ (y \in ℕ \land H \in ℕ \land y \leq H) \to ((\neg 2 ∥ y \land φ) \to \neg P - y < \frac{P}{2})$
380	379	com12	$⊢ (\neg 2 ∥ y \land φ) \to ((y \in ℕ \land H \in ℕ \land y \leq H) \to \neg P - y < \frac{P}{2})$
381	149 380	biimtrid	$⊢ (\neg 2 ∥ y \land φ) \to (y \in (1 \dots H) \to \neg P - y < \frac{P}{2})$
382	381	3impia	$⊢ (\neg 2 ∥ y \land φ \land y \in (1 \dots H)) \to \neg P - y < \frac{P}{2}$
383	328 382	eqnbrtrd	$⊢ (\neg 2 ∥ y \land φ \land y \in (1 \dots H)) \to \neg (\frac{P - y}{2}) \cdot 2 < \frac{P}{2}$
384	383	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$
385	328	oveq2d	$⊢ (\neg 2 ∥ y \land φ \land y \in (1 \dots H)) \to P - (\frac{P - y}{2}) \cdot 2 = P - (P - y)$
386	322 183	anim12i	$⊢ (φ \land y \in (1 \dots H)) \to (P \in ℂ \land y \in ℂ)$
387	386	3adant1	$⊢ (\neg 2 ∥ y \land φ \land y \in (1 \dots H)) \to (P \in ℂ \land y \in ℂ)$
388		nncan	$⊢ (P \in ℂ \land y \in ℂ) \to P - (P - y) = y$
389	387 388	syl	$⊢ (\neg 2 ∥ y \land φ \land y \in (1 \dots H)) \to P - (P - y) = y$
390	384 385 389	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)$
391	315 321 390	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)$
392	391	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)))$
393	210 392	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))$
394	148 393	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))$
395	5 394	bitrid	$⊢ φ \to (y \in ran R \leftrightarrow y \in (1 \dots H))$
396	395	eqrdv	$⊢ φ \to ran R = (1 \dots H)$

Metamath Proof Explorer

Theorem gausslemma2dlem1a

Proof