Theorem 2lgslem3d

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

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

Proof

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