Theorem 2lgslem3c 15853

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

Hypothesis

Ref	Expression
2lgslem2.n	|- N = ( ( ( P - 1 ) / 2 ) - ( |_ ` ( P / 4 ) ) )

Assertion

Ref	Expression
2lgslem3c	|- ( ( K e. NN0 /\ P = ( ( 8 x. K ) + 5 ) ) -> N = ( ( 2 x. K ) + 1 ) )

Proof of Theorem 2lgslem3c

Step	Hyp	Ref	Expression
1		2lgslem2.n	. . 3 |- N = ( ( ( P - 1 ) / 2 ) - ( |_ ` ( P / 4 ) ) )
2		oveq1 6030	. . . . 5 |- ( P = ( ( 8 x. K ) + 5 ) -> ( P - 1 ) = ( ( ( 8 x. K ) + 5 ) - 1 ) )
3	2	oveq1d 6038	. . . 4 |- ( P = ( ( 8 x. K ) + 5 ) -> ( ( P - 1 ) / 2 ) = ( ( ( ( 8 x. K ) + 5 ) - 1 ) / 2 ) )
4		fvoveq1 6046	. . . 4 |- ( P = ( ( 8 x. K ) + 5 ) -> ( |_ ` ( P / 4 ) ) = ( |_ ` ( ( ( 8 x. K ) + 5 ) / 4 ) ) )
5	3, 4	oveq12d 6041	. . 3 |- ( P = ( ( 8 x. K ) + 5 ) -> ( ( ( P - 1 ) / 2 ) - ( |_ ` ( P / 4 ) ) ) = ( ( ( ( ( 8 x. K ) + 5 ) - 1 ) / 2 ) - ( |_ ` ( ( ( 8 x. K ) + 5 ) / 4 ) ) ) )
6	1, 5	eqtrid 2275	. 2 |- ( P = ( ( 8 x. K ) + 5 ) -> N = ( ( ( ( ( 8 x. K ) + 5 ) - 1 ) / 2 ) - ( |_ ` ( ( ( 8 x. K ) + 5 ) / 4 ) ) ) )
7		8nn0 9430	. . . . . . . . . . 11 |- 8 e. NN0
8	7	a1i 9	. . . . . . . . . 10 |- ( K e. NN0 -> 8 e. NN0 )
9		id 19	. . . . . . . . . 10 |- ( K e. NN0 -> K e. NN0 )
10	8, 9	nn0mulcld 9465	. . . . . . . . 9 |- ( K e. NN0 -> ( 8 x. K ) e. NN0 )
11	10	nn0cnd 9462	. . . . . . . 8 |- ( K e. NN0 -> ( 8 x. K ) e. CC )
12		5cn 9228	. . . . . . . . 9 |- 5 e. CC
13	12	a1i 9	. . . . . . . 8 |- ( K e. NN0 -> 5 e. CC )
14		1cnd 8200	. . . . . . . 8 |- ( K e. NN0 -> 1 e. CC )
15	11, 13, 14	addsubassd 8515	. . . . . . 7 |- ( K e. NN0 -> ( ( ( 8 x. K ) + 5 ) - 1 ) = ( ( 8 x. K ) + ( 5 - 1 ) ) )
16		4t2e8 9307	. . . . . . . . . . . 12 |- ( 4 x. 2 ) = 8
17	16	eqcomi 2234	. . . . . . . . . . 11 |- 8 = ( 4 x. 2 )
18	17	a1i 9	. . . . . . . . . 10 |- ( K e. NN0 -> 8 = ( 4 x. 2 ) )
19	18	oveq1d 6038	. . . . . . . . 9 |- ( K e. NN0 -> ( 8 x. K ) = ( ( 4 x. 2 ) x. K ) )
20		4cn 9226	. . . . . . . . . . 11 |- 4 e. CC
21	20	a1i 9	. . . . . . . . . 10 |- ( K e. NN0 -> 4 e. CC )
22		2cn 9219	. . . . . . . . . . 11 |- 2 e. CC
23	22	a1i 9	. . . . . . . . . 10 |- ( K e. NN0 -> 2 e. CC )
24		nn0cn 9417	. . . . . . . . . 10 |- ( K e. NN0 -> K e. CC )
25	21, 23, 24	mul32d 8337	. . . . . . . . 9 |- ( K e. NN0 -> ( ( 4 x. 2 ) x. K ) = ( ( 4 x. K ) x. 2 ) )
26	19, 25	eqtrd 2263	. . . . . . . 8 |- ( K e. NN0 -> ( 8 x. K ) = ( ( 4 x. K ) x. 2 ) )
27		5m1e4 9270	. . . . . . . . 9 |- ( 5 - 1 ) = 4
28	27	a1i 9	. . . . . . . 8 |- ( K e. NN0 -> ( 5 - 1 ) = 4 )
29	26, 28	oveq12d 6041	. . . . . . 7 |- ( K e. NN0 -> ( ( 8 x. K ) + ( 5 - 1 ) ) = ( ( ( 4 x. K ) x. 2 ) + 4 ) )
30	15, 29	eqtrd 2263	. . . . . 6 |- ( K e. NN0 -> ( ( ( 8 x. K ) + 5 ) - 1 ) = ( ( ( 4 x. K ) x. 2 ) + 4 ) )
31	30	oveq1d 6038	. . . . 5 |- ( K e. NN0 -> ( ( ( ( 8 x. K ) + 5 ) - 1 ) / 2 ) = ( ( ( ( 4 x. K ) x. 2 ) + 4 ) / 2 ) )
32		4nn0 9426	. . . . . . . . . 10 |- 4 e. NN0
33	32	a1i 9	. . . . . . . . 9 |- ( K e. NN0 -> 4 e. NN0 )
34	33, 9	nn0mulcld 9465	. . . . . . . 8 |- ( K e. NN0 -> ( 4 x. K ) e. NN0 )
35	34	nn0cnd 9462	. . . . . . 7 |- ( K e. NN0 -> ( 4 x. K ) e. CC )
36	35, 23	mulcld 8205	. . . . . 6 |- ( K e. NN0 -> ( ( 4 x. K ) x. 2 ) e. CC )
37		2rp 9898	. . . . . . . 8 |- 2 e. RR+
38	37	a1i 9	. . . . . . 7 |- ( K e. NN0 -> 2 e. RR+ )
39	38	rpap0d 9942	. . . . . 6 |- ( K e. NN0 -> 2 # 0 )
40	36, 21, 23, 39	divdirapd 9014	. . . . 5 |- ( K e. NN0 -> ( ( ( ( 4 x. K ) x. 2 ) + 4 ) / 2 ) = ( ( ( ( 4 x. K ) x. 2 ) / 2 ) + ( 4 / 2 ) ) )
41	35, 23, 39	divcanap4d 8981	. . . . . 6 |- ( K e. NN0 -> ( ( ( 4 x. K ) x. 2 ) / 2 ) = ( 4 x. K ) )
42		4d2e2 9309	. . . . . . 7 |- ( 4 / 2 ) = 2
43	42	a1i 9	. . . . . 6 |- ( K e. NN0 -> ( 4 / 2 ) = 2 )
44	41, 43	oveq12d 6041	. . . . 5 |- ( K e. NN0 -> ( ( ( ( 4 x. K ) x. 2 ) / 2 ) + ( 4 / 2 ) ) = ( ( 4 x. K ) + 2 ) )
45	31, 40, 44	3eqtrd 2267	. . . 4 |- ( K e. NN0 -> ( ( ( ( 8 x. K ) + 5 ) - 1 ) / 2 ) = ( ( 4 x. K ) + 2 ) )
46		4ap0 9247	. . . . . . . . 9 |- 4 # 0
47	46	a1i 9	. . . . . . . 8 |- ( K e. NN0 -> 4 # 0 )
48	11, 13, 21, 47	divdirapd 9014	. . . . . . 7 |- ( K e. NN0 -> ( ( ( 8 x. K ) + 5 ) / 4 ) = ( ( ( 8 x. K ) / 4 ) + ( 5 / 4 ) ) )
49		8cn 9234	. . . . . . . . . . 11 |- 8 e. CC
50	49	a1i 9	. . . . . . . . . 10 |- ( K e. NN0 -> 8 e. CC )
51	50, 24, 21, 47	div23apd 9013	. . . . . . . . 9 |- ( K e. NN0 -> ( ( 8 x. K ) / 4 ) = ( ( 8 / 4 ) x. K ) )
52	17	oveq1i 6033	. . . . . . . . . . . 12 |- ( 8 / 4 ) = ( ( 4 x. 2 ) / 4 )
53	22, 20, 46	divcanap3i 8943	. . . . . . . . . . . 12 |- ( ( 4 x. 2 ) / 4 ) = 2
54	52, 53	eqtri 2251	. . . . . . . . . . 11 |- ( 8 / 4 ) = 2
55	54	a1i 9	. . . . . . . . . 10 |- ( K e. NN0 -> ( 8 / 4 ) = 2 )
56	55	oveq1d 6038	. . . . . . . . 9 |- ( K e. NN0 -> ( ( 8 / 4 ) x. K ) = ( 2 x. K ) )
57	51, 56	eqtrd 2263	. . . . . . . 8 |- ( K e. NN0 -> ( ( 8 x. K ) / 4 ) = ( 2 x. K ) )
58	57	oveq1d 6038	. . . . . . 7 |- ( K e. NN0 -> ( ( ( 8 x. K ) / 4 ) + ( 5 / 4 ) ) = ( ( 2 x. K ) + ( 5 / 4 ) ) )
59	48, 58	eqtrd 2263	. . . . . 6 |- ( K e. NN0 -> ( ( ( 8 x. K ) + 5 ) / 4 ) = ( ( 2 x. K ) + ( 5 / 4 ) ) )
60	59	fveq2d 5646	. . . . 5 |- ( K e. NN0 -> ( |_ ` ( ( ( 8 x. K ) + 5 ) / 4 ) ) = ( |_ ` ( ( 2 x. K ) + ( 5 / 4 ) ) ) )
61		1lt4 9323	. . . . . 6 |- 1 < 4
62		2nn0 9424	. . . . . . . . . . . 12 |- 2 e. NN0
63	62	a1i 9	. . . . . . . . . . 11 |- ( K e. NN0 -> 2 e. NN0 )
64	63, 9	nn0mulcld 9465	. . . . . . . . . 10 |- ( K e. NN0 -> ( 2 x. K ) e. NN0 )
65	64	nn0zd 9605	. . . . . . . . 9 |- ( K e. NN0 -> ( 2 x. K ) e. ZZ )
66	65	peano2zd 9610	. . . . . . . 8 |- ( K e. NN0 -> ( ( 2 x. K ) + 1 ) e. ZZ )
67		1nn0 9423	. . . . . . . . 9 |- 1 e. NN0
68	67	a1i 9	. . . . . . . 8 |- ( K e. NN0 -> 1 e. NN0 )
69		4nn 9312	. . . . . . . . 9 |- 4 e. NN
70	69	a1i 9	. . . . . . . 8 |- ( K e. NN0 -> 4 e. NN )
71		adddivflid 10558	. . . . . . . 8 |- ( ( ( ( 2 x. K ) + 1 ) e. ZZ /\ 1 e. NN0 /\ 4 e. NN ) -> ( 1 < 4 <-> ( |_ ` ( ( ( 2 x. K ) + 1 ) + ( 1 / 4 ) ) ) = ( ( 2 x. K ) + 1 ) ) )
72	66, 68, 70, 71	syl3anc 1273	. . . . . . 7 |- ( K e. NN0 -> ( 1 < 4 <-> ( |_ ` ( ( ( 2 x. K ) + 1 ) + ( 1 / 4 ) ) ) = ( ( 2 x. K ) + 1 ) ) )
73	23, 24	mulcld 8205	. . . . . . . . . 10 |- ( K e. NN0 -> ( 2 x. K ) e. CC )
74	21, 47	recclapd 8966	. . . . . . . . . 10 |- ( K e. NN0 -> ( 1 / 4 ) e. CC )
75	73, 14, 74	addassd 8207	. . . . . . . . 9 |- ( K e. NN0 -> ( ( ( 2 x. K ) + 1 ) + ( 1 / 4 ) ) = ( ( 2 x. K ) + ( 1 + ( 1 / 4 ) ) ) )
76		df-5 9210	. . . . . . . . . . . . . 14 |- 5 = ( 4 + 1 )
77	76	oveq1i 6033	. . . . . . . . . . . . 13 |- ( 5 / 4 ) = ( ( 4 + 1 ) / 4 )
78		ax-1cn 8130	. . . . . . . . . . . . . 14 |- 1 e. CC
79	20, 78, 20, 46	divdirapi 8954	. . . . . . . . . . . . 13 |- ( ( 4 + 1 ) / 4 ) = ( ( 4 / 4 ) + ( 1 / 4 ) )
80	20, 46	dividapi 8930	. . . . . . . . . . . . . 14 |- ( 4 / 4 ) = 1
81	80	oveq1i 6033	. . . . . . . . . . . . 13 |- ( ( 4 / 4 ) + ( 1 / 4 ) ) = ( 1 + ( 1 / 4 ) )
82	77, 79, 81	3eqtri 2255	. . . . . . . . . . . 12 |- ( 5 / 4 ) = ( 1 + ( 1 / 4 ) )
83	82	a1i 9	. . . . . . . . . . 11 |- ( K e. NN0 -> ( 5 / 4 ) = ( 1 + ( 1 / 4 ) ) )
84	83	eqcomd 2236	. . . . . . . . . 10 |- ( K e. NN0 -> ( 1 + ( 1 / 4 ) ) = ( 5 / 4 ) )
85	84	oveq2d 6039	. . . . . . . . 9 |- ( K e. NN0 -> ( ( 2 x. K ) + ( 1 + ( 1 / 4 ) ) ) = ( ( 2 x. K ) + ( 5 / 4 ) ) )
86	75, 85	eqtrd 2263	. . . . . . . 8 |- ( K e. NN0 -> ( ( ( 2 x. K ) + 1 ) + ( 1 / 4 ) ) = ( ( 2 x. K ) + ( 5 / 4 ) ) )
87	86	fveqeq2d 5650	. . . . . . 7 |- ( K e. NN0 -> ( ( |_ ` ( ( ( 2 x. K ) + 1 ) + ( 1 / 4 ) ) ) = ( ( 2 x. K ) + 1 ) <-> ( |_ ` ( ( 2 x. K ) + ( 5 / 4 ) ) ) = ( ( 2 x. K ) + 1 ) ) )
88	72, 87	bitrd 188	. . . . . 6 |- ( K e. NN0 -> ( 1 < 4 <-> ( |_ ` ( ( 2 x. K ) + ( 5 / 4 ) ) ) = ( ( 2 x. K ) + 1 ) ) )
89	61, 88	mpbii 148	. . . . 5 |- ( K e. NN0 -> ( |_ ` ( ( 2 x. K ) + ( 5 / 4 ) ) ) = ( ( 2 x. K ) + 1 ) )
90	60, 89	eqtrd 2263	. . . 4 |- ( K e. NN0 -> ( |_ ` ( ( ( 8 x. K ) + 5 ) / 4 ) ) = ( ( 2 x. K ) + 1 ) )
91	45, 90	oveq12d 6041	. . 3 |- ( K e. NN0 -> ( ( ( ( ( 8 x. K ) + 5 ) - 1 ) / 2 ) - ( |_ ` ( ( ( 8 x. K ) + 5 ) / 4 ) ) ) = ( ( ( 4 x. K ) + 2 ) - ( ( 2 x. K ) + 1 ) ) )
92	64	nn0cnd 9462	. . . 4 |- ( K e. NN0 -> ( 2 x. K ) e. CC )
93	35, 23, 92, 14	addsub4d 8542	. . 3 |- ( K e. NN0 -> ( ( ( 4 x. K ) + 2 ) - ( ( 2 x. K ) + 1 ) ) = ( ( ( 4 x. K ) - ( 2 x. K ) ) + ( 2 - 1 ) ) )
94		2t2e4 9303	. . . . . . . . . 10 |- ( 2 x. 2 ) = 4
95	94	eqcomi 2234	. . . . . . . . 9 |- 4 = ( 2 x. 2 )
96	95	a1i 9	. . . . . . . 8 |- ( K e. NN0 -> 4 = ( 2 x. 2 ) )
97	96	oveq1d 6038	. . . . . . 7 |- ( K e. NN0 -> ( 4 x. K ) = ( ( 2 x. 2 ) x. K ) )
98	23, 23, 24	mulassd 8208	. . . . . . 7 |- ( K e. NN0 -> ( ( 2 x. 2 ) x. K ) = ( 2 x. ( 2 x. K ) ) )
99	97, 98	eqtrd 2263	. . . . . 6 |- ( K e. NN0 -> ( 4 x. K ) = ( 2 x. ( 2 x. K ) ) )
100	99	oveq1d 6038	. . . . 5 |- ( K e. NN0 -> ( ( 4 x. K ) - ( 2 x. K ) ) = ( ( 2 x. ( 2 x. K ) ) - ( 2 x. K ) ) )
101		2txmxeqx 9280	. . . . . 6 |- ( ( 2 x. K ) e. CC -> ( ( 2 x. ( 2 x. K ) ) - ( 2 x. K ) ) = ( 2 x. K ) )
102	92, 101	syl 14	. . . . 5 |- ( K e. NN0 -> ( ( 2 x. ( 2 x. K ) ) - ( 2 x. K ) ) = ( 2 x. K ) )
103	100, 102	eqtrd 2263	. . . 4 |- ( K e. NN0 -> ( ( 4 x. K ) - ( 2 x. K ) ) = ( 2 x. K ) )
104		2m1e1 9266	. . . . 5 |- ( 2 - 1 ) = 1
105	104	a1i 9	. . . 4 |- ( K e. NN0 -> ( 2 - 1 ) = 1 )
106	103, 105	oveq12d 6041	. . 3 |- ( K e. NN0 -> ( ( ( 4 x. K ) - ( 2 x. K ) ) + ( 2 - 1 ) ) = ( ( 2 x. K ) + 1 ) )
107	91, 93, 106	3eqtrd 2267	. 2 |- ( K e. NN0 -> ( ( ( ( ( 8 x. K ) + 5 ) - 1 ) / 2 ) - ( |_ ` ( ( ( 8 x. K ) + 5 ) / 4 ) ) ) = ( ( 2 x. K ) + 1 ) )
108	6, 107	sylan9eqr 2285	1 |- ( ( K e. NN0 /\ P = ( ( 8 x. K ) + 5 ) ) -> N = ( ( 2 x. K ) + 1 ) )

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105   = wceq 1397   e. wcel 2201   class class class wbr 4089   ` cfv 5328  (class class class)co 6023   CCcc 8035   0cc0 8037   1c1 8038   + caddc 8040   x. cmul 8042   < clt 8219   - cmin 8355   # cap 8766   / cdiv 8857   NNcn 9148   2c2 9199   4c4 9201   5c5 9202   8c8 9205   NN0cn0 9407   ZZcz 9484   RR+crp 9893   |_cfl 10534

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 619  ax-in2 620  ax-io 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-13 2203  ax-14 2204  ax-ext 2212  ax-sep 4208  ax-pow 4266  ax-pr 4301  ax-un 4532  ax-setind 4637  ax-cnex 8128  ax-resscn 8129  ax-1cn 8130  ax-1re 8131  ax-icn 8132  ax-addcl 8133  ax-addrcl 8134  ax-mulcl 8135  ax-mulrcl 8136  ax-addcom 8137  ax-mulcom 8138  ax-addass 8139  ax-mulass 8140  ax-distr 8141  ax-i2m1 8142  ax-0lt1 8143  ax-1rid 8144  ax-0id 8145  ax-rnegex 8146  ax-precex 8147  ax-cnre 8148  ax-pre-ltirr 8149  ax-pre-ltwlin 8150  ax-pre-lttrn 8151  ax-pre-apti 8152  ax-pre-ltadd 8153  ax-pre-mulgt0 8154  ax-pre-mulext 8155  ax-arch 8156

This theorem depends on definitions:  df-bi 117  df-3or 1005  df-3an 1006  df-tru 1400  df-fal 1403  df-nf 1509  df-sb 1810  df-eu 2081  df-mo 2082  df-clab 2217  df-cleq 2223  df-clel 2226  df-nfc 2362  df-ne 2402  df-nel 2497  df-ral 2514  df-rex 2515  df-reu 2516  df-rmo 2517  df-rab 2518  df-v 2803  df-sbc 3031  df-csb 3127  df-dif 3201  df-un 3203  df-in 3205  df-ss 3212  df-pw 3655  df-sn 3676  df-pr 3677  df-op 3679  df-uni 3895  df-int 3930  df-iun 3973  df-br 4090  df-opab 4152  df-mpt 4153  df-id 4392  df-po 4395  df-iso 4396  df-xp 4733  df-rel 4734  df-cnv 4735  df-co 4736  df-dm 4737  df-rn 4738  df-res 4739  df-ima 4740  df-iota 5288  df-fun 5330  df-fn 5331  df-f 5332  df-fv 5336  df-riota 5976  df-ov 6026  df-oprab 6027  df-mpo 6028  df-1st 6308  df-2nd 6309  df-pnf 8221  df-mnf 8222  df-xr 8223  df-ltxr 8224  df-le 8225  df-sub 8357  df-neg 8358  df-reap 8760  df-ap 8767  df-div 8858  df-inn 9149  df-2 9207  df-3 9208  df-4 9209  df-5 9210  df-6 9211  df-7 9212  df-8 9213  df-n0 9408  df-z 9485  df-q 9859  df-rp 9894  df-fl 10536

This theorem is referenced by:  2lgslem3c1  15857