chpf

Description: Functionality of the second Chebyshev function. (Contributed by Mario Carneiro, 7-Apr-2016)

		Ref	Expression
	Assertion	chpf	$⊢ ψ : ℝ ⟶ ℝ$

Step	Hyp	Ref	Expression
1		df-chp	$⊢ ψ = (x \in ℝ ⟼ \sum_{n = 1}^{⌊x⌋} Λ (n))$
2		fzfid	$⊢ x \in ℝ \to (1 \dots ⌊x⌋) \in Fin$
3		elfznn	$⊢ n \in (1 \dots ⌊x⌋) \to n \in ℕ$
4	3	adantl	$⊢ (x \in ℝ \land n \in (1 \dots ⌊x⌋)) \to n \in ℕ$
5		vmacl	$⊢ n \in ℕ \to Λ (n) \in ℝ$
6	4 5	syl	$⊢ (x \in ℝ \land n \in (1 \dots ⌊x⌋)) \to Λ (n) \in ℝ$
7	2 6	fsumrecl	$⊢ x \in ℝ \to \sum_{n = 1}^{⌊x⌋} Λ (n) \in ℝ$
8	1 7	fmpti	$⊢ ψ : ℝ ⟶ ℝ$

Metamath Proof Explorer