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 ∥ n ↔ x ∥ n
4 3 ralbidv ⊢ z = x → ∀ n ∈ M N z ∥ n ↔ ∀ n ∈ M N x ∥ n
5 4 1 elrab2 ⊢ x ∈ S ↔ x ∈ ℤ ∧ ∀ n ∈ M N x ∥ n
6 breq2 ⊢ n = M → x ∥ n ↔ x ∥ M
7 breq2 ⊢ n = N → x ∥ n ↔ x ∥ N
8 6 7 ralprg ⊢ M ∈ ℤ ∧ N ∈ ℤ → ∀ n ∈ M N x ∥ n ↔ x ∥ M ∧ x ∥ N
9 8 anbi2d ⊢ M ∈ ℤ ∧ N ∈ ℤ → x ∈ ℤ ∧ ∀ n ∈ M N x ∥ n ↔ x ∈ ℤ ∧ x ∥ M ∧ x ∥ N
10 5 9 syl5bb ⊢ M ∈ ℤ ∧ N ∈ ℤ → x ∈ S ↔ x ∈ ℤ ∧ x ∥ M ∧ x ∥ N
11 breq1 ⊢ z = x → z ∥ M ↔ x ∥ M
12 breq1 ⊢ z = x → z ∥ N ↔ x ∥ N
13 11 12 anbi12d ⊢ z = x → z ∥ M ∧ z ∥ N ↔ x ∥ M ∧ x ∥ N
14 13 2 elrab2 ⊢ x ∈ R ↔ x ∈ ℤ ∧ x ∥ M ∧ x ∥ N
15 10 14 syl6rbbr ⊢ M ∈ ℤ ∧ N ∈ ℤ → x ∈ R ↔ x ∈ S
16 15 eqrdv ⊢ M ∈ ℤ ∧ N ∈ ℤ → R = S