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