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 ∈ M N z ∥ 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 ∈ M N z ∥ 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 ∈ M N z ∥ n ↔ ∀ n ∈ M N x ∥ n
9 8 1 elrab2 ⊢ x ∈ S ↔ x ∈ ℤ ∧ ∀ n ∈ 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 ∈ ℤ ∧ N ∈ ℤ → ∀ n ∈ M N x ∥ n ↔ x ∥ M ∧ x ∥ N
13 12 anbi2d ⊢ M ∈ ℤ ∧ N ∈ ℤ → x ∈ ℤ ∧ ∀ n ∈ M N x ∥ n ↔ x ∈ ℤ ∧ x ∥ M ∧ x ∥ N
14 9 13 syl5bb ⊢ 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