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 e. ZZ /\ N e. ZZ ) -> ( ( abs ` M ) gcd ( abs ` N ) ) = ( M gcd N ) )

Proof

Step Hyp Ref Expression
1 zre
 |-  ( M e. ZZ -> M e. RR )
2 zre
 |-  ( N e. ZZ -> N e. RR )
3 absor
 |-  ( M e. RR -> ( ( abs ` M ) = M \/ ( abs ` M ) = -u M ) )
4 absor
 |-  ( N e. RR -> ( ( abs ` N ) = N \/ ( abs ` N ) = -u N ) )
5 3 4 anim12i
 |-  ( ( M e. RR /\ N e. RR ) -> ( ( ( abs ` M ) = M \/ ( abs ` M ) = -u M ) /\ ( ( abs ` N ) = N \/ ( abs ` N ) = -u N ) ) )
6 1 2 5 syl2an
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( ( ( abs ` M ) = M \/ ( abs ` M ) = -u M ) /\ ( ( abs ` N ) = N \/ ( abs ` N ) = -u N ) ) )
7 oveq12
 |-  ( ( ( abs ` M ) = M /\ ( abs ` N ) = N ) -> ( ( abs ` M ) gcd ( abs ` N ) ) = ( M gcd N ) )
8 7 a1i
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( ( ( abs ` M ) = M /\ ( abs ` N ) = N ) -> ( ( abs ` M ) gcd ( abs ` N ) ) = ( M gcd N ) ) )
9 oveq12
 |-  ( ( ( abs ` M ) = -u M /\ ( abs ` N ) = N ) -> ( ( abs ` M ) gcd ( abs ` N ) ) = ( -u M gcd N ) )
10 neggcd
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( -u M gcd N ) = ( M gcd N ) )
11 9 10 sylan9eqr
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( ( abs ` M ) = -u M /\ ( abs ` N ) = N ) ) -> ( ( abs ` M ) gcd ( abs ` N ) ) = ( M gcd N ) )
12 11 ex
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( ( ( abs ` M ) = -u M /\ ( abs ` N ) = N ) -> ( ( abs ` M ) gcd ( abs ` N ) ) = ( M gcd N ) ) )
13 oveq12
 |-  ( ( ( abs ` M ) = M /\ ( abs ` N ) = -u N ) -> ( ( abs ` M ) gcd ( abs ` N ) ) = ( M gcd -u N ) )
14 gcdneg
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M gcd -u N ) = ( M gcd N ) )
15 13 14 sylan9eqr
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( ( abs ` M ) = M /\ ( abs ` N ) = -u N ) ) -> ( ( abs ` M ) gcd ( abs ` N ) ) = ( M gcd N ) )
16 15 ex
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( ( ( abs ` M ) = M /\ ( abs ` N ) = -u N ) -> ( ( abs ` M ) gcd ( abs ` N ) ) = ( M gcd N ) ) )
17 oveq12
 |-  ( ( ( abs ` M ) = -u M /\ ( abs ` N ) = -u N ) -> ( ( abs ` M ) gcd ( abs ` N ) ) = ( -u M gcd -u N ) )
18 znegcl
 |-  ( M e. ZZ -> -u M e. ZZ )
19 gcdneg
 |-  ( ( -u M e. ZZ /\ N e. ZZ ) -> ( -u M gcd -u N ) = ( -u M gcd N ) )
20 18 19 sylan
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( -u M gcd -u N ) = ( -u M gcd N ) )
21 20 10 eqtrd
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( -u M gcd -u N ) = ( M gcd N ) )
22 17 21 sylan9eqr
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( ( abs ` M ) = -u M /\ ( abs ` N ) = -u N ) ) -> ( ( abs ` M ) gcd ( abs ` N ) ) = ( M gcd N ) )
23 22 ex
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( ( ( abs ` M ) = -u M /\ ( abs ` N ) = -u N ) -> ( ( abs ` M ) gcd ( abs ` N ) ) = ( M gcd N ) ) )
24 8 12 16 23 ccased
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( ( ( ( abs ` M ) = M \/ ( abs ` M ) = -u M ) /\ ( ( abs ` N ) = N \/ ( abs ` N ) = -u N ) ) -> ( ( abs ` M ) gcd ( abs ` N ) ) = ( M gcd N ) ) )
25 6 24 mpd
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( ( abs ` M ) gcd ( abs ` N ) ) = ( M gcd N ) )