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 \in V \land N \neq 0) \to #_{b(N)=⌊\log_{2} \|N\|⌋ + 1}$

Step	Hyp	Ref	Expression
1		blenval	$⊢ N \in V \to #_{b(N)=if (N = 0, 1, ⌊\log_{2} \|N\|⌋ + 1)}$
2		ifnefalse	$⊢ N \neq 0 \to if (N = 0, 1, ⌊\log_{2} \|N\|⌋ + 1) = ⌊\log_{2} \|N\|⌋ + 1$
3	1 2	sylan9eq	$⊢ (N \in V \land N \neq 0) \to #_{b(N)=⌊\log_{2} \|N\|⌋ + 1}$