# Metamath Proof Explorer

## Theorem lcmf0val

Description: The value, by convention, of the least common multiple for a set containing 0 is 0. (Contributed by AV, 21-Apr-2020) (Proof shortened by AV, 16-Sep-2020)

Ref Expression
Assertion lcmf0val ${⊢}\left({Z}\subseteq ℤ\wedge 0\in {Z}\right)\to \underset{_}{\mathrm{lcm}}\left({Z}\right)=0$

### Proof

Step Hyp Ref Expression
1 df-lcmf ${⊢}\underset{_}{\mathrm{lcm}}=\left({z}\in 𝒫ℤ⟼if\left(0\in {z},0,sup\left(\left\{{n}\in ℕ|\forall {m}\in {z}\phantom{\rule{.4em}{0ex}}{m}\parallel {n}\right\},ℝ,<\right)\right)\right)$
2 eleq2 ${⊢}{z}={Z}\to \left(0\in {z}↔0\in {Z}\right)$
3 raleq ${⊢}{z}={Z}\to \left(\forall {m}\in {z}\phantom{\rule{.4em}{0ex}}{m}\parallel {n}↔\forall {m}\in {Z}\phantom{\rule{.4em}{0ex}}{m}\parallel {n}\right)$
4 3 rabbidv ${⊢}{z}={Z}\to \left\{{n}\in ℕ|\forall {m}\in {z}\phantom{\rule{.4em}{0ex}}{m}\parallel {n}\right\}=\left\{{n}\in ℕ|\forall {m}\in {Z}\phantom{\rule{.4em}{0ex}}{m}\parallel {n}\right\}$
5 4 infeq1d ${⊢}{z}={Z}\to sup\left(\left\{{n}\in ℕ|\forall {m}\in {z}\phantom{\rule{.4em}{0ex}}{m}\parallel {n}\right\},ℝ,<\right)=sup\left(\left\{{n}\in ℕ|\forall {m}\in {Z}\phantom{\rule{.4em}{0ex}}{m}\parallel {n}\right\},ℝ,<\right)$
6 2 5 ifbieq2d ${⊢}{z}={Z}\to if\left(0\in {z},0,sup\left(\left\{{n}\in ℕ|\forall {m}\in {z}\phantom{\rule{.4em}{0ex}}{m}\parallel {n}\right\},ℝ,<\right)\right)=if\left(0\in {Z},0,sup\left(\left\{{n}\in ℕ|\forall {m}\in {Z}\phantom{\rule{.4em}{0ex}}{m}\parallel {n}\right\},ℝ,<\right)\right)$
7 iftrue ${⊢}0\in {Z}\to if\left(0\in {Z},0,sup\left(\left\{{n}\in ℕ|\forall {m}\in {Z}\phantom{\rule{.4em}{0ex}}{m}\parallel {n}\right\},ℝ,<\right)\right)=0$
8 7 adantl ${⊢}\left({Z}\subseteq ℤ\wedge 0\in {Z}\right)\to if\left(0\in {Z},0,sup\left(\left\{{n}\in ℕ|\forall {m}\in {Z}\phantom{\rule{.4em}{0ex}}{m}\parallel {n}\right\},ℝ,<\right)\right)=0$
9 6 8 sylan9eqr ${⊢}\left(\left({Z}\subseteq ℤ\wedge 0\in {Z}\right)\wedge {z}={Z}\right)\to if\left(0\in {z},0,sup\left(\left\{{n}\in ℕ|\forall {m}\in {z}\phantom{\rule{.4em}{0ex}}{m}\parallel {n}\right\},ℝ,<\right)\right)=0$
10 zex ${⊢}ℤ\in \mathrm{V}$
11 10 ssex ${⊢}{Z}\subseteq ℤ\to {Z}\in \mathrm{V}$
12 elpwg ${⊢}{Z}\in \mathrm{V}\to \left({Z}\in 𝒫ℤ↔{Z}\subseteq ℤ\right)$
13 11 12 syl ${⊢}{Z}\subseteq ℤ\to \left({Z}\in 𝒫ℤ↔{Z}\subseteq ℤ\right)$
14 13 ibir ${⊢}{Z}\subseteq ℤ\to {Z}\in 𝒫ℤ$
15 14 adantr ${⊢}\left({Z}\subseteq ℤ\wedge 0\in {Z}\right)\to {Z}\in 𝒫ℤ$
16 simpr ${⊢}\left({Z}\subseteq ℤ\wedge 0\in {Z}\right)\to 0\in {Z}$
17 1 9 15 16 fvmptd2 ${⊢}\left({Z}\subseteq ℤ\wedge 0\in {Z}\right)\to \underset{_}{\mathrm{lcm}}\left({Z}\right)=0$