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 ( { 𝑛 ∈ ℕ ∣ ( 𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛 ) } , ℝ , < ) ) )