Theorem lcmfval

Description: Value of the _lcm function. ( _lcmZ ) is the least common multiple of the integers contained in the finite subset of integers Z . If at least one of the elements of Z is 0 , the result is defined conventionally as 0 . (Contributed by AV, 21-Apr-2020) (Revised by AV, 16-Sep-2020)

	Ref	Expression
Assertion	lcmfval	⊢ ( ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ) → ( lcm ‘ 𝑍 ) = if ( 0 ∈ 𝑍 , 0 , inf ( { 𝑛 ∈ ℕ ∣ ∀ 𝑚 ∈ 𝑍 𝑚 ∥ 𝑛 } , ℝ , < ) ) )

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		zex	⊢ ℤ ∈ V
8	7	ssex	⊢ ( 𝑍 ⊆ ℤ → 𝑍 ∈ V )
9		elpwg	⊢ ( 𝑍 ∈ V → ( 𝑍 ∈ 𝒫 ℤ ↔ 𝑍 ⊆ ℤ ) )
10	8 9	syl	⊢ ( 𝑍 ⊆ ℤ → ( 𝑍 ∈ 𝒫 ℤ ↔ 𝑍 ⊆ ℤ ) )
11	10	ibir	⊢ ( 𝑍 ⊆ ℤ → 𝑍 ∈ 𝒫 ℤ )
12	11	adantr	⊢ ( ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ) → 𝑍 ∈ 𝒫 ℤ )
13		0nn0	⊢ 0 ∈ ℕ0
14	13	a1i	⊢ ( ( ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ) ∧ 0 ∈ 𝑍 ) → 0 ∈ ℕ0 )
15		df-nel	⊢ ( 0 ∉ 𝑍 ↔ ¬ 0 ∈ 𝑍 )
16		ssrab2	⊢ { 𝑛 ∈ ℕ ∣ ∀ 𝑚 ∈ 𝑍 𝑚 ∥ 𝑛 } ⊆ ℕ
17		nnssnn0	⊢ ℕ ⊆ ℕ0
18	16 17	sstri	⊢ { 𝑛 ∈ ℕ ∣ ∀ 𝑚 ∈ 𝑍 𝑚 ∥ 𝑛 } ⊆ ℕ0
19		nnuz	⊢ ℕ = ( ℤ≥ ‘ 1 )
20	16 19	sseqtri	⊢ { 𝑛 ∈ ℕ ∣ ∀ 𝑚 ∈ 𝑍 𝑚 ∥ 𝑛 } ⊆ ( ℤ≥ ‘ 1 )
21		fissn0dvdsn0	⊢ ( ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ∧ 0 ∉ 𝑍 ) → { 𝑛 ∈ ℕ ∣ ∀ 𝑚 ∈ 𝑍 𝑚 ∥ 𝑛 } ≠ ∅ )
22	21	3expa	⊢ ( ( ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ) ∧ 0 ∉ 𝑍 ) → { 𝑛 ∈ ℕ ∣ ∀ 𝑚 ∈ 𝑍 𝑚 ∥ 𝑛 } ≠ ∅ )
23		infssuzcl	⊢ ( ( { 𝑛 ∈ ℕ ∣ ∀ 𝑚 ∈ 𝑍 𝑚 ∥ 𝑛 } ⊆ ( ℤ≥ ‘ 1 ) ∧ { 𝑛 ∈ ℕ ∣ ∀ 𝑚 ∈ 𝑍 𝑚 ∥ 𝑛 } ≠ ∅ ) → inf ( { 𝑛 ∈ ℕ ∣ ∀ 𝑚 ∈ 𝑍 𝑚 ∥ 𝑛 } , ℝ , < ) ∈ { 𝑛 ∈ ℕ ∣ ∀ 𝑚 ∈ 𝑍 𝑚 ∥ 𝑛 } )
24	20 22 23	sylancr	⊢ ( ( ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ) ∧ 0 ∉ 𝑍 ) → inf ( { 𝑛 ∈ ℕ ∣ ∀ 𝑚 ∈ 𝑍 𝑚 ∥ 𝑛 } , ℝ , < ) ∈ { 𝑛 ∈ ℕ ∣ ∀ 𝑚 ∈ 𝑍 𝑚 ∥ 𝑛 } )
25	18 24	sselid	⊢ ( ( ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ) ∧ 0 ∉ 𝑍 ) → inf ( { 𝑛 ∈ ℕ ∣ ∀ 𝑚 ∈ 𝑍 𝑚 ∥ 𝑛 } , ℝ , < ) ∈ ℕ0 )
26	15 25	sylan2br	⊢ ( ( ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ) ∧ ¬ 0 ∈ 𝑍 ) → inf ( { 𝑛 ∈ ℕ ∣ ∀ 𝑚 ∈ 𝑍 𝑚 ∥ 𝑛 } , ℝ , < ) ∈ ℕ0 )
27	14 26	ifclda	⊢ ( ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ) → if ( 0 ∈ 𝑍 , 0 , inf ( { 𝑛 ∈ ℕ ∣ ∀ 𝑚 ∈ 𝑍 𝑚 ∥ 𝑛 } , ℝ , < ) ) ∈ ℕ0 )
28	1 6 12 27	fvmptd3	⊢ ( ( 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ) → ( lcm ‘ 𝑍 ) = if ( 0 ∈ 𝑍 , 0 , inf ( { 𝑛 ∈ ℕ ∣ ∀ 𝑚 ∈ 𝑍 𝑚 ∥ 𝑛 } , ℝ , < ) ) )