Metamath Proof Explorer

Theorem 2lgslem3d1

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

Ref Expression
Hypothesis 2lgslem2.n ⊢N=P−12−P4
Assertion 2lgslem3d1 ⊢P∈ℕ∧Pmod8=7→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=7→∃k∈ℕ0P=k⋅8+7
7 2 5 6 sylancl ⊢P∈ℕ→Pmod8=7→∃k∈ℕ0P=k⋅8+7
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+7=8⁢k+7
15 14 eqeq2d ⊢P∈ℕ∧k∈ℕ0→P=k⋅8+7↔P=8⁢k+7
16 15 biimpa ⊢P∈ℕ∧k∈ℕ0∧P=k⋅8+7→P=8⁢k+7
17 1 2lgslem3d ⊢k∈ℕ0∧P=8⁢k+7→N=2⁢k+2
18 8 16 17 syl2an2r ⊢P∈ℕ∧k∈ℕ0∧P=k⋅8+7→N=2⁢k+2
19 oveq1 ⊢N=2⁢k+2→Nmod2=2⁢k+2mod2
20 2t1e2 ⊢2⋅1=2
21 20 eqcomi ⊢2=2⋅1
22 21 a1i ⊢k∈ℕ0→2=2⋅1
23 22 oveq2d ⊢k∈ℕ0→2⁢k+2=2⁢k+2⋅1
24 2cnd ⊢k∈ℕ0→2∈ℂ
25 1cnd ⊢k∈ℕ0→1∈ℂ
26 adddi ⊢2∈ℂ∧k∈ℂ∧1∈ℂ→2⁢k+1=2⁢k+2⋅1
27 26 eqcomd ⊢2∈ℂ∧k∈ℂ∧1∈ℂ→2⁢k+2⋅1=2⁢k+1
28 24 9 25 27 syl3anc ⊢k∈ℕ0→2⁢k+2⋅1=2⁢k+1
29 9 25 addcld ⊢k∈ℕ0→k+1∈ℂ
30 24 29 mulcomd ⊢k∈ℕ0→2⁢k+1=k+1⋅2
31 23 28 30 3eqtrd ⊢k∈ℕ0→2⁢k+2=k+1⋅2
32 31 oveq1d ⊢k∈ℕ0→2⁢k+2mod2=k+1⋅2mod2
33 peano2nn0 ⊢k∈ℕ0→k+1∈ℕ0
34 33 nn0zd ⊢k∈ℕ0→k+1∈ℤ
35 2rp ⊢2∈ℝ+
36 mulmod0 ⊢k+1∈ℤ∧2∈ℝ+→k+1⋅2mod2=0
37 34 35 36 sylancl ⊢k∈ℕ0→k+1⋅2mod2=0
38 32 37 eqtrd ⊢k∈ℕ0→2⁢k+2mod2=0
39 19 38 sylan9eqr ⊢k∈ℕ0∧N=2⁢k+2→Nmod2=0
40 8 18 39 syl2an2r ⊢P∈ℕ∧k∈ℕ0∧P=k⋅8+7→Nmod2=0
41 40 rexlimdva2 ⊢P∈ℕ→∃k∈ℕ0P=k⋅8+7→Nmod2=0
42 7 41 syld ⊢P∈ℕ→Pmod8=7→Nmod2=0
43 42 imp ⊢P∈ℕ∧Pmod8=7→Nmod2=0