# Metamath Proof Explorer

## Theorem 2lgslem3a

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

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

### Proof

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