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