This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem gcdcom

Description: The gcd operator is commutative. Theorem 1.4(a) in ApostolNT p. 16. (Contributed by Paul Chapman, 21-Mar-2011)

Ref Expression
Assertion gcdcom ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 gcd 𝑁 ) = ( 𝑁 gcd 𝑀 ) )

Proof

Step Hyp Ref Expression
1 ancom ⊢ ( ( 𝑀 = 0 ∧ 𝑁 = 0 ) ↔ ( 𝑁 = 0 ∧ 𝑀 = 0 ) )
2 ancom ⊢ ( ( 𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁 ) ↔ ( 𝑛 ∥ 𝑁 ∧ 𝑛 ∥ 𝑀 ) )
3 2 rabbii ⊢ { 𝑛 ∈ ℤ ∣ ( 𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁 ) } = { 𝑛 ∈ ℤ ∣ ( 𝑛 ∥ 𝑁 ∧ 𝑛 ∥ 𝑀 ) }
4 3 supeq1i ⊢ sup ( { 𝑛 ∈ ℤ ∣ ( 𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁 ) } , ℝ , < ) = sup ( { 𝑛 ∈ ℤ ∣ ( 𝑛 ∥ 𝑁 ∧ 𝑛 ∥ 𝑀 ) } , ℝ , < )
5 1 4 ifbieq2i ⊢ if ( ( 𝑀 = 0 ∧ 𝑁 = 0 ) , 0 , sup ( { 𝑛 ∈ ℤ ∣ ( 𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁 ) } , ℝ , < ) ) = if ( ( 𝑁 = 0 ∧ 𝑀 = 0 ) , 0 , sup ( { 𝑛 ∈ ℤ ∣ ( 𝑛 ∥ 𝑁 ∧ 𝑛 ∥ 𝑀 ) } , ℝ , < ) )
6 gcdval ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 gcd 𝑁 ) = if ( ( 𝑀 = 0 ∧ 𝑁 = 0 ) , 0 , sup ( { 𝑛 ∈ ℤ ∣ ( 𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁 ) } , ℝ , < ) ) )
7 gcdval ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝑁 gcd 𝑀 ) = if ( ( 𝑁 = 0 ∧ 𝑀 = 0 ) , 0 , sup ( { 𝑛 ∈ ℤ ∣ ( 𝑛 ∥ 𝑁 ∧ 𝑛 ∥ 𝑀 ) } , ℝ , < ) ) )
8 7 ancoms ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑁 gcd 𝑀 ) = if ( ( 𝑁 = 0 ∧ 𝑀 = 0 ) , 0 , sup ( { 𝑛 ∈ ℤ ∣ ( 𝑛 ∥ 𝑁 ∧ 𝑛 ∥ 𝑀 ) } , ℝ , < ) ) )
9 5 6 8 3eqtr4a ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 gcd 𝑁 ) = ( 𝑁 gcd 𝑀 ) )