blenval

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

		Ref	Expression
	Assertion	blenval	$⊢ N \in V \to #_{b(N)=if (N = 0, 1, ⌊\log_{2} \|N\|⌋ + 1)}$

Step	Hyp	Ref	Expression
1		df-blen	$⊢ #_{b=(n \in V ⟼ if (n = 0, 1, ⌊\log_{2} \|n\|⌋ + 1))}$
2		eqeq1	$⊢ n = N \to (n = 0 \leftrightarrow N = 0)$
3		fveq2	$⊢ n = N \to \|n\| = \|N\|$
4	3	oveq2d	$⊢ n = N \to \log_{2} \|n\| = \log_{2} \|N\|$
5	4	fveq2d	$⊢ n = N \to ⌊\log_{2} \|n\|⌋ = ⌊\log_{2} \|N\|⌋$
6	5	oveq1d	$⊢ n = N \to ⌊\log_{2} \|n\|⌋ + 1 = ⌊\log_{2} \|N\|⌋ + 1$
7	2 6	ifbieq2d	$⊢ n = N \to if (n = 0, 1, ⌊\log_{2} \|n\|⌋ + 1) = if (N = 0, 1, ⌊\log_{2} \|N\|⌋ + 1)$
8		elex	$⊢ N \in V \to N \in V$
9		1ex	$⊢ 1 \in V$
10		ovex	$⊢ ⌊\log_{2} \|N\|⌋ + 1 \in V$
11	9 10	ifex	$⊢ if (N = 0, 1, ⌊\log_{2} \|N\|⌋ + 1) \in V$
12	11	a1i	$⊢ N \in V \to if (N = 0, 1, ⌊\log_{2} \|N\|⌋ + 1) \in V$
13	1 7 8 12	fvmptd3	$⊢ N \in V \to #_{b(N)=if (N = 0, 1, ⌊\log_{2} \|N\|⌋ + 1)}$

Metamath Proof Explorer