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 M N M gcd N = M gcd N

Proof

Step Hyp Ref Expression
1 zre M M
2 zre N N
3 absor M M = M M = M
4 absor N N = N N = N
5 3 4 anim12i M N M = M M = M N = N N = N
6 1 2 5 syl2an M N M = M M = M N = N N = N
7 oveq12 M = M N = N M gcd N = M gcd N
8 7 a1i M N M = M N = N M gcd N = M gcd N
9 oveq12 M = M N = N M gcd N = -M gcd N
10 neggcd M N -M gcd N = M gcd N
11 9 10 sylan9eqr M N M = M N = N M gcd N = M gcd N
12 11 ex M N M = M N = N M gcd N = M gcd N
13 oveq12 M = M N = N M gcd N = M gcd -N
14 gcdneg M N M gcd -N = M gcd N
15 13 14 sylan9eqr M N M = M N = N M gcd N = M gcd N
16 15 ex M N M = M N = N M gcd N = M gcd N
17 oveq12 M = M N = N M gcd N = -M gcd -N
18 znegcl M M
19 gcdneg M N -M gcd -N = -M gcd N
20 18 19 sylan M N -M gcd -N = -M gcd N
21 20 10 eqtrd M N -M gcd -N = M gcd N
22 17 21 sylan9eqr M N M = M N = N M gcd N = M gcd N
23 22 ex M N M = M N = N M gcd N = M gcd N
24 8 12 16 23 ccased M N M = M M = M N = N N = N M gcd N = M gcd N
25 6 24 mpd M N M gcd N = M gcd N