Metamath Proof Explorer

Theorem hashfz

Description: Value of the numeric cardinality of a nonempty integer range. (Contributed by Stefan O'Rear, 12-Sep-2014) (Proof shortened by Mario Carneiro, 15-Apr-2015)

Ref Expression
Assertion hashfz 
|- ( B e. ( ZZ>= ` A ) -> ( # ` ( A ... B ) ) = ( ( B - A ) + 1 ) )

Proof

Step Hyp Ref Expression
1 eluzel2 
 |-  ( B e. ( ZZ>= ` A ) -> A e. ZZ )
2 eluzelz 
 |-  ( B e. ( ZZ>= ` A ) -> B e. ZZ )
3 1z 
 |-  1 e. ZZ
4 zsubcl 
 |-  ( ( 1 e. ZZ /\ A e. ZZ ) -> ( 1 - A ) e. ZZ )
5 3 1 4 sylancr 
 |-  ( B e. ( ZZ>= ` A ) -> ( 1 - A ) e. ZZ )
6 fzen 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ ( 1 - A ) e. ZZ ) -> ( A ... B ) ~~ ( ( A + ( 1 - A ) ) ... ( B + ( 1 - A ) ) ) )
7 1 2 5 6 syl3anc 
 |-  ( B e. ( ZZ>= ` A ) -> ( A ... B ) ~~ ( ( A + ( 1 - A ) ) ... ( B + ( 1 - A ) ) ) )
8 1 zcnd 
 |-  ( B e. ( ZZ>= ` A ) -> A e. CC )
9 ax-1cn 
 |-  1 e. CC
10 pncan3 
 |-  ( ( A e. CC /\ 1 e. CC ) -> ( A + ( 1 - A ) ) = 1 )
11 8 9 10 sylancl 
 |-  ( B e. ( ZZ>= ` A ) -> ( A + ( 1 - A ) ) = 1 )
12 1cnd 
 |-  ( B e. ( ZZ>= ` A ) -> 1 e. CC )
13 2 zcnd 
 |-  ( B e. ( ZZ>= ` A ) -> B e. CC )
14 13 8 subcld 
 |-  ( B e. ( ZZ>= ` A ) -> ( B - A ) e. CC )
15 13 12 8 addsub12d 
 |-  ( B e. ( ZZ>= ` A ) -> ( B + ( 1 - A ) ) = ( 1 + ( B - A ) ) )
16 12 14 15 comraddd 
 |-  ( B e. ( ZZ>= ` A ) -> ( B + ( 1 - A ) ) = ( ( B - A ) + 1 ) )
17 11 16 oveq12d 
 |-  ( B e. ( ZZ>= ` A ) -> ( ( A + ( 1 - A ) ) ... ( B + ( 1 - A ) ) ) = ( 1 ... ( ( B - A ) + 1 ) ) )
18 7 17 breqtrd 
 |-  ( B e. ( ZZ>= ` A ) -> ( A ... B ) ~~ ( 1 ... ( ( B - A ) + 1 ) ) )
19 hasheni 
 |-  ( ( A ... B ) ~~ ( 1 ... ( ( B - A ) + 1 ) ) -> ( # ` ( A ... B ) ) = ( # ` ( 1 ... ( ( B - A ) + 1 ) ) ) )
20 18 19 syl 
 |-  ( B e. ( ZZ>= ` A ) -> ( # ` ( A ... B ) ) = ( # ` ( 1 ... ( ( B - A ) + 1 ) ) ) )
21 uznn0sub 
 |-  ( B e. ( ZZ>= ` A ) -> ( B - A ) e. NN0 )
22 peano2nn0 
 |-  ( ( B - A ) e. NN0 -> ( ( B - A ) + 1 ) e. NN0 )
23 hashfz1 
 |-  ( ( ( B - A ) + 1 ) e. NN0 -> ( # ` ( 1 ... ( ( B - A ) + 1 ) ) ) = ( ( B - A ) + 1 ) )
24 21 22 23 3syl 
 |-  ( B e. ( ZZ>= ` A ) -> ( # ` ( 1 ... ( ( B - A ) + 1 ) ) ) = ( ( B - A ) + 1 ) )
25 20 24 eqtrd 
 |-  ( B e. ( ZZ>= ` A ) -> ( # ` ( A ... B ) ) = ( ( B - A ) + 1 ) )