Metamath Proof Explorer

Theorem blenre

Description: The binary length of a positive real number. (Contributed by AV, 20-May-2020)

Ref Expression
Assertion blenre 
|- ( N e. RR+ -> ( #b ` N ) = ( ( |_ ` ( 2 logb N ) ) + 1 ) )

Proof

Step Hyp Ref Expression
1 rpne0 
 |-  ( N e. RR+ -> N =/= 0 )
2 blenn0 
 |-  ( ( N e. RR+ /\ N =/= 0 ) -> ( #b ` N ) = ( ( |_ ` ( 2 logb ( abs ` N ) ) ) + 1 ) )
3 1 2 mpdan 
 |-  ( N e. RR+ -> ( #b ` N ) = ( ( |_ ` ( 2 logb ( abs ` N ) ) ) + 1 ) )
4 rpre 
 |-  ( N e. RR+ -> N e. RR )
5 rpge0 
 |-  ( N e. RR+ -> 0 <_ N )
6 4 5 absidd 
 |-  ( N e. RR+ -> ( abs ` N ) = N )
7 6 oveq2d 
 |-  ( N e. RR+ -> ( 2 logb ( abs ` N ) ) = ( 2 logb N ) )
8 7 fveq2d 
 |-  ( N e. RR+ -> ( |_ ` ( 2 logb ( abs ` N ) ) ) = ( |_ ` ( 2 logb N ) ) )
9 8 oveq1d 
 |-  ( N e. RR+ -> ( ( |_ ` ( 2 logb ( abs ` N ) ) ) + 1 ) = ( ( |_ ` ( 2 logb N ) ) + 1 ) )
10 3 9 eqtrd 
 |-  ( N e. RR+ -> ( #b ` N ) = ( ( |_ ` ( 2 logb N ) ) + 1 ) )