Metamath Proof Explorer

Theorem 2lgslem3c

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

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

Proof

Step Hyp Ref Expression
1 2lgslem2.n ⊢ 𝑁 = ( ( ( 𝑃 − 1 ) / 2 ) − ( ⌊ ‘ ( 𝑃 / 4 ) ) )
2 oveq1 ⊢ ( 𝑃 = ( ( 8 · 𝐾 ) + 5 ) → ( 𝑃 − 1 ) = ( ( ( 8 · 𝐾 ) + 5 ) − 1 ) )
3 2 oveq1d ⊢ ( 𝑃 = ( ( 8 · 𝐾 ) + 5 ) → ( ( 𝑃 − 1 ) / 2 ) = ( ( ( ( 8 · 𝐾 ) + 5 ) − 1 ) / 2 ) )
4 fvoveq1 ⊢ ( 𝑃 = ( ( 8 · 𝐾 ) + 5 ) → ( ⌊ ‘ ( 𝑃 / 4 ) ) = ( ⌊ ‘ ( ( ( 8 · 𝐾 ) + 5 ) / 4 ) ) )
5 3 4 oveq12d ⊢ ( 𝑃 = ( ( 8 · 𝐾 ) + 5 ) → ( ( ( 𝑃 − 1 ) / 2 ) − ( ⌊ ‘ ( 𝑃 / 4 ) ) ) = ( ( ( ( ( 8 · 𝐾 ) + 5 ) − 1 ) / 2 ) − ( ⌊ ‘ ( ( ( 8 · 𝐾 ) + 5 ) / 4 ) ) ) )
6 1 5 syl5eq ⊢ ( 𝑃 = ( ( 8 · 𝐾 ) + 5 ) → 𝑁 = ( ( ( ( ( 8 · 𝐾 ) + 5 ) − 1 ) / 2 ) − ( ⌊ ‘ ( ( ( 8 · 𝐾 ) + 5 ) / 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 5cn ⊢ 5 ∈ ℂ
13 12 a1i ⊢ ( 𝐾 ∈ ℕ0 → 5 ∈ ℂ )
14 1cnd ⊢ ( 𝐾 ∈ ℕ0 → 1 ∈ ℂ )
15 11 13 14 addsubassd ⊢ ( 𝐾 ∈ ℕ0 → ( ( ( 8 · 𝐾 ) + 5 ) − 1 ) = ( ( 8 · 𝐾 ) + ( 5 − 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 5m1e4 ⊢ ( 5 − 1 ) = 4
28 27 a1i ⊢ ( 𝐾 ∈ ℕ0 → ( 5 − 1 ) = 4 )
29 26 28 oveq12d ⊢ ( 𝐾 ∈ ℕ0 → ( ( 8 · 𝐾 ) + ( 5 − 1 ) ) = ( ( ( 4 · 𝐾 ) · 2 ) + 4 ) )
30 15 29 eqtrd ⊢ ( 𝐾 ∈ ℕ0 → ( ( ( 8 · 𝐾 ) + 5 ) − 1 ) = ( ( ( 4 · 𝐾 ) · 2 ) + 4 ) )
31 30 oveq1d ⊢ ( 𝐾 ∈ ℕ0 → ( ( ( ( 8 · 𝐾 ) + 5 ) − 1 ) / 2 ) = ( ( ( ( 4 · 𝐾 ) · 2 ) + 4 ) / 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 ) ∈ ℂ ∧ 4 ∈ ℂ ∧ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ) → ( ( ( ( 4 · 𝐾 ) · 2 ) + 4 ) / 2 ) = ( ( ( ( 4 · 𝐾 ) · 2 ) / 2 ) + ( 4 / 2 ) ) )
41 36 21 39 40 syl3anc ⊢ ( 𝐾 ∈ ℕ0 → ( ( ( ( 4 · 𝐾 ) · 2 ) + 4 ) / 2 ) = ( ( ( ( 4 · 𝐾 ) · 2 ) / 2 ) + ( 4 / 2 ) ) )
42 2ne0 ⊢ 2 ≠ 0
43 42 a1i ⊢ ( 𝐾 ∈ ℕ0 → 2 ≠ 0 )
44 35 23 43 divcan4d ⊢ ( 𝐾 ∈ ℕ0 → ( ( ( 4 · 𝐾 ) · 2 ) / 2 ) = ( 4 · 𝐾 ) )
45 4d2e2 ⊢ ( 4 / 2 ) = 2
46 45 a1i ⊢ ( 𝐾 ∈ ℕ0 → ( 4 / 2 ) = 2 )
47 44 46 oveq12d ⊢ ( 𝐾 ∈ ℕ0 → ( ( ( ( 4 · 𝐾 ) · 2 ) / 2 ) + ( 4 / 2 ) ) = ( ( 4 · 𝐾 ) + 2 ) )
48 31 41 47 3eqtrd ⊢ ( 𝐾 ∈ ℕ0 → ( ( ( ( 8 · 𝐾 ) + 5 ) − 1 ) / 2 ) = ( ( 4 · 𝐾 ) + 2 ) )
49 4ne0 ⊢ 4 ≠ 0
50 20 49 pm3.2i ⊢ ( 4 ∈ ℂ ∧ 4 ≠ 0 )
51 50 a1i ⊢ ( 𝐾 ∈ ℕ0 → ( 4 ∈ ℂ ∧ 4 ≠ 0 ) )
52 divdir ⊢ ( ( ( 8 · 𝐾 ) ∈ ℂ ∧ 5 ∈ ℂ ∧ ( 4 ∈ ℂ ∧ 4 ≠ 0 ) ) → ( ( ( 8 · 𝐾 ) + 5 ) / 4 ) = ( ( ( 8 · 𝐾 ) / 4 ) + ( 5 / 4 ) ) )
53 11 13 51 52 syl3anc ⊢ ( 𝐾 ∈ ℕ0 → ( ( ( 8 · 𝐾 ) + 5 ) / 4 ) = ( ( ( 8 · 𝐾 ) / 4 ) + ( 5 / 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 ) + ( 5 / 4 ) ) = ( ( 2 · 𝐾 ) + ( 5 / 4 ) ) )
65 53 64 eqtrd ⊢ ( 𝐾 ∈ ℕ0 → ( ( ( 8 · 𝐾 ) + 5 ) / 4 ) = ( ( 2 · 𝐾 ) + ( 5 / 4 ) ) )
66 65 fveq2d ⊢ ( 𝐾 ∈ ℕ0 → ( ⌊ ‘ ( ( ( 8 · 𝐾 ) + 5 ) / 4 ) ) = ( ⌊ ‘ ( ( 2 · 𝐾 ) + ( 5 / 4 ) ) ) )
67 1lt4 ⊢ 1 < 4
68 2nn0 ⊢ 2 ∈ ℕ0
69 68 a1i ⊢ ( 𝐾 ∈ ℕ0 → 2 ∈ ℕ0 )
70 69 9 nn0mulcld ⊢ ( 𝐾 ∈ ℕ0 → ( 2 · 𝐾 ) ∈ ℕ0 )
71 70 nn0zd ⊢ ( 𝐾 ∈ ℕ0 → ( 2 · 𝐾 ) ∈ ℤ )
72 71 peano2zd ⊢ ( 𝐾 ∈ ℕ0 → ( ( 2 · 𝐾 ) + 1 ) ∈ ℤ )
73 1nn0 ⊢ 1 ∈ ℕ0
74 73 a1i ⊢ ( 𝐾 ∈ ℕ0 → 1 ∈ ℕ0 )
75 4nn ⊢ 4 ∈ ℕ
76 75 a1i ⊢ ( 𝐾 ∈ ℕ0 → 4 ∈ ℕ )
77 adddivflid ⊢ ( ( ( ( 2 · 𝐾 ) + 1 ) ∈ ℤ ∧ 1 ∈ ℕ0 ∧ 4 ∈ ℕ ) → ( 1 < 4 ↔ ( ⌊ ‘ ( ( ( 2 · 𝐾 ) + 1 ) + ( 1 / 4 ) ) ) = ( ( 2 · 𝐾 ) + 1 ) ) )
78 72 74 76 77 syl3anc ⊢ ( 𝐾 ∈ ℕ0 → ( 1 < 4 ↔ ( ⌊ ‘ ( ( ( 2 · 𝐾 ) + 1 ) + ( 1 / 4 ) ) ) = ( ( 2 · 𝐾 ) + 1 ) ) )
79 23 24 mulcld ⊢ ( 𝐾 ∈ ℕ0 → ( 2 · 𝐾 ) ∈ ℂ )
80 49 a1i ⊢ ( 𝐾 ∈ ℕ0 → 4 ≠ 0 )
81 21 80 reccld ⊢ ( 𝐾 ∈ ℕ0 → ( 1 / 4 ) ∈ ℂ )
82 79 14 81 addassd ⊢ ( 𝐾 ∈ ℕ0 → ( ( ( 2 · 𝐾 ) + 1 ) + ( 1 / 4 ) ) = ( ( 2 · 𝐾 ) + ( 1 + ( 1 / 4 ) ) ) )
83 df-5 ⊢ 5 = ( 4 + 1 )
84 83 oveq1i ⊢ ( 5 / 4 ) = ( ( 4 + 1 ) / 4 )
85 ax-1cn ⊢ 1 ∈ ℂ
86 20 85 20 49 divdiri ⊢ ( ( 4 + 1 ) / 4 ) = ( ( 4 / 4 ) + ( 1 / 4 ) )
87 20 49 dividi ⊢ ( 4 / 4 ) = 1
88 87 oveq1i ⊢ ( ( 4 / 4 ) + ( 1 / 4 ) ) = ( 1 + ( 1 / 4 ) )
89 84 86 88 3eqtri ⊢ ( 5 / 4 ) = ( 1 + ( 1 / 4 ) )
90 89 a1i ⊢ ( 𝐾 ∈ ℕ0 → ( 5 / 4 ) = ( 1 + ( 1 / 4 ) ) )
91 90 eqcomd ⊢ ( 𝐾 ∈ ℕ0 → ( 1 + ( 1 / 4 ) ) = ( 5 / 4 ) )
92 91 oveq2d ⊢ ( 𝐾 ∈ ℕ0 → ( ( 2 · 𝐾 ) + ( 1 + ( 1 / 4 ) ) ) = ( ( 2 · 𝐾 ) + ( 5 / 4 ) ) )
93 82 92 eqtrd ⊢ ( 𝐾 ∈ ℕ0 → ( ( ( 2 · 𝐾 ) + 1 ) + ( 1 / 4 ) ) = ( ( 2 · 𝐾 ) + ( 5 / 4 ) ) )
94 93 fveqeq2d ⊢ ( 𝐾 ∈ ℕ0 → ( ( ⌊ ‘ ( ( ( 2 · 𝐾 ) + 1 ) + ( 1 / 4 ) ) ) = ( ( 2 · 𝐾 ) + 1 ) ↔ ( ⌊ ‘ ( ( 2 · 𝐾 ) + ( 5 / 4 ) ) ) = ( ( 2 · 𝐾 ) + 1 ) ) )
95 78 94 bitrd ⊢ ( 𝐾 ∈ ℕ0 → ( 1 < 4 ↔ ( ⌊ ‘ ( ( 2 · 𝐾 ) + ( 5 / 4 ) ) ) = ( ( 2 · 𝐾 ) + 1 ) ) )
96 67 95 mpbii ⊢ ( 𝐾 ∈ ℕ0 → ( ⌊ ‘ ( ( 2 · 𝐾 ) + ( 5 / 4 ) ) ) = ( ( 2 · 𝐾 ) + 1 ) )
97 66 96 eqtrd ⊢ ( 𝐾 ∈ ℕ0 → ( ⌊ ‘ ( ( ( 8 · 𝐾 ) + 5 ) / 4 ) ) = ( ( 2 · 𝐾 ) + 1 ) )
98 48 97 oveq12d ⊢ ( 𝐾 ∈ ℕ0 → ( ( ( ( ( 8 · 𝐾 ) + 5 ) − 1 ) / 2 ) − ( ⌊ ‘ ( ( ( 8 · 𝐾 ) + 5 ) / 4 ) ) ) = ( ( ( 4 · 𝐾 ) + 2 ) − ( ( 2 · 𝐾 ) + 1 ) ) )
99 70 nn0cnd ⊢ ( 𝐾 ∈ ℕ0 → ( 2 · 𝐾 ) ∈ ℂ )
100 35 23 99 14 addsub4d ⊢ ( 𝐾 ∈ ℕ0 → ( ( ( 4 · 𝐾 ) + 2 ) − ( ( 2 · 𝐾 ) + 1 ) ) = ( ( ( 4 · 𝐾 ) − ( 2 · 𝐾 ) ) + ( 2 − 1 ) ) )
101 2t2e4 ⊢ ( 2 · 2 ) = 4
102 101 eqcomi ⊢ 4 = ( 2 · 2 )
103 102 a1i ⊢ ( 𝐾 ∈ ℕ0 → 4 = ( 2 · 2 ) )
104 103 oveq1d ⊢ ( 𝐾 ∈ ℕ0 → ( 4 · 𝐾 ) = ( ( 2 · 2 ) · 𝐾 ) )
105 23 23 24 mulassd ⊢ ( 𝐾 ∈ ℕ0 → ( ( 2 · 2 ) · 𝐾 ) = ( 2 · ( 2 · 𝐾 ) ) )
106 104 105 eqtrd ⊢ ( 𝐾 ∈ ℕ0 → ( 4 · 𝐾 ) = ( 2 · ( 2 · 𝐾 ) ) )
107 106 oveq1d ⊢ ( 𝐾 ∈ ℕ0 → ( ( 4 · 𝐾 ) − ( 2 · 𝐾 ) ) = ( ( 2 · ( 2 · 𝐾 ) ) − ( 2 · 𝐾 ) ) )
108 2txmxeqx ⊢ ( ( 2 · 𝐾 ) ∈ ℂ → ( ( 2 · ( 2 · 𝐾 ) ) − ( 2 · 𝐾 ) ) = ( 2 · 𝐾 ) )
109 99 108 syl ⊢ ( 𝐾 ∈ ℕ0 → ( ( 2 · ( 2 · 𝐾 ) ) − ( 2 · 𝐾 ) ) = ( 2 · 𝐾 ) )
110 107 109 eqtrd ⊢ ( 𝐾 ∈ ℕ0 → ( ( 4 · 𝐾 ) − ( 2 · 𝐾 ) ) = ( 2 · 𝐾 ) )
111 2m1e1 ⊢ ( 2 − 1 ) = 1
112 111 a1i ⊢ ( 𝐾 ∈ ℕ0 → ( 2 − 1 ) = 1 )
113 110 112 oveq12d ⊢ ( 𝐾 ∈ ℕ0 → ( ( ( 4 · 𝐾 ) − ( 2 · 𝐾 ) ) + ( 2 − 1 ) ) = ( ( 2 · 𝐾 ) + 1 ) )
114 98 100 113 3eqtrd ⊢ ( 𝐾 ∈ ℕ0 → ( ( ( ( ( 8 · 𝐾 ) + 5 ) − 1 ) / 2 ) − ( ⌊ ‘ ( ( ( 8 · 𝐾 ) + 5 ) / 4 ) ) ) = ( ( 2 · 𝐾 ) + 1 ) )
115 6 114 sylan9eqr ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑃 = ( ( 8 · 𝐾 ) + 5 ) ) → 𝑁 = ( ( 2 · 𝐾 ) + 1 ) )