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

Metamath Proof Explorer

Theorem lcmledvds

Description: A positive integer which both operands of the lcm operator divide bounds it. (Contributed by Steve Rodriguez, 20-Jan-2020) (Proof shortened by AV, 16-Sep-2020)

Ref Expression
Assertion lcmledvds ⊢ K ∈ ℕ ∧ M ∈ ℤ ∧ N ∈ ℤ ∧ ¬ M = 0 ∨ N = 0 → M ∥ K ∧ N ∥ K → M lcm N ≤ K

Proof

Step Hyp Ref Expression
1 lcmn0val ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ ¬ M = 0 ∨ N = 0 → M lcm N = inf n ∈ ℕ | M ∥ n ∧ N ∥ n ℝ <
2 1 3adantl1 ⊢ K ∈ ℕ ∧ M ∈ ℤ ∧ N ∈ ℤ ∧ ¬ M = 0 ∨ N = 0 → M lcm N = inf n ∈ ℕ | M ∥ n ∧ N ∥ n ℝ <
3 2 adantr ⊢ K ∈ ℕ ∧ M ∈ ℤ ∧ N ∈ ℤ ∧ ¬ M = 0 ∨ N = 0 ∧ M ∥ K ∧ N ∥ K → M lcm N = inf n ∈ ℕ | M ∥ n ∧ N ∥ n ℝ <
4 breq2 ⊢ n = K → M ∥ n ↔ M ∥ K
5 breq2 ⊢ n = K → N ∥ n ↔ N ∥ K
6 4 5 anbi12d ⊢ n = K → M ∥ n ∧ N ∥ n ↔ M ∥ K ∧ N ∥ K
7 6 elrab ⊢ K ∈ n ∈ ℕ | M ∥ n ∧ N ∥ n ↔ K ∈ ℕ ∧ M ∥ K ∧ N ∥ K
8 ssrab2 ⊢ n ∈ ℕ | M ∥ n ∧ N ∥ n ⊆ ℕ
9 nnuz ⊢ ℕ = ℤ ≥ 1
10 8 9 sseqtri ⊢ n ∈ ℕ | M ∥ n ∧ N ∥ n ⊆ ℤ ≥ 1
11 infssuzle ⊢ n ∈ ℕ | M ∥ n ∧ N ∥ n ⊆ ℤ ≥ 1 ∧ K ∈ n ∈ ℕ | M ∥ n ∧ N ∥ n → inf n ∈ ℕ | M ∥ n ∧ N ∥ n ℝ < ≤ K
12 10 11 mpan ⊢ K ∈ n ∈ ℕ | M ∥ n ∧ N ∥ n → inf n ∈ ℕ | M ∥ n ∧ N ∥ n ℝ < ≤ K
13 7 12 sylbir ⊢ K ∈ ℕ ∧ M ∥ K ∧ N ∥ K → inf n ∈ ℕ | M ∥ n ∧ N ∥ n ℝ < ≤ K
14 13 ex ⊢ K ∈ ℕ → M ∥ K ∧ N ∥ K → inf n ∈ ℕ | M ∥ n ∧ N ∥ n ℝ < ≤ K
15 14 3ad2ant1 ⊢ K ∈ ℕ ∧ M ∈ ℤ ∧ N ∈ ℤ → M ∥ K ∧ N ∥ K → inf n ∈ ℕ | M ∥ n ∧ N ∥ n ℝ < ≤ K
16 15 adantr ⊢ K ∈ ℕ ∧ M ∈ ℤ ∧ N ∈ ℤ ∧ ¬ M = 0 ∨ N = 0 → M ∥ K ∧ N ∥ K → inf n ∈ ℕ | M ∥ n ∧ N ∥ n ℝ < ≤ K
17 16 imp ⊢ K ∈ ℕ ∧ M ∈ ℤ ∧ N ∈ ℤ ∧ ¬ M = 0 ∨ N = 0 ∧ M ∥ K ∧ N ∥ K → inf n ∈ ℕ | M ∥ n ∧ N ∥ n ℝ < ≤ K
18 3 17 eqbrtrd ⊢ K ∈ ℕ ∧ M ∈ ℤ ∧ N ∈ ℤ ∧ ¬ M = 0 ∨ N = 0 ∧ M ∥ K ∧ N ∥ K → M lcm N ≤ K
19 18 ex ⊢ K ∈ ℕ ∧ M ∈ ℤ ∧ N ∈ ℤ ∧ ¬ M = 0 ∨ N = 0 → M ∥ K ∧ N ∥ K → M lcm N ≤ K