Theorem blennn0em1

Description: The binary length of the half of an even positive integer is the binary length of the integer minus 1. (Contributed by AV, 30-May-2010)

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

Proof

Step	Hyp	Ref	Expression
1		nncn	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℂ )
2		2cnd	⊢ ( 𝑁 ∈ ℕ → 2 ∈ ℂ )
3		2ne0	⊢ 2 ≠ 0
4	3	a1i	⊢ ( 𝑁 ∈ ℕ → 2 ≠ 0 )
5	1 2 4	3jca	⊢ ( 𝑁 ∈ ℕ → ( 𝑁 ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0 ) )
6	5	adantr	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑁 / 2 ) ∈ ℕ0 ) → ( 𝑁 ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0 ) )
7		divcan2	⊢ ( ( 𝑁 ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0 ) → ( 2 · ( 𝑁 / 2 ) ) = 𝑁 )
8	7	eqcomd	⊢ ( ( 𝑁 ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0 ) → 𝑁 = ( 2 · ( 𝑁 / 2 ) ) )
9	6 8	syl	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑁 / 2 ) ∈ ℕ0 ) → 𝑁 = ( 2 · ( 𝑁 / 2 ) ) )
10	9	fveq2d	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑁 / 2 ) ∈ ℕ0 ) → ( #b ‘ 𝑁 ) = ( #b ‘ ( 2 · ( 𝑁 / 2 ) ) ) )
11		nn0enne	⊢ ( 𝑁 ∈ ℕ → ( ( 𝑁 / 2 ) ∈ ℕ0 ↔ ( 𝑁 / 2 ) ∈ ℕ ) )
12	11	biimpa	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑁 / 2 ) ∈ ℕ0 ) → ( 𝑁 / 2 ) ∈ ℕ )
13		blennnt2	⊢ ( ( 𝑁 / 2 ) ∈ ℕ → ( #b ‘ ( 2 · ( 𝑁 / 2 ) ) ) = ( ( #b ‘ ( 𝑁 / 2 ) ) + 1 ) )
14	12 13	syl	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑁 / 2 ) ∈ ℕ0 ) → ( #b ‘ ( 2 · ( 𝑁 / 2 ) ) ) = ( ( #b ‘ ( 𝑁 / 2 ) ) + 1 ) )
15	10 14	eqtr2d	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑁 / 2 ) ∈ ℕ0 ) → ( ( #b ‘ ( 𝑁 / 2 ) ) + 1 ) = ( #b ‘ 𝑁 ) )
16		blennnelnn	⊢ ( 𝑁 ∈ ℕ → ( #b ‘ 𝑁 ) ∈ ℕ )
17	16	nncnd	⊢ ( 𝑁 ∈ ℕ → ( #b ‘ 𝑁 ) ∈ ℂ )
18	17	adantr	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑁 / 2 ) ∈ ℕ0 ) → ( #b ‘ 𝑁 ) ∈ ℂ )
19		1cnd	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑁 / 2 ) ∈ ℕ0 ) → 1 ∈ ℂ )
20		blennn0elnn	⊢ ( ( 𝑁 / 2 ) ∈ ℕ0 → ( #b ‘ ( 𝑁 / 2 ) ) ∈ ℕ )
21	20	nncnd	⊢ ( ( 𝑁 / 2 ) ∈ ℕ0 → ( #b ‘ ( 𝑁 / 2 ) ) ∈ ℂ )
22	21	adantl	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑁 / 2 ) ∈ ℕ0 ) → ( #b ‘ ( 𝑁 / 2 ) ) ∈ ℂ )
23	18 19 22	subadd2d	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑁 / 2 ) ∈ ℕ0 ) → ( ( ( #b ‘ 𝑁 ) − 1 ) = ( #b ‘ ( 𝑁 / 2 ) ) ↔ ( ( #b ‘ ( 𝑁 / 2 ) ) + 1 ) = ( #b ‘ 𝑁 ) ) )
24	15 23	mpbird	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑁 / 2 ) ∈ ℕ0 ) → ( ( #b ‘ 𝑁 ) − 1 ) = ( #b ‘ ( 𝑁 / 2 ) ) )
25	24	eqcomd	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑁 / 2 ) ∈ ℕ0 ) → ( #b ‘ ( 𝑁 / 2 ) ) = ( ( #b ‘ 𝑁 ) − 1 ) )