blennngt2o2

Description: The binary length of an odd integer greater than 1 is the binary length of the half of the integer decreased by 1, increased by 1. (Contributed by AV, 3-Jun-2020)

		Ref	Expression
	Assertion	blennngt2o2	$⊢ (N \in ℤ_{\geq 2} \land \frac{N + 1}{2} \in ℕ_{0}) \to #_{b(N)=#_{b} (\frac{N - 1}{2}) + 1}$

Proof

Step	Hyp	Ref	Expression
1		2rp	$⊢ 2 \in ℝ^{+}$
2		1ne2	$⊢ 1 \neq 2$
3	2	necomi	$⊢ 2 \neq 1$
4		eldifsn	$⊢ 2 \in (ℝ^{+} ∖ \{1\}) \leftrightarrow (2 \in ℝ^{+} \land 2 \neq 1)$
5	1 3 4	mpbir2an	$⊢ 2 \in (ℝ^{+} ∖ \{1\})$
6		uz2m1nn	$⊢ N \in ℤ_{\geq 2} \to N - 1 \in ℕ$
7	6	nnrpd	$⊢ N \in ℤ_{\geq 2} \to N - 1 \in ℝ^{+}$
8	7	adantr	$⊢ (N \in ℤ_{\geq 2} \land \frac{N + 1}{2} \in ℕ_{0}) \to N - 1 \in ℝ^{+}$
9		relogbdivb	$⊢ (2 \in (ℝ^{+} ∖ \{1\}) \land N - 1 \in ℝ^{+}) \to \log_{2} (\frac{N - 1}{2}) = \log_{2} (N - 1) - 1$
10	5 8 9	sylancr	$⊢ (N \in ℤ_{\geq 2} \land \frac{N + 1}{2} \in ℕ_{0}) \to \log_{2} (\frac{N - 1}{2}) = \log_{2} (N - 1) - 1$
11	10	fveq2d	$⊢ (N \in ℤ_{\geq 2} \land \frac{N + 1}{2} \in ℕ_{0}) \to ⌊\log_{2} (\frac{N - 1}{2})⌋ = ⌊\log_{2} (N - 1) - 1⌋$
12	11	oveq1d	$⊢ (N \in ℤ_{\geq 2} \land \frac{N + 1}{2} \in ℕ_{0}) \to ⌊\log_{2} (\frac{N - 1}{2})⌋ + 1 = ⌊\log_{2} (N - 1) - 1⌋ + 1$
13	1	a1i	$⊢ N \in ℤ_{\geq 2} \to 2 \in ℝ^{+}$
14	3	a1i	$⊢ N \in ℤ_{\geq 2} \to 2 \neq 1$
15		relogbcl	$⊢ (2 \in ℝ^{+} \land N - 1 \in ℝ^{+} \land 2 \neq 1) \to \log_{2} (N - 1) \in ℝ$
16	13 7 14 15	syl3anc	$⊢ N \in ℤ_{\geq 2} \to \log_{2} (N - 1) \in ℝ$
17		1z	$⊢ 1 \in ℤ$
18	16 17	jctir	$⊢ N \in ℤ_{\geq 2} \to (\log_{2} (N - 1) \in ℝ \land 1 \in ℤ)$
19	18	adantr	$⊢ (N \in ℤ_{\geq 2} \land \frac{N + 1}{2} \in ℕ_{0}) \to (\log_{2} (N - 1) \in ℝ \land 1 \in ℤ)$
20		flsubz	$⊢ (\log_{2} (N - 1) \in ℝ \land 1 \in ℤ) \to ⌊\log_{2} (N - 1) - 1⌋ = ⌊\log_{2} (N - 1)⌋ - 1$
21	19 20	syl	$⊢ (N \in ℤ_{\geq 2} \land \frac{N + 1}{2} \in ℕ_{0}) \to ⌊\log_{2} (N - 1) - 1⌋ = ⌊\log_{2} (N - 1)⌋ - 1$
22	21	oveq1d	$⊢ (N \in ℤ_{\geq 2} \land \frac{N + 1}{2} \in ℕ_{0}) \to ⌊\log_{2} (N - 1) - 1⌋ + 1 = ⌊\log_{2} (N - 1)⌋ - 1 + 1$
23	16	flcld	$⊢ N \in ℤ_{\geq 2} \to ⌊\log_{2} (N - 1)⌋ \in ℤ$
24	23	zcnd	$⊢ N \in ℤ_{\geq 2} \to ⌊\log_{2} (N - 1)⌋ \in ℂ$
25		npcan1	$⊢ ⌊\log_{2} (N - 1)⌋ \in ℂ \to ⌊\log_{2} (N - 1)⌋ - 1 + 1 = ⌊\log_{2} (N - 1)⌋$
26	24 25	syl	$⊢ N \in ℤ_{\geq 2} \to ⌊\log_{2} (N - 1)⌋ - 1 + 1 = ⌊\log_{2} (N - 1)⌋$
27	26	adantr	$⊢ (N \in ℤ_{\geq 2} \land \frac{N + 1}{2} \in ℕ_{0}) \to ⌊\log_{2} (N - 1)⌋ - 1 + 1 = ⌊\log_{2} (N - 1)⌋$
28		eluz2nn	$⊢ N \in ℤ_{\geq 2} \to N \in ℕ$
29	28	peano2nnd	$⊢ N \in ℤ_{\geq 2} \to N + 1 \in ℕ$
30	29	nnred	$⊢ N \in ℤ_{\geq 2} \to N + 1 \in ℝ$
31		2re	$⊢ 2 \in ℝ$
32	31	a1i	$⊢ N \in ℤ_{\geq 2} \to 2 \in ℝ$
33		eluzge2nn0	$⊢ N \in ℤ_{\geq 2} \to N \in ℕ_{0}$
34		nn0p1gt0	$⊢ N \in ℕ_{0} \to 0 < N + 1$
35	33 34	syl	$⊢ N \in ℤ_{\geq 2} \to 0 < N + 1$
36		2pos	$⊢ 0 < 2$
37	36	a1i	$⊢ N \in ℤ_{\geq 2} \to 0 < 2$
38	30 32 35 37	divgt0d	$⊢ N \in ℤ_{\geq 2} \to 0 < \frac{N + 1}{2}$
39		nn0z	$⊢ \frac{N + 1}{2} \in ℕ_{0} \to \frac{N + 1}{2} \in ℤ$
40	38 39	anim12ci	$⊢ (N \in ℤ_{\geq 2} \land \frac{N + 1}{2} \in ℕ_{0}) \to (\frac{N + 1}{2} \in ℤ \land 0 < \frac{N + 1}{2})$
41		elnnz	$⊢ \frac{N + 1}{2} \in ℕ \leftrightarrow (\frac{N + 1}{2} \in ℤ \land 0 < \frac{N + 1}{2})$
42	40 41	sylibr	$⊢ (N \in ℤ_{\geq 2} \land \frac{N + 1}{2} \in ℕ_{0}) \to \frac{N + 1}{2} \in ℕ$
43		nnolog2flm1	$⊢ (N \in ℤ_{\geq 2} \land \frac{N + 1}{2} \in ℕ) \to ⌊\log_{2} N⌋ = ⌊\log_{2} (N - 1)⌋$
44	42 43	syldan	$⊢ (N \in ℤ_{\geq 2} \land \frac{N + 1}{2} \in ℕ_{0}) \to ⌊\log_{2} N⌋ = ⌊\log_{2} (N - 1)⌋$
45	27 44	eqtr4d	$⊢ (N \in ℤ_{\geq 2} \land \frac{N + 1}{2} \in ℕ_{0}) \to ⌊\log_{2} (N - 1)⌋ - 1 + 1 = ⌊\log_{2} N⌋$
46	12 22 45	3eqtrd	$⊢ (N \in ℤ_{\geq 2} \land \frac{N + 1}{2} \in ℕ_{0}) \to ⌊\log_{2} (\frac{N - 1}{2})⌋ + 1 = ⌊\log_{2} N⌋$
47	46	oveq1d	$⊢ (N \in ℤ_{\geq 2} \land \frac{N + 1}{2} \in ℕ_{0}) \to ⌊\log_{2} (\frac{N - 1}{2})⌋ + 1 + 1 = ⌊\log_{2} N⌋ + 1$
48		nno	$⊢ (N \in ℤ_{\geq 2} \land \frac{N + 1}{2} \in ℕ_{0}) \to \frac{N - 1}{2} \in ℕ$
49		blennn	$⊢ \frac{N - 1}{2} \in ℕ \to #_{b(\frac{N - 1}{2})=⌊\log_{2} (\frac{N - 1}{2})⌋ + 1}$
50	49	oveq1d	$⊢ \frac{N - 1}{2} \in ℕ \to #_{b(\frac{N - 1}{2})+1=⌊\log_{2} (\frac{N - 1}{2})⌋ + 1 + 1}$
51	48 50	syl	$⊢ (N \in ℤ_{\geq 2} \land \frac{N + 1}{2} \in ℕ_{0}) \to #_{b(\frac{N - 1}{2})+1=⌊\log_{2} (\frac{N - 1}{2})⌋ + 1 + 1}$
52		blennn	$⊢ N \in ℕ \to #_{b(N)=⌊\log_{2} N⌋ + 1}$
53	28 52	syl	$⊢ N \in ℤ_{\geq 2} \to #_{b(N)=⌊\log_{2} N⌋ + 1}$
54	53	adantr	$⊢ (N \in ℤ_{\geq 2} \land \frac{N + 1}{2} \in ℕ_{0}) \to #_{b(N)=⌊\log_{2} N⌋ + 1}$
55	47 51 54	3eqtr4rd	$⊢ (N \in ℤ_{\geq 2} \land \frac{N + 1}{2} \in ℕ_{0}) \to #_{b(N)=#_{b} (\frac{N - 1}{2}) + 1}$

Metamath Proof Explorer

Theorem blennngt2o2

Proof