Metamath Proof Explorer

Theorem 6lcm4e12

Description: The least common multiple of six and four is twelve. (Contributed by AV, 27-Aug-2020)

Ref Expression
Assertion 6lcm4e12 ( 6 lcm 4 ) = 1 2

Proof

Step Hyp Ref Expression
1 6cn ⊢ 6 ∈ ℂ
2 4cn ⊢ 4 ∈ ℂ
3 1 2 mulcli ⊢ ( 6 · 4 ) ∈ ℂ
4 6nn0 ⊢ 6 ∈ ℕ0
5 4 nn0zi ⊢ 6 ∈ ℤ
6 4z ⊢ 4 ∈ ℤ
7 lcmcl ⊢ ( ( 6 ∈ ℤ ∧ 4 ∈ ℤ ) → ( 6 lcm 4 ) ∈ ℕ0 )
8 7 nn0cnd ⊢ ( ( 6 ∈ ℤ ∧ 4 ∈ ℤ ) → ( 6 lcm 4 ) ∈ ℂ )
9 5 6 8 mp2an ⊢ ( 6 lcm 4 ) ∈ ℂ
10 gcdcl ⊢ ( ( 6 ∈ ℤ ∧ 4 ∈ ℤ ) → ( 6 gcd 4 ) ∈ ℕ0 )
11 10 nn0cnd ⊢ ( ( 6 ∈ ℤ ∧ 4 ∈ ℤ ) → ( 6 gcd 4 ) ∈ ℂ )
12 5 6 11 mp2an ⊢ ( 6 gcd 4 ) ∈ ℂ
13 5 6 pm3.2i ⊢ ( 6 ∈ ℤ ∧ 4 ∈ ℤ )
14 4ne0 ⊢ 4 ≠ 0
15 14 neii ⊢ ¬ 4 = 0
16 15 intnan ⊢ ¬ ( 6 = 0 ∧ 4 = 0 )
17 gcdn0cl ⊢ ( ( ( 6 ∈ ℤ ∧ 4 ∈ ℤ ) ∧ ¬ ( 6 = 0 ∧ 4 = 0 ) ) → ( 6 gcd 4 ) ∈ ℕ )
18 13 16 17 mp2an ⊢ ( 6 gcd 4 ) ∈ ℕ
19 18 nnne0i ⊢ ( 6 gcd 4 ) ≠ 0
20 12 19 pm3.2i ⊢ ( ( 6 gcd 4 ) ∈ ℂ ∧ ( 6 gcd 4 ) ≠ 0 )
21 6nn ⊢ 6 ∈ ℕ
22 4nn ⊢ 4 ∈ ℕ
23 21 22 pm3.2i ⊢ ( 6 ∈ ℕ ∧ 4 ∈ ℕ )
24 lcmgcdnn ⊢ ( ( 6 ∈ ℕ ∧ 4 ∈ ℕ ) → ( ( 6 lcm 4 ) · ( 6 gcd 4 ) ) = ( 6 · 4 ) )
25 23 24 mp1i ⊢ ( ( ( 6 · 4 ) ∈ ℂ ∧ ( 6 lcm 4 ) ∈ ℂ ∧ ( ( 6 gcd 4 ) ∈ ℂ ∧ ( 6 gcd 4 ) ≠ 0 ) ) → ( ( 6 lcm 4 ) · ( 6 gcd 4 ) ) = ( 6 · 4 ) )
26 25 eqcomd ⊢ ( ( ( 6 · 4 ) ∈ ℂ ∧ ( 6 lcm 4 ) ∈ ℂ ∧ ( ( 6 gcd 4 ) ∈ ℂ ∧ ( 6 gcd 4 ) ≠ 0 ) ) → ( 6 · 4 ) = ( ( 6 lcm 4 ) · ( 6 gcd 4 ) ) )
27 divmul3 ⊢ ( ( ( 6 · 4 ) ∈ ℂ ∧ ( 6 lcm 4 ) ∈ ℂ ∧ ( ( 6 gcd 4 ) ∈ ℂ ∧ ( 6 gcd 4 ) ≠ 0 ) ) → ( ( ( 6 · 4 ) / ( 6 gcd 4 ) ) = ( 6 lcm 4 ) ↔ ( 6 · 4 ) = ( ( 6 lcm 4 ) · ( 6 gcd 4 ) ) ) )
28 26 27 mpbird ⊢ ( ( ( 6 · 4 ) ∈ ℂ ∧ ( 6 lcm 4 ) ∈ ℂ ∧ ( ( 6 gcd 4 ) ∈ ℂ ∧ ( 6 gcd 4 ) ≠ 0 ) ) → ( ( 6 · 4 ) / ( 6 gcd 4 ) ) = ( 6 lcm 4 ) )
29 28 eqcomd ⊢ ( ( ( 6 · 4 ) ∈ ℂ ∧ ( 6 lcm 4 ) ∈ ℂ ∧ ( ( 6 gcd 4 ) ∈ ℂ ∧ ( 6 gcd 4 ) ≠ 0 ) ) → ( 6 lcm 4 ) = ( ( 6 · 4 ) / ( 6 gcd 4 ) ) )
30 3 9 20 29 mp3an ⊢ ( 6 lcm 4 ) = ( ( 6 · 4 ) / ( 6 gcd 4 ) )
31 6gcd4e2 ⊢ ( 6 gcd 4 ) = 2
32 31 oveq2i ⊢ ( ( 6 · 4 ) / ( 6 gcd 4 ) ) = ( ( 6 · 4 ) / 2 )
33 2cn ⊢ 2 ∈ ℂ
34 2ne0 ⊢ 2 ≠ 0
35 1 2 33 34 divassi ⊢ ( ( 6 · 4 ) / 2 ) = ( 6 · ( 4 / 2 ) )
36 4d2e2 ⊢ ( 4 / 2 ) = 2
37 36 oveq2i ⊢ ( 6 · ( 4 / 2 ) ) = ( 6 · 2 )
38 6t2e12 ⊢ ( 6 · 2 ) = 1 2
39 35 37 38 3eqtri ⊢ ( ( 6 · 4 ) / 2 ) = 1 2
40 30 32 39 3eqtri ⊢ ( 6 lcm 4 ) = 1 2