Theorem lcmn0val

Description: The value of the lcm operator when both operands are nonzero. (Contributed by Steve Rodriguez, 20-Jan-2020) (Revised by AV, 16-Sep-2020)

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

Proof

Step	Hyp	Ref	Expression
1		lcmval	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 lcm 𝑁 ) = if ( ( 𝑀 = 0 ∨ 𝑁 = 0 ) , 0 , inf ( { 𝑛 ∈ ℕ ∣ ( 𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛 ) } , ℝ , < ) ) )
2		iffalse	⊢ ( ¬ ( 𝑀 = 0 ∨ 𝑁 = 0 ) → if ( ( 𝑀 = 0 ∨ 𝑁 = 0 ) , 0 , inf ( { 𝑛 ∈ ℕ ∣ ( 𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛 ) } , ℝ , < ) ) = inf ( { 𝑛 ∈ ℕ ∣ ( 𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛 ) } , ℝ , < ) )
3	1 2	sylan9eq	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ¬ ( 𝑀 = 0 ∨ 𝑁 = 0 ) ) → ( 𝑀 lcm 𝑁 ) = inf ( { 𝑛 ∈ ℕ ∣ ( 𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛 ) } , ℝ , < ) )