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