# Metamath Proof Explorer

## Theorem 2lgslem3c

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

Ref Expression
Hypothesis 2lgslem2.n ${⊢}{N}=\left(\frac{{P}-1}{2}\right)-⌊\frac{{P}}{4}⌋$
Assertion 2lgslem3c ${⊢}\left({K}\in {ℕ}_{0}\wedge {P}=8{K}+5\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}+5\to {P}-1=8{K}+5-1$
3 2 oveq1d ${⊢}{P}=8{K}+5\to \frac{{P}-1}{2}=\frac{8{K}+5-1}{2}$
4 fvoveq1 ${⊢}{P}=8{K}+5\to ⌊\frac{{P}}{4}⌋=⌊\frac{8{K}+5}{4}⌋$
5 3 4 oveq12d ${⊢}{P}=8{K}+5\to \left(\frac{{P}-1}{2}\right)-⌊\frac{{P}}{4}⌋=\left(\frac{8{K}+5-1}{2}\right)-⌊\frac{8{K}+5}{4}⌋$
6 1 5 syl5eq ${⊢}{P}=8{K}+5\to {N}=\left(\frac{8{K}+5-1}{2}\right)-⌊\frac{8{K}+5}{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 5cn ${⊢}5\in ℂ$
13 12 a1i ${⊢}{K}\in {ℕ}_{0}\to 5\in ℂ$
14 1cnd ${⊢}{K}\in {ℕ}_{0}\to 1\in ℂ$
15 11 13 14 addsubassd ${⊢}{K}\in {ℕ}_{0}\to 8{K}+5-1=8{K}+5-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 5m1e4 ${⊢}5-1=4$
28 27 a1i ${⊢}{K}\in {ℕ}_{0}\to 5-1=4$
29 26 28 oveq12d ${⊢}{K}\in {ℕ}_{0}\to 8{K}+5-1=4{K}\cdot 2+4$
30 15 29 eqtrd ${⊢}{K}\in {ℕ}_{0}\to 8{K}+5-1=4{K}\cdot 2+4$
31 30 oveq1d ${⊢}{K}\in {ℕ}_{0}\to \frac{8{K}+5-1}{2}=\frac{4{K}\cdot 2+4}{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 4\in ℂ\wedge \left(2\in ℂ\wedge 2\ne 0\right)\right)\to \frac{4{K}\cdot 2+4}{2}=\left(\frac{4{K}\cdot 2}{2}\right)+\left(\frac{4}{2}\right)$
41 36 21 39 40 syl3anc ${⊢}{K}\in {ℕ}_{0}\to \frac{4{K}\cdot 2+4}{2}=\left(\frac{4{K}\cdot 2}{2}\right)+\left(\frac{4}{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 4d2e2 ${⊢}\frac{4}{2}=2$
46 45 a1i ${⊢}{K}\in {ℕ}_{0}\to \frac{4}{2}=2$
47 44 46 oveq12d ${⊢}{K}\in {ℕ}_{0}\to \left(\frac{4{K}\cdot 2}{2}\right)+\left(\frac{4}{2}\right)=4{K}+2$
48 31 41 47 3eqtrd ${⊢}{K}\in {ℕ}_{0}\to \frac{8{K}+5-1}{2}=4{K}+2$
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 5\in ℂ\wedge \left(4\in ℂ\wedge 4\ne 0\right)\right)\to \frac{8{K}+5}{4}=\left(\frac{8{K}}{4}\right)+\left(\frac{5}{4}\right)$
53 11 13 51 52 syl3anc ${⊢}{K}\in {ℕ}_{0}\to \frac{8{K}+5}{4}=\left(\frac{8{K}}{4}\right)+\left(\frac{5}{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{5}{4}\right)=2{K}+\left(\frac{5}{4}\right)$
65 53 64 eqtrd ${⊢}{K}\in {ℕ}_{0}\to \frac{8{K}+5}{4}=2{K}+\left(\frac{5}{4}\right)$
66 65 fveq2d ${⊢}{K}\in {ℕ}_{0}\to ⌊\frac{8{K}+5}{4}⌋=⌊2{K}+\left(\frac{5}{4}\right)⌋$
67 1lt4 ${⊢}1<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 71 peano2zd ${⊢}{K}\in {ℕ}_{0}\to 2{K}+1\in ℤ$
73 1nn0 ${⊢}1\in {ℕ}_{0}$
74 73 a1i ${⊢}{K}\in {ℕ}_{0}\to 1\in {ℕ}_{0}$
75 4nn ${⊢}4\in ℕ$
76 75 a1i ${⊢}{K}\in {ℕ}_{0}\to 4\in ℕ$
77 adddivflid ${⊢}\left(2{K}+1\in ℤ\wedge 1\in {ℕ}_{0}\wedge 4\in ℕ\right)\to \left(1<4↔⌊2{K}+1+\left(\frac{1}{4}\right)⌋=2{K}+1\right)$
78 72 74 76 77 syl3anc ${⊢}{K}\in {ℕ}_{0}\to \left(1<4↔⌊2{K}+1+\left(\frac{1}{4}\right)⌋=2{K}+1\right)$
79 23 24 mulcld ${⊢}{K}\in {ℕ}_{0}\to 2{K}\in ℂ$
80 49 a1i ${⊢}{K}\in {ℕ}_{0}\to 4\ne 0$
81 21 80 reccld ${⊢}{K}\in {ℕ}_{0}\to \frac{1}{4}\in ℂ$
82 79 14 81 addassd ${⊢}{K}\in {ℕ}_{0}\to 2{K}+1+\left(\frac{1}{4}\right)=2{K}+1+\left(\frac{1}{4}\right)$
83 df-5 ${⊢}5=4+1$
84 83 oveq1i ${⊢}\frac{5}{4}=\frac{4+1}{4}$
85 ax-1cn ${⊢}1\in ℂ$
86 20 85 20 49 divdiri ${⊢}\frac{4+1}{4}=\left(\frac{4}{4}\right)+\left(\frac{1}{4}\right)$
87 20 49 dividi ${⊢}\frac{4}{4}=1$
88 87 oveq1i ${⊢}\left(\frac{4}{4}\right)+\left(\frac{1}{4}\right)=1+\left(\frac{1}{4}\right)$
89 84 86 88 3eqtri ${⊢}\frac{5}{4}=1+\left(\frac{1}{4}\right)$
90 89 a1i ${⊢}{K}\in {ℕ}_{0}\to \frac{5}{4}=1+\left(\frac{1}{4}\right)$
91 90 eqcomd ${⊢}{K}\in {ℕ}_{0}\to 1+\left(\frac{1}{4}\right)=\frac{5}{4}$
92 91 oveq2d ${⊢}{K}\in {ℕ}_{0}\to 2{K}+1+\left(\frac{1}{4}\right)=2{K}+\left(\frac{5}{4}\right)$
93 82 92 eqtrd ${⊢}{K}\in {ℕ}_{0}\to 2{K}+1+\left(\frac{1}{4}\right)=2{K}+\left(\frac{5}{4}\right)$
94 93 fveqeq2d ${⊢}{K}\in {ℕ}_{0}\to \left(⌊2{K}+1+\left(\frac{1}{4}\right)⌋=2{K}+1↔⌊2{K}+\left(\frac{5}{4}\right)⌋=2{K}+1\right)$
95 78 94 bitrd ${⊢}{K}\in {ℕ}_{0}\to \left(1<4↔⌊2{K}+\left(\frac{5}{4}\right)⌋=2{K}+1\right)$
96 67 95 mpbii ${⊢}{K}\in {ℕ}_{0}\to ⌊2{K}+\left(\frac{5}{4}\right)⌋=2{K}+1$
97 66 96 eqtrd ${⊢}{K}\in {ℕ}_{0}\to ⌊\frac{8{K}+5}{4}⌋=2{K}+1$
98 48 97 oveq12d ${⊢}{K}\in {ℕ}_{0}\to \left(\frac{8{K}+5-1}{2}\right)-⌊\frac{8{K}+5}{4}⌋=4{K}+2-\left(2{K}+1\right)$
99 70 nn0cnd ${⊢}{K}\in {ℕ}_{0}\to 2{K}\in ℂ$
100 35 23 99 14 addsub4d ${⊢}{K}\in {ℕ}_{0}\to 4{K}+2-\left(2{K}+1\right)=\left(4{K}-2{K}\right)+2-1$
101 2t2e4 ${⊢}2\cdot 2=4$
102 101 eqcomi ${⊢}4=2\cdot 2$
103 102 a1i ${⊢}{K}\in {ℕ}_{0}\to 4=2\cdot 2$
104 103 oveq1d ${⊢}{K}\in {ℕ}_{0}\to 4{K}=2\cdot 2{K}$
105 23 23 24 mulassd ${⊢}{K}\in {ℕ}_{0}\to 2\cdot 2{K}=22{K}$
106 104 105 eqtrd ${⊢}{K}\in {ℕ}_{0}\to 4{K}=22{K}$
107 106 oveq1d ${⊢}{K}\in {ℕ}_{0}\to 4{K}-2{K}=22{K}-2{K}$
108 2txmxeqx ${⊢}2{K}\in ℂ\to 22{K}-2{K}=2{K}$
109 99 108 syl ${⊢}{K}\in {ℕ}_{0}\to 22{K}-2{K}=2{K}$
110 107 109 eqtrd ${⊢}{K}\in {ℕ}_{0}\to 4{K}-2{K}=2{K}$
111 2m1e1 ${⊢}2-1=1$
112 111 a1i ${⊢}{K}\in {ℕ}_{0}\to 2-1=1$
113 110 112 oveq12d ${⊢}{K}\in {ℕ}_{0}\to \left(4{K}-2{K}\right)+2-1=2{K}+1$
114 98 100 113 3eqtrd ${⊢}{K}\in {ℕ}_{0}\to \left(\frac{8{K}+5-1}{2}\right)-⌊\frac{8{K}+5}{4}⌋=2{K}+1$
115 6 114 sylan9eqr ${⊢}\left({K}\in {ℕ}_{0}\wedge {P}=8{K}+5\right)\to {N}=2{K}+1$