Metamath Proof Explorer

Theorem dig2nn0ld

Description: The leading digits of a positive integer in a binary system are 0. (Contributed by AV, 25-May-2020)

Ref Expression
Assertion dig2nn0ld 
|- ( ( N e. NN /\ K e. ( ZZ>= ` ( #b ` N ) ) ) -> ( K ( digit ` 2 ) N ) = 0 )

Proof

Step Hyp Ref Expression
1 2z 
 |-  2 e. ZZ
2 uzid 
 |-  ( 2 e. ZZ -> 2 e. ( ZZ>= ` 2 ) )
3 1 2 mp1i 
 |-  ( ( N e. NN /\ K e. ( ZZ>= ` ( #b ` N ) ) ) -> 2 e. ( ZZ>= ` 2 ) )
4 simpl 
 |-  ( ( N e. NN /\ K e. ( ZZ>= ` ( #b ` N ) ) ) -> N e. NN )
5 blennn 
 |-  ( N e. NN -> ( #b ` N ) = ( ( |_ ` ( 2 logb N ) ) + 1 ) )
6 5 fveq2d 
 |-  ( N e. NN -> ( ZZ>= ` ( #b ` N ) ) = ( ZZ>= ` ( ( |_ ` ( 2 logb N ) ) + 1 ) ) )
7 6 eleq2d 
 |-  ( N e. NN -> ( K e. ( ZZ>= ` ( #b ` N ) ) <-> K e. ( ZZ>= ` ( ( |_ ` ( 2 logb N ) ) + 1 ) ) ) )
8 7 biimpa 
 |-  ( ( N e. NN /\ K e. ( ZZ>= ` ( #b ` N ) ) ) -> K e. ( ZZ>= ` ( ( |_ ` ( 2 logb N ) ) + 1 ) ) )
9 dignnld 
 |-  ( ( 2 e. ( ZZ>= ` 2 ) /\ N e. NN /\ K e. ( ZZ>= ` ( ( |_ ` ( 2 logb N ) ) + 1 ) ) ) -> ( K ( digit ` 2 ) N ) = 0 )
10 3 4 8 9 syl3anc 
 |-  ( ( N e. NN /\ K e. ( ZZ>= ` ( #b ` N ) ) ) -> ( K ( digit ` 2 ) N ) = 0 )