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