Theorem isppw

Description: Two ways to say that A is a prime power. (Contributed by Mario Carneiro, 7-Apr-2016)

	Ref	Expression
Assertion	isppw	$$⊢A\in \mathbb{N}\to \left(\Lambda \left(A\right)\ne 0\leftrightarrow \exists !p\in \mathbb{P}p\parallel A\right)$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢\left\{p\in \mathbb{P}|p\parallel A\right\}=\left\{p\in \mathbb{P}|p\parallel A\right\}$$
2	1	vmaval	$$⊢A\in \mathbb{N}\to \Lambda \left(A\right)=if\left(\left|\left\{p\in \mathbb{P}|p\parallel A\right\}\right|=1,\log \bigcup \left\{p\in \mathbb{P}|p\parallel A\right\},0\right)$$
3	2	neeq1d	$$⊢A\in \mathbb{N}\to \left(\Lambda \left(A\right)\ne 0\leftrightarrow if\left(\left|\left\{p\in \mathbb{P}|p\parallel A\right\}\right|=1,\log \bigcup \left\{p\in \mathbb{P}|p\parallel A\right\},0\right)\ne 0\right)$$
4		reuen1	$$⊢\exists !p\in \mathbb{P}p\parallel A\leftrightarrow \left\{p\in \mathbb{P}|p\parallel A\right\}\approx 1_{𝑜}$$
5		hash1	$$⊢\left|1_{𝑜}\right|=1$$
6	5	eqeq2i	$$⊢\left|\left\{p\in \mathbb{P}|p\parallel A\right\}\right|=\left|1_{𝑜}\right|\leftrightarrow \left|\left\{p\in \mathbb{P}|p\parallel A\right\}\right|=1$$
7		prmdvdsfi	$$⊢A\in \mathbb{N}\to \left\{p\in \mathbb{P}|p\parallel A\right\}\in \mathrm{Fin}$$
8		1onn	$$⊢1_{𝑜}\in \mathrm{\omega }$$
9		nnfi	$$⊢1_{𝑜}\in \mathrm{\omega }\to 1_{𝑜}\in \mathrm{Fin}$$
10	8 9	ax-mp	$$⊢1_{𝑜}\in \mathrm{Fin}$$
11		hashen	$$⊢\left(\left\{p\in \mathbb{P}|p\parallel A\right\}\in \mathrm{Fin}\wedge 1_{𝑜}\in \mathrm{Fin}\right)\to \left(\left|\left\{p\in \mathbb{P}|p\parallel A\right\}\right|=\left|1_{𝑜}\right|\leftrightarrow \left\{p\in \mathbb{P}|p\parallel A\right\}\approx 1_{𝑜}\right)$$
12	7 10 11	sylancl	$$⊢A\in \mathbb{N}\to \left(\left|\left\{p\in \mathbb{P}|p\parallel A\right\}\right|=\left|1_{𝑜}\right|\leftrightarrow \left\{p\in \mathbb{P}|p\parallel A\right\}\approx 1_{𝑜}\right)$$
13	6 12	bitr3id	$$⊢A\in \mathbb{N}\to \left(\left|\left\{p\in \mathbb{P}|p\parallel A\right\}\right|=1\leftrightarrow \left\{p\in \mathbb{P}|p\parallel A\right\}\approx 1_{𝑜}\right)$$
14	13	biimpar	$$⊢\left(A\in \mathbb{N}\wedge \left\{p\in \mathbb{P}|p\parallel A\right\}\approx 1_{𝑜}\right)\to \left|\left\{p\in \mathbb{P}|p\parallel A\right\}\right|=1$$
15	14	iftrued	$$⊢\left(A\in \mathbb{N}\wedge \left\{p\in \mathbb{P}|p\parallel A\right\}\approx 1_{𝑜}\right)\to if\left(\left|\left\{p\in \mathbb{P}|p\parallel A\right\}\right|=1,\log \bigcup \left\{p\in \mathbb{P}|p\parallel A\right\},0\right)=\log \bigcup \left\{p\in \mathbb{P}|p\parallel A\right\}$$
16		en1b	$$⊢\left\{p\in \mathbb{P}|p\parallel A\right\}\approx 1_{𝑜}\leftrightarrow \left\{p\in \mathbb{P}|p\parallel A\right\}=\left\{\bigcup \left\{p\in \mathbb{P}|p\parallel A\right\}\right\}$$
17	16	bilani	$$⊢\left(A\in \mathbb{N}\wedge \left\{p\in \mathbb{P}|p\parallel A\right\}\approx 1_{𝑜}\right)\to \left\{p\in \mathbb{P}|p\parallel A\right\}=\left\{\bigcup \left\{p\in \mathbb{P}|p\parallel A\right\}\right\}$$
18		ssrab2	$$⊢\left\{p\in \mathbb{P}|p\parallel A\right\}\subseteq \mathbb{P}$$
19	17 18	eqsstrrdi	$$⊢\left(A\in \mathbb{N}\wedge \left\{p\in \mathbb{P}|p\parallel A\right\}\approx 1_{𝑜}\right)\to \left\{\bigcup \left\{p\in \mathbb{P}|p\parallel A\right\}\right\}\subseteq \mathbb{P}$$
20	7	uniexd	$$⊢A\in \mathbb{N}\to \bigcup \left\{p\in \mathbb{P}|p\parallel A\right\}\in \mathrm{V}$$
21	20	adantr	$$⊢\left(A\in \mathbb{N}\wedge \left\{p\in \mathbb{P}|p\parallel A\right\}\approx 1_{𝑜}\right)\to \bigcup \left\{p\in \mathbb{P}|p\parallel A\right\}\in \mathrm{V}$$
22		snssg	$$⊢\bigcup \left\{p\in \mathbb{P}|p\parallel A\right\}\in \mathrm{V}\to \left(\bigcup \left\{p\in \mathbb{P}|p\parallel A\right\}\in \mathbb{P}\leftrightarrow \left\{\bigcup \left\{p\in \mathbb{P}|p\parallel A\right\}\right\}\subseteq \mathbb{P}\right)$$
23	21 22	syl	$$⊢\left(A\in \mathbb{N}\wedge \left\{p\in \mathbb{P}|p\parallel A\right\}\approx 1_{𝑜}\right)\to \left(\bigcup \left\{p\in \mathbb{P}|p\parallel A\right\}\in \mathbb{P}\leftrightarrow \left\{\bigcup \left\{p\in \mathbb{P}|p\parallel A\right\}\right\}\subseteq \mathbb{P}\right)$$
24	19 23	mpbird	$$⊢\left(A\in \mathbb{N}\wedge \left\{p\in \mathbb{P}|p\parallel A\right\}\approx 1_{𝑜}\right)\to \bigcup \left\{p\in \mathbb{P}|p\parallel A\right\}\in \mathbb{P}$$
25		prmuz2	$$⊢\bigcup \left\{p\in \mathbb{P}|p\parallel A\right\}\in \mathbb{P}\to \bigcup \left\{p\in \mathbb{P}|p\parallel A\right\}\in {\mathbb{Z}}_{\ge 2}$$
26	24 25	syl	$$⊢\left(A\in \mathbb{N}\wedge \left\{p\in \mathbb{P}|p\parallel A\right\}\approx 1_{𝑜}\right)\to \bigcup \left\{p\in \mathbb{P}|p\parallel A\right\}\in {\mathbb{Z}}_{\ge 2}$$
27		eluzelre	$$⊢\bigcup \left\{p\in \mathbb{P}|p\parallel A\right\}\in {\mathbb{Z}}_{\ge 2}\to \bigcup \left\{p\in \mathbb{P}|p\parallel A\right\}\in ℝ$$
28	26 27	syl	$$⊢\left(A\in \mathbb{N}\wedge \left\{p\in \mathbb{P}|p\parallel A\right\}\approx 1_{𝑜}\right)\to \bigcup \left\{p\in \mathbb{P}|p\parallel A\right\}\in ℝ$$
29		eluz2gt1	$$⊢\bigcup \left\{p\in \mathbb{P}|p\parallel A\right\}\in {\mathbb{Z}}_{\ge 2}\to 1<\bigcup \left\{p\in \mathbb{P}|p\parallel A\right\}$$
30	26 29	syl	$$⊢\left(A\in \mathbb{N}\wedge \left\{p\in \mathbb{P}|p\parallel A\right\}\approx 1_{𝑜}\right)\to 1<\bigcup \left\{p\in \mathbb{P}|p\parallel A\right\}$$
31	28 30	rplogcld	$$⊢\left(A\in \mathbb{N}\wedge \left\{p\in \mathbb{P}|p\parallel A\right\}\approx 1_{𝑜}\right)\to \log \bigcup \left\{p\in \mathbb{P}|p\parallel A\right\}\in {ℝ}^{+}$$
32	31	rpne0d	$$⊢\left(A\in \mathbb{N}\wedge \left\{p\in \mathbb{P}|p\parallel A\right\}\approx 1_{𝑜}\right)\to \log \bigcup \left\{p\in \mathbb{P}|p\parallel A\right\}\ne 0$$
33	15 32	eqnetrd	$$⊢\left(A\in \mathbb{N}\wedge \left\{p\in \mathbb{P}|p\parallel A\right\}\approx 1_{𝑜}\right)\to if\left(\left|\left\{p\in \mathbb{P}|p\parallel A\right\}\right|=1,\log \bigcup \left\{p\in \mathbb{P}|p\parallel A\right\},0\right)\ne 0$$
34	33	ex	$$⊢A\in \mathbb{N}\to \left(\left\{p\in \mathbb{P}|p\parallel A\right\}\approx 1_{𝑜}\to if\left(\left|\left\{p\in \mathbb{P}|p\parallel A\right\}\right|=1,\log \bigcup \left\{p\in \mathbb{P}|p\parallel A\right\},0\right)\ne 0\right)$$
35		iffalse	$$⊢\neg \left|\left\{p\in \mathbb{P}|p\parallel A\right\}\right|=1\to if\left(\left|\left\{p\in \mathbb{P}|p\parallel A\right\}\right|=1,\log \bigcup \left\{p\in \mathbb{P}|p\parallel A\right\},0\right)=0$$
36	35	necon1ai	$$⊢if\left(\left|\left\{p\in \mathbb{P}|p\parallel A\right\}\right|=1,\log \bigcup \left\{p\in \mathbb{P}|p\parallel A\right\},0\right)\ne 0\to \left|\left\{p\in \mathbb{P}|p\parallel A\right\}\right|=1$$
37	36 13	imbitrid	$$⊢A\in \mathbb{N}\to \left(if\left(\left|\left\{p\in \mathbb{P}|p\parallel A\right\}\right|=1,\log \bigcup \left\{p\in \mathbb{P}|p\parallel A\right\},0\right)\ne 0\to \left\{p\in \mathbb{P}|p\parallel A\right\}\approx 1_{𝑜}\right)$$
38	34 37	impbid	$$⊢A\in \mathbb{N}\to \left(\left\{p\in \mathbb{P}|p\parallel A\right\}\approx 1_{𝑜}\leftrightarrow if\left(\left|\left\{p\in \mathbb{P}|p\parallel A\right\}\right|=1,\log \bigcup \left\{p\in \mathbb{P}|p\parallel A\right\},0\right)\ne 0\right)$$
39	4 38	bitrid	$$⊢A\in \mathbb{N}\to \left(\exists !p\in \mathbb{P}p\parallel A\leftrightarrow if\left(\left|\left\{p\in \mathbb{P}|p\parallel A\right\}\right|=1,\log \bigcup \left\{p\in \mathbb{P}|p\parallel A\right\},0\right)\ne 0\right)$$
40	3 39	bitr4d	$$⊢A\in \mathbb{N}\to \left(\Lambda \left(A\right)\ne 0\leftrightarrow \exists !p\in \mathbb{P}p\parallel A\right)$$