This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dvdssqf

Description: A divisor of a squarefree number is squarefree. (Contributed by Mario Carneiro, 1-Jul-2015)

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

Proof

Step Hyp Ref Expression
1 simpl3 
 |-  ( ( ( A e. NN /\ B e. NN /\ B || A ) /\ p e. Prime ) -> B || A )
2 prmz 
 |-  ( p e. Prime -> p e. ZZ )
3 2 adantl 
 |-  ( ( ( A e. NN /\ B e. NN /\ B || A ) /\ p e. Prime ) -> p e. ZZ )
4 zsqcl 
 |-  ( p e. ZZ -> ( p ^ 2 ) e. ZZ )
5 3 4 syl 
 |-  ( ( ( A e. NN /\ B e. NN /\ B || A ) /\ p e. Prime ) -> ( p ^ 2 ) e. ZZ )
6 simpl2 
 |-  ( ( ( A e. NN /\ B e. NN /\ B || A ) /\ p e. Prime ) -> B e. NN )
7 6 nnzd 
 |-  ( ( ( A e. NN /\ B e. NN /\ B || A ) /\ p e. Prime ) -> B e. ZZ )
8 simpl1 
 |-  ( ( ( A e. NN /\ B e. NN /\ B || A ) /\ p e. Prime ) -> A e. NN )
9 8 nnzd 
 |-  ( ( ( A e. NN /\ B e. NN /\ B || A ) /\ p e. Prime ) -> A e. ZZ )
10 dvdstr 
 |-  ( ( ( p ^ 2 ) e. ZZ /\ B e. ZZ /\ A e. ZZ ) -> ( ( ( p ^ 2 ) || B /\ B || A ) -> ( p ^ 2 ) || A ) )
11 5 7 9 10 syl3anc 
 |-  ( ( ( A e. NN /\ B e. NN /\ B || A ) /\ p e. Prime ) -> ( ( ( p ^ 2 ) || B /\ B || A ) -> ( p ^ 2 ) || A ) )
12 1 11 mpan2d 
 |-  ( ( ( A e. NN /\ B e. NN /\ B || A ) /\ p e. Prime ) -> ( ( p ^ 2 ) || B -> ( p ^ 2 ) || A ) )
13 12 reximdva 
 |-  ( ( A e. NN /\ B e. NN /\ B || A ) -> ( E. p e. Prime ( p ^ 2 ) || B -> E. p e. Prime ( p ^ 2 ) || A ) )
14 isnsqf 
 |-  ( B e. NN -> ( ( mmu ` B ) = 0 <-> E. p e. Prime ( p ^ 2 ) || B ) )
15 14 3ad2ant2 
 |-  ( ( A e. NN /\ B e. NN /\ B || A ) -> ( ( mmu ` B ) = 0 <-> E. p e. Prime ( p ^ 2 ) || B ) )
16 isnsqf 
 |-  ( A e. NN -> ( ( mmu ` A ) = 0 <-> E. p e. Prime ( p ^ 2 ) || A ) )
17 16 3ad2ant1 
 |-  ( ( A e. NN /\ B e. NN /\ B || A ) -> ( ( mmu ` A ) = 0 <-> E. p e. Prime ( p ^ 2 ) || A ) )
18 13 15 17 3imtr4d 
 |-  ( ( A e. NN /\ B e. NN /\ B || A ) -> ( ( mmu ` B ) = 0 -> ( mmu ` A ) = 0 ) )
19 18 necon3d 
 |-  ( ( A e. NN /\ B e. NN /\ B || A ) -> ( ( mmu ` A ) =/= 0 -> ( mmu ` B ) =/= 0 ) )