Metamath Proof Explorer

Theorem 2lgslem3a

Description: Lemma for 2lgslem3a1 . (Contributed by AV, 14-Jul-2021)

Ref Expression
Hypothesis 2lgslem2.n ⊢ 𝑁 = ( ( ( 𝑃 − 1 ) / 2 ) − ( ⌊ ‘ ( 𝑃 / 4 ) ) )
Assertion 2lgslem3a ( ( 𝐾 ∈ ℕ0 ∧ 𝑃 = ( ( 8 · 𝐾 ) + 1 ) ) → 𝑁 = ( 2 · 𝐾 ) )

Proof

Step Hyp Ref Expression
1 2lgslem2.n ⊢ 𝑁 = ( ( ( 𝑃 − 1 ) / 2 ) − ( ⌊ ‘ ( 𝑃 / 4 ) ) )
2 oveq1 ⊢ ( 𝑃 = ( ( 8 · 𝐾 ) + 1 ) → ( 𝑃 − 1 ) = ( ( ( 8 · 𝐾 ) + 1 ) − 1 ) )
3 2 oveq1d ⊢ ( 𝑃 = ( ( 8 · 𝐾 ) + 1 ) → ( ( 𝑃 − 1 ) / 2 ) = ( ( ( ( 8 · 𝐾 ) + 1 ) − 1 ) / 2 ) )
4 fvoveq1 ⊢ ( 𝑃 = ( ( 8 · 𝐾 ) + 1 ) → ( ⌊ ‘ ( 𝑃 / 4 ) ) = ( ⌊ ‘ ( ( ( 8 · 𝐾 ) + 1 ) / 4 ) ) )
5 3 4 oveq12d ⊢ ( 𝑃 = ( ( 8 · 𝐾 ) + 1 ) → ( ( ( 𝑃 − 1 ) / 2 ) − ( ⌊ ‘ ( 𝑃 / 4 ) ) ) = ( ( ( ( ( 8 · 𝐾 ) + 1 ) − 1 ) / 2 ) − ( ⌊ ‘ ( ( ( 8 · 𝐾 ) + 1 ) / 4 ) ) ) )
6 1 5 syl5eq ⊢ ( 𝑃 = ( ( 8 · 𝐾 ) + 1 ) → 𝑁 = ( ( ( ( ( 8 · 𝐾 ) + 1 ) − 1 ) / 2 ) − ( ⌊ ‘ ( ( ( 8 · 𝐾 ) + 1 ) / 4 ) ) ) )
7 8nn0 ⊢ 8 ∈ ℕ0
8 7 a1i ⊢ ( 𝐾 ∈ ℕ0 → 8 ∈ ℕ0 )
9 id ⊢ ( 𝐾 ∈ ℕ0 → 𝐾 ∈ ℕ0 )
10 8 9 nn0mulcld ⊢ ( 𝐾 ∈ ℕ0 → ( 8 · 𝐾 ) ∈ ℕ0 )
11 10 nn0cnd ⊢ ( 𝐾 ∈ ℕ0 → ( 8 · 𝐾 ) ∈ ℂ )
12 pncan1 ⊢ ( ( 8 · 𝐾 ) ∈ ℂ → ( ( ( 8 · 𝐾 ) + 1 ) − 1 ) = ( 8 · 𝐾 ) )
13 11 12 syl ⊢ ( 𝐾 ∈ ℕ0 → ( ( ( 8 · 𝐾 ) + 1 ) − 1 ) = ( 8 · 𝐾 ) )
14 13 oveq1d ⊢ ( 𝐾 ∈ ℕ0 → ( ( ( ( 8 · 𝐾 ) + 1 ) − 1 ) / 2 ) = ( ( 8 · 𝐾 ) / 2 ) )
15 4cn ⊢ 4 ∈ ℂ
16 2cn ⊢ 2 ∈ ℂ
17 4t2e8 ⊢ ( 4 · 2 ) = 8
18 15 16 17 mulcomli ⊢ ( 2 · 4 ) = 8
19 18 eqcomi ⊢ 8 = ( 2 · 4 )
20 19 a1i ⊢ ( 𝐾 ∈ ℕ0 → 8 = ( 2 · 4 ) )
21 20 oveq1d ⊢ ( 𝐾 ∈ ℕ0 → ( 8 · 𝐾 ) = ( ( 2 · 4 ) · 𝐾 ) )
22 16 a1i ⊢ ( 𝐾 ∈ ℕ0 → 2 ∈ ℂ )
23 15 a1i ⊢ ( 𝐾 ∈ ℕ0 → 4 ∈ ℂ )
24 nn0cn ⊢ ( 𝐾 ∈ ℕ0 → 𝐾 ∈ ℂ )
25 22 23 24 mulassd ⊢ ( 𝐾 ∈ ℕ0 → ( ( 2 · 4 ) · 𝐾 ) = ( 2 · ( 4 · 𝐾 ) ) )
26 21 25 eqtrd ⊢ ( 𝐾 ∈ ℕ0 → ( 8 · 𝐾 ) = ( 2 · ( 4 · 𝐾 ) ) )
27 26 oveq1d ⊢ ( 𝐾 ∈ ℕ0 → ( ( 8 · 𝐾 ) / 2 ) = ( ( 2 · ( 4 · 𝐾 ) ) / 2 ) )
28 4nn0 ⊢ 4 ∈ ℕ0
29 28 a1i ⊢ ( 𝐾 ∈ ℕ0 → 4 ∈ ℕ0 )
30 29 9 nn0mulcld ⊢ ( 𝐾 ∈ ℕ0 → ( 4 · 𝐾 ) ∈ ℕ0 )
31 30 nn0cnd ⊢ ( 𝐾 ∈ ℕ0 → ( 4 · 𝐾 ) ∈ ℂ )
32 2ne0 ⊢ 2 ≠ 0
33 32 a1i ⊢ ( 𝐾 ∈ ℕ0 → 2 ≠ 0 )
34 31 22 33 divcan3d ⊢ ( 𝐾 ∈ ℕ0 → ( ( 2 · ( 4 · 𝐾 ) ) / 2 ) = ( 4 · 𝐾 ) )
35 14 27 34 3eqtrd ⊢ ( 𝐾 ∈ ℕ0 → ( ( ( ( 8 · 𝐾 ) + 1 ) − 1 ) / 2 ) = ( 4 · 𝐾 ) )
36 1cnd ⊢ ( 𝐾 ∈ ℕ0 → 1 ∈ ℂ )
37 4ne0 ⊢ 4 ≠ 0
38 15 37 pm3.2i ⊢ ( 4 ∈ ℂ ∧ 4 ≠ 0 )
39 38 a1i ⊢ ( 𝐾 ∈ ℕ0 → ( 4 ∈ ℂ ∧ 4 ≠ 0 ) )
40 divdir ⊢ ( ( ( 8 · 𝐾 ) ∈ ℂ ∧ 1 ∈ ℂ ∧ ( 4 ∈ ℂ ∧ 4 ≠ 0 ) ) → ( ( ( 8 · 𝐾 ) + 1 ) / 4 ) = ( ( ( 8 · 𝐾 ) / 4 ) + ( 1 / 4 ) ) )
41 11 36 39 40 syl3anc ⊢ ( 𝐾 ∈ ℕ0 → ( ( ( 8 · 𝐾 ) + 1 ) / 4 ) = ( ( ( 8 · 𝐾 ) / 4 ) + ( 1 / 4 ) ) )
42 8cn ⊢ 8 ∈ ℂ
43 42 a1i ⊢ ( 𝐾 ∈ ℕ0 → 8 ∈ ℂ )
44 div23 ⊢ ( ( 8 ∈ ℂ ∧ 𝐾 ∈ ℂ ∧ ( 4 ∈ ℂ ∧ 4 ≠ 0 ) ) → ( ( 8 · 𝐾 ) / 4 ) = ( ( 8 / 4 ) · 𝐾 ) )
45 43 24 39 44 syl3anc ⊢ ( 𝐾 ∈ ℕ0 → ( ( 8 · 𝐾 ) / 4 ) = ( ( 8 / 4 ) · 𝐾 ) )
46 17 eqcomi ⊢ 8 = ( 4 · 2 )
47 46 oveq1i ⊢ ( 8 / 4 ) = ( ( 4 · 2 ) / 4 )
48 16 15 37 divcan3i ⊢ ( ( 4 · 2 ) / 4 ) = 2
49 47 48 eqtri ⊢ ( 8 / 4 ) = 2
50 49 a1i ⊢ ( 𝐾 ∈ ℕ0 → ( 8 / 4 ) = 2 )
51 50 oveq1d ⊢ ( 𝐾 ∈ ℕ0 → ( ( 8 / 4 ) · 𝐾 ) = ( 2 · 𝐾 ) )
52 45 51 eqtrd ⊢ ( 𝐾 ∈ ℕ0 → ( ( 8 · 𝐾 ) / 4 ) = ( 2 · 𝐾 ) )
53 52 oveq1d ⊢ ( 𝐾 ∈ ℕ0 → ( ( ( 8 · 𝐾 ) / 4 ) + ( 1 / 4 ) ) = ( ( 2 · 𝐾 ) + ( 1 / 4 ) ) )
54 41 53 eqtrd ⊢ ( 𝐾 ∈ ℕ0 → ( ( ( 8 · 𝐾 ) + 1 ) / 4 ) = ( ( 2 · 𝐾 ) + ( 1 / 4 ) ) )
55 54 fveq2d ⊢ ( 𝐾 ∈ ℕ0 → ( ⌊ ‘ ( ( ( 8 · 𝐾 ) + 1 ) / 4 ) ) = ( ⌊ ‘ ( ( 2 · 𝐾 ) + ( 1 / 4 ) ) ) )
56 1lt4 ⊢ 1 < 4
57 2nn0 ⊢ 2 ∈ ℕ0
58 57 a1i ⊢ ( 𝐾 ∈ ℕ0 → 2 ∈ ℕ0 )
59 58 9 nn0mulcld ⊢ ( 𝐾 ∈ ℕ0 → ( 2 · 𝐾 ) ∈ ℕ0 )
60 59 nn0zd ⊢ ( 𝐾 ∈ ℕ0 → ( 2 · 𝐾 ) ∈ ℤ )
61 1nn0 ⊢ 1 ∈ ℕ0
62 61 a1i ⊢ ( 𝐾 ∈ ℕ0 → 1 ∈ ℕ0 )
63 4nn ⊢ 4 ∈ ℕ
64 63 a1i ⊢ ( 𝐾 ∈ ℕ0 → 4 ∈ ℕ )
65 adddivflid ⊢ ( ( ( 2 · 𝐾 ) ∈ ℤ ∧ 1 ∈ ℕ0 ∧ 4 ∈ ℕ ) → ( 1 < 4 ↔ ( ⌊ ‘ ( ( 2 · 𝐾 ) + ( 1 / 4 ) ) ) = ( 2 · 𝐾 ) ) )
66 60 62 64 65 syl3anc ⊢ ( 𝐾 ∈ ℕ0 → ( 1 < 4 ↔ ( ⌊ ‘ ( ( 2 · 𝐾 ) + ( 1 / 4 ) ) ) = ( 2 · 𝐾 ) ) )
67 56 66 mpbii ⊢ ( 𝐾 ∈ ℕ0 → ( ⌊ ‘ ( ( 2 · 𝐾 ) + ( 1 / 4 ) ) ) = ( 2 · 𝐾 ) )
68 55 67 eqtrd ⊢ ( 𝐾 ∈ ℕ0 → ( ⌊ ‘ ( ( ( 8 · 𝐾 ) + 1 ) / 4 ) ) = ( 2 · 𝐾 ) )
69 35 68 oveq12d ⊢ ( 𝐾 ∈ ℕ0 → ( ( ( ( ( 8 · 𝐾 ) + 1 ) − 1 ) / 2 ) − ( ⌊ ‘ ( ( ( 8 · 𝐾 ) + 1 ) / 4 ) ) ) = ( ( 4 · 𝐾 ) − ( 2 · 𝐾 ) ) )
70 2t2e4 ⊢ ( 2 · 2 ) = 4
71 70 eqcomi ⊢ 4 = ( 2 · 2 )
72 71 a1i ⊢ ( 𝐾 ∈ ℕ0 → 4 = ( 2 · 2 ) )
73 72 oveq1d ⊢ ( 𝐾 ∈ ℕ0 → ( 4 · 𝐾 ) = ( ( 2 · 2 ) · 𝐾 ) )
74 22 22 24 mulassd ⊢ ( 𝐾 ∈ ℕ0 → ( ( 2 · 2 ) · 𝐾 ) = ( 2 · ( 2 · 𝐾 ) ) )
75 73 74 eqtrd ⊢ ( 𝐾 ∈ ℕ0 → ( 4 · 𝐾 ) = ( 2 · ( 2 · 𝐾 ) ) )
76 75 oveq1d ⊢ ( 𝐾 ∈ ℕ0 → ( ( 4 · 𝐾 ) − ( 2 · 𝐾 ) ) = ( ( 2 · ( 2 · 𝐾 ) ) − ( 2 · 𝐾 ) ) )
77 59 nn0cnd ⊢ ( 𝐾 ∈ ℕ0 → ( 2 · 𝐾 ) ∈ ℂ )
78 2txmxeqx ⊢ ( ( 2 · 𝐾 ) ∈ ℂ → ( ( 2 · ( 2 · 𝐾 ) ) − ( 2 · 𝐾 ) ) = ( 2 · 𝐾 ) )
79 77 78 syl ⊢ ( 𝐾 ∈ ℕ0 → ( ( 2 · ( 2 · 𝐾 ) ) − ( 2 · 𝐾 ) ) = ( 2 · 𝐾 ) )
80 69 76 79 3eqtrd ⊢ ( 𝐾 ∈ ℕ0 → ( ( ( ( ( 8 · 𝐾 ) + 1 ) − 1 ) / 2 ) − ( ⌊ ‘ ( ( ( 8 · 𝐾 ) + 1 ) / 4 ) ) ) = ( 2 · 𝐾 ) )
81 6 80 sylan9eqr ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑃 = ( ( 8 · 𝐾 ) + 1 ) ) → 𝑁 = ( 2 · 𝐾 ) )