Metamath Proof Explorer

Theorem 6lcm4e12

Description: The least common multiple of six and four is twelve. (Contributed by AV, 27-Aug-2020)

Ref Expression
Assertion 6lcm4e12 
|- ( 6 lcm 4 ) = ; 1 2

Proof

Step Hyp Ref Expression
1 6cn 
 |-  6 e. CC
2 4cn 
 |-  4 e. CC
3 1 2 mulcli 
 |-  ( 6 x. 4 ) e. CC
4 6nn0 
 |-  6 e. NN0
5 4 nn0zi 
 |-  6 e. ZZ
6 4z 
 |-  4 e. ZZ
7 lcmcl 
 |-  ( ( 6 e. ZZ /\ 4 e. ZZ ) -> ( 6 lcm 4 ) e. NN0 )
8 7 nn0cnd 
 |-  ( ( 6 e. ZZ /\ 4 e. ZZ ) -> ( 6 lcm 4 ) e. CC )
9 5 6 8 mp2an 
 |-  ( 6 lcm 4 ) e. CC
10 gcdcl 
 |-  ( ( 6 e. ZZ /\ 4 e. ZZ ) -> ( 6 gcd 4 ) e. NN0 )
11 10 nn0cnd 
 |-  ( ( 6 e. ZZ /\ 4 e. ZZ ) -> ( 6 gcd 4 ) e. CC )
12 5 6 11 mp2an 
 |-  ( 6 gcd 4 ) e. CC
13 5 6 pm3.2i 
 |-  ( 6 e. ZZ /\ 4 e. ZZ )
14 4ne0 
 |-  4 =/= 0
15 14 neii 
 |-  -. 4 = 0
16 15 intnan 
 |-  -. ( 6 = 0 /\ 4 = 0 )
17 gcdn0cl 
 |-  ( ( ( 6 e. ZZ /\ 4 e. ZZ ) /\ -. ( 6 = 0 /\ 4 = 0 ) ) -> ( 6 gcd 4 ) e. NN )
18 13 16 17 mp2an 
 |-  ( 6 gcd 4 ) e. NN
19 18 nnne0i 
 |-  ( 6 gcd 4 ) =/= 0
20 12 19 pm3.2i 
 |-  ( ( 6 gcd 4 ) e. CC /\ ( 6 gcd 4 ) =/= 0 )
21 6nn 
 |-  6 e. NN
22 4nn 
 |-  4 e. NN
23 21 22 pm3.2i 
 |-  ( 6 e. NN /\ 4 e. NN )
24 lcmgcdnn 
 |-  ( ( 6 e. NN /\ 4 e. NN ) -> ( ( 6 lcm 4 ) x. ( 6 gcd 4 ) ) = ( 6 x. 4 ) )
25 23 24 mp1i 
 |-  ( ( ( 6 x. 4 ) e. CC /\ ( 6 lcm 4 ) e. CC /\ ( ( 6 gcd 4 ) e. CC /\ ( 6 gcd 4 ) =/= 0 ) ) -> ( ( 6 lcm 4 ) x. ( 6 gcd 4 ) ) = ( 6 x. 4 ) )
26 25 eqcomd 
 |-  ( ( ( 6 x. 4 ) e. CC /\ ( 6 lcm 4 ) e. CC /\ ( ( 6 gcd 4 ) e. CC /\ ( 6 gcd 4 ) =/= 0 ) ) -> ( 6 x. 4 ) = ( ( 6 lcm 4 ) x. ( 6 gcd 4 ) ) )
27 divmul3 
 |-  ( ( ( 6 x. 4 ) e. CC /\ ( 6 lcm 4 ) e. CC /\ ( ( 6 gcd 4 ) e. CC /\ ( 6 gcd 4 ) =/= 0 ) ) -> ( ( ( 6 x. 4 ) / ( 6 gcd 4 ) ) = ( 6 lcm 4 ) <-> ( 6 x. 4 ) = ( ( 6 lcm 4 ) x. ( 6 gcd 4 ) ) ) )
28 26 27 mpbird 
 |-  ( ( ( 6 x. 4 ) e. CC /\ ( 6 lcm 4 ) e. CC /\ ( ( 6 gcd 4 ) e. CC /\ ( 6 gcd 4 ) =/= 0 ) ) -> ( ( 6 x. 4 ) / ( 6 gcd 4 ) ) = ( 6 lcm 4 ) )
29 28 eqcomd 
 |-  ( ( ( 6 x. 4 ) e. CC /\ ( 6 lcm 4 ) e. CC /\ ( ( 6 gcd 4 ) e. CC /\ ( 6 gcd 4 ) =/= 0 ) ) -> ( 6 lcm 4 ) = ( ( 6 x. 4 ) / ( 6 gcd 4 ) ) )
30 3 9 20 29 mp3an 
 |-  ( 6 lcm 4 ) = ( ( 6 x. 4 ) / ( 6 gcd 4 ) )
31 6gcd4e2 
 |-  ( 6 gcd 4 ) = 2
32 31 oveq2i 
 |-  ( ( 6 x. 4 ) / ( 6 gcd 4 ) ) = ( ( 6 x. 4 ) / 2 )
33 2cn 
 |-  2 e. CC
34 2ne0 
 |-  2 =/= 0
35 1 2 33 34 divassi 
 |-  ( ( 6 x. 4 ) / 2 ) = ( 6 x. ( 4 / 2 ) )
36 4d2e2 
 |-  ( 4 / 2 ) = 2
37 36 oveq2i 
 |-  ( 6 x. ( 4 / 2 ) ) = ( 6 x. 2 )
38 6t2e12 
 |-  ( 6 x. 2 ) = ; 1 2
39 35 37 38 3eqtri 
 |-  ( ( 6 x. 4 ) / 2 ) = ; 1 2
40 30 32 39 3eqtri 
 |-  ( 6 lcm 4 ) = ; 1 2