Metamath Proof Explorer

Theorem 2lgslem3c1

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

Ref Expression
Hypothesis 2lgslem2.n ⊢ 𝑁 = ( ( ( 𝑃 − 1 ) / 2 ) − ( ⌊ ‘ ( 𝑃 / 4 ) ) )
Assertion 2lgslem3c1 ( ( 𝑃 ∈ ℕ ∧ ( 𝑃 mod 8 ) = 5 ) → ( 𝑁 mod 2 ) = 1 )

Proof

Step Hyp Ref Expression
1 2lgslem2.n ⊢ 𝑁 = ( ( ( 𝑃 − 1 ) / 2 ) − ( ⌊ ‘ ( 𝑃 / 4 ) ) )
2 nnnn0 ⊢ ( 𝑃 ∈ ℕ → 𝑃 ∈ ℕ0 )
3 8nn ⊢ 8 ∈ ℕ
4 nnrp ⊢ ( 8 ∈ ℕ → 8 ∈ ℝ+ )
5 3 4 ax-mp ⊢ 8 ∈ ℝ+
6 modmuladdnn0 ⊢ ( ( 𝑃 ∈ ℕ0 ∧ 8 ∈ ℝ+ ) → ( ( 𝑃 mod 8 ) = 5 → ∃ 𝑘 ∈ ℕ0 𝑃 = ( ( 𝑘 · 8 ) + 5 ) ) )
7 2 5 6 sylancl ⊢ ( 𝑃 ∈ ℕ → ( ( 𝑃 mod 8 ) = 5 → ∃ 𝑘 ∈ ℕ0 𝑃 = ( ( 𝑘 · 8 ) + 5 ) ) )
8 simpr ⊢ ( ( 𝑃 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) → 𝑘 ∈ ℕ0 )
9 nn0cn ⊢ ( 𝑘 ∈ ℕ0 → 𝑘 ∈ ℂ )
10 8cn ⊢ 8 ∈ ℂ
11 10 a1i ⊢ ( 𝑘 ∈ ℕ0 → 8 ∈ ℂ )
12 9 11 mulcomd ⊢ ( 𝑘 ∈ ℕ0 → ( 𝑘 · 8 ) = ( 8 · 𝑘 ) )
13 12 adantl ⊢ ( ( 𝑃 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) → ( 𝑘 · 8 ) = ( 8 · 𝑘 ) )
14 13 oveq1d ⊢ ( ( 𝑃 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑘 · 8 ) + 5 ) = ( ( 8 · 𝑘 ) + 5 ) )
15 14 eqeq2d ⊢ ( ( 𝑃 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) → ( 𝑃 = ( ( 𝑘 · 8 ) + 5 ) ↔ 𝑃 = ( ( 8 · 𝑘 ) + 5 ) ) )
16 15 biimpa ⊢ ( ( ( 𝑃 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑃 = ( ( 𝑘 · 8 ) + 5 ) ) → 𝑃 = ( ( 8 · 𝑘 ) + 5 ) )
17 1 2lgslem3c ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑃 = ( ( 8 · 𝑘 ) + 5 ) ) → 𝑁 = ( ( 2 · 𝑘 ) + 1 ) )
18 8 16 17 syl2an2r ⊢ ( ( ( 𝑃 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑃 = ( ( 𝑘 · 8 ) + 5 ) ) → 𝑁 = ( ( 2 · 𝑘 ) + 1 ) )
19 oveq1 ⊢ ( 𝑁 = ( ( 2 · 𝑘 ) + 1 ) → ( 𝑁 mod 2 ) = ( ( ( 2 · 𝑘 ) + 1 ) mod 2 ) )
20 nn0z ⊢ ( 𝑘 ∈ ℕ0 → 𝑘 ∈ ℤ )
21 eqidd ⊢ ( 𝑘 ∈ ℕ0 → ( ( 2 · 𝑘 ) + 1 ) = ( ( 2 · 𝑘 ) + 1 ) )
22 2tp1odd ⊢ ( ( 𝑘 ∈ ℤ ∧ ( ( 2 · 𝑘 ) + 1 ) = ( ( 2 · 𝑘 ) + 1 ) ) → ¬ 2 ∥ ( ( 2 · 𝑘 ) + 1 ) )
23 20 21 22 syl2anc ⊢ ( 𝑘 ∈ ℕ0 → ¬ 2 ∥ ( ( 2 · 𝑘 ) + 1 ) )
24 2z ⊢ 2 ∈ ℤ
25 24 a1i ⊢ ( 𝑘 ∈ ℕ0 → 2 ∈ ℤ )
26 25 20 zmulcld ⊢ ( 𝑘 ∈ ℕ0 → ( 2 · 𝑘 ) ∈ ℤ )
27 26 peano2zd ⊢ ( 𝑘 ∈ ℕ0 → ( ( 2 · 𝑘 ) + 1 ) ∈ ℤ )
28 mod2eq1n2dvds ⊢ ( ( ( 2 · 𝑘 ) + 1 ) ∈ ℤ → ( ( ( ( 2 · 𝑘 ) + 1 ) mod 2 ) = 1 ↔ ¬ 2 ∥ ( ( 2 · 𝑘 ) + 1 ) ) )
29 27 28 syl ⊢ ( 𝑘 ∈ ℕ0 → ( ( ( ( 2 · 𝑘 ) + 1 ) mod 2 ) = 1 ↔ ¬ 2 ∥ ( ( 2 · 𝑘 ) + 1 ) ) )
30 23 29 mpbird ⊢ ( 𝑘 ∈ ℕ0 → ( ( ( 2 · 𝑘 ) + 1 ) mod 2 ) = 1 )
31 19 30 sylan9eqr ⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑁 = ( ( 2 · 𝑘 ) + 1 ) ) → ( 𝑁 mod 2 ) = 1 )
32 8 18 31 syl2an2r ⊢ ( ( ( 𝑃 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑃 = ( ( 𝑘 · 8 ) + 5 ) ) → ( 𝑁 mod 2 ) = 1 )
33 32 rexlimdva2 ⊢ ( 𝑃 ∈ ℕ → ( ∃ 𝑘 ∈ ℕ0 𝑃 = ( ( 𝑘 · 8 ) + 5 ) → ( 𝑁 mod 2 ) = 1 ) )
34 7 33 syld ⊢ ( 𝑃 ∈ ℕ → ( ( 𝑃 mod 8 ) = 5 → ( 𝑁 mod 2 ) = 1 ) )
35 34 imp ⊢ ( ( 𝑃 ∈ ℕ ∧ ( 𝑃 mod 8 ) = 5 ) → ( 𝑁 mod 2 ) = 1 )