Theorem 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 {\mathrm{e}}^{\psi \left(A\right)}\in \mathbb{N}$$

Proof

Step	Hyp	Ref	Expression
1		chpval	$$⊢A\in ℝ\to \psi \left(A\right)=\sum _{n=1}^{⌊A⌋}\Lambda \left(n\right)$$
2	1	fveq2d	$$⊢A\in ℝ\to {\mathrm{e}}^{\psi \left(A\right)}={\mathrm{e}}^{\sum _{n=1}^{⌊A⌋}\Lambda \left(n\right)}$$
3		fzfid	$$⊢A\in ℝ\to \left(1\dots ⌊A⌋\right)\in \mathrm{Fin}$$
4		elfznn	$$⊢n\in \left(1\dots ⌊A⌋\right)\to n\in \mathbb{N}$$
5	4	adantl	$$⊢\left(A\in ℝ\wedge n\in \left(1\dots ⌊A⌋\right)\right)\to n\in \mathbb{N}$$
6		vmacl	$$⊢n\in \mathbb{N}\to \Lambda \left(n\right)\in ℝ$$
7	5 6	syl	$$⊢\left(A\in ℝ\wedge n\in \left(1\dots ⌊A⌋\right)\right)\to \Lambda \left(n\right)\in ℝ$$
8		efvmacl	$$⊢n\in \mathbb{N}\to {\mathrm{e}}^{\Lambda \left(n\right)}\in \mathbb{N}$$
9	5 8	syl	$$⊢\left(A\in ℝ\wedge n\in \left(1\dots ⌊A⌋\right)\right)\to {\mathrm{e}}^{\Lambda \left(n\right)}\in \mathbb{N}$$
10	3 7 9	efnnfsumcl	$$⊢A\in ℝ\to {\mathrm{e}}^{\sum _{n=1}^{⌊A⌋}\Lambda \left(n\right)}\in \mathbb{N}$$
11	2 10	eqeltrd	$$⊢A\in ℝ\to {\mathrm{e}}^{\psi \left(A\right)}\in \mathbb{N}$$