Metamath Proof Explorer

Theorem 2lgslem3b

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

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

Proof

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