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 e. NN |-> if ( n e. Prime , ( n ^ A ) , 1 ) )
pcmpt.2 
|- ( ph -> A. n e. Prime A e. NN0 )
Assertion pcmptcl 
|- ( ph -> ( F : NN --> NN /\ seq 1 ( x. , F ) : NN --> NN ) )

Proof

Step Hyp Ref Expression
1 pcmpt.1 
 |-  F = ( n e. NN |-> if ( n e. Prime , ( n ^ A ) , 1 ) )
2 pcmpt.2 
 |-  ( ph -> A. n e. Prime A e. NN0 )
3 pm2.27 
 |-  ( n e. Prime -> ( ( n e. Prime -> A e. NN0 ) -> A e. NN0 ) )
4 iftrue 
 |-  ( n e. Prime -> if ( n e. Prime , ( n ^ A ) , 1 ) = ( n ^ A ) )
5 4 adantr 
 |-  ( ( n e. Prime /\ A e. NN0 ) -> if ( n e. Prime , ( n ^ A ) , 1 ) = ( n ^ A ) )
6 prmnn 
 |-  ( n e. Prime -> n e. NN )
7 nnexpcl 
 |-  ( ( n e. NN /\ A e. NN0 ) -> ( n ^ A ) e. NN )
8 6 7 sylan 
 |-  ( ( n e. Prime /\ A e. NN0 ) -> ( n ^ A ) e. NN )
9 5 8 eqeltrd 
 |-  ( ( n e. Prime /\ A e. NN0 ) -> if ( n e. Prime , ( n ^ A ) , 1 ) e. NN )
10 9 ex 
 |-  ( n e. Prime -> ( A e. NN0 -> if ( n e. Prime , ( n ^ A ) , 1 ) e. NN ) )
11 3 10 syld 
 |-  ( n e. Prime -> ( ( n e. Prime -> A e. NN0 ) -> if ( n e. Prime , ( n ^ A ) , 1 ) e. NN ) )
12 iffalse 
 |-  ( -. n e. Prime -> if ( n e. Prime , ( n ^ A ) , 1 ) = 1 )
13 1nn 
 |-  1 e. NN
14 12 13 eqeltrdi 
 |-  ( -. n e. Prime -> if ( n e. Prime , ( n ^ A ) , 1 ) e. NN )
15 14 a1d 
 |-  ( -. n e. Prime -> ( ( n e. Prime -> A e. NN0 ) -> if ( n e. Prime , ( n ^ A ) , 1 ) e. NN ) )
16 11 15 pm2.61i 
 |-  ( ( n e. Prime -> A e. NN0 ) -> if ( n e. Prime , ( n ^ A ) , 1 ) e. NN )
17 16 a1d 
 |-  ( ( n e. Prime -> A e. NN0 ) -> ( n e. NN -> if ( n e. Prime , ( n ^ A ) , 1 ) e. NN ) )
18 17 ralimi2 
 |-  ( A. n e. Prime A e. NN0 -> A. n e. NN if ( n e. Prime , ( n ^ A ) , 1 ) e. NN )
19 2 18 syl 
 |-  ( ph -> A. n e. NN if ( n e. Prime , ( n ^ A ) , 1 ) e. NN )
20 1 fmpt 
 |-  ( A. n e. NN if ( n e. Prime , ( n ^ A ) , 1 ) e. NN <-> F : NN --> NN )
21 19 20 sylib 
 |-  ( ph -> F : NN --> NN )
22 nnuz 
 |-  NN = ( ZZ>= ` 1 )
23 1zzd 
 |-  ( ph -> 1 e. ZZ )
24 21 ffvelrnda 
 |-  ( ( ph /\ k e. NN ) -> ( F ` k ) e. NN )
25 nnmulcl 
 |-  ( ( k e. NN /\ p e. NN ) -> ( k x. p ) e. NN )
26 25 adantl 
 |-  ( ( ph /\ ( k e. NN /\ p e. NN ) ) -> ( k x. p ) e. NN )
27 22 23 24 26 seqf 
 |-  ( ph -> seq 1 ( x. , F ) : NN --> NN )
28 21 27 jca 
 |-  ( ph -> ( F : NN --> NN /\ seq 1 ( x. , F ) : NN --> NN ) )