Metamath Proof Explorer

Theorem isnsqf

Description: Two ways to say that a number is not squarefree. (Contributed by Mario Carneiro, 3-Oct-2014)

Ref Expression
Assertion isnsqf 
|- ( A e. NN -> ( ( mmu ` A ) = 0 <-> E. p e. Prime ( p ^ 2 ) || A ) )

Proof

Step Hyp Ref Expression
1 neg1cn 
 |-  -u 1 e. CC
2 neg1ne0 
 |-  -u 1 =/= 0
3 prmdvdsfi 
 |-  ( A e. NN -> { p e. Prime | p || A } e. Fin )
4 hashcl 
 |-  ( { p e. Prime | p || A } e. Fin -> ( # ` { p e. Prime | p || A } ) e. NN0 )
5 3 4 syl 
 |-  ( A e. NN -> ( # ` { p e. Prime | p || A } ) e. NN0 )
6 5 nn0zd 
 |-  ( A e. NN -> ( # ` { p e. Prime | p || A } ) e. ZZ )
7 expne0i 
 |-  ( ( -u 1 e. CC /\ -u 1 =/= 0 /\ ( # ` { p e. Prime | p || A } ) e. ZZ ) -> ( -u 1 ^ ( # ` { p e. Prime | p || A } ) ) =/= 0 )
8 1 2 6 7 mp3an12i 
 |-  ( A e. NN -> ( -u 1 ^ ( # ` { p e. Prime | p || A } ) ) =/= 0 )
9 iffalse 
 |-  ( -. E. p e. Prime ( p ^ 2 ) || A -> if ( E. p e. Prime ( p ^ 2 ) || A , 0 , ( -u 1 ^ ( # ` { p e. Prime | p || A } ) ) ) = ( -u 1 ^ ( # ` { p e. Prime | p || A } ) ) )
10 9 neeq1d 
 |-  ( -. E. p e. Prime ( p ^ 2 ) || A -> ( if ( E. p e. Prime ( p ^ 2 ) || A , 0 , ( -u 1 ^ ( # ` { p e. Prime | p || A } ) ) ) =/= 0 <-> ( -u 1 ^ ( # ` { p e. Prime | p || A } ) ) =/= 0 ) )
11 8 10 syl5ibrcom 
 |-  ( A e. NN -> ( -. E. p e. Prime ( p ^ 2 ) || A -> if ( E. p e. Prime ( p ^ 2 ) || A , 0 , ( -u 1 ^ ( # ` { p e. Prime | p || A } ) ) ) =/= 0 ) )
12 muval 
 |-  ( A e. NN -> ( mmu ` A ) = if ( E. p e. Prime ( p ^ 2 ) || A , 0 , ( -u 1 ^ ( # ` { p e. Prime | p || A } ) ) ) )
13 12 neeq1d 
 |-  ( A e. NN -> ( ( mmu ` A ) =/= 0 <-> if ( E. p e. Prime ( p ^ 2 ) || A , 0 , ( -u 1 ^ ( # ` { p e. Prime | p || A } ) ) ) =/= 0 ) )
14 11 13 sylibrd 
 |-  ( A e. NN -> ( -. E. p e. Prime ( p ^ 2 ) || A -> ( mmu ` A ) =/= 0 ) )
15 14 necon4bd 
 |-  ( A e. NN -> ( ( mmu ` A ) = 0 -> E. p e. Prime ( p ^ 2 ) || A ) )
16 iftrue 
 |-  ( E. p e. Prime ( p ^ 2 ) || A -> if ( E. p e. Prime ( p ^ 2 ) || A , 0 , ( -u 1 ^ ( # ` { p e. Prime | p || A } ) ) ) = 0 )
17 12 eqeq1d 
 |-  ( A e. NN -> ( ( mmu ` A ) = 0 <-> if ( E. p e. Prime ( p ^ 2 ) || A , 0 , ( -u 1 ^ ( # ` { p e. Prime | p || A } ) ) ) = 0 ) )
18 16 17 imbitrrid 
 |-  ( A e. NN -> ( E. p e. Prime ( p ^ 2 ) || A -> ( mmu ` A ) = 0 ) )
19 15 18 impbid 
 |-  ( A e. NN -> ( ( mmu ` A ) = 0 <-> E. p e. Prime ( p ^ 2 ) || A ) )