Metamath Proof Explorer

Theorem blennnelnn

Description: The binary length of a positive integer is a positive integer. (Contributed by AV, 25-May-2020)

Ref Expression
Assertion blennnelnn 
|- ( N e. NN -> ( #b ` N ) e. NN )

Proof

Step Hyp Ref Expression
1 blennn 
 |-  ( N e. NN -> ( #b ` N ) = ( ( |_ ` ( 2 logb N ) ) + 1 ) )
2 2rp 
 |-  2 e. RR+
3 2 a1i 
 |-  ( N e. NN -> 2 e. RR+ )
4 nnrp 
 |-  ( N e. NN -> N e. RR+ )
5 1ne2 
 |-  1 =/= 2
6 5 necomi 
 |-  2 =/= 1
7 6 a1i 
 |-  ( N e. NN -> 2 =/= 1 )
8 relogbcl 
 |-  ( ( 2 e. RR+ /\ N e. RR+ /\ 2 =/= 1 ) -> ( 2 logb N ) e. RR )
9 3 4 7 8 syl3anc 
 |-  ( N e. NN -> ( 2 logb N ) e. RR )
10 2z 
 |-  2 e. ZZ
11 uzid 
 |-  ( 2 e. ZZ -> 2 e. ( ZZ>= ` 2 ) )
12 10 11 mp1i 
 |-  ( N e. NN -> 2 e. ( ZZ>= ` 2 ) )
13 nnre 
 |-  ( N e. NN -> N e. RR )
14 nnge1 
 |-  ( N e. NN -> 1 <_ N )
15 1re 
 |-  1 e. RR
16 elicopnf 
 |-  ( 1 e. RR -> ( N e. ( 1 [,) +oo ) <-> ( N e. RR /\ 1 <_ N ) ) )
17 15 16 ax-mp 
 |-  ( N e. ( 1 [,) +oo ) <-> ( N e. RR /\ 1 <_ N ) )
18 13 14 17 sylanbrc 
 |-  ( N e. NN -> N e. ( 1 [,) +oo ) )
19 rege1logbzge0 
 |-  ( ( 2 e. ( ZZ>= ` 2 ) /\ N e. ( 1 [,) +oo ) ) -> 0 <_ ( 2 logb N ) )
20 12 18 19 syl2anc 
 |-  ( N e. NN -> 0 <_ ( 2 logb N ) )
21 flge0nn0 
 |-  ( ( ( 2 logb N ) e. RR /\ 0 <_ ( 2 logb N ) ) -> ( |_ ` ( 2 logb N ) ) e. NN0 )
22 9 20 21 syl2anc 
 |-  ( N e. NN -> ( |_ ` ( 2 logb N ) ) e. NN0 )
23 nn0p1nn 
 |-  ( ( |_ ` ( 2 logb N ) ) e. NN0 -> ( ( |_ ` ( 2 logb N ) ) + 1 ) e. NN )
24 22 23 syl 
 |-  ( N e. NN -> ( ( |_ ` ( 2 logb N ) ) + 1 ) e. NN )
25 1 24 eqeltrd 
 |-  ( N e. NN -> ( #b ` N ) e. NN )