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 e. NN -> ( ( ( #b ` N ) - 1 ) ( digit ` 2 ) N ) = 1 )

Proof

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