Metamath Proof Explorer

Theorem mumullem1

Description: Lemma for mumul . A multiple of a non-squarefree number is non-squarefree. (Contributed by Mario Carneiro, 3-Oct-2014)

Ref Expression
Assertion mumullem1 
|- ( ( ( A e. NN /\ B e. NN ) /\ ( mmu ` A ) = 0 ) -> ( mmu ` ( A x. B ) ) = 0 )

Proof

Step Hyp Ref Expression
1 prmz 
 |-  ( p e. Prime -> p e. ZZ )
2 1 adantl 
 |-  ( ( ( A e. NN /\ B e. NN ) /\ p e. Prime ) -> p e. ZZ )
3 zsqcl 
 |-  ( p e. ZZ -> ( p ^ 2 ) e. ZZ )
4 2 3 syl 
 |-  ( ( ( A e. NN /\ B e. NN ) /\ p e. Prime ) -> ( p ^ 2 ) e. ZZ )
5 nnz 
 |-  ( A e. NN -> A e. ZZ )
6 5 ad2antrr 
 |-  ( ( ( A e. NN /\ B e. NN ) /\ p e. Prime ) -> A e. ZZ )
7 nnz 
 |-  ( B e. NN -> B e. ZZ )
8 7 ad2antlr 
 |-  ( ( ( A e. NN /\ B e. NN ) /\ p e. Prime ) -> B e. ZZ )
9 dvdsmultr1 
 |-  ( ( ( p ^ 2 ) e. ZZ /\ A e. ZZ /\ B e. ZZ ) -> ( ( p ^ 2 ) || A -> ( p ^ 2 ) || ( A x. B ) ) )
10 4 6 8 9 syl3anc 
 |-  ( ( ( A e. NN /\ B e. NN ) /\ p e. Prime ) -> ( ( p ^ 2 ) || A -> ( p ^ 2 ) || ( A x. B ) ) )
11 10 reximdva 
 |-  ( ( A e. NN /\ B e. NN ) -> ( E. p e. Prime ( p ^ 2 ) || A -> E. p e. Prime ( p ^ 2 ) || ( A x. B ) ) )
12 isnsqf 
 |-  ( A e. NN -> ( ( mmu ` A ) = 0 <-> E. p e. Prime ( p ^ 2 ) || A ) )
13 12 adantr 
 |-  ( ( A e. NN /\ B e. NN ) -> ( ( mmu ` A ) = 0 <-> E. p e. Prime ( p ^ 2 ) || A ) )
14 nnmulcl 
 |-  ( ( A e. NN /\ B e. NN ) -> ( A x. B ) e. NN )
15 isnsqf 
 |-  ( ( A x. B ) e. NN -> ( ( mmu ` ( A x. B ) ) = 0 <-> E. p e. Prime ( p ^ 2 ) || ( A x. B ) ) )
16 14 15 syl 
 |-  ( ( A e. NN /\ B e. NN ) -> ( ( mmu ` ( A x. B ) ) = 0 <-> E. p e. Prime ( p ^ 2 ) || ( A x. B ) ) )
17 11 13 16 3imtr4d 
 |-  ( ( A e. NN /\ B e. NN ) -> ( ( mmu ` A ) = 0 -> ( mmu ` ( A x. B ) ) = 0 ) )
18 17 imp 
 |-  ( ( ( A e. NN /\ B e. NN ) /\ ( mmu ` A ) = 0 ) -> ( mmu ` ( A x. B ) ) = 0 )