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 0 K 0 K digit 2 N = 1 K bits N

Proof

Step Hyp Ref Expression
1 nn0re N 0 N
2 1 adantr N 0 K 0 N
3 2re 2
4 3 a1i N 0 2
5 reexpcl 2 K 0 2 K
6 4 5 sylan N 0 K 0 2 K
7 2cnd N 0 K 0 2
8 2ne0 2 0
9 8 a1i N 0 K 0 2 0
10 nn0z K 0 K
11 10 adantl N 0 K 0 K
12 7 9 11 expne0d N 0 K 0 2 K 0
13 2 6 12 redivcld N 0 K 0 N 2 K
14 13 flcld N 0 K 0 N 2 K
15 mod2eq1n2dvds N 2 K N 2 K mod 2 = 1 ¬ 2 N 2 K
16 14 15 syl N 0 K 0 N 2 K mod 2 = 1 ¬ 2 N 2 K
17 2nn 2
18 17 a1i N 0 K 0 2
19 simpr N 0 K 0 K 0
20 nn0rp0 N 0 N 0 +∞
21 20 adantr N 0 K 0 N 0 +∞
22 nn0digval 2 K 0 N 0 +∞ K digit 2 N = N 2 K mod 2
23 18 19 21 22 syl3anc N 0 K 0 K digit 2 N = N 2 K mod 2
24 23 eqeq1d N 0 K 0 K digit 2 N = 1 N 2 K mod 2 = 1
25 nn0z N 0 N
26 bitsval2 N K 0 K bits N ¬ 2 N 2 K
27 25 26 sylan N 0 K 0 K bits N ¬ 2 N 2 K
28 16 24 27 3bitr4d N 0 K 0 K digit 2 N = 1 K bits N