# Metamath Proof Explorer

## Theorem 2lgslem3b

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

Ref Expression
Hypothesis 2lgslem2.n ${⊢}{N}=\left(\frac{{P}-1}{2}\right)-⌊\frac{{P}}{4}⌋$
Assertion 2lgslem3b ${⊢}\left({K}\in {ℕ}_{0}\wedge {P}=8{K}+3\right)\to {N}=2{K}+1$

### Proof

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