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 𝑀 ) ) |