Theorem rplogsumlem2 22739

Description: Lemma for rplogsum 22781. Equation 9.2.14 of [Shapiro], p. 331. (Contributed by Mario Carneiro, 2-May-2016.)

Assertion

Ref	Expression
rplogsumlem2	|- ( A e. ZZ -> sum_ n e. ( 1 ... A ) ( ( (Λ ` n ) - if ( n e. Prime , ( log ` n ) , 0 ) ) / n ) <_ 2 )

Distinct variable group:   A, n

Proof of Theorem rplogsumlem2

Dummy variables k p are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		flid 11662	. . . . 5 |- ( A e. ZZ -> ( |_ ` A ) = A )
2	1	oveq2d 6112	. . . 4 |- ( A e. ZZ -> ( 1 ... ( |_ ` A ) ) = ( 1 ... A ) )
3	2	sumeq1d 13183	. . 3 |- ( A e. ZZ -> sum_ n e. ( 1 ... ( |_ ` A ) ) ( ( (Λ ` n ) - if ( n e. Prime , ( log ` n ) , 0 ) ) / n ) = sum_ n e. ( 1 ... A ) ( ( (Λ ` n ) - if ( n e. Prime , ( log ` n ) , 0 ) ) / n ) )
4		fveq2 5696	. . . . . 6 |- ( n = ( p ^ k ) -> (Λ ` n ) = (Λ ` ( p ^ k ) ) )
5		eleq1 2503	. . . . . . 7 |- ( n = ( p ^ k ) -> ( n e. Prime <-> ( p ^ k ) e. Prime ) )
6		fveq2 5696	. . . . . . 7 |- ( n = ( p ^ k ) -> ( log ` n ) = ( log ` ( p ^ k ) ) )
7	5, 6	ifbieq1d 3817	. . . . . 6 |- ( n = ( p ^ k ) -> if ( n e. Prime , ( log ` n ) , 0 ) = if ( ( p ^ k ) e. Prime , ( log ` ( p ^ k ) ) , 0 ) )
8	4, 7	oveq12d 6114	. . . . 5 |- ( n = ( p ^ k ) -> ( (Λ ` n ) - if ( n e. Prime , ( log ` n ) , 0 ) ) = ( (Λ ` ( p ^ k ) ) - if ( ( p ^ k ) e. Prime , ( log ` ( p ^ k ) ) , 0 ) ) )
9		id 22	. . . . 5 |- ( n = ( p ^ k ) -> n = ( p ^ k ) )
10	8, 9	oveq12d 6114	. . . 4 |- ( n = ( p ^ k ) -> ( ( (Λ ` n ) - if ( n e. Prime , ( log ` n ) , 0 ) ) / n ) = ( ( (Λ ` ( p ^ k ) ) - if ( ( p ^ k ) e. Prime , ( log ` ( p ^ k ) ) , 0 ) ) / ( p ^ k ) ) )
11		zre 10655	. . . 4 |- ( A e. ZZ -> A e. RR )
12		elfznn 11483	. . . . . . . . 9 |- ( n e. ( 1 ... ( |_ ` A ) ) -> n e. NN )
13	12	adantl 466	. . . . . . . 8 |- ( ( A e. ZZ /\ n e. ( 1 ... ( |_ ` A ) ) ) -> n e. NN )
14		vmacl 22461	. . . . . . . 8 |- ( n e. NN -> (Λ ` n ) e. RR )
15	13, 14	syl 16	. . . . . . 7 |- ( ( A e. ZZ /\ n e. ( 1 ... ( |_ ` A ) ) ) -> (Λ ` n ) e. RR )
16	13	nnrpd 11031	. . . . . . . . 9 |- ( ( A e. ZZ /\ n e. ( 1 ... ( |_ ` A ) ) ) -> n e. RR+ )
17	16	relogcld 22077	. . . . . . . 8 |- ( ( A e. ZZ /\ n e. ( 1 ... ( |_ ` A ) ) ) -> ( log ` n ) e. RR )
18		0re 9391	. . . . . . . 8 |- 0 e. RR
19		ifcl 3836	. . . . . . . 8 |- ( ( ( log ` n ) e. RR /\ 0 e. RR ) -> if ( n e. Prime , ( log ` n ) , 0 ) e. RR )
20	17, 18, 19	sylancl 662	. . . . . . 7 |- ( ( A e. ZZ /\ n e. ( 1 ... ( |_ ` A ) ) ) -> if ( n e. Prime , ( log ` n ) , 0 ) e. RR )
21	15, 20	resubcld 9781	. . . . . 6 |- ( ( A e. ZZ /\ n e. ( 1 ... ( |_ ` A ) ) ) -> ( (Λ ` n ) - if ( n e. Prime , ( log ` n ) , 0 ) ) e. RR )
22	21, 13	nndivred 10375	. . . . 5 |- ( ( A e. ZZ /\ n e. ( 1 ... ( |_ ` A ) ) ) -> ( ( (Λ ` n ) - if ( n e. Prime , ( log ` n ) , 0 ) ) / n ) e. RR )
23	22	recnd 9417	. . . 4 |- ( ( A e. ZZ /\ n e. ( 1 ... ( |_ ` A ) ) ) -> ( ( (Λ ` n ) - if ( n e. Prime , ( log ` n ) , 0 ) ) / n ) e. CC )
24		simprr 756	. . . . . . . 8 |- ( ( A e. ZZ /\ ( n e. ( 1 ... ( |_ ` A ) ) /\ (Λ ` n ) = 0 ) ) -> (Λ ` n ) = 0 )
25		vmaprm 22460	. . . . . . . . . . . . 13 |- ( n e. Prime -> (Λ ` n ) = ( log ` n ) )
26		prmnn 13771	. . . . . . . . . . . . . . 15 |- ( n e. Prime -> n e. NN )
27	26	nnred 10342	. . . . . . . . . . . . . 14 |- ( n e. Prime -> n e. RR )
28		prmuz2 13786	. . . . . . . . . . . . . . 15 |- ( n e. Prime -> n e. ( ZZ>= ` 2 ) )
29		eluz2b2 10932	. . . . . . . . . . . . . . . 16 |- ( n e. ( ZZ>= ` 2 ) <-> ( n e. NN /\ 1 < n ) )
30	29	simprbi 464	. . . . . . . . . . . . . . 15 |- ( n e. ( ZZ>= ` 2 ) -> 1 < n )
31	28, 30	syl 16	. . . . . . . . . . . . . 14 |- ( n e. Prime -> 1 < n )
32	27, 31	rplogcld 22083	. . . . . . . . . . . . 13 |- ( n e. Prime -> ( log ` n ) e. RR+ )
33	25, 32	eqeltrd 2517	. . . . . . . . . . . 12 |- ( n e. Prime -> (Λ ` n ) e. RR+ )
34	33	rpne0d 11037	. . . . . . . . . . 11 |- ( n e. Prime -> (Λ ` n ) =/= 0 )
35	34	necon2bi 2662	. . . . . . . . . 10 |- ( (Λ ` n ) = 0 -> -. n e. Prime )
36	35	ad2antll 728	. . . . . . . . 9 |- ( ( A e. ZZ /\ ( n e. ( 1 ... ( |_ ` A ) ) /\ (Λ ` n ) = 0 ) ) -> -. n e. Prime )
37		iffalse 3804	. . . . . . . . 9 |- ( -. n e. Prime -> if ( n e. Prime , ( log ` n ) , 0 ) = 0 )
38	36, 37	syl 16	. . . . . . . 8 |- ( ( A e. ZZ /\ ( n e. ( 1 ... ( |_ ` A ) ) /\ (Λ ` n ) = 0 ) ) -> if ( n e. Prime , ( log ` n ) , 0 ) = 0 )
39	24, 38	oveq12d 6114	. . . . . . 7 |- ( ( A e. ZZ /\ ( n e. ( 1 ... ( |_ ` A ) ) /\ (Λ ` n ) = 0 ) ) -> ( (Λ ` n ) - if ( n e. Prime , ( log ` n ) , 0 ) ) = ( 0 - 0 ) )
40		0m0e0 10436	. . . . . . 7 |- ( 0 - 0 ) = 0
41	39, 40	syl6eq 2491	. . . . . 6 |- ( ( A e. ZZ /\ ( n e. ( 1 ... ( |_ ` A ) ) /\ (Λ ` n ) = 0 ) ) -> ( (Λ ` n ) - if ( n e. Prime , ( log ` n ) , 0 ) ) = 0 )
42	41	oveq1d 6111	. . . . 5 |- ( ( A e. ZZ /\ ( n e. ( 1 ... ( |_ ` A ) ) /\ (Λ ` n ) = 0 ) ) -> ( ( (Λ ` n ) - if ( n e. Prime , ( log ` n ) , 0 ) ) / n ) = ( 0 / n ) )
43	12	ad2antrl 727	. . . . . . . 8 |- ( ( A e. ZZ /\ ( n e. ( 1 ... ( |_ ` A ) ) /\ (Λ ` n ) = 0 ) ) -> n e. NN )
44	43	nnrpd 11031	. . . . . . 7 |- ( ( A e. ZZ /\ ( n e. ( 1 ... ( |_ ` A ) ) /\ (Λ ` n ) = 0 ) ) -> n e. RR+ )
45	44	rpcnne0d 11041	. . . . . 6 |- ( ( A e. ZZ /\ ( n e. ( 1 ... ( |_ ` A ) ) /\ (Λ ` n ) = 0 ) ) -> ( n e. CC /\ n =/= 0 ) )
46		div0 10027	. . . . . 6 |- ( ( n e. CC /\ n =/= 0 ) -> ( 0 / n ) = 0 )
47	45, 46	syl 16	. . . . 5 |- ( ( A e. ZZ /\ ( n e. ( 1 ... ( |_ ` A ) ) /\ (Λ ` n ) = 0 ) ) -> ( 0 / n ) = 0 )
48	42, 47	eqtrd 2475	. . . 4 |- ( ( A e. ZZ /\ ( n e. ( 1 ... ( |_ ` A ) ) /\ (Λ ` n ) = 0 ) ) -> ( ( (Λ ` n ) - if ( n e. Prime , ( log ` n ) , 0 ) ) / n ) = 0 )
49	10, 11, 23, 48	fsumvma2 22558	. . 3 |- ( A e. ZZ -> sum_ n e. ( 1 ... ( |_ ` A ) ) ( ( (Λ ` n ) - if ( n e. Prime , ( log ` n ) , 0 ) ) / n ) = sum_ p e. ( ( 0 [,] A ) i^i Prime ) sum_ k e. ( 1 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) ( ( (Λ ` ( p ^ k ) ) - if ( ( p ^ k ) e. Prime , ( log ` ( p ^ k ) ) , 0 ) ) / ( p ^ k ) ) )
50	3, 49	eqtr3d 2477	. 2 |- ( A e. ZZ -> sum_ n e. ( 1 ... A ) ( ( (Λ ` n ) - if ( n e. Prime , ( log ` n ) , 0 ) ) / n ) = sum_ p e. ( ( 0 [,] A ) i^i Prime ) sum_ k e. ( 1 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) ( ( (Λ ` ( p ^ k ) ) - if ( ( p ^ k ) e. Prime , ( log ` ( p ^ k ) ) , 0 ) ) / ( p ^ k ) ) )
51		fzfid 11800	. . . . 5 |- ( A e. ZZ -> ( 2 ... ( ( abs ` A ) + 1 ) ) e. Fin )
52		inss2 3576	. . . . . . . . . . . 12 |- ( ( 0 [,] A ) i^i Prime ) C_ Prime
53		simpr 461	. . . . . . . . . . . 12 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> p e. ( ( 0 [,] A ) i^i Prime ) )
54	52, 53	sseldi 3359	. . . . . . . . . . 11 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> p e. Prime )
55		prmnn 13771	. . . . . . . . . . 11 |- ( p e. Prime -> p e. NN )
56	54, 55	syl 16	. . . . . . . . . 10 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> p e. NN )
57	56	nnred 10342	. . . . . . . . 9 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> p e. RR )
58	11	adantr 465	. . . . . . . . 9 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> A e. RR )
59		zcn 10656	. . . . . . . . . . . 12 |- ( A e. ZZ -> A e. CC )
60	59	abscld 12927	. . . . . . . . . . 11 |- ( A e. ZZ -> ( abs ` A ) e. RR )
61		peano2re 9547	. . . . . . . . . . 11 |- ( ( abs ` A ) e. RR -> ( ( abs ` A ) + 1 ) e. RR )
62	60, 61	syl 16	. . . . . . . . . 10 |- ( A e. ZZ -> ( ( abs ` A ) + 1 ) e. RR )
63	62	adantr 465	. . . . . . . . 9 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( ( abs ` A ) + 1 ) e. RR )
64		inss1 3575	. . . . . . . . . . . . 13 |- ( ( 0 [,] A ) i^i Prime ) C_ ( 0 [,] A )
65	64	sseli 3357	. . . . . . . . . . . 12 |- ( p e. ( ( 0 [,] A ) i^i Prime ) -> p e. ( 0 [,] A ) )
66		elicc2 11365	. . . . . . . . . . . . 13 |- ( ( 0 e. RR /\ A e. RR ) -> ( p e. ( 0 [,] A ) <-> ( p e. RR /\ 0 <_ p /\ p <_ A ) ) )
67	18, 11, 66	sylancr 663	. . . . . . . . . . . 12 |- ( A e. ZZ -> ( p e. ( 0 [,] A ) <-> ( p e. RR /\ 0 <_ p /\ p <_ A ) ) )
68	65, 67	syl5ib 219	. . . . . . . . . . 11 |- ( A e. ZZ -> ( p e. ( ( 0 [,] A ) i^i Prime ) -> ( p e. RR /\ 0 <_ p /\ p <_ A ) ) )
69	68	imp 429	. . . . . . . . . 10 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( p e. RR /\ 0 <_ p /\ p <_ A ) )
70	69	simp3d 1002	. . . . . . . . 9 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> p <_ A )
71	59	adantr 465	. . . . . . . . . . 11 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> A e. CC )
72	71	abscld 12927	. . . . . . . . . 10 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( abs ` A ) e. RR )
73	58	leabsd 12906	. . . . . . . . . 10 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> A <_ ( abs ` A ) )
74	72	lep1d 10269	. . . . . . . . . 10 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( abs ` A ) <_ ( ( abs ` A ) + 1 ) )
75	58, 72, 63, 73, 74	letrd 9533	. . . . . . . . 9 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> A <_ ( ( abs ` A ) + 1 ) )
76	57, 58, 63, 70, 75	letrd 9533	. . . . . . . 8 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> p <_ ( ( abs ` A ) + 1 ) )
77		prmuz2 13786	. . . . . . . . . 10 |- ( p e. Prime -> p e. ( ZZ>= ` 2 ) )
78	54, 77	syl 16	. . . . . . . . 9 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> p e. ( ZZ>= ` 2 ) )
79		nn0abscl 12806	. . . . . . . . . . . 12 |- ( A e. ZZ -> ( abs ` A ) e. NN0 )
80		nn0p1nn 10624	. . . . . . . . . . . 12 |- ( ( abs ` A ) e. NN0 -> ( ( abs ` A ) + 1 ) e. NN )
81	79, 80	syl 16	. . . . . . . . . . 11 |- ( A e. ZZ -> ( ( abs ` A ) + 1 ) e. NN )
82	81	nnzd 10751	. . . . . . . . . 10 |- ( A e. ZZ -> ( ( abs ` A ) + 1 ) e. ZZ )
83	82	adantr 465	. . . . . . . . 9 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( ( abs ` A ) + 1 ) e. ZZ )
84		elfz5 11450	. . . . . . . . 9 |- ( ( p e. ( ZZ>= ` 2 ) /\ ( ( abs ` A ) + 1 ) e. ZZ ) -> ( p e. ( 2 ... ( ( abs ` A ) + 1 ) ) <-> p <_ ( ( abs ` A ) + 1 ) ) )
85	78, 83, 84	syl2anc 661	. . . . . . . 8 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( p e. ( 2 ... ( ( abs ` A ) + 1 ) ) <-> p <_ ( ( abs ` A ) + 1 ) ) )
86	76, 85	mpbird 232	. . . . . . 7 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> p e. ( 2 ... ( ( abs ` A ) + 1 ) ) )
87	86	ex 434	. . . . . 6 |- ( A e. ZZ -> ( p e. ( ( 0 [,] A ) i^i Prime ) -> p e. ( 2 ... ( ( abs ` A ) + 1 ) ) ) )
88	87	ssrdv 3367	. . . . 5 |- ( A e. ZZ -> ( ( 0 [,] A ) i^i Prime ) C_ ( 2 ... ( ( abs ` A ) + 1 ) ) )
89		ssfi 7538	. . . . 5 |- ( ( ( 2 ... ( ( abs ` A ) + 1 ) ) e. Fin /\ ( ( 0 [,] A ) i^i Prime ) C_ ( 2 ... ( ( abs ` A ) + 1 ) ) ) -> ( ( 0 [,] A ) i^i Prime ) e. Fin )
90	51, 88, 89	syl2anc 661	. . . 4 |- ( A e. ZZ -> ( ( 0 [,] A ) i^i Prime ) e. Fin )
91		fzfid 11800	. . . . 5 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( 1 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) e. Fin )
92		simprl 755	. . . . . . . . . . 11 |- ( ( A e. ZZ /\ ( p e. ( ( 0 [,] A ) i^i Prime ) /\ k e. ( 1 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) ) ) -> p e. ( ( 0 [,] A ) i^i Prime ) )
93	52, 92	sseldi 3359	. . . . . . . . . 10 |- ( ( A e. ZZ /\ ( p e. ( ( 0 [,] A ) i^i Prime ) /\ k e. ( 1 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) ) ) -> p e. Prime )
94		elfznn 11483	. . . . . . . . . . 11 |- ( k e. ( 1 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) -> k e. NN )
95	94	ad2antll 728	. . . . . . . . . 10 |- ( ( A e. ZZ /\ ( p e. ( ( 0 [,] A ) i^i Prime ) /\ k e. ( 1 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) ) ) -> k e. NN )
96		vmappw 22459	. . . . . . . . . 10 |- ( ( p e. Prime /\ k e. NN ) -> (Λ ` ( p ^ k ) ) = ( log ` p ) )
97	93, 95, 96	syl2anc 661	. . . . . . . . 9 |- ( ( A e. ZZ /\ ( p e. ( ( 0 [,] A ) i^i Prime ) /\ k e. ( 1 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) ) ) -> (Λ ` ( p ^ k ) ) = ( log ` p ) )
98	56	adantrr 716	. . . . . . . . . . 11 |- ( ( A e. ZZ /\ ( p e. ( ( 0 [,] A ) i^i Prime ) /\ k e. ( 1 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) ) ) -> p e. NN )
99	98	nnrpd 11031	. . . . . . . . . 10 |- ( ( A e. ZZ /\ ( p e. ( ( 0 [,] A ) i^i Prime ) /\ k e. ( 1 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) ) ) -> p e. RR+ )
100	99	relogcld 22077	. . . . . . . . 9 |- ( ( A e. ZZ /\ ( p e. ( ( 0 [,] A ) i^i Prime ) /\ k e. ( 1 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) ) ) -> ( log ` p ) e. RR )
101	97, 100	eqeltrd 2517	. . . . . . . 8 |- ( ( A e. ZZ /\ ( p e. ( ( 0 [,] A ) i^i Prime ) /\ k e. ( 1 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) ) ) -> (Λ ` ( p ^ k ) ) e. RR )
102	95	nnnn0d 10641	. . . . . . . . . . . 12 |- ( ( A e. ZZ /\ ( p e. ( ( 0 [,] A ) i^i Prime ) /\ k e. ( 1 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) ) ) -> k e. NN0 )
103		nnexpcl 11883	. . . . . . . . . . . 12 |- ( ( p e. NN /\ k e. NN0 ) -> ( p ^ k ) e. NN )
104	98, 102, 103	syl2anc 661	. . . . . . . . . . 11 |- ( ( A e. ZZ /\ ( p e. ( ( 0 [,] A ) i^i Prime ) /\ k e. ( 1 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) ) ) -> ( p ^ k ) e. NN )
105	104	nnrpd 11031	. . . . . . . . . 10 |- ( ( A e. ZZ /\ ( p e. ( ( 0 [,] A ) i^i Prime ) /\ k e. ( 1 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) ) ) -> ( p ^ k ) e. RR+ )
106	105	relogcld 22077	. . . . . . . . 9 |- ( ( A e. ZZ /\ ( p e. ( ( 0 [,] A ) i^i Prime ) /\ k e. ( 1 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) ) ) -> ( log ` ( p ^ k ) ) e. RR )
107		ifcl 3836	. . . . . . . . 9 |- ( ( ( log ` ( p ^ k ) ) e. RR /\ 0 e. RR ) -> if ( ( p ^ k ) e. Prime , ( log ` ( p ^ k ) ) , 0 ) e. RR )
108	106, 18, 107	sylancl 662	. . . . . . . 8 |- ( ( A e. ZZ /\ ( p e. ( ( 0 [,] A ) i^i Prime ) /\ k e. ( 1 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) ) ) -> if ( ( p ^ k ) e. Prime , ( log ` ( p ^ k ) ) , 0 ) e. RR )
109	101, 108	resubcld 9781	. . . . . . 7 |- ( ( A e. ZZ /\ ( p e. ( ( 0 [,] A ) i^i Prime ) /\ k e. ( 1 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) ) ) -> ( (Λ ` ( p ^ k ) ) - if ( ( p ^ k ) e. Prime , ( log ` ( p ^ k ) ) , 0 ) ) e. RR )
110	109, 104	nndivred 10375	. . . . . 6 |- ( ( A e. ZZ /\ ( p e. ( ( 0 [,] A ) i^i Prime ) /\ k e. ( 1 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) ) ) -> ( ( (Λ ` ( p ^ k ) ) - if ( ( p ^ k ) e. Prime , ( log ` ( p ^ k ) ) , 0 ) ) / ( p ^ k ) ) e. RR )
111	110	anassrs 648	. . . . 5 |- ( ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) /\ k e. ( 1 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) ) -> ( ( (Λ ` ( p ^ k ) ) - if ( ( p ^ k ) e. Prime , ( log ` ( p ^ k ) ) , 0 ) ) / ( p ^ k ) ) e. RR )
112	91, 111	fsumrecl 13216	. . . 4 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> sum_ k e. ( 1 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) ( ( (Λ ` ( p ^ k ) ) - if ( ( p ^ k ) e. Prime , ( log ` ( p ^ k ) ) , 0 ) ) / ( p ^ k ) ) e. RR )
113	90, 112	fsumrecl 13216	. . 3 |- ( A e. ZZ -> sum_ p e. ( ( 0 [,] A ) i^i Prime ) sum_ k e. ( 1 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) ( ( (Λ ` ( p ^ k ) ) - if ( ( p ^ k ) e. Prime , ( log ` ( p ^ k ) ) , 0 ) ) / ( p ^ k ) ) e. RR )
114	56	nnrpd 11031	. . . . . 6 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> p e. RR+ )
115	114	relogcld 22077	. . . . 5 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( log ` p ) e. RR )
116		uz2m1nn 10934	. . . . . . 7 |- ( p e. ( ZZ>= ` 2 ) -> ( p - 1 ) e. NN )
117	78, 116	syl 16	. . . . . 6 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( p - 1 ) e. NN )
118	56, 117	nnmulcld 10374	. . . . 5 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( p x. ( p - 1 ) ) e. NN )
119	115, 118	nndivred 10375	. . . 4 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( ( log ` p ) / ( p x. ( p - 1 ) ) ) e. RR )
120	90, 119	fsumrecl 13216	. . 3 |- ( A e. ZZ -> sum_ p e. ( ( 0 [,] A ) i^i Prime ) ( ( log ` p ) / ( p x. ( p - 1 ) ) ) e. RR )
121		2re 10396	. . . 4 |- 2 e. RR
122	121	a1i 11	. . 3 |- ( A e. ZZ -> 2 e. RR )
123	18	a1i 11	. . . . . . . . . . . . 13 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> 0 e. RR )
124	56	nngt0d 10370	. . . . . . . . . . . . 13 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> 0 < p )
125	123, 57, 58, 124, 70	ltletrd 9536	. . . . . . . . . . . 12 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> 0 < A )
126	58, 125	elrpd 11030	. . . . . . . . . . 11 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> A e. RR+ )
127	126	relogcld 22077	. . . . . . . . . 10 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( log ` A ) e. RR )
128		eluz2b2 10932	. . . . . . . . . . . . . 14 |- ( p e. ( ZZ>= ` 2 ) <-> ( p e. NN /\ 1 < p ) )
129	128	simprbi 464	. . . . . . . . . . . . 13 |- ( p e. ( ZZ>= ` 2 ) -> 1 < p )
130	77, 129	syl 16	. . . . . . . . . . . 12 |- ( p e. Prime -> 1 < p )
131	54, 130	syl 16	. . . . . . . . . . 11 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> 1 < p )
132	57, 131	rplogcld 22083	. . . . . . . . . 10 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( log ` p ) e. RR+ )
133	127, 132	rerpdivcld 11059	. . . . . . . . 9 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( ( log ` A ) / ( log ` p ) ) e. RR )
134	132	rpcnd 11034	. . . . . . . . . . . 12 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( log ` p ) e. CC )
135	134	mulid2d 9409	. . . . . . . . . . 11 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( 1 x. ( log ` p ) ) = ( log ` p ) )
136	114, 126	logled 22081	. . . . . . . . . . . 12 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( p <_ A <-> ( log ` p ) <_ ( log ` A ) ) )
137	70, 136	mpbid 210	. . . . . . . . . . 11 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( log ` p ) <_ ( log ` A ) )
138	135, 137	eqbrtrd 4317	. . . . . . . . . 10 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( 1 x. ( log ` p ) ) <_ ( log ` A ) )
139		1re 9390	. . . . . . . . . . . 12 |- 1 e. RR
140	139	a1i 11	. . . . . . . . . . 11 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> 1 e. RR )
141	140, 127, 132	lemuldivd 11077	. . . . . . . . . 10 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( ( 1 x. ( log ` p ) ) <_ ( log ` A ) <-> 1 <_ ( ( log ` A ) / ( log ` p ) ) ) )
142	138, 141	mpbid 210	. . . . . . . . 9 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> 1 <_ ( ( log ` A ) / ( log ` p ) ) )
143		flge1nn 11672	. . . . . . . . 9 |- ( ( ( ( log ` A ) / ( log ` p ) ) e. RR /\ 1 <_ ( ( log ` A ) / ( log ` p ) ) ) -> ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) e. NN )
144	133, 142, 143	syl2anc 661	. . . . . . . 8 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) e. NN )
145		nnuz 10901	. . . . . . . 8 |- NN = ( ZZ>= ` 1 )
146	144, 145	syl6eleq 2533	. . . . . . 7 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) e. ( ZZ>= ` 1 ) )
147	110	recnd 9417	. . . . . . . 8 |- ( ( A e. ZZ /\ ( p e. ( ( 0 [,] A ) i^i Prime ) /\ k e. ( 1 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) ) ) -> ( ( (Λ ` ( p ^ k ) ) - if ( ( p ^ k ) e. Prime , ( log ` ( p ^ k ) ) , 0 ) ) / ( p ^ k ) ) e. CC )
148	147	anassrs 648	. . . . . . 7 |- ( ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) /\ k e. ( 1 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) ) -> ( ( (Λ ` ( p ^ k ) ) - if ( ( p ^ k ) e. Prime , ( log ` ( p ^ k ) ) , 0 ) ) / ( p ^ k ) ) e. CC )
149		oveq2 6104	. . . . . . . . . 10 |- ( k = 1 -> ( p ^ k ) = ( p ^ 1 ) )
150	149	fveq2d 5700	. . . . . . . . 9 |- ( k = 1 -> (Λ ` ( p ^ k ) ) = (Λ ` ( p ^ 1 ) ) )
151	149	eleq1d 2509	. . . . . . . . . 10 |- ( k = 1 -> ( ( p ^ k ) e. Prime <-> ( p ^ 1 ) e. Prime ) )
152	149	fveq2d 5700	. . . . . . . . . 10 |- ( k = 1 -> ( log ` ( p ^ k ) ) = ( log ` ( p ^ 1 ) ) )
153	151, 152	ifbieq1d 3817	. . . . . . . . 9 |- ( k = 1 -> if ( ( p ^ k ) e. Prime , ( log ` ( p ^ k ) ) , 0 ) = if ( ( p ^ 1 ) e. Prime , ( log ` ( p ^ 1 ) ) , 0 ) )
154	150, 153	oveq12d 6114	. . . . . . . 8 |- ( k = 1 -> ( (Λ ` ( p ^ k ) ) - if ( ( p ^ k ) e. Prime , ( log ` ( p ^ k ) ) , 0 ) ) = ( (Λ ` ( p ^ 1 ) ) - if ( ( p ^ 1 ) e. Prime , ( log ` ( p ^ 1 ) ) , 0 ) ) )
155	154, 149	oveq12d 6114	. . . . . . 7 |- ( k = 1 -> ( ( (Λ ` ( p ^ k ) ) - if ( ( p ^ k ) e. Prime , ( log ` ( p ^ k ) ) , 0 ) ) / ( p ^ k ) ) = ( ( (Λ ` ( p ^ 1 ) ) - if ( ( p ^ 1 ) e. Prime , ( log ` ( p ^ 1 ) ) , 0 ) ) / ( p ^ 1 ) ) )
156	146, 148, 155	fsum1p 13227	. . . . . 6 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> sum_ k e. ( 1 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) ( ( (Λ ` ( p ^ k ) ) - if ( ( p ^ k ) e. Prime , ( log ` ( p ^ k ) ) , 0 ) ) / ( p ^ k ) ) = ( ( ( (Λ ` ( p ^ 1 ) ) - if ( ( p ^ 1 ) e. Prime , ( log ` ( p ^ 1 ) ) , 0 ) ) / ( p ^ 1 ) ) + sum_ k e. ( ( 1 + 1 ) ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) ( ( (Λ ` ( p ^ k ) ) - if ( ( p ^ k ) e. Prime , ( log ` ( p ^ k ) ) , 0 ) ) / ( p ^ k ) ) ) )
157	56	nncnd 10343	. . . . . . . . . . . . . 14 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> p e. CC )
158	157	exp1d 12008	. . . . . . . . . . . . 13 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( p ^ 1 ) = p )
159	158	fveq2d 5700	. . . . . . . . . . . 12 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> (Λ ` ( p ^ 1 ) ) = (Λ ` p ) )
160		vmaprm 22460	. . . . . . . . . . . . 13 |- ( p e. Prime -> (Λ ` p ) = ( log ` p ) )
161	54, 160	syl 16	. . . . . . . . . . . 12 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> (Λ ` p ) = ( log ` p ) )
162	159, 161	eqtrd 2475	. . . . . . . . . . 11 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> (Λ ` ( p ^ 1 ) ) = ( log ` p ) )
163	158, 54	eqeltrd 2517	. . . . . . . . . . . . 13 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( p ^ 1 ) e. Prime )
164		iftrue 3802	. . . . . . . . . . . . 13 |- ( ( p ^ 1 ) e. Prime -> if ( ( p ^ 1 ) e. Prime , ( log ` ( p ^ 1 ) ) , 0 ) = ( log ` ( p ^ 1 ) ) )
165	163, 164	syl 16	. . . . . . . . . . . 12 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> if ( ( p ^ 1 ) e. Prime , ( log ` ( p ^ 1 ) ) , 0 ) = ( log ` ( p ^ 1 ) ) )
166	158	fveq2d 5700	. . . . . . . . . . . 12 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( log ` ( p ^ 1 ) ) = ( log ` p ) )
167	165, 166	eqtrd 2475	. . . . . . . . . . 11 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> if ( ( p ^ 1 ) e. Prime , ( log ` ( p ^ 1 ) ) , 0 ) = ( log ` p ) )
168	162, 167	oveq12d 6114	. . . . . . . . . 10 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( (Λ ` ( p ^ 1 ) ) - if ( ( p ^ 1 ) e. Prime , ( log ` ( p ^ 1 ) ) , 0 ) ) = ( ( log ` p ) - ( log ` p ) ) )
169	134	subidd 9712	. . . . . . . . . 10 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( ( log ` p ) - ( log ` p ) ) = 0 )
170	168, 169	eqtrd 2475	. . . . . . . . 9 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( (Λ ` ( p ^ 1 ) ) - if ( ( p ^ 1 ) e. Prime , ( log ` ( p ^ 1 ) ) , 0 ) ) = 0 )
171	170, 158	oveq12d 6114	. . . . . . . 8 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( ( (Λ ` ( p ^ 1 ) ) - if ( ( p ^ 1 ) e. Prime , ( log ` ( p ^ 1 ) ) , 0 ) ) / ( p ^ 1 ) ) = ( 0 / p ) )
172	114	rpcnne0d 11041	. . . . . . . . 9 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( p e. CC /\ p =/= 0 ) )
173		div0 10027	. . . . . . . . 9 |- ( ( p e. CC /\ p =/= 0 ) -> ( 0 / p ) = 0 )
174	172, 173	syl 16	. . . . . . . 8 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( 0 / p ) = 0 )
175	171, 174	eqtrd 2475	. . . . . . 7 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( ( (Λ ` ( p ^ 1 ) ) - if ( ( p ^ 1 ) e. Prime , ( log ` ( p ^ 1 ) ) , 0 ) ) / ( p ^ 1 ) ) = 0 )
176		1p1e2 10440	. . . . . . . . . 10 |- ( 1 + 1 ) = 2
177	176	oveq1i 6106	. . . . . . . . 9 |- ( ( 1 + 1 ) ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) = ( 2 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) )
178	177	a1i 11	. . . . . . . 8 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( ( 1 + 1 ) ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) = ( 2 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) )
179		elfzuz 11454	. . . . . . . . . . . . . 14 |- ( k e. ( 2 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) -> k e. ( ZZ>= ` 2 ) )
180		eluz2b2 10932	. . . . . . . . . . . . . . 15 |- ( k e. ( ZZ>= ` 2 ) <-> ( k e. NN /\ 1 < k ) )
181	180	simplbi 460	. . . . . . . . . . . . . 14 |- ( k e. ( ZZ>= ` 2 ) -> k e. NN )
182	179, 181	syl 16	. . . . . . . . . . . . 13 |- ( k e. ( 2 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) -> k e. NN )
183	182, 177	eleq2s 2535	. . . . . . . . . . . 12 |- ( k e. ( ( 1 + 1 ) ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) -> k e. NN )
184	54, 183, 96	syl2an 477	. . . . . . . . . . 11 |- ( ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) /\ k e. ( ( 1 + 1 ) ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) ) -> (Λ ` ( p ^ k ) ) = ( log ` p ) )
185	56	adantr 465	. . . . . . . . . . . . . 14 |- ( ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) /\ k e. ( ( 1 + 1 ) ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) ) -> p e. NN )
186		nnq 10971	. . . . . . . . . . . . . 14 |- ( p e. NN -> p e. QQ )
187	185, 186	syl 16	. . . . . . . . . . . . 13 |- ( ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) /\ k e. ( ( 1 + 1 ) ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) ) -> p e. QQ )
188	179, 177	eleq2s 2535	. . . . . . . . . . . . . 14 |- ( k e. ( ( 1 + 1 ) ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) -> k e. ( ZZ>= ` 2 ) )
189	188	adantl 466	. . . . . . . . . . . . 13 |- ( ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) /\ k e. ( ( 1 + 1 ) ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) ) -> k e. ( ZZ>= ` 2 ) )
190		expnprm 13969	. . . . . . . . . . . . 13 |- ( ( p e. QQ /\ k e. ( ZZ>= ` 2 ) ) -> -. ( p ^ k ) e. Prime )
191	187, 189, 190	syl2anc 661	. . . . . . . . . . . 12 |- ( ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) /\ k e. ( ( 1 + 1 ) ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) ) -> -. ( p ^ k ) e. Prime )
192		iffalse 3804	. . . . . . . . . . . 12 |- ( -. ( p ^ k ) e. Prime -> if ( ( p ^ k ) e. Prime , ( log ` ( p ^ k ) ) , 0 ) = 0 )
193	191, 192	syl 16	. . . . . . . . . . 11 |- ( ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) /\ k e. ( ( 1 + 1 ) ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) ) -> if ( ( p ^ k ) e. Prime , ( log ` ( p ^ k ) ) , 0 ) = 0 )
194	184, 193	oveq12d 6114	. . . . . . . . . 10 |- ( ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) /\ k e. ( ( 1 + 1 ) ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) ) -> ( (Λ ` ( p ^ k ) ) - if ( ( p ^ k ) e. Prime , ( log ` ( p ^ k ) ) , 0 ) ) = ( ( log ` p ) - 0 ) )
195	134	subid1d 9713	. . . . . . . . . . 11 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( ( log ` p ) - 0 ) = ( log ` p ) )
196	195	adantr 465	. . . . . . . . . 10 |- ( ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) /\ k e. ( ( 1 + 1 ) ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) ) -> ( ( log ` p ) - 0 ) = ( log ` p ) )
197	194, 196	eqtrd 2475	. . . . . . . . 9 |- ( ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) /\ k e. ( ( 1 + 1 ) ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) ) -> ( (Λ ` ( p ^ k ) ) - if ( ( p ^ k ) e. Prime , ( log ` ( p ^ k ) ) , 0 ) ) = ( log ` p ) )
198	197	oveq1d 6111	. . . . . . . 8 |- ( ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) /\ k e. ( ( 1 + 1 ) ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) ) -> ( ( (Λ ` ( p ^ k ) ) - if ( ( p ^ k ) e. Prime , ( log ` ( p ^ k ) ) , 0 ) ) / ( p ^ k ) ) = ( ( log ` p ) / ( p ^ k ) ) )
199	178, 198	sumeq12dv 13188	. . . . . . 7 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> sum_ k e. ( ( 1 + 1 ) ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) ( ( (Λ ` ( p ^ k ) ) - if ( ( p ^ k ) e. Prime , ( log ` ( p ^ k ) ) , 0 ) ) / ( p ^ k ) ) = sum_ k e. ( 2 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) ( ( log ` p ) / ( p ^ k ) ) )
200	175, 199	oveq12d 6114	. . . . . 6 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( ( ( (Λ ` ( p ^ 1 ) ) - if ( ( p ^ 1 ) e. Prime , ( log ` ( p ^ 1 ) ) , 0 ) ) / ( p ^ 1 ) ) + sum_ k e. ( ( 1 + 1 ) ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) ( ( (Λ ` ( p ^ k ) ) - if ( ( p ^ k ) e. Prime , ( log ` ( p ^ k ) ) , 0 ) ) / ( p ^ k ) ) ) = ( 0 + sum_ k e. ( 2 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) ( ( log ` p ) / ( p ^ k ) ) ) )
201		fzfid 11800	. . . . . . . . 9 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( 2 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) e. Fin )
202	115	adantr 465	. . . . . . . . . . 11 |- ( ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) /\ k e. NN ) -> ( log ` p ) e. RR )
203		nnnn0 10591	. . . . . . . . . . . 12 |- ( k e. NN -> k e. NN0 )
204	56, 203, 103	syl2an 477	. . . . . . . . . . 11 |- ( ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) /\ k e. NN ) -> ( p ^ k ) e. NN )
205	202, 204	nndivred 10375	. . . . . . . . . 10 |- ( ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) /\ k e. NN ) -> ( ( log ` p ) / ( p ^ k ) ) e. RR )
206	182, 205	sylan2 474	. . . . . . . . 9 |- ( ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) /\ k e. ( 2 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) ) -> ( ( log ` p ) / ( p ^ k ) ) e. RR )
207	201, 206	fsumrecl 13216	. . . . . . . 8 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> sum_ k e. ( 2 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) ( ( log ` p ) / ( p ^ k ) ) e. RR )
208	207	recnd 9417	. . . . . . 7 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> sum_ k e. ( 2 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) ( ( log ` p ) / ( p ^ k ) ) e. CC )
209	208	addid2d 9575	. . . . . 6 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( 0 + sum_ k e. ( 2 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) ( ( log ` p ) / ( p ^ k ) ) ) = sum_ k e. ( 2 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) ( ( log ` p ) / ( p ^ k ) ) )
210	156, 200, 209	3eqtrd 2479	. . . . 5 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> sum_ k e. ( 1 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) ( ( (Λ ` ( p ^ k ) ) - if ( ( p ^ k ) e. Prime , ( log ` ( p ^ k ) ) , 0 ) ) / ( p ^ k ) ) = sum_ k e. ( 2 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) ( ( log ` p ) / ( p ^ k ) ) )
211	114	rpreccld 11042	. . . . . . . . . . . 12 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( 1 / p ) e. RR+ )
212	133	flcld 11653	. . . . . . . . . . . . 13 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) e. ZZ )
213	212	peano2zd 10755	. . . . . . . . . . . 12 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) + 1 ) e. ZZ )
214	211, 213	rpexpcld 12036	. . . . . . . . . . 11 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( ( 1 / p ) ^ ( ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) + 1 ) ) e. RR+ )
215	214	rpge0d 11036	. . . . . . . . . 10 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> 0 <_ ( ( 1 / p ) ^ ( ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) + 1 ) ) )
216	56	nnrecred 10372	. . . . . . . . . . . 12 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( 1 / p ) e. RR )
217	216	resqcld 12039	. . . . . . . . . . 11 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( ( 1 / p ) ^ 2 ) e. RR )
218	144	peano2nnd 10344	. . . . . . . . . . . . 13 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) + 1 ) e. NN )
219	218	nnnn0d 10641	. . . . . . . . . . . 12 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) + 1 ) e. NN0 )
220	216, 219	reexpcld 12030	. . . . . . . . . . 11 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( ( 1 / p ) ^ ( ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) + 1 ) ) e. RR )
221	217, 220	subge02d 9936	. . . . . . . . . 10 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( 0 <_ ( ( 1 / p ) ^ ( ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) + 1 ) ) <-> ( ( ( 1 / p ) ^ 2 ) - ( ( 1 / p ) ^ ( ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) + 1 ) ) ) <_ ( ( 1 / p ) ^ 2 ) ) )
222	215, 221	mpbid 210	. . . . . . . . 9 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( ( ( 1 / p ) ^ 2 ) - ( ( 1 / p ) ^ ( ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) + 1 ) ) ) <_ ( ( 1 / p ) ^ 2 ) )
223	117	nnrpd 11031	. . . . . . . . . . . 12 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( p - 1 ) e. RR+ )
224	223	rpcnne0d 11041	. . . . . . . . . . 11 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( ( p - 1 ) e. CC /\ ( p - 1 ) =/= 0 ) )
225	211	rpcnd 11034	. . . . . . . . . . 11 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( 1 / p ) e. CC )
226		dmdcan 10046	. . . . . . . . . . 11 |- ( ( ( ( p - 1 ) e. CC /\ ( p - 1 ) =/= 0 ) /\ ( p e. CC /\ p =/= 0 ) /\ ( 1 / p ) e. CC ) -> ( ( ( p - 1 ) / p ) x. ( ( 1 / p ) / ( p - 1 ) ) ) = ( ( 1 / p ) / p ) )
227	224, 172, 225, 226	syl3anc 1218	. . . . . . . . . 10 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( ( ( p - 1 ) / p ) x. ( ( 1 / p ) / ( p - 1 ) ) ) = ( ( 1 / p ) / p ) )
228	140	recnd 9417	. . . . . . . . . . . . 13 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> 1 e. CC )
229		divsubdir 10032	. . . . . . . . . . . . 13 |- ( ( p e. CC /\ 1 e. CC /\ ( p e. CC /\ p =/= 0 ) ) -> ( ( p - 1 ) / p ) = ( ( p / p ) - ( 1 / p ) ) )
230	157, 228, 172, 229	syl3anc 1218	. . . . . . . . . . . 12 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( ( p - 1 ) / p ) = ( ( p / p ) - ( 1 / p ) ) )
231		divid 10026	. . . . . . . . . . . . . 14 |- ( ( p e. CC /\ p =/= 0 ) -> ( p / p ) = 1 )
232	172, 231	syl 16	. . . . . . . . . . . . 13 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( p / p ) = 1 )
233	232	oveq1d 6111	. . . . . . . . . . . 12 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( ( p / p ) - ( 1 / p ) ) = ( 1 - ( 1 / p ) ) )
234	230, 233	eqtrd 2475	. . . . . . . . . . 11 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( ( p - 1 ) / p ) = ( 1 - ( 1 / p ) ) )
235		divdiv1 10047	. . . . . . . . . . . 12 |- ( ( 1 e. CC /\ ( p e. CC /\ p =/= 0 ) /\ ( ( p - 1 ) e. CC /\ ( p - 1 ) =/= 0 ) ) -> ( ( 1 / p ) / ( p - 1 ) ) = ( 1 / ( p x. ( p - 1 ) ) ) )
236	228, 172, 224, 235	syl3anc 1218	. . . . . . . . . . 11 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( ( 1 / p ) / ( p - 1 ) ) = ( 1 / ( p x. ( p - 1 ) ) ) )
237	234, 236	oveq12d 6114	. . . . . . . . . 10 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( ( ( p - 1 ) / p ) x. ( ( 1 / p ) / ( p - 1 ) ) ) = ( ( 1 - ( 1 / p ) ) x. ( 1 / ( p x. ( p - 1 ) ) ) ) )
238	56	nnne0d 10371	. . . . . . . . . . . 12 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> p =/= 0 )
239	225, 157, 238	divrecd 10115	. . . . . . . . . . 11 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( ( 1 / p ) / p ) = ( ( 1 / p ) x. ( 1 / p ) ) )
240	225	sqvald 12010	. . . . . . . . . . 11 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( ( 1 / p ) ^ 2 ) = ( ( 1 / p ) x. ( 1 / p ) ) )
241	239, 240	eqtr4d 2478	. . . . . . . . . 10 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( ( 1 / p ) / p ) = ( ( 1 / p ) ^ 2 ) )
242	227, 237, 241	3eqtr3d 2483	. . . . . . . . 9 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( ( 1 - ( 1 / p ) ) x. ( 1 / ( p x. ( p - 1 ) ) ) ) = ( ( 1 / p ) ^ 2 ) )
243	222, 242	breqtrrd 4323	. . . . . . . 8 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( ( ( 1 / p ) ^ 2 ) - ( ( 1 / p ) ^ ( ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) + 1 ) ) ) <_ ( ( 1 - ( 1 / p ) ) x. ( 1 / ( p x. ( p - 1 ) ) ) ) )
244	217, 220	resubcld 9781	. . . . . . . . 9 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( ( ( 1 / p ) ^ 2 ) - ( ( 1 / p ) ^ ( ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) + 1 ) ) ) e. RR )
245	118	nnrecred 10372	. . . . . . . . 9 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( 1 / ( p x. ( p - 1 ) ) ) e. RR )
246		resubcl 9678	. . . . . . . . . 10 |- ( ( 1 e. RR /\ ( 1 / p ) e. RR ) -> ( 1 - ( 1 / p ) ) e. RR )
247	139, 216, 246	sylancr 663	. . . . . . . . 9 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( 1 - ( 1 / p ) ) e. RR )
248		recgt1 10233	. . . . . . . . . . . 12 |- ( ( p e. RR /\ 0 < p ) -> ( 1 < p <-> ( 1 / p ) < 1 ) )
249	57, 124, 248	syl2anc 661	. . . . . . . . . . 11 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( 1 < p <-> ( 1 / p ) < 1 ) )
250	131, 249	mpbid 210	. . . . . . . . . 10 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( 1 / p ) < 1 )
251		posdif 9837	. . . . . . . . . . 11 |- ( ( ( 1 / p ) e. RR /\ 1 e. RR ) -> ( ( 1 / p ) < 1 <-> 0 < ( 1 - ( 1 / p ) ) ) )
252	216, 139, 251	sylancl 662	. . . . . . . . . 10 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( ( 1 / p ) < 1 <-> 0 < ( 1 - ( 1 / p ) ) ) )
253	250, 252	mpbid 210	. . . . . . . . 9 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> 0 < ( 1 - ( 1 / p ) ) )
254		ledivmul 10210	. . . . . . . . 9 |- ( ( ( ( ( 1 / p ) ^ 2 ) - ( ( 1 / p ) ^ ( ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) + 1 ) ) ) e. RR /\ ( 1 / ( p x. ( p - 1 ) ) ) e. RR /\ ( ( 1 - ( 1 / p ) ) e. RR /\ 0 < ( 1 - ( 1 / p ) ) ) ) -> ( ( ( ( ( 1 / p ) ^ 2 ) - ( ( 1 / p ) ^ ( ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) + 1 ) ) ) / ( 1 - ( 1 / p ) ) ) <_ ( 1 / ( p x. ( p - 1 ) ) ) <-> ( ( ( 1 / p ) ^ 2 ) - ( ( 1 / p ) ^ ( ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) + 1 ) ) ) <_ ( ( 1 - ( 1 / p ) ) x. ( 1 / ( p x. ( p - 1 ) ) ) ) ) )
255	244, 245, 247, 253, 254	syl112anc 1222	. . . . . . . 8 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( ( ( ( ( 1 / p ) ^ 2 ) - ( ( 1 / p ) ^ ( ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) + 1 ) ) ) / ( 1 - ( 1 / p ) ) ) <_ ( 1 / ( p x. ( p - 1 ) ) ) <-> ( ( ( 1 / p ) ^ 2 ) - ( ( 1 / p ) ^ ( ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) + 1 ) ) ) <_ ( ( 1 - ( 1 / p ) ) x. ( 1 / ( p x. ( p - 1 ) ) ) ) ) )
256	243, 255	mpbird 232	. . . . . . 7 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( ( ( ( 1 / p ) ^ 2 ) - ( ( 1 / p ) ^ ( ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) + 1 ) ) ) / ( 1 - ( 1 / p ) ) ) <_ ( 1 / ( p x. ( p - 1 ) ) ) )
257	247, 253	elrpd 11030	. . . . . . . . 9 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( 1 - ( 1 / p ) ) e. RR+ )
258	244, 257	rerpdivcld 11059	. . . . . . . 8 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( ( ( ( 1 / p ) ^ 2 ) - ( ( 1 / p ) ^ ( ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) + 1 ) ) ) / ( 1 - ( 1 / p ) ) ) e. RR )
259	258, 245, 132	lemul2d 11072	. . . . . . 7 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( ( ( ( ( 1 / p ) ^ 2 ) - ( ( 1 / p ) ^ ( ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) + 1 ) ) ) / ( 1 - ( 1 / p ) ) ) <_ ( 1 / ( p x. ( p - 1 ) ) ) <-> ( ( log ` p ) x. ( ( ( ( 1 / p ) ^ 2 ) - ( ( 1 / p ) ^ ( ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) + 1 ) ) ) / ( 1 - ( 1 / p ) ) ) ) <_ ( ( log ` p ) x. ( 1 / ( p x. ( p - 1 ) ) ) ) ) )
260	256, 259	mpbid 210	. . . . . 6 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( ( log ` p ) x. ( ( ( ( 1 / p ) ^ 2 ) - ( ( 1 / p ) ^ ( ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) + 1 ) ) ) / ( 1 - ( 1 / p ) ) ) ) <_ ( ( log ` p ) x. ( 1 / ( p x. ( p - 1 ) ) ) ) )
261	134	adantr 465	. . . . . . . . . . 11 |- ( ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) /\ k e. NN ) -> ( log ` p ) e. CC )
262	204	nncnd 10343	. . . . . . . . . . 11 |- ( ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) /\ k e. NN ) -> ( p ^ k ) e. CC )
263	204	nnne0d 10371	. . . . . . . . . . 11 |- ( ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) /\ k e. NN ) -> ( p ^ k ) =/= 0 )
264	261, 262, 263	divrecd 10115	. . . . . . . . . 10 |- ( ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) /\ k e. NN ) -> ( ( log ` p ) / ( p ^ k ) ) = ( ( log ` p ) x. ( 1 / ( p ^ k ) ) ) )
265	157	adantr 465	. . . . . . . . . . . 12 |- ( ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) /\ k e. NN ) -> p e. CC )
266	56	adantr 465	. . . . . . . . . . . . 13 |- ( ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) /\ k e. NN ) -> p e. NN )
267	266	nnne0d 10371	. . . . . . . . . . . 12 |- ( ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) /\ k e. NN ) -> p =/= 0 )
268		nnz 10673	. . . . . . . . . . . . 13 |- ( k e. NN -> k e. ZZ )
269	268	adantl 466	. . . . . . . . . . . 12 |- ( ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) /\ k e. NN ) -> k e. ZZ )
270	265, 267, 269	exprecd 12021	. . . . . . . . . . 11 |- ( ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) /\ k e. NN ) -> ( ( 1 / p ) ^ k ) = ( 1 / ( p ^ k ) ) )
271	270	oveq2d 6112	. . . . . . . . . 10 |- ( ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) /\ k e. NN ) -> ( ( log ` p ) x. ( ( 1 / p ) ^ k ) ) = ( ( log ` p ) x. ( 1 / ( p ^ k ) ) ) )
272	264, 271	eqtr4d 2478	. . . . . . . . 9 |- ( ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) /\ k e. NN ) -> ( ( log ` p ) / ( p ^ k ) ) = ( ( log ` p ) x. ( ( 1 / p ) ^ k ) ) )
273	182, 272	sylan2 474	. . . . . . . 8 |- ( ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) /\ k e. ( 2 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) ) -> ( ( log ` p ) / ( p ^ k ) ) = ( ( log ` p ) x. ( ( 1 / p ) ^ k ) ) )
274	273	sumeq2dv 13185	. . . . . . 7 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> sum_ k e. ( 2 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) ( ( log ` p ) / ( p ^ k ) ) = sum_ k e. ( 2 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) ( ( log ` p ) x. ( ( 1 / p ) ^ k ) ) )
275	182	nnnn0d 10641	. . . . . . . . 9 |- ( k e. ( 2 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) -> k e. NN0 )
276		expcl 11888	. . . . . . . . 9 |- ( ( ( 1 / p ) e. CC /\ k e. NN0 ) -> ( ( 1 / p ) ^ k ) e. CC )
277	225, 275, 276	syl2an 477	. . . . . . . 8 |- ( ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) /\ k e. ( 2 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) ) -> ( ( 1 / p ) ^ k ) e. CC )
278	201, 134, 277	fsummulc2 13256	. . . . . . 7 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( ( log ` p ) x. sum_ k e. ( 2 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) ( ( 1 / p ) ^ k ) ) = sum_ k e. ( 2 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) ( ( log ` p ) x. ( ( 1 / p ) ^ k ) ) )
279		fzval3 11610	. . . . . . . . . . 11 |- ( ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) e. ZZ -> ( 2 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) = ( 2..^ ( ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) + 1 ) ) )
280	212, 279	syl 16	. . . . . . . . . 10 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( 2 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) = ( 2..^ ( ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) + 1 ) ) )
281	280	sumeq1d 13183	. . . . . . . . 9 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> sum_ k e. ( 2 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) ( ( 1 / p ) ^ k ) = sum_ k e. ( 2..^ ( ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) + 1 ) ) ( ( 1 / p ) ^ k ) )
282	216, 250	ltned 9515	. . . . . . . . . 10 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( 1 / p ) =/= 1 )
283		2nn0 10601	. . . . . . . . . . 11 |- 2 e. NN0
284	283	a1i 11	. . . . . . . . . 10 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> 2 e. NN0 )
285		eluzp1p1 10891	. . . . . . . . . . . 12 |- ( ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) e. ( ZZ>= ` 1 ) -> ( ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) + 1 ) e. ( ZZ>= ` ( 1 + 1 ) ) )
286	146, 285	syl 16	. . . . . . . . . . 11 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) + 1 ) e. ( ZZ>= ` ( 1 + 1 ) ) )
287		df-2 10385	. . . . . . . . . . . 12 |- 2 = ( 1 + 1 )
288	287	fveq2i 5699	. . . . . . . . . . 11 |- ( ZZ>= ` 2 ) = ( ZZ>= ` ( 1 + 1 ) )
289	286, 288	syl6eleqr 2534	. . . . . . . . . 10 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) + 1 ) e. ( ZZ>= ` 2 ) )
290	225, 282, 284, 289	geoserg 13333	. . . . . . . . 9 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> sum_ k e. ( 2..^ ( ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) + 1 ) ) ( ( 1 / p ) ^ k ) = ( ( ( ( 1 / p ) ^ 2 ) - ( ( 1 / p ) ^ ( ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) + 1 ) ) ) / ( 1 - ( 1 / p ) ) ) )
291	281, 290	eqtrd 2475	. . . . . . . 8 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> sum_ k e. ( 2 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) ( ( 1 / p ) ^ k ) = ( ( ( ( 1 / p ) ^ 2 ) - ( ( 1 / p ) ^ ( ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) + 1 ) ) ) / ( 1 - ( 1 / p ) ) ) )
292	291	oveq2d 6112	. . . . . . 7 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( ( log ` p ) x. sum_ k e. ( 2 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) ( ( 1 / p ) ^ k ) ) = ( ( log ` p ) x. ( ( ( ( 1 / p ) ^ 2 ) - ( ( 1 / p ) ^ ( ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) + 1 ) ) ) / ( 1 - ( 1 / p ) ) ) ) )
293	274, 278, 292	3eqtr2d 2481	. . . . . 6 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> sum_ k e. ( 2 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) ( ( log ` p ) / ( p ^ k ) ) = ( ( log ` p ) x. ( ( ( ( 1 / p ) ^ 2 ) - ( ( 1 / p ) ^ ( ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) + 1 ) ) ) / ( 1 - ( 1 / p ) ) ) ) )
294	118	nncnd 10343	. . . . . . 7 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( p x. ( p - 1 ) ) e. CC )
295	118	nnne0d 10371	. . . . . . 7 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( p x. ( p - 1 ) ) =/= 0 )
296	134, 294, 295	divrecd 10115	. . . . . 6 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> ( ( log ` p ) / ( p x. ( p - 1 ) ) ) = ( ( log ` p ) x. ( 1 / ( p x. ( p - 1 ) ) ) ) )
297	260, 293, 296	3brtr4d 4327	. . . . 5 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> sum_ k e. ( 2 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) ( ( log ` p ) / ( p ^ k ) ) <_ ( ( log ` p ) / ( p x. ( p - 1 ) ) ) )
298	210, 297	eqbrtrd 4317	. . . 4 |- ( ( A e. ZZ /\ p e. ( ( 0 [,] A ) i^i Prime ) ) -> sum_ k e. ( 1 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) ( ( (Λ ` ( p ^ k ) ) - if ( ( p ^ k ) e. Prime , ( log ` ( p ^ k ) ) , 0 ) ) / ( p ^ k ) ) <_ ( ( log ` p ) / ( p x. ( p - 1 ) ) ) )
299	90, 112, 119, 298	fsumle 13267	. . 3 |- ( A e. ZZ -> sum_ p e. ( ( 0 [,] A ) i^i Prime ) sum_ k e. ( 1 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) ( ( (Λ ` ( p ^ k ) ) - if ( ( p ^ k ) e. Prime , ( log ` ( p ^ k ) ) , 0 ) ) / ( p ^ k ) ) <_ sum_ p e. ( ( 0 [,] A ) i^i Prime ) ( ( log ` p ) / ( p x. ( p - 1 ) ) ) )
300		elfzuz 11454	. . . . . . . . . . 11 |- ( p e. ( 2 ... ( ( abs ` A ) + 1 ) ) -> p e. ( ZZ>= ` 2 ) )
301	128	simplbi 460	. . . . . . . . . . 11 |- ( p e. ( ZZ>= ` 2 ) -> p e. NN )
302	300, 301	syl 16	. . . . . . . . . 10 |- ( p e. ( 2 ... ( ( abs ` A ) + 1 ) ) -> p e. NN )
303	302	adantl 466	. . . . . . . . 9 |- ( ( A e. ZZ /\ p e. ( 2 ... ( ( abs ` A ) + 1 ) ) ) -> p e. NN )
304	303	nnred 10342	. . . . . . . 8 |- ( ( A e. ZZ /\ p e. ( 2 ... ( ( abs ` A ) + 1 ) ) ) -> p e. RR )
305	300	adantl 466	. . . . . . . . 9 |- ( ( A e. ZZ /\ p e. ( 2 ... ( ( abs ` A ) + 1 ) ) ) -> p e. ( ZZ>= ` 2 ) )
306	305, 129	syl 16	. . . . . . . 8 |- ( ( A e. ZZ /\ p e. ( 2 ... ( ( abs ` A ) + 1 ) ) ) -> 1 < p )
307	304, 306	rplogcld 22083	. . . . . . 7 |- ( ( A e. ZZ /\ p e. ( 2 ... ( ( abs ` A ) + 1 ) ) ) -> ( log ` p ) e. RR+ )
308	305, 116	syl 16	. . . . . . . . 9 |- ( ( A e. ZZ /\ p e. ( 2 ... ( ( abs ` A ) + 1 ) ) ) -> ( p - 1 ) e. NN )
309	303, 308	nnmulcld 10374	. . . . . . . 8 |- ( ( A e. ZZ /\ p e. ( 2 ... ( ( abs ` A ) + 1 ) ) ) -> ( p x. ( p - 1 ) ) e. NN )
310	309	nnrpd 11031	. . . . . . 7 |- ( ( A e. ZZ /\ p e. ( 2 ... ( ( abs ` A ) + 1 ) ) ) -> ( p x. ( p - 1 ) ) e. RR+ )
311	307, 310	rpdivcld 11049	. . . . . 6 |- ( ( A e. ZZ /\ p e. ( 2 ... ( ( abs ` A ) + 1 ) ) ) -> ( ( log ` p ) / ( p x. ( p - 1 ) ) ) e. RR+ )
312	311	rpred 11032	. . . . 5 |- ( ( A e. ZZ /\ p e. ( 2 ... ( ( abs ` A ) + 1 ) ) ) -> ( ( log ` p ) / ( p x. ( p - 1 ) ) ) e. RR )
313	51, 312	fsumrecl 13216	. . . 4 |- ( A e. ZZ -> sum_ p e. ( 2 ... ( ( abs ` A ) + 1 ) ) ( ( log ` p ) / ( p x. ( p - 1 ) ) ) e. RR )
314	311	rpge0d 11036	. . . . 5 |- ( ( A e. ZZ /\ p e. ( 2 ... ( ( abs ` A ) + 1 ) ) ) -> 0 <_ ( ( log ` p ) / ( p x. ( p - 1 ) ) ) )
315	51, 312, 314, 88	fsumless 13264	. . . 4 |- ( A e. ZZ -> sum_ p e. ( ( 0 [,] A ) i^i Prime ) ( ( log ` p ) / ( p x. ( p - 1 ) ) ) <_ sum_ p e. ( 2 ... ( ( abs ` A ) + 1 ) ) ( ( log ` p ) / ( p x. ( p - 1 ) ) ) )
316		rplogsumlem1 22738	. . . . 5 |- ( ( ( abs ` A ) + 1 ) e. NN -> sum_ p e. ( 2 ... ( ( abs ` A ) + 1 ) ) ( ( log ` p ) / ( p x. ( p - 1 ) ) ) <_ 2 )
317	81, 316	syl 16	. . . 4 |- ( A e. ZZ -> sum_ p e. ( 2 ... ( ( abs ` A ) + 1 ) ) ( ( log ` p ) / ( p x. ( p - 1 ) ) ) <_ 2 )
318	120, 313, 122, 315, 317	letrd 9533	. . 3 |- ( A e. ZZ -> sum_ p e. ( ( 0 [,] A ) i^i Prime ) ( ( log ` p ) / ( p x. ( p - 1 ) ) ) <_ 2 )
319	113, 120, 122, 299, 318	letrd 9533	. 2 |- ( A e. ZZ -> sum_ p e. ( ( 0 [,] A ) i^i Prime ) sum_ k e. ( 1 ... ( |_ ` ( ( log ` A ) / ( log ` p ) ) ) ) ( ( (Λ ` ( p ^ k ) ) - if ( ( p ^ k ) e. Prime , ( log ` ( p ^ k ) ) , 0 ) ) / ( p ^ k ) ) <_ 2 )
320	50, 319	eqbrtrd 4317	1 |- ( A e. ZZ -> sum_ n e. ( 1 ... A ) ( ( (Λ ` n ) - if ( n e. Prime , ( log ` n ) , 0 ) ) / n ) <_ 2 )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 184   /\ wa 369   /\ w3a 965   = wceq 1369   e. wcel 1756   =/= wne 2611   i^i cin 3332   C_ wss 3333   ifcif 3796   class class class wbr 4297   ` cfv 5423  (class class class)co 6096   Fincfn 7315   CCcc 9285   RRcr 9286   0cc0 9287   1c1 9288   + caddc 9290   x. cmul 9292   < clt 9423   <_ cle 9424   - cmin 9600   / cdiv 9998   NNcn 10327   2c2 10376   NN0cn0 10584   ZZcz 10651   ZZ>=cuz 10866   QQcq 10958   RR+crp 10996   [,]cicc 11308   ...cfz 11442  ..^cfzo 11553   |_cfl 11645   ^cexp 11870   abscabs 12728   sum_csu 13168   Primecprime 13768   logclog 22011  Λcvma 22434

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-rep 4408  ax-sep 4418  ax-nul 4426  ax-pow 4475  ax-pr 4536  ax-un 6377  ax-inf2 7852  ax-cnex 9343  ax-resscn 9344  ax-1cn 9345  ax-icn 9346  ax-addcl 9347  ax-addrcl 9348  ax-mulcl 9349  ax-mulrcl 9350  ax-mulcom 9351  ax-addass 9352  ax-mulass 9353  ax-distr 9354  ax-i2m1 9355  ax-1ne0 9356  ax-1rid 9357  ax-rnegex 9358  ax-rrecex 9359  ax-cnre 9360  ax-pre-lttri 9361  ax-pre-lttrn 9362  ax-pre-ltadd 9363  ax-pre-mulgt0 9364  ax-pre-sup 9365  ax-addf 9366  ax-mulf 9367

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-fal 1375  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2573  df-ne 2613  df-nel 2614  df-ral 2725  df-rex 2726  df-reu 2727  df-rmo 2728  df-rab 2729  df-v 2979  df-sbc 3192  df-csb 3294  df-dif 3336  df-un 3338  df-in 3340  df-ss 3347  df-pss 3349  df-nul 3643  df-if 3797  df-pw 3867  df-sn 3883  df-pr 3885  df-tp 3887  df-op 3889  df-uni 4097  df-int 4134  df-iun 4178  df-iin 4179  df-br 4298  df-opab 4356  df-mpt 4357  df-tr 4391  df-eprel 4637  df-id 4641  df-po 4646  df-so 4647  df-fr 4684  df-se 4685  df-we 4686  df-ord 4727  df-on 4728  df-lim 4729  df-suc 4730  df-xp 4851  df-rel 4852  df-cnv 4853  df-co 4854  df-dm 4855  df-rn 4856  df-res 4857  df-ima 4858  df-iota 5386  df-fun 5425  df-fn 5426  df-f 5427  df-f1 5428  df-fo 5429  df-f1o 5430  df-fv 5431  df-isom 5432  df-riota 6057  df-ov 6099  df-oprab 6100  df-mpt2 6101  df-of 6325  df-om 6482  df-1st 6582  df-2nd 6583  df-supp 6696  df-recs 6837  df-rdg 6871  df-1o 6925  df-2o 6926  df-oadd 6929  df-er 7106  df-map 7221  df-pm 7222  df-ixp 7269  df-en 7316  df-dom 7317  df-sdom 7318  df-fin 7319  df-fsupp 7626  df-fi 7666  df-sup 7696  df-oi 7729  df-card 8114  df-cda 8342  df-pnf 9425  df-mnf 9426  df-xr 9427  df-ltxr 9428  df-le 9429  df-sub 9602  df-neg 9603  df-div 9999  df-nn 10328  df-2 10385  df-3 10386  df-4 10387  df-5 10388  df-6 10389  df-7 10390  df-8 10391  df-9 10392  df-10 10393  df-n0 10585  df-z 10652  df-dec 10761  df-uz 10867  df-q 10959  df-rp 10997  df-xneg 11094  df-xadd 11095  df-xmul 11096  df-ioo 11309  df-ioc 11310  df-ico 11311  df-icc 11312  df-fz 11443  df-fzo 11554  df-fl 11647  df-mod 11714  df-seq 11812  df-exp 11871  df-fac 12057  df-bc 12084  df-hash 12109  df-shft 12561  df-cj 12593  df-re 12594  df-im 12595  df-sqr 12729  df-abs 12730  df-limsup 12954  df-clim 12971  df-rlim 12972  df-sum 13169  df-ef 13358  df-sin 13360  df-cos 13361  df-tan 13362  df-pi 13363  df-dvds 13541  df-gcd 13696  df-prm 13769  df-pc 13909  df-struct 14181  df-ndx 14182  df-slot 14183  df-base 14184  df-sets 14185  df-ress 14186  df-plusg 14256  df-mulr 14257  df-starv 14258  df-sca 14259  df-vsca 14260  df-ip 14261  df-tset 14262  df-ple 14263  df-ds 14265  df-unif 14266  df-hom 14267  df-cco 14268  df-rest 14366  df-topn 14367  df-0g 14385  df-gsum 14386  df-topgen 14387  df-pt 14388  df-prds 14391  df-xrs 14445  df-qtop 14450  df-imas 14451  df-xps 14453  df-mre 14529  df-mrc 14530  df-acs 14532  df-mnd 15420  df-submnd 15470  df-mulg 15553  df-cntz 15840  df-cmn 16284  df-psmet 17814  df-xmet 17815  df-met 17816  df-bl 17817  df-mopn 17818  df-fbas 17819  df-fg 17820  df-cnfld 17824  df-top 18508  df-bases 18510  df-topon 18511  df-topsp 18512  df-cld 18628  df-ntr 18629  df-cls 18630  df-nei 18707  df-lp 18745  df-perf 18746  df-cn 18836  df-cnp 18837  df-haus 18924  df-cmp 18995  df-tx 19140  df-hmeo 19333  df-fil 19424  df-fm 19516  df-flim 19517  df-flf 19518  df-xms 19900  df-ms 19901  df-tms 19902  df-cncf 20459  df-limc 21346  df-dv 21347  df-log 22013  df-cxp 22014  df-vma 22440

This theorem is referenced by:  rplogsum  22781