Metamath Proof Explorer

Theorem gcdabsOLD

Description: Obsolete version of gcdabs as of 15-Sep-2024. (Contributed by Paul Chapman, 31-Mar-2011) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Assertion gcdabsOLD ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( abs ‘ 𝑀 ) gcd ( abs ‘ 𝑁 ) ) = ( 𝑀 gcd 𝑁 ) )

Proof

Step Hyp Ref Expression
1 zre ⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℝ )
2 zre ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ )
3 absor ⊢ ( 𝑀 ∈ ℝ → ( ( abs ‘ 𝑀 ) = 𝑀 ∨ ( abs ‘ 𝑀 ) = - 𝑀 ) )
4 absor ⊢ ( 𝑁 ∈ ℝ → ( ( abs ‘ 𝑁 ) = 𝑁 ∨ ( abs ‘ 𝑁 ) = - 𝑁 ) )
5 3 4 anim12i ⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( ( ( abs ‘ 𝑀 ) = 𝑀 ∨ ( abs ‘ 𝑀 ) = - 𝑀 ) ∧ ( ( abs ‘ 𝑁 ) = 𝑁 ∨ ( abs ‘ 𝑁 ) = - 𝑁 ) ) )
6 1 2 5 syl2an ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( ( abs ‘ 𝑀 ) = 𝑀 ∨ ( abs ‘ 𝑀 ) = - 𝑀 ) ∧ ( ( abs ‘ 𝑁 ) = 𝑁 ∨ ( abs ‘ 𝑁 ) = - 𝑁 ) ) )
7 oveq12 ⊢ ( ( ( abs ‘ 𝑀 ) = 𝑀 ∧ ( abs ‘ 𝑁 ) = 𝑁 ) → ( ( abs ‘ 𝑀 ) gcd ( abs ‘ 𝑁 ) ) = ( 𝑀 gcd 𝑁 ) )
8 7 a1i ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( ( abs ‘ 𝑀 ) = 𝑀 ∧ ( abs ‘ 𝑁 ) = 𝑁 ) → ( ( abs ‘ 𝑀 ) gcd ( abs ‘ 𝑁 ) ) = ( 𝑀 gcd 𝑁 ) ) )
9 oveq12 ⊢ ( ( ( abs ‘ 𝑀 ) = - 𝑀 ∧ ( abs ‘ 𝑁 ) = 𝑁 ) → ( ( abs ‘ 𝑀 ) gcd ( abs ‘ 𝑁 ) ) = ( - 𝑀 gcd 𝑁 ) )
10 neggcd ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( - 𝑀 gcd 𝑁 ) = ( 𝑀 gcd 𝑁 ) )
11 9 10 sylan9eqr ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( ( abs ‘ 𝑀 ) = - 𝑀 ∧ ( abs ‘ 𝑁 ) = 𝑁 ) ) → ( ( abs ‘ 𝑀 ) gcd ( abs ‘ 𝑁 ) ) = ( 𝑀 gcd 𝑁 ) )
12 11 ex ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( ( abs ‘ 𝑀 ) = - 𝑀 ∧ ( abs ‘ 𝑁 ) = 𝑁 ) → ( ( abs ‘ 𝑀 ) gcd ( abs ‘ 𝑁 ) ) = ( 𝑀 gcd 𝑁 ) ) )
13 oveq12 ⊢ ( ( ( abs ‘ 𝑀 ) = 𝑀 ∧ ( abs ‘ 𝑁 ) = - 𝑁 ) → ( ( abs ‘ 𝑀 ) gcd ( abs ‘ 𝑁 ) ) = ( 𝑀 gcd - 𝑁 ) )
14 gcdneg ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 gcd - 𝑁 ) = ( 𝑀 gcd 𝑁 ) )
15 13 14 sylan9eqr ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( ( abs ‘ 𝑀 ) = 𝑀 ∧ ( abs ‘ 𝑁 ) = - 𝑁 ) ) → ( ( abs ‘ 𝑀 ) gcd ( abs ‘ 𝑁 ) ) = ( 𝑀 gcd 𝑁 ) )
16 15 ex ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( ( abs ‘ 𝑀 ) = 𝑀 ∧ ( abs ‘ 𝑁 ) = - 𝑁 ) → ( ( abs ‘ 𝑀 ) gcd ( abs ‘ 𝑁 ) ) = ( 𝑀 gcd 𝑁 ) ) )
17 oveq12 ⊢ ( ( ( abs ‘ 𝑀 ) = - 𝑀 ∧ ( abs ‘ 𝑁 ) = - 𝑁 ) → ( ( abs ‘ 𝑀 ) gcd ( abs ‘ 𝑁 ) ) = ( - 𝑀 gcd - 𝑁 ) )
18 znegcl ⊢ ( 𝑀 ∈ ℤ → - 𝑀 ∈ ℤ )
19 gcdneg ⊢ ( ( - 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( - 𝑀 gcd - 𝑁 ) = ( - 𝑀 gcd 𝑁 ) )
20 18 19 sylan ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( - 𝑀 gcd - 𝑁 ) = ( - 𝑀 gcd 𝑁 ) )
21 20 10 eqtrd ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( - 𝑀 gcd - 𝑁 ) = ( 𝑀 gcd 𝑁 ) )
22 17 21 sylan9eqr ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( ( abs ‘ 𝑀 ) = - 𝑀 ∧ ( abs ‘ 𝑁 ) = - 𝑁 ) ) → ( ( abs ‘ 𝑀 ) gcd ( abs ‘ 𝑁 ) ) = ( 𝑀 gcd 𝑁 ) )
23 22 ex ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( ( abs ‘ 𝑀 ) = - 𝑀 ∧ ( abs ‘ 𝑁 ) = - 𝑁 ) → ( ( abs ‘ 𝑀 ) gcd ( abs ‘ 𝑁 ) ) = ( 𝑀 gcd 𝑁 ) ) )
24 8 12 16 23 ccased ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( ( ( abs ‘ 𝑀 ) = 𝑀 ∨ ( abs ‘ 𝑀 ) = - 𝑀 ) ∧ ( ( abs ‘ 𝑁 ) = 𝑁 ∨ ( abs ‘ 𝑁 ) = - 𝑁 ) ) → ( ( abs ‘ 𝑀 ) gcd ( abs ‘ 𝑁 ) ) = ( 𝑀 gcd 𝑁 ) ) )
25 6 24 mpd ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( abs ‘ 𝑀 ) gcd ( abs ‘ 𝑁 ) ) = ( 𝑀 gcd 𝑁 ) )