Metamath Proof Explorer

Theorem bitsp1e

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

Ref Expression
Assertion bitsp1e 
|- ( ( N e. ZZ /\ M e. NN0 ) -> ( ( M + 1 ) e. ( bits ` ( 2 x. N ) ) <-> 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 bitsp1 
 |-  ( ( ( 2 x. N ) e. ZZ /\ M e. NN0 ) -> ( ( M + 1 ) e. ( bits ` ( 2 x. N ) ) <-> M e. ( bits ` ( |_ ` ( ( 2 x. N ) / 2 ) ) ) ) )
6 4 5 sylan 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( ( M + 1 ) e. ( bits ` ( 2 x. N ) ) <-> M e. ( bits ` ( |_ ` ( ( 2 x. N ) / 2 ) ) ) ) )
7 zcn 
 |-  ( N e. ZZ -> N e. CC )
8 2cnd 
 |-  ( N e. ZZ -> 2 e. CC )
9 2ne0 
 |-  2 =/= 0
10 9 a1i 
 |-  ( N e. ZZ -> 2 =/= 0 )
11 7 8 10 divcan3d 
 |-  ( N e. ZZ -> ( ( 2 x. N ) / 2 ) = N )
12 11 fveq2d 
 |-  ( N e. ZZ -> ( |_ ` ( ( 2 x. N ) / 2 ) ) = ( |_ ` N ) )
13 flid 
 |-  ( N e. ZZ -> ( |_ ` N ) = N )
14 12 13 eqtrd 
 |-  ( N e. ZZ -> ( |_ ` ( ( 2 x. N ) / 2 ) ) = N )
15 14 adantr 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( |_ ` ( ( 2 x. N ) / 2 ) ) = N )
16 15 fveq2d 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( bits ` ( |_ ` ( ( 2 x. N ) / 2 ) ) ) = ( bits ` N ) )
17 16 eleq2d 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( M e. ( bits ` ( |_ ` ( ( 2 x. N ) / 2 ) ) ) <-> M e. ( bits ` N ) ) )
18 6 17 bitrd 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( ( M + 1 ) e. ( bits ` ( 2 x. N ) ) <-> M e. ( bits ` N ) ) )