Metamath Proof Explorer

Theorem lcmeprodgcdi

Description: Calculate the least common multiple of two natural numbers. (Contributed by metakunt, 25-Apr-2024)

Ref Expression
Hypotheses lcmeprodgcdi.1 
|- M e. NN
lcmeprodgcdi.2 
|- N e. NN
lcmeprodgcdi.3 
|- G e. NN
lcmeprodgcdi.4 
|- H e. NN
lcmeprodgcdi.5 
|- ( M gcd N ) = G
lcmeprodgcdi.6 
|- ( G x. H ) = A
lcmeprodgcdi.7 
|- ( M x. N ) = A
Assertion lcmeprodgcdi 
|- ( M lcm N ) = H

Proof

Step Hyp Ref Expression
1 lcmeprodgcdi.1 
 |-  M e. NN
2 lcmeprodgcdi.2 
 |-  N e. NN
3 lcmeprodgcdi.3 
 |-  G e. NN
4 lcmeprodgcdi.4 
 |-  H e. NN
5 lcmeprodgcdi.5 
 |-  ( M gcd N ) = G
6 lcmeprodgcdi.6 
 |-  ( G x. H ) = A
7 lcmeprodgcdi.7 
 |-  ( M x. N ) = A
8 5 oveq2i 
 |-  ( ( M lcm N ) x. ( M gcd N ) ) = ( ( M lcm N ) x. G )
9 lcmgcdnn 
 |-  ( ( M e. NN /\ N e. NN ) -> ( ( M lcm N ) x. ( M gcd N ) ) = ( M x. N ) )
10 1 2 9 mp2an 
 |-  ( ( M lcm N ) x. ( M gcd N ) ) = ( M x. N )
11 6 7 eqtr4i 
 |-  ( G x. H ) = ( M x. N )
12 10 11 eqtr4i 
 |-  ( ( M lcm N ) x. ( M gcd N ) ) = ( G x. H )
13 3 4 mulcomnni 
 |-  ( G x. H ) = ( H x. G )
14 12 13 eqtri 
 |-  ( ( M lcm N ) x. ( M gcd N ) ) = ( H x. G )
15 8 14 eqtr3i 
 |-  ( ( M lcm N ) x. G ) = ( H x. G )
16 1 nnzi 
 |-  M e. ZZ
17 2 nnzi 
 |-  N e. ZZ
18 16 17 pm3.2i 
 |-  ( M e. ZZ /\ N e. ZZ )
19 lcmcl 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M lcm N ) e. NN0 )
20 18 19 ax-mp 
 |-  ( M lcm N ) e. NN0
21 20 nn0cni 
 |-  ( M lcm N ) e. CC
22 4 nncni 
 |-  H e. CC
23 3 nncni 
 |-  G e. CC
24 3 nnne0i 
 |-  G =/= 0
25 23 24 pm3.2i 
 |-  ( G e. CC /\ G =/= 0 )
26 21 22 25 3pm3.2i 
 |-  ( ( M lcm N ) e. CC /\ H e. CC /\ ( G e. CC /\ G =/= 0 ) )
27 mulcan2 
 |-  ( ( ( M lcm N ) e. CC /\ H e. CC /\ ( G e. CC /\ G =/= 0 ) ) -> ( ( ( M lcm N ) x. G ) = ( H x. G ) <-> ( M lcm N ) = H ) )
28 26 27 ax-mp 
 |-  ( ( ( M lcm N ) x. G ) = ( H x. G ) <-> ( M lcm N ) = H )
29 15 28 mpbi 
 |-  ( M lcm N ) = H