2lgslem3d1

		Ref	Expression
	Hypothesis	2lgslem2.n	$⊢ N = (\frac{P - 1}{2}) - ⌊\frac{P}{4}⌋$
	Assertion	2lgslem3d1	$⊢ (P \in ℕ \land P \mod 8 = 7) \to N \mod 2 = 0$

Proof

Step	Hyp	Ref	Expression
1		2lgslem2.n	$⊢ N = (\frac{P - 1}{2}) - ⌊\frac{P}{4}⌋$
2		nnnn0	$⊢ P \in ℕ \to P \in ℕ_{0}$
3		8nn	$⊢ 8 \in ℕ$
4		nnrp	$⊢ 8 \in ℕ \to 8 \in ℝ^{+}$
5	3 4	ax-mp	$⊢ 8 \in ℝ^{+}$
6		modmuladdnn0	$⊢ (P \in ℕ_{0} \land 8 \in ℝ^{+}) \to (P \mod 8 = 7 \to \exists k \in ℕ_{0} P = k \cdot 8 + 7)$
7	2 5 6	sylancl	$⊢ P \in ℕ \to (P \mod 8 = 7 \to \exists k \in ℕ_{0} P = k \cdot 8 + 7)$
8		simpr	$⊢ (P \in ℕ \land k \in ℕ_{0}) \to k \in ℕ_{0}$
9		nn0cn	$⊢ k \in ℕ_{0} \to k \in ℂ$
10		8cn	$⊢ 8 \in ℂ$
11	10	a1i	$⊢ k \in ℕ_{0} \to 8 \in ℂ$
12	9 11	mulcomd	$⊢ k \in ℕ_{0} \to k \cdot 8 = 8 k$
13	12	adantl	$⊢ (P \in ℕ \land k \in ℕ_{0}) \to k \cdot 8 = 8 k$
14	13	oveq1d	$⊢ (P \in ℕ \land k \in ℕ_{0}) \to k \cdot 8 + 7 = 8 k + 7$
15	14	eqeq2d	$⊢ (P \in ℕ \land k \in ℕ_{0}) \to (P = k \cdot 8 + 7 \leftrightarrow P = 8 k + 7)$
16	15	biimpa	$⊢ ((P \in ℕ \land k \in ℕ_{0}) \land P = k \cdot 8 + 7) \to P = 8 k + 7$
17	1	2lgslem3d	$⊢ (k \in ℕ_{0} \land P = 8 k + 7) \to N = 2 k + 2$
18	8 16 17	syl2an2r	$⊢ ((P \in ℕ \land k \in ℕ_{0}) \land P = k \cdot 8 + 7) \to N = 2 k + 2$
19		oveq1	$⊢ N = 2 k + 2 \to N \mod 2 = (2 k + 2) \mod 2$
20		2t1e2	$⊢ 2 \cdot 1 = 2$
21	20	eqcomi	$⊢ 2 = 2 \cdot 1$
22	21	a1i	$⊢ k \in ℕ_{0} \to 2 = 2 \cdot 1$
23	22	oveq2d	$⊢ k \in ℕ_{0} \to 2 k + 2 = 2 k + 2 \cdot 1$
24		2cnd	$⊢ k \in ℕ_{0} \to 2 \in ℂ$
25		1cnd	$⊢ k \in ℕ_{0} \to 1 \in ℂ$
26		adddi	$⊢ (2 \in ℂ \land k \in ℂ \land 1 \in ℂ) \to 2 (k + 1) = 2 k + 2 \cdot 1$
27	26	eqcomd	$⊢ (2 \in ℂ \land k \in ℂ \land 1 \in ℂ) \to 2 k + 2 \cdot 1 = 2 (k + 1)$
28	24 9 25 27	syl3anc	$⊢ k \in ℕ_{0} \to 2 k + 2 \cdot 1 = 2 (k + 1)$
29	9 25	addcld	$⊢ k \in ℕ_{0} \to k + 1 \in ℂ$
30	24 29	mulcomd	$⊢ k \in ℕ_{0} \to 2 (k + 1) = (k + 1) \cdot 2$
31	23 28 30	3eqtrd	$⊢ k \in ℕ_{0} \to 2 k + 2 = (k + 1) \cdot 2$
32	31	oveq1d	$⊢ k \in ℕ_{0} \to (2 k + 2) \mod 2 = (k + 1) \cdot 2 \mod 2$
33		peano2nn0	$⊢ k \in ℕ_{0} \to k + 1 \in ℕ_{0}$
34	33	nn0zd	$⊢ k \in ℕ_{0} \to k + 1 \in ℤ$
35		2rp	$⊢ 2 \in ℝ^{+}$
36		mulmod0	$⊢ (k + 1 \in ℤ \land 2 \in ℝ^{+}) \to (k + 1) \cdot 2 \mod 2 = 0$
37	34 35 36	sylancl	$⊢ k \in ℕ_{0} \to (k + 1) \cdot 2 \mod 2 = 0$
38	32 37	eqtrd	$⊢ k \in ℕ_{0} \to (2 k + 2) \mod 2 = 0$
39	19 38	sylan9eqr	$⊢ (k \in ℕ_{0} \land N = 2 k + 2) \to N \mod 2 = 0$
40	8 18 39	syl2an2r	$⊢ ((P \in ℕ \land k \in ℕ_{0}) \land P = k \cdot 8 + 7) \to N \mod 2 = 0$
41	40	rexlimdva2	$⊢ P \in ℕ \to (\exists k \in ℕ_{0} P = k \cdot 8 + 7 \to N \mod 2 = 0)$
42	7 41	syld	$⊢ P \in ℕ \to (P \mod 8 = 7 \to N \mod 2 = 0)$
43	42	imp	$⊢ (P \in ℕ \land P \mod 8 = 7) \to N \mod 2 = 0$

Metamath Proof Explorer

Theorem 2lgslem3d1

Proof