Metamath Proof Explorer

Theorem lcm6un

Description: Least common multiple of natural numbers up to 6 equals 60. (Contributed by metakunt, 25-Apr-2024)

Ref Expression
Assertion lcm6un ( lcm ‘ ( 1 ... 6 ) ) = 6 0

Proof

Step Hyp Ref Expression
1 6nn ⊢ 6 ∈ ℕ
2 1 a1i ⊢ ( 6 ∈ ℕ → 6 ∈ ℕ )
3 2 lcmfunnnd ⊢ ( 6 ∈ ℕ → ( lcm ‘ ( 1 ... 6 ) ) = ( ( lcm ‘ ( 1 ... ( 6 − 1 ) ) ) lcm 6 ) )
4 1 3 ax-mp ⊢ ( lcm ‘ ( 1 ... 6 ) ) = ( ( lcm ‘ ( 1 ... ( 6 − 1 ) ) ) lcm 6 )
5 6m1e5 ⊢ ( 6 − 1 ) = 5
6 5 oveq2i ⊢ ( 1 ... ( 6 − 1 ) ) = ( 1 ... 5 )
7 6 fveq2i ⊢ ( lcm ‘ ( 1 ... ( 6 − 1 ) ) ) = ( lcm ‘ ( 1 ... 5 ) )
8 7 oveq1i ⊢ ( ( lcm ‘ ( 1 ... ( 6 − 1 ) ) ) lcm 6 ) = ( ( lcm ‘ ( 1 ... 5 ) ) lcm 6 )
9 lcm5un ⊢ ( lcm ‘ ( 1 ... 5 ) ) = 6 0
10 9 oveq1i ⊢ ( ( lcm ‘ ( 1 ... 5 ) ) lcm 6 ) = ( 6 0 lcm 6 )
11 8 10 eqtri ⊢ ( ( lcm ‘ ( 1 ... ( 6 − 1 ) ) ) lcm 6 ) = ( 6 0 lcm 6 )
12 60lcm6e60 ⊢ ( 6 0 lcm 6 ) = 6 0
13 4 11 12 3eqtri ⊢ ( lcm ‘ ( 1 ... 6 ) ) = 6 0