Theorem blen0

Description: The binary length of 0. (Contributed by AV, 20-May-2020)

	Ref	Expression
Assertion	blen0	|- ( #b ` 0 ) = 1

Proof

Step	Hyp	Ref	Expression
1		c0ex	|- 0 e. _V
2		blenval	|- ( 0 e. _V -> ( #b ` 0 ) = if ( 0 = 0 , 1 , ( ( |_ ` ( 2 logb ( abs ` 0 ) ) ) + 1 ) ) )
3	1 2	ax-mp	|- ( #b ` 0 ) = if ( 0 = 0 , 1 , ( ( |_ ` ( 2 logb ( abs ` 0 ) ) ) + 1 ) )
4		eqid	|- 0 = 0
5	4	iftruei	|- if ( 0 = 0 , 1 , ( ( |_ ` ( 2 logb ( abs ` 0 ) ) ) + 1 ) ) = 1
6	3 5	eqtri	|- ( #b ` 0 ) = 1