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