efchpcl

Description: The second Chebyshev function is closed in the log-integers. (Contributed by Mario Carneiro, 7-Apr-2016)

		Ref	Expression
	Assertion	efchpcl	$⊢ A \in ℝ \to e^{ψ (A)} \in ℕ$

Step	Hyp	Ref	Expression
1		chpval	$⊢ A \in ℝ \to ψ (A) = \sum_{n = 1}^{⌊A⌋} Λ (n)$
2	1	fveq2d	$⊢ A \in ℝ \to e^{ψ (A)} = e^{\sum_{n = 1}^{⌊A⌋} Λ (n)}$
3		fzfid	$⊢ A \in ℝ \to (1 \dots ⌊A⌋) \in Fin$
4		elfznn	$⊢ n \in (1 \dots ⌊A⌋) \to n \in ℕ$
5	4	adantl	$⊢ (A \in ℝ \land n \in (1 \dots ⌊A⌋)) \to n \in ℕ$
6		vmacl	$⊢ n \in ℕ \to Λ (n) \in ℝ$
7	5 6	syl	$⊢ (A \in ℝ \land n \in (1 \dots ⌊A⌋)) \to Λ (n) \in ℝ$
8		efvmacl	$⊢ n \in ℕ \to e^{Λ (n)} \in ℕ$
9	5 8	syl	$⊢ (A \in ℝ \land n \in (1 \dots ⌊A⌋)) \to e^{Λ (n)} \in ℕ$
10	3 7 9	efnnfsumcl	$⊢ A \in ℝ \to e^{\sum_{n = 1}^{⌊A⌋} Λ (n)} \in ℕ$
11	2 10	eqeltrd	$⊢ A \in ℝ \to e^{ψ (A)} \in ℕ$

Metamath Proof Explorer