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	syl5eq	$$⊢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		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 {\mathbb{N}}_0\to 8=2\cdot 4$$
21	20	oveq1d	$$⊢K\in {\mathbb{N}}_0\to 8K=2\cdot 4K$$
22	16	a1i	$$⊢K\in {\mathbb{N}}_0\to 2\in ℂ$$
23	15	a1i	$$⊢K\in {\mathbb{N}}_0\to 4\in ℂ$$
24		nn0cn	$$⊢K\in {\mathbb{N}}_0\to K\in ℂ$$
25	22 23 24	mulassd	$$⊢K\in {\mathbb{N}}_0\to 2\cdot 4K=24K$$
26	21 25	eqtrd	$$⊢K\in {\mathbb{N}}_0\to 8K=24K$$
27	26	oveq1d	$$⊢K\in {\mathbb{N}}_0\to \frac{8K}{2}=\frac{24K}{2}$$
28		4nn0	$$⊢4\in {\mathbb{N}}_0$$
29	28	a1i	$$⊢K\in {\mathbb{N}}_0\to 4\in {\mathbb{N}}_0$$
30	29 9	nn0mulcld	$$⊢K\in {\mathbb{N}}_0\to 4K\in {\mathbb{N}}_0$$
31	30	nn0cnd	$$⊢K\in {\mathbb{N}}_0\to 4K\in ℂ$$
32		2ne0	$$⊢2\ne 0$$
33	32	a1i	$$⊢K\in {\mathbb{N}}_0\to 2\ne 0$$
34	31 22 33	divcan3d	$$⊢K\in {\mathbb{N}}_0\to \frac{24K}{2}=4K$$
35	14 27 34	3eqtrd	$$⊢K\in {\mathbb{N}}_0\to \frac{8K+1-1}{2}=4K$$
36		1cnd	$$⊢K\in {\mathbb{N}}_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 {\mathbb{N}}_0\to \left(4\in ℂ\wedge 4\ne 0\right)$$
40		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)$$
41	11 36 39 40	syl3anc	$$⊢K\in {\mathbb{N}}_0\to \frac{8K+1}{4}=\left(\frac{8K}{4}\right)+\left(\frac{1}{4}\right)$$
42		8cn	$$⊢8\in ℂ$$
43	42	a1i	$$⊢K\in {\mathbb{N}}_0\to 8\in ℂ$$
44		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$$
45	43 24 39 44	syl3anc	$$⊢K\in {\mathbb{N}}_0\to \frac{8K}{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 {\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	45 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	41 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	35 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	22 22 24	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$$