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

Metamath Proof Explorer

Theorem dvds1lem

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

Ref Expression
Hypotheses dvds1lem.1 
|- ( ph -> ( J e. ZZ /\ K e. ZZ ) )
dvds1lem.2 
|- ( ph -> ( M e. ZZ /\ N e. ZZ ) )
dvds1lem.3 
|- ( ( ph /\ x e. ZZ ) -> Z e. ZZ )
dvds1lem.4 
|- ( ( ph /\ x e. ZZ ) -> ( ( x x. J ) = K -> ( Z x. M ) = N ) )
Assertion dvds1lem 
|- ( ph -> ( J || K -> M || N ) )

Proof

Step Hyp Ref Expression
1 dvds1lem.1 
 |-  ( ph -> ( J e. ZZ /\ K e. ZZ ) )
2 dvds1lem.2 
 |-  ( ph -> ( M e. ZZ /\ N e. ZZ ) )
3 dvds1lem.3 
 |-  ( ( ph /\ x e. ZZ ) -> Z e. ZZ )
4 dvds1lem.4 
 |-  ( ( ph /\ x e. ZZ ) -> ( ( x x. J ) = K -> ( Z x. M ) = N ) )
5 oveq1 
 |-  ( z = Z -> ( z x. M ) = ( Z x. M ) )
6 5 eqeq1d 
 |-  ( z = Z -> ( ( z x. M ) = N <-> ( Z x. M ) = N ) )
7 6 rspcev 
 |-  ( ( Z e. ZZ /\ ( Z x. M ) = N ) -> E. z e. ZZ ( z x. M ) = N )
8 3 4 7 syl6an 
 |-  ( ( ph /\ x e. ZZ ) -> ( ( x x. J ) = K -> E. z e. ZZ ( z x. M ) = N ) )
9 8 rexlimdva 
 |-  ( ph -> ( E. x e. ZZ ( x x. J ) = K -> E. z e. ZZ ( z x. M ) = N ) )
10 divides 
 |-  ( ( J e. ZZ /\ K e. ZZ ) -> ( J || K <-> E. x e. ZZ ( x x. J ) = K ) )
11 1 10 syl 
 |-  ( ph -> ( J || K <-> E. x e. ZZ ( x x. J ) = K ) )
12 divides 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M || N <-> E. z e. ZZ ( z x. M ) = N ) )
13 2 12 syl 
 |-  ( ph -> ( M || N <-> E. z e. ZZ ( z x. M ) = N ) )
14 9 11 13 3imtr4d 
 |-  ( ph -> ( J || K -> M || N ) )