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 simpr 
 |-  ( ( A e. NN /\ { p e. Prime | p || A } ~~ 1o ) -> { p e. Prime | p || A } ~~ 1o )
17 en1b 
 |-  ( { p e. Prime | p || A } ~~ 1o <-> { p e. Prime | p || A } = { U. { p e. Prime | p || A } } )
18 16 17 sylib 
 |-  ( ( A e. NN /\ { p e. Prime | p || A } ~~ 1o ) -> { p e. Prime | p || A } = { U. { p e. Prime | p || A } } )
19 ssrab2 
 |-  { p e. Prime | p || A } C_ Prime
20 18 19 eqsstrrdi 
 |-  ( ( A e. NN /\ { p e. Prime | p || A } ~~ 1o ) -> { U. { p e. Prime | p || A } } C_ Prime )
21 7 uniexd 
 |-  ( A e. NN -> U. { p e. Prime | p || A } e. _V )
22 21 adantr 
 |-  ( ( A e. NN /\ { p e. Prime | p || A } ~~ 1o ) -> U. { p e. Prime | p || A } e. _V )
23 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 ) )
24 22 23 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 ) )
25 20 24 mpbird 
 |-  ( ( A e. NN /\ { p e. Prime | p || A } ~~ 1o ) -> U. { p e. Prime | p || A } e. Prime )
26 prmuz2 
 |-  ( U. { p e. Prime | p || A } e. Prime -> U. { p e. Prime | p || A } e. ( ZZ>= ` 2 ) )
27 25 26 syl 
 |-  ( ( A e. NN /\ { p e. Prime | p || A } ~~ 1o ) -> U. { p e. Prime | p || A } e. ( ZZ>= ` 2 ) )
28 eluzelre 
 |-  ( U. { p e. Prime | p || A } e. ( ZZ>= ` 2 ) -> U. { p e. Prime | p || A } e. RR )
29 27 28 syl 
 |-  ( ( A e. NN /\ { p e. Prime | p || A } ~~ 1o ) -> U. { p e. Prime | p || A } e. RR )
30 eluz2gt1 
 |-  ( U. { p e. Prime | p || A } e. ( ZZ>= ` 2 ) -> 1 < U. { p e. Prime | p || A } )
31 27 30 syl 
 |-  ( ( A e. NN /\ { p e. Prime | p || A } ~~ 1o ) -> 1 < U. { p e. Prime | p || A } )
32 29 31 rplogcld 
 |-  ( ( A e. NN /\ { p e. Prime | p || A } ~~ 1o ) -> ( log ` U. { p e. Prime | p || A } ) e. RR+ )
33 32 rpne0d 
 |-  ( ( A e. NN /\ { p e. Prime | p || A } ~~ 1o ) -> ( log ` U. { p e. Prime | p || A } ) =/= 0 )
34 15 33 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 )
35 34 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 ) )
36 iffalse 
 |-  ( -. ( # ` { p e. Prime | p || A } ) = 1 -> if ( ( # ` { p e. Prime | p || A } ) = 1 , ( log ` U. { p e. Prime | p || A } ) , 0 ) = 0 )
37 36 necon1ai 
 |-  ( if ( ( # ` { p e. Prime | p || A } ) = 1 , ( log ` U. { p e. Prime | p || A } ) , 0 ) =/= 0 -> ( # ` { p e. Prime | p || A } ) = 1 )
38 37 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 ) )
39 35 38 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 ) )
40 4 39 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 ) )
41 3 40 bitr4d 
 |-  ( A e. NN -> ( ( Lam ` A ) =/= 0 <-> E! p e. Prime p || A ) )