Metamath Proof Explorer

Theorem 2lgslem3b1

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

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

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=3→∃k∈ℕ0P=k⋅8+3
7 2 5 6 sylancl ⊢P∈ℕ→Pmod8=3→∃k∈ℕ0P=k⋅8+3
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+3=8⁢k+3
15 14 eqeq2d ⊢P∈ℕ∧k∈ℕ0→P=k⋅8+3↔P=8⁢k+3
16 15 biimpa ⊢P∈ℕ∧k∈ℕ0∧P=k⋅8+3→P=8⁢k+3
17 1 2lgslem3b ⊢k∈ℕ0∧P=8⁢k+3→N=2⁢k+1
18 8 16 17 syl2an2r ⊢P∈ℕ∧k∈ℕ0∧P=k⋅8+3→N=2⁢k+1
19 oveq1 ⊢N=2⁢k+1→Nmod2=2⁢k+1mod2
20 nn0z ⊢k∈ℕ0→k∈ℤ
21 eqidd ⊢k∈ℕ0→2⁢k+1=2⁢k+1
22 2tp1odd ⊢k∈ℤ∧2⁢k+1=2⁢k+1→¬2∥2⁢k+1
23 20 21 22 syl2anc ⊢k∈ℕ0→¬2∥2⁢k+1
24 2z ⊢2∈ℤ
25 24 a1i ⊢k∈ℕ0→2∈ℤ
26 25 20 zmulcld ⊢k∈ℕ0→2⁢k∈ℤ
27 26 peano2zd ⊢k∈ℕ0→2⁢k+1∈ℤ
28 mod2eq1n2dvds ⊢2⁢k+1∈ℤ→2⁢k+1mod2=1↔¬2∥2⁢k+1
29 27 28 syl ⊢k∈ℕ0→2⁢k+1mod2=1↔¬2∥2⁢k+1
30 23 29 mpbird ⊢k∈ℕ0→2⁢k+1mod2=1
31 19 30 sylan9eqr ⊢k∈ℕ0∧N=2⁢k+1→Nmod2=1
32 8 18 31 syl2an2r ⊢P∈ℕ∧k∈ℕ0∧P=k⋅8+3→Nmod2=1
33 32 rexlimdva2 ⊢P∈ℕ→∃k∈ℕ0P=k⋅8+3→Nmod2=1
34 7 33 syld ⊢P∈ℕ→Pmod8=3→Nmod2=1
35 34 imp ⊢P∈ℕ∧Pmod8=3→Nmod2=1