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