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

Proof

Step	Hyp	Ref	Expression
1		2nn	$$⊢2\in \mathbb{N}$$
2	1	a1i	$$⊢N\in \mathbb{N}\to 2\in \mathbb{N}$$
3		blennnelnn
4		nnm1nn0
5	3 4	syl
6		nnre	$$⊢N\in \mathbb{N}\to N\in ℝ$$
7		nnnn0	$$⊢N\in \mathbb{N}\to N\in {\mathbb{N}}_0$$
8	7	nn0ge0d	$$⊢N\in \mathbb{N}\to 0\le N$$
9		elrege0	$$⊢N\in \left[0,\mathrm{+\infty }\right)\leftrightarrow \left(N\in ℝ\wedge 0\le N\right)$$
10	6 8 9	sylanbrc	$$⊢N\in \mathbb{N}\to N\in \left[0,\mathrm{+\infty }\right)$$
11		nn0digval
12	2 5 10 11	syl3anc
13		n2dvds1	$$⊢\neg 2\parallel 1$$
14		blennn
15	14	oveq1d
16		2z	$$⊢2\in \mathbb{Z}$$
17		uzid	$$⊢2\in \mathbb{Z}\to 2\in {\mathbb{Z}}_{\ge 2}$$
18	16 17	ax-mp	$$⊢2\in {\mathbb{Z}}_{\ge 2}$$
19		nnrp	$$⊢N\in \mathbb{N}\to N\in {ℝ}^{+}$$
20		relogbzcl	$$⊢\left(2\in {\mathbb{Z}}_{\ge 2}\wedge N\in {ℝ}^{+}\right)\to {\log }_{2}N\in ℝ$$
21	18 19 20	sylancr	$$⊢N\in \mathbb{N}\to {\log }_{2}N\in ℝ$$
22	21	flcld	$$⊢N\in \mathbb{N}\to ⌊{\log }_{2}N⌋\in \mathbb{Z}$$
23	22	zcnd	$$⊢N\in \mathbb{N}\to ⌊{\log }_{2}N⌋\in ℂ$$
24		pncan1	$$⊢⌊{\log }_{2}N⌋\in ℂ\to ⌊{\log }_{2}N⌋+1-1=⌊{\log }_{2}N⌋$$
25	23 24	syl	$$⊢N\in \mathbb{N}\to ⌊{\log }_{2}N⌋+1-1=⌊{\log }_{2}N⌋$$
26	15 25	eqtrd
27	26	oveq2d
28	27	oveq2d
29	28	fveq2d
30		fldivexpfllog2	$$⊢N\in {ℝ}^{+}\to ⌊\frac{N}{2^{⌊{\log }_{2}N⌋}}⌋=1$$
31	19 30	syl	$$⊢N\in \mathbb{N}\to ⌊\frac{N}{2^{⌊{\log }_{2}N⌋}}⌋=1$$
32	29 31	eqtrd
33	32	breq2d
34	13 33	mtbiri
35		2re	$$⊢2\in ℝ$$
36	35	a1i	$$⊢N\in \mathbb{N}\to 2\in ℝ$$
37	36 5	reexpcld
38		2cnd	$$⊢N\in \mathbb{N}\to 2\in ℂ$$
39		2ne0	$$⊢2\ne 0$$
40	39	a1i	$$⊢N\in \mathbb{N}\to 2\ne 0$$
41	5	nn0zd
42	38 40 41	expne0d
43	6 37 42	redivcld
44	43	flcld
45		mod2eq1n2dvds
46	44 45	syl
47	34 46	mpbird
48	12 47	eqtrd