# Metamath Proof Explorer

## Theorem 2lgslem3c1

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

Ref Expression
Hypothesis 2lgslem2.n $⊢ N = P − 1 2 − P 4$
Assertion 2lgslem3c1 $⊢ P ∈ ℕ ∧ P mod 8 = 5 → N mod 2 = 1$

### Proof

Step Hyp Ref Expression
1 2lgslem2.n $⊢ N = P − 1 2 − P 4$
2 nnnn0 $⊢ P ∈ ℕ → P ∈ ℕ 0$
3 8nn $⊢ 8 ∈ ℕ$
4 nnrp $⊢ 8 ∈ ℕ → 8 ∈ ℝ +$
5 3 4 ax-mp $⊢ 8 ∈ ℝ +$
6 modmuladdnn0 $⊢ P ∈ ℕ 0 ∧ 8 ∈ ℝ + → P mod 8 = 5 → ∃ k ∈ ℕ 0 P = k ⋅ 8 + 5$
7 2 5 6 sylancl $⊢ P ∈ ℕ → P mod 8 = 5 → ∃ k ∈ ℕ 0 P = k ⋅ 8 + 5$
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 + 5 = 8 ⁢ k + 5$
15 14 eqeq2d $⊢ P ∈ ℕ ∧ k ∈ ℕ 0 → P = k ⋅ 8 + 5 ↔ P = 8 ⁢ k + 5$
16 15 biimpa $⊢ P ∈ ℕ ∧ k ∈ ℕ 0 ∧ P = k ⋅ 8 + 5 → P = 8 ⁢ k + 5$
17 1 2lgslem3c $⊢ k ∈ ℕ 0 ∧ P = 8 ⁢ k + 5 → N = 2 ⁢ k + 1$
18 8 16 17 syl2an2r $⊢ P ∈ ℕ ∧ k ∈ ℕ 0 ∧ P = k ⋅ 8 + 5 → N = 2 ⁢ k + 1$
19 oveq1 $⊢ N = 2 ⁢ k + 1 → N mod 2 = 2 ⁢ k + 1 mod 2$
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 + 1 mod 2 = 1 ↔ ¬ 2 ∥ 2 ⁢ k + 1$
29 27 28 syl $⊢ k ∈ ℕ 0 → 2 ⁢ k + 1 mod 2 = 1 ↔ ¬ 2 ∥ 2 ⁢ k + 1$
30 23 29 mpbird $⊢ k ∈ ℕ 0 → 2 ⁢ k + 1 mod 2 = 1$
31 19 30 sylan9eqr $⊢ k ∈ ℕ 0 ∧ N = 2 ⁢ k + 1 → N mod 2 = 1$
32 8 18 31 syl2an2r $⊢ P ∈ ℕ ∧ k ∈ ℕ 0 ∧ P = k ⋅ 8 + 5 → N mod 2 = 1$
33 32 rexlimdva2 $⊢ P ∈ ℕ → ∃ k ∈ ℕ 0 P = k ⋅ 8 + 5 → N mod 2 = 1$
34 7 33 syld $⊢ P ∈ ℕ → P mod 8 = 5 → N mod 2 = 1$
35 34 imp $⊢ P ∈ ℕ ∧ P mod 8 = 5 → N mod 2 = 1$