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