Metamath Proof Explorer

Theorem pcprod

Description: The product of the primes taken to their respective powers reconstructs the original number. (Contributed by Mario Carneiro, 12-Mar-2014)

Ref Expression
Hypothesis pcprod.1 ⊢ F = n ∈ ℕ ⟼ if n ∈ ℙ n n pCnt N 1
Assertion pcprod ⊢ N ∈ ℕ → seq 1 × F ⁡ N = N

Proof

Step Hyp Ref Expression
1 pcprod.1 ⊢ F = n ∈ ℕ ⟼ if n ∈ ℙ n n pCnt N 1
2 pccl ⊢ n ∈ ℙ ∧ N ∈ ℕ → n pCnt N ∈ ℕ 0
3 2 ancoms ⊢ N ∈ ℕ ∧ n ∈ ℙ → n pCnt N ∈ ℕ 0
4 3 ralrimiva ⊢ N ∈ ℕ → ∀ n ∈ ℙ n pCnt N ∈ ℕ 0
5 4 adantl ⊢ p ∈ ℙ ∧ N ∈ ℕ → ∀ n ∈ ℙ n pCnt N ∈ ℕ 0
6 simpr ⊢ p ∈ ℙ ∧ N ∈ ℕ → N ∈ ℕ
7 simpl ⊢ p ∈ ℙ ∧ N ∈ ℕ → p ∈ ℙ
8 oveq1 ⊢ n = p → n pCnt N = p pCnt N
9 1 5 6 7 8 pcmpt ⊢ p ∈ ℙ ∧ N ∈ ℕ → p pCnt seq 1 × F ⁡ N = if p ≤ N p pCnt N 0
10 iftrue ⊢ p ≤ N → if p ≤ N p pCnt N 0 = p pCnt N
11 10 adantl ⊢ p ∈ ℙ ∧ N ∈ ℕ ∧ p ≤ N → if p ≤ N p pCnt N 0 = p pCnt N
12 iffalse ⊢ ¬ p ≤ N → if p ≤ N p pCnt N 0 = 0
13 12 adantl ⊢ p ∈ ℙ ∧ N ∈ ℕ ∧ ¬ p ≤ N → if p ≤ N p pCnt N 0 = 0
14 prmz ⊢ p ∈ ℙ → p ∈ ℤ
15 dvdsle ⊢ p ∈ ℤ ∧ N ∈ ℕ → p ∥ N → p ≤ N
16 14 15 sylan ⊢ p ∈ ℙ ∧ N ∈ ℕ → p ∥ N → p ≤ N
17 16 con3dimp ⊢ p ∈ ℙ ∧ N ∈ ℕ ∧ ¬ p ≤ N → ¬ p ∥ N
18 pceq0 ⊢ p ∈ ℙ ∧ N ∈ ℕ → p pCnt N = 0 ↔ ¬ p ∥ N
19 18 adantr ⊢ p ∈ ℙ ∧ N ∈ ℕ ∧ ¬ p ≤ N → p pCnt N = 0 ↔ ¬ p ∥ N
20 17 19 mpbird ⊢ p ∈ ℙ ∧ N ∈ ℕ ∧ ¬ p ≤ N → p pCnt N = 0
21 13 20 eqtr4d ⊢ p ∈ ℙ ∧ N ∈ ℕ ∧ ¬ p ≤ N → if p ≤ N p pCnt N 0 = p pCnt N
22 11 21 pm2.61dan ⊢ p ∈ ℙ ∧ N ∈ ℕ → if p ≤ N p pCnt N 0 = p pCnt N
23 9 22 eqtrd ⊢ p ∈ ℙ ∧ N ∈ ℕ → p pCnt seq 1 × F ⁡ N = p pCnt N
24 23 ancoms ⊢ N ∈ ℕ ∧ p ∈ ℙ → p pCnt seq 1 × F ⁡ N = p pCnt N
25 24 ralrimiva ⊢ N ∈ ℕ → ∀ p ∈ ℙ p pCnt seq 1 × F ⁡ N = p pCnt N
26 1 4 pcmptcl ⊢ N ∈ ℕ → F : ℕ ⟶ ℕ ∧ seq 1 × F : ℕ ⟶ ℕ
27 26 simprd ⊢ N ∈ ℕ → seq 1 × F : ℕ ⟶ ℕ
28 ffvelrn ⊢ seq 1 × F : ℕ ⟶ ℕ ∧ N ∈ ℕ → seq 1 × F ⁡ N ∈ ℕ
29 27 28 mpancom ⊢ N ∈ ℕ → seq 1 × F ⁡ N ∈ ℕ
30 29 nnnn0d ⊢ N ∈ ℕ → seq 1 × F ⁡ N ∈ ℕ 0
31 nnnn0 ⊢ N ∈ ℕ → N ∈ ℕ 0
32 pc11 ⊢ seq 1 × F ⁡ N ∈ ℕ 0 ∧ N ∈ ℕ 0 → seq 1 × F ⁡ N = N ↔ ∀ p ∈ ℙ p pCnt seq 1 × F ⁡ N = p pCnt N
33 30 31 32 syl2anc ⊢ N ∈ ℕ → seq 1 × F ⁡ N = N ↔ ∀ p ∈ ℙ p pCnt seq 1 × F ⁡ N = p pCnt N
34 25 33 mpbird ⊢ N ∈ ℕ → seq 1 × F ⁡ N = N