Theorem pcmptcl

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

	Ref	Expression
Hypotheses	pcmpt.1	⊢ 𝐹 = ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( 𝑛 ↑ 𝐴 ) , 1 ) )
	pcmpt.2	⊢ ( 𝜑 → ∀ 𝑛 ∈ ℙ 𝐴 ∈ ℕ0 )
Assertion	pcmptcl	⊢ ( 𝜑 → ( 𝐹 : ℕ ⟶ ℕ ∧ seq 1 ( · , 𝐹 ) : ℕ ⟶ ℕ ) )

Proof

Step	Hyp	Ref	Expression
1		pcmpt.1	⊢ 𝐹 = ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( 𝑛 ↑ 𝐴 ) , 1 ) )
2		pcmpt.2	⊢ ( 𝜑 → ∀ 𝑛 ∈ ℙ 𝐴 ∈ ℕ0 )
3		pm2.27	⊢ ( 𝑛 ∈ ℙ → ( ( 𝑛 ∈ ℙ → 𝐴 ∈ ℕ0 ) → 𝐴 ∈ ℕ0 ) )
4		iftrue	⊢ ( 𝑛 ∈ ℙ → if ( 𝑛 ∈ ℙ , ( 𝑛 ↑ 𝐴 ) , 1 ) = ( 𝑛 ↑ 𝐴 ) )
5	4	adantr	⊢ ( ( 𝑛 ∈ ℙ ∧ 𝐴 ∈ ℕ0 ) → if ( 𝑛 ∈ ℙ , ( 𝑛 ↑ 𝐴 ) , 1 ) = ( 𝑛 ↑ 𝐴 ) )
6		prmnn	⊢ ( 𝑛 ∈ ℙ → 𝑛 ∈ ℕ )
7		nnexpcl	⊢ ( ( 𝑛 ∈ ℕ ∧ 𝐴 ∈ ℕ0 ) → ( 𝑛 ↑ 𝐴 ) ∈ ℕ )
8	6 7	sylan	⊢ ( ( 𝑛 ∈ ℙ ∧ 𝐴 ∈ ℕ0 ) → ( 𝑛 ↑ 𝐴 ) ∈ ℕ )
9	5 8	eqeltrd	⊢ ( ( 𝑛 ∈ ℙ ∧ 𝐴 ∈ ℕ0 ) → if ( 𝑛 ∈ ℙ , ( 𝑛 ↑ 𝐴 ) , 1 ) ∈ ℕ )
10	9	ex	⊢ ( 𝑛 ∈ ℙ → ( 𝐴 ∈ ℕ0 → if ( 𝑛 ∈ ℙ , ( 𝑛 ↑ 𝐴 ) , 1 ) ∈ ℕ ) )
11	3 10	syld	⊢ ( 𝑛 ∈ ℙ → ( ( 𝑛 ∈ ℙ → 𝐴 ∈ ℕ0 ) → if ( 𝑛 ∈ ℙ , ( 𝑛 ↑ 𝐴 ) , 1 ) ∈ ℕ ) )
12		iffalse	⊢ ( ¬ 𝑛 ∈ ℙ → if ( 𝑛 ∈ ℙ , ( 𝑛 ↑ 𝐴 ) , 1 ) = 1 )
13		1nn	⊢ 1 ∈ ℕ
14	12 13	eqeltrdi	⊢ ( ¬ 𝑛 ∈ ℙ → if ( 𝑛 ∈ ℙ , ( 𝑛 ↑ 𝐴 ) , 1 ) ∈ ℕ )
15	14	a1d	⊢ ( ¬ 𝑛 ∈ ℙ → ( ( 𝑛 ∈ ℙ → 𝐴 ∈ ℕ0 ) → if ( 𝑛 ∈ ℙ , ( 𝑛 ↑ 𝐴 ) , 1 ) ∈ ℕ ) )
16	11 15	pm2.61i	⊢ ( ( 𝑛 ∈ ℙ → 𝐴 ∈ ℕ0 ) → if ( 𝑛 ∈ ℙ , ( 𝑛 ↑ 𝐴 ) , 1 ) ∈ ℕ )
17	16	a1d	⊢ ( ( 𝑛 ∈ ℙ → 𝐴 ∈ ℕ0 ) → ( 𝑛 ∈ ℕ → if ( 𝑛 ∈ ℙ , ( 𝑛 ↑ 𝐴 ) , 1 ) ∈ ℕ ) )
18	17	ralimi2	⊢ ( ∀ 𝑛 ∈ ℙ 𝐴 ∈ ℕ0 → ∀ 𝑛 ∈ ℕ if ( 𝑛 ∈ ℙ , ( 𝑛 ↑ 𝐴 ) , 1 ) ∈ ℕ )
19	2 18	syl	⊢ ( 𝜑 → ∀ 𝑛 ∈ ℕ if ( 𝑛 ∈ ℙ , ( 𝑛 ↑ 𝐴 ) , 1 ) ∈ ℕ )
20	1	fmpt	⊢ ( ∀ 𝑛 ∈ ℕ if ( 𝑛 ∈ ℙ , ( 𝑛 ↑ 𝐴 ) , 1 ) ∈ ℕ ↔ 𝐹 : ℕ ⟶ ℕ )
21	19 20	sylib	⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ℕ )
22		nnuz	⊢ ℕ = ( ℤ≥ ‘ 1 )
23		1zzd	⊢ ( 𝜑 → 1 ∈ ℤ )
24	21	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝐹 ‘ 𝑘 ) ∈ ℕ )
25		nnmulcl	⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑝 ∈ ℕ ) → ( 𝑘 · 𝑝 ) ∈ ℕ )
26	25	adantl	⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 𝑝 ∈ ℕ ) ) → ( 𝑘 · 𝑝 ) ∈ ℕ )
27	22 23 24 26	seqf	⊢ ( 𝜑 → seq 1 ( · , 𝐹 ) : ℕ ⟶ ℕ )
28	21 27	jca	⊢ ( 𝜑 → ( 𝐹 : ℕ ⟶ ℕ ∧ seq 1 ( · , 𝐹 ) : ℕ ⟶ ℕ ) )