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	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝑅 = 𝑆 )