fllog2

Description: The floor of the binary logarithm of 2 to the power of an element of a half-open integer interval bounded by powers of 2 is equal to the integer. (Contributed by AV, 31-May-2020)

		Ref	Expression
	Assertion	fllog2	$⊢ (I \in ℕ_{0} \land N \in (2^{I} ..^2^{I + 1})) \to ⌊\log_{2} N⌋ = I$

Proof

Step	Hyp	Ref	Expression
1		nn0z	$⊢ I \in ℕ_{0} \to I \in ℤ$
2	1	adantr	$⊢ (I \in ℕ_{0} \land N \in (2^{I} ..^2^{I + 1})) \to I \in ℤ$
3		2rp	$⊢ 2 \in ℝ^{+}$
4		elfzoelz	$⊢ N \in (2^{I} ..^2^{I + 1}) \to N \in ℤ$
5	4	zred	$⊢ N \in (2^{I} ..^2^{I + 1}) \to N \in ℝ$
6	5	adantl	$⊢ (I \in ℕ_{0} \land N \in (2^{I} ..^2^{I + 1})) \to N \in ℝ$
7		elfzo2	$⊢ N \in (2^{I} ..^2^{I + 1}) \leftrightarrow (N \in ℤ_{\geq 2^{I}} \land 2^{I + 1} \in ℤ \land N < 2^{I + 1})$
8		eluz2	$⊢ N \in ℤ_{\geq 2^{I}} \leftrightarrow (2^{I} \in ℤ \land N \in ℤ \land 2^{I} \leq N)$
9		2re	$⊢ 2 \in ℝ$
10		2pos	$⊢ 0 < 2$
11	10	a1i	$⊢ I \in ℕ_{0} \to 0 < 2$
12		expgt0	$⊢ (2 \in ℝ \land I \in ℤ \land 0 < 2) \to 0 < 2^{I}$
13	9 1 11 12	mp3an2i	$⊢ I \in ℕ_{0} \to 0 < 2^{I}$
14	13	adantl	$⊢ ((2^{I} \in ℤ \land N \in ℤ) \land I \in ℕ_{0}) \to 0 < 2^{I}$
15		0red	$⊢ ((2^{I} \in ℤ \land N \in ℤ) \land I \in ℕ_{0}) \to 0 \in ℝ$
16		zre	$⊢ 2^{I} \in ℤ \to 2^{I} \in ℝ$
17	16	adantr	$⊢ (2^{I} \in ℤ \land N \in ℤ) \to 2^{I} \in ℝ$
18	17	adantr	$⊢ ((2^{I} \in ℤ \land N \in ℤ) \land I \in ℕ_{0}) \to 2^{I} \in ℝ$
19		zre	$⊢ N \in ℤ \to N \in ℝ$
20	19	ad2antlr	$⊢ ((2^{I} \in ℤ \land N \in ℤ) \land I \in ℕ_{0}) \to N \in ℝ$
21		ltletr	$⊢ (0 \in ℝ \land 2^{I} \in ℝ \land N \in ℝ) \to ((0 < 2^{I} \land 2^{I} \leq N) \to 0 < N)$
22	15 18 20 21	syl3anc	$⊢ ((2^{I} \in ℤ \land N \in ℤ) \land I \in ℕ_{0}) \to ((0 < 2^{I} \land 2^{I} \leq N) \to 0 < N)$
23	14 22	mpand	$⊢ ((2^{I} \in ℤ \land N \in ℤ) \land I \in ℕ_{0}) \to (2^{I} \leq N \to 0 < N)$
24	23	ex	$⊢ (2^{I} \in ℤ \land N \in ℤ) \to (I \in ℕ_{0} \to (2^{I} \leq N \to 0 < N))$
25	24	com23	$⊢ (2^{I} \in ℤ \land N \in ℤ) \to (2^{I} \leq N \to (I \in ℕ_{0} \to 0 < N))$
26	25	3impia	$⊢ (2^{I} \in ℤ \land N \in ℤ \land 2^{I} \leq N) \to (I \in ℕ_{0} \to 0 < N)$
27	8 26	sylbi	$⊢ N \in ℤ_{\geq 2^{I}} \to (I \in ℕ_{0} \to 0 < N)$
28	27	3ad2ant1	$⊢ (N \in ℤ_{\geq 2^{I}} \land 2^{I + 1} \in ℤ \land N < 2^{I + 1}) \to (I \in ℕ_{0} \to 0 < N)$
29	7 28	sylbi	$⊢ N \in (2^{I} ..^2^{I + 1}) \to (I \in ℕ_{0} \to 0 < N)$
30	29	impcom	$⊢ (I \in ℕ_{0} \land N \in (2^{I} ..^2^{I + 1})) \to 0 < N$
31	6 30	elrpd	$⊢ (I \in ℕ_{0} \land N \in (2^{I} ..^2^{I + 1})) \to N \in ℝ^{+}$
32		1ne2	$⊢ 1 \neq 2$
33	32	necomi	$⊢ 2 \neq 1$
34	33	a1i	$⊢ (I \in ℕ_{0} \land N \in (2^{I} ..^2^{I + 1})) \to 2 \neq 1$
35		relogbcl	$⊢ (2 \in ℝ^{+} \land N \in ℝ^{+} \land 2 \neq 1) \to \log_{2} N \in ℝ$
36	3 31 34 35	mp3an2i	$⊢ (I \in ℕ_{0} \land N \in (2^{I} ..^2^{I + 1})) \to \log_{2} N \in ℝ$
37	36	flcld	$⊢ (I \in ℕ_{0} \land N \in (2^{I} ..^2^{I + 1})) \to ⌊\log_{2} N⌋ \in ℤ$
38		eluzelz	$⊢ N \in ℤ_{\geq 2^{I}} \to N \in ℤ$
39		zltlem1	$⊢ (N \in ℤ \land 2^{I + 1} \in ℤ) \to (N < 2^{I + 1} \leftrightarrow N \leq 2^{I + 1} - 1)$
40	38 39	sylan	$⊢ (N \in ℤ_{\geq 2^{I}} \land 2^{I + 1} \in ℤ) \to (N < 2^{I + 1} \leftrightarrow N \leq 2^{I + 1} - 1)$
41		2z	$⊢ 2 \in ℤ$
42		uzid	$⊢ 2 \in ℤ \to 2 \in ℤ_{\geq 2}$
43	41 42	ax-mp	$⊢ 2 \in ℤ_{\geq 2}$
44		eluzelre	$⊢ N \in ℤ_{\geq 2^{I}} \to N \in ℝ$
45	44	adantr	$⊢ (N \in ℤ_{\geq 2^{I}} \land I \in ℕ_{0}) \to N \in ℝ$
46	9	a1i	$⊢ I \in ℕ_{0} \to 2 \in ℝ$
47	46 1 11	3jca	$⊢ I \in ℕ_{0} \to (2 \in ℝ \land I \in ℤ \land 0 < 2)$
48	47	3ad2ant3	$⊢ (2^{I} \in ℤ \land N \in ℤ \land I \in ℕ_{0}) \to (2 \in ℝ \land I \in ℤ \land 0 < 2)$
49	48 12	syl	$⊢ (2^{I} \in ℤ \land N \in ℤ \land I \in ℕ_{0}) \to 0 < 2^{I}$
50		0red	$⊢ (2^{I} \in ℤ \land N \in ℤ \land I \in ℕ_{0}) \to 0 \in ℝ$
51	16	3ad2ant1	$⊢ (2^{I} \in ℤ \land N \in ℤ \land I \in ℕ_{0}) \to 2^{I} \in ℝ$
52	19	3ad2ant2	$⊢ (2^{I} \in ℤ \land N \in ℤ \land I \in ℕ_{0}) \to N \in ℝ$
53	50 51 52 21	syl3anc	$⊢ (2^{I} \in ℤ \land N \in ℤ \land I \in ℕ_{0}) \to ((0 < 2^{I} \land 2^{I} \leq N) \to 0 < N)$
54	49 53	mpand	$⊢ (2^{I} \in ℤ \land N \in ℤ \land I \in ℕ_{0}) \to (2^{I} \leq N \to 0 < N)$
55	54	3exp	$⊢ 2^{I} \in ℤ \to (N \in ℤ \to (I \in ℕ_{0} \to (2^{I} \leq N \to 0 < N)))$
56	55	com34	$⊢ 2^{I} \in ℤ \to (N \in ℤ \to (2^{I} \leq N \to (I \in ℕ_{0} \to 0 < N)))$
57	56	3imp	$⊢ (2^{I} \in ℤ \land N \in ℤ \land 2^{I} \leq N) \to (I \in ℕ_{0} \to 0 < N)$
58	8 57	sylbi	$⊢ N \in ℤ_{\geq 2^{I}} \to (I \in ℕ_{0} \to 0 < N)$
59	58	imp	$⊢ (N \in ℤ_{\geq 2^{I}} \land I \in ℕ_{0}) \to 0 < N$
60	45 59	elrpd	$⊢ (N \in ℤ_{\geq 2^{I}} \land I \in ℕ_{0}) \to N \in ℝ^{+}$
61	60	adantlr	$⊢ ((N \in ℤ_{\geq 2^{I}} \land 2^{I + 1} \in ℤ) \land I \in ℕ_{0}) \to N \in ℝ^{+}$
62	9	a1i	$⊢ ((N \in ℤ_{\geq 2^{I}} \land 2^{I + 1} \in ℤ) \land I \in ℕ_{0}) \to 2 \in ℝ$
63		peano2nn0	$⊢ I \in ℕ_{0} \to I + 1 \in ℕ_{0}$
64	63	adantl	$⊢ ((N \in ℤ_{\geq 2^{I}} \land 2^{I + 1} \in ℤ) \land I \in ℕ_{0}) \to I + 1 \in ℕ_{0}$
65	62 64	reexpcld	$⊢ ((N \in ℤ_{\geq 2^{I}} \land 2^{I + 1} \in ℤ) \land I \in ℕ_{0}) \to 2^{I + 1} \in ℝ$
66		peano2rem	$⊢ 2^{I + 1} \in ℝ \to 2^{I + 1} - 1 \in ℝ$
67	65 66	syl	$⊢ ((N \in ℤ_{\geq 2^{I}} \land 2^{I + 1} \in ℤ) \land I \in ℕ_{0}) \to 2^{I + 1} - 1 \in ℝ$
68		nn0p1nn	$⊢ I \in ℕ_{0} \to I + 1 \in ℕ$
69		1lt2	$⊢ 1 < 2$
70	69	a1i	$⊢ I \in ℕ_{0} \to 1 < 2$
71	46 68 70	3jca	$⊢ I \in ℕ_{0} \to (2 \in ℝ \land I + 1 \in ℕ \land 1 < 2)$
72	71	adantl	$⊢ ((N \in ℤ_{\geq 2^{I}} \land 2^{I + 1} \in ℤ) \land I \in ℕ_{0}) \to (2 \in ℝ \land I + 1 \in ℕ \land 1 < 2)$
73		expgt1	$⊢ (2 \in ℝ \land I + 1 \in ℕ \land 1 < 2) \to 1 < 2^{I + 1}$
74	72 73	syl	$⊢ ((N \in ℤ_{\geq 2^{I}} \land 2^{I + 1} \in ℤ) \land I \in ℕ_{0}) \to 1 < 2^{I + 1}$
75		1red	$⊢ ((N \in ℤ_{\geq 2^{I}} \land 2^{I + 1} \in ℤ) \land I \in ℕ_{0}) \to 1 \in ℝ$
76		zre	$⊢ 2^{I + 1} \in ℤ \to 2^{I + 1} \in ℝ$
77	76	ad2antlr	$⊢ ((N \in ℤ_{\geq 2^{I}} \land 2^{I + 1} \in ℤ) \land I \in ℕ_{0}) \to 2^{I + 1} \in ℝ$
78	75 77	posdifd	$⊢ ((N \in ℤ_{\geq 2^{I}} \land 2^{I + 1} \in ℤ) \land I \in ℕ_{0}) \to (1 < 2^{I + 1} \leftrightarrow 0 < 2^{I + 1} - 1)$
79	74 78	mpbid	$⊢ ((N \in ℤ_{\geq 2^{I}} \land 2^{I + 1} \in ℤ) \land I \in ℕ_{0}) \to 0 < 2^{I + 1} - 1$
80	67 79	elrpd	$⊢ ((N \in ℤ_{\geq 2^{I}} \land 2^{I + 1} \in ℤ) \land I \in ℕ_{0}) \to 2^{I + 1} - 1 \in ℝ^{+}$
81		logbleb	$⊢ (2 \in ℤ_{\geq 2} \land N \in ℝ^{+} \land 2^{I + 1} - 1 \in ℝ^{+}) \to (N \leq 2^{I + 1} - 1 \leftrightarrow \log_{2} N \leq \log_{2} (2^{I + 1} - 1))$
82	43 61 80 81	mp3an2i	$⊢ ((N \in ℤ_{\geq 2^{I}} \land 2^{I + 1} \in ℤ) \land I \in ℕ_{0}) \to (N \leq 2^{I + 1} - 1 \leftrightarrow \log_{2} N \leq \log_{2} (2^{I + 1} - 1))$
83	44	adantr	$⊢ (N \in ℤ_{\geq 2^{I}} \land 2^{I + 1} \in ℤ) \to N \in ℝ$
84	83	adantr	$⊢ ((N \in ℤ_{\geq 2^{I}} \land 2^{I + 1} \in ℤ) \land I \in ℕ_{0}) \to N \in ℝ$
85	59	adantlr	$⊢ ((N \in ℤ_{\geq 2^{I}} \land 2^{I + 1} \in ℤ) \land I \in ℕ_{0}) \to 0 < N$
86	84 85	elrpd	$⊢ ((N \in ℤ_{\geq 2^{I}} \land 2^{I + 1} \in ℤ) \land I \in ℕ_{0}) \to N \in ℝ^{+}$
87	33	a1i	$⊢ ((N \in ℤ_{\geq 2^{I}} \land 2^{I + 1} \in ℤ) \land I \in ℕ_{0}) \to 2 \neq 1$
88	3 86 87 35	mp3an2i	$⊢ ((N \in ℤ_{\geq 2^{I}} \land 2^{I + 1} \in ℤ) \land I \in ℕ_{0}) \to \log_{2} N \in ℝ$
89	88	adantr	$⊢ (((N \in ℤ_{\geq 2^{I}} \land 2^{I + 1} \in ℤ) \land I \in ℕ_{0}) \land \log_{2} N \leq \log_{2} (2^{I + 1} - 1)) \to \log_{2} N \in ℝ$
90	43	a1i	$⊢ I \in ℕ_{0} \to 2 \in ℤ_{\geq 2}$
91	46 63	reexpcld	$⊢ I \in ℕ_{0} \to 2^{I + 1} \in ℝ$
92	91 66	syl	$⊢ I \in ℕ_{0} \to 2^{I + 1} - 1 \in ℝ$
93	9 68 70 73	mp3an2i	$⊢ I \in ℕ_{0} \to 1 < 2^{I + 1}$
94		1red	$⊢ I \in ℕ_{0} \to 1 \in ℝ$
95	94 91	posdifd	$⊢ I \in ℕ_{0} \to (1 < 2^{I + 1} \leftrightarrow 0 < 2^{I + 1} - 1)$
96	93 95	mpbid	$⊢ I \in ℕ_{0} \to 0 < 2^{I + 1} - 1$
97	92 96	elrpd	$⊢ I \in ℕ_{0} \to 2^{I + 1} - 1 \in ℝ^{+}$
98	90 97	jca	$⊢ I \in ℕ_{0} \to (2 \in ℤ_{\geq 2} \land 2^{I + 1} - 1 \in ℝ^{+})$
99	98	adantl	$⊢ ((N \in ℤ_{\geq 2^{I}} \land 2^{I + 1} \in ℤ) \land I \in ℕ_{0}) \to (2 \in ℤ_{\geq 2} \land 2^{I + 1} - 1 \in ℝ^{+})$
100		relogbzcl	$⊢ (2 \in ℤ_{\geq 2} \land 2^{I + 1} - 1 \in ℝ^{+}) \to \log_{2} (2^{I + 1} - 1) \in ℝ$
101	99 100	syl	$⊢ ((N \in ℤ_{\geq 2^{I}} \land 2^{I + 1} \in ℤ) \land I \in ℕ_{0}) \to \log_{2} (2^{I + 1} - 1) \in ℝ$
102	101	adantr	$⊢ (((N \in ℤ_{\geq 2^{I}} \land 2^{I + 1} \in ℤ) \land I \in ℕ_{0}) \land \log_{2} N \leq \log_{2} (2^{I + 1} - 1)) \to \log_{2} (2^{I + 1} - 1) \in ℝ$
103		simpr	$⊢ (((N \in ℤ_{\geq 2^{I}} \land 2^{I + 1} \in ℤ) \land I \in ℕ_{0}) \land \log_{2} N \leq \log_{2} (2^{I + 1} - 1)) \to \log_{2} N \leq \log_{2} (2^{I + 1} - 1)$
104		flwordi	$⊢ (\log_{2} N \in ℝ \land \log_{2} (2^{I + 1} - 1) \in ℝ \land \log_{2} N \leq \log_{2} (2^{I + 1} - 1)) \to ⌊\log_{2} N⌋ \leq ⌊\log_{2} (2^{I + 1} - 1)⌋$
105	89 102 103 104	syl3anc	$⊢ (((N \in ℤ_{\geq 2^{I}} \land 2^{I + 1} \in ℤ) \land I \in ℕ_{0}) \land \log_{2} N \leq \log_{2} (2^{I + 1} - 1)) \to ⌊\log_{2} N⌋ \leq ⌊\log_{2} (2^{I + 1} - 1)⌋$
106	105	ex	$⊢ ((N \in ℤ_{\geq 2^{I}} \land 2^{I + 1} \in ℤ) \land I \in ℕ_{0}) \to (\log_{2} N \leq \log_{2} (2^{I + 1} - 1) \to ⌊\log_{2} N⌋ \leq ⌊\log_{2} (2^{I + 1} - 1)⌋)$
107	68	adantl	$⊢ ((N \in ℤ_{\geq 2^{I}} \land 2^{I + 1} \in ℤ) \land I \in ℕ_{0}) \to I + 1 \in ℕ$
108		logbpw2m1	$⊢ I + 1 \in ℕ \to ⌊\log_{2} (2^{I + 1} - 1)⌋ = I + 1 - 1$
109	107 108	syl	$⊢ ((N \in ℤ_{\geq 2^{I}} \land 2^{I + 1} \in ℤ) \land I \in ℕ_{0}) \to ⌊\log_{2} (2^{I + 1} - 1)⌋ = I + 1 - 1$
110		nn0cn	$⊢ I \in ℕ_{0} \to I \in ℂ$
111		pncan1	$⊢ I \in ℂ \to I + 1 - 1 = I$
112	110 111	syl	$⊢ I \in ℕ_{0} \to I + 1 - 1 = I$
113	112	adantl	$⊢ ((N \in ℤ_{\geq 2^{I}} \land 2^{I + 1} \in ℤ) \land I \in ℕ_{0}) \to I + 1 - 1 = I$
114	109 113	eqtrd	$⊢ ((N \in ℤ_{\geq 2^{I}} \land 2^{I + 1} \in ℤ) \land I \in ℕ_{0}) \to ⌊\log_{2} (2^{I + 1} - 1)⌋ = I$
115	114	breq2d	$⊢ ((N \in ℤ_{\geq 2^{I}} \land 2^{I + 1} \in ℤ) \land I \in ℕ_{0}) \to (⌊\log_{2} N⌋ \leq ⌊\log_{2} (2^{I + 1} - 1)⌋ \leftrightarrow ⌊\log_{2} N⌋ \leq I)$
116	106 115	sylibd	$⊢ ((N \in ℤ_{\geq 2^{I}} \land 2^{I + 1} \in ℤ) \land I \in ℕ_{0}) \to (\log_{2} N \leq \log_{2} (2^{I + 1} - 1) \to ⌊\log_{2} N⌋ \leq I)$
117	82 116	sylbid	$⊢ ((N \in ℤ_{\geq 2^{I}} \land 2^{I + 1} \in ℤ) \land I \in ℕ_{0}) \to (N \leq 2^{I + 1} - 1 \to ⌊\log_{2} N⌋ \leq I)$
118	117	ex	$⊢ (N \in ℤ_{\geq 2^{I}} \land 2^{I + 1} \in ℤ) \to (I \in ℕ_{0} \to (N \leq 2^{I + 1} - 1 \to ⌊\log_{2} N⌋ \leq I))$
119	118	com23	$⊢ (N \in ℤ_{\geq 2^{I}} \land 2^{I + 1} \in ℤ) \to (N \leq 2^{I + 1} - 1 \to (I \in ℕ_{0} \to ⌊\log_{2} N⌋ \leq I))$
120	40 119	sylbid	$⊢ (N \in ℤ_{\geq 2^{I}} \land 2^{I + 1} \in ℤ) \to (N < 2^{I + 1} \to (I \in ℕ_{0} \to ⌊\log_{2} N⌋ \leq I))$
121	120	3impia	$⊢ (N \in ℤ_{\geq 2^{I}} \land 2^{I + 1} \in ℤ \land N < 2^{I + 1}) \to (I \in ℕ_{0} \to ⌊\log_{2} N⌋ \leq I)$
122	7 121	sylbi	$⊢ N \in (2^{I} ..^2^{I + 1}) \to (I \in ℕ_{0} \to ⌊\log_{2} N⌋ \leq I)$
123	122	impcom	$⊢ (I \in ℕ_{0} \land N \in (2^{I} ..^2^{I + 1})) \to ⌊\log_{2} N⌋ \leq I$
124		nn0re	$⊢ I \in ℕ_{0} \to I \in ℝ$
125		nn0ge0	$⊢ I \in ℕ_{0} \to 0 \leq I$
126		flge0nn0	$⊢ (I \in ℝ \land 0 \leq I) \to ⌊I⌋ \in ℕ_{0}$
127	124 125 126	syl2anc	$⊢ I \in ℕ_{0} \to ⌊I⌋ \in ℕ_{0}$
128	127	nn0red	$⊢ I \in ℕ_{0} \to ⌊I⌋ \in ℝ$
129	128	adantr	$⊢ (I \in ℕ_{0} \land N \in (2^{I} ..^2^{I + 1})) \to ⌊I⌋ \in ℝ$
130	124	adantr	$⊢ (I \in ℕ_{0} \land N \in (2^{I} ..^2^{I + 1})) \to I \in ℝ$
131		flle	$⊢ I \in ℝ \to ⌊I⌋ \leq I$
132	124 131	syl	$⊢ I \in ℕ_{0} \to ⌊I⌋ \leq I$
133	132	adantr	$⊢ (I \in ℕ_{0} \land N \in (2^{I} ..^2^{I + 1})) \to ⌊I⌋ \leq I$
134	3	a1i	$⊢ I \in ℕ_{0} \to 2 \in ℝ^{+}$
135	134 1	rpexpcld	$⊢ I \in ℕ_{0} \to 2^{I} \in ℝ^{+}$
136	33	a1i	$⊢ I \in ℕ_{0} \to 2 \neq 1$
137		relogbcl	$⊢ (2 \in ℝ^{+} \land 2^{I} \in ℝ^{+} \land 2 \neq 1) \to \log_{2} 2^{I} \in ℝ$
138	3 135 136 137	mp3an2i	$⊢ I \in ℕ_{0} \to \log_{2} 2^{I} \in ℝ$
139	138	adantr	$⊢ (I \in ℕ_{0} \land N \in (2^{I} ..^2^{I + 1})) \to \log_{2} 2^{I} \in ℝ$
140		nnlogbexp	$⊢ (2 \in ℤ_{\geq 2} \land I \in ℤ) \to \log_{2} 2^{I} = I$
141	90 1 140	syl2anc	$⊢ I \in ℕ_{0} \to \log_{2} 2^{I} = I$
142	141	eqcomd	$⊢ I \in ℕ_{0} \to I = \log_{2} 2^{I}$
143	124 142	eqled	$⊢ I \in ℕ_{0} \to I \leq \log_{2} 2^{I}$
144	143	adantr	$⊢ (I \in ℕ_{0} \land N \in (2^{I} ..^2^{I + 1})) \to I \leq \log_{2} 2^{I}$
145		elfzole1	$⊢ N \in (2^{I} ..^2^{I + 1}) \to 2^{I} \leq N$
146	145	adantl	$⊢ (I \in ℕ_{0} \land N \in (2^{I} ..^2^{I + 1})) \to 2^{I} \leq N$
147	135	adantr	$⊢ (I \in ℕ_{0} \land N \in (2^{I} ..^2^{I + 1})) \to 2^{I} \in ℝ^{+}$
148		logbleb	$⊢ (2 \in ℤ_{\geq 2} \land 2^{I} \in ℝ^{+} \land N \in ℝ^{+}) \to (2^{I} \leq N \leftrightarrow \log_{2} 2^{I} \leq \log_{2} N)$
149	43 147 31 148	mp3an2i	$⊢ (I \in ℕ_{0} \land N \in (2^{I} ..^2^{I + 1})) \to (2^{I} \leq N \leftrightarrow \log_{2} 2^{I} \leq \log_{2} N)$
150	146 149	mpbid	$⊢ (I \in ℕ_{0} \land N \in (2^{I} ..^2^{I + 1})) \to \log_{2} 2^{I} \leq \log_{2} N$
151	130 139 36 144 150	letrd	$⊢ (I \in ℕ_{0} \land N \in (2^{I} ..^2^{I + 1})) \to I \leq \log_{2} N$
152	129 130 36 133 151	letrd	$⊢ (I \in ℕ_{0} \land N \in (2^{I} ..^2^{I + 1})) \to ⌊I⌋ \leq \log_{2} N$
153		flflp1	$⊢ (I \in ℝ \land \log_{2} N \in ℝ) \to (⌊I⌋ \leq \log_{2} N \leftrightarrow I < ⌊\log_{2} N⌋ + 1)$
154	130 36 153	syl2anc	$⊢ (I \in ℕ_{0} \land N \in (2^{I} ..^2^{I + 1})) \to (⌊I⌋ \leq \log_{2} N \leftrightarrow I < ⌊\log_{2} N⌋ + 1)$
155	152 154	mpbid	$⊢ (I \in ℕ_{0} \land N \in (2^{I} ..^2^{I + 1})) \to I < ⌊\log_{2} N⌋ + 1$
156		zgeltp1eq	$⊢ (I \in ℤ \land ⌊\log_{2} N⌋ \in ℤ) \to ((⌊\log_{2} N⌋ \leq I \land I < ⌊\log_{2} N⌋ + 1) \to I = ⌊\log_{2} N⌋)$
157	156	imp	$⊢ ((I \in ℤ \land ⌊\log_{2} N⌋ \in ℤ) \land (⌊\log_{2} N⌋ \leq I \land I < ⌊\log_{2} N⌋ + 1)) \to I = ⌊\log_{2} N⌋$
158	2 37 123 155 157	syl22anc	$⊢ (I \in ℕ_{0} \land N \in (2^{I} ..^2^{I + 1})) \to I = ⌊\log_{2} N⌋$
159	158	eqcomd	$⊢ (I \in ℕ_{0} \land N \in (2^{I} ..^2^{I + 1})) \to ⌊\log_{2} N⌋ = I$

Metamath Proof Explorer

Theorem fllog2

Proof