Metamath Proof Explorer

Theorem dvds0lem

Description: A lemma to assist theorems of || with no antecedents. (Contributed by Paul Chapman, 21-Mar-2011)

Ref Expression
Assertion dvds0lem 
|- ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( K x. M ) = N ) -> M || N )

Proof

Step Hyp Ref Expression
1 oveq1 
 |-  ( x = K -> ( x x. M ) = ( K x. M ) )
2 1 eqeq1d 
 |-  ( x = K -> ( ( x x. M ) = N <-> ( K x. M ) = N ) )
3 2 rspcev 
 |-  ( ( K e. ZZ /\ ( K x. M ) = N ) -> E. x e. ZZ ( x x. M ) = N )
4 3 adantl 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( K e. ZZ /\ ( K x. M ) = N ) ) -> E. x e. ZZ ( x x. M ) = N )
5 divides 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M || N <-> E. x e. ZZ ( x x. M ) = N ) )
6 5 adantr 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( K e. ZZ /\ ( K x. M ) = N ) ) -> ( M || N <-> E. x e. ZZ ( x x. M ) = N ) )
7 4 6 mpbird 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( K e. ZZ /\ ( K x. M ) = N ) ) -> M || N )
8 7 expr 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ K e. ZZ ) -> ( ( K x. M ) = N -> M || N ) )
9 8 3impa 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ K e. ZZ ) -> ( ( K x. M ) = N -> M || N ) )
10 9 3comr 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( K x. M ) = N -> M || N ) )
11 10 imp 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( K x. M ) = N ) -> M || N )