Metamath Proof Explorer

Theorem 3lcm2e6woprm

Description: The least common multiple of three and two is six. In contrast to 3lcm2e6 , this proof does not use the property of 2 and 3 being prime, therefore it is much longer. (Contributed by Steve Rodriguez, 20-Jan-2020) (Revised by AV, 27-Aug-2020) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 3cn 
 |-  3 e. CC
2 2cn 
 |-  2 e. CC
3 1 2 mulcli 
 |-  ( 3 x. 2 ) e. CC
4 3z 
 |-  3 e. ZZ
5 2z 
 |-  2 e. ZZ
6 lcmcl 
 |-  ( ( 3 e. ZZ /\ 2 e. ZZ ) -> ( 3 lcm 2 ) e. NN0 )
7 6 nn0cnd 
 |-  ( ( 3 e. ZZ /\ 2 e. ZZ ) -> ( 3 lcm 2 ) e. CC )
8 4 5 7 mp2an 
 |-  ( 3 lcm 2 ) e. CC
9 4 5 pm3.2i 
 |-  ( 3 e. ZZ /\ 2 e. ZZ )
10 2ne0 
 |-  2 =/= 0
11 10 neii 
 |-  -. 2 = 0
12 11 intnan 
 |-  -. ( 3 = 0 /\ 2 = 0 )
13 gcdn0cl 
 |-  ( ( ( 3 e. ZZ /\ 2 e. ZZ ) /\ -. ( 3 = 0 /\ 2 = 0 ) ) -> ( 3 gcd 2 ) e. NN )
14 13 nncnd 
 |-  ( ( ( 3 e. ZZ /\ 2 e. ZZ ) /\ -. ( 3 = 0 /\ 2 = 0 ) ) -> ( 3 gcd 2 ) e. CC )
15 9 12 14 mp2an 
 |-  ( 3 gcd 2 ) e. CC
16 9 12 13 mp2an 
 |-  ( 3 gcd 2 ) e. NN
17 16 nnne0i 
 |-  ( 3 gcd 2 ) =/= 0
18 15 17 pm3.2i 
 |-  ( ( 3 gcd 2 ) e. CC /\ ( 3 gcd 2 ) =/= 0 )
19 3nn 
 |-  3 e. NN
20 2nn 
 |-  2 e. NN
21 19 20 pm3.2i 
 |-  ( 3 e. NN /\ 2 e. NN )
22 lcmgcdnn 
 |-  ( ( 3 e. NN /\ 2 e. NN ) -> ( ( 3 lcm 2 ) x. ( 3 gcd 2 ) ) = ( 3 x. 2 ) )
23 22 eqcomd 
 |-  ( ( 3 e. NN /\ 2 e. NN ) -> ( 3 x. 2 ) = ( ( 3 lcm 2 ) x. ( 3 gcd 2 ) ) )
24 21 23 mp1i 
 |-  ( ( ( 3 x. 2 ) e. CC /\ ( 3 lcm 2 ) e. CC /\ ( ( 3 gcd 2 ) e. CC /\ ( 3 gcd 2 ) =/= 0 ) ) -> ( 3 x. 2 ) = ( ( 3 lcm 2 ) x. ( 3 gcd 2 ) ) )
25 divmul3 
 |-  ( ( ( 3 x. 2 ) e. CC /\ ( 3 lcm 2 ) e. CC /\ ( ( 3 gcd 2 ) e. CC /\ ( 3 gcd 2 ) =/= 0 ) ) -> ( ( ( 3 x. 2 ) / ( 3 gcd 2 ) ) = ( 3 lcm 2 ) <-> ( 3 x. 2 ) = ( ( 3 lcm 2 ) x. ( 3 gcd 2 ) ) ) )
26 24 25 mpbird 
 |-  ( ( ( 3 x. 2 ) e. CC /\ ( 3 lcm 2 ) e. CC /\ ( ( 3 gcd 2 ) e. CC /\ ( 3 gcd 2 ) =/= 0 ) ) -> ( ( 3 x. 2 ) / ( 3 gcd 2 ) ) = ( 3 lcm 2 ) )
27 26 eqcomd 
 |-  ( ( ( 3 x. 2 ) e. CC /\ ( 3 lcm 2 ) e. CC /\ ( ( 3 gcd 2 ) e. CC /\ ( 3 gcd 2 ) =/= 0 ) ) -> ( 3 lcm 2 ) = ( ( 3 x. 2 ) / ( 3 gcd 2 ) ) )
28 3 8 18 27 mp3an 
 |-  ( 3 lcm 2 ) = ( ( 3 x. 2 ) / ( 3 gcd 2 ) )
29 gcdcom 
 |-  ( ( 3 e. ZZ /\ 2 e. ZZ ) -> ( 3 gcd 2 ) = ( 2 gcd 3 ) )
30 4 5 29 mp2an 
 |-  ( 3 gcd 2 ) = ( 2 gcd 3 )
31 1z 
 |-  1 e. ZZ
32 gcdid 
 |-  ( 1 e. ZZ -> ( 1 gcd 1 ) = ( abs ` 1 ) )
33 31 32 ax-mp 
 |-  ( 1 gcd 1 ) = ( abs ` 1 )
34 abs1 
 |-  ( abs ` 1 ) = 1
35 33 34 eqtr2i 
 |-  1 = ( 1 gcd 1 )
36 gcdadd 
 |-  ( ( 1 e. ZZ /\ 1 e. ZZ ) -> ( 1 gcd 1 ) = ( 1 gcd ( 1 + 1 ) ) )
37 31 31 36 mp2an 
 |-  ( 1 gcd 1 ) = ( 1 gcd ( 1 + 1 ) )
38 1p1e2 
 |-  ( 1 + 1 ) = 2
39 38 oveq2i 
 |-  ( 1 gcd ( 1 + 1 ) ) = ( 1 gcd 2 )
40 35 37 39 3eqtri 
 |-  1 = ( 1 gcd 2 )
41 gcdcom 
 |-  ( ( 1 e. ZZ /\ 2 e. ZZ ) -> ( 1 gcd 2 ) = ( 2 gcd 1 ) )
42 31 5 41 mp2an 
 |-  ( 1 gcd 2 ) = ( 2 gcd 1 )
43 gcdadd 
 |-  ( ( 2 e. ZZ /\ 1 e. ZZ ) -> ( 2 gcd 1 ) = ( 2 gcd ( 1 + 2 ) ) )
44 5 31 43 mp2an 
 |-  ( 2 gcd 1 ) = ( 2 gcd ( 1 + 2 ) )
45 40 42 44 3eqtri 
 |-  1 = ( 2 gcd ( 1 + 2 ) )
46 1p2e3 
 |-  ( 1 + 2 ) = 3
47 46 oveq2i 
 |-  ( 2 gcd ( 1 + 2 ) ) = ( 2 gcd 3 )
48 45 47 eqtr2i 
 |-  ( 2 gcd 3 ) = 1
49 30 48 eqtri 
 |-  ( 3 gcd 2 ) = 1
50 49 oveq2i 
 |-  ( ( 3 x. 2 ) / ( 3 gcd 2 ) ) = ( ( 3 x. 2 ) / 1 )
51 3t2e6 
 |-  ( 3 x. 2 ) = 6
52 51 oveq1i 
 |-  ( ( 3 x. 2 ) / 1 ) = ( 6 / 1 )
53 6cn 
 |-  6 e. CC
54 53 div1i 
 |-  ( 6 / 1 ) = 6
55 52 54 eqtri 
 |-  ( ( 3 x. 2 ) / 1 ) = 6
56 28 50 55 3eqtri 
 |-  ( 3 lcm 2 ) = 6