Metamath Proof Explorer


Theorem lcm8un

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

Ref Expression
Assertion lcm8un ( lcm ‘ ( 1 ... 8 ) ) = 8 4 0

Proof

Step Hyp Ref Expression
1 8nn 8 ∈ ℕ
2 id ( 8 ∈ ℕ → 8 ∈ ℕ )
3 2 lcmfunnnd ( 8 ∈ ℕ → ( lcm ‘ ( 1 ... 8 ) ) = ( ( lcm ‘ ( 1 ... ( 8 − 1 ) ) ) lcm 8 ) )
4 1 3 ax-mp ( lcm ‘ ( 1 ... 8 ) ) = ( ( lcm ‘ ( 1 ... ( 8 − 1 ) ) ) lcm 8 )
5 8m1e7 ( 8 − 1 ) = 7
6 5 oveq2i ( 1 ... ( 8 − 1 ) ) = ( 1 ... 7 )
7 6 fveq2i ( lcm ‘ ( 1 ... ( 8 − 1 ) ) ) = ( lcm ‘ ( 1 ... 7 ) )
8 7 oveq1i ( ( lcm ‘ ( 1 ... ( 8 − 1 ) ) ) lcm 8 ) = ( ( lcm ‘ ( 1 ... 7 ) ) lcm 8 )
9 lcm7un ( lcm ‘ ( 1 ... 7 ) ) = 4 2 0
10 9 oveq1i ( ( lcm ‘ ( 1 ... 7 ) ) lcm 8 ) = ( 4 2 0 lcm 8 )
11 8 10 eqtri ( ( lcm ‘ ( 1 ... ( 8 − 1 ) ) ) lcm 8 ) = ( 4 2 0 lcm 8 )
12 420lcm8e840 ( 4 2 0 lcm 8 ) = 8 4 0
13 4 11 12 3eqtri ( lcm ‘ ( 1 ... 8 ) ) = 8 4 0