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 addridd 
 |-  ( 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 )