Metamath Proof Explorer

Theorem 3lcm2e6

Description: The least common multiple of three and two is six. The operands are unequal primes and thus coprime, so the result is (the absolute value of) their product. (Contributed by Steve Rodriguez, 20-Jan-2020) (Proof shortened by AV, 27-Aug-2020)

Ref Expression
Assertion 3lcm2e6 
|- ( 3 lcm 2 ) = 6

Proof

Step Hyp Ref Expression
1 2re 
 |-  2 e. RR
2 2lt3 
 |-  2 < 3
3 1 2 gtneii 
 |-  3 =/= 2
4 3prm 
 |-  3 e. Prime
5 2prm 
 |-  2 e. Prime
6 prmrp 
 |-  ( ( 3 e. Prime /\ 2 e. Prime ) -> ( ( 3 gcd 2 ) = 1 <-> 3 =/= 2 ) )
7 4 5 6 mp2an 
 |-  ( ( 3 gcd 2 ) = 1 <-> 3 =/= 2 )
8 3 7 mpbir 
 |-  ( 3 gcd 2 ) = 1
9 8 oveq2i 
 |-  ( ( 3 lcm 2 ) x. ( 3 gcd 2 ) ) = ( ( 3 lcm 2 ) x. 1 )
10 3nn 
 |-  3 e. NN
11 2nn 
 |-  2 e. NN
12 lcmgcdnn 
 |-  ( ( 3 e. NN /\ 2 e. NN ) -> ( ( 3 lcm 2 ) x. ( 3 gcd 2 ) ) = ( 3 x. 2 ) )
13 10 11 12 mp2an 
 |-  ( ( 3 lcm 2 ) x. ( 3 gcd 2 ) ) = ( 3 x. 2 )
14 10 nnzi 
 |-  3 e. ZZ
15 11 nnzi 
 |-  2 e. ZZ
16 lcmcl 
 |-  ( ( 3 e. ZZ /\ 2 e. ZZ ) -> ( 3 lcm 2 ) e. NN0 )
17 14 15 16 mp2an 
 |-  ( 3 lcm 2 ) e. NN0
18 17 nn0cni 
 |-  ( 3 lcm 2 ) e. CC
19 18 mulridi 
 |-  ( ( 3 lcm 2 ) x. 1 ) = ( 3 lcm 2 )
20 9 13 19 3eqtr3ri 
 |-  ( 3 lcm 2 ) = ( 3 x. 2 )
21 3t2e6 
 |-  ( 3 x. 2 ) = 6
22 20 21 eqtri 
 |-  ( 3 lcm 2 ) = 6