Theorem efchtcl

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

	Ref	Expression
Assertion	efchtcl	$$⊢A\in ℝ\to {\mathrm{e}}^{\theta \left(A\right)}\in \mathbb{N}$$

Proof

Step	Hyp	Ref	Expression
1		chtval	$$⊢A\in ℝ\to \theta \left(A\right)=\sum _{p\in \left[0,A\right]\cap \mathbb{P}}\log p$$
2	1	fveq2d	$$⊢A\in ℝ\to {\mathrm{e}}^{\theta \left(A\right)}={\mathrm{e}}^{\sum _{p\in \left[0,A\right]\cap \mathbb{P}}\log p}$$
3		ppifi	$$⊢A\in ℝ\to \left[0,A\right]\cap \mathbb{P}\in \mathrm{Fin}$$
4		simpr	$$⊢\left(A\in ℝ\wedge p\in \left(\left[0,A\right]\cap \mathbb{P}\right)\right)\to p\in \left(\left[0,A\right]\cap \mathbb{P}\right)$$
5	4	elin2d	$$⊢\left(A\in ℝ\wedge p\in \left(\left[0,A\right]\cap \mathbb{P}\right)\right)\to p\in \mathbb{P}$$
6		prmnn	$$⊢p\in \mathbb{P}\to p\in \mathbb{N}$$
7	5 6	syl	$$⊢\left(A\in ℝ\wedge p\in \left(\left[0,A\right]\cap \mathbb{P}\right)\right)\to p\in \mathbb{N}$$
8	7	nnrpd	$$⊢\left(A\in ℝ\wedge p\in \left(\left[0,A\right]\cap \mathbb{P}\right)\right)\to p\in {ℝ}^{+}$$
9	8	relogcld	$$⊢\left(A\in ℝ\wedge p\in \left(\left[0,A\right]\cap \mathbb{P}\right)\right)\to \log p\in ℝ$$
10	8	reeflogd	$$⊢\left(A\in ℝ\wedge p\in \left(\left[0,A\right]\cap \mathbb{P}\right)\right)\to {\mathrm{e}}^{\log p}=p$$
11	10 7	eqeltrd	$$⊢\left(A\in ℝ\wedge p\in \left(\left[0,A\right]\cap \mathbb{P}\right)\right)\to {\mathrm{e}}^{\log p}\in \mathbb{N}$$
12	3 9 11	efnnfsumcl	$$⊢A\in ℝ\to {\mathrm{e}}^{\sum _{p\in \left[0,A\right]\cap \mathbb{P}}\log p}\in \mathbb{N}$$
13	2 12	eqeltrd	$$⊢A\in ℝ\to {\mathrm{e}}^{\theta \left(A\right)}\in \mathbb{N}$$