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

Metamath Proof Explorer

Definition df-gcd

Description: Define the gcd operator. For example, ( -u 6 gcd 9 ) = 3 ( ex-gcd ). For an alternate definition, based on the definition in ApostolNT p. 15, see dfgcd2 . (Contributed by Paul Chapman, 21-Mar-2011)

Ref Expression
Assertion df-gcd gcd = ( 𝑥 ∈ ℤ , 𝑦 ∈ ℤ ↦ if ( ( 𝑥 = 0 ∧ 𝑦 = 0 ) , 0 , sup ( { 𝑛 ∈ ℤ ∣ ( 𝑛 ∥ 𝑥 ∧ 𝑛 ∥ 𝑦 ) } , ℝ , < ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cgcd ⊢ gcd
1 vx ⊢ 𝑥
2 cz ⊢ ℤ
3 vy ⊢ 𝑦
4 1 cv ⊢ 𝑥
5 cc0 ⊢ 0
6 4 5 wceq ⊢ 𝑥 = 0
7 3 cv ⊢ 𝑦
8 7 5 wceq ⊢ 𝑦 = 0
9 6 8 wa ⊢ ( 𝑥 = 0 ∧ 𝑦 = 0 )
10 vn ⊢ 𝑛
11 10 cv ⊢ 𝑛
12 cdvds ⊢ ∥
13 11 4 12 wbr ⊢ 𝑛 ∥ 𝑥
14 11 7 12 wbr ⊢ 𝑛 ∥ 𝑦
15 13 14 wa ⊢ ( 𝑛 ∥ 𝑥 ∧ 𝑛 ∥ 𝑦 )
16 15 10 2 crab ⊢ { 𝑛 ∈ ℤ ∣ ( 𝑛 ∥ 𝑥 ∧ 𝑛 ∥ 𝑦 ) }
17 cr ⊢ ℝ
18 clt ⊢ <
19 16 17 18 csup ⊢ sup ( { 𝑛 ∈ ℤ ∣ ( 𝑛 ∥ 𝑥 ∧ 𝑛 ∥ 𝑦 ) } , ℝ , < )
20 9 5 19 cif ⊢ if ( ( 𝑥 = 0 ∧ 𝑦 = 0 ) , 0 , sup ( { 𝑛 ∈ ℤ ∣ ( 𝑛 ∥ 𝑥 ∧ 𝑛 ∥ 𝑦 ) } , ℝ , < ) )
21 1 3 2 2 20 cmpo ⊢ ( 𝑥 ∈ ℤ , 𝑦 ∈ ℤ ↦ if ( ( 𝑥 = 0 ∧ 𝑦 = 0 ) , 0 , sup ( { 𝑛 ∈ ℤ ∣ ( 𝑛 ∥ 𝑥 ∧ 𝑛 ∥ 𝑦 ) } , ℝ , < ) ) )
22 0 21 wceq ⊢ gcd = ( 𝑥 ∈ ℤ , 𝑦 ∈ ℤ ↦ if ( ( 𝑥 = 0 ∧ 𝑦 = 0 ) , 0 , sup ( { 𝑛 ∈ ℤ ∣ ( 𝑛 ∥ 𝑥 ∧ 𝑛 ∥ 𝑦 ) } , ℝ , < ) ) )