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 ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ¬ ( 𝑀 = 0 ∧ 𝑁 = 0 ) ) → ( ( 𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁 ) → 𝐾 ≤ ( 𝑀 gcd 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 eqid ⊢ { 𝑛 ∈ ℤ ∣ ∀ 𝑧 ∈ { 𝑀 , 𝑁 } 𝑛 ∥ 𝑧 } = { 𝑛 ∈ ℤ ∣ ∀ 𝑧 ∈ { 𝑀 , 𝑁 } 𝑛 ∥ 𝑧 }
2 eqid ⊢ { 𝑛 ∈ ℤ ∣ ( 𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁 ) } = { 𝑛 ∈ ℤ ∣ ( 𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁 ) }
3 1 2 gcdcllem3 ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ¬ ( 𝑀 = 0 ∧ 𝑁 = 0 ) ) → ( sup ( { 𝑛 ∈ ℤ ∣ ( 𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁 ) } , ℝ , < ) ∈ ℕ ∧ ( sup ( { 𝑛 ∈ ℤ ∣ ( 𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁 ) } , ℝ , < ) ∥ 𝑀 ∧ sup ( { 𝑛 ∈ ℤ ∣ ( 𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁 ) } , ℝ , < ) ∥ 𝑁 ) ∧ ( ( 𝐾 ∈ ℤ ∧ 𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁 ) → 𝐾 ≤ sup ( { 𝑛 ∈ ℤ ∣ ( 𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁 ) } , ℝ , < ) ) ) )
4 3 simp3d ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ¬ ( 𝑀 = 0 ∧ 𝑁 = 0 ) ) → ( ( 𝐾 ∈ ℤ ∧ 𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁 ) → 𝐾 ≤ sup ( { 𝑛 ∈ ℤ ∣ ( 𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁 ) } , ℝ , < ) ) )
5 gcdn0val ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ¬ ( 𝑀 = 0 ∧ 𝑁 = 0 ) ) → ( 𝑀 gcd 𝑁 ) = sup ( { 𝑛 ∈ ℤ ∣ ( 𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁 ) } , ℝ , < ) )
6 5 breq2d ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ¬ ( 𝑀 = 0 ∧ 𝑁 = 0 ) ) → ( 𝐾 ≤ ( 𝑀 gcd 𝑁 ) ↔ 𝐾 ≤ sup ( { 𝑛 ∈ ℤ ∣ ( 𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁 ) } , ℝ , < ) ) )
7 4 6 sylibrd ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ¬ ( 𝑀 = 0 ∧ 𝑁 = 0 ) ) → ( ( 𝐾 ∈ ℤ ∧ 𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁 ) → 𝐾 ≤ ( 𝑀 gcd 𝑁 ) ) )
8 7 com12 ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁 ) → ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ¬ ( 𝑀 = 0 ∧ 𝑁 = 0 ) ) → 𝐾 ≤ ( 𝑀 gcd 𝑁 ) ) )
9 8 3expb ⊢ ( ( 𝐾 ∈ ℤ ∧ ( 𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁 ) ) → ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ¬ ( 𝑀 = 0 ∧ 𝑁 = 0 ) ) → 𝐾 ≤ ( 𝑀 gcd 𝑁 ) ) )
10 9 com12 ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ¬ ( 𝑀 = 0 ∧ 𝑁 = 0 ) ) → ( ( 𝐾 ∈ ℤ ∧ ( 𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁 ) ) → 𝐾 ≤ ( 𝑀 gcd 𝑁 ) ) )
11 10 exp4b ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ¬ ( 𝑀 = 0 ∧ 𝑁 = 0 ) → ( 𝐾 ∈ ℤ → ( ( 𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁 ) → 𝐾 ≤ ( 𝑀 gcd 𝑁 ) ) ) ) )
12 11 com23 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 ∈ ℤ → ( ¬ ( 𝑀 = 0 ∧ 𝑁 = 0 ) → ( ( 𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁 ) → 𝐾 ≤ ( 𝑀 gcd 𝑁 ) ) ) ) )
13 12 impcom ⊢ ( ( 𝐾 ∈ ℤ ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( ¬ ( 𝑀 = 0 ∧ 𝑁 = 0 ) → ( ( 𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁 ) → 𝐾 ≤ ( 𝑀 gcd 𝑁 ) ) ) )
14 13 3impb ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ¬ ( 𝑀 = 0 ∧ 𝑁 = 0 ) → ( ( 𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁 ) → 𝐾 ≤ ( 𝑀 gcd 𝑁 ) ) ) )
15 14 imp ⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ¬ ( 𝑀 = 0 ∧ 𝑁 = 0 ) ) → ( ( 𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁 ) → 𝐾 ≤ ( 𝑀 gcd 𝑁 ) ) )