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

Metamath Proof Explorer

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