Metamath Proof Explorer

Theorem bitsp1

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

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

Proof

Step Hyp Ref Expression
1 2nn 
 |-  2 e. NN
2 1 a1i 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> 2 e. NN )
3 2 nncnd 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> 2 e. CC )
4 simpr 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> M e. NN0 )
5 3 4 expp1d 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( 2 ^ ( M + 1 ) ) = ( ( 2 ^ M ) x. 2 ) )
6 2 4 nnexpcld 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( 2 ^ M ) e. NN )
7 6 nncnd 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( 2 ^ M ) e. CC )
8 7 3 mulcomd 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( ( 2 ^ M ) x. 2 ) = ( 2 x. ( 2 ^ M ) ) )
9 5 8 eqtrd 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( 2 ^ ( M + 1 ) ) = ( 2 x. ( 2 ^ M ) ) )
10 9 oveq2d 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( N / ( 2 ^ ( M + 1 ) ) ) = ( N / ( 2 x. ( 2 ^ M ) ) ) )
11 simpl 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> N e. ZZ )
12 11 zcnd 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> N e. CC )
13 2 nnne0d 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> 2 =/= 0 )
14 6 nnne0d 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( 2 ^ M ) =/= 0 )
15 12 3 7 13 14 divdiv1d 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( ( N / 2 ) / ( 2 ^ M ) ) = ( N / ( 2 x. ( 2 ^ M ) ) ) )
16 10 15 eqtr4d 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( N / ( 2 ^ ( M + 1 ) ) ) = ( ( N / 2 ) / ( 2 ^ M ) ) )
17 16 fveq2d 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( |_ ` ( N / ( 2 ^ ( M + 1 ) ) ) ) = ( |_ ` ( ( N / 2 ) / ( 2 ^ M ) ) ) )
18 11 zred 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> N e. RR )
19 18 rehalfcld 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( N / 2 ) e. RR )
20 fldiv 
 |-  ( ( ( N / 2 ) e. RR /\ ( 2 ^ M ) e. NN ) -> ( |_ ` ( ( |_ ` ( N / 2 ) ) / ( 2 ^ M ) ) ) = ( |_ ` ( ( N / 2 ) / ( 2 ^ M ) ) ) )
21 19 6 20 syl2anc 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( |_ ` ( ( |_ ` ( N / 2 ) ) / ( 2 ^ M ) ) ) = ( |_ ` ( ( N / 2 ) / ( 2 ^ M ) ) ) )
22 17 21 eqtr4d 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( |_ ` ( N / ( 2 ^ ( M + 1 ) ) ) ) = ( |_ ` ( ( |_ ` ( N / 2 ) ) / ( 2 ^ M ) ) ) )
23 22 breq2d 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( 2 || ( |_ ` ( N / ( 2 ^ ( M + 1 ) ) ) ) <-> 2 || ( |_ ` ( ( |_ ` ( N / 2 ) ) / ( 2 ^ M ) ) ) ) )
24 23 notbid 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( -. 2 || ( |_ ` ( N / ( 2 ^ ( M + 1 ) ) ) ) <-> -. 2 || ( |_ ` ( ( |_ ` ( N / 2 ) ) / ( 2 ^ M ) ) ) ) )
25 peano2nn0 
 |-  ( M e. NN0 -> ( M + 1 ) e. NN0 )
26 bitsval2 
 |-  ( ( N e. ZZ /\ ( M + 1 ) e. NN0 ) -> ( ( M + 1 ) e. ( bits ` N ) <-> -. 2 || ( |_ ` ( N / ( 2 ^ ( M + 1 ) ) ) ) ) )
27 25 26 sylan2 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( ( M + 1 ) e. ( bits ` N ) <-> -. 2 || ( |_ ` ( N / ( 2 ^ ( M + 1 ) ) ) ) ) )
28 19 flcld 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( |_ ` ( N / 2 ) ) e. ZZ )
29 bitsval2 
 |-  ( ( ( |_ ` ( N / 2 ) ) e. ZZ /\ M e. NN0 ) -> ( M e. ( bits ` ( |_ ` ( N / 2 ) ) ) <-> -. 2 || ( |_ ` ( ( |_ ` ( N / 2 ) ) / ( 2 ^ M ) ) ) ) )
30 28 29 sylancom 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( M e. ( bits ` ( |_ ` ( N / 2 ) ) ) <-> -. 2 || ( |_ ` ( ( |_ ` ( N / 2 ) ) / ( 2 ^ M ) ) ) ) )
31 24 27 30 3bitr4d 
 |-  ( ( N e. ZZ /\ M e. NN0 ) -> ( ( M + 1 ) e. ( bits ` N ) <-> M e. ( bits ` ( |_ ` ( N / 2 ) ) ) ) )