Metamath Proof Explorer


Theorem dig2nn1st

Description: The first (relevant) digit of a positive integer in a binary system is 1. (Contributed by AV, 26-May-2020)

Ref Expression
Assertion dig2nn1st N # b N 1 digit 2 N = 1

Proof

Step Hyp Ref Expression
1 2nn 2
2 1 a1i N 2
3 blennnelnn N # b N
4 nnm1nn0 # b N # b N 1 0
5 3 4 syl N # b N 1 0
6 nnre N N
7 nnnn0 N N 0
8 7 nn0ge0d N 0 N
9 elrege0 N 0 +∞ N 0 N
10 6 8 9 sylanbrc N N 0 +∞
11 nn0digval 2 # b N 1 0 N 0 +∞ # b N 1 digit 2 N = N 2 # b N 1 mod 2
12 2 5 10 11 syl3anc N # b N 1 digit 2 N = N 2 # b N 1 mod 2
13 n2dvds1 ¬ 2 1
14 blennn N # b N = log 2 N + 1
15 14 oveq1d N # b N 1 = log 2 N + 1 - 1
16 2z 2
17 uzid 2 2 2
18 16 17 ax-mp 2 2
19 nnrp N N +
20 relogbzcl 2 2 N + log 2 N
21 18 19 20 sylancr N log 2 N
22 21 flcld N log 2 N
23 22 zcnd N log 2 N
24 pncan1 log 2 N log 2 N + 1 - 1 = log 2 N
25 23 24 syl N log 2 N + 1 - 1 = log 2 N
26 15 25 eqtrd N # b N 1 = log 2 N
27 26 oveq2d N 2 # b N 1 = 2 log 2 N
28 27 oveq2d N N 2 # b N 1 = N 2 log 2 N
29 28 fveq2d N N 2 # b N 1 = N 2 log 2 N
30 fldivexpfllog2 N + N 2 log 2 N = 1
31 19 30 syl N N 2 log 2 N = 1
32 29 31 eqtrd N N 2 # b N 1 = 1
33 32 breq2d N 2 N 2 # b N 1 2 1
34 13 33 mtbiri N ¬ 2 N 2 # b N 1
35 2re 2
36 35 a1i N 2
37 36 5 reexpcld N 2 # b N 1
38 2cnd N 2
39 2ne0 2 0
40 39 a1i N 2 0
41 5 nn0zd N # b N 1
42 38 40 41 expne0d N 2 # b N 1 0
43 6 37 42 redivcld N N 2 # b N 1
44 43 flcld N N 2 # b N 1
45 mod2eq1n2dvds N 2 # b N 1 N 2 # b N 1 mod 2 = 1 ¬ 2 N 2 # b N 1
46 44 45 syl N N 2 # b N 1 mod 2 = 1 ¬ 2 N 2 # b N 1
47 34 46 mpbird N N 2 # b N 1 mod 2 = 1
48 12 47 eqtrd N # b N 1 digit 2 N = 1