Metamath Proof Explorer

Theorem bitsp1o

Description: The M + 1 -th bit of 2 N + 1 is the M -th bit of N . (Contributed by Mario Carneiro, 5-Sep-2016)

Ref Expression
Assertion bitsp1o 
|- ( ( N e. ZZ /\ M e. NN0 ) -> ( ( M + 1 ) e. ( bits ` ( ( 2 x. N ) + 1 ) ) <-> M e. ( bits ` N ) ) )

Proof

Step Hyp Ref Expression
1 2z 
 |-  2 e. ZZ
2 1 a1i 
 |-  ( N e. ZZ -> 2 e. ZZ )
3 id 
 |-  ( N e. ZZ -> N e. ZZ )
4 2 3 zmulcld 
 |-  ( N e. ZZ -> ( 2 x. N ) e. ZZ )
5 4 peano2zd 
 |-  ( N e. ZZ -> ( ( 2 x. N ) + 1 ) e. ZZ )
6 bitsp1 
 |-  ( ( ( ( 2 x. N ) + 1 ) e. ZZ /\ M e. NN0 ) -> ( ( M + 1 ) e. ( bits ` ( ( 2 x. N ) + 1 ) ) <-> M e. ( bits ` ( |_ ` ( ( ( 2 x. N ) + 1 ) / 2 ) ) ) ) )
7 5 6 sylan 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( ( M + 1 ) e. ( bits ` ( ( 2 x. N ) + 1 ) ) <-> M e. ( bits ` ( |_ ` ( ( ( 2 x. N ) + 1 ) / 2 ) ) ) ) )
8 2re 
 |-  2 e. RR
9 8 a1i 
 |-  ( N e. ZZ -> 2 e. RR )
10 zre 
 |-  ( N e. ZZ -> N e. RR )
11 9 10 remulcld 
 |-  ( N e. ZZ -> ( 2 x. N ) e. RR )
12 11 recnd 
 |-  ( N e. ZZ -> ( 2 x. N ) e. CC )
13 1cnd 
 |-  ( N e. ZZ -> 1 e. CC )
14 2cnd 
 |-  ( N e. ZZ -> 2 e. CC )
15 2ne0 
 |-  2 =/= 0
16 15 a1i 
 |-  ( N e. ZZ -> 2 =/= 0 )
17 12 13 14 16 divdird 
 |-  ( N e. ZZ -> ( ( ( 2 x. N ) + 1 ) / 2 ) = ( ( ( 2 x. N ) / 2 ) + ( 1 / 2 ) ) )
18 zcn 
 |-  ( N e. ZZ -> N e. CC )
19 18 14 16 divcan3d 
 |-  ( N e. ZZ -> ( ( 2 x. N ) / 2 ) = N )
20 19 oveq1d 
 |-  ( N e. ZZ -> ( ( ( 2 x. N ) / 2 ) + ( 1 / 2 ) ) = ( N + ( 1 / 2 ) ) )
21 17 20 eqtrd 
 |-  ( N e. ZZ -> ( ( ( 2 x. N ) + 1 ) / 2 ) = ( N + ( 1 / 2 ) ) )
22 21 fveq2d 
 |-  ( N e. ZZ -> ( |_ ` ( ( ( 2 x. N ) + 1 ) / 2 ) ) = ( |_ ` ( N + ( 1 / 2 ) ) ) )
23 halfge0 
 |-  0 <_ ( 1 / 2 )
24 halflt1 
 |-  ( 1 / 2 ) < 1
25 23 24 pm3.2i 
 |-  ( 0 <_ ( 1 / 2 ) /\ ( 1 / 2 ) < 1 )
26 halfre 
 |-  ( 1 / 2 ) e. RR
27 flbi2 
 |-  ( ( N e. ZZ /\ ( 1 / 2 ) e. RR ) -> ( ( |_ ` ( N + ( 1 / 2 ) ) ) = N <-> ( 0 <_ ( 1 / 2 ) /\ ( 1 / 2 ) < 1 ) ) )
28 26 27 mpan2 
 |-  ( N e. ZZ -> ( ( |_ ` ( N + ( 1 / 2 ) ) ) = N <-> ( 0 <_ ( 1 / 2 ) /\ ( 1 / 2 ) < 1 ) ) )
29 25 28 mpbiri 
 |-  ( N e. ZZ -> ( |_ ` ( N + ( 1 / 2 ) ) ) = N )
30 22 29 eqtrd 
 |-  ( N e. ZZ -> ( |_ ` ( ( ( 2 x. N ) + 1 ) / 2 ) ) = N )
31 30 adantr 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( |_ ` ( ( ( 2 x. N ) + 1 ) / 2 ) ) = N )
32 31 fveq2d 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( bits ` ( |_ ` ( ( ( 2 x. N ) + 1 ) / 2 ) ) ) = ( bits ` N ) )
33 32 eleq2d 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( M e. ( bits ` ( |_ ` ( ( ( 2 x. N ) + 1 ) / 2 ) ) ) <-> M e. ( bits ` N ) ) )
34 7 33 bitrd 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( ( M + 1 ) e. ( bits ` ( ( 2 x. N ) + 1 ) ) <-> M e. ( bits ` N ) ) )