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 ⊢ M gcd N = G
lcmeprodgcdi.6 ⊢ G ⁢ H = A
lcmeprodgcdi.7 ⊢ M ⋅ N = A
Assertion lcmeprodgcdi ⊢ M lcm N = 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 ⊢ M gcd N = G
6 lcmeprodgcdi.6 ⊢ G ⁢ H = A
7 lcmeprodgcdi.7 ⊢ M ⋅ N = A
8 5 oveq2i ⊢ M lcm N ⁢ M gcd N = M lcm N ⁢ G
9 lcmgcdnn ⊢ M ∈ ℕ ∧ N ∈ ℕ → M lcm N ⁢ M gcd N = M ⋅ N
10 1 2 9 mp2an ⊢ M lcm N ⁢ M gcd N = M ⋅ N
11 6 7 eqtr4i ⊢ G ⁢ H = M ⋅ N
12 10 11 eqtr4i ⊢ M lcm N ⁢ M gcd N = G ⁢ H
13 3 4 mulcomnni ⊢ G ⁢ H = H ⁢ G
14 12 13 eqtri ⊢ M lcm N ⁢ M gcd N = H ⁢ G
15 8 14 eqtr3i ⊢ M lcm N ⁢ G = H ⁢ G
16 1 nnzi ⊢ M ∈ ℤ
17 2 nnzi ⊢ N ∈ ℤ
18 16 17 pm3.2i ⊢ M ∈ ℤ ∧ N ∈ ℤ
19 lcmcl ⊢ M ∈ ℤ ∧ N ∈ ℤ → M lcm N ∈ ℕ 0
20 18 19 ax-mp ⊢ M lcm N ∈ ℕ 0
21 20 nn0cni ⊢ M lcm N ∈ ℂ
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 ⊢ M lcm N ∈ ℂ ∧ H ∈ ℂ ∧ G ∈ ℂ ∧ G ≠ 0
27 mulcan2 ⊢ M lcm N ∈ ℂ ∧ H ∈ ℂ ∧ G ∈ ℂ ∧ G ≠ 0 → M lcm N ⁢ G = H ⁢ G ↔ M lcm N = H
28 26 27 ax-mp ⊢ M lcm N ⁢ G = H ⁢ G ↔ M lcm N = H
29 15 28 mpbi ⊢ M lcm N = H