Theorem 2lgslem3b

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

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

Proof

Step	Hyp	Ref	Expression
1		2lgslem2.n	$$⊢N=\left(\frac{P-1}{2}\right)-⌊\frac{P}{4}⌋$$
2		oveq1	$$⊢P=8K+3\to P-1=8K+3-1$$
3	2	oveq1d	$$⊢P=8K+3\to \frac{P-1}{2}=\frac{8K+3-1}{2}$$
4		fvoveq1	$$⊢P=8K+3\to ⌊\frac{P}{4}⌋=⌊\frac{8K+3}{4}⌋$$
5	3 4	oveq12d	$$⊢P=8K+3\to \left(\frac{P-1}{2}\right)-⌊\frac{P}{4}⌋=\left(\frac{8K+3-1}{2}\right)-⌊\frac{8K+3}{4}⌋$$
6	1 5	syl5eq	$$⊢P=8K+3\to N=\left(\frac{8K+3-1}{2}\right)-⌊\frac{8K+3}{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		3cn	$$⊢3\in ℂ$$
13	12	a1i	$$⊢K\in {\mathbb{N}}_0\to 3\in ℂ$$
14		1cnd	$$⊢K\in {\mathbb{N}}_0\to 1\in ℂ$$
15	11 13 14	addsubassd	$$⊢K\in {\mathbb{N}}_0\to 8K+3-1=8K+3-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		3m1e2	$$⊢3-1=2$$
28	27	a1i	$$⊢K\in {\mathbb{N}}_0\to 3-1=2$$
29	26 28	oveq12d	$$⊢K\in {\mathbb{N}}_0\to 8K+3-1=4K\cdot 2+2$$
30	15 29	eqtrd	$$⊢K\in {\mathbb{N}}_0\to 8K+3-1=4K\cdot 2+2$$
31	30	oveq1d	$$⊢K\in {\mathbb{N}}_0\to \frac{8K+3-1}{2}=\frac{4K\cdot 2+2}{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		2rp	$$⊢2\in {ℝ}^{+}$$
38	37	a1i	$$⊢K\in {\mathbb{N}}_0\to 2\in {ℝ}^{+}$$
39	38	rpcnne0d	$$⊢K\in {\mathbb{N}}_0\to \left(2\in ℂ\wedge 2\ne 0\right)$$
40		divdir	$$⊢\left(4K\cdot 2\in ℂ\wedge 2\in ℂ\wedge \left(2\in ℂ\wedge 2\ne 0\right)\right)\to \frac{4K\cdot 2+2}{2}=\left(\frac{4K\cdot 2}{2}\right)+\left(\frac{2}{2}\right)$$
41	36 23 39 40	syl3anc	$$⊢K\in {\mathbb{N}}_0\to \frac{4K\cdot 2+2}{2}=\left(\frac{4K\cdot 2}{2}\right)+\left(\frac{2}{2}\right)$$
42		2ne0	$$⊢2\ne 0$$
43	42	a1i	$$⊢K\in {\mathbb{N}}_0\to 2\ne 0$$
44	35 23 43	divcan4d	$$⊢K\in {\mathbb{N}}_0\to \frac{4K\cdot 2}{2}=4K$$
45		2div2e1	$$⊢\frac{2}{2}=1$$
46	45	a1i	$$⊢K\in {\mathbb{N}}_0\to \frac{2}{2}=1$$
47	44 46	oveq12d	$$⊢K\in {\mathbb{N}}_0\to \left(\frac{4K\cdot 2}{2}\right)+\left(\frac{2}{2}\right)=4K+1$$
48	31 41 47	3eqtrd	$$⊢K\in {\mathbb{N}}_0\to \frac{8K+3-1}{2}=4K+1$$
49		4ne0	$$⊢4\ne 0$$
50	20 49	pm3.2i	$$⊢\left(4\in ℂ\wedge 4\ne 0\right)$$
51	50	a1i	$$⊢K\in {\mathbb{N}}_0\to \left(4\in ℂ\wedge 4\ne 0\right)$$
52		divdir	$$⊢\left(8K\in ℂ\wedge 3\in ℂ\wedge \left(4\in ℂ\wedge 4\ne 0\right)\right)\to \frac{8K+3}{4}=\left(\frac{8K}{4}\right)+\left(\frac{3}{4}\right)$$
53	11 13 51 52	syl3anc	$$⊢K\in {\mathbb{N}}_0\to \frac{8K+3}{4}=\left(\frac{8K}{4}\right)+\left(\frac{3}{4}\right)$$
54		8cn	$$⊢8\in ℂ$$
55	54	a1i	$$⊢K\in {\mathbb{N}}_0\to 8\in ℂ$$
56		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$$
57	55 24 51 56	syl3anc	$$⊢K\in {\mathbb{N}}_0\to \frac{8K}{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 {\mathbb{N}}_0\to \frac{8}{4}=2$$
62	61	oveq1d	$$⊢K\in {\mathbb{N}}_0\to \left(\frac{8}{4}\right)K=2K$$
63	57 62	eqtrd	$$⊢K\in {\mathbb{N}}_0\to \frac{8K}{4}=2K$$
64	63	oveq1d	$$⊢K\in {\mathbb{N}}_0\to \left(\frac{8K}{4}\right)+\left(\frac{3}{4}\right)=2K+\left(\frac{3}{4}\right)$$
65	53 64	eqtrd	$$⊢K\in {\mathbb{N}}_0\to \frac{8K+3}{4}=2K+\left(\frac{3}{4}\right)$$
66	65	fveq2d	$$⊢K\in {\mathbb{N}}_0\to ⌊\frac{8K+3}{4}⌋=⌊2K+\left(\frac{3}{4}\right)⌋$$
67		3lt4	$$⊢3<4$$
68		2nn0	$$⊢2\in {\mathbb{N}}_0$$
69	68	a1i	$$⊢K\in {\mathbb{N}}_0\to 2\in {\mathbb{N}}_0$$
70	69 9	nn0mulcld	$$⊢K\in {\mathbb{N}}_0\to 2K\in {\mathbb{N}}_0$$
71	70	nn0zd	$$⊢K\in {\mathbb{N}}_0\to 2K\in \mathbb{Z}$$
72		3nn0	$$⊢3\in {\mathbb{N}}_0$$
73	72	a1i	$$⊢K\in {\mathbb{N}}_0\to 3\in {\mathbb{N}}_0$$
74		4nn	$$⊢4\in \mathbb{N}$$
75	74	a1i	$$⊢K\in {\mathbb{N}}_0\to 4\in \mathbb{N}$$
76		adddivflid	$$⊢\left(2K\in \mathbb{Z}\wedge 3\in {\mathbb{N}}_0\wedge 4\in \mathbb{N}\right)\to \left(3<4\leftrightarrow ⌊2K+\left(\frac{3}{4}\right)⌋=2K\right)$$
77	71 73 75 76	syl3anc	$$⊢K\in {\mathbb{N}}_0\to \left(3<4\leftrightarrow ⌊2K+\left(\frac{3}{4}\right)⌋=2K\right)$$
78	67 77	mpbii	$$⊢K\in {\mathbb{N}}_0\to ⌊2K+\left(\frac{3}{4}\right)⌋=2K$$
79	66 78	eqtrd	$$⊢K\in {\mathbb{N}}_0\to ⌊\frac{8K+3}{4}⌋=2K$$
80	48 79	oveq12d	$$⊢K\in {\mathbb{N}}_0\to \left(\frac{8K+3-1}{2}\right)-⌊\frac{8K+3}{4}⌋=4K+1-2K$$
81	70	nn0cnd	$$⊢K\in {\mathbb{N}}_0\to 2K\in ℂ$$
82	35 14 81	addsubd	$$⊢K\in {\mathbb{N}}_0\to 4K+1-2K=4K-2K+1$$
83		2t2e4	$$⊢2\cdot 2=4$$
84	83	eqcomi	$$⊢4=2\cdot 2$$
85	84	a1i	$$⊢K\in {\mathbb{N}}_0\to 4=2\cdot 2$$
86	85	oveq1d	$$⊢K\in {\mathbb{N}}_0\to 4K=2\cdot 2K$$
87	23 23 24	mulassd	$$⊢K\in {\mathbb{N}}_0\to 2\cdot 2K=22K$$
88	86 87	eqtrd	$$⊢K\in {\mathbb{N}}_0\to 4K=22K$$
89	88	oveq1d	$$⊢K\in {\mathbb{N}}_0\to 4K-2K=22K-2K$$
90		2txmxeqx	$$⊢2K\in ℂ\to 22K-2K=2K$$
91	81 90	syl	$$⊢K\in {\mathbb{N}}_0\to 22K-2K=2K$$
92	89 91	eqtrd	$$⊢K\in {\mathbb{N}}_0\to 4K-2K=2K$$
93	92	oveq1d	$$⊢K\in {\mathbb{N}}_0\to 4K-2K+1=2K+1$$
94	80 82 93	3eqtrd	$$⊢K\in {\mathbb{N}}_0\to \left(\frac{8K+3-1}{2}\right)-⌊\frac{8K+3}{4}⌋=2K+1$$
95	6 94	sylan9eqr	$$⊢\left(K\in {\mathbb{N}}_0\wedge P=8K+3\right)\to N=2K+1$$