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