nnolog2flm1

Description: The floor of the binary logarithm of an odd integer greater than 1 is the floor of the binary logarithm of the integer decreased by 1. (Contributed by AV, 2-Jun-2020)

		Ref	Expression
	Assertion	nnolog2flm1	$⊢ (N \in ℤ_{\geq 2} \land \frac{N + 1}{2} \in ℕ) \to ⌊\log_{2} N⌋ = ⌊\log_{2} (N - 1)⌋$

Proof

Step	Hyp	Ref	Expression
1		eluz2nn	$⊢ N \in ℤ_{\geq 2} \to N \in ℕ$
2		nnpw2blenfzo2	$⊢ N \in ℕ \to (N = 2^{#_{b(N)-1\lorN \in (2^{#_{b} (N) - 1} + 1 ..^2^{#_{b} (N)})}})$
3	1 2	syl	$⊢ N \in ℤ_{\geq 2} \to (N = 2^{#_{b(N)-1\lorN \in (2^{#_{b} (N) - 1} + 1 ..^2^{#_{b} (N)})}})$
4	1	adantl	$⊢ (N = 2^{#_{b(N)-1\landN \in ℤ_{\geq 2}\toN \in ℕ}})$
5		nneo	$⊢ N \in ℕ \to (\frac{N}{2} \in ℕ \leftrightarrow \neg \frac{N + 1}{2} \in ℕ)$
6	5	bicomd	$⊢ N \in ℕ \to (\neg \frac{N + 1}{2} \in ℕ \leftrightarrow \frac{N}{2} \in ℕ)$
7	4 6	syl	$⊢ (N = 2^{#_{b(N)-1\landN \in ℤ_{\geq 2}\to(\neg \frac{N + 1}{2} \in ℕ \leftrightarrow \frac{N}{2} \in ℕ)}})$
8		notnotb	$⊢ \frac{N}{2} \in ℕ \leftrightarrow \neg \neg \frac{N}{2} \in ℕ$
9	7 8	bitrdi	$⊢ (N = 2^{#_{b(N)-1\landN \in ℤ_{\geq 2}\to(\neg \frac{N + 1}{2} \in ℕ \leftrightarrow \neg \neg \frac{N}{2} \in ℕ)}})$
10	9	con4bid	$⊢ (N = 2^{#_{b(N)-1\landN \in ℤ_{\geq 2}\to(\frac{N + 1}{2} \in ℕ \leftrightarrow \neg \frac{N}{2} \in ℕ)}})$
11		simpl	$⊢ (N = 2^{#_{b(N)-1\landN \in ℤ_{\geq 2}\toN = 2^{#_{b} (N) - 1}}})$
12	11	oveq1d	$⊢ (N = 2^{#_{b(N)-1\landN \in ℤ_{\geq 2}\to\frac{N}{2} = \frac{2^{#_{b} (N) - 1}}{2}}})$
13		blennnelnn	$⊢ N \in ℕ \to #_{b(N)\inℕ}$
14	13	nnnn0d	$⊢ N \in ℕ \to #_{b(N)\inℕ_{0}}$
15	1 14	syl	$⊢ N \in ℤ_{\geq 2} \to #_{b(N)\inℕ_{0}}$
16		2m1e1	$⊢ 2 - 1 = 1$
17		2cn	$⊢ 2 \in ℂ$
18		2ne0	$⊢ 2 \neq 0$
19		1ne2	$⊢ 1 \neq 2$
20	19	necomi	$⊢ 2 \neq 1$
21		logbid1	$⊢ (2 \in ℂ \land 2 \neq 0 \land 2 \neq 1) \to \log_{2} 2 = 1$
22	17 18 20 21	mp3an	$⊢ \log_{2} 2 = 1$
23		eluzle	$⊢ N \in ℤ_{\geq 2} \to 2 \leq N$
24		2z	$⊢ 2 \in ℤ$
25		uzid	$⊢ 2 \in ℤ \to 2 \in ℤ_{\geq 2}$
26	24 25	mp1i	$⊢ N \in ℤ_{\geq 2} \to 2 \in ℤ_{\geq 2}$
27		2rp	$⊢ 2 \in ℝ^{+}$
28	27	a1i	$⊢ N \in ℤ_{\geq 2} \to 2 \in ℝ^{+}$
29	1	nnrpd	$⊢ N \in ℤ_{\geq 2} \to N \in ℝ^{+}$
30		logbleb	$⊢ (2 \in ℤ_{\geq 2} \land 2 \in ℝ^{+} \land N \in ℝ^{+}) \to (2 \leq N \leftrightarrow \log_{2} 2 \leq \log_{2} N)$
31	26 28 29 30	syl3anc	$⊢ N \in ℤ_{\geq 2} \to (2 \leq N \leftrightarrow \log_{2} 2 \leq \log_{2} N)$
32	23 31	mpbid	$⊢ N \in ℤ_{\geq 2} \to \log_{2} 2 \leq \log_{2} N$
33	22 32	eqbrtrrid	$⊢ N \in ℤ_{\geq 2} \to 1 \leq \log_{2} N$
34	20	a1i	$⊢ N \in ℤ_{\geq 2} \to 2 \neq 1$
35		relogbcl	$⊢ (2 \in ℝ^{+} \land N \in ℝ^{+} \land 2 \neq 1) \to \log_{2} N \in ℝ$
36	28 29 34 35	syl3anc	$⊢ N \in ℤ_{\geq 2} \to \log_{2} N \in ℝ$
37		1zzd	$⊢ N \in ℤ_{\geq 2} \to 1 \in ℤ$
38		flge	$⊢ (\log_{2} N \in ℝ \land 1 \in ℤ) \to (1 \leq \log_{2} N \leftrightarrow 1 \leq ⌊\log_{2} N⌋)$
39	36 37 38	syl2anc	$⊢ N \in ℤ_{\geq 2} \to (1 \leq \log_{2} N \leftrightarrow 1 \leq ⌊\log_{2} N⌋)$
40	33 39	mpbid	$⊢ N \in ℤ_{\geq 2} \to 1 \leq ⌊\log_{2} N⌋$
41	16 40	eqbrtrid	$⊢ N \in ℤ_{\geq 2} \to 2 - 1 \leq ⌊\log_{2} N⌋$
42		2re	$⊢ 2 \in ℝ$
43	42	a1i	$⊢ N \in ℤ_{\geq 2} \to 2 \in ℝ$
44		1red	$⊢ N \in ℤ_{\geq 2} \to 1 \in ℝ$
45	36	flcld	$⊢ N \in ℤ_{\geq 2} \to ⌊\log_{2} N⌋ \in ℤ$
46	45	zred	$⊢ N \in ℤ_{\geq 2} \to ⌊\log_{2} N⌋ \in ℝ$
47	43 44 46	lesubaddd	$⊢ N \in ℤ_{\geq 2} \to (2 - 1 \leq ⌊\log_{2} N⌋ \leftrightarrow 2 \leq ⌊\log_{2} N⌋ + 1)$
48	41 47	mpbid	$⊢ N \in ℤ_{\geq 2} \to 2 \leq ⌊\log_{2} N⌋ + 1$
49		blennn	$⊢ N \in ℕ \to #_{b(N)=⌊\log_{2} N⌋ + 1}$
50	1 49	syl	$⊢ N \in ℤ_{\geq 2} \to #_{b(N)=⌊\log_{2} N⌋ + 1}$
51	48 50	breqtrrd	$⊢ N \in ℤ_{\geq 2} \to 2 \leq #_{b(N)}$
52		nn0ge2m1nn	$⊢ (#_{b(N)\inℕ_{0}\land2 \leq #_{b} (N)\to#_{b} (N) - 1 \in ℕ})$
53	15 51 52	syl2anc	$⊢ N \in ℤ_{\geq 2} \to #_{b(N)-1\inℕ}$
54	53	adantl	$⊢ (N = 2^{#_{b(N)-1\landN \in ℤ_{\geq 2}\to#_{b} (N) - 1 \in ℕ}})$
55		nnpw2even	$⊢ #_{b(N)-1\inℕ\to\frac{2^{#_{b} (N) - 1}}{2} \in ℕ}$
56	54 55	syl	$⊢ (N = 2^{#_{b(N)-1\landN \in ℤ_{\geq 2}\to\frac{2^{#_{b} (N) - 1}}{2} \in ℕ}})$
57	12 56	eqeltrd	$⊢ (N = 2^{#_{b(N)-1\landN \in ℤ_{\geq 2}\to\frac{N}{2} \in ℕ}})$
58	57	pm2.24d	$⊢ (N = 2^{#_{b(N)-1\landN \in ℤ_{\geq 2}\to(\neg \frac{N}{2} \in ℕ \to ⌊\log_{2} N⌋ = ⌊\log_{2} (N - 1)⌋)}})$
59	10 58	sylbid	$⊢ (N = 2^{#_{b(N)-1\landN \in ℤ_{\geq 2}\to(\frac{N + 1}{2} \in ℕ \to ⌊\log_{2} N⌋ = ⌊\log_{2} (N - 1)⌋)}})$
60	59	ex	$⊢ N = 2^{#_{b(N)-1\to(N \in ℤ_{\geq 2} \to (\frac{N + 1}{2} \in ℕ \to ⌊\log_{2} N⌋ = ⌊\log_{2} (N - 1)⌋))}}$
61	1 13	syl	$⊢ N \in ℤ_{\geq 2} \to #_{b(N)\inℕ}$
62		nnm1nn0	$⊢ #_{b(N)\inℕ\to#_{b} (N) - 1 \in ℕ_{0}}$
63	61 62	syl	$⊢ N \in ℤ_{\geq 2} \to #_{b(N)-1\inℕ_{0}}$
64	63	ad2antlr	$⊢ ((N \in (2^{#_{b(N)-1+1..^2^{#_{b} (N)}\landN \in ℤ_{\geq 2}\land\frac{N + 1}{2} \in ℕ\to#_{b} (N) - 1 \in ℕ_{0}}})))$
65	1	ad2antlr	$⊢ ((N \in (2^{#_{b(N)-1+1..^2^{#_{b} (N)}\landN \in ℤ_{\geq 2}\land\frac{N + 1}{2} \in ℕ\toN \in ℕ}})))$
66		nnpw2blenfzo	$⊢ N \in ℕ \to N \in (2^{#_{b(N)-1..^2^{#_{b} (N)}}})$
67	65 66	syl	$⊢ ((N \in (2^{#_{b(N)-1+1..^2^{#_{b} (N)}\landN \in ℤ_{\geq 2}\land\frac{N + 1}{2} \in ℕ\toN \in (2^{#_{b} (N) - 1} ..^2^{#_{b} (N)})}})))$
68	61	nncnd	$⊢ N \in ℤ_{\geq 2} \to #_{b(N)\inℂ}$
69	68	ad2antlr	$⊢ ((N \in (2^{#_{b(N)-1+1..^2^{#_{b} (N)}\landN \in ℤ_{\geq 2}\land\frac{N + 1}{2} \in ℕ\to#_{b} (N) \in ℂ}})))$
70		npcan1	$⊢ #_{b(N)\inℂ\to#_{b} (N) - 1 + 1 = #_{b} (N)}$
71	69 70	syl	$⊢ ((N \in (2^{#_{b(N)-1+1..^2^{#_{b} (N)}\landN \in ℤ_{\geq 2}\land\frac{N + 1}{2} \in ℕ\to#_{b} (N) - 1 + 1 = #_{b} (N)}})))$
72	71	oveq2d	$⊢ ((N \in (2^{#_{b(N)-1+1..^2^{#_{b} (N)}\landN \in ℤ_{\geq 2}\land\frac{N + 1}{2} \in ℕ\to2^{#_{b} (N) - 1 + 1} = 2^{#_{b} (N)}}})))$
73	72	oveq2d	$⊢ ((N \in (2^{#_{b(N)-1+1..^2^{#_{b} (N)}\landN \in ℤ_{\geq 2}\land\frac{N + 1}{2} \in ℕ\to(2^{#_{b} (N) - 1} ..^2^{#_{b} (N) - 1 + 1}) = (2^{#_{b} (N) - 1} ..^2^{#_{b} (N)})}})))$
74	67 73	eleqtrrd	$⊢ ((N \in (2^{#_{b(N)-1+1..^2^{#_{b} (N)}\landN \in ℤ_{\geq 2}\land\frac{N + 1}{2} \in ℕ\toN \in (2^{#_{b} (N) - 1} ..^2^{#_{b} (N) - 1 + 1})}})))$
75		fllog2	$⊢ (#_{b(N)-1\inℕ_{0}\landN \in (2^{#_{b} (N) - 1} ..^2^{#_{b} (N) - 1 + 1})\to⌊\log_{2} N⌋ = #_{b} (N) - 1})$
76	64 74 75	syl2anc	$⊢ ((N \in (2^{#_{b(N)-1+1..^2^{#_{b} (N)}\landN \in ℤ_{\geq 2}\land\frac{N + 1}{2} \in ℕ\to⌊\log_{2} N⌋ = #_{b} (N) - 1}})))$
77	61	ad2antlr	$⊢ ((N \in (2^{#_{b(N)-1+1..^2^{#_{b} (N)}\landN \in ℤ_{\geq 2}\land\frac{N + 1}{2} \in ℕ\to#_{b} (N) \in ℕ}})))$
78	77 62	syl	$⊢ ((N \in (2^{#_{b(N)-1+1..^2^{#_{b} (N)}\landN \in ℤ_{\geq 2}\land\frac{N + 1}{2} \in ℕ\to#_{b} (N) - 1 \in ℕ_{0}}})))$
79		elfzo2	$⊢ N \in (2^{#_{b(N)-1+1..^2^{#_{b} (N)}\leftrightarrow(N \in ℤ_{\geq (2^{#_{b} (N) - 1} + 1)} \land 2^{#_{b} (N)} \in ℤ \land N < 2^{#_{b} (N)})}})$
80		eluz2	$⊢ N \in ℤ_{\geq (2^{#_{b(N)-1+1\leftrightarrow(2^{#_{b} (N) - 1} + 1 \in ℤ \land N \in ℤ \land 2^{#_{b} (N) - 1} + 1 \leq N)}})}$
81	80	3anbi1i	$⊢ (N \in ℤ_{\geq (2^{#_{b(N)-1+1\land2^{#_{b} (N)} \in ℤ\landN < 2^{#_{b} (N)}\leftrightarrow((2^{#_{b} (N) - 1} + 1 \in ℤ \land N \in ℤ \land 2^{#_{b} (N) - 1} + 1 \leq N) \land 2^{#_{b} (N)} \in ℤ \land N < 2^{#_{b} (N)})}})})$
82	79 81	bitri	$⊢ N \in (2^{#_{b(N)-1+1..^2^{#_{b} (N)}\leftrightarrow((2^{#_{b} (N) - 1} + 1 \in ℤ \land N \in ℤ \land 2^{#_{b} (N) - 1} + 1 \leq N) \land 2^{#_{b} (N)} \in ℤ \land N < 2^{#_{b} (N)})}})$
83		2nn	$⊢ 2 \in ℕ$
84	83	a1i	$⊢ N \in ℤ_{\geq 2} \to 2 \in ℕ$
85	84 63	jca	$⊢ N \in ℤ_{\geq 2} \to (2 \in ℕ \land #_{b(N)-1\inℕ_{0}})$
86	85	adantl	$⊢ (((2^{#_{b(N)-1+1\inℤ\landN \in ℤ\land2^{#_{b} (N) - 1} + 1 \leq N\landN < 2^{#_{b} (N)}\landN \in ℤ_{\geq 2}\to(2 \in ℕ \land #_{b} (N) - 1 \in ℕ_{0})}})))$
87		nnexpcl	$⊢ (2 \in ℕ \land #_{b(N)-1\inℕ_{0}\to2^{#_{b} (N) - 1} \in ℕ})$
88	86 87	syl	$⊢ (((2^{#_{b(N)-1+1\inℤ\landN \in ℤ\land2^{#_{b} (N) - 1} + 1 \leq N\landN < 2^{#_{b} (N)}\landN \in ℤ_{\geq 2}\to2^{#_{b} (N) - 1} \in ℕ}})))$
89	88	nnzd	$⊢ (((2^{#_{b(N)-1+1\inℤ\landN \in ℤ\land2^{#_{b} (N) - 1} + 1 \leq N\landN < 2^{#_{b} (N)}\landN \in ℤ_{\geq 2}\to2^{#_{b} (N) - 1} \in ℤ}})))$
90		peano2zm	$⊢ N \in ℤ \to N - 1 \in ℤ$
91	90	3ad2ant2	$⊢ (2^{#_{b(N)-1+1\inℤ\landN \in ℤ\land2^{#_{b} (N) - 1} + 1 \leq N\toN - 1 \in ℤ}})$
92	91	adantr	$⊢ ((2^{#_{b(N)-1+1\inℤ\landN \in ℤ\land2^{#_{b} (N) - 1} + 1 \leq N\landN < 2^{#_{b} (N)}\toN - 1 \in ℤ}}))$
93	92	adantr	$⊢ (((2^{#_{b(N)-1+1\inℤ\landN \in ℤ\land2^{#_{b} (N) - 1} + 1 \leq N\landN < 2^{#_{b} (N)}\landN \in ℤ_{\geq 2}\toN - 1 \in ℤ}})))$
94	84 63	nnexpcld	$⊢ N \in ℤ_{\geq 2} \to 2^{#_{b(N)-1\inℕ}}$
95	94	nnred	$⊢ N \in ℤ_{\geq 2} \to 2^{#_{b(N)-1\inℝ}}$
96	1	nnred	$⊢ N \in ℤ_{\geq 2} \to N \in ℝ$
97		leaddsub	$⊢ (2^{#_{b(N)-1\inℝ\land1 \in ℝ\landN \in ℝ\to(2^{#_{b} (N) - 1} + 1 \leq N \leftrightarrow 2^{#_{b} (N) - 1} \leq N - 1)}})$
98	95 44 96 97	syl3anc	$⊢ N \in ℤ_{\geq 2} \to (2^{#_{b(N)-1+1\leqN\leftrightarrow2^{#_{b} (N) - 1} \leq N - 1}})$
99	98	biimpcd	$⊢ 2^{#_{b(N)-1+1\leqN\to(N \in ℤ_{\geq 2} \to 2^{#_{b} (N) - 1} \leq N - 1)}}$
100	99	3ad2ant3	$⊢ (2^{#_{b(N)-1+1\inℤ\landN \in ℤ\land2^{#_{b} (N) - 1} + 1 \leq N\to(N \in ℤ_{\geq 2} \to 2^{#_{b} (N) - 1} \leq N - 1)}})$
101	100	adantr	$⊢ ((2^{#_{b(N)-1+1\inℤ\landN \in ℤ\land2^{#_{b} (N) - 1} + 1 \leq N\landN < 2^{#_{b} (N)}\to(N \in ℤ_{\geq 2} \to 2^{#_{b} (N) - 1} \leq N - 1)}}))$
102	101	imp	$⊢ (((2^{#_{b(N)-1+1\inℤ\landN \in ℤ\land2^{#_{b} (N) - 1} + 1 \leq N\landN < 2^{#_{b} (N)}\landN \in ℤ_{\geq 2}\to2^{#_{b} (N) - 1} \leq N - 1}})))$
103		eluz2	$⊢ N - 1 \in ℤ_{\geq 2^{#_{b(N)-1\leftrightarrow(2^{#_{b} (N) - 1} \in ℤ \land N - 1 \in ℤ \land 2^{#_{b} (N) - 1} \leq N - 1)}}}$
104	89 93 102 103	syl3anbrc	$⊢ (((2^{#_{b(N)-1+1\inℤ\landN \in ℤ\land2^{#_{b} (N) - 1} + 1 \leq N\landN < 2^{#_{b} (N)}\landN \in ℤ_{\geq 2}\toN - 1 \in ℤ_{\geq 2^{#_{b} (N) - 1}}}})))$
105	70	eleq1d	$⊢ #_{b(N)\inℂ\to(#_{b} (N) - 1 + 1 \in ℕ_{0} \leftrightarrow #_{b} (N) \in ℕ_{0})}$
106	68 105	syl	$⊢ N \in ℤ_{\geq 2} \to (#_{b(N)-1+1\inℕ_{0}\leftrightarrow#_{b} (N) \in ℕ_{0}})$
107	15 106	mpbird	$⊢ N \in ℤ_{\geq 2} \to #_{b(N)-1+1\inℕ_{0}}$
108	84 107	jca	$⊢ N \in ℤ_{\geq 2} \to (2 \in ℕ \land #_{b(N)-1+1\inℕ_{0}})$
109	108	adantl	$⊢ (((2^{#_{b(N)-1+1\inℤ\landN \in ℤ\land2^{#_{b} (N) - 1} + 1 \leq N\landN < 2^{#_{b} (N)}\landN \in ℤ_{\geq 2}\to(2 \in ℕ \land #_{b} (N) - 1 + 1 \in ℕ_{0})}})))$
110		nnexpcl	$⊢ (2 \in ℕ \land #_{b(N)-1+1\inℕ_{0}\to2^{#_{b} (N) - 1 + 1} \in ℕ})$
111	109 110	syl	$⊢ (((2^{#_{b(N)-1+1\inℤ\landN \in ℤ\land2^{#_{b} (N) - 1} + 1 \leq N\landN < 2^{#_{b} (N)}\landN \in ℤ_{\geq 2}\to2^{#_{b} (N) - 1 + 1} \in ℕ}})))$
112	111	nnzd	$⊢ (((2^{#_{b(N)-1+1\inℤ\landN \in ℤ\land2^{#_{b} (N) - 1} + 1 \leq N\landN < 2^{#_{b} (N)}\landN \in ℤ_{\geq 2}\to2^{#_{b} (N) - 1 + 1} \in ℤ}})))$
113		ltle	$⊢ (N \in ℝ \land 2^{#_{b(N)\inℝ\to(N < 2^{#_{b} (N)} \to N \leq 2^{#_{b} (N)})}})$
114		nnre	$⊢ N \in ℕ \to N \in ℝ$
115	42	a1i	$⊢ N \in ℕ \to 2 \in ℝ$
116	115 14	reexpcld	$⊢ N \in ℕ \to 2^{#_{b(N)\inℝ}}$
117	114 116	jca	$⊢ N \in ℕ \to (N \in ℝ \land 2^{#_{b(N)\inℝ}})$
118	1 117	syl	$⊢ N \in ℤ_{\geq 2} \to (N \in ℝ \land 2^{#_{b(N)\inℝ}})$
119	113 118	syl11	$⊢ N < 2^{#_{b(N)\to(N \in ℤ_{\geq 2} \to N \leq 2^{#_{b} (N)})}}$
120	119	adantl	$⊢ ((2^{#_{b(N)-1+1\inℤ\landN \in ℤ\land2^{#_{b} (N) - 1} + 1 \leq N\landN < 2^{#_{b} (N)}\to(N \in ℤ_{\geq 2} \to N \leq 2^{#_{b} (N)})}}))$
121	120	imp	$⊢ (((2^{#_{b(N)-1+1\inℤ\landN \in ℤ\land2^{#_{b} (N) - 1} + 1 \leq N\landN < 2^{#_{b} (N)}\landN \in ℤ_{\geq 2}\toN \leq 2^{#_{b} (N)}}})))$
122		simpll2	$⊢ (((2^{#_{b(N)-1+1\inℤ\landN \in ℤ\land2^{#_{b} (N) - 1} + 1 \leq N\landN < 2^{#_{b} (N)}\landN \in ℤ_{\geq 2}\toN \in ℤ}})))$
123	84 15	nnexpcld	$⊢ N \in ℤ_{\geq 2} \to 2^{#_{b(N)\inℕ}}$
124	123	nnzd	$⊢ N \in ℤ_{\geq 2} \to 2^{#_{b(N)\inℤ}}$
125	124	adantl	$⊢ (((2^{#_{b(N)-1+1\inℤ\landN \in ℤ\land2^{#_{b} (N) - 1} + 1 \leq N\landN < 2^{#_{b} (N)}\landN \in ℤ_{\geq 2}\to2^{#_{b} (N)} \in ℤ}})))$
126		zlem1lt	$⊢ (N \in ℤ \land 2^{#_{b(N)\inℤ\to(N \leq 2^{#_{b} (N)} \leftrightarrow N - 1 < 2^{#_{b} (N)})}})$
127	122 125 126	syl2anc	$⊢ (((2^{#_{b(N)-1+1\inℤ\landN \in ℤ\land2^{#_{b} (N) - 1} + 1 \leq N\landN < 2^{#_{b} (N)}\landN \in ℤ_{\geq 2}\to(N \leq 2^{#_{b} (N)} \leftrightarrow N - 1 < 2^{#_{b} (N)})}})))$
128	121 127	mpbid	$⊢ (((2^{#_{b(N)-1+1\inℤ\landN \in ℤ\land2^{#_{b} (N) - 1} + 1 \leq N\landN < 2^{#_{b} (N)}\landN \in ℤ_{\geq 2}\toN - 1 < 2^{#_{b} (N)}}})))$
129	68 70	syl	$⊢ N \in ℤ_{\geq 2} \to #_{b(N)-1+1=#_{b} (N)}$
130	129	oveq2d	$⊢ N \in ℤ_{\geq 2} \to 2^{#_{b(N)-1+1=2^{#_{b} (N)}}}$
131	130	adantl	$⊢ (((2^{#_{b(N)-1+1\inℤ\landN \in ℤ\land2^{#_{b} (N) - 1} + 1 \leq N\landN < 2^{#_{b} (N)}\landN \in ℤ_{\geq 2}\to2^{#_{b} (N) - 1 + 1} = 2^{#_{b} (N)}}})))$
132	128 131	breqtrrd	$⊢ (((2^{#_{b(N)-1+1\inℤ\landN \in ℤ\land2^{#_{b} (N) - 1} + 1 \leq N\landN < 2^{#_{b} (N)}\landN \in ℤ_{\geq 2}\toN - 1 < 2^{#_{b} (N) - 1 + 1}}})))$
133	104 112 132	3jca	$⊢ (((2^{#_{b(N)-1+1\inℤ\landN \in ℤ\land2^{#_{b} (N) - 1} + 1 \leq N\landN < 2^{#_{b} (N)}\landN \in ℤ_{\geq 2}\to(N - 1 \in ℤ_{\geq 2^{#_{b} (N) - 1}} \land 2^{#_{b} (N) - 1 + 1} \in ℤ \land N - 1 < 2^{#_{b} (N) - 1 + 1})}})))$
134	133	ex	$⊢ ((2^{#_{b(N)-1+1\inℤ\landN \in ℤ\land2^{#_{b} (N) - 1} + 1 \leq N\landN < 2^{#_{b} (N)}\to(N \in ℤ_{\geq 2} \to (N - 1 \in ℤ_{\geq 2^{#_{b} (N) - 1}} \land 2^{#_{b} (N) - 1 + 1} \in ℤ \land N - 1 < 2^{#_{b} (N) - 1 + 1}))}}))$
135	134	3adant2	$⊢ ((2^{#_{b(N)-1+1\inℤ\landN \in ℤ\land2^{#_{b} (N) - 1} + 1 \leq N\land2^{#_{b} (N)} \in ℤ\landN < 2^{#_{b} (N)}\to(N \in ℤ_{\geq 2} \to (N - 1 \in ℤ_{\geq 2^{#_{b} (N) - 1}} \land 2^{#_{b} (N) - 1 + 1} \in ℤ \land N - 1 < 2^{#_{b} (N) - 1 + 1}))}}))$
136	82 135	sylbi	$⊢ N \in (2^{#_{b(N)-1+1..^2^{#_{b} (N)}\to(N \in ℤ_{\geq 2} \to (N - 1 \in ℤ_{\geq 2^{#_{b} (N) - 1}} \land 2^{#_{b} (N) - 1 + 1} \in ℤ \land N - 1 < 2^{#_{b} (N) - 1 + 1}))}})$
137	136	imp	$⊢ (N \in (2^{#_{b(N)-1+1..^2^{#_{b} (N)}\landN \in ℤ_{\geq 2}\to(N - 1 \in ℤ_{\geq 2^{#_{b} (N) - 1}} \land 2^{#_{b} (N) - 1 + 1} \in ℤ \land N - 1 < 2^{#_{b} (N) - 1 + 1})}}))$
138		elfzo2	$⊢ N - 1 \in (2^{#_{b(N)-1..^2^{#_{b} (N) - 1 + 1}\leftrightarrow(N - 1 \in ℤ_{\geq 2^{#_{b} (N) - 1}} \land 2^{#_{b} (N) - 1 + 1} \in ℤ \land N - 1 < 2^{#_{b} (N) - 1 + 1})}})$
139	137 138	sylibr	$⊢ (N \in (2^{#_{b(N)-1+1..^2^{#_{b} (N)}\landN \in ℤ_{\geq 2}\toN - 1 \in (2^{#_{b} (N) - 1} ..^2^{#_{b} (N) - 1 + 1})}}))$
140	139	adantr	$⊢ ((N \in (2^{#_{b(N)-1+1..^2^{#_{b} (N)}\landN \in ℤ_{\geq 2}\land\frac{N + 1}{2} \in ℕ\toN - 1 \in (2^{#_{b} (N) - 1} ..^2^{#_{b} (N) - 1 + 1})}})))$
141		fllog2	$⊢ (#_{b(N)-1\inℕ_{0}\landN - 1 \in (2^{#_{b} (N) - 1} ..^2^{#_{b} (N) - 1 + 1})\to⌊\log_{2} (N - 1)⌋ = #_{b} (N) - 1})$
142	78 140 141	syl2anc	$⊢ ((N \in (2^{#_{b(N)-1+1..^2^{#_{b} (N)}\landN \in ℤ_{\geq 2}\land\frac{N + 1}{2} \in ℕ\to⌊\log_{2} (N - 1)⌋ = #_{b} (N) - 1}})))$
143	76 142	eqtr4d	$⊢ ((N \in (2^{#_{b(N)-1+1..^2^{#_{b} (N)}\landN \in ℤ_{\geq 2}\land\frac{N + 1}{2} \in ℕ\to⌊\log_{2} N⌋ = ⌊\log_{2} (N - 1)⌋}})))$
144	143	exp31	$⊢ N \in (2^{#_{b(N)-1+1..^2^{#_{b} (N)}\to(N \in ℤ_{\geq 2} \to (\frac{N + 1}{2} \in ℕ \to ⌊\log_{2} N⌋ = ⌊\log_{2} (N - 1)⌋))}})$
145	60 144	jaoi	$⊢ (N = 2^{#_{b(N)-1\lorN \in (2^{#_{b} (N) - 1} + 1 ..^2^{#_{b} (N)})\to(N \in ℤ_{\geq 2} \to (\frac{N + 1}{2} \in ℕ \to ⌊\log_{2} N⌋ = ⌊\log_{2} (N - 1)⌋))}})$
146	3 145	mpcom	$⊢ N \in ℤ_{\geq 2} \to (\frac{N + 1}{2} \in ℕ \to ⌊\log_{2} N⌋ = ⌊\log_{2} (N - 1)⌋)$
147	146	imp	$⊢ (N \in ℤ_{\geq 2} \land \frac{N + 1}{2} \in ℕ) \to ⌊\log_{2} N⌋ = ⌊\log_{2} (N - 1)⌋$

Metamath Proof Explorer

Theorem nnolog2flm1

Proof