Theorem gcdcllem2

Description: Lemma for gcdn0cl , gcddvds and dvdslegcd . (Contributed by Paul Chapman, 21-Mar-2011)

	Ref	Expression
Hypotheses	gcdcllem2.1	|- S = { z e. ZZ | A. n e. { M , N } z || n }
	gcdcllem2.2	|- R = { z e. ZZ | ( z || M /\ z || N ) }
Assertion	gcdcllem2	|- ( ( M e. ZZ /\ N e. ZZ ) -> R = S )

Proof

Step	Hyp	Ref	Expression
1		gcdcllem2.1	|- S = { z e. ZZ | A. n e. { M , N } z || n }
2		gcdcllem2.2	|- R = { z e. ZZ | ( z || M /\ z || N ) }
3		breq1	|- ( z = x -> ( z || M <-> x || M ) )
4		breq1	|- ( z = x -> ( z || N <-> x || N ) )
5	3 4	anbi12d	|- ( z = x -> ( ( z || M /\ z || N ) <-> ( x || M /\ x || N ) ) )
6	5 2	elrab2	|- ( x e. R <-> ( x e. ZZ /\ ( x || M /\ x || N ) ) )
7		breq1	|- ( z = x -> ( z || n <-> x || n ) )
8	7	ralbidv	|- ( z = x -> ( A. n e. { M , N } z || n <-> A. n e. { M , N } x || n ) )
9	8 1	elrab2	|- ( x e. S <-> ( x e. ZZ /\ A. n e. { M , N } x || n ) )
10		breq2	|- ( n = M -> ( x || n <-> x || M ) )
11		breq2	|- ( n = N -> ( x || n <-> x || N ) )
12	10 11	ralprg	|- ( ( M e. ZZ /\ N e. ZZ ) -> ( A. n e. { M , N } x || n <-> ( x || M /\ x || N ) ) )
13	12	anbi2d	|- ( ( M e. ZZ /\ N e. ZZ ) -> ( ( x e. ZZ /\ A. n e. { M , N } x || n ) <-> ( x e. ZZ /\ ( x || M /\ x || N ) ) ) )
14	9 13	syl5bb	|- ( ( M e. ZZ /\ N e. ZZ ) -> ( x e. S <-> ( x e. ZZ /\ ( x || M /\ x || N ) ) ) )
15	6 14	bitr4id	|- ( ( M e. ZZ /\ N e. ZZ ) -> ( x e. R <-> x e. S ) )
16	15	eqrdv	|- ( ( M e. ZZ /\ N e. ZZ ) -> R = S )