Metamath Proof Explorer

Theorem lcmfunnnd

Description: Useful equation to calculate the least common multiple of 1 to n. (Contributed by metakunt, 29-Apr-2024)

Ref Expression
Hypothesis lcmfunnnd.1 
|- ( ph -> N e. NN )
Assertion lcmfunnnd 
|- ( ph -> ( _lcm ` ( 1 ... N ) ) = ( ( _lcm ` ( 1 ... ( N - 1 ) ) ) lcm N ) )

Proof

Step Hyp Ref Expression
1 lcmfunnnd.1 
 |-  ( ph -> N e. NN )
2 1 nncnd 
 |-  ( ph -> N e. CC )
3 1cnd 
 |-  ( ph -> 1 e. CC )
4 2 3 npcand 
 |-  ( ph -> ( ( N - 1 ) + 1 ) = N )
5 4 oveq2d 
 |-  ( ph -> ( 1 ... ( ( N - 1 ) + 1 ) ) = ( 1 ... N ) )
6 nnm1nn0 
 |-  ( N e. NN -> ( N - 1 ) e. NN0 )
7 1 6 syl 
 |-  ( ph -> ( N - 1 ) e. NN0 )
8 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
9 8 eleq2i 
 |-  ( ( N - 1 ) e. NN0 <-> ( N - 1 ) e. ( ZZ>= ` 0 ) )
10 7 9 sylib 
 |-  ( ph -> ( N - 1 ) e. ( ZZ>= ` 0 ) )
11 1m1e0 
 |-  ( 1 - 1 ) = 0
12 11 fveq2i 
 |-  ( ZZ>= ` ( 1 - 1 ) ) = ( ZZ>= ` 0 )
13 12 eleq2i 
 |-  ( ( N - 1 ) e. ( ZZ>= ` ( 1 - 1 ) ) <-> ( N - 1 ) e. ( ZZ>= ` 0 ) )
14 13 a1i 
 |-  ( ph -> ( ( N - 1 ) e. ( ZZ>= ` ( 1 - 1 ) ) <-> ( N - 1 ) e. ( ZZ>= ` 0 ) ) )
15 10 14 mpbird 
 |-  ( ph -> ( N - 1 ) e. ( ZZ>= ` ( 1 - 1 ) ) )
16 1z 
 |-  1 e. ZZ
17 fzsuc2 
 |-  ( ( 1 e. ZZ /\ ( N - 1 ) e. ( ZZ>= ` ( 1 - 1 ) ) ) -> ( 1 ... ( ( N - 1 ) + 1 ) ) = ( ( 1 ... ( N - 1 ) ) u. { ( ( N - 1 ) + 1 ) } ) )
18 16 17 mpan 
 |-  ( ( N - 1 ) e. ( ZZ>= ` ( 1 - 1 ) ) -> ( 1 ... ( ( N - 1 ) + 1 ) ) = ( ( 1 ... ( N - 1 ) ) u. { ( ( N - 1 ) + 1 ) } ) )
19 15 18 syl 
 |-  ( ph -> ( 1 ... ( ( N - 1 ) + 1 ) ) = ( ( 1 ... ( N - 1 ) ) u. { ( ( N - 1 ) + 1 ) } ) )
20 5 19 eqtr3d 
 |-  ( ph -> ( 1 ... N ) = ( ( 1 ... ( N - 1 ) ) u. { ( ( N - 1 ) + 1 ) } ) )
21 4 sneqd 
 |-  ( ph -> { ( ( N - 1 ) + 1 ) } = { N } )
22 21 uneq2d 
 |-  ( ph -> ( ( 1 ... ( N - 1 ) ) u. { ( ( N - 1 ) + 1 ) } ) = ( ( 1 ... ( N - 1 ) ) u. { N } ) )
23 20 22 eqtrd 
 |-  ( ph -> ( 1 ... N ) = ( ( 1 ... ( N - 1 ) ) u. { N } ) )
24 23 fveq2d 
 |-  ( ph -> ( _lcm ` ( 1 ... N ) ) = ( _lcm ` ( ( 1 ... ( N - 1 ) ) u. { N } ) ) )
25 fzssz 
 |-  ( 1 ... ( N - 1 ) ) C_ ZZ
26 25 a1i 
 |-  ( ph -> ( 1 ... ( N - 1 ) ) C_ ZZ )
27 fzfi 
 |-  ( 1 ... ( N - 1 ) ) e. Fin
28 27 a1i 
 |-  ( ph -> ( 1 ... ( N - 1 ) ) e. Fin )
29 nnz 
 |-  ( N e. NN -> N e. ZZ )
30 1 29 syl 
 |-  ( ph -> N e. ZZ )
31 26 28 30 3jca 
 |-  ( ph -> ( ( 1 ... ( N - 1 ) ) C_ ZZ /\ ( 1 ... ( N - 1 ) ) e. Fin /\ N e. ZZ ) )
32 lcmfunsn 
 |-  ( ( ( 1 ... ( N - 1 ) ) C_ ZZ /\ ( 1 ... ( N - 1 ) ) e. Fin /\ N e. ZZ ) -> ( _lcm ` ( ( 1 ... ( N - 1 ) ) u. { N } ) ) = ( ( _lcm ` ( 1 ... ( N - 1 ) ) ) lcm N ) )
33 31 32 syl 
 |-  ( ph -> ( _lcm ` ( ( 1 ... ( N - 1 ) ) u. { N } ) ) = ( ( _lcm ` ( 1 ... ( N - 1 ) ) ) lcm N ) )
34 24 33 eqtrd 
 |-  ( ph -> ( _lcm ` ( 1 ... N ) ) = ( ( _lcm ` ( 1 ... ( N - 1 ) ) ) lcm N ) )