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∈ℕ⟼ifn∈ℙnnpCntN1
Assertion pcprod ⊢N∈ℕ→seq1×F⁡N=N

Proof

Step Hyp Ref Expression
1 pcprod.1 ⊢F=n∈ℕ⟼ifn∈ℙnnpCntN1
2 pccl ⊢n∈ℙ∧N∈ℕ→npCntN∈ℕ0
3 2 ancoms ⊢N∈ℕ∧n∈ℙ→npCntN∈ℕ0
4 3 ralrimiva ⊢N∈ℕ→∀n∈ℙnpCntN∈ℕ0
5 4 adantl ⊢p∈ℙ∧N∈ℕ→∀n∈ℙnpCntN∈ℕ0
6 simpr ⊢p∈ℙ∧N∈ℕ→N∈ℕ
7 simpl ⊢p∈ℙ∧N∈ℕ→p∈ℙ
8 oveq1 ⊢n=p→npCntN=ppCntN
9 1 5 6 7 8 pcmpt ⊢p∈ℙ∧N∈ℕ→ppCntseq1×F⁡N=ifp≤NppCntN0
10 iftrue ⊢p≤N→ifp≤NppCntN0=ppCntN
11 10 adantl ⊢p∈ℙ∧N∈ℕ∧p≤N→ifp≤NppCntN0=ppCntN
12 iffalse ⊢¬p≤N→ifp≤NppCntN0=0
13 12 adantl ⊢p∈ℙ∧N∈ℕ∧¬p≤N→ifp≤NppCntN0=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∈ℕ→ppCntN=0↔¬p∥N
19 18 adantr ⊢p∈ℙ∧N∈ℕ∧¬p≤N→ppCntN=0↔¬p∥N
20 17 19 mpbird ⊢p∈ℙ∧N∈ℕ∧¬p≤N→ppCntN=0
21 13 20 eqtr4d ⊢p∈ℙ∧N∈ℕ∧¬p≤N→ifp≤NppCntN0=ppCntN
22 11 21 pm2.61dan ⊢p∈ℙ∧N∈ℕ→ifp≤NppCntN0=ppCntN
23 9 22 eqtrd ⊢p∈ℙ∧N∈ℕ→ppCntseq1×F⁡N=ppCntN
24 23 ancoms ⊢N∈ℕ∧p∈ℙ→ppCntseq1×F⁡N=ppCntN
25 24 ralrimiva ⊢N∈ℕ→∀p∈ℙppCntseq1×F⁡N=ppCntN
26 1 4 pcmptcl ⊢N∈ℕ→F:ℕ⟶ℕ∧seq1×F:ℕ⟶ℕ
27 26 simprd ⊢N∈ℕ→seq1×F:ℕ⟶ℕ
28 ffvelcdm ⊢seq1×F:ℕ⟶ℕ∧N∈ℕ→seq1×F⁡N∈ℕ
29 27 28 mpancom ⊢N∈ℕ→seq1×F⁡N∈ℕ
30 29 nnnn0d ⊢N∈ℕ→seq1×F⁡N∈ℕ0
31 nnnn0 ⊢N∈ℕ→N∈ℕ0
32 pc11 ⊢seq1×F⁡N∈ℕ0∧N∈ℕ0→seq1×F⁡N=N↔∀p∈ℙppCntseq1×F⁡N=ppCntN
33 30 31 32 syl2anc ⊢N∈ℕ→seq1×F⁡N=N↔∀p∈ℙppCntseq1×F⁡N=ppCntN
34 25 33 mpbird ⊢N∈ℕ→seq1×F⁡N=N