blengt1fldiv2p1

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

		Ref	Expression
	Assertion	blengt1fldiv2p1	$⊢ N \in ℤ_{\geq 2} \to #_{b(N)=#_{b} (⌊\frac{N}{2}⌋) + 1}$

Proof

Step	Hyp	Ref	Expression
1		eluz2nn	$⊢ N \in ℤ_{\geq 2} \to N \in ℕ$
2		nneop	$⊢ N \in ℕ \to (\frac{N}{2} \in ℕ \lor \frac{N + 1}{2} \in ℕ)$
3	1 2	syl	$⊢ N \in ℤ_{\geq 2} \to (\frac{N}{2} \in ℕ \lor \frac{N + 1}{2} \in ℕ)$
4		nnnn0	$⊢ \frac{N}{2} \in ℕ \to \frac{N}{2} \in ℕ_{0}$
5		blennn0em1	$⊢ (N \in ℕ \land \frac{N}{2} \in ℕ_{0}) \to #_{b(\frac{N}{2})=#_{b} (N) - 1}$
6	4 5	sylan2	$⊢ (N \in ℕ \land \frac{N}{2} \in ℕ) \to #_{b(\frac{N}{2})=#_{b} (N) - 1}$
7	6	ancoms	$⊢ (\frac{N}{2} \in ℕ \land N \in ℕ) \to #_{b(\frac{N}{2})=#_{b} (N) - 1}$
8	7	oveq1d	$⊢ (\frac{N}{2} \in ℕ \land N \in ℕ) \to #_{b(\frac{N}{2})+1=#_{b} (N) - 1 + 1}$
9		nnz	$⊢ \frac{N}{2} \in ℕ \to \frac{N}{2} \in ℤ$
10		flid	$⊢ \frac{N}{2} \in ℤ \to ⌊\frac{N}{2}⌋ = \frac{N}{2}$
11	9 10	syl	$⊢ \frac{N}{2} \in ℕ \to ⌊\frac{N}{2}⌋ = \frac{N}{2}$
12	11	eqcomd	$⊢ \frac{N}{2} \in ℕ \to \frac{N}{2} = ⌊\frac{N}{2}⌋$
13	12	fveq2d	$⊢ \frac{N}{2} \in ℕ \to #_{b(\frac{N}{2})=#_{b} (⌊\frac{N}{2}⌋)}$
14	13	oveq1d	$⊢ \frac{N}{2} \in ℕ \to #_{b(\frac{N}{2})+1=#_{b} (⌊\frac{N}{2}⌋) + 1}$
15	14	adantr	$⊢ (\frac{N}{2} \in ℕ \land N \in ℕ) \to #_{b(\frac{N}{2})+1=#_{b} (⌊\frac{N}{2}⌋) + 1}$
16		blennnelnn	$⊢ N \in ℕ \to #_{b(N)\inℕ}$
17	16	nncnd	$⊢ N \in ℕ \to #_{b(N)\inℂ}$
18		npcan1	$⊢ #_{b(N)\inℂ\to#_{b} (N) - 1 + 1 = #_{b} (N)}$
19	17 18	syl	$⊢ N \in ℕ \to #_{b(N)-1+1=#_{b} (N)}$
20	19	adantl	$⊢ (\frac{N}{2} \in ℕ \land N \in ℕ) \to #_{b(N)-1+1=#_{b} (N)}$
21	8 15 20	3eqtr3rd	$⊢ (\frac{N}{2} \in ℕ \land N \in ℕ) \to #_{b(N)=#_{b} (⌊\frac{N}{2}⌋) + 1}$
22	21	expcom	$⊢ N \in ℕ \to (\frac{N}{2} \in ℕ \to #_{b(N)=#_{b} (⌊\frac{N}{2}⌋) + 1})$
23	22 1	syl11	$⊢ \frac{N}{2} \in ℕ \to (N \in ℤ_{\geq 2} \to #_{b(N)=#_{b} (⌊\frac{N}{2}⌋) + 1})$
24		nnnn0	$⊢ \frac{N + 1}{2} \in ℕ \to \frac{N + 1}{2} \in ℕ_{0}$
25		blennngt2o2	$⊢ (N \in ℤ_{\geq 2} \land \frac{N + 1}{2} \in ℕ_{0}) \to #_{b(N)=#_{b} (\frac{N - 1}{2}) + 1}$
26	24 25	sylan2	$⊢ (N \in ℤ_{\geq 2} \land \frac{N + 1}{2} \in ℕ) \to #_{b(N)=#_{b} (\frac{N - 1}{2}) + 1}$
27	26	ancoms	$⊢ (\frac{N + 1}{2} \in ℕ \land N \in ℤ_{\geq 2}) \to #_{b(N)=#_{b} (\frac{N - 1}{2}) + 1}$
28		eluzge2nn0	$⊢ N \in ℤ_{\geq 2} \to N \in ℕ_{0}$
29		nn0ofldiv2	$⊢ (N \in ℕ_{0} \land \frac{N + 1}{2} \in ℕ_{0}) \to ⌊\frac{N}{2}⌋ = \frac{N - 1}{2}$
30	28 24 29	syl2anr	$⊢ (\frac{N + 1}{2} \in ℕ \land N \in ℤ_{\geq 2}) \to ⌊\frac{N}{2}⌋ = \frac{N - 1}{2}$
31	30	eqcomd	$⊢ (\frac{N + 1}{2} \in ℕ \land N \in ℤ_{\geq 2}) \to \frac{N - 1}{2} = ⌊\frac{N}{2}⌋$
32	31	fveq2d	$⊢ (\frac{N + 1}{2} \in ℕ \land N \in ℤ_{\geq 2}) \to #_{b(\frac{N - 1}{2})=#_{b} (⌊\frac{N}{2}⌋)}$
33	32	oveq1d	$⊢ (\frac{N + 1}{2} \in ℕ \land N \in ℤ_{\geq 2}) \to #_{b(\frac{N - 1}{2})+1=#_{b} (⌊\frac{N}{2}⌋) + 1}$
34	27 33	eqtrd	$⊢ (\frac{N + 1}{2} \in ℕ \land N \in ℤ_{\geq 2}) \to #_{b(N)=#_{b} (⌊\frac{N}{2}⌋) + 1}$
35	34	ex	$⊢ \frac{N + 1}{2} \in ℕ \to (N \in ℤ_{\geq 2} \to #_{b(N)=#_{b} (⌊\frac{N}{2}⌋) + 1})$
36	23 35	jaoi	$⊢ (\frac{N}{2} \in ℕ \lor \frac{N + 1}{2} \in ℕ) \to (N \in ℤ_{\geq 2} \to #_{b(N)=#_{b} (⌊\frac{N}{2}⌋) + 1})$
37	3 36	mpcom	$⊢ N \in ℤ_{\geq 2} \to #_{b(N)=#_{b} (⌊\frac{N}{2}⌋) + 1}$

Metamath Proof Explorer

Theorem blengt1fldiv2p1

Proof