Metamath Proof Explorer

Theorem ex-lcm

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

Ref Expression
Assertion ex-lcm ( 6 lcm 9 ) = 1 8

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 ∈ ℤ ) → ( 6 lcm 9 ) ∈ ℕ0 )
9 8 nn0cnd ⊢ ( ( 6 ∈ ℤ ∧ 9 ∈ ℤ ) → ( 6 lcm 9 ) ∈ ℂ )
10 7 9 ax-mp ⊢ ( 6 lcm 9 ) ∈ ℂ
11 neggcd ⊢ ( ( 6 ∈ ℤ ∧ 9 ∈ ℤ ) → ( - 6 gcd 9 ) = ( 6 gcd 9 ) )
12 7 11 ax-mp ⊢ ( - 6 gcd 9 ) = ( 6 gcd 9 )
13 12 eqcomi ⊢ ( 6 gcd 9 ) = ( - 6 gcd 9 )
14 ex-gcd ⊢ ( - 6 gcd 9 ) = 3
15 13 14 eqtri ⊢ ( 6 gcd 9 ) = 3
16 3cn ⊢ 3 ∈ ℂ
17 15 16 eqeltri ⊢ ( 6 gcd 9 ) ∈ ℂ
18 3ne0 ⊢ 3 ≠ 0
19 15 18 eqnetri ⊢ ( 6 gcd 9 ) ≠ 0
20 17 19 pm3.2i ⊢ ( ( 6 gcd 9 ) ∈ ℂ ∧ ( 6 gcd 9 ) ≠ 0 )
21 1 2 pm3.2i ⊢ ( 6 ∈ ℕ ∧ 9 ∈ ℕ )
22 lcmgcdnn ⊢ ( ( 6 ∈ ℕ ∧ 9 ∈ ℕ ) → ( ( 6 lcm 9 ) · ( 6 gcd 9 ) ) = ( 6 · 9 ) )
23 21 22 mp1i ⊢ ( ( ( 6 · 9 ) ∈ ℂ ∧ ( 6 lcm 9 ) ∈ ℂ ∧ ( ( 6 gcd 9 ) ∈ ℂ ∧ ( 6 gcd 9 ) ≠ 0 ) ) → ( ( 6 lcm 9 ) · ( 6 gcd 9 ) ) = ( 6 · 9 ) )
24 23 eqcomd ⊢ ( ( ( 6 · 9 ) ∈ ℂ ∧ ( 6 lcm 9 ) ∈ ℂ ∧ ( ( 6 gcd 9 ) ∈ ℂ ∧ ( 6 gcd 9 ) ≠ 0 ) ) → ( 6 · 9 ) = ( ( 6 lcm 9 ) · ( 6 gcd 9 ) ) )
25 divmul3 ⊢ ( ( ( 6 · 9 ) ∈ ℂ ∧ ( 6 lcm 9 ) ∈ ℂ ∧ ( ( 6 gcd 9 ) ∈ ℂ ∧ ( 6 gcd 9 ) ≠ 0 ) ) → ( ( ( 6 · 9 ) / ( 6 gcd 9 ) ) = ( 6 lcm 9 ) ↔ ( 6 · 9 ) = ( ( 6 lcm 9 ) · ( 6 gcd 9 ) ) ) )
26 24 25 mpbird ⊢ ( ( ( 6 · 9 ) ∈ ℂ ∧ ( 6 lcm 9 ) ∈ ℂ ∧ ( ( 6 gcd 9 ) ∈ ℂ ∧ ( 6 gcd 9 ) ≠ 0 ) ) → ( ( 6 · 9 ) / ( 6 gcd 9 ) ) = ( 6 lcm 9 ) )
27 26 eqcomd ⊢ ( ( ( 6 · 9 ) ∈ ℂ ∧ ( 6 lcm 9 ) ∈ ℂ ∧ ( ( 6 gcd 9 ) ∈ ℂ ∧ ( 6 gcd 9 ) ≠ 0 ) ) → ( 6 lcm 9 ) = ( ( 6 · 9 ) / ( 6 gcd 9 ) ) )
28 4 10 20 27 mp3an ⊢ ( 6 lcm 9 ) = ( ( 6 · 9 ) / ( 6 gcd 9 ) )
29 15 oveq2i ⊢ ( ( 6 · 9 ) / ( 6 gcd 9 ) ) = ( ( 6 · 9 ) / 3 )
30 6cn ⊢ 6 ∈ ℂ
31 9cn ⊢ 9 ∈ ℂ
32 30 31 16 18 divassi ⊢ ( ( 6 · 9 ) / 3 ) = ( 6 · ( 9 / 3 ) )
33 3t3e9 ⊢ ( 3 · 3 ) = 9
34 33 eqcomi ⊢ 9 = ( 3 · 3 )
35 34 oveq1i ⊢ ( 9 / 3 ) = ( ( 3 · 3 ) / 3 )
36 16 16 18 divcan3i ⊢ ( ( 3 · 3 ) / 3 ) = 3
37 35 36 eqtri ⊢ ( 9 / 3 ) = 3
38 37 oveq2i ⊢ ( 6 · ( 9 / 3 ) ) = ( 6 · 3 )
39 6t3e18 ⊢ ( 6 · 3 ) = 1 8
40 32 38 39 3eqtri ⊢ ( ( 6 · 9 ) / 3 ) = 1 8
41 28 29 40 3eqtri ⊢ ( 6 lcm 9 ) = 1 8