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 ∈ ℕ ∧ N 2 ∈ ℕ 0 → # b ⁡ N 2 = # 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 ∈ ℕ ∧ N 2 ∈ ℕ 0 → N ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0
7 divcan2 ⊢ N ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0 → 2 ⁢ N 2 = N
8 7 eqcomd ⊢ N ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0 → N = 2 ⁢ N 2
9 6 8 syl ⊢ N ∈ ℕ ∧ N 2 ∈ ℕ 0 → N = 2 ⁢ N 2
10 9 fveq2d ⊢ N ∈ ℕ ∧ N 2 ∈ ℕ 0 → # b ⁡ N = # b ⁡ 2 ⁢ N 2
11 nn0enne ⊢ N ∈ ℕ → N 2 ∈ ℕ 0 ↔ N 2 ∈ ℕ
12 11 biimpa ⊢ N ∈ ℕ ∧ N 2 ∈ ℕ 0 → N 2 ∈ ℕ
13 blennnt2 ⊢ N 2 ∈ ℕ → # b ⁡ 2 ⁢ N 2 = # b ⁡ N 2 + 1
14 12 13 syl ⊢ N ∈ ℕ ∧ N 2 ∈ ℕ 0 → # b ⁡ 2 ⁢ N 2 = # b ⁡ N 2 + 1
15 10 14 eqtr2d ⊢ N ∈ ℕ ∧ N 2 ∈ ℕ 0 → # b ⁡ N 2 + 1 = # b ⁡ N
16 blennnelnn ⊢ N ∈ ℕ → # b ⁡ N ∈ ℕ
17 16 nncnd ⊢ N ∈ ℕ → # b ⁡ N ∈ ℂ
18 17 adantr ⊢ N ∈ ℕ ∧ N 2 ∈ ℕ 0 → # b ⁡ N ∈ ℂ
19 1cnd ⊢ N ∈ ℕ ∧ N 2 ∈ ℕ 0 → 1 ∈ ℂ
20 blennn0elnn ⊢ N 2 ∈ ℕ 0 → # b ⁡ N 2 ∈ ℕ
21 20 nncnd ⊢ N 2 ∈ ℕ 0 → # b ⁡ N 2 ∈ ℂ
22 21 adantl ⊢ N ∈ ℕ ∧ N 2 ∈ ℕ 0 → # b ⁡ N 2 ∈ ℂ
23 18 19 22 subadd2d ⊢ N ∈ ℕ ∧ N 2 ∈ ℕ 0 → # b ⁡ N − 1 = # b ⁡ N 2 ↔ # b ⁡ N 2 + 1 = # b ⁡ N
24 15 23 mpbird ⊢ N ∈ ℕ ∧ N 2 ∈ ℕ 0 → # b ⁡ N − 1 = # b ⁡ N 2
25 24 eqcomd ⊢ N ∈ ℕ ∧ N 2 ∈ ℕ 0 → # b ⁡ N 2 = # b ⁡ N − 1