This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝑍 ⊆ ℤ ∧ 0 ∈ 𝑍 ) → ( lcm ‘ 𝑍 ) = 0 )

Proof

Step Hyp Ref Expression
1 df-lcmf ⊢ lcm = ( 𝑧 ∈ 𝒫 ℤ ↦ if ( 0 ∈ 𝑧 , 0 , inf ( { 𝑛 ∈ ℕ ∣ ∀ 𝑚 ∈ 𝑧 𝑚 ∥ 𝑛 } , ℝ , < ) ) )
2 eleq2 ⊢ ( 𝑧 = 𝑍 → ( 0 ∈ 𝑧 ↔ 0 ∈ 𝑍 ) )
3 raleq ⊢ ( 𝑧 = 𝑍 → ( ∀ 𝑚 ∈ 𝑧 𝑚 ∥ 𝑛 ↔ ∀ 𝑚 ∈ 𝑍 𝑚 ∥ 𝑛 ) )
4 3 rabbidv ⊢ ( 𝑧 = 𝑍 → { 𝑛 ∈ ℕ ∣ ∀ 𝑚 ∈ 𝑧 𝑚 ∥ 𝑛 } = { 𝑛 ∈ ℕ ∣ ∀ 𝑚 ∈ 𝑍 𝑚 ∥ 𝑛 } )
5 4 infeq1d ⊢ ( 𝑧 = 𝑍 → inf ( { 𝑛 ∈ ℕ ∣ ∀ 𝑚 ∈ 𝑧 𝑚 ∥ 𝑛 } , ℝ , < ) = inf ( { 𝑛 ∈ ℕ ∣ ∀ 𝑚 ∈ 𝑍 𝑚 ∥ 𝑛 } , ℝ , < ) )
6 2 5 ifbieq2d ⊢ ( 𝑧 = 𝑍 → if ( 0 ∈ 𝑧 , 0 , inf ( { 𝑛 ∈ ℕ ∣ ∀ 𝑚 ∈ 𝑧 𝑚 ∥ 𝑛 } , ℝ , < ) ) = if ( 0 ∈ 𝑍 , 0 , inf ( { 𝑛 ∈ ℕ ∣ ∀ 𝑚 ∈ 𝑍 𝑚 ∥ 𝑛 } , ℝ , < ) ) )
7 iftrue ⊢ ( 0 ∈ 𝑍 → if ( 0 ∈ 𝑍 , 0 , inf ( { 𝑛 ∈ ℕ ∣ ∀ 𝑚 ∈ 𝑍 𝑚 ∥ 𝑛 } , ℝ , < ) ) = 0 )
8 7 adantl ⊢ ( ( 𝑍 ⊆ ℤ ∧ 0 ∈ 𝑍 ) → if ( 0 ∈ 𝑍 , 0 , inf ( { 𝑛 ∈ ℕ ∣ ∀ 𝑚 ∈ 𝑍 𝑚 ∥ 𝑛 } , ℝ , < ) ) = 0 )
9 6 8 sylan9eqr ⊢ ( ( ( 𝑍 ⊆ ℤ ∧ 0 ∈ 𝑍 ) ∧ 𝑧 = 𝑍 ) → if ( 0 ∈ 𝑧 , 0 , inf ( { 𝑛 ∈ ℕ ∣ ∀ 𝑚 ∈ 𝑧 𝑚 ∥ 𝑛 } , ℝ , < ) ) = 0 )
10 zex ⊢ ℤ ∈ V
11 10 ssex ⊢ ( 𝑍 ⊆ ℤ → 𝑍 ∈ V )
12 elpwg ⊢ ( 𝑍 ∈ V → ( 𝑍 ∈ 𝒫 ℤ ↔ 𝑍 ⊆ ℤ ) )
13 11 12 syl ⊢ ( 𝑍 ⊆ ℤ → ( 𝑍 ∈ 𝒫 ℤ ↔ 𝑍 ⊆ ℤ ) )
14 13 ibir ⊢ ( 𝑍 ⊆ ℤ → 𝑍 ∈ 𝒫 ℤ )
15 14 adantr ⊢ ( ( 𝑍 ⊆ ℤ ∧ 0 ∈ 𝑍 ) → 𝑍 ∈ 𝒫 ℤ )
16 simpr ⊢ ( ( 𝑍 ⊆ ℤ ∧ 0 ∈ 𝑍 ) → 0 ∈ 𝑍 )
17 1 9 15 16 fvmptd2 ⊢ ( ( 𝑍 ⊆ ℤ ∧ 0 ∈ 𝑍 ) → ( lcm ‘ 𝑍 ) = 0 )