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 {\mathbb{N}}_0\wedge P=8K+1\right)\to N=2K$$

Proof

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