Metamath Proof Explorer

Theorem lcmval

Description: Value of the lcm operator. ( M lcm N ) is the least common multiple of M and N . If either M or N is 0 , the result is defined conventionally as 0 . Contrast with df-gcd and gcdval . (Contributed by Steve Rodriguez, 20-Jan-2020) (Revised by AV, 16-Sep-2020)

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

Proof

Step Hyp Ref Expression
1 eqeq1 ⊢ x = M → x = 0 ↔ M = 0
2 1 orbi1d ⊢ x = M → x = 0 ∨ y = 0 ↔ M = 0 ∨ y = 0
3 breq1 ⊢ x = M → x ∥ n ↔ M ∥ n
4 3 anbi1d ⊢ x = M → x ∥ n ∧ y ∥ n ↔ M ∥ n ∧ y ∥ n
5 4 rabbidv ⊢ x = M → n ∈ ℕ | x ∥ n ∧ y ∥ n = n ∈ ℕ | M ∥ n ∧ y ∥ n
6 5 infeq1d ⊢ x = M → inf n ∈ ℕ | x ∥ n ∧ y ∥ n ℝ < = inf n ∈ ℕ | M ∥ n ∧ y ∥ n ℝ <
7 2 6 ifbieq2d ⊢ x = M → if x = 0 ∨ y = 0 0 inf n ∈ ℕ | x ∥ n ∧ y ∥ n ℝ < = if M = 0 ∨ y = 0 0 inf n ∈ ℕ | M ∥ n ∧ y ∥ n ℝ <
8 eqeq1 ⊢ y = N → y = 0 ↔ N = 0
9 8 orbi2d ⊢ y = N → M = 0 ∨ y = 0 ↔ M = 0 ∨ N = 0
10 breq1 ⊢ y = N → y ∥ n ↔ N ∥ n
11 10 anbi2d ⊢ y = N → M ∥ n ∧ y ∥ n ↔ M ∥ n ∧ N ∥ n
12 11 rabbidv ⊢ y = N → n ∈ ℕ | M ∥ n ∧ y ∥ n = n ∈ ℕ | M ∥ n ∧ N ∥ n
13 12 infeq1d ⊢ y = N → inf n ∈ ℕ | M ∥ n ∧ y ∥ n ℝ < = inf n ∈ ℕ | M ∥ n ∧ N ∥ n ℝ <
14 9 13 ifbieq2d ⊢ y = N → if M = 0 ∨ y = 0 0 inf n ∈ ℕ | M ∥ n ∧ y ∥ n ℝ < = if M = 0 ∨ N = 0 0 inf n ∈ ℕ | M ∥ n ∧ N ∥ n ℝ <
15 df-lcm ⊢ lcm = x ∈ ℤ , y ∈ ℤ ⟼ if x = 0 ∨ y = 0 0 inf n ∈ ℕ | x ∥ n ∧ y ∥ n ℝ <
16 c0ex ⊢ 0 ∈ V
17 ltso ⊢ < Or ℝ
18 17 infex ⊢ inf n ∈ ℕ | M ∥ n ∧ N ∥ n ℝ < ∈ V
19 16 18 ifex ⊢ if M = 0 ∨ N = 0 0 inf n ∈ ℕ | M ∥ n ∧ N ∥ n ℝ < ∈ V
20 7 14 15 19 ovmpo ⊢ M ∈ ℤ ∧ N ∈ ℤ → M lcm N = if M = 0 ∨ N = 0 0 inf n ∈ ℕ | M ∥ n ∧ N ∥ n ℝ <