gausslemma2dlem2

	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))$
	gausslemma2d.m	$⊢ M = ⌊\frac{P}{4}⌋$
Assertion	gausslemma2dlem2	$⊢ φ \to \forall k \in (1 \dots M) R (k) = k \cdot 2$

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		gausslemma2d.m	$⊢ M = ⌊\frac{P}{4}⌋$
5		oveq1	$⊢ x = k \to x \cdot 2 = k \cdot 2$
6	5	breq1d	$⊢ x = k \to (x \cdot 2 < \frac{P}{2} \leftrightarrow k \cdot 2 < \frac{P}{2})$
7	5	oveq2d	$⊢ x = k \to P - x \cdot 2 = P - k \cdot 2$
8	6 5 7	ifbieq12d	$⊢ x = k \to if (x \cdot 2 < \frac{P}{2}, x \cdot 2, P - x \cdot 2) = if (k \cdot 2 < \frac{P}{2}, k \cdot 2, P - k \cdot 2)$
9	8	adantl	$⊢ ((φ \land k \in (1 \dots M)) \land x = k) \to if (x \cdot 2 < \frac{P}{2}, x \cdot 2, P - x \cdot 2) = if (k \cdot 2 < \frac{P}{2}, k \cdot 2, P - k \cdot 2)$
10		elfz1b	$⊢ k \in (1 \dots M) \leftrightarrow (k \in ℕ \land M \in ℕ \land k \leq M)$
11		nnre	$⊢ k \in ℕ \to k \in ℝ$
12	11	adantr	$⊢ (k \in ℕ \land M \in ℕ) \to k \in ℝ$
13		nnre	$⊢ M \in ℕ \to M \in ℝ$
14	13	adantl	$⊢ (k \in ℕ \land M \in ℕ) \to M \in ℝ$
15		2re	$⊢ 2 \in ℝ$
16		2pos	$⊢ 0 < 2$
17	15 16	pm3.2i	$⊢ (2 \in ℝ \land 0 < 2)$
18	17	a1i	$⊢ (k \in ℕ \land M \in ℕ) \to (2 \in ℝ \land 0 < 2)$
19		lemul1	$⊢ (k \in ℝ \land M \in ℝ \land (2 \in ℝ \land 0 < 2)) \to (k \leq M \leftrightarrow k \cdot 2 \leq M \cdot 2)$
20	12 14 18 19	syl3anc	$⊢ (k \in ℕ \land M \in ℕ) \to (k \leq M \leftrightarrow k \cdot 2 \leq M \cdot 2)$
21	1 4	gausslemma2dlem0e	$⊢ φ \to M \cdot 2 < \frac{P}{2}$
22	21	adantl	$⊢ ((k \in ℕ \land M \in ℕ) \land φ) \to M \cdot 2 < \frac{P}{2}$
23	15	a1i	$⊢ k \in ℕ \to 2 \in ℝ$
24	11 23	remulcld	$⊢ k \in ℕ \to k \cdot 2 \in ℝ$
25	24	adantr	$⊢ (k \in ℕ \land M \in ℕ) \to k \cdot 2 \in ℝ$
26	15	a1i	$⊢ M \in ℕ \to 2 \in ℝ$
27	13 26	remulcld	$⊢ M \in ℕ \to M \cdot 2 \in ℝ$
28	27	adantl	$⊢ (k \in ℕ \land M \in ℕ) \to M \cdot 2 \in ℝ$
29	1	gausslemma2dlem0a	$⊢ φ \to P \in ℕ$
30	29	nnred	$⊢ φ \to P \in ℝ$
31	30	rehalfcld	$⊢ φ \to \frac{P}{2} \in ℝ$
32		lelttr	$⊢ (k \cdot 2 \in ℝ \land M \cdot 2 \in ℝ \land \frac{P}{2} \in ℝ) \to ((k \cdot 2 \leq M \cdot 2 \land M \cdot 2 < \frac{P}{2}) \to k \cdot 2 < \frac{P}{2})$
33	25 28 31 32	syl2an3an	$⊢ ((k \in ℕ \land M \in ℕ) \land φ) \to ((k \cdot 2 \leq M \cdot 2 \land M \cdot 2 < \frac{P}{2}) \to k \cdot 2 < \frac{P}{2})$
34	22 33	mpan2d	$⊢ ((k \in ℕ \land M \in ℕ) \land φ) \to (k \cdot 2 \leq M \cdot 2 \to k \cdot 2 < \frac{P}{2})$
35	34	ex	$⊢ (k \in ℕ \land M \in ℕ) \to (φ \to (k \cdot 2 \leq M \cdot 2 \to k \cdot 2 < \frac{P}{2}))$
36	35	com23	$⊢ (k \in ℕ \land M \in ℕ) \to (k \cdot 2 \leq M \cdot 2 \to (φ \to k \cdot 2 < \frac{P}{2}))$
37	20 36	sylbid	$⊢ (k \in ℕ \land M \in ℕ) \to (k \leq M \to (φ \to k \cdot 2 < \frac{P}{2}))$
38	37	3impia	$⊢ (k \in ℕ \land M \in ℕ \land k \leq M) \to (φ \to k \cdot 2 < \frac{P}{2})$
39	10 38	sylbi	$⊢ k \in (1 \dots M) \to (φ \to k \cdot 2 < \frac{P}{2})$
40	39	impcom	$⊢ (φ \land k \in (1 \dots M)) \to k \cdot 2 < \frac{P}{2}$
41	40	adantr	$⊢ ((φ \land k \in (1 \dots M)) \land x = k) \to k \cdot 2 < \frac{P}{2}$
42	41	iftrued	$⊢ ((φ \land k \in (1 \dots M)) \land x = k) \to if (k \cdot 2 < \frac{P}{2}, k \cdot 2, P - k \cdot 2) = k \cdot 2$
43	9 42	eqtrd	$⊢ ((φ \land k \in (1 \dots M)) \land x = k) \to if (x \cdot 2 < \frac{P}{2}, x \cdot 2, P - x \cdot 2) = k \cdot 2$
44	1 4	gausslemma2dlem0d	$⊢ φ \to M \in ℕ_{0}$
45	44	nn0zd	$⊢ φ \to M \in ℤ$
46	1 2	gausslemma2dlem0b	$⊢ φ \to H \in ℕ$
47	46	nnzd	$⊢ φ \to H \in ℤ$
48	1 4 2	gausslemma2dlem0g	$⊢ φ \to M \leq H$
49		eluz2	$⊢ H \in ℤ_{\geq M} \leftrightarrow (M \in ℤ \land H \in ℤ \land M \leq H)$
50	45 47 48 49	syl3anbrc	$⊢ φ \to H \in ℤ_{\geq M}$
51		fzss2	$⊢ H \in ℤ_{\geq M} \to (1 \dots M) \subseteq (1 \dots H)$
52	50 51	syl	$⊢ φ \to (1 \dots M) \subseteq (1 \dots H)$
53	52	sselda	$⊢ (φ \land k \in (1 \dots M)) \to k \in (1 \dots H)$
54		ovexd	$⊢ (φ \land k \in (1 \dots M)) \to k \cdot 2 \in V$
55	3 43 53 54	fvmptd2	$⊢ (φ \land k \in (1 \dots M)) \to R (k) = k \cdot 2$
56	55	ralrimiva	$⊢ φ \to \forall k \in (1 \dots M) R (k) = k \cdot 2$

Metamath Proof Explorer

Theorem gausslemma2dlem2

Proof