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

Metamath Proof Explorer

Theorem dvds2lem

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

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

Proof

Step Hyp Ref Expression
1 dvds2lem.1 
 |-  ( ph -> ( I e. ZZ /\ J e. ZZ ) )
2 dvds2lem.2 
 |-  ( ph -> ( K e. ZZ /\ L e. ZZ ) )
3 dvds2lem.3 
 |-  ( ph -> ( M e. ZZ /\ N e. ZZ ) )
4 dvds2lem.4 
 |-  ( ( ph /\ ( x e. ZZ /\ y e. ZZ ) ) -> Z e. ZZ )
5 dvds2lem.5 
 |-  ( ( ph /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( ( ( x x. I ) = J /\ ( y x. K ) = L ) -> ( Z x. M ) = N ) )
6 divides 
 |-  ( ( I e. ZZ /\ J e. ZZ ) -> ( I || J <-> E. x e. ZZ ( x x. I ) = J ) )
7 divides 
 |-  ( ( K e. ZZ /\ L e. ZZ ) -> ( K || L <-> E. y e. ZZ ( y x. K ) = L ) )
8 6 7 bi2anan9 
 |-  ( ( ( I e. ZZ /\ J e. ZZ ) /\ ( K e. ZZ /\ L e. ZZ ) ) -> ( ( I || J /\ K || L ) <-> ( E. x e. ZZ ( x x. I ) = J /\ E. y e. ZZ ( y x. K ) = L ) ) )
9 1 2 8 syl2anc 
 |-  ( ph -> ( ( I || J /\ K || L ) <-> ( E. x e. ZZ ( x x. I ) = J /\ E. y e. ZZ ( y x. K ) = L ) ) )
10 9 biimpd 
 |-  ( ph -> ( ( I || J /\ K || L ) -> ( E. x e. ZZ ( x x. I ) = J /\ E. y e. ZZ ( y x. K ) = L ) ) )
11 reeanv 
 |-  ( E. x e. ZZ E. y e. ZZ ( ( x x. I ) = J /\ ( y x. K ) = L ) <-> ( E. x e. ZZ ( x x. I ) = J /\ E. y e. ZZ ( y x. K ) = L ) )
12 10 11 imbitrrdi 
 |-  ( ph -> ( ( I || J /\ K || L ) -> E. x e. ZZ E. y e. ZZ ( ( x x. I ) = J /\ ( y x. K ) = L ) ) )
13 oveq1 
 |-  ( z = Z -> ( z x. M ) = ( Z x. M ) )
14 13 eqeq1d 
 |-  ( z = Z -> ( ( z x. M ) = N <-> ( Z x. M ) = N ) )
15 14 rspcev 
 |-  ( ( Z e. ZZ /\ ( Z x. M ) = N ) -> E. z e. ZZ ( z x. M ) = N )
16 4 5 15 syl6an 
 |-  ( ( ph /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( ( ( x x. I ) = J /\ ( y x. K ) = L ) -> E. z e. ZZ ( z x. M ) = N ) )
17 16 rexlimdvva 
 |-  ( ph -> ( E. x e. ZZ E. y e. ZZ ( ( x x. I ) = J /\ ( y x. K ) = L ) -> E. z e. ZZ ( z x. M ) = N ) )
18 12 17 syld 
 |-  ( ph -> ( ( I || J /\ K || L ) -> E. z e. ZZ ( z x. M ) = N ) )
19 divides 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M || N <-> E. z e. ZZ ( z x. M ) = N ) )
20 3 19 syl 
 |-  ( ph -> ( M || N <-> E. z e. ZZ ( z x. M ) = N ) )
21 18 20 sylibrd 
 |-  ( ph -> ( ( I || J /\ K || L ) -> M || N ) )