Metamath Proof Explorer

Theorem hashfzo0

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

Ref Expression
Assertion hashfzo0 
|- ( B e. NN0 -> ( # ` ( 0 ..^ B ) ) = B )

Proof

Step Hyp Ref Expression
1 hashfzo 
 |-  ( B e. ( ZZ>= ` 0 ) -> ( # ` ( 0 ..^ B ) ) = ( B - 0 ) )
2 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
3 1 2 eleq2s 
 |-  ( B e. NN0 -> ( # ` ( 0 ..^ B ) ) = ( B - 0 ) )
4 nn0cn 
 |-  ( B e. NN0 -> B e. CC )
5 4 subid1d 
 |-  ( B e. NN0 -> ( B - 0 ) = B )
6 3 5 eqtrd 
 |-  ( B e. NN0 -> ( # ` ( 0 ..^ B ) ) = B )