Theorem blen2

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

	Ref	Expression
Assertion	blen2	|- ( #b ` 2 ) = 2

Proof

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