Theorem vmacl

Description: Closure for the von Mangoldt function. (Contributed by Mario Carneiro, 7-Apr-2016)

	Ref	Expression
Assertion	vmacl	$$⊢A\in \mathbb{N}\to \Lambda \left(A\right)\in ℝ$$

Proof

Step	Hyp	Ref	Expression
1		eleq1	$$⊢\Lambda \left(A\right)=0\to \left(\Lambda \left(A\right)\in ℝ\leftrightarrow 0\in ℝ\right)$$
2		isppw2	$$⊢A\in \mathbb{N}\to \left(\Lambda \left(A\right)\ne 0\leftrightarrow \exists p\in \mathbb{P}\exists k\in \mathbb{N}A=p^k\right)$$
3		vmappw	$$⊢\left(p\in \mathbb{P}\wedge k\in \mathbb{N}\right)\to \Lambda \left(p^k\right)=\log p$$
4		prmnn	$$⊢p\in \mathbb{P}\to p\in \mathbb{N}$$
5	4	nnrpd	$$⊢p\in \mathbb{P}\to p\in {ℝ}^{+}$$
6	5	relogcld	$$⊢p\in \mathbb{P}\to \log p\in ℝ$$
7	6	adantr	$$⊢\left(p\in \mathbb{P}\wedge k\in \mathbb{N}\right)\to \log p\in ℝ$$
8	3 7	eqeltrd	$$⊢\left(p\in \mathbb{P}\wedge k\in \mathbb{N}\right)\to \Lambda \left(p^k\right)\in ℝ$$
9		fveq2	$$⊢A=p^k\to \Lambda \left(A\right)=\Lambda \left(p^k\right)$$
10	9	eleq1d	$$⊢A=p^k\to \left(\Lambda \left(A\right)\in ℝ\leftrightarrow \Lambda \left(p^k\right)\in ℝ\right)$$
11	8 10	syl5ibrcom	$$⊢\left(p\in \mathbb{P}\wedge k\in \mathbb{N}\right)\to \left(A=p^k\to \Lambda \left(A\right)\in ℝ\right)$$
12	11	rexlimivv	$$⊢\exists p\in \mathbb{P}\exists k\in \mathbb{N}A=p^k\to \Lambda \left(A\right)\in ℝ$$
13	2 12	biimtrdi	$$⊢A\in \mathbb{N}\to \left(\Lambda \left(A\right)\ne 0\to \Lambda \left(A\right)\in ℝ\right)$$
14	13	imp	$$⊢\left(A\in \mathbb{N}\wedge \Lambda \left(A\right)\ne 0\right)\to \Lambda \left(A\right)\in ℝ$$
15		0red	$$⊢A\in \mathbb{N}\to 0\in ℝ$$
16	1 14 15	pm2.61ne	$$⊢A\in \mathbb{N}\to \Lambda \left(A\right)\in ℝ$$