Metamath Proof Explorer

Theorem hashfzo

Description: Cardinality of a half-open set of integers. (Contributed by Stefan O'Rear, 15-Aug-2015)

Ref Expression
Assertion hashfzo 
|- ( B e. ( ZZ>= ` A ) -> ( # ` ( A ..^ B ) ) = ( B - A ) )

Proof

Step Hyp Ref Expression
1 fzo0 
 |-  ( A ..^ A ) = (/)
2 1 fveq2i 
 |-  ( # ` ( A ..^ A ) ) = ( # ` (/) )
3 hash0 
 |-  ( # ` (/) ) = 0
4 2 3 eqtri 
 |-  ( # ` ( A ..^ A ) ) = 0
5 eluzel2 
 |-  ( B e. ( ZZ>= ` A ) -> A e. ZZ )
6 5 zcnd 
 |-  ( B e. ( ZZ>= ` A ) -> A e. CC )
7 6 subidd 
 |-  ( B e. ( ZZ>= ` A ) -> ( A - A ) = 0 )
8 4 7 eqtr4id 
 |-  ( B e. ( ZZ>= ` A ) -> ( # ` ( A ..^ A ) ) = ( A - A ) )
9 oveq2 
 |-  ( B = A -> ( A ..^ B ) = ( A ..^ A ) )
10 9 fveq2d 
 |-  ( B = A -> ( # ` ( A ..^ B ) ) = ( # ` ( A ..^ A ) ) )
11 oveq1 
 |-  ( B = A -> ( B - A ) = ( A - A ) )
12 10 11 eqeq12d 
 |-  ( B = A -> ( ( # ` ( A ..^ B ) ) = ( B - A ) <-> ( # ` ( A ..^ A ) ) = ( A - A ) ) )
13 8 12 syl5ibrcom 
 |-  ( B e. ( ZZ>= ` A ) -> ( B = A -> ( # ` ( A ..^ B ) ) = ( B - A ) ) )
14 eluzelz 
 |-  ( B e. ( ZZ>= ` A ) -> B e. ZZ )
15 fzoval 
 |-  ( B e. ZZ -> ( A ..^ B ) = ( A ... ( B - 1 ) ) )
16 14 15 syl 
 |-  ( B e. ( ZZ>= ` A ) -> ( A ..^ B ) = ( A ... ( B - 1 ) ) )
17 16 fveq2d 
 |-  ( B e. ( ZZ>= ` A ) -> ( # ` ( A ..^ B ) ) = ( # ` ( A ... ( B - 1 ) ) ) )
18 17 adantr 
 |-  ( ( B e. ( ZZ>= ` A ) /\ ( B - 1 ) e. ( ZZ>= ` A ) ) -> ( # ` ( A ..^ B ) ) = ( # ` ( A ... ( B - 1 ) ) ) )
19 hashfz 
 |-  ( ( B - 1 ) e. ( ZZ>= ` A ) -> ( # ` ( A ... ( B - 1 ) ) ) = ( ( ( B - 1 ) - A ) + 1 ) )
20 14 zcnd 
 |-  ( B e. ( ZZ>= ` A ) -> B e. CC )
21 1cnd 
 |-  ( B e. ( ZZ>= ` A ) -> 1 e. CC )
22 20 21 6 sub32d 
 |-  ( B e. ( ZZ>= ` A ) -> ( ( B - 1 ) - A ) = ( ( B - A ) - 1 ) )
23 22 oveq1d 
 |-  ( B e. ( ZZ>= ` A ) -> ( ( ( B - 1 ) - A ) + 1 ) = ( ( ( B - A ) - 1 ) + 1 ) )
24 20 6 subcld 
 |-  ( B e. ( ZZ>= ` A ) -> ( B - A ) e. CC )
25 ax-1cn 
 |-  1 e. CC
26 npcan 
 |-  ( ( ( B - A ) e. CC /\ 1 e. CC ) -> ( ( ( B - A ) - 1 ) + 1 ) = ( B - A ) )
27 24 25 26 sylancl 
 |-  ( B e. ( ZZ>= ` A ) -> ( ( ( B - A ) - 1 ) + 1 ) = ( B - A ) )
28 23 27 eqtrd 
 |-  ( B e. ( ZZ>= ` A ) -> ( ( ( B - 1 ) - A ) + 1 ) = ( B - A ) )
29 19 28 sylan9eqr 
 |-  ( ( B e. ( ZZ>= ` A ) /\ ( B - 1 ) e. ( ZZ>= ` A ) ) -> ( # ` ( A ... ( B - 1 ) ) ) = ( B - A ) )
30 18 29 eqtrd 
 |-  ( ( B e. ( ZZ>= ` A ) /\ ( B - 1 ) e. ( ZZ>= ` A ) ) -> ( # ` ( A ..^ B ) ) = ( B - A ) )
31 30 ex 
 |-  ( B e. ( ZZ>= ` A ) -> ( ( B - 1 ) e. ( ZZ>= ` A ) -> ( # ` ( A ..^ B ) ) = ( B - A ) ) )
32 uzm1 
 |-  ( B e. ( ZZ>= ` A ) -> ( B = A \/ ( B - 1 ) e. ( ZZ>= ` A ) ) )
33 13 31 32 mpjaod 
 |-  ( B e. ( ZZ>= ` A ) -> ( # ` ( A ..^ B ) ) = ( B - A ) )