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 ) = ( abs ‘ 1 ) )
33 31 32 ax-mp ⊢ ( 1 gcd 1 ) = ( abs ‘ 1 )
34 abs1 ⊢ ( abs ‘ 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