Metamath Proof Explorer

Theorem blenn0

Description: The binary length of a "number" not being 0. (Contributed by AV, 20-May-2020)

		Ref	Expression
	Assertion	blenn0	\|- ( ( N e. V /\ N =/= 0 ) -> ( #b ` N ) = ( ( \|_ ` ( 2 logb ( abs ` N ) ) ) + 1 ) )

Step	Hyp	Ref	Expression
1		blenval	\|- ( N e. V -> ( #b ` N ) = if ( N = 0 , 1 , ( ( \|_ ` ( 2 logb ( abs ` N ) ) ) + 1 ) ) )
2		ifnefalse	\|- ( N =/= 0 -> if ( N = 0 , 1 , ( ( \|_ ` ( 2 logb ( abs ` N ) ) ) + 1 ) ) = ( ( \|_ ` ( 2 logb ( abs ` N ) ) ) + 1 ) )
3	1 2	sylan9eq	\|- ( ( N e. V /\ N =/= 0 ) -> ( #b ` N ) = ( ( \|_ ` ( 2 logb ( abs ` N ) ) ) + 1 ) )

Step

Hyp

Ref

Expression

 |-  ( N e. V -> ( #b ` N ) = if ( N = 0 , 1 , ( ( |_ ` ( 2 logb ( abs ` N ) ) ) + 1 ) ) )

 |-  ( N =/= 0 -> if ( N = 0 , 1 , ( ( |_ ` ( 2 logb ( abs ` N ) ) ) + 1 ) ) = ( ( |_ ` ( 2 logb ( abs ` N ) ) ) + 1 ) )

1 2

 |-  ( ( N e. V /\ N =/= 0 ) -> ( #b ` N ) = ( ( |_ ` ( 2 logb ( abs ` N ) ) ) + 1 ) )