logbpw2m1

Description: The floor of the binary logarithm of 2 to the power of a positive integer minus 1 is equal to the integer minus 1. (Contributed by AV, 31-May-2020)

		Ref	Expression
	Assertion	logbpw2m1	$⊢ I \in ℕ \to ⌊\log_{2} (2^{I} - 1)⌋ = I - 1$

Proof

Step	Hyp	Ref	Expression
1		2rp	$⊢ 2 \in ℝ^{+}$
2	1	a1i	$⊢ I \in ℕ \to 2 \in ℝ^{+}$
3		2nn0	$⊢ 2 \in ℕ_{0}$
4	3	a1i	$⊢ I \in ℕ \to 2 \in ℕ_{0}$
5		nnnn0	$⊢ I \in ℕ \to I \in ℕ_{0}$
6	4 5	nn0expcld	$⊢ I \in ℕ \to 2^{I} \in ℕ_{0}$
7		nnge1	$⊢ I \in ℕ \to 1 \leq I$
8		2re	$⊢ 2 \in ℝ$
9	8	a1i	$⊢ I \in ℕ \to 2 \in ℝ$
10		1zzd	$⊢ I \in ℕ \to 1 \in ℤ$
11		nnz	$⊢ I \in ℕ \to I \in ℤ$
12		1lt2	$⊢ 1 < 2$
13	12	a1i	$⊢ I \in ℕ \to 1 < 2$
14	9 10 11 13	leexp2d	$⊢ I \in ℕ \to (1 \leq I \leftrightarrow 2^{1} \leq 2^{I})$
15		2cn	$⊢ 2 \in ℂ$
16		exp1	$⊢ 2 \in ℂ \to 2^{1} = 2$
17	15 16	ax-mp	$⊢ 2^{1} = 2$
18	17	a1i	$⊢ I \in ℕ \to 2^{1} = 2$
19	18	breq1d	$⊢ I \in ℕ \to (2^{1} \leq 2^{I} \leftrightarrow 2 \leq 2^{I})$
20	14 19	bitrd	$⊢ I \in ℕ \to (1 \leq I \leftrightarrow 2 \leq 2^{I})$
21	7 20	mpbid	$⊢ I \in ℕ \to 2 \leq 2^{I}$
22		nn0ge2m1nn	$⊢ (2^{I} \in ℕ_{0} \land 2 \leq 2^{I}) \to 2^{I} - 1 \in ℕ$
23	6 21 22	syl2anc	$⊢ I \in ℕ \to 2^{I} - 1 \in ℕ$
24	23	nnrpd	$⊢ I \in ℕ \to 2^{I} - 1 \in ℝ^{+}$
25		1ne2	$⊢ 1 \neq 2$
26	25	necomi	$⊢ 2 \neq 1$
27	26	a1i	$⊢ I \in ℕ \to 2 \neq 1$
28		relogbcl	$⊢ (2 \in ℝ^{+} \land 2^{I} - 1 \in ℝ^{+} \land 2 \neq 1) \to \log_{2} (2^{I} - 1) \in ℝ$
29	2 24 27 28	syl3anc	$⊢ I \in ℕ \to \log_{2} (2^{I} - 1) \in ℝ$
30	29	flcld	$⊢ I \in ℕ \to ⌊\log_{2} (2^{I} - 1)⌋ \in ℤ$
31		peano2zm	$⊢ I \in ℤ \to I - 1 \in ℤ$
32	11 31	syl	$⊢ I \in ℕ \to I - 1 \in ℤ$
33		2z	$⊢ 2 \in ℤ$
34		uzid	$⊢ 2 \in ℤ \to 2 \in ℤ_{\geq 2}$
35	33 34	ax-mp	$⊢ 2 \in ℤ_{\geq 2}$
36		nnlogbexp	$⊢ (2 \in ℤ_{\geq 2} \land I - 1 \in ℤ) \to \log_{2} 2^{I - 1} = I - 1$
37	35 32 36	sylancr	$⊢ I \in ℕ \to \log_{2} 2^{I - 1} = I - 1$
38	37	fveq2d	$⊢ I \in ℕ \to ⌊\log_{2} 2^{I - 1}⌋ = ⌊I - 1⌋$
39		flid	$⊢ I - 1 \in ℤ \to ⌊I - 1⌋ = I - 1$
40	32 39	syl	$⊢ I \in ℕ \to ⌊I - 1⌋ = I - 1$
41	38 40	eqtrd	$⊢ I \in ℕ \to ⌊\log_{2} 2^{I - 1}⌋ = I - 1$
42		2nn	$⊢ 2 \in ℕ$
43	42	a1i	$⊢ I \in ℕ \to 2 \in ℕ$
44		nnm1nn0	$⊢ I \in ℕ \to I - 1 \in ℕ_{0}$
45	43 44	nnexpcld	$⊢ I \in ℕ \to 2^{I - 1} \in ℕ$
46	45	nnrpd	$⊢ I \in ℕ \to 2^{I - 1} \in ℝ^{+}$
47		relogbcl	$⊢ (2 \in ℝ^{+} \land 2^{I - 1} \in ℝ^{+} \land 2 \neq 1) \to \log_{2} 2^{I - 1} \in ℝ$
48	2 46 27 47	syl3anc	$⊢ I \in ℕ \to \log_{2} 2^{I - 1} \in ℝ$
49		pw2m1lepw2m1	$⊢ I \in ℕ \to 2^{I - 1} \leq 2^{I} - 1$
50	35	a1i	$⊢ I \in ℕ \to 2 \in ℤ_{\geq 2}$
51		logbleb	$⊢ (2 \in ℤ_{\geq 2} \land 2^{I - 1} \in ℝ^{+} \land 2^{I} - 1 \in ℝ^{+}) \to (2^{I - 1} \leq 2^{I} - 1 \leftrightarrow \log_{2} 2^{I - 1} \leq \log_{2} (2^{I} - 1))$
52	50 46 24 51	syl3anc	$⊢ I \in ℕ \to (2^{I - 1} \leq 2^{I} - 1 \leftrightarrow \log_{2} 2^{I - 1} \leq \log_{2} (2^{I} - 1))$
53	49 52	mpbid	$⊢ I \in ℕ \to \log_{2} 2^{I - 1} \leq \log_{2} (2^{I} - 1)$
54		flwordi	$⊢ (\log_{2} 2^{I - 1} \in ℝ \land \log_{2} (2^{I} - 1) \in ℝ \land \log_{2} 2^{I - 1} \leq \log_{2} (2^{I} - 1)) \to ⌊\log_{2} 2^{I - 1}⌋ \leq ⌊\log_{2} (2^{I} - 1)⌋$
55	48 29 53 54	syl3anc	$⊢ I \in ℕ \to ⌊\log_{2} 2^{I - 1}⌋ \leq ⌊\log_{2} (2^{I} - 1)⌋$
56	41 55	eqbrtrrd	$⊢ I \in ℕ \to I - 1 \leq ⌊\log_{2} (2^{I} - 1)⌋$
57	43 5	nnexpcld	$⊢ I \in ℕ \to 2^{I} \in ℕ$
58	57	nnnn0d	$⊢ I \in ℕ \to 2^{I} \in ℕ_{0}$
59	58 21 22	syl2anc	$⊢ I \in ℕ \to 2^{I} - 1 \in ℕ$
60	59	nnrpd	$⊢ I \in ℕ \to 2^{I} - 1 \in ℝ^{+}$
61	2 60 27 28	syl3anc	$⊢ I \in ℕ \to \log_{2} (2^{I} - 1) \in ℝ$
62	61	flcld	$⊢ I \in ℕ \to ⌊\log_{2} (2^{I} - 1)⌋ \in ℤ$
63	62	zred	$⊢ I \in ℕ \to ⌊\log_{2} (2^{I} - 1)⌋ \in ℝ$
64		nnre	$⊢ I \in ℕ \to I \in ℝ$
65		peano2rem	$⊢ I \in ℝ \to I - 1 \in ℝ$
66	64 65	syl	$⊢ I \in ℕ \to I - 1 \in ℝ$
67		peano2re	$⊢ I - 1 \in ℝ \to I - 1 + 1 \in ℝ$
68	66 67	syl	$⊢ I \in ℕ \to I - 1 + 1 \in ℝ$
69		flle	$⊢ \log_{2} (2^{I} - 1) \in ℝ \to ⌊\log_{2} (2^{I} - 1)⌋ \leq \log_{2} (2^{I} - 1)$
70	29 69	syl	$⊢ I \in ℕ \to ⌊\log_{2} (2^{I} - 1)⌋ \leq \log_{2} (2^{I} - 1)$
71	57	nnrpd	$⊢ I \in ℕ \to 2^{I} \in ℝ^{+}$
72		relogbcl	$⊢ (2 \in ℝ^{+} \land 2^{I} \in ℝ^{+} \land 2 \neq 1) \to \log_{2} 2^{I} \in ℝ$
73	2 71 27 72	syl3anc	$⊢ I \in ℕ \to \log_{2} 2^{I} \in ℝ$
74	57	nnred	$⊢ I \in ℕ \to 2^{I} \in ℝ$
75	74	ltm1d	$⊢ I \in ℕ \to 2^{I} - 1 < 2^{I}$
76		logblt	$⊢ (2 \in ℤ_{\geq 2} \land 2^{I} - 1 \in ℝ^{+} \land 2^{I} \in ℝ^{+}) \to (2^{I} - 1 < 2^{I} \leftrightarrow \log_{2} (2^{I} - 1) < \log_{2} 2^{I})$
77	50 24 71 76	syl3anc	$⊢ I \in ℕ \to (2^{I} - 1 < 2^{I} \leftrightarrow \log_{2} (2^{I} - 1) < \log_{2} 2^{I})$
78	75 77	mpbid	$⊢ I \in ℕ \to \log_{2} (2^{I} - 1) < \log_{2} 2^{I}$
79	64	leidd	$⊢ I \in ℕ \to I \leq I$
80		nnlogbexp	$⊢ (2 \in ℤ_{\geq 2} \land I \in ℤ) \to \log_{2} 2^{I} = I$
81	35 11 80	sylancr	$⊢ I \in ℕ \to \log_{2} 2^{I} = I$
82		nncn	$⊢ I \in ℕ \to I \in ℂ$
83		npcan1	$⊢ I \in ℂ \to I - 1 + 1 = I$
84	82 83	syl	$⊢ I \in ℕ \to I - 1 + 1 = I$
85	79 81 84	3brtr4d	$⊢ I \in ℕ \to \log_{2} 2^{I} \leq I - 1 + 1$
86	29 73 68 78 85	ltletrd	$⊢ I \in ℕ \to \log_{2} (2^{I} - 1) < I - 1 + 1$
87	63 29 68 70 86	lelttrd	$⊢ I \in ℕ \to ⌊\log_{2} (2^{I} - 1)⌋ < I - 1 + 1$
88		zgeltp1eq	$⊢ (⌊\log_{2} (2^{I} - 1)⌋ \in ℤ \land I - 1 \in ℤ) \to ((I - 1 \leq ⌊\log_{2} (2^{I} - 1)⌋ \land ⌊\log_{2} (2^{I} - 1)⌋ < I - 1 + 1) \to ⌊\log_{2} (2^{I} - 1)⌋ = I - 1)$
89	88	imp	$⊢ ((⌊\log_{2} (2^{I} - 1)⌋ \in ℤ \land I - 1 \in ℤ) \land (I - 1 \leq ⌊\log_{2} (2^{I} - 1)⌋ \land ⌊\log_{2} (2^{I} - 1)⌋ < I - 1 + 1)) \to ⌊\log_{2} (2^{I} - 1)⌋ = I - 1$
90	30 32 56 87 89	syl22anc	$⊢ I \in ℕ \to ⌊\log_{2} (2^{I} - 1)⌋ = I - 1$

Metamath Proof Explorer

Theorem logbpw2m1

Proof