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 e. NN |-> if ( n e. Prime , ( n ^ ( n pCnt N ) ) , 1 ) )
Assertion pcprod 
|- ( N e. NN -> ( seq 1 ( x. , F ) ` N ) = N )

Proof

Step Hyp Ref Expression
1 pcprod.1 
 |-  F = ( n e. NN |-> if ( n e. Prime , ( n ^ ( n pCnt N ) ) , 1 ) )
2 pccl 
 |-  ( ( n e. Prime /\ N e. NN ) -> ( n pCnt N ) e. NN0 )
3 2 ancoms 
 |-  ( ( N e. NN /\ n e. Prime ) -> ( n pCnt N ) e. NN0 )
4 3 ralrimiva 
 |-  ( N e. NN -> A. n e. Prime ( n pCnt N ) e. NN0 )
5 4 adantl 
 |-  ( ( p e. Prime /\ N e. NN ) -> A. n e. Prime ( n pCnt N ) e. NN0 )
6 simpr 
 |-  ( ( p e. Prime /\ N e. NN ) -> N e. NN )
7 simpl 
 |-  ( ( p e. Prime /\ N e. NN ) -> p e. Prime )
8 oveq1 
 |-  ( n = p -> ( n pCnt N ) = ( p pCnt N ) )
9 1 5 6 7 8 pcmpt 
 |-  ( ( p e. Prime /\ N e. NN ) -> ( p pCnt ( seq 1 ( x. , 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 e. Prime /\ N e. NN ) /\ 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 e. Prime /\ N e. NN ) /\ -. p <_ N ) -> if ( p <_ N , ( p pCnt N ) , 0 ) = 0 )
14 prmz 
 |-  ( p e. Prime -> p e. ZZ )
15 dvdsle 
 |-  ( ( p e. ZZ /\ N e. NN ) -> ( p || N -> p <_ N ) )
16 14 15 sylan 
 |-  ( ( p e. Prime /\ N e. NN ) -> ( p || N -> p <_ N ) )
17 16 con3dimp 
 |-  ( ( ( p e. Prime /\ N e. NN ) /\ -. p <_ N ) -> -. p || N )
18 pceq0 
 |-  ( ( p e. Prime /\ N e. NN ) -> ( ( p pCnt N ) = 0 <-> -. p || N ) )
19 18 adantr 
 |-  ( ( ( p e. Prime /\ N e. NN ) /\ -. p <_ N ) -> ( ( p pCnt N ) = 0 <-> -. p || N ) )
20 17 19 mpbird 
 |-  ( ( ( p e. Prime /\ N e. NN ) /\ -. p <_ N ) -> ( p pCnt N ) = 0 )
21 13 20 eqtr4d 
 |-  ( ( ( p e. Prime /\ N e. NN ) /\ -. p <_ N ) -> if ( p <_ N , ( p pCnt N ) , 0 ) = ( p pCnt N ) )
22 11 21 pm2.61dan 
 |-  ( ( p e. Prime /\ N e. NN ) -> if ( p <_ N , ( p pCnt N ) , 0 ) = ( p pCnt N ) )
23 9 22 eqtrd 
 |-  ( ( p e. Prime /\ N e. NN ) -> ( p pCnt ( seq 1 ( x. , F ) ` N ) ) = ( p pCnt N ) )
24 23 ancoms 
 |-  ( ( N e. NN /\ p e. Prime ) -> ( p pCnt ( seq 1 ( x. , F ) ` N ) ) = ( p pCnt N ) )
25 24 ralrimiva 
 |-  ( N e. NN -> A. p e. Prime ( p pCnt ( seq 1 ( x. , F ) ` N ) ) = ( p pCnt N ) )
26 1 4 pcmptcl 
 |-  ( N e. NN -> ( F : NN --> NN /\ seq 1 ( x. , F ) : NN --> NN ) )
27 26 simprd 
 |-  ( N e. NN -> seq 1 ( x. , F ) : NN --> NN )
28 ffvelrn 
 |-  ( ( seq 1 ( x. , F ) : NN --> NN /\ N e. NN ) -> ( seq 1 ( x. , F ) ` N ) e. NN )
29 27 28 mpancom 
 |-  ( N e. NN -> ( seq 1 ( x. , F ) ` N ) e. NN )
30 29 nnnn0d 
 |-  ( N e. NN -> ( seq 1 ( x. , F ) ` N ) e. NN0 )
31 nnnn0 
 |-  ( N e. NN -> N e. NN0 )
32 pc11 
 |-  ( ( ( seq 1 ( x. , F ) ` N ) e. NN0 /\ N e. NN0 ) -> ( ( seq 1 ( x. , F ) ` N ) = N <-> A. p e. Prime ( p pCnt ( seq 1 ( x. , F ) ` N ) ) = ( p pCnt N ) ) )
33 30 31 32 syl2anc 
 |-  ( N e. NN -> ( ( seq 1 ( x. , F ) ` N ) = N <-> A. p e. Prime ( p pCnt ( seq 1 ( x. , F ) ` N ) ) = ( p pCnt N ) ) )
34 25 33 mpbird 
 |-  ( N e. NN -> ( seq 1 ( x. , F ) ` N ) = N )