Metamath Proof Explorer

Theorem 2lgslem3d

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

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

Proof

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