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∈ℤ→MgcdN=MgcdN

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→MgcdN=MgcdN
8 7 a1i ⊢M∈ℤ∧N∈ℤ→M=M∧N=N→MgcdN=MgcdN
9 oveq12 ⊢M=−M∧N=N→MgcdN=- MgcdN
10 neggcd ⊢M∈ℤ∧N∈ℤ→- MgcdN=MgcdN
11 9 10 sylan9eqr ⊢M∈ℤ∧N∈ℤ∧M=−M∧N=N→MgcdN=MgcdN
12 11 ex ⊢M∈ℤ∧N∈ℤ→M=−M∧N=N→MgcdN=MgcdN
13 oveq12 ⊢M=M∧N=−N→MgcdN=Mgcd- N
14 gcdneg ⊢M∈ℤ∧N∈ℤ→Mgcd- N=MgcdN
15 13 14 sylan9eqr ⊢M∈ℤ∧N∈ℤ∧M=M∧N=−N→MgcdN=MgcdN
16 15 ex ⊢M∈ℤ∧N∈ℤ→M=M∧N=−N→MgcdN=MgcdN
17 oveq12 ⊢M=−M∧N=−N→MgcdN=- Mgcd- N
18 znegcl ⊢M∈ℤ→−M∈ℤ
19 gcdneg ⊢−M∈ℤ∧N∈ℤ→- Mgcd- N=- MgcdN
20 18 19 sylan ⊢M∈ℤ∧N∈ℤ→- Mgcd- N=- MgcdN
21 20 10 eqtrd ⊢M∈ℤ∧N∈ℤ→- Mgcd- N=MgcdN
22 17 21 sylan9eqr ⊢M∈ℤ∧N∈ℤ∧M=−M∧N=−N→MgcdN=MgcdN
23 22 ex ⊢M∈ℤ∧N∈ℤ→M=−M∧N=−N→MgcdN=MgcdN
24 8 12 16 23 ccased ⊢M∈ℤ∧N∈ℤ→M=M∨M=−M∧N=N∨N=−N→MgcdN=MgcdN
25 6 24 mpd ⊢M∈ℤ∧N∈ℤ→MgcdN=MgcdN