prmorcht

Description: Relate the primorial (product of the first n primes) to the Chebyshev function. (Contributed by Mario Carneiro, 22-Sep-2014)

		Ref	Expression
	Hypothesis	prmorcht.1	\|- F = ( n e. NN \|-> if ( n e. Prime , n , 1 ) )
	Assertion	prmorcht	\|- ( A e. NN -> ( exp ` ( theta ` A ) ) = ( seq 1 ( x. , F ) ` A ) )

Proof

Step	Hyp	Ref	Expression
1		prmorcht.1	\|- F = ( n e. NN \|-> if ( n e. Prime , n , 1 ) )
2		nnre	\|- ( A e. NN -> A e. RR )
3		chtval	\|- ( A e. RR -> ( theta ` A ) = sum_ k e. ( ( 0 [,] A ) i^i Prime ) ( log ` k ) )
4	2 3	syl	\|- ( A e. NN -> ( theta ` A ) = sum_ k e. ( ( 0 [,] A ) i^i Prime ) ( log ` k ) )
5		2eluzge1	\|- 2 e. ( ZZ>= ` 1 )
6		ppisval2	\|- ( ( A e. RR /\ 2 e. ( ZZ>= ` 1 ) ) -> ( ( 0 [,] A ) i^i Prime ) = ( ( 1 ... ( \|_ ` A ) ) i^i Prime ) )
7	2 5 6	sylancl	\|- ( A e. NN -> ( ( 0 [,] A ) i^i Prime ) = ( ( 1 ... ( \|_ ` A ) ) i^i Prime ) )
8		nnz	\|- ( A e. NN -> A e. ZZ )
9		flid	\|- ( A e. ZZ -> ( \|_ ` A ) = A )
10	8 9	syl	\|- ( A e. NN -> ( \|_ ` A ) = A )
11	10	oveq2d	\|- ( A e. NN -> ( 1 ... ( \|_ ` A ) ) = ( 1 ... A ) )
12	11	ineq1d	\|- ( A e. NN -> ( ( 1 ... ( \|_ ` A ) ) i^i Prime ) = ( ( 1 ... A ) i^i Prime ) )
13	7 12	eqtrd	\|- ( A e. NN -> ( ( 0 [,] A ) i^i Prime ) = ( ( 1 ... A ) i^i Prime ) )
14	13	sumeq1d	\|- ( A e. NN -> sum_ k e. ( ( 0 [,] A ) i^i Prime ) ( log ` k ) = sum_ k e. ( ( 1 ... A ) i^i Prime ) ( log ` k ) )
15		inss1	\|- ( ( 1 ... A ) i^i Prime ) C_ ( 1 ... A )
16		elinel1	\|- ( k e. ( ( 1 ... A ) i^i Prime ) -> k e. ( 1 ... A ) )
17		elfznn	\|- ( k e. ( 1 ... A ) -> k e. NN )
18	17	adantl	\|- ( ( A e. NN /\ k e. ( 1 ... A ) ) -> k e. NN )
19	18	nnrpd	\|- ( ( A e. NN /\ k e. ( 1 ... A ) ) -> k e. RR+ )
20	19	relogcld	\|- ( ( A e. NN /\ k e. ( 1 ... A ) ) -> ( log ` k ) e. RR )
21	20	recnd	\|- ( ( A e. NN /\ k e. ( 1 ... A ) ) -> ( log ` k ) e. CC )
22	16 21	sylan2	\|- ( ( A e. NN /\ k e. ( ( 1 ... A ) i^i Prime ) ) -> ( log ` k ) e. CC )
23	22	ralrimiva	\|- ( A e. NN -> A. k e. ( ( 1 ... A ) i^i Prime ) ( log ` k ) e. CC )
24		fzfi	\|- ( 1 ... A ) e. Fin
25	24	olci	\|- ( ( 1 ... A ) C_ ( ZZ>= ` 1 ) \/ ( 1 ... A ) e. Fin )
26		sumss2	\|- ( ( ( ( ( 1 ... A ) i^i Prime ) C_ ( 1 ... A ) /\ A. k e. ( ( 1 ... A ) i^i Prime ) ( log ` k ) e. CC ) /\ ( ( 1 ... A ) C_ ( ZZ>= ` 1 ) \/ ( 1 ... A ) e. Fin ) ) -> sum_ k e. ( ( 1 ... A ) i^i Prime ) ( log ` k ) = sum_ k e. ( 1 ... A ) if ( k e. ( ( 1 ... A ) i^i Prime ) , ( log ` k ) , 0 ) )
27	25 26	mpan2	\|- ( ( ( ( 1 ... A ) i^i Prime ) C_ ( 1 ... A ) /\ A. k e. ( ( 1 ... A ) i^i Prime ) ( log ` k ) e. CC ) -> sum_ k e. ( ( 1 ... A ) i^i Prime ) ( log ` k ) = sum_ k e. ( 1 ... A ) if ( k e. ( ( 1 ... A ) i^i Prime ) , ( log ` k ) , 0 ) )
28	15 23 27	sylancr	\|- ( A e. NN -> sum_ k e. ( ( 1 ... A ) i^i Prime ) ( log ` k ) = sum_ k e. ( 1 ... A ) if ( k e. ( ( 1 ... A ) i^i Prime ) , ( log ` k ) , 0 ) )
29	14 28	eqtrd	\|- ( A e. NN -> sum_ k e. ( ( 0 [,] A ) i^i Prime ) ( log ` k ) = sum_ k e. ( 1 ... A ) if ( k e. ( ( 1 ... A ) i^i Prime ) , ( log ` k ) , 0 ) )
30	4 29	eqtrd	\|- ( A e. NN -> ( theta ` A ) = sum_ k e. ( 1 ... A ) if ( k e. ( ( 1 ... A ) i^i Prime ) , ( log ` k ) , 0 ) )
31		elin	\|- ( k e. ( ( 1 ... A ) i^i Prime ) <-> ( k e. ( 1 ... A ) /\ k e. Prime ) )
32	31	baibr	\|- ( k e. ( 1 ... A ) -> ( k e. Prime <-> k e. ( ( 1 ... A ) i^i Prime ) ) )
33	32	ifbid	\|- ( k e. ( 1 ... A ) -> if ( k e. Prime , ( log ` k ) , 0 ) = if ( k e. ( ( 1 ... A ) i^i Prime ) , ( log ` k ) , 0 ) )
34	33	sumeq2i	\|- sum_ k e. ( 1 ... A ) if ( k e. Prime , ( log ` k ) , 0 ) = sum_ k e. ( 1 ... A ) if ( k e. ( ( 1 ... A ) i^i Prime ) , ( log ` k ) , 0 )
35	30 34	eqtr4di	\|- ( A e. NN -> ( theta ` A ) = sum_ k e. ( 1 ... A ) if ( k e. Prime , ( log ` k ) , 0 ) )
36		eleq1w	\|- ( n = k -> ( n e. Prime <-> k e. Prime ) )
37		fveq2	\|- ( n = k -> ( log ` n ) = ( log ` k ) )
38	36 37	ifbieq1d	\|- ( n = k -> if ( n e. Prime , ( log ` n ) , 0 ) = if ( k e. Prime , ( log ` k ) , 0 ) )
39		eqid	\|- ( n e. NN \|-> if ( n e. Prime , ( log ` n ) , 0 ) ) = ( n e. NN \|-> if ( n e. Prime , ( log ` n ) , 0 ) )
40		fvex	\|- ( log ` k ) e. _V
41		0cn	\|- 0 e. CC
42	41	elexi	\|- 0 e. _V
43	40 42	ifex	\|- if ( k e. Prime , ( log ` k ) , 0 ) e. _V
44	38 39 43	fvmpt	\|- ( k e. NN -> ( ( n e. NN \|-> if ( n e. Prime , ( log ` n ) , 0 ) ) ` k ) = if ( k e. Prime , ( log ` k ) , 0 ) )
45	18 44	syl	\|- ( ( A e. NN /\ k e. ( 1 ... A ) ) -> ( ( n e. NN \|-> if ( n e. Prime , ( log ` n ) , 0 ) ) ` k ) = if ( k e. Prime , ( log ` k ) , 0 ) )
46		elnnuz	\|- ( A e. NN <-> A e. ( ZZ>= ` 1 ) )
47	46	biimpi	\|- ( A e. NN -> A e. ( ZZ>= ` 1 ) )
48		ifcl	\|- ( ( ( log ` k ) e. CC /\ 0 e. CC ) -> if ( k e. Prime , ( log ` k ) , 0 ) e. CC )
49	21 41 48	sylancl	\|- ( ( A e. NN /\ k e. ( 1 ... A ) ) -> if ( k e. Prime , ( log ` k ) , 0 ) e. CC )
50	45 47 49	fsumser	\|- ( A e. NN -> sum_ k e. ( 1 ... A ) if ( k e. Prime , ( log ` k ) , 0 ) = ( seq 1 ( + , ( n e. NN \|-> if ( n e. Prime , ( log ` n ) , 0 ) ) ) ` A ) )
51	35 50	eqtrd	\|- ( A e. NN -> ( theta ` A ) = ( seq 1 ( + , ( n e. NN \|-> if ( n e. Prime , ( log ` n ) , 0 ) ) ) ` A ) )
52	51	fveq2d	\|- ( A e. NN -> ( exp ` ( theta ` A ) ) = ( exp ` ( seq 1 ( + , ( n e. NN \|-> if ( n e. Prime , ( log ` n ) , 0 ) ) ) ` A ) ) )
53		addcl	\|- ( ( k e. CC /\ p e. CC ) -> ( k + p ) e. CC )
54	53	adantl	\|- ( ( A e. NN /\ ( k e. CC /\ p e. CC ) ) -> ( k + p ) e. CC )
55	45 49	eqeltrd	\|- ( ( A e. NN /\ k e. ( 1 ... A ) ) -> ( ( n e. NN \|-> if ( n e. Prime , ( log ` n ) , 0 ) ) ` k ) e. CC )
56		efadd	\|- ( ( k e. CC /\ p e. CC ) -> ( exp ` ( k + p ) ) = ( ( exp ` k ) x. ( exp ` p ) ) )
57	56	adantl	\|- ( ( A e. NN /\ ( k e. CC /\ p e. CC ) ) -> ( exp ` ( k + p ) ) = ( ( exp ` k ) x. ( exp ` p ) ) )
58		1nn	\|- 1 e. NN
59		ifcl	\|- ( ( k e. NN /\ 1 e. NN ) -> if ( k e. Prime , k , 1 ) e. NN )
60	18 58 59	sylancl	\|- ( ( A e. NN /\ k e. ( 1 ... A ) ) -> if ( k e. Prime , k , 1 ) e. NN )
61	60	nnrpd	\|- ( ( A e. NN /\ k e. ( 1 ... A ) ) -> if ( k e. Prime , k , 1 ) e. RR+ )
62	61	reeflogd	\|- ( ( A e. NN /\ k e. ( 1 ... A ) ) -> ( exp ` ( log ` if ( k e. Prime , k , 1 ) ) ) = if ( k e. Prime , k , 1 ) )
63		fvif	\|- ( log ` if ( k e. Prime , k , 1 ) ) = if ( k e. Prime , ( log ` k ) , ( log ` 1 ) )
64		log1	\|- ( log ` 1 ) = 0
65		ifeq2	\|- ( ( log ` 1 ) = 0 -> if ( k e. Prime , ( log ` k ) , ( log ` 1 ) ) = if ( k e. Prime , ( log ` k ) , 0 ) )
66	64 65	ax-mp	\|- if ( k e. Prime , ( log ` k ) , ( log ` 1 ) ) = if ( k e. Prime , ( log ` k ) , 0 )
67	63 66	eqtri	\|- ( log ` if ( k e. Prime , k , 1 ) ) = if ( k e. Prime , ( log ` k ) , 0 )
68	45 67	eqtr4di	\|- ( ( A e. NN /\ k e. ( 1 ... A ) ) -> ( ( n e. NN \|-> if ( n e. Prime , ( log ` n ) , 0 ) ) ` k ) = ( log ` if ( k e. Prime , k , 1 ) ) )
69	68	fveq2d	\|- ( ( A e. NN /\ k e. ( 1 ... A ) ) -> ( exp ` ( ( n e. NN \|-> if ( n e. Prime , ( log ` n ) , 0 ) ) ` k ) ) = ( exp ` ( log ` if ( k e. Prime , k , 1 ) ) ) )
70		id	\|- ( n = k -> n = k )
71	36 70	ifbieq1d	\|- ( n = k -> if ( n e. Prime , n , 1 ) = if ( k e. Prime , k , 1 ) )
72		vex	\|- k e. _V
73	58	elexi	\|- 1 e. _V
74	72 73	ifex	\|- if ( k e. Prime , k , 1 ) e. _V
75	71 1 74	fvmpt	\|- ( k e. NN -> ( F ` k ) = if ( k e. Prime , k , 1 ) )
76	18 75	syl	\|- ( ( A e. NN /\ k e. ( 1 ... A ) ) -> ( F ` k ) = if ( k e. Prime , k , 1 ) )
77	62 69 76	3eqtr4d	\|- ( ( A e. NN /\ k e. ( 1 ... A ) ) -> ( exp ` ( ( n e. NN \|-> if ( n e. Prime , ( log ` n ) , 0 ) ) ` k ) ) = ( F ` k ) )
78	54 55 47 57 77	seqhomo	\|- ( A e. NN -> ( exp ` ( seq 1 ( + , ( n e. NN \|-> if ( n e. Prime , ( log ` n ) , 0 ) ) ) ` A ) ) = ( seq 1 ( x. , F ) ` A ) )
79	52 78	eqtrd	\|- ( A e. NN -> ( exp ` ( theta ` A ) ) = ( seq 1 ( x. , F ) ` A ) )

Metamath Proof Explorer

Theorem prmorcht

Proof