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

Metamath Proof Explorer

Theorem lcmval

Description: Value of the lcm operator. ( M lcm N ) is the least common multiple of M and N . If either M or N is 0 , the result is defined conventionally as 0 . Contrast with df-gcd and gcdval . (Contributed by Steve Rodriguez, 20-Jan-2020) (Revised by AV, 16-Sep-2020)

Ref Expression
Assertion lcmval ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 lcm 𝑁 ) = if ( ( 𝑀 = 0 ∨ 𝑁 = 0 ) , 0 , inf ( { 𝑛 ∈ ℕ ∣ ( 𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛 ) } , ℝ , < ) ) )

Proof

Step Hyp Ref Expression
1 eqeq1 ⊢ ( 𝑥 = 𝑀 → ( 𝑥 = 0 ↔ 𝑀 = 0 ) )
2 1 orbi1d ⊢ ( 𝑥 = 𝑀 → ( ( 𝑥 = 0 ∨ 𝑦 = 0 ) ↔ ( 𝑀 = 0 ∨ 𝑦 = 0 ) ) )
3 breq1 ⊢ ( 𝑥 = 𝑀 → ( 𝑥 ∥ 𝑛 ↔ 𝑀 ∥ 𝑛 ) )
4 3 anbi1d ⊢ ( 𝑥 = 𝑀 → ( ( 𝑥 ∥ 𝑛 ∧ 𝑦 ∥ 𝑛 ) ↔ ( 𝑀 ∥ 𝑛 ∧ 𝑦 ∥ 𝑛 ) ) )
5 4 rabbidv ⊢ ( 𝑥 = 𝑀 → { 𝑛 ∈ ℕ ∣ ( 𝑥 ∥ 𝑛 ∧ 𝑦 ∥ 𝑛 ) } = { 𝑛 ∈ ℕ ∣ ( 𝑀 ∥ 𝑛 ∧ 𝑦 ∥ 𝑛 ) } )
6 5 infeq1d ⊢ ( 𝑥 = 𝑀 → inf ( { 𝑛 ∈ ℕ ∣ ( 𝑥 ∥ 𝑛 ∧ 𝑦 ∥ 𝑛 ) } , ℝ , < ) = inf ( { 𝑛 ∈ ℕ ∣ ( 𝑀 ∥ 𝑛 ∧ 𝑦 ∥ 𝑛 ) } , ℝ , < ) )
7 2 6 ifbieq2d ⊢ ( 𝑥 = 𝑀 → if ( ( 𝑥 = 0 ∨ 𝑦 = 0 ) , 0 , inf ( { 𝑛 ∈ ℕ ∣ ( 𝑥 ∥ 𝑛 ∧ 𝑦 ∥ 𝑛 ) } , ℝ , < ) ) = if ( ( 𝑀 = 0 ∨ 𝑦 = 0 ) , 0 , inf ( { 𝑛 ∈ ℕ ∣ ( 𝑀 ∥ 𝑛 ∧ 𝑦 ∥ 𝑛 ) } , ℝ , < ) ) )
8 eqeq1 ⊢ ( 𝑦 = 𝑁 → ( 𝑦 = 0 ↔ 𝑁 = 0 ) )
9 8 orbi2d ⊢ ( 𝑦 = 𝑁 → ( ( 𝑀 = 0 ∨ 𝑦 = 0 ) ↔ ( 𝑀 = 0 ∨ 𝑁 = 0 ) ) )
10 breq1 ⊢ ( 𝑦 = 𝑁 → ( 𝑦 ∥ 𝑛 ↔ 𝑁 ∥ 𝑛 ) )
11 10 anbi2d ⊢ ( 𝑦 = 𝑁 → ( ( 𝑀 ∥ 𝑛 ∧ 𝑦 ∥ 𝑛 ) ↔ ( 𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛 ) ) )
12 11 rabbidv ⊢ ( 𝑦 = 𝑁 → { 𝑛 ∈ ℕ ∣ ( 𝑀 ∥ 𝑛 ∧ 𝑦 ∥ 𝑛 ) } = { 𝑛 ∈ ℕ ∣ ( 𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛 ) } )
13 12 infeq1d ⊢ ( 𝑦 = 𝑁 → inf ( { 𝑛 ∈ ℕ ∣ ( 𝑀 ∥ 𝑛 ∧ 𝑦 ∥ 𝑛 ) } , ℝ , < ) = inf ( { 𝑛 ∈ ℕ ∣ ( 𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛 ) } , ℝ , < ) )
14 9 13 ifbieq2d ⊢ ( 𝑦 = 𝑁 → if ( ( 𝑀 = 0 ∨ 𝑦 = 0 ) , 0 , inf ( { 𝑛 ∈ ℕ ∣ ( 𝑀 ∥ 𝑛 ∧ 𝑦 ∥ 𝑛 ) } , ℝ , < ) ) = if ( ( 𝑀 = 0 ∨ 𝑁 = 0 ) , 0 , inf ( { 𝑛 ∈ ℕ ∣ ( 𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛 ) } , ℝ , < ) ) )
15 df-lcm ⊢ lcm = ( 𝑥 ∈ ℤ , 𝑦 ∈ ℤ ↦ if ( ( 𝑥 = 0 ∨ 𝑦 = 0 ) , 0 , inf ( { 𝑛 ∈ ℕ ∣ ( 𝑥 ∥ 𝑛 ∧ 𝑦 ∥ 𝑛 ) } , ℝ , < ) ) )
16 c0ex ⊢ 0 ∈ V
17 ltso ⊢ < Or ℝ
18 17 infex ⊢ inf ( { 𝑛 ∈ ℕ ∣ ( 𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛 ) } , ℝ , < ) ∈ V
19 16 18 ifex ⊢ if ( ( 𝑀 = 0 ∨ 𝑁 = 0 ) , 0 , inf ( { 𝑛 ∈ ℕ ∣ ( 𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛 ) } , ℝ , < ) ) ∈ V
20 7 14 15 19 ovmpo ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 lcm 𝑁 ) = if ( ( 𝑀 = 0 ∨ 𝑁 = 0 ) , 0 , inf ( { 𝑛 ∈ ℕ ∣ ( 𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛 ) } , ℝ , < ) ) )