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

Metamath Proof Explorer

Theorem dvdslegcd

Description: An integer which divides both operands of the gcd operator is bounded by it. (Contributed by Paul Chapman, 21-Mar-2011)

Ref Expression
Assertion dvdslegcd ⊢ K ∈ ℤ ∧ M ∈ ℤ ∧ N ∈ ℤ ∧ ¬ M = 0 ∧ N = 0 → K ∥ M ∧ K ∥ N → K ≤ M gcd N

Proof

Step Hyp Ref Expression
1 eqid ⊢ n ∈ ℤ | ∀ z ∈ M N n ∥ z = n ∈ ℤ | ∀ z ∈ M N n ∥ z
2 eqid ⊢ n ∈ ℤ | n ∥ M ∧ n ∥ N = n ∈ ℤ | n ∥ M ∧ n ∥ N
3 1 2 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 ℝ <
4 3 simp3d ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ ¬ M = 0 ∧ N = 0 → K ∈ ℤ ∧ K ∥ M ∧ K ∥ N → K ≤ sup n ∈ ℤ | n ∥ M ∧ n ∥ N ℝ <
5 gcdn0val ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ ¬ M = 0 ∧ N = 0 → M gcd N = sup n ∈ ℤ | n ∥ M ∧ n ∥ N ℝ <
6 5 breq2d ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ ¬ M = 0 ∧ N = 0 → K ≤ M gcd N ↔ K ≤ sup n ∈ ℤ | n ∥ M ∧ n ∥ N ℝ <
7 4 6 sylibrd ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ ¬ M = 0 ∧ N = 0 → K ∈ ℤ ∧ K ∥ M ∧ K ∥ N → K ≤ M gcd N
8 7 com12 ⊢ K ∈ ℤ ∧ K ∥ M ∧ K ∥ N → M ∈ ℤ ∧ N ∈ ℤ ∧ ¬ M = 0 ∧ N = 0 → K ≤ M gcd N
9 8 3expb ⊢ K ∈ ℤ ∧ K ∥ M ∧ K ∥ N → M ∈ ℤ ∧ N ∈ ℤ ∧ ¬ M = 0 ∧ N = 0 → K ≤ M gcd N
10 9 com12 ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ ¬ M = 0 ∧ N = 0 → K ∈ ℤ ∧ K ∥ M ∧ K ∥ N → K ≤ M gcd N
11 10 exp4b ⊢ M ∈ ℤ ∧ N ∈ ℤ → ¬ M = 0 ∧ N = 0 → K ∈ ℤ → K ∥ M ∧ K ∥ N → K ≤ M gcd N
12 11 com23 ⊢ M ∈ ℤ ∧ N ∈ ℤ → K ∈ ℤ → ¬ M = 0 ∧ N = 0 → K ∥ M ∧ K ∥ N → K ≤ M gcd N
13 12 impcom ⊢ K ∈ ℤ ∧ M ∈ ℤ ∧ N ∈ ℤ → ¬ M = 0 ∧ N = 0 → K ∥ M ∧ K ∥ N → K ≤ M gcd N
14 13 3impb ⊢ K ∈ ℤ ∧ M ∈ ℤ ∧ N ∈ ℤ → ¬ M = 0 ∧ N = 0 → K ∥ M ∧ K ∥ N → K ≤ M gcd N
15 14 imp ⊢ K ∈ ℤ ∧ M ∈ ℤ ∧ N ∈ ℤ ∧ ¬ M = 0 ∧ N = 0 → K ∥ M ∧ K ∥ N → K ≤ M gcd N