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_⁡MN=MlcmN

Proof

Step Hyp Ref Expression
1 c0ex ⊢0∈V
2 1 elpr ⊢0∈MN↔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∈MN↔M=0∨N=0
7 6 a1i ⊢M∈ℤ∧N∈ℤ→0∈MN↔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∈MNm∥n↔M∥n∧N∥n
11 10 rabbidv ⊢M∈ℤ∧N∈ℤ→n∈ℕ|∀m∈MNm∥n=n∈ℕ|M∥n∧N∥n
12 11 infeq1d ⊢M∈ℤ∧N∈ℤ→supn∈ℕ|∀m∈MNm∥nℝ<=supn∈ℕ|M∥n∧N∥nℝ<
13 7 12 ifbieq2d ⊢M∈ℤ∧N∈ℤ→if0∈MN0supn∈ℕ|∀m∈MNm∥nℝ<=ifM=0∨N=00supn∈ℕ|M∥n∧N∥nℝ<
14 prssi ⊢M∈ℤ∧N∈ℤ→MN⊆ℤ
15 prfi ⊢MN∈Fin
16 lcmfval ⊢MN⊆ℤ∧MN∈Fin→lcm_⁡MN=if0∈MN0supn∈ℕ|∀m∈MNm∥nℝ<
17 14 15 16 sylancl ⊢M∈ℤ∧N∈ℤ→lcm_⁡MN=if0∈MN0supn∈ℕ|∀m∈MNm∥nℝ<
18 lcmval ⊢M∈ℤ∧N∈ℤ→MlcmN=ifM=0∨N=00supn∈ℕ|M∥n∧N∥nℝ<
19 13 17 18 3eqtr4d ⊢M∈ℤ∧N∈ℤ→lcm_⁡MN=MlcmN