Metamath Proof Explorer

Theorem 2lgslem3a1

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

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

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 = 1 → ∃ k ∈ ℕ 0 P = k ⋅ 8 + 1
7 2 5 6 sylancl ⊢ P ∈ ℕ → P mod 8 = 1 → ∃ k ∈ ℕ 0 P = 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 → N mod 2 = 2 ⁢ k mod 2
20 2cnd ⊢ k ∈ ℕ 0 → 2 ∈ ℂ
21 20 9 mulcomd ⊢ k ∈ ℕ 0 → 2 ⁢ k = k ⋅ 2
22 21 oveq1d ⊢ k ∈ ℕ 0 → 2 ⁢ k mod 2 = k ⋅ 2 mod 2
23 nn0z ⊢ k ∈ ℕ 0 → k ∈ ℤ
24 2rp ⊢ 2 ∈ ℝ +
25 mulmod0 ⊢ k ∈ ℤ ∧ 2 ∈ ℝ + → k ⋅ 2 mod 2 = 0
26 23 24 25 sylancl ⊢ k ∈ ℕ 0 → k ⋅ 2 mod 2 = 0
27 22 26 eqtrd ⊢ k ∈ ℕ 0 → 2 ⁢ k mod 2 = 0
28 19 27 sylan9eqr ⊢ k ∈ ℕ 0 ∧ N = 2 ⁢ k → N mod 2 = 0
29 8 18 28 syl2an2r ⊢ P ∈ ℕ ∧ k ∈ ℕ 0 ∧ P = k ⋅ 8 + 1 → N mod 2 = 0
30 29 rexlimdva2 ⊢ P ∈ ℕ → ∃ k ∈ ℕ 0 P = k ⋅ 8 + 1 → N mod 2 = 0
31 7 30 syld ⊢ P ∈ ℕ → P mod 8 = 1 → N mod 2 = 0
32 31 imp ⊢ P ∈ ℕ ∧ P mod 8 = 1 → N mod 2 = 0