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 ∈ V
2		blenval	⊢ ( 0 ∈ 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