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∈ℤ|∀n∈MNz∥n
gcdcllem2.2 ⊢R=z∈ℤ|z∥M∧z∥N
Assertion gcdcllem2 ⊢M∈ℤ∧N∈ℤ→R=S

Proof

Step Hyp Ref Expression
1 gcdcllem2.1 ⊢S=z∈ℤ|∀n∈MNz∥n
2 gcdcllem2.2 ⊢R=z∈ℤ|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∈R↔x∈ℤ∧x∥M∧x∥N
7 breq1 ⊢z=x→z∥n↔x∥n
8 7 ralbidv ⊢z=x→∀n∈MNz∥n↔∀n∈MNx∥n
9 8 1 elrab2 ⊢x∈S↔x∈ℤ∧∀n∈MNx∥n
10 breq2 ⊢n=M→x∥n↔x∥M
11 breq2 ⊢n=N→x∥n↔x∥N
12 10 11 ralprg ⊢M∈ℤ∧N∈ℤ→∀n∈MNx∥n↔x∥M∧x∥N
13 12 anbi2d ⊢M∈ℤ∧N∈ℤ→x∈ℤ∧∀n∈MNx∥n↔x∈ℤ∧x∥M∧x∥N
14 9 13 bitrid ⊢M∈ℤ∧N∈ℤ→x∈S↔x∈ℤ∧x∥M∧x∥N
15 6 14 bitr4id ⊢M∈ℤ∧N∈ℤ→x∈R↔x∈S
16 15 eqrdv ⊢M∈ℤ∧N∈ℤ→R=S