Metamath Proof Explorer

Theorem gcdval

Description: The value of the gcd operator. ( M gcd N ) is the greatest common divisor of M and N . If M and N are both 0 , the result is defined conventionally as 0 . (Contributed by Paul Chapman, 21-Mar-2011) (Revised by Mario Carneiro, 10-Nov-2013)

Ref Expression
Assertion gcdval ⊢ M ∈ ℤ ∧ N ∈ ℤ → M gcd N = if M = 0 ∧ N = 0 0 sup n ∈ ℤ | n ∥ M ∧ n ∥ N ℝ <

Proof

Step Hyp Ref Expression
1 eqeq1 ⊢ x = M → x = 0 ↔ M = 0
2 1 anbi1d ⊢ x = M → x = 0 ∧ y = 0 ↔ M = 0 ∧ y = 0
3 breq2 ⊢ x = M → n ∥ x ↔ n ∥ M
4 3 anbi1d ⊢ x = M → n ∥ x ∧ n ∥ y ↔ n ∥ M ∧ n ∥ y
5 4 rabbidv ⊢ x = M → n ∈ ℤ | n ∥ x ∧ n ∥ y = n ∈ ℤ | n ∥ M ∧ n ∥ y
6 5 supeq1d ⊢ x = M → sup n ∈ ℤ | n ∥ x ∧ n ∥ y ℝ < = sup n ∈ ℤ | n ∥ M ∧ n ∥ y ℝ <
7 2 6 ifbieq2d ⊢ x = M → if x = 0 ∧ y = 0 0 sup n ∈ ℤ | n ∥ x ∧ n ∥ y ℝ < = if M = 0 ∧ y = 0 0 sup n ∈ ℤ | n ∥ M ∧ n ∥ y ℝ <
8 eqeq1 ⊢ y = N → y = 0 ↔ N = 0
9 8 anbi2d ⊢ y = N → M = 0 ∧ y = 0 ↔ M = 0 ∧ N = 0
10 breq2 ⊢ y = N → n ∥ y ↔ n ∥ N
11 10 anbi2d ⊢ y = N → n ∥ M ∧ n ∥ y ↔ n ∥ M ∧ n ∥ N
12 11 rabbidv ⊢ y = N → n ∈ ℤ | n ∥ M ∧ n ∥ y = n ∈ ℤ | n ∥ M ∧ n ∥ N
13 12 supeq1d ⊢ y = N → sup n ∈ ℤ | n ∥ M ∧ n ∥ y ℝ < = sup n ∈ ℤ | n ∥ M ∧ n ∥ N ℝ <
14 9 13 ifbieq2d ⊢ y = N → if M = 0 ∧ y = 0 0 sup n ∈ ℤ | n ∥ M ∧ n ∥ y ℝ < = if M = 0 ∧ N = 0 0 sup n ∈ ℤ | n ∥ M ∧ n ∥ N ℝ <
15 df-gcd ⊢ gcd = x ∈ ℤ , y ∈ ℤ ⟼ if x = 0 ∧ y = 0 0 sup n ∈ ℤ | n ∥ x ∧ n ∥ y ℝ <
16 c0ex ⊢ 0 ∈ V
17 ltso ⊢ < Or ℝ
18 17 supex ⊢ sup n ∈ ℤ | n ∥ M ∧ n ∥ N ℝ < ∈ V
19 16 18 ifex ⊢ if M = 0 ∧ N = 0 0 sup n ∈ ℤ | n ∥ M ∧ n ∥ N ℝ < ∈ V
20 7 14 15 19 ovmpo ⊢ M ∈ ℤ ∧ N ∈ ℤ → M gcd N = if M = 0 ∧ N = 0 0 sup n ∈ ℤ | n ∥ M ∧ n ∥ N ℝ <