Metamath Proof Explorer


Theorem fzsdom2

Description: Condition for finite ranges to have a strict dominance relation. (Contributed by Stefan O'Rear, 12-Sep-2014) (Revised by Mario Carneiro, 15-Apr-2015)

Ref Expression
Assertion fzsdom2
|- ( ( ( B e. ( ZZ>= ` A ) /\ C e. ZZ ) /\ B < C ) -> ( A ... B ) ~< ( A ... C ) )

Proof

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