Metamath Proof Explorer

Theorem hashfzp1

Description: Value of the numeric cardinality of a (possibly empty) integer range. (Contributed by AV, 19-Jun-2021)

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

Proof

Step Hyp Ref Expression
1 hash0 
 |-  ( # ` (/) ) = 0
2 eluzelre 
 |-  ( B e. ( ZZ>= ` A ) -> B e. RR )
3 2 ltp1d 
 |-  ( B e. ( ZZ>= ` A ) -> B < ( B + 1 ) )
4 eluzelz 
 |-  ( B e. ( ZZ>= ` A ) -> B e. ZZ )
5 peano2z 
 |-  ( B e. ZZ -> ( B + 1 ) e. ZZ )
6 5 ancri 
 |-  ( B e. ZZ -> ( ( B + 1 ) e. ZZ /\ B e. ZZ ) )
7 fzn 
 |-  ( ( ( B + 1 ) e. ZZ /\ B e. ZZ ) -> ( B < ( B + 1 ) <-> ( ( B + 1 ) ... B ) = (/) ) )
8 4 6 7 3syl 
 |-  ( B e. ( ZZ>= ` A ) -> ( B < ( B + 1 ) <-> ( ( B + 1 ) ... B ) = (/) ) )
9 3 8 mpbid 
 |-  ( B e. ( ZZ>= ` A ) -> ( ( B + 1 ) ... B ) = (/) )
10 9 fveq2d 
 |-  ( B e. ( ZZ>= ` A ) -> ( # ` ( ( B + 1 ) ... B ) ) = ( # ` (/) ) )
11 4 zcnd 
 |-  ( B e. ( ZZ>= ` A ) -> B e. CC )
12 11 subidd 
 |-  ( B e. ( ZZ>= ` A ) -> ( B - B ) = 0 )
13 1 10 12 3eqtr4a 
 |-  ( B e. ( ZZ>= ` A ) -> ( # ` ( ( B + 1 ) ... B ) ) = ( B - B ) )
14 oveq1 
 |-  ( A = B -> ( A + 1 ) = ( B + 1 ) )
15 14 fvoveq1d 
 |-  ( A = B -> ( # ` ( ( A + 1 ) ... B ) ) = ( # ` ( ( B + 1 ) ... B ) ) )
16 oveq2 
 |-  ( A = B -> ( B - A ) = ( B - B ) )
17 15 16 eqeq12d 
 |-  ( A = B -> ( ( # ` ( ( A + 1 ) ... B ) ) = ( B - A ) <-> ( # ` ( ( B + 1 ) ... B ) ) = ( B - B ) ) )
18 13 17 imbitrrid 
 |-  ( A = B -> ( B e. ( ZZ>= ` A ) -> ( # ` ( ( A + 1 ) ... B ) ) = ( B - A ) ) )
19 uzp1 
 |-  ( B e. ( ZZ>= ` A ) -> ( B = A \/ B e. ( ZZ>= ` ( A + 1 ) ) ) )
20 pm2.24 
 |-  ( A = B -> ( -. A = B -> B e. ( ZZ>= ` ( A + 1 ) ) ) )
21 20 eqcoms 
 |-  ( B = A -> ( -. A = B -> B e. ( ZZ>= ` ( A + 1 ) ) ) )
22 ax-1 
 |-  ( B e. ( ZZ>= ` ( A + 1 ) ) -> ( -. A = B -> B e. ( ZZ>= ` ( A + 1 ) ) ) )
23 21 22 jaoi 
 |-  ( ( B = A \/ B e. ( ZZ>= ` ( A + 1 ) ) ) -> ( -. A = B -> B e. ( ZZ>= ` ( A + 1 ) ) ) )
24 19 23 syl 
 |-  ( B e. ( ZZ>= ` A ) -> ( -. A = B -> B e. ( ZZ>= ` ( A + 1 ) ) ) )
25 24 impcom 
 |-  ( ( -. A = B /\ B e. ( ZZ>= ` A ) ) -> B e. ( ZZ>= ` ( A + 1 ) ) )
26 hashfz 
 |-  ( B e. ( ZZ>= ` ( A + 1 ) ) -> ( # ` ( ( A + 1 ) ... B ) ) = ( ( B - ( A + 1 ) ) + 1 ) )
27 25 26 syl 
 |-  ( ( -. A = B /\ B e. ( ZZ>= ` A ) ) -> ( # ` ( ( A + 1 ) ... B ) ) = ( ( B - ( A + 1 ) ) + 1 ) )
28 eluzel2 
 |-  ( B e. ( ZZ>= ` A ) -> A e. ZZ )
29 28 zcnd 
 |-  ( B e. ( ZZ>= ` A ) -> A e. CC )
30 1cnd 
 |-  ( B e. ( ZZ>= ` A ) -> 1 e. CC )
31 11 29 30 nppcan2d 
 |-  ( B e. ( ZZ>= ` A ) -> ( ( B - ( A + 1 ) ) + 1 ) = ( B - A ) )
32 31 adantl 
 |-  ( ( -. A = B /\ B e. ( ZZ>= ` A ) ) -> ( ( B - ( A + 1 ) ) + 1 ) = ( B - A ) )
33 27 32 eqtrd 
 |-  ( ( -. A = B /\ B e. ( ZZ>= ` A ) ) -> ( # ` ( ( A + 1 ) ... B ) ) = ( B - A ) )
34 33 ex 
 |-  ( -. A = B -> ( B e. ( ZZ>= ` A ) -> ( # ` ( ( A + 1 ) ... B ) ) = ( B - A ) ) )
35 18 34 pm2.61i 
 |-  ( B e. ( ZZ>= ` A ) -> ( # ` ( ( A + 1 ) ... B ) ) = ( B - A ) )