Metamath Proof Explorer

Theorem ex-lcm

Description: Example for df-lcm . (Contributed by AV, 5-Sep-2021)

Ref Expression
Assertion ex-lcm 
|- ( 6 lcm 9 ) = ; 1 8

Proof

Step Hyp Ref Expression
1 6nn 
 |-  6 e. NN
2 9nn 
 |-  9 e. NN
3 1 2 nnmulcli 
 |-  ( 6 x. 9 ) e. NN
4 3 nncni 
 |-  ( 6 x. 9 ) e. CC
5 1 nnzi 
 |-  6 e. ZZ
6 2 nnzi 
 |-  9 e. ZZ
7 5 6 pm3.2i 
 |-  ( 6 e. ZZ /\ 9 e. ZZ )
8 lcmcl 
 |-  ( ( 6 e. ZZ /\ 9 e. ZZ ) -> ( 6 lcm 9 ) e. NN0 )
9 8 nn0cnd 
 |-  ( ( 6 e. ZZ /\ 9 e. ZZ ) -> ( 6 lcm 9 ) e. CC )
10 7 9 ax-mp 
 |-  ( 6 lcm 9 ) e. CC
11 neggcd 
 |-  ( ( 6 e. ZZ /\ 9 e. ZZ ) -> ( -u 6 gcd 9 ) = ( 6 gcd 9 ) )
12 7 11 ax-mp 
 |-  ( -u 6 gcd 9 ) = ( 6 gcd 9 )
13 12 eqcomi 
 |-  ( 6 gcd 9 ) = ( -u 6 gcd 9 )
14 ex-gcd 
 |-  ( -u 6 gcd 9 ) = 3
15 13 14 eqtri 
 |-  ( 6 gcd 9 ) = 3
16 3cn 
 |-  3 e. CC
17 15 16 eqeltri 
 |-  ( 6 gcd 9 ) e. CC
18 3ne0 
 |-  3 =/= 0
19 15 18 eqnetri 
 |-  ( 6 gcd 9 ) =/= 0
20 17 19 pm3.2i 
 |-  ( ( 6 gcd 9 ) e. CC /\ ( 6 gcd 9 ) =/= 0 )
21 1 2 pm3.2i 
 |-  ( 6 e. NN /\ 9 e. NN )
22 lcmgcdnn 
 |-  ( ( 6 e. NN /\ 9 e. NN ) -> ( ( 6 lcm 9 ) x. ( 6 gcd 9 ) ) = ( 6 x. 9 ) )
23 21 22 mp1i 
 |-  ( ( ( 6 x. 9 ) e. CC /\ ( 6 lcm 9 ) e. CC /\ ( ( 6 gcd 9 ) e. CC /\ ( 6 gcd 9 ) =/= 0 ) ) -> ( ( 6 lcm 9 ) x. ( 6 gcd 9 ) ) = ( 6 x. 9 ) )
24 23 eqcomd 
 |-  ( ( ( 6 x. 9 ) e. CC /\ ( 6 lcm 9 ) e. CC /\ ( ( 6 gcd 9 ) e. CC /\ ( 6 gcd 9 ) =/= 0 ) ) -> ( 6 x. 9 ) = ( ( 6 lcm 9 ) x. ( 6 gcd 9 ) ) )
25 divmul3 
 |-  ( ( ( 6 x. 9 ) e. CC /\ ( 6 lcm 9 ) e. CC /\ ( ( 6 gcd 9 ) e. CC /\ ( 6 gcd 9 ) =/= 0 ) ) -> ( ( ( 6 x. 9 ) / ( 6 gcd 9 ) ) = ( 6 lcm 9 ) <-> ( 6 x. 9 ) = ( ( 6 lcm 9 ) x. ( 6 gcd 9 ) ) ) )
26 24 25 mpbird 
 |-  ( ( ( 6 x. 9 ) e. CC /\ ( 6 lcm 9 ) e. CC /\ ( ( 6 gcd 9 ) e. CC /\ ( 6 gcd 9 ) =/= 0 ) ) -> ( ( 6 x. 9 ) / ( 6 gcd 9 ) ) = ( 6 lcm 9 ) )
27 26 eqcomd 
 |-  ( ( ( 6 x. 9 ) e. CC /\ ( 6 lcm 9 ) e. CC /\ ( ( 6 gcd 9 ) e. CC /\ ( 6 gcd 9 ) =/= 0 ) ) -> ( 6 lcm 9 ) = ( ( 6 x. 9 ) / ( 6 gcd 9 ) ) )
28 4 10 20 27 mp3an 
 |-  ( 6 lcm 9 ) = ( ( 6 x. 9 ) / ( 6 gcd 9 ) )
29 15 oveq2i 
 |-  ( ( 6 x. 9 ) / ( 6 gcd 9 ) ) = ( ( 6 x. 9 ) / 3 )
30 6cn 
 |-  6 e. CC
31 9cn 
 |-  9 e. CC
32 30 31 16 18 divassi 
 |-  ( ( 6 x. 9 ) / 3 ) = ( 6 x. ( 9 / 3 ) )
33 3t3e9 
 |-  ( 3 x. 3 ) = 9
34 33 eqcomi 
 |-  9 = ( 3 x. 3 )
35 34 oveq1i 
 |-  ( 9 / 3 ) = ( ( 3 x. 3 ) / 3 )
36 16 16 18 divcan3i 
 |-  ( ( 3 x. 3 ) / 3 ) = 3
37 35 36 eqtri 
 |-  ( 9 / 3 ) = 3
38 37 oveq2i 
 |-  ( 6 x. ( 9 / 3 ) ) = ( 6 x. 3 )
39 6t3e18 
 |-  ( 6 x. 3 ) = ; 1 8
40 32 38 39 3eqtri 
 |-  ( ( 6 x. 9 ) / 3 ) = ; 1 8
41 28 29 40 3eqtri 
 |-  ( 6 lcm 9 ) = ; 1 8