Metamath Proof Explorer

Theorem gcddvds

Description: The gcd of two integers divides each of them. (Contributed by Paul Chapman, 21-Mar-2011)

Ref Expression
Assertion gcddvds ⊢ M ∈ ℤ ∧ N ∈ ℤ → M gcd N ∥ M ∧ M gcd N ∥ N

Proof

Step Hyp Ref Expression
1 0z ⊢ 0 ∈ ℤ
2 dvds0 ⊢ 0 ∈ ℤ → 0 ∥ 0
3 1 2 ax-mp ⊢ 0 ∥ 0
4 breq2 ⊢ M = 0 → 0 ∥ M ↔ 0 ∥ 0
5 breq2 ⊢ N = 0 → 0 ∥ N ↔ 0 ∥ 0
6 4 5 bi2anan9 ⊢ M = 0 ∧ N = 0 → 0 ∥ M ∧ 0 ∥ N ↔ 0 ∥ 0 ∧ 0 ∥ 0
7 anidm ⊢ 0 ∥ 0 ∧ 0 ∥ 0 ↔ 0 ∥ 0
8 6 7 syl6bb ⊢ M = 0 ∧ N = 0 → 0 ∥ M ∧ 0 ∥ N ↔ 0 ∥ 0
9 3 8 mpbiri ⊢ M = 0 ∧ N = 0 → 0 ∥ M ∧ 0 ∥ N
10 oveq12 ⊢ M = 0 ∧ N = 0 → M gcd N = 0 gcd 0
11 gcd0val ⊢ 0 gcd 0 = 0
12 10 11 syl6eq ⊢ M = 0 ∧ N = 0 → M gcd N = 0
13 12 breq1d ⊢ M = 0 ∧ N = 0 → M gcd N ∥ M ↔ 0 ∥ M
14 12 breq1d ⊢ M = 0 ∧ N = 0 → M gcd N ∥ N ↔ 0 ∥ N
15 13 14 anbi12d ⊢ M = 0 ∧ N = 0 → M gcd N ∥ M ∧ M gcd N ∥ N ↔ 0 ∥ M ∧ 0 ∥ N
16 9 15 mpbird ⊢ M = 0 ∧ N = 0 → M gcd N ∥ M ∧ M gcd N ∥ N
17 16 adantl ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ M = 0 ∧ N = 0 → M gcd N ∥ M ∧ M gcd N ∥ N
18 eqid ⊢ n ∈ ℤ | ∀ z ∈ M N n ∥ z = n ∈ ℤ | ∀ z ∈ M N n ∥ z
19 eqid ⊢ n ∈ ℤ | n ∥ M ∧ n ∥ N = n ∈ ℤ | n ∥ M ∧ n ∥ N
20 18 19 gcdcllem3 ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ ¬ M = 0 ∧ N = 0 → sup n ∈ ℤ | n ∥ M ∧ n ∥ N ℝ < ∈ ℕ ∧ sup n ∈ ℤ | n ∥ M ∧ n ∥ N ℝ < ∥ M ∧ sup n ∈ ℤ | n ∥ M ∧ n ∥ N ℝ < ∥ N ∧ K ∈ ℤ ∧ K ∥ M ∧ K ∥ N → K ≤ sup n ∈ ℤ | n ∥ M ∧ n ∥ N ℝ <
21 20 simp2d ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ ¬ M = 0 ∧ N = 0 → sup n ∈ ℤ | n ∥ M ∧ n ∥ N ℝ < ∥ M ∧ sup n ∈ ℤ | n ∥ M ∧ n ∥ N ℝ < ∥ N
22 gcdn0val ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ ¬ M = 0 ∧ N = 0 → M gcd N = sup n ∈ ℤ | n ∥ M ∧ n ∥ N ℝ <
23 22 breq1d ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ ¬ M = 0 ∧ N = 0 → M gcd N ∥ M ↔ sup n ∈ ℤ | n ∥ M ∧ n ∥ N ℝ < ∥ M
24 22 breq1d ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ ¬ M = 0 ∧ N = 0 → M gcd N ∥ N ↔ sup n ∈ ℤ | n ∥ M ∧ n ∥ N ℝ < ∥ N
25 23 24 anbi12d ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ ¬ M = 0 ∧ N = 0 → M gcd N ∥ M ∧ M gcd N ∥ N ↔ sup n ∈ ℤ | n ∥ M ∧ n ∥ N ℝ < ∥ M ∧ sup n ∈ ℤ | n ∥ M ∧ n ∥ N ℝ < ∥ N
26 21 25 mpbird ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ ¬ M = 0 ∧ N = 0 → M gcd N ∥ M ∧ M gcd N ∥ N
27 17 26 pm2.61dan ⊢ M ∈ ℤ ∧ N ∈ ℤ → M gcd N ∥ M ∧ M gcd N ∥ N