Metamath Proof Explorer

Theorem isppw

Description: Two ways to say that A is a prime power. (Contributed by Mario Carneiro, 7-Apr-2016)

Ref Expression
Assertion isppw 
|- ( A e. NN -> ( ( Lam ` A ) =/= 0 <-> E! p e. Prime p || A ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  { p e. Prime | p || A } = { p e. Prime | p || A }
2 1 vmaval 
 |-  ( A e. NN -> ( Lam ` A ) = if ( ( # ` { p e. Prime | p || A } ) = 1 , ( log ` U. { p e. Prime | p || A } ) , 0 ) )
3 2 neeq1d 
 |-  ( A e. NN -> ( ( Lam ` A ) =/= 0 <-> if ( ( # ` { p e. Prime | p || A } ) = 1 , ( log ` U. { p e. Prime | p || A } ) , 0 ) =/= 0 ) )
4 reuen1 
 |-  ( E! p e. Prime p || A <-> { p e. Prime | p || A } ~~ 1o )
5 hash1 
 |-  ( # ` 1o ) = 1
6 5 eqeq2i 
 |-  ( ( # ` { p e. Prime | p || A } ) = ( # ` 1o ) <-> ( # ` { p e. Prime | p || A } ) = 1 )
7 prmdvdsfi 
 |-  ( A e. NN -> { p e. Prime | p || A } e. Fin )
8 1onn 
 |-  1o e. _om
9 nnfi 
 |-  ( 1o e. _om -> 1o e. Fin )
10 8 9 ax-mp 
 |-  1o e. Fin
11 hashen 
 |-  ( ( { p e. Prime | p || A } e. Fin /\ 1o e. Fin ) -> ( ( # ` { p e. Prime | p || A } ) = ( # ` 1o ) <-> { p e. Prime | p || A } ~~ 1o ) )
12 7 10 11 sylancl 
 |-  ( A e. NN -> ( ( # ` { p e. Prime | p || A } ) = ( # ` 1o ) <-> { p e. Prime | p || A } ~~ 1o ) )
13 6 12 bitr3id 
 |-  ( A e. NN -> ( ( # ` { p e. Prime | p || A } ) = 1 <-> { p e. Prime | p || A } ~~ 1o ) )
14 13 biimpar 
 |-  ( ( A e. NN /\ { p e. Prime | p || A } ~~ 1o ) -> ( # ` { p e. Prime | p || A } ) = 1 )
15 14 iftrued 
 |-  ( ( A e. NN /\ { p e. Prime | p || A } ~~ 1o ) -> if ( ( # ` { p e. Prime | p || A } ) = 1 , ( log ` U. { p e. Prime | p || A } ) , 0 ) = ( log ` U. { p e. Prime | p || A } ) )
16 en1b 
 |-  ( { p e. Prime | p || A } ~~ 1o <-> { p e. Prime | p || A } = { U. { p e. Prime | p || A } } )
17 16 bilani 
 |-  ( ( A e. NN /\ { p e. Prime | p || A } ~~ 1o ) -> { p e. Prime | p || A } = { U. { p e. Prime | p || A } } )
18 ssrab2 
 |-  { p e. Prime | p || A } C_ Prime
19 17 18 eqsstrrdi 
 |-  ( ( A e. NN /\ { p e. Prime | p || A } ~~ 1o ) -> { U. { p e. Prime | p || A } } C_ Prime )
20 7 uniexd 
 |-  ( A e. NN -> U. { p e. Prime | p || A } e. _V )
21 20 adantr 
 |-  ( ( A e. NN /\ { p e. Prime | p || A } ~~ 1o ) -> U. { p e. Prime | p || A } e. _V )
22 snssg 
 |-  ( U. { p e. Prime | p || A } e. _V -> ( U. { p e. Prime | p || A } e. Prime <-> { U. { p e. Prime | p || A } } C_ Prime ) )
23 21 22 syl 
 |-  ( ( A e. NN /\ { p e. Prime | p || A } ~~ 1o ) -> ( U. { p e. Prime | p || A } e. Prime <-> { U. { p e. Prime | p || A } } C_ Prime ) )
24 19 23 mpbird 
 |-  ( ( A e. NN /\ { p e. Prime | p || A } ~~ 1o ) -> U. { p e. Prime | p || A } e. Prime )
25 prmuz2 
 |-  ( U. { p e. Prime | p || A } e. Prime -> U. { p e. Prime | p || A } e. ( ZZ>= ` 2 ) )
26 24 25 syl 
 |-  ( ( A e. NN /\ { p e. Prime | p || A } ~~ 1o ) -> U. { p e. Prime | p || A } e. ( ZZ>= ` 2 ) )
27 eluzelre 
 |-  ( U. { p e. Prime | p || A } e. ( ZZ>= ` 2 ) -> U. { p e. Prime | p || A } e. RR )
28 26 27 syl 
 |-  ( ( A e. NN /\ { p e. Prime | p || A } ~~ 1o ) -> U. { p e. Prime | p || A } e. RR )
29 eluz2gt1 
 |-  ( U. { p e. Prime | p || A } e. ( ZZ>= ` 2 ) -> 1 < U. { p e. Prime | p || A } )
30 26 29 syl 
 |-  ( ( A e. NN /\ { p e. Prime | p || A } ~~ 1o ) -> 1 < U. { p e. Prime | p || A } )
31 28 30 rplogcld 
 |-  ( ( A e. NN /\ { p e. Prime | p || A } ~~ 1o ) -> ( log ` U. { p e. Prime | p || A } ) e. RR+ )
32 31 rpne0d 
 |-  ( ( A e. NN /\ { p e. Prime | p || A } ~~ 1o ) -> ( log ` U. { p e. Prime | p || A } ) =/= 0 )
33 15 32 eqnetrd 
 |-  ( ( A e. NN /\ { p e. Prime | p || A } ~~ 1o ) -> if ( ( # ` { p e. Prime | p || A } ) = 1 , ( log ` U. { p e. Prime | p || A } ) , 0 ) =/= 0 )
34 33 ex 
 |-  ( A e. NN -> ( { p e. Prime | p || A } ~~ 1o -> if ( ( # ` { p e. Prime | p || A } ) = 1 , ( log ` U. { p e. Prime | p || A } ) , 0 ) =/= 0 ) )
35 iffalse 
 |-  ( -. ( # ` { p e. Prime | p || A } ) = 1 -> if ( ( # ` { p e. Prime | p || A } ) = 1 , ( log ` U. { p e. Prime | p || A } ) , 0 ) = 0 )
36 35 necon1ai 
 |-  ( if ( ( # ` { p e. Prime | p || A } ) = 1 , ( log ` U. { p e. Prime | p || A } ) , 0 ) =/= 0 -> ( # ` { p e. Prime | p || A } ) = 1 )
37 36 13 imbitrid 
 |-  ( A e. NN -> ( if ( ( # ` { p e. Prime | p || A } ) = 1 , ( log ` U. { p e. Prime | p || A } ) , 0 ) =/= 0 -> { p e. Prime | p || A } ~~ 1o ) )
38 34 37 impbid 
 |-  ( A e. NN -> ( { p e. Prime | p || A } ~~ 1o <-> if ( ( # ` { p e. Prime | p || A } ) = 1 , ( log ` U. { p e. Prime | p || A } ) , 0 ) =/= 0 ) )
39 4 38 bitrid 
 |-  ( A e. NN -> ( E! p e. Prime p || A <-> if ( ( # ` { p e. Prime | p || A } ) = 1 , ( log ` U. { p e. Prime | p || A } ) , 0 ) =/= 0 ) )
40 3 39 bitr4d 
 |-  ( A e. NN -> ( ( Lam ` A ) =/= 0 <-> E! p e. Prime p || A ) )