This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem gcdadd

Description: The GCD of two numbers is the same as the GCD of the left and their sum. (Contributed by Scott Fenton, 20-Apr-2014)

Ref Expression
Assertion gcdadd ⊢ M ∈ ℤ ∧ N ∈ ℤ → M gcd N = M gcd N + M

Proof

Step Hyp Ref Expression
1 1z ⊢ 1 ∈ ℤ
2 gcdaddm ⊢ 1 ∈ ℤ ∧ M ∈ ℤ ∧ N ∈ ℤ → M gcd N = M gcd N + 1 ⋅ M
3 1 2 mp3an1 ⊢ M ∈ ℤ ∧ N ∈ ℤ → M gcd N = M gcd N + 1 ⋅ M
4 zcn ⊢ M ∈ ℤ → M ∈ ℂ
5 mullid ⊢ M ∈ ℂ → 1 ⋅ M = M
6 5 oveq2d ⊢ M ∈ ℂ → N + 1 ⋅ M = N + M
7 6 oveq2d ⊢ M ∈ ℂ → M gcd N + 1 ⋅ M = M gcd N + M
8 4 7 syl ⊢ M ∈ ℤ → M gcd N + 1 ⋅ M = M gcd N + M
9 8 adantr ⊢ M ∈ ℤ ∧ N ∈ ℤ → M gcd N + 1 ⋅ M = M gcd N + M
10 3 9 eqtrd ⊢ M ∈ ℤ ∧ N ∈ ℤ → M gcd N = M gcd N + M