gausslemma2dlem3

	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	gausslemma2dlem3	$⊢ φ \to \forall k \in (M + 1 \dots H) R (k) = P - 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 (M + 1 \dots H)) \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	1	gausslemma2dlem0a	$⊢ φ \to P \in ℕ$
11		elfz2	$⊢ k \in (M + 1 \dots H) \leftrightarrow ((M + 1 \in ℤ \land H \in ℤ \land k \in ℤ) \land (M + 1 \leq k \land k \leq H))$
12	4	oveq1i	$⊢ M + 1 = ⌊\frac{P}{4}⌋ + 1$
13	12	breq1i	$⊢ M + 1 \leq k \leftrightarrow ⌊\frac{P}{4}⌋ + 1 \leq k$
14		nnre	$⊢ P \in ℕ \to P \in ℝ$
15		4re	$⊢ 4 \in ℝ$
16	15	a1i	$⊢ P \in ℕ \to 4 \in ℝ$
17		4ne0	$⊢ 4 \neq 0$
18	17	a1i	$⊢ P \in ℕ \to 4 \neq 0$
19	14 16 18	redivcld	$⊢ P \in ℕ \to \frac{P}{4} \in ℝ$
20	19	adantl	$⊢ (k \in ℤ \land P \in ℕ) \to \frac{P}{4} \in ℝ$
21		fllelt	$⊢ \frac{P}{4} \in ℝ \to (⌊\frac{P}{4}⌋ \leq \frac{P}{4} \land \frac{P}{4} < ⌊\frac{P}{4}⌋ + 1)$
22	20 21	syl	$⊢ (k \in ℤ \land P \in ℕ) \to (⌊\frac{P}{4}⌋ \leq \frac{P}{4} \land \frac{P}{4} < ⌊\frac{P}{4}⌋ + 1)$
23	19	flcld	$⊢ P \in ℕ \to ⌊\frac{P}{4}⌋ \in ℤ$
24	23	zred	$⊢ P \in ℕ \to ⌊\frac{P}{4}⌋ \in ℝ$
25		peano2re	$⊢ ⌊\frac{P}{4}⌋ \in ℝ \to ⌊\frac{P}{4}⌋ + 1 \in ℝ$
26	24 25	syl	$⊢ P \in ℕ \to ⌊\frac{P}{4}⌋ + 1 \in ℝ$
27	26	adantl	$⊢ (k \in ℤ \land P \in ℕ) \to ⌊\frac{P}{4}⌋ + 1 \in ℝ$
28		zre	$⊢ k \in ℤ \to k \in ℝ$
29	28	adantr	$⊢ (k \in ℤ \land P \in ℕ) \to k \in ℝ$
30		ltleletr	$⊢ (\frac{P}{4} \in ℝ \land ⌊\frac{P}{4}⌋ + 1 \in ℝ \land k \in ℝ) \to ((\frac{P}{4} < ⌊\frac{P}{4}⌋ + 1 \land ⌊\frac{P}{4}⌋ + 1 \leq k) \to \frac{P}{4} \leq k)$
31	20 27 29 30	syl3anc	$⊢ (k \in ℤ \land P \in ℕ) \to ((\frac{P}{4} < ⌊\frac{P}{4}⌋ + 1 \land ⌊\frac{P}{4}⌋ + 1 \leq k) \to \frac{P}{4} \leq k)$
32	31	expd	$⊢ (k \in ℤ \land P \in ℕ) \to (\frac{P}{4} < ⌊\frac{P}{4}⌋ + 1 \to (⌊\frac{P}{4}⌋ + 1 \leq k \to \frac{P}{4} \leq k))$
33	32	adantld	$⊢ (k \in ℤ \land P \in ℕ) \to ((⌊\frac{P}{4}⌋ \leq \frac{P}{4} \land \frac{P}{4} < ⌊\frac{P}{4}⌋ + 1) \to (⌊\frac{P}{4}⌋ + 1 \leq k \to \frac{P}{4} \leq k))$
34	22 33	mpd	$⊢ (k \in ℤ \land P \in ℕ) \to (⌊\frac{P}{4}⌋ + 1 \leq k \to \frac{P}{4} \leq k)$
35	34	imp	$⊢ ((k \in ℤ \land P \in ℕ) \land ⌊\frac{P}{4}⌋ + 1 \leq k) \to \frac{P}{4} \leq k$
36	14	rehalfcld	$⊢ P \in ℕ \to \frac{P}{2} \in ℝ$
37	36	adantl	$⊢ (k \in ℤ \land P \in ℕ) \to \frac{P}{2} \in ℝ$
38		2re	$⊢ 2 \in ℝ$
39	38	a1i	$⊢ k \in ℤ \to 2 \in ℝ$
40	28 39	remulcld	$⊢ k \in ℤ \to k \cdot 2 \in ℝ$
41	40	adantr	$⊢ (k \in ℤ \land P \in ℕ) \to k \cdot 2 \in ℝ$
42		2pos	$⊢ 0 < 2$
43	38 42	pm3.2i	$⊢ (2 \in ℝ \land 0 < 2)$
44	43	a1i	$⊢ (k \in ℤ \land P \in ℕ) \to (2 \in ℝ \land 0 < 2)$
45		lediv1	$⊢ (\frac{P}{2} \in ℝ \land k \cdot 2 \in ℝ \land (2 \in ℝ \land 0 < 2)) \to (\frac{P}{2} \leq k \cdot 2 \leftrightarrow \frac{\frac{P}{2}}{2} \leq \frac{k \cdot 2}{2})$
46	37 41 44 45	syl3anc	$⊢ (k \in ℤ \land P \in ℕ) \to (\frac{P}{2} \leq k \cdot 2 \leftrightarrow \frac{\frac{P}{2}}{2} \leq \frac{k \cdot 2}{2})$
47		nncn	$⊢ P \in ℕ \to P \in ℂ$
48		2cnne0	$⊢ (2 \in ℂ \land 2 \neq 0)$
49	48	a1i	$⊢ P \in ℕ \to (2 \in ℂ \land 2 \neq 0)$
50		divdiv1	$⊢ (P \in ℂ \land (2 \in ℂ \land 2 \neq 0) \land (2 \in ℂ \land 2 \neq 0)) \to \frac{\frac{P}{2}}{2} = \frac{P}{2 \cdot 2}$
51	47 49 49 50	syl3anc	$⊢ P \in ℕ \to \frac{\frac{P}{2}}{2} = \frac{P}{2 \cdot 2}$
52		2t2e4	$⊢ 2 \cdot 2 = 4$
53	52	oveq2i	$⊢ \frac{P}{2 \cdot 2} = \frac{P}{4}$
54	51 53	eqtrdi	$⊢ P \in ℕ \to \frac{\frac{P}{2}}{2} = \frac{P}{4}$
55		zcn	$⊢ k \in ℤ \to k \in ℂ$
56		2cnd	$⊢ k \in ℤ \to 2 \in ℂ$
57		2ne0	$⊢ 2 \neq 0$
58	57	a1i	$⊢ k \in ℤ \to 2 \neq 0$
59	55 56 58	divcan4d	$⊢ k \in ℤ \to \frac{k \cdot 2}{2} = k$
60	54 59	breqan12rd	$⊢ (k \in ℤ \land P \in ℕ) \to (\frac{\frac{P}{2}}{2} \leq \frac{k \cdot 2}{2} \leftrightarrow \frac{P}{4} \leq k)$
61	46 60	bitrd	$⊢ (k \in ℤ \land P \in ℕ) \to (\frac{P}{2} \leq k \cdot 2 \leftrightarrow \frac{P}{4} \leq k)$
62	61	adantr	$⊢ ((k \in ℤ \land P \in ℕ) \land ⌊\frac{P}{4}⌋ + 1 \leq k) \to (\frac{P}{2} \leq k \cdot 2 \leftrightarrow \frac{P}{4} \leq k)$
63	35 62	mpbird	$⊢ ((k \in ℤ \land P \in ℕ) \land ⌊\frac{P}{4}⌋ + 1 \leq k) \to \frac{P}{2} \leq k \cdot 2$
64	63	exp31	$⊢ k \in ℤ \to (P \in ℕ \to (⌊\frac{P}{4}⌋ + 1 \leq k \to \frac{P}{2} \leq k \cdot 2))$
65	64	com23	$⊢ k \in ℤ \to (⌊\frac{P}{4}⌋ + 1 \leq k \to (P \in ℕ \to \frac{P}{2} \leq k \cdot 2))$
66	13 65	biimtrid	$⊢ k \in ℤ \to (M + 1 \leq k \to (P \in ℕ \to \frac{P}{2} \leq k \cdot 2))$
67	66	3ad2ant3	$⊢ (M + 1 \in ℤ \land H \in ℤ \land k \in ℤ) \to (M + 1 \leq k \to (P \in ℕ \to \frac{P}{2} \leq k \cdot 2))$
68	67	com12	$⊢ M + 1 \leq k \to ((M + 1 \in ℤ \land H \in ℤ \land k \in ℤ) \to (P \in ℕ \to \frac{P}{2} \leq k \cdot 2))$
69	68	adantr	$⊢ (M + 1 \leq k \land k \leq H) \to ((M + 1 \in ℤ \land H \in ℤ \land k \in ℤ) \to (P \in ℕ \to \frac{P}{2} \leq k \cdot 2))$
70	69	impcom	$⊢ ((M + 1 \in ℤ \land H \in ℤ \land k \in ℤ) \land (M + 1 \leq k \land k \leq H)) \to (P \in ℕ \to \frac{P}{2} \leq k \cdot 2)$
71	11 70	sylbi	$⊢ k \in (M + 1 \dots H) \to (P \in ℕ \to \frac{P}{2} \leq k \cdot 2)$
72	71	impcom	$⊢ (P \in ℕ \land k \in (M + 1 \dots H)) \to \frac{P}{2} \leq k \cdot 2$
73		elfzelz	$⊢ k \in (M + 1 \dots H) \to k \in ℤ$
74	73	zred	$⊢ k \in (M + 1 \dots H) \to k \in ℝ$
75	38	a1i	$⊢ k \in (M + 1 \dots H) \to 2 \in ℝ$
76	74 75	remulcld	$⊢ k \in (M + 1 \dots H) \to k \cdot 2 \in ℝ$
77		lenlt	$⊢ (\frac{P}{2} \in ℝ \land k \cdot 2 \in ℝ) \to (\frac{P}{2} \leq k \cdot 2 \leftrightarrow \neg k \cdot 2 < \frac{P}{2})$
78	36 76 77	syl2an	$⊢ (P \in ℕ \land k \in (M + 1 \dots H)) \to (\frac{P}{2} \leq k \cdot 2 \leftrightarrow \neg k \cdot 2 < \frac{P}{2})$
79	72 78	mpbid	$⊢ (P \in ℕ \land k \in (M + 1 \dots H)) \to \neg k \cdot 2 < \frac{P}{2}$
80	10 79	sylan	$⊢ (φ \land k \in (M + 1 \dots H)) \to \neg k \cdot 2 < \frac{P}{2}$
81	80	adantr	$⊢ ((φ \land k \in (M + 1 \dots H)) \land x = k) \to \neg k \cdot 2 < \frac{P}{2}$
82	81	iffalsed	$⊢ ((φ \land k \in (M + 1 \dots H)) \land x = k) \to if (k \cdot 2 < \frac{P}{2}, k \cdot 2, P - k \cdot 2) = P - k \cdot 2$
83	9 82	eqtrd	$⊢ ((φ \land k \in (M + 1 \dots H)) \land x = k) \to if (x \cdot 2 < \frac{P}{2}, x \cdot 2, P - x \cdot 2) = P - k \cdot 2$
84	1 4	gausslemma2dlem0d	$⊢ φ \to M \in ℕ_{0}$
85		nn0p1nn	$⊢ M \in ℕ_{0} \to M + 1 \in ℕ$
86		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
87	85 86	eleqtrdi	$⊢ M \in ℕ_{0} \to M + 1 \in ℤ_{\geq 1}$
88	84 87	syl	$⊢ φ \to M + 1 \in ℤ_{\geq 1}$
89		fzss1	$⊢ M + 1 \in ℤ_{\geq 1} \to (M + 1 \dots H) \subseteq (1 \dots H)$
90	88 89	syl	$⊢ φ \to (M + 1 \dots H) \subseteq (1 \dots H)$
91	90	sselda	$⊢ (φ \land k \in (M + 1 \dots H)) \to k \in (1 \dots H)$
92		ovexd	$⊢ (φ \land k \in (M + 1 \dots H)) \to P - k \cdot 2 \in V$
93	3 83 91 92	fvmptd2	$⊢ (φ \land k \in (M + 1 \dots H)) \to R (k) = P - k \cdot 2$
94	93	ralrimiva	$⊢ φ \to \forall k \in (M + 1 \dots H) R (k) = P - k \cdot 2$

Metamath Proof Explorer

Theorem gausslemma2dlem3

Proof