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 ⊢N∈ℕ∧N2∈ℕ0→#b ⁡ N2 = #b ⁡N−1

Proof

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