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