# Metamath Proof Explorer

## Theorem 2lgslem3d1

Description: Lemma 4 for 2lgslem3 . (Contributed by AV, 15-Jul-2021)

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

### Proof

Step Hyp Ref Expression
1 2lgslem2.n ${⊢}{N}=\left(\frac{{P}-1}{2}\right)-⌊\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 ${⊢}\left({P}\in {ℕ}_{0}\wedge 8\in {ℝ}^{+}\right)\to \left({P}\mathrm{mod}8=7\to \exists {k}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}{P}={k}\cdot 8+7\right)$
7 2 5 6 sylancl ${⊢}{P}\in ℕ\to \left({P}\mathrm{mod}8=7\to \exists {k}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}{P}={k}\cdot 8+7\right)$
8 simpr ${⊢}\left({P}\in ℕ\wedge {k}\in {ℕ}_{0}\right)\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 ${⊢}\left({P}\in ℕ\wedge {k}\in {ℕ}_{0}\right)\to {k}\cdot 8=8{k}$
14 13 oveq1d ${⊢}\left({P}\in ℕ\wedge {k}\in {ℕ}_{0}\right)\to {k}\cdot 8+7=8{k}+7$
15 14 eqeq2d ${⊢}\left({P}\in ℕ\wedge {k}\in {ℕ}_{0}\right)\to \left({P}={k}\cdot 8+7↔{P}=8{k}+7\right)$
16 15 biimpa ${⊢}\left(\left({P}\in ℕ\wedge {k}\in {ℕ}_{0}\right)\wedge {P}={k}\cdot 8+7\right)\to {P}=8{k}+7$
17 1 2lgslem3d ${⊢}\left({k}\in {ℕ}_{0}\wedge {P}=8{k}+7\right)\to {N}=2{k}+2$
18 8 16 17 syl2an2r ${⊢}\left(\left({P}\in ℕ\wedge {k}\in {ℕ}_{0}\right)\wedge {P}={k}\cdot 8+7\right)\to {N}=2{k}+2$
19 oveq1 ${⊢}{N}=2{k}+2\to {N}\mathrm{mod}2=\left(2{k}+2\right)\mathrm{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 ${⊢}\left(2\in ℂ\wedge {k}\in ℂ\wedge 1\in ℂ\right)\to 2\left({k}+1\right)=2{k}+2\cdot 1$
27 26 eqcomd ${⊢}\left(2\in ℂ\wedge {k}\in ℂ\wedge 1\in ℂ\right)\to 2{k}+2\cdot 1=2\left({k}+1\right)$
28 24 9 25 27 syl3anc ${⊢}{k}\in {ℕ}_{0}\to 2{k}+2\cdot 1=2\left({k}+1\right)$
29 9 25 addcld ${⊢}{k}\in {ℕ}_{0}\to {k}+1\in ℂ$
30 24 29 mulcomd ${⊢}{k}\in {ℕ}_{0}\to 2\left({k}+1\right)=\left({k}+1\right)\cdot 2$
31 23 28 30 3eqtrd ${⊢}{k}\in {ℕ}_{0}\to 2{k}+2=\left({k}+1\right)\cdot 2$
32 31 oveq1d ${⊢}{k}\in {ℕ}_{0}\to \left(2{k}+2\right)\mathrm{mod}2=\left({k}+1\right)\cdot 2\mathrm{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 ${⊢}\left({k}+1\in ℤ\wedge 2\in {ℝ}^{+}\right)\to \left({k}+1\right)\cdot 2\mathrm{mod}2=0$
37 34 35 36 sylancl ${⊢}{k}\in {ℕ}_{0}\to \left({k}+1\right)\cdot 2\mathrm{mod}2=0$
38 32 37 eqtrd ${⊢}{k}\in {ℕ}_{0}\to \left(2{k}+2\right)\mathrm{mod}2=0$
39 19 38 sylan9eqr ${⊢}\left({k}\in {ℕ}_{0}\wedge {N}=2{k}+2\right)\to {N}\mathrm{mod}2=0$
40 8 18 39 syl2an2r ${⊢}\left(\left({P}\in ℕ\wedge {k}\in {ℕ}_{0}\right)\wedge {P}={k}\cdot 8+7\right)\to {N}\mathrm{mod}2=0$
41 40 rexlimdva2 ${⊢}{P}\in ℕ\to \left(\exists {k}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}{P}={k}\cdot 8+7\to {N}\mathrm{mod}2=0\right)$
42 7 41 syld ${⊢}{P}\in ℕ\to \left({P}\mathrm{mod}8=7\to {N}\mathrm{mod}2=0\right)$
43 42 imp ${⊢}\left({P}\in ℕ\wedge {P}\mathrm{mod}8=7\right)\to {N}\mathrm{mod}2=0$