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 ∈ ℕ
2		blennn	⊢ ( 2 ∈ ℕ → ( #b ‘ 2 ) = ( ( ⌊ ‘ ( 2 logb 2 ) ) + 1 ) )
3		2cn	⊢ 2 ∈ ℂ
4		2ne0	⊢ 2 ≠ 0
5		1ne2	⊢ 1 ≠ 2
6	5	necomi	⊢ 2 ≠ 1
7		logbid1	⊢ ( ( 2 ∈ ℂ ∧ 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 ∈ ℤ
11		flid	⊢ ( 1 ∈ ℤ → ( ⌊ ‘ 1 ) = 1 )
12	10 11	ax-mp	⊢ ( ⌊ ‘ 1 ) = 1
13	9 12	eqtri	⊢ ( ⌊ ‘ ( 2 logb 2 ) ) = 1
14	13	a1i	⊢ ( 2 ∈ ℕ → ( ⌊ ‘ ( 2 logb 2 ) ) = 1 )
15	14	oveq1d	⊢ ( 2 ∈ ℕ → ( ( ⌊ ‘ ( 2 logb 2 ) ) + 1 ) = ( 1 + 1 ) )
16		1p1e2	⊢ ( 1 + 1 ) = 2
17	16	a1i	⊢ ( 2 ∈ ℕ → ( 1 + 1 ) = 2 )
18	2 15 17	3eqtrd	⊢ ( 2 ∈ ℕ → ( #b ‘ 2 ) = 2 )
19	1 18	ax-mp	⊢ ( #b ‘ 2 ) = 2