Metamath Proof Explorer


Theorem lcmfpr

Description: The value of the _lcm function for an unordered pair is the value of the lcm operator for both elements. (Contributed by AV, 22-Aug-2020) (Proof shortened by AV, 16-Sep-2020)

Ref Expression
Assertion lcmfpr ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( lcm ‘ { 𝑀 , 𝑁 } ) = ( 𝑀 lcm 𝑁 ) )

Proof

Step Hyp Ref Expression
1 c0ex 0 ∈ V
2 1 elpr ( 0 ∈ { 𝑀 , 𝑁 } ↔ ( 0 = 𝑀 ∨ 0 = 𝑁 ) )
3 eqcom ( 0 = 𝑀𝑀 = 0 )
4 eqcom ( 0 = 𝑁𝑁 = 0 )
5 3 4 orbi12i ( ( 0 = 𝑀 ∨ 0 = 𝑁 ) ↔ ( 𝑀 = 0 ∨ 𝑁 = 0 ) )
6 2 5 bitri ( 0 ∈ { 𝑀 , 𝑁 } ↔ ( 𝑀 = 0 ∨ 𝑁 = 0 ) )
7 6 a1i ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 0 ∈ { 𝑀 , 𝑁 } ↔ ( 𝑀 = 0 ∨ 𝑁 = 0 ) ) )
8 breq1 ( 𝑚 = 𝑀 → ( 𝑚𝑛𝑀𝑛 ) )
9 breq1 ( 𝑚 = 𝑁 → ( 𝑚𝑛𝑁𝑛 ) )
10 8 9 ralprg ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ∀ 𝑚 ∈ { 𝑀 , 𝑁 } 𝑚𝑛 ↔ ( 𝑀𝑛𝑁𝑛 ) ) )
11 10 rabbidv ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → { 𝑛 ∈ ℕ ∣ ∀ 𝑚 ∈ { 𝑀 , 𝑁 } 𝑚𝑛 } = { 𝑛 ∈ ℕ ∣ ( 𝑀𝑛𝑁𝑛 ) } )
12 11 infeq1d ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → inf ( { 𝑛 ∈ ℕ ∣ ∀ 𝑚 ∈ { 𝑀 , 𝑁 } 𝑚𝑛 } , ℝ , < ) = inf ( { 𝑛 ∈ ℕ ∣ ( 𝑀𝑛𝑁𝑛 ) } , ℝ , < ) )
13 7 12 ifbieq2d ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → if ( 0 ∈ { 𝑀 , 𝑁 } , 0 , inf ( { 𝑛 ∈ ℕ ∣ ∀ 𝑚 ∈ { 𝑀 , 𝑁 } 𝑚𝑛 } , ℝ , < ) ) = if ( ( 𝑀 = 0 ∨ 𝑁 = 0 ) , 0 , inf ( { 𝑛 ∈ ℕ ∣ ( 𝑀𝑛𝑁𝑛 ) } , ℝ , < ) ) )
14 prssi ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → { 𝑀 , 𝑁 } ⊆ ℤ )
15 prfi { 𝑀 , 𝑁 } ∈ Fin
16 lcmfval ( ( { 𝑀 , 𝑁 } ⊆ ℤ ∧ { 𝑀 , 𝑁 } ∈ Fin ) → ( lcm ‘ { 𝑀 , 𝑁 } ) = if ( 0 ∈ { 𝑀 , 𝑁 } , 0 , inf ( { 𝑛 ∈ ℕ ∣ ∀ 𝑚 ∈ { 𝑀 , 𝑁 } 𝑚𝑛 } , ℝ , < ) ) )
17 14 15 16 sylancl ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( lcm ‘ { 𝑀 , 𝑁 } ) = if ( 0 ∈ { 𝑀 , 𝑁 } , 0 , inf ( { 𝑛 ∈ ℕ ∣ ∀ 𝑚 ∈ { 𝑀 , 𝑁 } 𝑚𝑛 } , ℝ , < ) ) )
18 lcmval ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 lcm 𝑁 ) = if ( ( 𝑀 = 0 ∨ 𝑁 = 0 ) , 0 , inf ( { 𝑛 ∈ ℕ ∣ ( 𝑀𝑛𝑁𝑛 ) } , ℝ , < ) ) )
19 13 17 18 3eqtr4d ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( lcm ‘ { 𝑀 , 𝑁 } ) = ( 𝑀 lcm 𝑁 ) )