Metamath Proof Explorer

Theorem 3lcm2e6woprm

Description: The least common multiple of three and two is six. In contrast to 3lcm2e6 , this proof does not use the property of 2 and 3 being prime, therefore it is much longer. (Contributed by Steve Rodriguez, 20-Jan-2020) (Revised by AV, 27-Aug-2020) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion 3lcm2e6woprm ⊢ 3 lcm 2 = 6

Proof

Step Hyp Ref Expression
1 3cn ⊢ 3 ∈ ℂ
2 2cn ⊢ 2 ∈ ℂ
3 1 2 mulcli ⊢ 3 ⋅ 2 ∈ ℂ
4 3z ⊢ 3 ∈ ℤ
5 2z ⊢ 2 ∈ ℤ
6 lcmcl ⊢ 3 ∈ ℤ ∧ 2 ∈ ℤ → 3 lcm 2 ∈ ℕ 0
7 6 nn0cnd ⊢ 3 ∈ ℤ ∧ 2 ∈ ℤ → 3 lcm 2 ∈ ℂ
8 4 5 7 mp2an ⊢ 3 lcm 2 ∈ ℂ
9 4 5 pm3.2i ⊢ 3 ∈ ℤ ∧ 2 ∈ ℤ
10 2ne0 ⊢ 2 ≠ 0
11 10 neii ⊢ ¬ 2 = 0
12 11 intnan ⊢ ¬ 3 = 0 ∧ 2 = 0
13 gcdn0cl ⊢ 3 ∈ ℤ ∧ 2 ∈ ℤ ∧ ¬ 3 = 0 ∧ 2 = 0 → 3 gcd 2 ∈ ℕ
14 13 nncnd ⊢ 3 ∈ ℤ ∧ 2 ∈ ℤ ∧ ¬ 3 = 0 ∧ 2 = 0 → 3 gcd 2 ∈ ℂ
15 9 12 14 mp2an ⊢ 3 gcd 2 ∈ ℂ
16 9 12 13 mp2an ⊢ 3 gcd 2 ∈ ℕ
17 16 nnne0i ⊢ 3 gcd 2 ≠ 0
18 15 17 pm3.2i ⊢ 3 gcd 2 ∈ ℂ ∧ 3 gcd 2 ≠ 0
19 3nn ⊢ 3 ∈ ℕ
20 2nn ⊢ 2 ∈ ℕ
21 19 20 pm3.2i ⊢ 3 ∈ ℕ ∧ 2 ∈ ℕ
22 lcmgcdnn ⊢ 3 ∈ ℕ ∧ 2 ∈ ℕ → 3 lcm 2 ⁢ 3 gcd 2 = 3 ⋅ 2
23 22 eqcomd ⊢ 3 ∈ ℕ ∧ 2 ∈ ℕ → 3 ⋅ 2 = 3 lcm 2 ⁢ 3 gcd 2
24 21 23 mp1i ⊢ 3 ⋅ 2 ∈ ℂ ∧ 3 lcm 2 ∈ ℂ ∧ 3 gcd 2 ∈ ℂ ∧ 3 gcd 2 ≠ 0 → 3 ⋅ 2 = 3 lcm 2 ⁢ 3 gcd 2
25 divmul3 ⊢ 3 ⋅ 2 ∈ ℂ ∧ 3 lcm 2 ∈ ℂ ∧ 3 gcd 2 ∈ ℂ ∧ 3 gcd 2 ≠ 0 → 3 ⋅ 2 3 gcd 2 = 3 lcm 2 ↔ 3 ⋅ 2 = 3 lcm 2 ⁢ 3 gcd 2
26 24 25 mpbird ⊢ 3 ⋅ 2 ∈ ℂ ∧ 3 lcm 2 ∈ ℂ ∧ 3 gcd 2 ∈ ℂ ∧ 3 gcd 2 ≠ 0 → 3 ⋅ 2 3 gcd 2 = 3 lcm 2
27 26 eqcomd ⊢ 3 ⋅ 2 ∈ ℂ ∧ 3 lcm 2 ∈ ℂ ∧ 3 gcd 2 ∈ ℂ ∧ 3 gcd 2 ≠ 0 → 3 lcm 2 = 3 ⋅ 2 3 gcd 2
28 3 8 18 27 mp3an ⊢ 3 lcm 2 = 3 ⋅ 2 3 gcd 2
29 gcdcom ⊢ 3 ∈ ℤ ∧ 2 ∈ ℤ → 3 gcd 2 = 2 gcd 3
30 4 5 29 mp2an ⊢ 3 gcd 2 = 2 gcd 3
31 1z ⊢ 1 ∈ ℤ
32 gcdid ⊢ 1 ∈ ℤ → 1 gcd 1 = 1
33 31 32 ax-mp ⊢ 1 gcd 1 = 1
34 abs1 ⊢ 1 = 1
35 33 34 eqtr2i ⊢ 1 = 1 gcd 1
36 gcdadd ⊢ 1 ∈ ℤ ∧ 1 ∈ ℤ → 1 gcd 1 = 1 gcd 1 + 1
37 31 31 36 mp2an ⊢ 1 gcd 1 = 1 gcd 1 + 1
38 1p1e2 ⊢ 1 + 1 = 2
39 38 oveq2i ⊢ 1 gcd 1 + 1 = 1 gcd 2
40 35 37 39 3eqtri ⊢ 1 = 1 gcd 2
41 gcdcom ⊢ 1 ∈ ℤ ∧ 2 ∈ ℤ → 1 gcd 2 = 2 gcd 1
42 31 5 41 mp2an ⊢ 1 gcd 2 = 2 gcd 1
43 gcdadd ⊢ 2 ∈ ℤ ∧ 1 ∈ ℤ → 2 gcd 1 = 2 gcd 1 + 2
44 5 31 43 mp2an ⊢ 2 gcd 1 = 2 gcd 1 + 2
45 40 42 44 3eqtri ⊢ 1 = 2 gcd 1 + 2
46 1p2e3 ⊢ 1 + 2 = 3
47 46 oveq2i ⊢ 2 gcd 1 + 2 = 2 gcd 3
48 45 47 eqtr2i ⊢ 2 gcd 3 = 1
49 30 48 eqtri ⊢ 3 gcd 2 = 1
50 49 oveq2i ⊢ 3 ⋅ 2 3 gcd 2 = 3 ⋅ 2 1
51 3t2e6 ⊢ 3 ⋅ 2 = 6
52 51 oveq1i ⊢ 3 ⋅ 2 1 = 6 1
53 6cn ⊢ 6 ∈ ℂ
54 53 div1i ⊢ 6 1 = 6
55 52 54 eqtri ⊢ 3 ⋅ 2 1 = 6
56 28 50 55 3eqtri ⊢ 3 lcm 2 = 6