blennn0e2

Description: The binary length of an even positive integer is the binary length of the half of the integer, increased by 1. (Contributed by AV, 29-May-2020)

		Ref	Expression
	Assertion	blennn0e2	$⊢ (N \in ℕ \land \frac{N}{2} \in ℕ_{0}) \to #_{b(N)=#_{b} (\frac{N}{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		nnrp	$⊢ N \in ℕ \to N \in ℝ^{+}$
7	6	adantr	$⊢ (N \in ℕ \land \frac{N}{2} \in ℕ_{0}) \to N \in ℝ^{+}$
8		relogbdivb	$⊢ (2 \in (ℝ^{+} ∖ \{1\}) \land N \in ℝ^{+}) \to \log_{2} (\frac{N}{2}) = \log_{2} N - 1$
9	5 7 8	sylancr	$⊢ (N \in ℕ \land \frac{N}{2} \in ℕ_{0}) \to \log_{2} (\frac{N}{2}) = \log_{2} N - 1$
10	9	fveq2d	$⊢ (N \in ℕ \land \frac{N}{2} \in ℕ_{0}) \to ⌊\log_{2} (\frac{N}{2})⌋ = ⌊\log_{2} N - 1⌋$
11	10	oveq1d	$⊢ (N \in ℕ \land \frac{N}{2} \in ℕ_{0}) \to ⌊\log_{2} (\frac{N}{2})⌋ + 1 = ⌊\log_{2} N - 1⌋ + 1$
12	1	a1i	$⊢ N \in ℕ \to 2 \in ℝ^{+}$
13	3	a1i	$⊢ N \in ℕ \to 2 \neq 1$
14		relogbcl	$⊢ (2 \in ℝ^{+} \land N \in ℝ^{+} \land 2 \neq 1) \to \log_{2} N \in ℝ$
15	12 6 13 14	syl3anc	$⊢ N \in ℕ \to \log_{2} N \in ℝ$
16		1zzd	$⊢ N \in ℕ \to 1 \in ℤ$
17	15 16	jca	$⊢ N \in ℕ \to (\log_{2} N \in ℝ \land 1 \in ℤ)$
18	17	adantr	$⊢ (N \in ℕ \land \frac{N}{2} \in ℕ_{0}) \to (\log_{2} N \in ℝ \land 1 \in ℤ)$
19		flsubz	$⊢ (\log_{2} N \in ℝ \land 1 \in ℤ) \to ⌊\log_{2} N - 1⌋ = ⌊\log_{2} N⌋ - 1$
20	18 19	syl	$⊢ (N \in ℕ \land \frac{N}{2} \in ℕ_{0}) \to ⌊\log_{2} N - 1⌋ = ⌊\log_{2} N⌋ - 1$
21	20	oveq1d	$⊢ (N \in ℕ \land \frac{N}{2} \in ℕ_{0}) \to ⌊\log_{2} N - 1⌋ + 1 = ⌊\log_{2} N⌋ - 1 + 1$
22	15	flcld	$⊢ N \in ℕ \to ⌊\log_{2} N⌋ \in ℤ$
23	22	zcnd	$⊢ N \in ℕ \to ⌊\log_{2} N⌋ \in ℂ$
24		npcan1	$⊢ ⌊\log_{2} N⌋ \in ℂ \to ⌊\log_{2} N⌋ - 1 + 1 = ⌊\log_{2} N⌋$
25	23 24	syl	$⊢ N \in ℕ \to ⌊\log_{2} N⌋ - 1 + 1 = ⌊\log_{2} N⌋$
26	25	adantr	$⊢ (N \in ℕ \land \frac{N}{2} \in ℕ_{0}) \to ⌊\log_{2} N⌋ - 1 + 1 = ⌊\log_{2} N⌋$
27	11 21 26	3eqtrd	$⊢ (N \in ℕ \land \frac{N}{2} \in ℕ_{0}) \to ⌊\log_{2} (\frac{N}{2})⌋ + 1 = ⌊\log_{2} N⌋$
28	27	oveq1d	$⊢ (N \in ℕ \land \frac{N}{2} \in ℕ_{0}) \to ⌊\log_{2} (\frac{N}{2})⌋ + 1 + 1 = ⌊\log_{2} N⌋ + 1$
29		nn0enne	$⊢ N \in ℕ \to (\frac{N}{2} \in ℕ_{0} \leftrightarrow \frac{N}{2} \in ℕ)$
30	29	biimpa	$⊢ (N \in ℕ \land \frac{N}{2} \in ℕ_{0}) \to \frac{N}{2} \in ℕ$
31		blennn	$⊢ \frac{N}{2} \in ℕ \to #_{b(\frac{N}{2})=⌊\log_{2} (\frac{N}{2})⌋ + 1}$
32	31	oveq1d	$⊢ \frac{N}{2} \in ℕ \to #_{b(\frac{N}{2})+1=⌊\log_{2} (\frac{N}{2})⌋ + 1 + 1}$
33	30 32	syl	$⊢ (N \in ℕ \land \frac{N}{2} \in ℕ_{0}) \to #_{b(\frac{N}{2})+1=⌊\log_{2} (\frac{N}{2})⌋ + 1 + 1}$
34		blennn	$⊢ N \in ℕ \to #_{b(N)=⌊\log_{2} N⌋ + 1}$
35	34	adantr	$⊢ (N \in ℕ \land \frac{N}{2} \in ℕ_{0}) \to #_{b(N)=⌊\log_{2} N⌋ + 1}$
36	28 33 35	3eqtr4rd	$⊢ (N \in ℕ \land \frac{N}{2} \in ℕ_{0}) \to #_{b(N)=#_{b} (\frac{N}{2}) + 1}$

Metamath Proof Explorer

Theorem blennn0e2

Proof