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 ABμA=0μAB=0

Proof

Step Hyp Ref Expression
1 prmz pp
2 1 adantl ABpp
3 zsqcl pp2
4 2 3 syl ABpp2
5 nnz AA
6 5 ad2antrr ABpA
7 nnz BB
8 7 ad2antlr ABpB
9 dvdsmultr1 p2ABp2Ap2AB
10 4 6 8 9 syl3anc ABpp2Ap2AB
11 10 reximdva ABpp2App2AB
12 isnsqf AμA=0pp2A
13 12 adantr ABμA=0pp2A
14 nnmulcl ABAB
15 isnsqf ABμAB=0pp2AB
16 14 15 syl ABμAB=0pp2AB
17 11 13 16 3imtr4d ABμA=0μAB=0
18 17 imp ABμA=0μAB=0