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