Theorem 2lgslem3c

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

	Ref	Expression
Hypothesis	2lgslem2.n	⊢ 𝑁 = ( ( ( 𝑃 − 1 ) / 2 ) − ( ⌊ ‘ ( 𝑃 / 4 ) ) )
Assertion	2lgslem3c	⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑃 = ( ( 8 · 𝐾 ) + 5 ) ) → 𝑁 = ( ( 2 · 𝐾 ) + 1 ) )

Proof

Step	Hyp	Ref	Expression
1		2lgslem2.n	⊢ 𝑁 = ( ( ( 𝑃 − 1 ) / 2 ) − ( ⌊ ‘ ( 𝑃 / 4 ) ) )
2		oveq1	⊢ ( 𝑃 = ( ( 8 · 𝐾 ) + 5 ) → ( 𝑃 − 1 ) = ( ( ( 8 · 𝐾 ) + 5 ) − 1 ) )
3	2	oveq1d	⊢ ( 𝑃 = ( ( 8 · 𝐾 ) + 5 ) → ( ( 𝑃 − 1 ) / 2 ) = ( ( ( ( 8 · 𝐾 ) + 5 ) − 1 ) / 2 ) )
4		fvoveq1	⊢ ( 𝑃 = ( ( 8 · 𝐾 ) + 5 ) → ( ⌊ ‘ ( 𝑃 / 4 ) ) = ( ⌊ ‘ ( ( ( 8 · 𝐾 ) + 5 ) / 4 ) ) )
5	3 4	oveq12d	⊢ ( 𝑃 = ( ( 8 · 𝐾 ) + 5 ) → ( ( ( 𝑃 − 1 ) / 2 ) − ( ⌊ ‘ ( 𝑃 / 4 ) ) ) = ( ( ( ( ( 8 · 𝐾 ) + 5 ) − 1 ) / 2 ) − ( ⌊ ‘ ( ( ( 8 · 𝐾 ) + 5 ) / 4 ) ) ) )
6	1 5	eqtrid	⊢ ( 𝑃 = ( ( 8 · 𝐾 ) + 5 ) → 𝑁 = ( ( ( ( ( 8 · 𝐾 ) + 5 ) − 1 ) / 2 ) − ( ⌊ ‘ ( ( ( 8 · 𝐾 ) + 5 ) / 4 ) ) ) )
7		8nn0	⊢ 8 ∈ ℕ0
8	7	a1i	⊢ ( 𝐾 ∈ ℕ0 → 8 ∈ ℕ0 )
9		id	⊢ ( 𝐾 ∈ ℕ0 → 𝐾 ∈ ℕ0 )
10	8 9	nn0mulcld	⊢ ( 𝐾 ∈ ℕ0 → ( 8 · 𝐾 ) ∈ ℕ0 )
11	10	nn0cnd	⊢ ( 𝐾 ∈ ℕ0 → ( 8 · 𝐾 ) ∈ ℂ )
12		5cn	⊢ 5 ∈ ℂ
13	12	a1i	⊢ ( 𝐾 ∈ ℕ0 → 5 ∈ ℂ )
14		1cnd	⊢ ( 𝐾 ∈ ℕ0 → 1 ∈ ℂ )
15	11 13 14	addsubassd	⊢ ( 𝐾 ∈ ℕ0 → ( ( ( 8 · 𝐾 ) + 5 ) − 1 ) = ( ( 8 · 𝐾 ) + ( 5 − 1 ) ) )
16		4t2e8	⊢ ( 4 · 2 ) = 8
17	16	eqcomi	⊢ 8 = ( 4 · 2 )
18	17	a1i	⊢ ( 𝐾 ∈ ℕ0 → 8 = ( 4 · 2 ) )
19	18	oveq1d	⊢ ( 𝐾 ∈ ℕ0 → ( 8 · 𝐾 ) = ( ( 4 · 2 ) · 𝐾 ) )
20		4cn	⊢ 4 ∈ ℂ
21	20	a1i	⊢ ( 𝐾 ∈ ℕ0 → 4 ∈ ℂ )
22		2cn	⊢ 2 ∈ ℂ
23	22	a1i	⊢ ( 𝐾 ∈ ℕ0 → 2 ∈ ℂ )
24		nn0cn	⊢ ( 𝐾 ∈ ℕ0 → 𝐾 ∈ ℂ )
25	21 23 24	mul32d	⊢ ( 𝐾 ∈ ℕ0 → ( ( 4 · 2 ) · 𝐾 ) = ( ( 4 · 𝐾 ) · 2 ) )
26	19 25	eqtrd	⊢ ( 𝐾 ∈ ℕ0 → ( 8 · 𝐾 ) = ( ( 4 · 𝐾 ) · 2 ) )
27		5m1e4	⊢ ( 5 − 1 ) = 4
28	27	a1i	⊢ ( 𝐾 ∈ ℕ0 → ( 5 − 1 ) = 4 )
29	26 28	oveq12d	⊢ ( 𝐾 ∈ ℕ0 → ( ( 8 · 𝐾 ) + ( 5 − 1 ) ) = ( ( ( 4 · 𝐾 ) · 2 ) + 4 ) )
30	15 29	eqtrd	⊢ ( 𝐾 ∈ ℕ0 → ( ( ( 8 · 𝐾 ) + 5 ) − 1 ) = ( ( ( 4 · 𝐾 ) · 2 ) + 4 ) )
31	30	oveq1d	⊢ ( 𝐾 ∈ ℕ0 → ( ( ( ( 8 · 𝐾 ) + 5 ) − 1 ) / 2 ) = ( ( ( ( 4 · 𝐾 ) · 2 ) + 4 ) / 2 ) )
32		4nn0	⊢ 4 ∈ ℕ0
33	32	a1i	⊢ ( 𝐾 ∈ ℕ0 → 4 ∈ ℕ0 )
34	33 9	nn0mulcld	⊢ ( 𝐾 ∈ ℕ0 → ( 4 · 𝐾 ) ∈ ℕ0 )
35	34	nn0cnd	⊢ ( 𝐾 ∈ ℕ0 → ( 4 · 𝐾 ) ∈ ℂ )
36	35 23	mulcld	⊢ ( 𝐾 ∈ ℕ0 → ( ( 4 · 𝐾 ) · 2 ) ∈ ℂ )
37		2rp	⊢ 2 ∈ ℝ+
38	37	a1i	⊢ ( 𝐾 ∈ ℕ0 → 2 ∈ ℝ+ )
39	38	rpcnne0d	⊢ ( 𝐾 ∈ ℕ0 → ( 2 ∈ ℂ ∧ 2 ≠ 0 ) )
40		divdir	⊢ ( ( ( ( 4 · 𝐾 ) · 2 ) ∈ ℂ ∧ 4 ∈ ℂ ∧ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ) → ( ( ( ( 4 · 𝐾 ) · 2 ) + 4 ) / 2 ) = ( ( ( ( 4 · 𝐾 ) · 2 ) / 2 ) + ( 4 / 2 ) ) )
41	36 21 39 40	syl3anc	⊢ ( 𝐾 ∈ ℕ0 → ( ( ( ( 4 · 𝐾 ) · 2 ) + 4 ) / 2 ) = ( ( ( ( 4 · 𝐾 ) · 2 ) / 2 ) + ( 4 / 2 ) ) )
42		2ne0	⊢ 2 ≠ 0
43	42	a1i	⊢ ( 𝐾 ∈ ℕ0 → 2 ≠ 0 )
44	35 23 43	divcan4d	⊢ ( 𝐾 ∈ ℕ0 → ( ( ( 4 · 𝐾 ) · 2 ) / 2 ) = ( 4 · 𝐾 ) )
45		4d2e2	⊢ ( 4 / 2 ) = 2
46	45	a1i	⊢ ( 𝐾 ∈ ℕ0 → ( 4 / 2 ) = 2 )
47	44 46	oveq12d	⊢ ( 𝐾 ∈ ℕ0 → ( ( ( ( 4 · 𝐾 ) · 2 ) / 2 ) + ( 4 / 2 ) ) = ( ( 4 · 𝐾 ) + 2 ) )
48	31 41 47	3eqtrd	⊢ ( 𝐾 ∈ ℕ0 → ( ( ( ( 8 · 𝐾 ) + 5 ) − 1 ) / 2 ) = ( ( 4 · 𝐾 ) + 2 ) )
49		4ne0	⊢ 4 ≠ 0
50	20 49	pm3.2i	⊢ ( 4 ∈ ℂ ∧ 4 ≠ 0 )
51	50	a1i	⊢ ( 𝐾 ∈ ℕ0 → ( 4 ∈ ℂ ∧ 4 ≠ 0 ) )
52		divdir	⊢ ( ( ( 8 · 𝐾 ) ∈ ℂ ∧ 5 ∈ ℂ ∧ ( 4 ∈ ℂ ∧ 4 ≠ 0 ) ) → ( ( ( 8 · 𝐾 ) + 5 ) / 4 ) = ( ( ( 8 · 𝐾 ) / 4 ) + ( 5 / 4 ) ) )
53	11 13 51 52	syl3anc	⊢ ( 𝐾 ∈ ℕ0 → ( ( ( 8 · 𝐾 ) + 5 ) / 4 ) = ( ( ( 8 · 𝐾 ) / 4 ) + ( 5 / 4 ) ) )
54		8cn	⊢ 8 ∈ ℂ
55	54	a1i	⊢ ( 𝐾 ∈ ℕ0 → 8 ∈ ℂ )
56		div23	⊢ ( ( 8 ∈ ℂ ∧ 𝐾 ∈ ℂ ∧ ( 4 ∈ ℂ ∧ 4 ≠ 0 ) ) → ( ( 8 · 𝐾 ) / 4 ) = ( ( 8 / 4 ) · 𝐾 ) )
57	55 24 51 56	syl3anc	⊢ ( 𝐾 ∈ ℕ0 → ( ( 8 · 𝐾 ) / 4 ) = ( ( 8 / 4 ) · 𝐾 ) )
58	17	oveq1i	⊢ ( 8 / 4 ) = ( ( 4 · 2 ) / 4 )
59	22 20 49	divcan3i	⊢ ( ( 4 · 2 ) / 4 ) = 2
60	58 59	eqtri	⊢ ( 8 / 4 ) = 2
61	60	a1i	⊢ ( 𝐾 ∈ ℕ0 → ( 8 / 4 ) = 2 )
62	61	oveq1d	⊢ ( 𝐾 ∈ ℕ0 → ( ( 8 / 4 ) · 𝐾 ) = ( 2 · 𝐾 ) )
63	57 62	eqtrd	⊢ ( 𝐾 ∈ ℕ0 → ( ( 8 · 𝐾 ) / 4 ) = ( 2 · 𝐾 ) )
64	63	oveq1d	⊢ ( 𝐾 ∈ ℕ0 → ( ( ( 8 · 𝐾 ) / 4 ) + ( 5 / 4 ) ) = ( ( 2 · 𝐾 ) + ( 5 / 4 ) ) )
65	53 64	eqtrd	⊢ ( 𝐾 ∈ ℕ0 → ( ( ( 8 · 𝐾 ) + 5 ) / 4 ) = ( ( 2 · 𝐾 ) + ( 5 / 4 ) ) )
66	65	fveq2d	⊢ ( 𝐾 ∈ ℕ0 → ( ⌊ ‘ ( ( ( 8 · 𝐾 ) + 5 ) / 4 ) ) = ( ⌊ ‘ ( ( 2 · 𝐾 ) + ( 5 / 4 ) ) ) )
67		1lt4	⊢ 1 < 4
68		2nn0	⊢ 2 ∈ ℕ0
69	68	a1i	⊢ ( 𝐾 ∈ ℕ0 → 2 ∈ ℕ0 )
70	69 9	nn0mulcld	⊢ ( 𝐾 ∈ ℕ0 → ( 2 · 𝐾 ) ∈ ℕ0 )
71	70	nn0zd	⊢ ( 𝐾 ∈ ℕ0 → ( 2 · 𝐾 ) ∈ ℤ )
72	71	peano2zd	⊢ ( 𝐾 ∈ ℕ0 → ( ( 2 · 𝐾 ) + 1 ) ∈ ℤ )
73		1nn0	⊢ 1 ∈ ℕ0
74	73	a1i	⊢ ( 𝐾 ∈ ℕ0 → 1 ∈ ℕ0 )
75		4nn	⊢ 4 ∈ ℕ
76	75	a1i	⊢ ( 𝐾 ∈ ℕ0 → 4 ∈ ℕ )
77		adddivflid	⊢ ( ( ( ( 2 · 𝐾 ) + 1 ) ∈ ℤ ∧ 1 ∈ ℕ0 ∧ 4 ∈ ℕ ) → ( 1 < 4 ↔ ( ⌊ ‘ ( ( ( 2 · 𝐾 ) + 1 ) + ( 1 / 4 ) ) ) = ( ( 2 · 𝐾 ) + 1 ) ) )
78	72 74 76 77	syl3anc	⊢ ( 𝐾 ∈ ℕ0 → ( 1 < 4 ↔ ( ⌊ ‘ ( ( ( 2 · 𝐾 ) + 1 ) + ( 1 / 4 ) ) ) = ( ( 2 · 𝐾 ) + 1 ) ) )
79	23 24	mulcld	⊢ ( 𝐾 ∈ ℕ0 → ( 2 · 𝐾 ) ∈ ℂ )
80	49	a1i	⊢ ( 𝐾 ∈ ℕ0 → 4 ≠ 0 )
81	21 80	reccld	⊢ ( 𝐾 ∈ ℕ0 → ( 1 / 4 ) ∈ ℂ )
82	79 14 81	addassd	⊢ ( 𝐾 ∈ ℕ0 → ( ( ( 2 · 𝐾 ) + 1 ) + ( 1 / 4 ) ) = ( ( 2 · 𝐾 ) + ( 1 + ( 1 / 4 ) ) ) )
83		df-5	⊢ 5 = ( 4 + 1 )
84	83	oveq1i	⊢ ( 5 / 4 ) = ( ( 4 + 1 ) / 4 )
85		ax-1cn	⊢ 1 ∈ ℂ
86	20 85 20 49	divdiri	⊢ ( ( 4 + 1 ) / 4 ) = ( ( 4 / 4 ) + ( 1 / 4 ) )
87	20 49	dividi	⊢ ( 4 / 4 ) = 1
88	87	oveq1i	⊢ ( ( 4 / 4 ) + ( 1 / 4 ) ) = ( 1 + ( 1 / 4 ) )
89	84 86 88	3eqtri	⊢ ( 5 / 4 ) = ( 1 + ( 1 / 4 ) )
90	89	a1i	⊢ ( 𝐾 ∈ ℕ0 → ( 5 / 4 ) = ( 1 + ( 1 / 4 ) ) )
91	90	eqcomd	⊢ ( 𝐾 ∈ ℕ0 → ( 1 + ( 1 / 4 ) ) = ( 5 / 4 ) )
92	91	oveq2d	⊢ ( 𝐾 ∈ ℕ0 → ( ( 2 · 𝐾 ) + ( 1 + ( 1 / 4 ) ) ) = ( ( 2 · 𝐾 ) + ( 5 / 4 ) ) )
93	82 92	eqtrd	⊢ ( 𝐾 ∈ ℕ0 → ( ( ( 2 · 𝐾 ) + 1 ) + ( 1 / 4 ) ) = ( ( 2 · 𝐾 ) + ( 5 / 4 ) ) )
94	93	fveqeq2d	⊢ ( 𝐾 ∈ ℕ0 → ( ( ⌊ ‘ ( ( ( 2 · 𝐾 ) + 1 ) + ( 1 / 4 ) ) ) = ( ( 2 · 𝐾 ) + 1 ) ↔ ( ⌊ ‘ ( ( 2 · 𝐾 ) + ( 5 / 4 ) ) ) = ( ( 2 · 𝐾 ) + 1 ) ) )
95	78 94	bitrd	⊢ ( 𝐾 ∈ ℕ0 → ( 1 < 4 ↔ ( ⌊ ‘ ( ( 2 · 𝐾 ) + ( 5 / 4 ) ) ) = ( ( 2 · 𝐾 ) + 1 ) ) )
96	67 95	mpbii	⊢ ( 𝐾 ∈ ℕ0 → ( ⌊ ‘ ( ( 2 · 𝐾 ) + ( 5 / 4 ) ) ) = ( ( 2 · 𝐾 ) + 1 ) )
97	66 96	eqtrd	⊢ ( 𝐾 ∈ ℕ0 → ( ⌊ ‘ ( ( ( 8 · 𝐾 ) + 5 ) / 4 ) ) = ( ( 2 · 𝐾 ) + 1 ) )
98	48 97	oveq12d	⊢ ( 𝐾 ∈ ℕ0 → ( ( ( ( ( 8 · 𝐾 ) + 5 ) − 1 ) / 2 ) − ( ⌊ ‘ ( ( ( 8 · 𝐾 ) + 5 ) / 4 ) ) ) = ( ( ( 4 · 𝐾 ) + 2 ) − ( ( 2 · 𝐾 ) + 1 ) ) )
99	70	nn0cnd	⊢ ( 𝐾 ∈ ℕ0 → ( 2 · 𝐾 ) ∈ ℂ )
100	35 23 99 14	addsub4d	⊢ ( 𝐾 ∈ ℕ0 → ( ( ( 4 · 𝐾 ) + 2 ) − ( ( 2 · 𝐾 ) + 1 ) ) = ( ( ( 4 · 𝐾 ) − ( 2 · 𝐾 ) ) + ( 2 − 1 ) ) )
101		2t2e4	⊢ ( 2 · 2 ) = 4
102	101	eqcomi	⊢ 4 = ( 2 · 2 )
103	102	a1i	⊢ ( 𝐾 ∈ ℕ0 → 4 = ( 2 · 2 ) )
104	103	oveq1d	⊢ ( 𝐾 ∈ ℕ0 → ( 4 · 𝐾 ) = ( ( 2 · 2 ) · 𝐾 ) )
105	23 23 24	mulassd	⊢ ( 𝐾 ∈ ℕ0 → ( ( 2 · 2 ) · 𝐾 ) = ( 2 · ( 2 · 𝐾 ) ) )
106	104 105	eqtrd	⊢ ( 𝐾 ∈ ℕ0 → ( 4 · 𝐾 ) = ( 2 · ( 2 · 𝐾 ) ) )
107	106	oveq1d	⊢ ( 𝐾 ∈ ℕ0 → ( ( 4 · 𝐾 ) − ( 2 · 𝐾 ) ) = ( ( 2 · ( 2 · 𝐾 ) ) − ( 2 · 𝐾 ) ) )
108		2txmxeqx	⊢ ( ( 2 · 𝐾 ) ∈ ℂ → ( ( 2 · ( 2 · 𝐾 ) ) − ( 2 · 𝐾 ) ) = ( 2 · 𝐾 ) )
109	99 108	syl	⊢ ( 𝐾 ∈ ℕ0 → ( ( 2 · ( 2 · 𝐾 ) ) − ( 2 · 𝐾 ) ) = ( 2 · 𝐾 ) )
110	107 109	eqtrd	⊢ ( 𝐾 ∈ ℕ0 → ( ( 4 · 𝐾 ) − ( 2 · 𝐾 ) ) = ( 2 · 𝐾 ) )
111		2m1e1	⊢ ( 2 − 1 ) = 1
112	111	a1i	⊢ ( 𝐾 ∈ ℕ0 → ( 2 − 1 ) = 1 )
113	110 112	oveq12d	⊢ ( 𝐾 ∈ ℕ0 → ( ( ( 4 · 𝐾 ) − ( 2 · 𝐾 ) ) + ( 2 − 1 ) ) = ( ( 2 · 𝐾 ) + 1 ) )
114	98 100 113	3eqtrd	⊢ ( 𝐾 ∈ ℕ0 → ( ( ( ( ( 8 · 𝐾 ) + 5 ) − 1 ) / 2 ) − ( ⌊ ‘ ( ( ( 8 · 𝐾 ) + 5 ) / 4 ) ) ) = ( ( 2 · 𝐾 ) + 1 ) )
115	6 114	sylan9eqr	⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑃 = ( ( 8 · 𝐾 ) + 5 ) ) → 𝑁 = ( ( 2 · 𝐾 ) + 1 ) )