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		simpr	$$⊢\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\}\approx 1_{𝑜}$$
17		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\}$$
18	16 17	sylib	$$⊢\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\}$$
19		ssrab2	$$⊢\left\{p\in \mathbb{P}|p\parallel A\right\}\subseteq \mathbb{P}$$
20	18 19	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}$$
21	7	uniexd	$$⊢A\in \mathbb{N}\to \bigcup \left\{p\in \mathbb{P}|p\parallel A\right\}\in \mathrm{V}$$
22	21	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}$$
23		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)$$
24	22 23	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)$$
25	20 24	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}$$
26		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}$$
27	25 26	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}$$
28		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 ℝ$$
29	27 28	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 ℝ$$
30		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\}$$
31	27 30	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\}$$
32	29 31	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 {ℝ}^{+}$$
33	32	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$$
34	15 33	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$$
35	34	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)$$
36		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$$
37	36	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$$
38	37 13	syl5ib	$$⊢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)$$
39	35 38	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)$$
40	4 39	syl5bb	$$⊢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)$$
41	3 40	bitr4d	$$⊢A\in \mathbb{N}\to \left(\Lambda \left(A\right)\ne 0\leftrightarrow \exists !p\in \mathbb{P}p\parallel A\right)$$