Metamath Proof Explorer

Theorem lcmfpr

Description: The value of the _lcm function for an unordered pair is the value of the lcm operator for both elements. (Contributed by AV, 22-Aug-2020) (Proof shortened by AV, 16-Sep-2020)

Ref Expression
Assertion lcmfpr ⊢ M ∈ ℤ ∧ N ∈ ℤ → lcm _ ⁡ M N = M lcm N

Proof

Step Hyp Ref Expression
1 c0ex ⊢ 0 ∈ V
2 1 elpr ⊢ 0 ∈ M N ↔ 0 = M ∨ 0 = N
3 eqcom ⊢ 0 = M ↔ M = 0
4 eqcom ⊢ 0 = N ↔ N = 0
5 3 4 orbi12i ⊢ 0 = M ∨ 0 = N ↔ M = 0 ∨ N = 0
6 2 5 bitri ⊢ 0 ∈ M N ↔ M = 0 ∨ N = 0
7 6 a1i ⊢ M ∈ ℤ ∧ N ∈ ℤ → 0 ∈ M N ↔ M = 0 ∨ N = 0
8 breq1 ⊢ m = M → m ∥ n ↔ M ∥ n
9 breq1 ⊢ m = N → m ∥ n ↔ N ∥ n
10 8 9 ralprg ⊢ M ∈ ℤ ∧ N ∈ ℤ → ∀ m ∈ M N m ∥ n ↔ M ∥ n ∧ N ∥ n
11 10 rabbidv ⊢ M ∈ ℤ ∧ N ∈ ℤ → n ∈ ℕ | ∀ m ∈ M N m ∥ n = n ∈ ℕ | M ∥ n ∧ N ∥ n
12 11 infeq1d ⊢ M ∈ ℤ ∧ N ∈ ℤ → inf n ∈ ℕ | ∀ m ∈ M N m ∥ n ℝ < = inf n ∈ ℕ | M ∥ n ∧ N ∥ n ℝ <
13 7 12 ifbieq2d ⊢ M ∈ ℤ ∧ N ∈ ℤ → if 0 ∈ M N 0 inf n ∈ ℕ | ∀ m ∈ M N m ∥ n ℝ < = if M = 0 ∨ N = 0 0 inf n ∈ ℕ | M ∥ n ∧ N ∥ n ℝ <
14 prssi ⊢ M ∈ ℤ ∧ N ∈ ℤ → M N ⊆ ℤ
15 prfi ⊢ M N ∈ Fin
16 lcmfval ⊢ M N ⊆ ℤ ∧ M N ∈ Fin → lcm _ ⁡ M N = if 0 ∈ M N 0 inf n ∈ ℕ | ∀ m ∈ M N m ∥ n ℝ <
17 14 15 16 sylancl ⊢ M ∈ ℤ ∧ N ∈ ℤ → lcm _ ⁡ M N = if 0 ∈ M N 0 inf n ∈ ℕ | ∀ m ∈ M N m ∥ n ℝ <
18 lcmval ⊢ M ∈ ℤ ∧ N ∈ ℤ → M lcm N = if M = 0 ∨ N = 0 0 inf n ∈ ℕ | M ∥ n ∧ N ∥ n ℝ <
19 13 17 18 3eqtr4d ⊢ M ∈ ℤ ∧ N ∈ ℤ → lcm _ ⁡ M N = M lcm N