blen1b

Description: The binary length of a nonnegative integer is 1 if the integer is 0 or 1. (Contributed by AV, 30-May-2020)

		Ref	Expression
	Assertion	blen1b	$⊢ N \in ℕ_{0} \to (#_{b(N)=1\leftrightarrow(N = 0 \lor N = 1)})$

Proof

Step	Hyp	Ref	Expression
1		elnn0	$⊢ N \in ℕ_{0} \leftrightarrow (N \in ℕ \lor N = 0)$
2		blennn	$⊢ N \in ℕ \to #_{b(N)=⌊\log_{2} N⌋ + 1}$
3	2	eqeq1d	$⊢ N \in ℕ \to (#_{b(N)=1\leftrightarrow⌊\log_{2} N⌋ + 1 = 1})$
4		2rp	$⊢ 2 \in ℝ^{+}$
5	4	a1i	$⊢ N \in ℕ \to 2 \in ℝ^{+}$
6		nnrp	$⊢ N \in ℕ \to N \in ℝ^{+}$
7		1ne2	$⊢ 1 \neq 2$
8	7	necomi	$⊢ 2 \neq 1$
9	8	a1i	$⊢ N \in ℕ \to 2 \neq 1$
10		relogbcl	$⊢ (2 \in ℝ^{+} \land N \in ℝ^{+} \land 2 \neq 1) \to \log_{2} N \in ℝ$
11	5 6 9 10	syl3anc	$⊢ N \in ℕ \to \log_{2} N \in ℝ$
12	11	flcld	$⊢ N \in ℕ \to ⌊\log_{2} N⌋ \in ℤ$
13	12	zcnd	$⊢ N \in ℕ \to ⌊\log_{2} N⌋ \in ℂ$
14		1cnd	$⊢ N \in ℕ \to 1 \in ℂ$
15	13 14 14	addlsub	$⊢ N \in ℕ \to (⌊\log_{2} N⌋ + 1 = 1 \leftrightarrow ⌊\log_{2} N⌋ = 1 - 1)$
16		1m1e0	$⊢ 1 - 1 = 0$
17	16	a1i	$⊢ N \in ℕ \to 1 - 1 = 0$
18	17	eqeq2d	$⊢ N \in ℕ \to (⌊\log_{2} N⌋ = 1 - 1 \leftrightarrow ⌊\log_{2} N⌋ = 0)$
19		0z	$⊢ 0 \in ℤ$
20		flbi	$⊢ (\log_{2} N \in ℝ \land 0 \in ℤ) \to (⌊\log_{2} N⌋ = 0 \leftrightarrow (0 \leq \log_{2} N \land \log_{2} N < 0 + 1))$
21	11 19 20	sylancl	$⊢ N \in ℕ \to (⌊\log_{2} N⌋ = 0 \leftrightarrow (0 \leq \log_{2} N \land \log_{2} N < 0 + 1))$
22	15 18 21	3bitrd	$⊢ N \in ℕ \to (⌊\log_{2} N⌋ + 1 = 1 \leftrightarrow (0 \leq \log_{2} N \land \log_{2} N < 0 + 1))$
23		0p1e1	$⊢ 0 + 1 = 1$
24	23	breq2i	$⊢ \log_{2} N < 0 + 1 \leftrightarrow \log_{2} N < 1$
25	24	anbi2i	$⊢ (0 \leq \log_{2} N \land \log_{2} N < 0 + 1) \leftrightarrow (0 \leq \log_{2} N \land \log_{2} N < 1)$
26		nnlog2ge0lt1	$⊢ N \in ℕ \to (N = 1 \leftrightarrow (0 \leq \log_{2} N \land \log_{2} N < 1))$
27	26	biimpar	$⊢ (N \in ℕ \land (0 \leq \log_{2} N \land \log_{2} N < 1)) \to N = 1$
28	27	olcd	$⊢ (N \in ℕ \land (0 \leq \log_{2} N \land \log_{2} N < 1)) \to (N = 0 \lor N = 1)$
29	28	ex	$⊢ N \in ℕ \to ((0 \leq \log_{2} N \land \log_{2} N < 1) \to (N = 0 \lor N = 1))$
30	25 29	syl5bi	$⊢ N \in ℕ \to ((0 \leq \log_{2} N \land \log_{2} N < 0 + 1) \to (N = 0 \lor N = 1))$
31	22 30	sylbid	$⊢ N \in ℕ \to (⌊\log_{2} N⌋ + 1 = 1 \to (N = 0 \lor N = 1))$
32	3 31	sylbid	$⊢ N \in ℕ \to (#_{b(N)=1\to(N = 0 \lor N = 1)})$
33		orc	$⊢ N = 0 \to (N = 0 \lor N = 1)$
34	33	a1d	$⊢ N = 0 \to (#_{b(N)=1\to(N = 0 \lor N = 1)})$
35	32 34	jaoi	$⊢ (N \in ℕ \lor N = 0) \to (#_{b(N)=1\to(N = 0 \lor N = 1)})$
36	1 35	sylbi	$⊢ N \in ℕ_{0} \to (#_{b(N)=1\to(N = 0 \lor N = 1)})$
37		fveq2	$⊢ N = 0 \to #_{b(N)=#_{b} (0)}$
38		blen0	$⊢ #_{b(0)=1}$
39	37 38	eqtrdi	$⊢ N = 0 \to #_{b(N)=1}$
40		fveq2	$⊢ N = 1 \to #_{b(N)=#_{b} (1)}$
41		blen1	$⊢ #_{b(1)=1}$
42	40 41	eqtrdi	$⊢ N = 1 \to #_{b(N)=1}$
43	39 42	jaoi	$⊢ (N = 0 \lor N = 1) \to #_{b(N)=1}$
44	36 43	impbid1	$⊢ N \in ℕ_{0} \to (#_{b(N)=1\leftrightarrow(N = 0 \lor N = 1)})$

Metamath Proof Explorer

Theorem blen1b

Proof