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 syl5ibr
 |-  ( 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 ) )