Metamath Proof Explorer

Theorem pcmptcl

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

Ref Expression
Hypotheses pcmpt.1 ⊢ F = n ∈ ℕ ⟼ if n ∈ ℙ n A 1
pcmpt.2 ⊢ φ → ∀ n ∈ ℙ A ∈ ℕ 0
Assertion pcmptcl ⊢ φ → F : ℕ ⟶ ℕ ∧ seq 1 × F : ℕ ⟶ ℕ

Proof

Step Hyp Ref Expression
1 pcmpt.1 ⊢ F = n ∈ ℕ ⟼ if n ∈ ℙ n A 1
2 pcmpt.2 ⊢ φ → ∀ n ∈ ℙ A ∈ ℕ 0
3 pm2.27 ⊢ n ∈ ℙ → n ∈ ℙ → A ∈ ℕ 0 → A ∈ ℕ 0
4 iftrue ⊢ n ∈ ℙ → if n ∈ ℙ n A 1 = n A
5 4 adantr ⊢ n ∈ ℙ ∧ A ∈ ℕ 0 → if n ∈ ℙ n A 1 = n A
6 prmnn ⊢ n ∈ ℙ → n ∈ ℕ
7 nnexpcl ⊢ n ∈ ℕ ∧ A ∈ ℕ 0 → n A ∈ ℕ
8 6 7 sylan ⊢ n ∈ ℙ ∧ A ∈ ℕ 0 → n A ∈ ℕ
9 5 8 eqeltrd ⊢ n ∈ ℙ ∧ A ∈ ℕ 0 → if n ∈ ℙ n A 1 ∈ ℕ
10 9 ex ⊢ n ∈ ℙ → A ∈ ℕ 0 → if n ∈ ℙ n A 1 ∈ ℕ
11 3 10 syld ⊢ n ∈ ℙ → n ∈ ℙ → A ∈ ℕ 0 → if n ∈ ℙ n A 1 ∈ ℕ
12 iffalse ⊢ ¬ n ∈ ℙ → if n ∈ ℙ n A 1 = 1
13 1nn ⊢ 1 ∈ ℕ
14 12 13 eqeltrdi ⊢ ¬ n ∈ ℙ → if n ∈ ℙ n A 1 ∈ ℕ
15 14 a1d ⊢ ¬ n ∈ ℙ → n ∈ ℙ → A ∈ ℕ 0 → if n ∈ ℙ n A 1 ∈ ℕ
16 11 15 pm2.61i ⊢ n ∈ ℙ → A ∈ ℕ 0 → if n ∈ ℙ n A 1 ∈ ℕ
17 16 a1d ⊢ n ∈ ℙ → A ∈ ℕ 0 → n ∈ ℕ → if n ∈ ℙ n A 1 ∈ ℕ
18 17 ralimi2 ⊢ ∀ n ∈ ℙ A ∈ ℕ 0 → ∀ n ∈ ℕ if n ∈ ℙ n A 1 ∈ ℕ
19 2 18 syl ⊢ φ → ∀ n ∈ ℕ if n ∈ ℙ n A 1 ∈ ℕ
20 1 fmpt ⊢ ∀ n ∈ ℕ if n ∈ ℙ n A 1 ∈ ℕ ↔ F : ℕ ⟶ ℕ
21 19 20 sylib ⊢ φ → F : ℕ ⟶ ℕ
22 nnuz ⊢ ℕ = ℤ ≥ 1
23 1zzd ⊢ φ → 1 ∈ ℤ
24 21 ffvelrnda ⊢ φ ∧ k ∈ ℕ → F ⁡ k ∈ ℕ
25 nnmulcl ⊢ k ∈ ℕ ∧ p ∈ ℕ → k ⁢ p ∈ ℕ
26 25 adantl ⊢ φ ∧ k ∈ ℕ ∧ p ∈ ℕ → k ⁢ p ∈ ℕ
27 22 23 24 26 seqf ⊢ φ → seq 1 × F : ℕ ⟶ ℕ
28 21 27 jca ⊢ φ → F : ℕ ⟶ ℕ ∧ seq 1 × F : ℕ ⟶ ℕ