Metamath Proof Explorer

Theorem lcmn0val

Description: The value of the lcm operator when both operands are nonzero. (Contributed by Steve Rodriguez, 20-Jan-2020) (Revised by AV, 16-Sep-2020)

Ref Expression
Assertion lcmn0val ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ ¬ M = 0 ∨ N = 0 → M lcm N = inf n ∈ ℕ | M ∥ n ∧ N ∥ n ℝ <

Proof

Step Hyp Ref Expression
1 lcmval ⊢ M ∈ ℤ ∧ N ∈ ℤ → M lcm N = if M = 0 ∨ N = 0 0 inf n ∈ ℕ | M ∥ n ∧ N ∥ n ℝ <
2 iffalse ⊢ ¬ M = 0 ∨ N = 0 → if M = 0 ∨ N = 0 0 inf n ∈ ℕ | M ∥ n ∧ N ∥ n ℝ < = inf n ∈ ℕ | M ∥ n ∧ N ∥ n ℝ <
3 1 2 sylan9eq ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ ¬ M = 0 ∨ N = 0 → M lcm N = inf n ∈ ℕ | M ∥ n ∧ N ∥ n ℝ <