Metamath Proof Explorer

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 ) )