Step |
Hyp |
Ref |
Expression |
1 |
|
eluzelz |
|- ( B e. ( ZZ>= ` A ) -> B e. ZZ ) |
2 |
1
|
ad2antrr |
|- ( ( ( B e. ( ZZ>= ` A ) /\ C e. ZZ ) /\ B < C ) -> B e. ZZ ) |
3 |
2
|
zred |
|- ( ( ( B e. ( ZZ>= ` A ) /\ C e. ZZ ) /\ B < C ) -> B e. RR ) |
4 |
|
eluzel2 |
|- ( B e. ( ZZ>= ` A ) -> A e. ZZ ) |
5 |
4
|
ad2antrr |
|- ( ( ( B e. ( ZZ>= ` A ) /\ C e. ZZ ) /\ B < C ) -> A e. ZZ ) |
6 |
5
|
zred |
|- ( ( ( B e. ( ZZ>= ` A ) /\ C e. ZZ ) /\ B < C ) -> A e. RR ) |
7 |
3 6
|
resubcld |
|- ( ( ( B e. ( ZZ>= ` A ) /\ C e. ZZ ) /\ B < C ) -> ( B - A ) e. RR ) |
8 |
|
simplr |
|- ( ( ( B e. ( ZZ>= ` A ) /\ C e. ZZ ) /\ B < C ) -> C e. ZZ ) |
9 |
8
|
zred |
|- ( ( ( B e. ( ZZ>= ` A ) /\ C e. ZZ ) /\ B < C ) -> C e. RR ) |
10 |
9 6
|
resubcld |
|- ( ( ( B e. ( ZZ>= ` A ) /\ C e. ZZ ) /\ B < C ) -> ( C - A ) e. RR ) |
11 |
|
1red |
|- ( ( ( B e. ( ZZ>= ` A ) /\ C e. ZZ ) /\ B < C ) -> 1 e. RR ) |
12 |
|
simpr |
|- ( ( ( B e. ( ZZ>= ` A ) /\ C e. ZZ ) /\ B < C ) -> B < C ) |
13 |
3 9 6 12
|
ltsub1dd |
|- ( ( ( B e. ( ZZ>= ` A ) /\ C e. ZZ ) /\ B < C ) -> ( B - A ) < ( C - A ) ) |
14 |
7 10 11 13
|
ltadd1dd |
|- ( ( ( B e. ( ZZ>= ` A ) /\ C e. ZZ ) /\ B < C ) -> ( ( B - A ) + 1 ) < ( ( C - A ) + 1 ) ) |
15 |
|
hashfz |
|- ( B e. ( ZZ>= ` A ) -> ( # ` ( A ... B ) ) = ( ( B - A ) + 1 ) ) |
16 |
15
|
ad2antrr |
|- ( ( ( B e. ( ZZ>= ` A ) /\ C e. ZZ ) /\ B < C ) -> ( # ` ( A ... B ) ) = ( ( B - A ) + 1 ) ) |
17 |
3 9 12
|
ltled |
|- ( ( ( B e. ( ZZ>= ` A ) /\ C e. ZZ ) /\ B < C ) -> B <_ C ) |
18 |
|
eluz2 |
|- ( C e. ( ZZ>= ` B ) <-> ( B e. ZZ /\ C e. ZZ /\ B <_ C ) ) |
19 |
2 8 17 18
|
syl3anbrc |
|- ( ( ( B e. ( ZZ>= ` A ) /\ C e. ZZ ) /\ B < C ) -> C e. ( ZZ>= ` B ) ) |
20 |
|
simpll |
|- ( ( ( B e. ( ZZ>= ` A ) /\ C e. ZZ ) /\ B < C ) -> B e. ( ZZ>= ` A ) ) |
21 |
|
uztrn |
|- ( ( C e. ( ZZ>= ` B ) /\ B e. ( ZZ>= ` A ) ) -> C e. ( ZZ>= ` A ) ) |
22 |
19 20 21
|
syl2anc |
|- ( ( ( B e. ( ZZ>= ` A ) /\ C e. ZZ ) /\ B < C ) -> C e. ( ZZ>= ` A ) ) |
23 |
|
hashfz |
|- ( C e. ( ZZ>= ` A ) -> ( # ` ( A ... C ) ) = ( ( C - A ) + 1 ) ) |
24 |
22 23
|
syl |
|- ( ( ( B e. ( ZZ>= ` A ) /\ C e. ZZ ) /\ B < C ) -> ( # ` ( A ... C ) ) = ( ( C - A ) + 1 ) ) |
25 |
14 16 24
|
3brtr4d |
|- ( ( ( B e. ( ZZ>= ` A ) /\ C e. ZZ ) /\ B < C ) -> ( # ` ( A ... B ) ) < ( # ` ( A ... C ) ) ) |
26 |
|
fzfi |
|- ( A ... B ) e. Fin |
27 |
|
fzfi |
|- ( A ... C ) e. Fin |
28 |
|
hashsdom |
|- ( ( ( A ... B ) e. Fin /\ ( A ... C ) e. Fin ) -> ( ( # ` ( A ... B ) ) < ( # ` ( A ... C ) ) <-> ( A ... B ) ~< ( A ... C ) ) ) |
29 |
26 27 28
|
mp2an |
|- ( ( # ` ( A ... B ) ) < ( # ` ( A ... C ) ) <-> ( A ... B ) ~< ( A ... C ) ) |
30 |
25 29
|
sylib |
|- ( ( ( B e. ( ZZ>= ` A ) /\ C e. ZZ ) /\ B < C ) -> ( A ... B ) ~< ( A ... C ) ) |