Theorem lcm2un

Description: Least common multiple of natural numbers up to 2 equals 2. (Contributed by metakunt, 25-Apr-2024)

	Ref	Expression
Assertion	lcm2un	|- ( _lcm ` ( 1 ... 2 ) ) = 2

Proof

Step	Hyp	Ref	Expression
1		2nn	|- 2 e. NN
2		id	|- ( 2 e. NN -> 2 e. NN )
3	2	lcmfunnnd	|- ( 2 e. NN -> ( _lcm ` ( 1 ... 2 ) ) = ( ( _lcm ` ( 1 ... ( 2 - 1 ) ) ) lcm 2 ) )
4	1 3	ax-mp	|- ( _lcm ` ( 1 ... 2 ) ) = ( ( _lcm ` ( 1 ... ( 2 - 1 ) ) ) lcm 2 )
5		2m1e1	|- ( 2 - 1 ) = 1
6	5	oveq2i	|- ( 1 ... ( 2 - 1 ) ) = ( 1 ... 1 )
7	6	fveq2i	|- ( _lcm ` ( 1 ... ( 2 - 1 ) ) ) = ( _lcm ` ( 1 ... 1 ) )
8	7	oveq1i	|- ( ( _lcm ` ( 1 ... ( 2 - 1 ) ) ) lcm 2 ) = ( ( _lcm ` ( 1 ... 1 ) ) lcm 2 )
9	4 8	eqtri	|- ( _lcm ` ( 1 ... 2 ) ) = ( ( _lcm ` ( 1 ... 1 ) ) lcm 2 )
10		lcm1un	|- ( _lcm ` ( 1 ... 1 ) ) = 1
11	10	oveq1i	|- ( ( _lcm ` ( 1 ... 1 ) ) lcm 2 ) = ( 1 lcm 2 )
12		1z	|- 1 e. ZZ
13		2z	|- 2 e. ZZ
14		lcmcom	|- ( ( 1 e. ZZ /\ 2 e. ZZ ) -> ( 1 lcm 2 ) = ( 2 lcm 1 ) )
15	12 13 14	mp2an	|- ( 1 lcm 2 ) = ( 2 lcm 1 )
16		lcm1	|- ( 2 e. ZZ -> ( 2 lcm 1 ) = ( abs ` 2 ) )
17	13 16	ax-mp	|- ( 2 lcm 1 ) = ( abs ` 2 )
18		2re	|- 2 e. RR
19		0le2	|- 0 <_ 2
20	18 19	pm3.2i	|- ( 2 e. RR /\ 0 <_ 2 )
21		absid	|- ( ( 2 e. RR /\ 0 <_ 2 ) -> ( abs ` 2 ) = 2 )
22	20 21	ax-mp	|- ( abs ` 2 ) = 2
23	17 22	eqtri	|- ( 2 lcm 1 ) = 2
24	15 23	eqtri	|- ( 1 lcm 2 ) = 2
25	11 24	eqtri	|- ( ( _lcm ` ( 1 ... 1 ) ) lcm 2 ) = 2
26	9 25	eqtri	|- ( _lcm ` ( 1 ... 2 ) ) = 2