Metamath Proof Explorer


Theorem lcmineqlem4

Description: Part of lcm inequality lemma, this part eventually shows that F times the least common multiple of 1 to n is an integer. F is found in lcmineqlem6 . (Contributed by metakunt, 10-May-2024)

Ref Expression
Hypotheses lcmineqlem4.1
|- ( ph -> N e. NN )
lcmineqlem4.2
|- ( ph -> M e. NN )
lcmineqlem4.3
|- ( ph -> M <_ N )
lcmineqlem4.4
|- ( ph -> K e. ( 0 ... ( N - M ) ) )
Assertion lcmineqlem4
|- ( ph -> ( ( _lcm ` ( 1 ... N ) ) / ( M + K ) ) e. ZZ )

Proof

Step Hyp Ref Expression
1 lcmineqlem4.1
 |-  ( ph -> N e. NN )
2 lcmineqlem4.2
 |-  ( ph -> M e. NN )
3 lcmineqlem4.3
 |-  ( ph -> M <_ N )
4 lcmineqlem4.4
 |-  ( ph -> K e. ( 0 ... ( N - M ) ) )
5 breq1
 |-  ( k = ( M + K ) -> ( k || ( _lcm ` ( 1 ... N ) ) <-> ( M + K ) || ( _lcm ` ( 1 ... N ) ) ) )
6 fzssz
 |-  ( 1 ... N ) C_ ZZ
7 fzfi
 |-  ( 1 ... N ) e. Fin
8 6 7 pm3.2i
 |-  ( ( 1 ... N ) C_ ZZ /\ ( 1 ... N ) e. Fin )
9 8 a1i
 |-  ( ph -> ( ( 1 ... N ) C_ ZZ /\ ( 1 ... N ) e. Fin ) )
10 dvdslcmf
 |-  ( ( ( 1 ... N ) C_ ZZ /\ ( 1 ... N ) e. Fin ) -> A. k e. ( 1 ... N ) k || ( _lcm ` ( 1 ... N ) ) )
11 9 10 syl
 |-  ( ph -> A. k e. ( 1 ... N ) k || ( _lcm ` ( 1 ... N ) ) )
12 1zzd
 |-  ( ph -> 1 e. ZZ )
13 2 nnzd
 |-  ( ph -> M e. ZZ )
14 0zd
 |-  ( ph -> 0 e. ZZ )
15 1 nnzd
 |-  ( ph -> N e. ZZ )
16 15 13 zsubcld
 |-  ( ph -> ( N - M ) e. ZZ )
17 2 nnred
 |-  ( ph -> M e. RR )
18 17 leidd
 |-  ( ph -> M <_ M )
19 fznn
 |-  ( M e. ZZ -> ( M e. ( 1 ... M ) <-> ( M e. NN /\ M <_ M ) ) )
20 13 19 syl
 |-  ( ph -> ( M e. ( 1 ... M ) <-> ( M e. NN /\ M <_ M ) ) )
21 2 18 20 mpbir2and
 |-  ( ph -> M e. ( 1 ... M ) )
22 1cnd
 |-  ( ph -> 1 e. CC )
23 22 addid1d
 |-  ( ph -> ( 1 + 0 ) = 1 )
24 23 eqcomd
 |-  ( ph -> 1 = ( 1 + 0 ) )
25 1 nncnd
 |-  ( ph -> N e. CC )
26 2 nncnd
 |-  ( ph -> M e. CC )
27 25 26 npcand
 |-  ( ph -> ( ( N - M ) + M ) = N )
28 eqcom
 |-  ( ( ( N - M ) + M ) = N <-> N = ( ( N - M ) + M ) )
29 28 a1i
 |-  ( ph -> ( ( ( N - M ) + M ) = N <-> N = ( ( N - M ) + M ) ) )
30 25 26 jca
 |-  ( ph -> ( N e. CC /\ M e. CC ) )
31 subcl
 |-  ( ( N e. CC /\ M e. CC ) -> ( N - M ) e. CC )
32 30 31 syl
 |-  ( ph -> ( N - M ) e. CC )
33 32 26 jca
 |-  ( ph -> ( ( N - M ) e. CC /\ M e. CC ) )
34 addcom
 |-  ( ( ( N - M ) e. CC /\ M e. CC ) -> ( ( N - M ) + M ) = ( M + ( N - M ) ) )
35 33 34 syl
 |-  ( ph -> ( ( N - M ) + M ) = ( M + ( N - M ) ) )
36 eqeq2
 |-  ( ( ( N - M ) + M ) = ( M + ( N - M ) ) -> ( N = ( ( N - M ) + M ) <-> N = ( M + ( N - M ) ) ) )
37 35 36 syl
 |-  ( ph -> ( N = ( ( N - M ) + M ) <-> N = ( M + ( N - M ) ) ) )
38 29 37 bitrd
 |-  ( ph -> ( ( ( N - M ) + M ) = N <-> N = ( M + ( N - M ) ) ) )
39 38 pm5.74i
 |-  ( ( ph -> ( ( N - M ) + M ) = N ) <-> ( ph -> N = ( M + ( N - M ) ) ) )
40 27 39 mpbi
 |-  ( ph -> N = ( M + ( N - M ) ) )
41 12 13 14 16 21 4 24 40 fzadd2d
 |-  ( ph -> ( M + K ) e. ( 1 ... N ) )
42 5 11 41 rspcdva
 |-  ( ph -> ( M + K ) || ( _lcm ` ( 1 ... N ) ) )
43 fz1ssnn
 |-  ( 1 ... N ) C_ NN
44 43 7 pm3.2i
 |-  ( ( 1 ... N ) C_ NN /\ ( 1 ... N ) e. Fin )
45 lcmfnncl
 |-  ( ( ( 1 ... N ) C_ NN /\ ( 1 ... N ) e. Fin ) -> ( _lcm ` ( 1 ... N ) ) e. NN )
46 44 45 ax-mp
 |-  ( _lcm ` ( 1 ... N ) ) e. NN
47 46 a1i
 |-  ( ph -> ( _lcm ` ( 1 ... N ) ) e. NN )
48 elfznn0
 |-  ( K e. ( 0 ... ( N - M ) ) -> K e. NN0 )
49 4 48 syl
 |-  ( ph -> K e. NN0 )
50 nnnn0addcl
 |-  ( ( M e. NN /\ K e. NN0 ) -> ( M + K ) e. NN )
51 2 49 50 syl2anc
 |-  ( ph -> ( M + K ) e. NN )
52 nndivdvds
 |-  ( ( ( _lcm ` ( 1 ... N ) ) e. NN /\ ( M + K ) e. NN ) -> ( ( M + K ) || ( _lcm ` ( 1 ... N ) ) <-> ( ( _lcm ` ( 1 ... N ) ) / ( M + K ) ) e. NN ) )
53 47 51 52 syl2anc
 |-  ( ph -> ( ( M + K ) || ( _lcm ` ( 1 ... N ) ) <-> ( ( _lcm ` ( 1 ... N ) ) / ( M + K ) ) e. NN ) )
54 42 53 mpbid
 |-  ( ph -> ( ( _lcm ` ( 1 ... N ) ) / ( M + K ) ) e. NN )
55 54 nnzd
 |-  ( ph -> ( ( _lcm ` ( 1 ... N ) ) / ( M + K ) ) e. ZZ )