Metamath Proof Explorer

Theorem dig2bits

Description: The K th digit of a nonnegative integer N in a binary system is its K th bit. (Contributed by AV, 24-May-2020)

Ref Expression
Assertion dig2bits 
|- ( ( N e. NN0 /\ K e. NN0 ) -> ( ( K ( digit ` 2 ) N ) = 1 <-> K e. ( bits ` N ) ) )

Proof

Step Hyp Ref Expression
1 nn0re 
 |-  ( N e. NN0 -> N e. RR )
2 1 adantr 
 |-  ( ( N e. NN0 /\ K e. NN0 ) -> N e. RR )
3 2re 
 |-  2 e. RR
4 3 a1i 
 |-  ( N e. NN0 -> 2 e. RR )
5 reexpcl 
 |-  ( ( 2 e. RR /\ K e. NN0 ) -> ( 2 ^ K ) e. RR )
6 4 5 sylan 
 |-  ( ( N e. NN0 /\ K e. NN0 ) -> ( 2 ^ K ) e. RR )
7 2cnd 
 |-  ( ( N e. NN0 /\ K e. NN0 ) -> 2 e. CC )
8 2ne0 
 |-  2 =/= 0
9 8 a1i 
 |-  ( ( N e. NN0 /\ K e. NN0 ) -> 2 =/= 0 )
10 nn0z 
 |-  ( K e. NN0 -> K e. ZZ )
11 10 adantl 
 |-  ( ( N e. NN0 /\ K e. NN0 ) -> K e. ZZ )
12 7 9 11 expne0d 
 |-  ( ( N e. NN0 /\ K e. NN0 ) -> ( 2 ^ K ) =/= 0 )
13 2 6 12 redivcld 
 |-  ( ( N e. NN0 /\ K e. NN0 ) -> ( N / ( 2 ^ K ) ) e. RR )
14 13 flcld 
 |-  ( ( N e. NN0 /\ K e. NN0 ) -> ( |_ ` ( N / ( 2 ^ K ) ) ) e. ZZ )
15 mod2eq1n2dvds 
 |-  ( ( |_ ` ( N / ( 2 ^ K ) ) ) e. ZZ -> ( ( ( |_ ` ( N / ( 2 ^ K ) ) ) mod 2 ) = 1 <-> -. 2 || ( |_ ` ( N / ( 2 ^ K ) ) ) ) )
16 14 15 syl 
 |-  ( ( N e. NN0 /\ K e. NN0 ) -> ( ( ( |_ ` ( N / ( 2 ^ K ) ) ) mod 2 ) = 1 <-> -. 2 || ( |_ ` ( N / ( 2 ^ K ) ) ) ) )
17 2nn 
 |-  2 e. NN
18 17 a1i 
 |-  ( ( N e. NN0 /\ K e. NN0 ) -> 2 e. NN )
19 simpr 
 |-  ( ( N e. NN0 /\ K e. NN0 ) -> K e. NN0 )
20 nn0rp0 
 |-  ( N e. NN0 -> N e. ( 0 [,) +oo ) )
21 20 adantr 
 |-  ( ( N e. NN0 /\ K e. NN0 ) -> N e. ( 0 [,) +oo ) )
22 nn0digval 
 |-  ( ( 2 e. NN /\ K e. NN0 /\ N e. ( 0 [,) +oo ) ) -> ( K ( digit ` 2 ) N ) = ( ( |_ ` ( N / ( 2 ^ K ) ) ) mod 2 ) )
23 18 19 21 22 syl3anc 
 |-  ( ( N e. NN0 /\ K e. NN0 ) -> ( K ( digit ` 2 ) N ) = ( ( |_ ` ( N / ( 2 ^ K ) ) ) mod 2 ) )
24 23 eqeq1d 
 |-  ( ( N e. NN0 /\ K e. NN0 ) -> ( ( K ( digit ` 2 ) N ) = 1 <-> ( ( |_ ` ( N / ( 2 ^ K ) ) ) mod 2 ) = 1 ) )
25 nn0z 
 |-  ( N e. NN0 -> N e. ZZ )
26 bitsval2 
 |-  ( ( N e. ZZ /\ K e. NN0 ) -> ( K e. ( bits ` N ) <-> -. 2 || ( |_ ` ( N / ( 2 ^ K ) ) ) ) )
27 25 26 sylan 
 |-  ( ( N e. NN0 /\ K e. NN0 ) -> ( K e. ( bits ` N ) <-> -. 2 || ( |_ ` ( N / ( 2 ^ K ) ) ) ) )
28 16 24 27 3bitr4d 
 |-  ( ( N e. NN0 /\ K e. NN0 ) -> ( ( K ( digit ` 2 ) N ) = 1 <-> K e. ( bits ` N ) ) )