Theorem blengt1fldiv2p1

Description: The binary length of an integer greater than 1 is the binary length of the integer divided by 2, increased by one. (Contributed by AV, 3-Jun-2020)

	Ref	Expression
Assertion	blengt1fldiv2p1	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( #b ‘ 𝑁 ) = ( ( #b ‘ ( ⌊ ‘ ( 𝑁 / 2 ) ) ) + 1 ) )

Proof

Step	Hyp	Ref	Expression
1		eluz2nn	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 𝑁 ∈ ℕ )
2		nneop	⊢ ( 𝑁 ∈ ℕ → ( ( 𝑁 / 2 ) ∈ ℕ ∨ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ ) )
3	1 2	syl	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( ( 𝑁 / 2 ) ∈ ℕ ∨ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ ) )
4		nnnn0	⊢ ( ( 𝑁 / 2 ) ∈ ℕ → ( 𝑁 / 2 ) ∈ ℕ0 )
5		blennn0em1	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑁 / 2 ) ∈ ℕ0 ) → ( #b ‘ ( 𝑁 / 2 ) ) = ( ( #b ‘ 𝑁 ) − 1 ) )
6	4 5	sylan2	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑁 / 2 ) ∈ ℕ ) → ( #b ‘ ( 𝑁 / 2 ) ) = ( ( #b ‘ 𝑁 ) − 1 ) )
7	6	ancoms	⊢ ( ( ( 𝑁 / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( #b ‘ ( 𝑁 / 2 ) ) = ( ( #b ‘ 𝑁 ) − 1 ) )
8	7	oveq1d	⊢ ( ( ( 𝑁 / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( #b ‘ ( 𝑁 / 2 ) ) + 1 ) = ( ( ( #b ‘ 𝑁 ) − 1 ) + 1 ) )
9		nnz	⊢ ( ( 𝑁 / 2 ) ∈ ℕ → ( 𝑁 / 2 ) ∈ ℤ )
10		flid	⊢ ( ( 𝑁 / 2 ) ∈ ℤ → ( ⌊ ‘ ( 𝑁 / 2 ) ) = ( 𝑁 / 2 ) )
11	9 10	syl	⊢ ( ( 𝑁 / 2 ) ∈ ℕ → ( ⌊ ‘ ( 𝑁 / 2 ) ) = ( 𝑁 / 2 ) )
12	11	eqcomd	⊢ ( ( 𝑁 / 2 ) ∈ ℕ → ( 𝑁 / 2 ) = ( ⌊ ‘ ( 𝑁 / 2 ) ) )
13	12	fveq2d	⊢ ( ( 𝑁 / 2 ) ∈ ℕ → ( #b ‘ ( 𝑁 / 2 ) ) = ( #b ‘ ( ⌊ ‘ ( 𝑁 / 2 ) ) ) )
14	13	oveq1d	⊢ ( ( 𝑁 / 2 ) ∈ ℕ → ( ( #b ‘ ( 𝑁 / 2 ) ) + 1 ) = ( ( #b ‘ ( ⌊ ‘ ( 𝑁 / 2 ) ) ) + 1 ) )
15	14	adantr	⊢ ( ( ( 𝑁 / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( #b ‘ ( 𝑁 / 2 ) ) + 1 ) = ( ( #b ‘ ( ⌊ ‘ ( 𝑁 / 2 ) ) ) + 1 ) )
16		blennnelnn	⊢ ( 𝑁 ∈ ℕ → ( #b ‘ 𝑁 ) ∈ ℕ )
17	16	nncnd	⊢ ( 𝑁 ∈ ℕ → ( #b ‘ 𝑁 ) ∈ ℂ )
18		npcan1	⊢ ( ( #b ‘ 𝑁 ) ∈ ℂ → ( ( ( #b ‘ 𝑁 ) − 1 ) + 1 ) = ( #b ‘ 𝑁 ) )
19	17 18	syl	⊢ ( 𝑁 ∈ ℕ → ( ( ( #b ‘ 𝑁 ) − 1 ) + 1 ) = ( #b ‘ 𝑁 ) )
20	19	adantl	⊢ ( ( ( 𝑁 / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( ( ( #b ‘ 𝑁 ) − 1 ) + 1 ) = ( #b ‘ 𝑁 ) )
21	8 15 20	3eqtr3rd	⊢ ( ( ( 𝑁 / 2 ) ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( #b ‘ 𝑁 ) = ( ( #b ‘ ( ⌊ ‘ ( 𝑁 / 2 ) ) ) + 1 ) )
22	21	expcom	⊢ ( 𝑁 ∈ ℕ → ( ( 𝑁 / 2 ) ∈ ℕ → ( #b ‘ 𝑁 ) = ( ( #b ‘ ( ⌊ ‘ ( 𝑁 / 2 ) ) ) + 1 ) ) )
23	22 1	syl11	⊢ ( ( 𝑁 / 2 ) ∈ ℕ → ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( #b ‘ 𝑁 ) = ( ( #b ‘ ( ⌊ ‘ ( 𝑁 / 2 ) ) ) + 1 ) ) )
24		nnnn0	⊢ ( ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ → ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 )
25		blennngt2o2	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 ) → ( #b ‘ 𝑁 ) = ( ( #b ‘ ( ( 𝑁 − 1 ) / 2 ) ) + 1 ) )
26	24 25	sylan2	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ ) → ( #b ‘ 𝑁 ) = ( ( #b ‘ ( ( 𝑁 − 1 ) / 2 ) ) + 1 ) )
27	26	ancoms	⊢ ( ( ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( #b ‘ 𝑁 ) = ( ( #b ‘ ( ( 𝑁 − 1 ) / 2 ) ) + 1 ) )
28		eluzge2nn0	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → 𝑁 ∈ ℕ0 )
29		nn0ofldiv2	⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ0 ) → ( ⌊ ‘ ( 𝑁 / 2 ) ) = ( ( 𝑁 − 1 ) / 2 ) )
30	28 24 29	syl2anr	⊢ ( ( ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( ⌊ ‘ ( 𝑁 / 2 ) ) = ( ( 𝑁 − 1 ) / 2 ) )
31	30	eqcomd	⊢ ( ( ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( 𝑁 − 1 ) / 2 ) = ( ⌊ ‘ ( 𝑁 / 2 ) ) )
32	31	fveq2d	⊢ ( ( ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( #b ‘ ( ( 𝑁 − 1 ) / 2 ) ) = ( #b ‘ ( ⌊ ‘ ( 𝑁 / 2 ) ) ) )
33	32	oveq1d	⊢ ( ( ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( #b ‘ ( ( 𝑁 − 1 ) / 2 ) ) + 1 ) = ( ( #b ‘ ( ⌊ ‘ ( 𝑁 / 2 ) ) ) + 1 ) )
34	27 33	eqtrd	⊢ ( ( ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ ∧ 𝑁 ∈ ( ℤ≥ ‘ 2 ) ) → ( #b ‘ 𝑁 ) = ( ( #b ‘ ( ⌊ ‘ ( 𝑁 / 2 ) ) ) + 1 ) )
35	34	ex	⊢ ( ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ → ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( #b ‘ 𝑁 ) = ( ( #b ‘ ( ⌊ ‘ ( 𝑁 / 2 ) ) ) + 1 ) ) )
36	23 35	jaoi	⊢ ( ( ( 𝑁 / 2 ) ∈ ℕ ∨ ( ( 𝑁 + 1 ) / 2 ) ∈ ℕ ) → ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( #b ‘ 𝑁 ) = ( ( #b ‘ ( ⌊ ‘ ( 𝑁 / 2 ) ) ) + 1 ) ) )
37	3 36	mpcom	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) → ( #b ‘ 𝑁 ) = ( ( #b ‘ ( ⌊ ‘ ( 𝑁 / 2 ) ) ) + 1 ) )