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 \in ℕ \to (#_{b(N)-1digit (2)N=1})$

Proof

Step	Hyp	Ref	Expression
1		2nn	$⊢ 2 \in ℕ$
2	1	a1i	$⊢ N \in ℕ \to 2 \in ℕ$
3		blennnelnn	$⊢ N \in ℕ \to #_{b(N)\inℕ}$
4		nnm1nn0	$⊢ #_{b(N)\inℕ\to#_{b} (N) - 1 \in ℕ_{0}}$
5	3 4	syl	$⊢ N \in ℕ \to #_{b(N)-1\inℕ_{0}}$
6		nnre	$⊢ N \in ℕ \to N \in ℝ$
7		nnnn0	$⊢ N \in ℕ \to N \in ℕ_{0}$
8	7	nn0ge0d	$⊢ N \in ℕ \to 0 \leq N$
9		elrege0	$⊢ N \in [0, +∞) \leftrightarrow (N \in ℝ \land 0 \leq N)$
10	6 8 9	sylanbrc	$⊢ N \in ℕ \to N \in [0, +∞)$
11		nn0digval	$⊢ (2 \in ℕ \land #_{b(N)-1\inℕ_{0}\landN \in [0, +∞)\to(#_{b} (N) - 1) digit (2) N = ⌊\frac{N}{2^{#_{b} (N) - 1}}⌋ \mod 2})$
12	2 5 10 11	syl3anc	$⊢ N \in ℕ \to (#_{b(N)-1digit (2)N=⌊\frac{N}{2^{#_{b} (N) - 1}}⌋ \mod 2})$
13		n2dvds1	$⊢ \neg 2 ∥ 1$
14		blennn	$⊢ N \in ℕ \to #_{b(N)=⌊\log_{2} N⌋ + 1}$
15	14	oveq1d	$⊢ N \in ℕ \to #_{b(N)-1=⌊\log_{2} N⌋ + 1 - 1}$
16		2z	$⊢ 2 \in ℤ$
17		uzid	$⊢ 2 \in ℤ \to 2 \in ℤ_{\geq 2}$
18	16 17	ax-mp	$⊢ 2 \in ℤ_{\geq 2}$
19		nnrp	$⊢ N \in ℕ \to N \in ℝ^{+}$
20		relogbzcl	$⊢ (2 \in ℤ_{\geq 2} \land N \in ℝ^{+}) \to \log_{2} N \in ℝ$
21	18 19 20	sylancr	$⊢ N \in ℕ \to \log_{2} N \in ℝ$
22	21	flcld	$⊢ N \in ℕ \to ⌊\log_{2} N⌋ \in ℤ$
23	22	zcnd	$⊢ N \in ℕ \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 ℕ \to ⌊\log_{2} N⌋ + 1 - 1 = ⌊\log_{2} N⌋$
26	15 25	eqtrd	$⊢ N \in ℕ \to #_{b(N)-1=⌊\log_{2} N⌋}$
27	26	oveq2d	$⊢ N \in ℕ \to 2^{#_{b(N)-1=2^{⌊\log_{2} N⌋}}}$
28	27	oveq2d	$⊢ N \in ℕ \to \frac{N}{2^{#_{b(N)-1=\frac{N}{2^{⌊\log_{2} N⌋}}}}}$
29	28	fveq2d	$⊢ N \in ℕ \to ⌊\frac{N}{2^{#_{b(N)-1=⌊\frac{N}{2^{⌊\log_{2} N⌋}}⌋}}}⌋$
30		fldivexpfllog2	$⊢ N \in ℝ^{+} \to ⌊\frac{N}{2^{⌊\log_{2} N⌋}}⌋ = 1$
31	19 30	syl	$⊢ N \in ℕ \to ⌊\frac{N}{2^{⌊\log_{2} N⌋}}⌋ = 1$
32	29 31	eqtrd	$⊢ N \in ℕ \to ⌊\frac{N}{2^{#_{b(N)-1=1}}}⌋$
33	32	breq2d	$⊢ N \in ℕ \to (2 ∥ ⌊\frac{N}{2^{#_{b(N)-1\leftrightarrow2 ∥ 1}}}⌋)$
34	13 33	mtbiri	$⊢ N \in ℕ \to \neg 2 ∥ ⌊\frac{N}{2^{#_{b(N)-1}}}⌋$
35		2re	$⊢ 2 \in ℝ$
36	35	a1i	$⊢ N \in ℕ \to 2 \in ℝ$
37	36 5	reexpcld	$⊢ N \in ℕ \to 2^{#_{b(N)-1\inℝ}}$
38		2cnd	$⊢ N \in ℕ \to 2 \in ℂ$
39		2ne0	$⊢ 2 \neq 0$
40	39	a1i	$⊢ N \in ℕ \to 2 \neq 0$
41	5	nn0zd	$⊢ N \in ℕ \to #_{b(N)-1\inℤ}$
42	38 40 41	expne0d	$⊢ N \in ℕ \to 2^{#_{b(N)-1\neq0}}$
43	6 37 42	redivcld	$⊢ N \in ℕ \to \frac{N}{2^{#_{b(N)-1\inℝ}}}$
44	43	flcld	$⊢ N \in ℕ \to ⌊\frac{N}{2^{#_{b(N)-1\inℤ}}}⌋$
45		mod2eq1n2dvds	$⊢ ⌊\frac{N}{2^{#_{b(N)-1\inℤ\to(⌊\frac{N}{2^{#_{b} (N) - 1}}⌋ \mod 2 = 1 \leftrightarrow \neg 2 ∥ ⌊\frac{N}{2^{#_{b} (N) - 1}}⌋)}}}⌋$
46	44 45	syl	$⊢ N \in ℕ \to (⌊\frac{N}{2^{#_{b(N)-1\mod2=1\leftrightarrow\neg 2 ∥ ⌊\frac{N}{2^{#_{b} (N) - 1}}⌋}}}⌋)$
47	34 46	mpbird	$⊢ N \in ℕ \to ⌊\frac{N}{2^{#_{b(N)-1\mod2=1}}}⌋$
48	12 47	eqtrd	$⊢ N \in ℕ \to (#_{b(N)-1digit (2)N=1})$

Metamath Proof Explorer

Theorem dig2nn1st

Proof