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 ⊢ 𝑆 = { 𝑧 ∈ ℤ ∣ ∀ 𝑛 ∈ { 𝑀 , 𝑁 } 𝑧 ∥ 𝑛 }
gcdcllem2.2 ⊢ 𝑅 = { 𝑧 ∈ ℤ ∣ ( 𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁 ) }
Assertion gcdcllem2 ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝑅 = 𝑆 )

Proof

Step Hyp Ref Expression
1 gcdcllem2.1 ⊢ 𝑆 = { 𝑧 ∈ ℤ ∣ ∀ 𝑛 ∈ { 𝑀 , 𝑁 } 𝑧 ∥ 𝑛 }
2 gcdcllem2.2 ⊢ 𝑅 = { 𝑧 ∈ ℤ ∣ ( 𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁 ) }
3 breq1 ⊢ ( 𝑧 = 𝑥 → ( 𝑧 ∥ 𝑀 ↔ 𝑥 ∥ 𝑀 ) )
4 breq1 ⊢ ( 𝑧 = 𝑥 → ( 𝑧 ∥ 𝑁 ↔ 𝑥 ∥ 𝑁 ) )
5 3 4 anbi12d ⊢ ( 𝑧 = 𝑥 → ( ( 𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁 ) ↔ ( 𝑥 ∥ 𝑀 ∧ 𝑥 ∥ 𝑁 ) ) )
6 5 2 elrab2 ⊢ ( 𝑥 ∈ 𝑅 ↔ ( 𝑥 ∈ ℤ ∧ ( 𝑥 ∥ 𝑀 ∧ 𝑥 ∥ 𝑁 ) ) )
7 breq1 ⊢ ( 𝑧 = 𝑥 → ( 𝑧 ∥ 𝑛 ↔ 𝑥 ∥ 𝑛 ) )
8 7 ralbidv ⊢ ( 𝑧 = 𝑥 → ( ∀ 𝑛 ∈ { 𝑀 , 𝑁 } 𝑧 ∥ 𝑛 ↔ ∀ 𝑛 ∈ { 𝑀 , 𝑁 } 𝑥 ∥ 𝑛 ) )
9 8 1 elrab2 ⊢ ( 𝑥 ∈ 𝑆 ↔ ( 𝑥 ∈ ℤ ∧ ∀ 𝑛 ∈ { 𝑀 , 𝑁 } 𝑥 ∥ 𝑛 ) )
10 breq2 ⊢ ( 𝑛 = 𝑀 → ( 𝑥 ∥ 𝑛 ↔ 𝑥 ∥ 𝑀 ) )
11 breq2 ⊢ ( 𝑛 = 𝑁 → ( 𝑥 ∥ 𝑛 ↔ 𝑥 ∥ 𝑁 ) )
12 10 11 ralprg ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ∀ 𝑛 ∈ { 𝑀 , 𝑁 } 𝑥 ∥ 𝑛 ↔ ( 𝑥 ∥ 𝑀 ∧ 𝑥 ∥ 𝑁 ) ) )
13 12 anbi2d ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑥 ∈ ℤ ∧ ∀ 𝑛 ∈ { 𝑀 , 𝑁 } 𝑥 ∥ 𝑛 ) ↔ ( 𝑥 ∈ ℤ ∧ ( 𝑥 ∥ 𝑀 ∧ 𝑥 ∥ 𝑁 ) ) ) )
14 9 13 bitrid ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑥 ∈ 𝑆 ↔ ( 𝑥 ∈ ℤ ∧ ( 𝑥 ∥ 𝑀 ∧ 𝑥 ∥ 𝑁 ) ) ) )
15 6 14 bitr4id ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑥 ∈ 𝑅 ↔ 𝑥 ∈ 𝑆 ) )
16 15 eqrdv ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝑅 = 𝑆 )