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 ⊢ 𝐹 = ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( 𝑛 ↑ ( 𝑛 pCnt 𝑁 ) ) , 1 ) )
Assertion pcprod ( 𝑁 ∈ ℕ → ( seq 1 ( · , 𝐹 ) ‘ 𝑁 ) = 𝑁 )

Proof

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