Metamath Proof Explorer

Theorem 2lgslem3a1

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

Ref Expression
Hypothesis 2lgslem2.n ⊢N=P−12−P4
Assertion 2lgslem3a1 ⊢P∈ℕ∧Pmod8=1→Nmod2=0

Proof

Step Hyp Ref Expression
1 2lgslem2.n ⊢N=P−12−P4
2 nnnn0 ⊢P∈ℕ→P∈ℕ0
3 8nn ⊢8∈ℕ
4 nnrp ⊢8∈ℕ→8∈ℝ+
5 3 4 ax-mp ⊢8∈ℝ+
6 modmuladdnn0 ⊢P∈ℕ0∧8∈ℝ+→Pmod8=1→∃k∈ℕ0P=k⋅8+1
7 2 5 6 sylancl ⊢P∈ℕ→Pmod8=1→∃k∈ℕ0P=k⋅8+1
8 simpr ⊢P∈ℕ∧k∈ℕ0→k∈ℕ0
9 nn0cn ⊢k∈ℕ0→k∈ℂ
10 8cn ⊢8∈ℂ
11 10 a1i ⊢k∈ℕ0→8∈ℂ
12 9 11 mulcomd ⊢k∈ℕ0→k⋅8=8⁢k
13 12 adantl ⊢P∈ℕ∧k∈ℕ0→k⋅8=8⁢k
14 13 oveq1d ⊢P∈ℕ∧k∈ℕ0→k⋅8+1=8⁢k+1
15 14 eqeq2d ⊢P∈ℕ∧k∈ℕ0→P=k⋅8+1↔P=8⁢k+1
16 15 biimpa ⊢P∈ℕ∧k∈ℕ0∧P=k⋅8+1→P=8⁢k+1
17 1 2lgslem3a ⊢k∈ℕ0∧P=8⁢k+1→N=2⁢k
18 8 16 17 syl2an2r ⊢P∈ℕ∧k∈ℕ0∧P=k⋅8+1→N=2⁢k
19 oveq1 ⊢N=2⁢k→Nmod2=2⁢kmod2
20 2cnd ⊢k∈ℕ0→2∈ℂ
21 20 9 mulcomd ⊢k∈ℕ0→2⁢k=k⋅2
22 21 oveq1d ⊢k∈ℕ0→2⁢kmod2=k⋅2mod2
23 nn0z ⊢k∈ℕ0→k∈ℤ
24 2rp ⊢2∈ℝ+
25 mulmod0 ⊢k∈ℤ∧2∈ℝ+→k⋅2mod2=0
26 23 24 25 sylancl ⊢k∈ℕ0→k⋅2mod2=0
27 22 26 eqtrd ⊢k∈ℕ0→2⁢kmod2=0
28 19 27 sylan9eqr ⊢k∈ℕ0∧N=2⁢k→Nmod2=0
29 8 18 28 syl2an2r ⊢P∈ℕ∧k∈ℕ0∧P=k⋅8+1→Nmod2=0
30 29 rexlimdva2 ⊢P∈ℕ→∃k∈ℕ0P=k⋅8+1→Nmod2=0
31 7 30 syld ⊢P∈ℕ→Pmod8=1→Nmod2=0
32 31 imp ⊢P∈ℕ∧Pmod8=1→Nmod2=0