Theorem blen1

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

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

Proof

Step	Hyp	Ref	Expression
1		1nn	|- 1 e. NN
2		blennn	|- ( 1 e. NN -> ( #b ` 1 ) = ( ( |_ ` ( 2 logb 1 ) ) + 1 ) )
3		2cn	|- 2 e. CC
4		2ne0	|- 2 =/= 0
5		1ne2	|- 1 =/= 2
6	5	necomi	|- 2 =/= 1
7		logb1	|- ( ( 2 e. CC /\ 2 =/= 0 /\ 2 =/= 1 ) -> ( 2 logb 1 ) = 0 )
8	3 4 6 7	mp3an	|- ( 2 logb 1 ) = 0
9	8	fveq2i	|- ( |_ ` ( 2 logb 1 ) ) = ( |_ ` 0 )
10		0z	|- 0 e. ZZ
11		flid	|- ( 0 e. ZZ -> ( |_ ` 0 ) = 0 )
12	10 11	ax-mp	|- ( |_ ` 0 ) = 0
13	9 12	eqtri	|- ( |_ ` ( 2 logb 1 ) ) = 0
14	13	a1i	|- ( 1 e. NN -> ( |_ ` ( 2 logb 1 ) ) = 0 )
15	14	oveq1d	|- ( 1 e. NN -> ( ( |_ ` ( 2 logb 1 ) ) + 1 ) = ( 0 + 1 ) )
16		0p1e1	|- ( 0 + 1 ) = 1
17	15 16	eqtrdi	|- ( 1 e. NN -> ( ( |_ ` ( 2 logb 1 ) ) + 1 ) = 1 )
18	2 17	eqtrd	|- ( 1 e. NN -> ( #b ` 1 ) = 1 )
19	1 18	ax-mp	|- ( #b ` 1 ) = 1