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 ⊢ 𝑀 ∈ ℕ
lcmeprodgcdi.2 ⊢ 𝑁 ∈ ℕ
lcmeprodgcdi.3 ⊢ 𝐺 ∈ ℕ
lcmeprodgcdi.4 ⊢ 𝐻 ∈ ℕ
lcmeprodgcdi.5 ⊢ ( 𝑀 gcd 𝑁 ) = 𝐺
lcmeprodgcdi.6 ⊢ ( 𝐺 · 𝐻 ) = 𝐴
lcmeprodgcdi.7 ⊢ ( 𝑀 · 𝑁 ) = 𝐴
Assertion lcmeprodgcdi ( 𝑀 lcm 𝑁 ) = 𝐻

Proof

Step Hyp Ref Expression
1 lcmeprodgcdi.1 ⊢ 𝑀 ∈ ℕ
2 lcmeprodgcdi.2 ⊢ 𝑁 ∈ ℕ
3 lcmeprodgcdi.3 ⊢ 𝐺 ∈ ℕ
4 lcmeprodgcdi.4 ⊢ 𝐻 ∈ ℕ
5 lcmeprodgcdi.5 ⊢ ( 𝑀 gcd 𝑁 ) = 𝐺
6 lcmeprodgcdi.6 ⊢ ( 𝐺 · 𝐻 ) = 𝐴
7 lcmeprodgcdi.7 ⊢ ( 𝑀 · 𝑁 ) = 𝐴
8 5 oveq2i ⊢ ( ( 𝑀 lcm 𝑁 ) · ( 𝑀 gcd 𝑁 ) ) = ( ( 𝑀 lcm 𝑁 ) · 𝐺 )
9 lcmgcdnn ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑀 lcm 𝑁 ) · ( 𝑀 gcd 𝑁 ) ) = ( 𝑀 · 𝑁 ) )
10 1 2 9 mp2an ⊢ ( ( 𝑀 lcm 𝑁 ) · ( 𝑀 gcd 𝑁 ) ) = ( 𝑀 · 𝑁 )
11 6 7 eqtr4i ⊢ ( 𝐺 · 𝐻 ) = ( 𝑀 · 𝑁 )
12 10 11 eqtr4i ⊢ ( ( 𝑀 lcm 𝑁 ) · ( 𝑀 gcd 𝑁 ) ) = ( 𝐺 · 𝐻 )
13 3 4 mulcomnni ⊢ ( 𝐺 · 𝐻 ) = ( 𝐻 · 𝐺 )
14 12 13 eqtri ⊢ ( ( 𝑀 lcm 𝑁 ) · ( 𝑀 gcd 𝑁 ) ) = ( 𝐻 · 𝐺 )
15 8 14 eqtr3i ⊢ ( ( 𝑀 lcm 𝑁 ) · 𝐺 ) = ( 𝐻 · 𝐺 )
16 1 nnzi ⊢ 𝑀 ∈ ℤ
17 2 nnzi ⊢ 𝑁 ∈ ℤ
18 16 17 pm3.2i ⊢ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ )
19 lcmcl ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 lcm 𝑁 ) ∈ ℕ0 )
20 18 19 ax-mp ⊢ ( 𝑀 lcm 𝑁 ) ∈ ℕ0
21 20 nn0cni ⊢ ( 𝑀 lcm 𝑁 ) ∈ ℂ
22 4 nncni ⊢ 𝐻 ∈ ℂ
23 3 nncni ⊢ 𝐺 ∈ ℂ
24 3 nnne0i ⊢ 𝐺 ≠ 0
25 23 24 pm3.2i ⊢ ( 𝐺 ∈ ℂ ∧ 𝐺 ≠ 0 )
26 21 22 25 3pm3.2i ⊢ ( ( 𝑀 lcm 𝑁 ) ∈ ℂ ∧ 𝐻 ∈ ℂ ∧ ( 𝐺 ∈ ℂ ∧ 𝐺 ≠ 0 ) )
27 mulcan2 ⊢ ( ( ( 𝑀 lcm 𝑁 ) ∈ ℂ ∧ 𝐻 ∈ ℂ ∧ ( 𝐺 ∈ ℂ ∧ 𝐺 ≠ 0 ) ) → ( ( ( 𝑀 lcm 𝑁 ) · 𝐺 ) = ( 𝐻 · 𝐺 ) ↔ ( 𝑀 lcm 𝑁 ) = 𝐻 ) )
28 26 27 ax-mp ⊢ ( ( ( 𝑀 lcm 𝑁 ) · 𝐺 ) = ( 𝐻 · 𝐺 ) ↔ ( 𝑀 lcm 𝑁 ) = 𝐻 )
29 15 28 mpbi ⊢ ( 𝑀 lcm 𝑁 ) = 𝐻