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 )