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

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 ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 gcd 𝑁 ) = if ( ( 𝑀 = 0 ∧ 𝑁 = 0 ) , 0 , sup ( { 𝑛 ∈ ℤ ∣ ( 𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁 ) } , ℝ , < ) ) )

Proof

Step Hyp Ref Expression
1 eqeq1 ⊢ ( 𝑥 = 𝑀 → ( 𝑥 = 0 ↔ 𝑀 = 0 ) )
2 1 anbi1d ⊢ ( 𝑥 = 𝑀 → ( ( 𝑥 = 0 ∧ 𝑦 = 0 ) ↔ ( 𝑀 = 0 ∧ 𝑦 = 0 ) ) )
3 breq2 ⊢ ( 𝑥 = 𝑀 → ( 𝑛 ∥ 𝑥 ↔ 𝑛 ∥ 𝑀 ) )
4 3 anbi1d ⊢ ( 𝑥 = 𝑀 → ( ( 𝑛 ∥ 𝑥 ∧ 𝑛 ∥ 𝑦 ) ↔ ( 𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑦 ) ) )
5 4 rabbidv ⊢ ( 𝑥 = 𝑀 → { 𝑛 ∈ ℤ ∣ ( 𝑛 ∥ 𝑥 ∧ 𝑛 ∥ 𝑦 ) } = { 𝑛 ∈ ℤ ∣ ( 𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑦 ) } )
6 5 supeq1d ⊢ ( 𝑥 = 𝑀 → sup ( { 𝑛 ∈ ℤ ∣ ( 𝑛 ∥ 𝑥 ∧ 𝑛 ∥ 𝑦 ) } , ℝ , < ) = sup ( { 𝑛 ∈ ℤ ∣ ( 𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑦 ) } , ℝ , < ) )
7 2 6 ifbieq2d ⊢ ( 𝑥 = 𝑀 → if ( ( 𝑥 = 0 ∧ 𝑦 = 0 ) , 0 , sup ( { 𝑛 ∈ ℤ ∣ ( 𝑛 ∥ 𝑥 ∧ 𝑛 ∥ 𝑦 ) } , ℝ , < ) ) = if ( ( 𝑀 = 0 ∧ 𝑦 = 0 ) , 0 , sup ( { 𝑛 ∈ ℤ ∣ ( 𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑦 ) } , ℝ , < ) ) )
8 eqeq1 ⊢ ( 𝑦 = 𝑁 → ( 𝑦 = 0 ↔ 𝑁 = 0 ) )
9 8 anbi2d ⊢ ( 𝑦 = 𝑁 → ( ( 𝑀 = 0 ∧ 𝑦 = 0 ) ↔ ( 𝑀 = 0 ∧ 𝑁 = 0 ) ) )
10 breq2 ⊢ ( 𝑦 = 𝑁 → ( 𝑛 ∥ 𝑦 ↔ 𝑛 ∥ 𝑁 ) )
11 10 anbi2d ⊢ ( 𝑦 = 𝑁 → ( ( 𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑦 ) ↔ ( 𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁 ) ) )
12 11 rabbidv ⊢ ( 𝑦 = 𝑁 → { 𝑛 ∈ ℤ ∣ ( 𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑦 ) } = { 𝑛 ∈ ℤ ∣ ( 𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁 ) } )
13 12 supeq1d ⊢ ( 𝑦 = 𝑁 → sup ( { 𝑛 ∈ ℤ ∣ ( 𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑦 ) } , ℝ , < ) = sup ( { 𝑛 ∈ ℤ ∣ ( 𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁 ) } , ℝ , < ) )
14 9 13 ifbieq2d ⊢ ( 𝑦 = 𝑁 → if ( ( 𝑀 = 0 ∧ 𝑦 = 0 ) , 0 , sup ( { 𝑛 ∈ ℤ ∣ ( 𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑦 ) } , ℝ , < ) ) = if ( ( 𝑀 = 0 ∧ 𝑁 = 0 ) , 0 , sup ( { 𝑛 ∈ ℤ ∣ ( 𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁 ) } , ℝ , < ) ) )
15 df-gcd ⊢ gcd = ( 𝑥 ∈ ℤ , 𝑦 ∈ ℤ ↦ if ( ( 𝑥 = 0 ∧ 𝑦 = 0 ) , 0 , sup ( { 𝑛 ∈ ℤ ∣ ( 𝑛 ∥ 𝑥 ∧ 𝑛 ∥ 𝑦 ) } , ℝ , < ) ) )
16 c0ex ⊢ 0 ∈ V
17 ltso ⊢ < Or ℝ
18 17 supex ⊢ sup ( { 𝑛 ∈ ℤ ∣ ( 𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁 ) } , ℝ , < ) ∈ V
19 16 18 ifex ⊢ if ( ( 𝑀 = 0 ∧ 𝑁 = 0 ) , 0 , sup ( { 𝑛 ∈ ℤ ∣ ( 𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁 ) } , ℝ , < ) ) ∈ V
20 7 14 15 19 ovmpo ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 gcd 𝑁 ) = if ( ( 𝑀 = 0 ∧ 𝑁 = 0 ) , 0 , sup ( { 𝑛 ∈ ℤ ∣ ( 𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁 ) } , ℝ , < ) ) )