Metamath Proof Explorer


Theorem 2lgslem3d1

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

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

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 ) = 7 → ∃ 𝑘 ∈ ℕ0 𝑃 = ( ( 𝑘 · 8 ) + 7 ) ) )
7 2 5 6 sylancl ( 𝑃 ∈ ℕ → ( ( 𝑃 mod 8 ) = 7 → ∃ 𝑘 ∈ ℕ0 𝑃 = ( ( 𝑘 · 8 ) + 7 ) ) )
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 ) + 7 ) = ( ( 8 · 𝑘 ) + 7 ) )
15 14 eqeq2d ( ( 𝑃 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) → ( 𝑃 = ( ( 𝑘 · 8 ) + 7 ) ↔ 𝑃 = ( ( 8 · 𝑘 ) + 7 ) ) )
16 15 biimpa ( ( ( 𝑃 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑃 = ( ( 𝑘 · 8 ) + 7 ) ) → 𝑃 = ( ( 8 · 𝑘 ) + 7 ) )
17 1 2lgslem3d ( ( 𝑘 ∈ ℕ0𝑃 = ( ( 8 · 𝑘 ) + 7 ) ) → 𝑁 = ( ( 2 · 𝑘 ) + 2 ) )
18 8 16 17 syl2an2r ( ( ( 𝑃 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑃 = ( ( 𝑘 · 8 ) + 7 ) ) → 𝑁 = ( ( 2 · 𝑘 ) + 2 ) )
19 oveq1 ( 𝑁 = ( ( 2 · 𝑘 ) + 2 ) → ( 𝑁 mod 2 ) = ( ( ( 2 · 𝑘 ) + 2 ) mod 2 ) )
20 2t1e2 ( 2 · 1 ) = 2
21 20 eqcomi 2 = ( 2 · 1 )
22 21 a1i ( 𝑘 ∈ ℕ0 → 2 = ( 2 · 1 ) )
23 22 oveq2d ( 𝑘 ∈ ℕ0 → ( ( 2 · 𝑘 ) + 2 ) = ( ( 2 · 𝑘 ) + ( 2 · 1 ) ) )
24 2cnd ( 𝑘 ∈ ℕ0 → 2 ∈ ℂ )
25 1cnd ( 𝑘 ∈ ℕ0 → 1 ∈ ℂ )
26 adddi ( ( 2 ∈ ℂ ∧ 𝑘 ∈ ℂ ∧ 1 ∈ ℂ ) → ( 2 · ( 𝑘 + 1 ) ) = ( ( 2 · 𝑘 ) + ( 2 · 1 ) ) )
27 26 eqcomd ( ( 2 ∈ ℂ ∧ 𝑘 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 2 · 𝑘 ) + ( 2 · 1 ) ) = ( 2 · ( 𝑘 + 1 ) ) )
28 24 9 25 27 syl3anc ( 𝑘 ∈ ℕ0 → ( ( 2 · 𝑘 ) + ( 2 · 1 ) ) = ( 2 · ( 𝑘 + 1 ) ) )
29 9 25 addcld ( 𝑘 ∈ ℕ0 → ( 𝑘 + 1 ) ∈ ℂ )
30 24 29 mulcomd ( 𝑘 ∈ ℕ0 → ( 2 · ( 𝑘 + 1 ) ) = ( ( 𝑘 + 1 ) · 2 ) )
31 23 28 30 3eqtrd ( 𝑘 ∈ ℕ0 → ( ( 2 · 𝑘 ) + 2 ) = ( ( 𝑘 + 1 ) · 2 ) )
32 31 oveq1d ( 𝑘 ∈ ℕ0 → ( ( ( 2 · 𝑘 ) + 2 ) mod 2 ) = ( ( ( 𝑘 + 1 ) · 2 ) mod 2 ) )
33 peano2nn0 ( 𝑘 ∈ ℕ0 → ( 𝑘 + 1 ) ∈ ℕ0 )
34 33 nn0zd ( 𝑘 ∈ ℕ0 → ( 𝑘 + 1 ) ∈ ℤ )
35 2rp 2 ∈ ℝ+
36 mulmod0 ( ( ( 𝑘 + 1 ) ∈ ℤ ∧ 2 ∈ ℝ+ ) → ( ( ( 𝑘 + 1 ) · 2 ) mod 2 ) = 0 )
37 34 35 36 sylancl ( 𝑘 ∈ ℕ0 → ( ( ( 𝑘 + 1 ) · 2 ) mod 2 ) = 0 )
38 32 37 eqtrd ( 𝑘 ∈ ℕ0 → ( ( ( 2 · 𝑘 ) + 2 ) mod 2 ) = 0 )
39 19 38 sylan9eqr ( ( 𝑘 ∈ ℕ0𝑁 = ( ( 2 · 𝑘 ) + 2 ) ) → ( 𝑁 mod 2 ) = 0 )
40 8 18 39 syl2an2r ( ( ( 𝑃 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑃 = ( ( 𝑘 · 8 ) + 7 ) ) → ( 𝑁 mod 2 ) = 0 )
41 40 rexlimdva2 ( 𝑃 ∈ ℕ → ( ∃ 𝑘 ∈ ℕ0 𝑃 = ( ( 𝑘 · 8 ) + 7 ) → ( 𝑁 mod 2 ) = 0 ) )
42 7 41 syld ( 𝑃 ∈ ℕ → ( ( 𝑃 mod 8 ) = 7 → ( 𝑁 mod 2 ) = 0 ) )
43 42 imp ( ( 𝑃 ∈ ℕ ∧ ( 𝑃 mod 8 ) = 7 ) → ( 𝑁 mod 2 ) = 0 )