Theorem chpval2

Description: Express the second Chebyshev function directly as a sum over the primes less than A (instead of indirectly through the von Mangoldt function). (Contributed by Mario Carneiro, 8-Apr-2016)

	Ref	Expression
Assertion	chpval2	⊢ ( 𝐴 ∈ ℝ → ( ψ ‘ 𝐴 ) = Σ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ( ( log ‘ 𝑝 ) · ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		chpval	⊢ ( 𝐴 ∈ ℝ → ( ψ ‘ 𝐴 ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( Λ ‘ 𝑛 ) )
2		fveq2	⊢ ( 𝑛 = ( 𝑝 ↑ 𝑘 ) → ( Λ ‘ 𝑛 ) = ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) )
3		id	⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℝ )
4		elfznn	⊢ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) → 𝑛 ∈ ℕ )
5	4	adantl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → 𝑛 ∈ ℕ )
6		vmacl	⊢ ( 𝑛 ∈ ℕ → ( Λ ‘ 𝑛 ) ∈ ℝ )
7	5 6	syl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( Λ ‘ 𝑛 ) ∈ ℝ )
8	7	recnd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( Λ ‘ 𝑛 ) ∈ ℂ )
9		simprr	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ ( Λ ‘ 𝑛 ) = 0 ) ) → ( Λ ‘ 𝑛 ) = 0 )
10	2 3 8 9	fsumvma2	⊢ ( 𝐴 ∈ ℝ → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( Λ ‘ 𝑛 ) = Σ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) )
11		simpr	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) )
12	11	elin2d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 𝑝 ∈ ℙ )
13		elfznn	⊢ ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) → 𝑘 ∈ ℕ )
14		vmappw	⊢ ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) → ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) = ( log ‘ 𝑝 ) )
15	12 13 14	syl2an	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) → ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) = ( log ‘ 𝑝 ) )
16	15	sumeq2dv	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) = Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ( log ‘ 𝑝 ) )
17		fzfid	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ∈ Fin )
18		prmuz2	⊢ ( 𝑝 ∈ ℙ → 𝑝 ∈ ( ℤ≥ ‘ 2 ) )
19		eluzelre	⊢ ( 𝑝 ∈ ( ℤ≥ ‘ 2 ) → 𝑝 ∈ ℝ )
20		eluz2gt1	⊢ ( 𝑝 ∈ ( ℤ≥ ‘ 2 ) → 1 < 𝑝 )
21	19 20	rplogcld	⊢ ( 𝑝 ∈ ( ℤ≥ ‘ 2 ) → ( log ‘ 𝑝 ) ∈ ℝ+ )
22	12 18 21	3syl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( log ‘ 𝑝 ) ∈ ℝ+ )
23	22	rpcnd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( log ‘ 𝑝 ) ∈ ℂ )
24		fsumconst	⊢ ( ( ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ∈ Fin ∧ ( log ‘ 𝑝 ) ∈ ℂ ) → Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ( log ‘ 𝑝 ) = ( ( ♯ ‘ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) · ( log ‘ 𝑝 ) ) )
25	17 23 24	syl2anc	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ( log ‘ 𝑝 ) = ( ( ♯ ‘ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) · ( log ‘ 𝑝 ) ) )
26		ppisval	⊢ ( 𝐴 ∈ ℝ → ( ( 0 [,] 𝐴 ) ∩ ℙ ) = ( ( 2 ... ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) )
27		inss1	⊢ ( ( 2 ... ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) ⊆ ( 2 ... ( ⌊ ‘ 𝐴 ) )
28	26 27	eqsstrdi	⊢ ( 𝐴 ∈ ℝ → ( ( 0 [,] 𝐴 ) ∩ ℙ ) ⊆ ( 2 ... ( ⌊ ‘ 𝐴 ) ) )
29	28	sselda	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 𝑝 ∈ ( 2 ... ( ⌊ ‘ 𝐴 ) ) )
30		elfzuz2	⊢ ( 𝑝 ∈ ( 2 ... ( ⌊ ‘ 𝐴 ) ) → ( ⌊ ‘ 𝐴 ) ∈ ( ℤ≥ ‘ 2 ) )
31	29 30	syl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ⌊ ‘ 𝐴 ) ∈ ( ℤ≥ ‘ 2 ) )
32		simpl	⊢ ( ( 𝐴 ∈ ℝ ∧ ( ⌊ ‘ 𝐴 ) ∈ ( ℤ≥ ‘ 2 ) ) → 𝐴 ∈ ℝ )
33		0red	⊢ ( ( 𝐴 ∈ ℝ ∧ ( ⌊ ‘ 𝐴 ) ∈ ( ℤ≥ ‘ 2 ) ) → 0 ∈ ℝ )
34		2re	⊢ 2 ∈ ℝ
35	34	a1i	⊢ ( ( 𝐴 ∈ ℝ ∧ ( ⌊ ‘ 𝐴 ) ∈ ( ℤ≥ ‘ 2 ) ) → 2 ∈ ℝ )
36		2pos	⊢ 0 < 2
37	36	a1i	⊢ ( ( 𝐴 ∈ ℝ ∧ ( ⌊ ‘ 𝐴 ) ∈ ( ℤ≥ ‘ 2 ) ) → 0 < 2 )
38		eluzle	⊢ ( ( ⌊ ‘ 𝐴 ) ∈ ( ℤ≥ ‘ 2 ) → 2 ≤ ( ⌊ ‘ 𝐴 ) )
39		2z	⊢ 2 ∈ ℤ
40		flge	⊢ ( ( 𝐴 ∈ ℝ ∧ 2 ∈ ℤ ) → ( 2 ≤ 𝐴 ↔ 2 ≤ ( ⌊ ‘ 𝐴 ) ) )
41	39 40	mpan2	⊢ ( 𝐴 ∈ ℝ → ( 2 ≤ 𝐴 ↔ 2 ≤ ( ⌊ ‘ 𝐴 ) ) )
42	38 41	imbitrrid	⊢ ( 𝐴 ∈ ℝ → ( ( ⌊ ‘ 𝐴 ) ∈ ( ℤ≥ ‘ 2 ) → 2 ≤ 𝐴 ) )
43	42	imp	⊢ ( ( 𝐴 ∈ ℝ ∧ ( ⌊ ‘ 𝐴 ) ∈ ( ℤ≥ ‘ 2 ) ) → 2 ≤ 𝐴 )
44	33 35 32 37 43	ltletrd	⊢ ( ( 𝐴 ∈ ℝ ∧ ( ⌊ ‘ 𝐴 ) ∈ ( ℤ≥ ‘ 2 ) ) → 0 < 𝐴 )
45	32 44	elrpd	⊢ ( ( 𝐴 ∈ ℝ ∧ ( ⌊ ‘ 𝐴 ) ∈ ( ℤ≥ ‘ 2 ) ) → 𝐴 ∈ ℝ+ )
46	31 45	syldan	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 𝐴 ∈ ℝ+ )
47	46	relogcld	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( log ‘ 𝐴 ) ∈ ℝ )
48	47 22	rerpdivcld	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ∈ ℝ )
49		1red	⊢ ( ( 𝐴 ∈ ℝ ∧ ( ⌊ ‘ 𝐴 ) ∈ ( ℤ≥ ‘ 2 ) ) → 1 ∈ ℝ )
50		1lt2	⊢ 1 < 2
51	50	a1i	⊢ ( ( 𝐴 ∈ ℝ ∧ ( ⌊ ‘ 𝐴 ) ∈ ( ℤ≥ ‘ 2 ) ) → 1 < 2 )
52	49 35 32 51 43	ltletrd	⊢ ( ( 𝐴 ∈ ℝ ∧ ( ⌊ ‘ 𝐴 ) ∈ ( ℤ≥ ‘ 2 ) ) → 1 < 𝐴 )
53	31 52	syldan	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 1 < 𝐴 )
54		rplogcl	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) → ( log ‘ 𝐴 ) ∈ ℝ+ )
55	53 54	syldan	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( log ‘ 𝐴 ) ∈ ℝ+ )
56	55 22	rpdivcld	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ∈ ℝ+ )
57	56	rpge0d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 0 ≤ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) )
58		flge0nn0	⊢ ( ( ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ∈ ℝ ∧ 0 ≤ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) → ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ∈ ℕ0 )
59	48 57 58	syl2anc	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ∈ ℕ0 )
60		hashfz1	⊢ ( ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ∈ ℕ0 → ( ♯ ‘ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) = ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) )
61	59 60	syl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ♯ ‘ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) = ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) )
62	61	oveq1d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( ♯ ‘ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) · ( log ‘ 𝑝 ) ) = ( ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) · ( log ‘ 𝑝 ) ) )
63	59	nn0cnd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ∈ ℂ )
64	63 23	mulcomd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) · ( log ‘ 𝑝 ) ) = ( ( log ‘ 𝑝 ) · ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) )
65	25 62 64	3eqtrd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ( log ‘ 𝑝 ) = ( ( log ‘ 𝑝 ) · ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) )
66	16 65	eqtrd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) = ( ( log ‘ 𝑝 ) · ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) )
67	66	sumeq2dv	⊢ ( 𝐴 ∈ ℝ → Σ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ( Λ ‘ ( 𝑝 ↑ 𝑘 ) ) = Σ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ( ( log ‘ 𝑝 ) · ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) )
68	1 10 67	3eqtrd	⊢ ( 𝐴 ∈ ℝ → ( ψ ‘ 𝐴 ) = Σ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ( ( log ‘ 𝑝 ) · ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) )