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	|- ( ( M e. ZZ /\ N e. ZZ ) -> ( _lcm ` { M , N } ) = ( M lcm N ) )

Proof

Step	Hyp	Ref	Expression
1		c0ex	|- 0 e. _V
2	1	elpr	|- ( 0 e. { M , N } <-> ( 0 = M \/ 0 = N ) )
3		eqcom	|- ( 0 = M <-> M = 0 )
4		eqcom	|- ( 0 = N <-> N = 0 )
5	3 4	orbi12i	|- ( ( 0 = M \/ 0 = N ) <-> ( M = 0 \/ N = 0 ) )
6	2 5	bitri	|- ( 0 e. { M , N } <-> ( M = 0 \/ N = 0 ) )
7	6	a1i	|- ( ( M e. ZZ /\ N e. ZZ ) -> ( 0 e. { M , N } <-> ( M = 0 \/ N = 0 ) ) )
8		breq1	|- ( m = M -> ( m || n <-> M || n ) )
9		breq1	|- ( m = N -> ( m || n <-> N || n ) )
10	8 9	ralprg	|- ( ( M e. ZZ /\ N e. ZZ ) -> ( A. m e. { M , N } m || n <-> ( M || n /\ N || n ) ) )
11	10	rabbidv	|- ( ( M e. ZZ /\ N e. ZZ ) -> { n e. NN | A. m e. { M , N } m || n } = { n e. NN | ( M || n /\ N || n ) } )
12	11	infeq1d	|- ( ( M e. ZZ /\ N e. ZZ ) -> inf ( { n e. NN | A. m e. { M , N } m || n } , RR , < ) = inf ( { n e. NN | ( M || n /\ N || n ) } , RR , < ) )
13	7 12	ifbieq2d	|- ( ( M e. ZZ /\ N e. ZZ ) -> if ( 0 e. { M , N } , 0 , inf ( { n e. NN | A. m e. { M , N } m || n } , RR , < ) ) = if ( ( M = 0 \/ N = 0 ) , 0 , inf ( { n e. NN | ( M || n /\ N || n ) } , RR , < ) ) )
14		prssi	|- ( ( M e. ZZ /\ N e. ZZ ) -> { M , N } C_ ZZ )
15		prfi	|- { M , N } e. Fin
16		lcmfval	|- ( ( { M , N } C_ ZZ /\ { M , N } e. Fin ) -> ( _lcm ` { M , N } ) = if ( 0 e. { M , N } , 0 , inf ( { n e. NN | A. m e. { M , N } m || n } , RR , < ) ) )
17	14 15 16	sylancl	|- ( ( M e. ZZ /\ N e. ZZ ) -> ( _lcm ` { M , N } ) = if ( 0 e. { M , N } , 0 , inf ( { n e. NN | A. m e. { M , N } m || n } , RR , < ) ) )
18		lcmval	|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M lcm N ) = if ( ( M = 0 \/ N = 0 ) , 0 , inf ( { n e. NN | ( M || n /\ N || n ) } , RR , < ) ) )
19	13 17 18	3eqtr4d	|- ( ( M e. ZZ /\ N e. ZZ ) -> ( _lcm ` { M , N } ) = ( M lcm N ) )