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