# Metamath Proof Explorer

## Theorem 2lgslem3a1

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

Ref Expression
Hypothesis 2lgslem2.n ${⊢}{N}=\left(\frac{{P}-1}{2}\right)-⌊\frac{{P}}{4}⌋$
Assertion 2lgslem3a1 ${⊢}\left({P}\in ℕ\wedge {P}\mathrm{mod}8=1\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=1\to \exists {k}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}{P}={k}\cdot 8+1\right)$
7 2 5 6 sylancl ${⊢}{P}\in ℕ\to \left({P}\mathrm{mod}8=1\to \exists {k}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}{P}={k}\cdot 8+1\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+1=8{k}+1$
15 14 eqeq2d ${⊢}\left({P}\in ℕ\wedge {k}\in {ℕ}_{0}\right)\to \left({P}={k}\cdot 8+1↔{P}=8{k}+1\right)$
16 15 biimpa ${⊢}\left(\left({P}\in ℕ\wedge {k}\in {ℕ}_{0}\right)\wedge {P}={k}\cdot 8+1\right)\to {P}=8{k}+1$
17 1 2lgslem3a ${⊢}\left({k}\in {ℕ}_{0}\wedge {P}=8{k}+1\right)\to {N}=2{k}$
18 8 16 17 syl2an2r ${⊢}\left(\left({P}\in ℕ\wedge {k}\in {ℕ}_{0}\right)\wedge {P}={k}\cdot 8+1\right)\to {N}=2{k}$
19 oveq1 ${⊢}{N}=2{k}\to {N}\mathrm{mod}2=2{k}\mathrm{mod}2$
20 2cnd ${⊢}{k}\in {ℕ}_{0}\to 2\in ℂ$
21 20 9 mulcomd ${⊢}{k}\in {ℕ}_{0}\to 2{k}={k}\cdot 2$
22 21 oveq1d ${⊢}{k}\in {ℕ}_{0}\to 2{k}\mathrm{mod}2={k}\cdot 2\mathrm{mod}2$
23 nn0z ${⊢}{k}\in {ℕ}_{0}\to {k}\in ℤ$
24 2rp ${⊢}2\in {ℝ}^{+}$
25 mulmod0 ${⊢}\left({k}\in ℤ\wedge 2\in {ℝ}^{+}\right)\to {k}\cdot 2\mathrm{mod}2=0$
26 23 24 25 sylancl ${⊢}{k}\in {ℕ}_{0}\to {k}\cdot 2\mathrm{mod}2=0$
27 22 26 eqtrd ${⊢}{k}\in {ℕ}_{0}\to 2{k}\mathrm{mod}2=0$
28 19 27 sylan9eqr ${⊢}\left({k}\in {ℕ}_{0}\wedge {N}=2{k}\right)\to {N}\mathrm{mod}2=0$
29 8 18 28 syl2an2r ${⊢}\left(\left({P}\in ℕ\wedge {k}\in {ℕ}_{0}\right)\wedge {P}={k}\cdot 8+1\right)\to {N}\mathrm{mod}2=0$
30 29 rexlimdva2 ${⊢}{P}\in ℕ\to \left(\exists {k}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}{P}={k}\cdot 8+1\to {N}\mathrm{mod}2=0\right)$
31 7 30 syld ${⊢}{P}\in ℕ\to \left({P}\mathrm{mod}8=1\to {N}\mathrm{mod}2=0\right)$
32 31 imp ${⊢}\left({P}\in ℕ\wedge {P}\mathrm{mod}8=1\right)\to {N}\mathrm{mod}2=0$