This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝐹 ‘ 𝑘 ) ∈ ℕ )
25 nnmulcl ⊢ ( ( 𝑘 ∈ ℕ ∧ 𝑝 ∈ ℕ ) → ( 𝑘 · 𝑝 ) ∈ ℕ )
26 25 adantl ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 𝑝 ∈ ℕ ) ) → ( 𝑘 · 𝑝 ) ∈ ℕ )
27 22 23 24 26 seqf ⊢ ( 𝜑 → seq 1 ( · , 𝐹 ) : ℕ ⟶ ℕ )
28 21 27 jca ⊢ ( 𝜑 → ( 𝐹 : ℕ ⟶ ℕ ∧ seq 1 ( · , 𝐹 ) : ℕ ⟶ ℕ ) )