Metamath Proof Explorer

Theorem hashfz0

Description: Value of the numeric cardinality of a nonempty range of nonnegative integers. (Contributed by Alexander van der Vekens, 21-Jul-2018)

Ref Expression
Assertion hashfz0 
|- ( B e. NN0 -> ( # ` ( 0 ... B ) ) = ( B + 1 ) )

Proof

Step Hyp Ref Expression
1 elnn0uz 
 |-  ( B e. NN0 <-> B e. ( ZZ>= ` 0 ) )
2 hashfz 
 |-  ( B e. ( ZZ>= ` 0 ) -> ( # ` ( 0 ... B ) ) = ( ( B - 0 ) + 1 ) )
3 1 2 sylbi 
 |-  ( B e. NN0 -> ( # ` ( 0 ... B ) ) = ( ( B - 0 ) + 1 ) )
4 nn0cn 
 |-  ( B e. NN0 -> B e. CC )
5 4 subid1d 
 |-  ( B e. NN0 -> ( B - 0 ) = B )
6 5 oveq1d 
 |-  ( B e. NN0 -> ( ( B - 0 ) + 1 ) = ( B + 1 ) )
7 3 6 eqtrd 
 |-  ( B e. NN0 -> ( # ` ( 0 ... B ) ) = ( B + 1 ) )