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 ⊢6lcm4=12

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∈ℤ→6lcm4∈ℕ0
8 7 nn0cnd ⊢6∈ℤ∧4∈ℤ→6lcm4∈ℂ
9 5 6 8 mp2an ⊢6lcm4∈ℂ
10 gcdcl ⊢6∈ℤ∧4∈ℤ→6gcd4∈ℕ0
11 10 nn0cnd ⊢6∈ℤ∧4∈ℤ→6gcd4∈ℂ
12 5 6 11 mp2an ⊢6gcd4∈ℂ
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→6gcd4∈ℕ
18 13 16 17 mp2an ⊢6gcd4∈ℕ
19 18 nnne0i ⊢6gcd4≠0
20 12 19 pm3.2i ⊢6gcd4∈ℂ∧6gcd4≠0
21 6nn ⊢6∈ℕ
22 4nn ⊢4∈ℕ
23 21 22 pm3.2i ⊢6∈ℕ∧4∈ℕ
24 lcmgcdnn ⊢6∈ℕ∧4∈ℕ→6lcm4⁢6gcd4=6⋅4
25 23 24 mp1i ⊢6⋅4∈ℂ∧6lcm4∈ℂ∧6gcd4∈ℂ∧6gcd4≠0→6lcm4⁢6gcd4=6⋅4
26 25 eqcomd ⊢6⋅4∈ℂ∧6lcm4∈ℂ∧6gcd4∈ℂ∧6gcd4≠0→6⋅4=6lcm4⁢6gcd4
27 divmul3 ⊢6⋅4∈ℂ∧6lcm4∈ℂ∧6gcd4∈ℂ∧6gcd4≠0→6⋅46gcd4=6lcm4↔6⋅4=6lcm4⁢6gcd4
28 26 27 mpbird ⊢6⋅4∈ℂ∧6lcm4∈ℂ∧6gcd4∈ℂ∧6gcd4≠0→6⋅46gcd4=6lcm4
29 28 eqcomd ⊢6⋅4∈ℂ∧6lcm4∈ℂ∧6gcd4∈ℂ∧6gcd4≠0→6lcm4=6⋅46gcd4
30 3 9 20 29 mp3an ⊢6lcm4=6⋅46gcd4
31 6gcd4e2 ⊢6gcd4=2
32 31 oveq2i ⊢6⋅46gcd4=6⋅42
33 2cn ⊢2∈ℂ
34 2ne0 ⊢2≠0
35 1 2 33 34 divassi ⊢6⋅42=6⁢42
36 4d2e2 ⊢42=2
37 36 oveq2i ⊢6⁢42=6⋅2
38 6t2e12 ⊢6⋅2=12
39 35 37 38 3eqtri ⊢6⋅42=12
40 30 32 39 3eqtri ⊢6lcm4=12