Theorem pcmptcl

Description: Closure for the prime power map. (Contributed by Mario Carneiro, 12-Mar-2014)

	Ref	Expression
Hypotheses	pcmpt.1	$$⊢F=\left(n\in \mathbb{N}⟼if\left(n\in \mathbb{P},n^A,1\right)\right)$$
	pcmpt.2	$$⊢\phi \to \forall n\in \mathbb{P}A\in {\mathbb{N}}_0$$
Assertion	pcmptcl	$$⊢\phi \to \left(F:\mathbb{N}⟶\mathbb{N}\wedge seq1\left(\times ,F\right):\mathbb{N}⟶\mathbb{N}\right)$$

Proof

Step	Hyp	Ref	Expression
1		pcmpt.1	$$⊢F=\left(n\in \mathbb{N}⟼if\left(n\in \mathbb{P},n^A,1\right)\right)$$
2		pcmpt.2	$$⊢\phi \to \forall n\in \mathbb{P}A\in {\mathbb{N}}_0$$
3		pm2.27	$$⊢n\in \mathbb{P}\to \left(\left(n\in \mathbb{P}\to A\in {\mathbb{N}}_0\right)\to A\in {\mathbb{N}}_0\right)$$
4		iftrue	$$⊢n\in \mathbb{P}\to if\left(n\in \mathbb{P},n^A,1\right)=n^A$$
5	4	adantr	$$⊢\left(n\in \mathbb{P}\wedge A\in {\mathbb{N}}_0\right)\to if\left(n\in \mathbb{P},n^A,1\right)=n^A$$
6		prmnn	$$⊢n\in \mathbb{P}\to n\in \mathbb{N}$$
7		nnexpcl	$$⊢\left(n\in \mathbb{N}\wedge A\in {\mathbb{N}}_0\right)\to n^A\in \mathbb{N}$$
8	6 7	sylan	$$⊢\left(n\in \mathbb{P}\wedge A\in {\mathbb{N}}_0\right)\to n^A\in \mathbb{N}$$
9	5 8	eqeltrd	$$⊢\left(n\in \mathbb{P}\wedge A\in {\mathbb{N}}_0\right)\to if\left(n\in \mathbb{P},n^A,1\right)\in \mathbb{N}$$
10	9	ex	$$⊢n\in \mathbb{P}\to \left(A\in {\mathbb{N}}_0\to if\left(n\in \mathbb{P},n^A,1\right)\in \mathbb{N}\right)$$
11	3 10	syld	$$⊢n\in \mathbb{P}\to \left(\left(n\in \mathbb{P}\to A\in {\mathbb{N}}_0\right)\to if\left(n\in \mathbb{P},n^A,1\right)\in \mathbb{N}\right)$$
12		iffalse	$$⊢\neg n\in \mathbb{P}\to if\left(n\in \mathbb{P},n^A,1\right)=1$$
13		1nn	$$⊢1\in \mathbb{N}$$
14	12 13	eqeltrdi	$$⊢\neg n\in \mathbb{P}\to if\left(n\in \mathbb{P},n^A,1\right)\in \mathbb{N}$$
15	14	a1d	$$⊢\neg n\in \mathbb{P}\to \left(\left(n\in \mathbb{P}\to A\in {\mathbb{N}}_0\right)\to if\left(n\in \mathbb{P},n^A,1\right)\in \mathbb{N}\right)$$
16	11 15	pm2.61i	$$⊢\left(n\in \mathbb{P}\to A\in {\mathbb{N}}_0\right)\to if\left(n\in \mathbb{P},n^A,1\right)\in \mathbb{N}$$
17	16	a1d	$$⊢\left(n\in \mathbb{P}\to A\in {\mathbb{N}}_0\right)\to \left(n\in \mathbb{N}\to if\left(n\in \mathbb{P},n^A,1\right)\in \mathbb{N}\right)$$
18	17	ralimi2	$$⊢\forall n\in \mathbb{P}A\in {\mathbb{N}}_0\to \forall n\in \mathbb{N}if\left(n\in \mathbb{P},n^A,1\right)\in \mathbb{N}$$
19	2 18	syl	$$⊢\phi \to \forall n\in \mathbb{N}if\left(n\in \mathbb{P},n^A,1\right)\in \mathbb{N}$$
20	1	fmpt	$$⊢\forall n\in \mathbb{N}if\left(n\in \mathbb{P},n^A,1\right)\in \mathbb{N}\leftrightarrow F:\mathbb{N}⟶\mathbb{N}$$
21	19 20	sylib	$$⊢\phi \to F:\mathbb{N}⟶\mathbb{N}$$
22		nnuz	$$⊢\mathbb{N}={\mathbb{Z}}_{\ge 1}$$
23		1zzd	$$⊢\phi \to 1\in \mathbb{Z}$$
24	21	ffvelcdmda	$$⊢\left(\phi \wedge k\in \mathbb{N}\right)\to F\left(k\right)\in \mathbb{N}$$
25		nnmulcl	$$⊢\left(k\in \mathbb{N}\wedge p\in \mathbb{N}\right)\to kp\in \mathbb{N}$$
26	25	adantl	$$⊢\left(\phi \wedge \left(k\in \mathbb{N}\wedge p\in \mathbb{N}\right)\right)\to kp\in \mathbb{N}$$
27	22 23 24 26	seqf	$$⊢\phi \to seq1\left(\times ,F\right):\mathbb{N}⟶\mathbb{N}$$
28	21 27	jca	$$⊢\phi \to \left(F:\mathbb{N}⟶\mathbb{N}\wedge seq1\left(\times ,F\right):\mathbb{N}⟶\mathbb{N}\right)$$