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