Metamath Proof Explorer

Theorem ex-lcm

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

Ref Expression
Assertion ex-lcm ⊢6lcm9=18

Proof

Step Hyp Ref Expression
1 6nn ⊢6∈ℕ
2 9nn ⊢9∈ℕ
3 1 2 nnmulcli ⊢6⋅9∈ℕ
4 3 nncni ⊢6⋅9∈ℂ
5 1 nnzi ⊢6∈ℤ
6 2 nnzi ⊢9∈ℤ
7 5 6 pm3.2i ⊢6∈ℤ∧9∈ℤ
8 lcmcl ⊢6∈ℤ∧9∈ℤ→6lcm9∈ℕ0
9 8 nn0cnd ⊢6∈ℤ∧9∈ℤ→6lcm9∈ℂ
10 7 9 ax-mp ⊢6lcm9∈ℂ
11 neggcd ⊢6∈ℤ∧9∈ℤ→-6gcd9=6gcd9
12 7 11 ax-mp ⊢-6gcd9=6gcd9
13 12 eqcomi ⊢6gcd9=-6gcd9
14 ex-gcd ⊢-6gcd9=3
15 13 14 eqtri ⊢6gcd9=3
16 3cn ⊢3∈ℂ
17 15 16 eqeltri ⊢6gcd9∈ℂ
18 3ne0 ⊢3≠0
19 15 18 eqnetri ⊢6gcd9≠0
20 17 19 pm3.2i ⊢6gcd9∈ℂ∧6gcd9≠0
21 1 2 pm3.2i ⊢6∈ℕ∧9∈ℕ
22 lcmgcdnn ⊢6∈ℕ∧9∈ℕ→6lcm9⁢6gcd9=6⋅9
23 21 22 mp1i ⊢6⋅9∈ℂ∧6lcm9∈ℂ∧6gcd9∈ℂ∧6gcd9≠0→6lcm9⁢6gcd9=6⋅9
24 23 eqcomd ⊢6⋅9∈ℂ∧6lcm9∈ℂ∧6gcd9∈ℂ∧6gcd9≠0→6⋅9=6lcm9⁢6gcd9
25 divmul3 ⊢6⋅9∈ℂ∧6lcm9∈ℂ∧6gcd9∈ℂ∧6gcd9≠0→6⋅96gcd9=6lcm9↔6⋅9=6lcm9⁢6gcd9
26 24 25 mpbird ⊢6⋅9∈ℂ∧6lcm9∈ℂ∧6gcd9∈ℂ∧6gcd9≠0→6⋅96gcd9=6lcm9
27 26 eqcomd ⊢6⋅9∈ℂ∧6lcm9∈ℂ∧6gcd9∈ℂ∧6gcd9≠0→6lcm9=6⋅96gcd9
28 4 10 20 27 mp3an ⊢6lcm9=6⋅96gcd9
29 15 oveq2i ⊢6⋅96gcd9=6⋅93
30 6cn ⊢6∈ℂ
31 9cn ⊢9∈ℂ
32 30 31 16 18 divassi ⊢6⋅93=6⁢93
33 3t3e9 ⊢3⋅3=9
34 33 eqcomi ⊢9=3⋅3
35 34 oveq1i ⊢93=3⋅33
36 16 16 18 divcan3i ⊢3⋅33=3
37 35 36 eqtri ⊢93=3
38 37 oveq2i ⊢6⁢93=6⋅3
39 6t3e18 ⊢6⋅3=18
40 32 38 39 3eqtri ⊢6⋅93=18
41 28 29 40 3eqtri ⊢6lcm9=18