Theorem 2lgslem3d

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

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

Proof

Step	Hyp	Ref	Expression
1		2lgslem2.n	$$⊢N=\left(\frac{P-1}{2}\right)-⌊\frac{P}{4}⌋$$
2		oveq1	$$⊢P=8K+7\to P-1=8K+7-1$$
3	2	oveq1d	$$⊢P=8K+7\to \frac{P-1}{2}=\frac{8K+7-1}{2}$$
4		fvoveq1	$$⊢P=8K+7\to ⌊\frac{P}{4}⌋=⌊\frac{8K+7}{4}⌋$$
5	3 4	oveq12d	$$⊢P=8K+7\to \left(\frac{P-1}{2}\right)-⌊\frac{P}{4}⌋=\left(\frac{8K+7-1}{2}\right)-⌊\frac{8K+7}{4}⌋$$
6	1 5	syl5eq	$$⊢P=8K+7\to N=\left(\frac{8K+7-1}{2}\right)-⌊\frac{8K+7}{4}⌋$$
7		8nn0	$$⊢8\in {\mathbb{N}}_0$$
8	7	a1i	$$⊢K\in {\mathbb{N}}_0\to 8\in {\mathbb{N}}_0$$
9		id	$$⊢K\in {\mathbb{N}}_0\to K\in {\mathbb{N}}_0$$
10	8 9	nn0mulcld	$$⊢K\in {\mathbb{N}}_0\to 8K\in {\mathbb{N}}_0$$
11	10	nn0cnd	$$⊢K\in {\mathbb{N}}_0\to 8K\in ℂ$$
12		7cn	$$⊢7\in ℂ$$
13	12	a1i	$$⊢K\in {\mathbb{N}}_0\to 7\in ℂ$$
14		1cnd	$$⊢K\in {\mathbb{N}}_0\to 1\in ℂ$$
15	11 13 14	addsubassd	$$⊢K\in {\mathbb{N}}_0\to 8K+7-1=8K+7-1$$
16		4t2e8	$$⊢4\cdot 2=8$$
17	16	eqcomi	$$⊢8=4\cdot 2$$
18	17	a1i	$$⊢K\in {\mathbb{N}}_0\to 8=4\cdot 2$$
19	18	oveq1d	$$⊢K\in {\mathbb{N}}_0\to 8K=4\cdot 2K$$
20		4cn	$$⊢4\in ℂ$$
21	20	a1i	$$⊢K\in {\mathbb{N}}_0\to 4\in ℂ$$
22		2cn	$$⊢2\in ℂ$$
23	22	a1i	$$⊢K\in {\mathbb{N}}_0\to 2\in ℂ$$
24		nn0cn	$$⊢K\in {\mathbb{N}}_0\to K\in ℂ$$
25	21 23 24	mul32d	$$⊢K\in {\mathbb{N}}_0\to 4\cdot 2K=4K\cdot 2$$
26	19 25	eqtrd	$$⊢K\in {\mathbb{N}}_0\to 8K=4K\cdot 2$$
27		7m1e6	$$⊢7-1=6$$
28	27	a1i	$$⊢K\in {\mathbb{N}}_0\to 7-1=6$$
29	26 28	oveq12d	$$⊢K\in {\mathbb{N}}_0\to 8K+7-1=4K\cdot 2+6$$
30	15 29	eqtrd	$$⊢K\in {\mathbb{N}}_0\to 8K+7-1=4K\cdot 2+6$$
31	30	oveq1d	$$⊢K\in {\mathbb{N}}_0\to \frac{8K+7-1}{2}=\frac{4K\cdot 2+6}{2}$$
32		4nn0	$$⊢4\in {\mathbb{N}}_0$$
33	32	a1i	$$⊢K\in {\mathbb{N}}_0\to 4\in {\mathbb{N}}_0$$
34	33 9	nn0mulcld	$$⊢K\in {\mathbb{N}}_0\to 4K\in {\mathbb{N}}_0$$
35	34	nn0cnd	$$⊢K\in {\mathbb{N}}_0\to 4K\in ℂ$$
36	35 23	mulcld	$$⊢K\in {\mathbb{N}}_0\to 4K\cdot 2\in ℂ$$
37		6cn	$$⊢6\in ℂ$$
38	37	a1i	$$⊢K\in {\mathbb{N}}_0\to 6\in ℂ$$
39		2rp	$$⊢2\in {ℝ}^{+}$$
40	39	a1i	$$⊢K\in {\mathbb{N}}_0\to 2\in {ℝ}^{+}$$
41	40	rpcnne0d	$$⊢K\in {\mathbb{N}}_0\to \left(2\in ℂ\wedge 2\ne 0\right)$$
42		divdir	$$⊢\left(4K\cdot 2\in ℂ\wedge 6\in ℂ\wedge \left(2\in ℂ\wedge 2\ne 0\right)\right)\to \frac{4K\cdot 2+6}{2}=\left(\frac{4K\cdot 2}{2}\right)+\left(\frac{6}{2}\right)$$
43	36 38 41 42	syl3anc	$$⊢K\in {\mathbb{N}}_0\to \frac{4K\cdot 2+6}{2}=\left(\frac{4K\cdot 2}{2}\right)+\left(\frac{6}{2}\right)$$
44		2ne0	$$⊢2\ne 0$$
45	44	a1i	$$⊢K\in {\mathbb{N}}_0\to 2\ne 0$$
46	35 23 45	divcan4d	$$⊢K\in {\mathbb{N}}_0\to \frac{4K\cdot 2}{2}=4K$$
47		3t2e6	$$⊢3\cdot 2=6$$
48	47	eqcomi	$$⊢6=3\cdot 2$$
49	48	oveq1i	$$⊢\frac{6}{2}=\frac{3\cdot 2}{2}$$
50		3cn	$$⊢3\in ℂ$$
51	50 22 44	divcan4i	$$⊢\frac{3\cdot 2}{2}=3$$
52	49 51	eqtri	$$⊢\frac{6}{2}=3$$
53	52	a1i	$$⊢K\in {\mathbb{N}}_0\to \frac{6}{2}=3$$
54	46 53	oveq12d	$$⊢K\in {\mathbb{N}}_0\to \left(\frac{4K\cdot 2}{2}\right)+\left(\frac{6}{2}\right)=4K+3$$
55	31 43 54	3eqtrd	$$⊢K\in {\mathbb{N}}_0\to \frac{8K+7-1}{2}=4K+3$$
56		4ne0	$$⊢4\ne 0$$
57	20 56	pm3.2i	$$⊢\left(4\in ℂ\wedge 4\ne 0\right)$$
58	57	a1i	$$⊢K\in {\mathbb{N}}_0\to \left(4\in ℂ\wedge 4\ne 0\right)$$
59		divdir	$$⊢\left(8K\in ℂ\wedge 7\in ℂ\wedge \left(4\in ℂ\wedge 4\ne 0\right)\right)\to \frac{8K+7}{4}=\left(\frac{8K}{4}\right)+\left(\frac{7}{4}\right)$$
60	11 13 58 59	syl3anc	$$⊢K\in {\mathbb{N}}_0\to \frac{8K+7}{4}=\left(\frac{8K}{4}\right)+\left(\frac{7}{4}\right)$$
61		8cn	$$⊢8\in ℂ$$
62	61	a1i	$$⊢K\in {\mathbb{N}}_0\to 8\in ℂ$$
63		div23	$$⊢\left(8\in ℂ\wedge K\in ℂ\wedge \left(4\in ℂ\wedge 4\ne 0\right)\right)\to \frac{8K}{4}=\left(\frac{8}{4}\right)K$$
64	62 24 58 63	syl3anc	$$⊢K\in {\mathbb{N}}_0\to \frac{8K}{4}=\left(\frac{8}{4}\right)K$$
65	17	oveq1i	$$⊢\frac{8}{4}=\frac{4\cdot 2}{4}$$
66	22 20 56	divcan3i	$$⊢\frac{4\cdot 2}{4}=2$$
67	65 66	eqtri	$$⊢\frac{8}{4}=2$$
68	67	a1i	$$⊢K\in {\mathbb{N}}_0\to \frac{8}{4}=2$$
69	68	oveq1d	$$⊢K\in {\mathbb{N}}_0\to \left(\frac{8}{4}\right)K=2K$$
70	64 69	eqtrd	$$⊢K\in {\mathbb{N}}_0\to \frac{8K}{4}=2K$$
71	70	oveq1d	$$⊢K\in {\mathbb{N}}_0\to \left(\frac{8K}{4}\right)+\left(\frac{7}{4}\right)=2K+\left(\frac{7}{4}\right)$$
72	60 71	eqtrd	$$⊢K\in {\mathbb{N}}_0\to \frac{8K+7}{4}=2K+\left(\frac{7}{4}\right)$$
73	72	fveq2d	$$⊢K\in {\mathbb{N}}_0\to ⌊\frac{8K+7}{4}⌋=⌊2K+\left(\frac{7}{4}\right)⌋$$
74		3lt4	$$⊢3<4$$
75		2nn0	$$⊢2\in {\mathbb{N}}_0$$
76	75	a1i	$$⊢K\in {\mathbb{N}}_0\to 2\in {\mathbb{N}}_0$$
77	76 9	nn0mulcld	$$⊢K\in {\mathbb{N}}_0\to 2K\in {\mathbb{N}}_0$$
78	77	nn0zd	$$⊢K\in {\mathbb{N}}_0\to 2K\in \mathbb{Z}$$
79	78	peano2zd	$$⊢K\in {\mathbb{N}}_0\to 2K+1\in \mathbb{Z}$$
80		3nn0	$$⊢3\in {\mathbb{N}}_0$$
81	80	a1i	$$⊢K\in {\mathbb{N}}_0\to 3\in {\mathbb{N}}_0$$
82		4nn	$$⊢4\in \mathbb{N}$$
83	82	a1i	$$⊢K\in {\mathbb{N}}_0\to 4\in \mathbb{N}$$
84		adddivflid	$$⊢\left(2K+1\in \mathbb{Z}\wedge 3\in {\mathbb{N}}_0\wedge 4\in \mathbb{N}\right)\to \left(3<4\leftrightarrow ⌊2K+1+\left(\frac{3}{4}\right)⌋=2K+1\right)$$
85	79 81 83 84	syl3anc	$$⊢K\in {\mathbb{N}}_0\to \left(3<4\leftrightarrow ⌊2K+1+\left(\frac{3}{4}\right)⌋=2K+1\right)$$
86	23 24	mulcld	$$⊢K\in {\mathbb{N}}_0\to 2K\in ℂ$$
87	50	a1i	$$⊢K\in {\mathbb{N}}_0\to 3\in ℂ$$
88	56	a1i	$$⊢K\in {\mathbb{N}}_0\to 4\ne 0$$
89	87 21 88	divcld	$$⊢K\in {\mathbb{N}}_0\to \frac{3}{4}\in ℂ$$
90	86 14 89	addassd	$$⊢K\in {\mathbb{N}}_0\to 2K+1+\left(\frac{3}{4}\right)=2K+1+\left(\frac{3}{4}\right)$$
91		4p3e7	$$⊢4+3=7$$
92	91	eqcomi	$$⊢7=4+3$$
93	92	oveq1i	$$⊢\frac{7}{4}=\frac{4+3}{4}$$
94	20 50 20 56	divdiri	$$⊢\frac{4+3}{4}=\left(\frac{4}{4}\right)+\left(\frac{3}{4}\right)$$
95	20 56	dividi	$$⊢\frac{4}{4}=1$$
96	95	oveq1i	$$⊢\left(\frac{4}{4}\right)+\left(\frac{3}{4}\right)=1+\left(\frac{3}{4}\right)$$
97	93 94 96	3eqtri	$$⊢\frac{7}{4}=1+\left(\frac{3}{4}\right)$$
98	97	a1i	$$⊢K\in {\mathbb{N}}_0\to \frac{7}{4}=1+\left(\frac{3}{4}\right)$$
99	98	eqcomd	$$⊢K\in {\mathbb{N}}_0\to 1+\left(\frac{3}{4}\right)=\frac{7}{4}$$
100	99	oveq2d	$$⊢K\in {\mathbb{N}}_0\to 2K+1+\left(\frac{3}{4}\right)=2K+\left(\frac{7}{4}\right)$$
101	90 100	eqtrd	$$⊢K\in {\mathbb{N}}_0\to 2K+1+\left(\frac{3}{4}\right)=2K+\left(\frac{7}{4}\right)$$
102	101	fveqeq2d	$$⊢K\in {\mathbb{N}}_0\to \left(⌊2K+1+\left(\frac{3}{4}\right)⌋=2K+1\leftrightarrow ⌊2K+\left(\frac{7}{4}\right)⌋=2K+1\right)$$
103	85 102	bitrd	$$⊢K\in {\mathbb{N}}_0\to \left(3<4\leftrightarrow ⌊2K+\left(\frac{7}{4}\right)⌋=2K+1\right)$$
104	74 103	mpbii	$$⊢K\in {\mathbb{N}}_0\to ⌊2K+\left(\frac{7}{4}\right)⌋=2K+1$$
105	73 104	eqtrd	$$⊢K\in {\mathbb{N}}_0\to ⌊\frac{8K+7}{4}⌋=2K+1$$
106	55 105	oveq12d	$$⊢K\in {\mathbb{N}}_0\to \left(\frac{8K+7-1}{2}\right)-⌊\frac{8K+7}{4}⌋=4K+3-\left(2K+1\right)$$
107	77	nn0cnd	$$⊢K\in {\mathbb{N}}_0\to 2K\in ℂ$$
108	35 87 107 14	addsub4d	$$⊢K\in {\mathbb{N}}_0\to 4K+3-\left(2K+1\right)=\left(4K-2K\right)+3-1$$
109		2t2e4	$$⊢2\cdot 2=4$$
110	109	eqcomi	$$⊢4=2\cdot 2$$
111	110	a1i	$$⊢K\in {\mathbb{N}}_0\to 4=2\cdot 2$$
112	111	oveq1d	$$⊢K\in {\mathbb{N}}_0\to 4K=2\cdot 2K$$
113	23 23 24	mulassd	$$⊢K\in {\mathbb{N}}_0\to 2\cdot 2K=22K$$
114	112 113	eqtrd	$$⊢K\in {\mathbb{N}}_0\to 4K=22K$$
115	114	oveq1d	$$⊢K\in {\mathbb{N}}_0\to 4K-2K=22K-2K$$
116		2txmxeqx	$$⊢2K\in ℂ\to 22K-2K=2K$$
117	107 116	syl	$$⊢K\in {\mathbb{N}}_0\to 22K-2K=2K$$
118	115 117	eqtrd	$$⊢K\in {\mathbb{N}}_0\to 4K-2K=2K$$
119		3m1e2	$$⊢3-1=2$$
120	119	a1i	$$⊢K\in {\mathbb{N}}_0\to 3-1=2$$
121	118 120	oveq12d	$$⊢K\in {\mathbb{N}}_0\to \left(4K-2K\right)+3-1=2K+2$$
122	106 108 121	3eqtrd	$$⊢K\in {\mathbb{N}}_0\to \left(\frac{8K+7-1}{2}\right)-⌊\frac{8K+7}{4}⌋=2K+2$$
123	6 122	sylan9eqr	$$⊢\left(K\in {\mathbb{N}}_0\wedge P=8K+7\right)\to N=2K+2$$