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∈ℕ
lcmeprodgcdi.2 ⊢N∈ℕ
lcmeprodgcdi.3 ⊢G∈ℕ
lcmeprodgcdi.4 ⊢H∈ℕ
lcmeprodgcdi.5 ⊢MgcdN=G
lcmeprodgcdi.6 ⊢G⁢H=A
lcmeprodgcdi.7 ⊢ M⋅ N=A
Assertion lcmeprodgcdi ⊢MlcmN=H

Proof

Step Hyp Ref Expression
1 lcmeprodgcdi.1 ⊢M∈ℕ
2 lcmeprodgcdi.2 ⊢N∈ℕ
3 lcmeprodgcdi.3 ⊢G∈ℕ
4 lcmeprodgcdi.4 ⊢H∈ℕ
5 lcmeprodgcdi.5 ⊢MgcdN=G
6 lcmeprodgcdi.6 ⊢G⁢H=A
7 lcmeprodgcdi.7 ⊢ M⋅ N=A
8 5 oveq2i ⊢MlcmN⁢MgcdN=MlcmN⁢G
9 lcmgcdnn ⊢M∈ℕ∧N∈ℕ→MlcmN⁢MgcdN= M⋅ N
10 1 2 9 mp2an ⊢MlcmN⁢MgcdN= M⋅ N
11 6 7 eqtr4i ⊢G⁢H= M⋅ N
12 10 11 eqtr4i ⊢MlcmN⁢MgcdN=G⁢H
13 3 4 mulcomnni ⊢G⁢H=H⁢G
14 12 13 eqtri ⊢MlcmN⁢MgcdN=H⁢G
15 8 14 eqtr3i ⊢MlcmN⁢G=H⁢G
16 1 nnzi ⊢M∈ℤ
17 2 nnzi ⊢N∈ℤ
18 16 17 pm3.2i ⊢M∈ℤ∧N∈ℤ
19 lcmcl ⊢M∈ℤ∧N∈ℤ→MlcmN∈ℕ0
20 18 19 ax-mp ⊢MlcmN∈ℕ0
21 20 nn0cni ⊢MlcmN∈ℂ
22 4 nncni ⊢H∈ℂ
23 3 nncni ⊢G∈ℂ
24 3 nnne0i ⊢G≠0
25 23 24 pm3.2i ⊢G∈ℂ∧G≠0
26 21 22 25 3pm3.2i ⊢MlcmN∈ℂ∧H∈ℂ∧G∈ℂ∧G≠0
27 mulcan2 ⊢MlcmN∈ℂ∧H∈ℂ∧G∈ℂ∧G≠0→MlcmN⁢G=H⁢G↔MlcmN=H
28 26 27 ax-mp ⊢MlcmN⁢G=H⁢G↔MlcmN=H
29 15 28 mpbi ⊢MlcmN=H