Theorem blennn0e2

Description: The binary length of an even positive integer is the binary length of the half of the integer, increased by 1. (Contributed by AV, 29-May-2020)

	Ref	Expression
Assertion	blennn0e2	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑁 / 2 ) ∈ ℕ0 ) → ( #b ‘ 𝑁 ) = ( ( #b ‘ ( 𝑁 / 2 ) ) + 1 ) )

Proof

Step	Hyp	Ref	Expression
1		2rp	⊢ 2 ∈ ℝ+
2		1ne2	⊢ 1 ≠ 2
3	2	necomi	⊢ 2 ≠ 1
4		eldifsn	⊢ ( 2 ∈ ( ℝ+ ∖ { 1 } ) ↔ ( 2 ∈ ℝ+ ∧ 2 ≠ 1 ) )
5	1 3 4	mpbir2an	⊢ 2 ∈ ( ℝ+ ∖ { 1 } )
6		nnrp	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ+ )
7	6	adantr	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑁 / 2 ) ∈ ℕ0 ) → 𝑁 ∈ ℝ+ )
8		relogbdivb	⊢ ( ( 2 ∈ ( ℝ+ ∖ { 1 } ) ∧ 𝑁 ∈ ℝ+ ) → ( 2 logb ( 𝑁 / 2 ) ) = ( ( 2 logb 𝑁 ) − 1 ) )
9	5 7 8	sylancr	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑁 / 2 ) ∈ ℕ0 ) → ( 2 logb ( 𝑁 / 2 ) ) = ( ( 2 logb 𝑁 ) − 1 ) )
10	9	fveq2d	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑁 / 2 ) ∈ ℕ0 ) → ( ⌊ ‘ ( 2 logb ( 𝑁 / 2 ) ) ) = ( ⌊ ‘ ( ( 2 logb 𝑁 ) − 1 ) ) )
11	10	oveq1d	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑁 / 2 ) ∈ ℕ0 ) → ( ( ⌊ ‘ ( 2 logb ( 𝑁 / 2 ) ) ) + 1 ) = ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) − 1 ) ) + 1 ) )
12	1	a1i	⊢ ( 𝑁 ∈ ℕ → 2 ∈ ℝ+ )
13	3	a1i	⊢ ( 𝑁 ∈ ℕ → 2 ≠ 1 )
14		relogbcl	⊢ ( ( 2 ∈ ℝ+ ∧ 𝑁 ∈ ℝ+ ∧ 2 ≠ 1 ) → ( 2 logb 𝑁 ) ∈ ℝ )
15	12 6 13 14	syl3anc	⊢ ( 𝑁 ∈ ℕ → ( 2 logb 𝑁 ) ∈ ℝ )
16		1zzd	⊢ ( 𝑁 ∈ ℕ → 1 ∈ ℤ )
17	15 16	jca	⊢ ( 𝑁 ∈ ℕ → ( ( 2 logb 𝑁 ) ∈ ℝ ∧ 1 ∈ ℤ ) )
18	17	adantr	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑁 / 2 ) ∈ ℕ0 ) → ( ( 2 logb 𝑁 ) ∈ ℝ ∧ 1 ∈ ℤ ) )
19		flsubz	⊢ ( ( ( 2 logb 𝑁 ) ∈ ℝ ∧ 1 ∈ ℤ ) → ( ⌊ ‘ ( ( 2 logb 𝑁 ) − 1 ) ) = ( ( ⌊ ‘ ( 2 logb 𝑁 ) ) − 1 ) )
20	18 19	syl	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑁 / 2 ) ∈ ℕ0 ) → ( ⌊ ‘ ( ( 2 logb 𝑁 ) − 1 ) ) = ( ( ⌊ ‘ ( 2 logb 𝑁 ) ) − 1 ) )
21	20	oveq1d	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑁 / 2 ) ∈ ℕ0 ) → ( ( ⌊ ‘ ( ( 2 logb 𝑁 ) − 1 ) ) + 1 ) = ( ( ( ⌊ ‘ ( 2 logb 𝑁 ) ) − 1 ) + 1 ) )
22	15	flcld	⊢ ( 𝑁 ∈ ℕ → ( ⌊ ‘ ( 2 logb 𝑁 ) ) ∈ ℤ )
23	22	zcnd	⊢ ( 𝑁 ∈ ℕ → ( ⌊ ‘ ( 2 logb 𝑁 ) ) ∈ ℂ )
24		npcan1	⊢ ( ( ⌊ ‘ ( 2 logb 𝑁 ) ) ∈ ℂ → ( ( ( ⌊ ‘ ( 2 logb 𝑁 ) ) − 1 ) + 1 ) = ( ⌊ ‘ ( 2 logb 𝑁 ) ) )
25	23 24	syl	⊢ ( 𝑁 ∈ ℕ → ( ( ( ⌊ ‘ ( 2 logb 𝑁 ) ) − 1 ) + 1 ) = ( ⌊ ‘ ( 2 logb 𝑁 ) ) )
26	25	adantr	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑁 / 2 ) ∈ ℕ0 ) → ( ( ( ⌊ ‘ ( 2 logb 𝑁 ) ) − 1 ) + 1 ) = ( ⌊ ‘ ( 2 logb 𝑁 ) ) )
27	11 21 26	3eqtrd	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑁 / 2 ) ∈ ℕ0 ) → ( ( ⌊ ‘ ( 2 logb ( 𝑁 / 2 ) ) ) + 1 ) = ( ⌊ ‘ ( 2 logb 𝑁 ) ) )
28	27	oveq1d	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑁 / 2 ) ∈ ℕ0 ) → ( ( ( ⌊ ‘ ( 2 logb ( 𝑁 / 2 ) ) ) + 1 ) + 1 ) = ( ( ⌊ ‘ ( 2 logb 𝑁 ) ) + 1 ) )
29		nn0enne	⊢ ( 𝑁 ∈ ℕ → ( ( 𝑁 / 2 ) ∈ ℕ0 ↔ ( 𝑁 / 2 ) ∈ ℕ ) )
30	29	biimpa	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑁 / 2 ) ∈ ℕ0 ) → ( 𝑁 / 2 ) ∈ ℕ )
31		blennn	⊢ ( ( 𝑁 / 2 ) ∈ ℕ → ( #b ‘ ( 𝑁 / 2 ) ) = ( ( ⌊ ‘ ( 2 logb ( 𝑁 / 2 ) ) ) + 1 ) )
32	31	oveq1d	⊢ ( ( 𝑁 / 2 ) ∈ ℕ → ( ( #b ‘ ( 𝑁 / 2 ) ) + 1 ) = ( ( ( ⌊ ‘ ( 2 logb ( 𝑁 / 2 ) ) ) + 1 ) + 1 ) )
33	30 32	syl	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑁 / 2 ) ∈ ℕ0 ) → ( ( #b ‘ ( 𝑁 / 2 ) ) + 1 ) = ( ( ( ⌊ ‘ ( 2 logb ( 𝑁 / 2 ) ) ) + 1 ) + 1 ) )
34		blennn	⊢ ( 𝑁 ∈ ℕ → ( #b ‘ 𝑁 ) = ( ( ⌊ ‘ ( 2 logb 𝑁 ) ) + 1 ) )
35	34	adantr	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑁 / 2 ) ∈ ℕ0 ) → ( #b ‘ 𝑁 ) = ( ( ⌊ ‘ ( 2 logb 𝑁 ) ) + 1 ) )
36	28 33 35	3eqtr4rd	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑁 / 2 ) ∈ ℕ0 ) → ( #b ‘ 𝑁 ) = ( ( #b ‘ ( 𝑁 / 2 ) ) + 1 ) )