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

Metamath Proof Explorer

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 ( { 𝑛 ∈ ℕ ∣ ∀ 𝑚 ∈ 𝑍 𝑚 ∥ 𝑛 } , ℝ , < ) ) )