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

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 𝑁 ) )