nnpw2pmod

Description: Every positive integer can be represented as the sum of a power of 2 and a "remainder" smaller than the power. (Contributed by AV, 31-May-2020)

		Ref	Expression
	Assertion	nnpw2pmod	$⊢ N \in ℕ \to N = 2^{#_{b(N)-1+(N \mod 2^{#_{b} (N) - 1})}}$

Proof

Step	Hyp	Ref	Expression
1		nnre	$⊢ N \in ℕ \to N \in ℝ$
2		2nn	$⊢ 2 \in ℕ$
3	2	a1i	$⊢ N \in ℕ \to 2 \in ℕ$
4		blennnelnn	$⊢ N \in ℕ \to #_{b(N)\inℕ}$
5		nnm1nn0	$⊢ #_{b(N)\inℕ\to#_{b} (N) - 1 \in ℕ_{0}}$
6	4 5	syl	$⊢ N \in ℕ \to #_{b(N)-1\inℕ_{0}}$
7	3 6	nnexpcld	$⊢ N \in ℕ \to 2^{#_{b(N)-1\inℕ}}$
8	7	nnrpd	$⊢ N \in ℕ \to 2^{#_{b(N)-1\inℝ^{+}}}$
9		modeqmodmin	$⊢ (N \in ℝ \land 2^{#_{b(N)-1\inℝ^{+}\toN \mod 2^{#_{b} (N) - 1} = (N - 2^{#_{b} (N) - 1}) \mod 2^{#_{b} (N) - 1}}})$
10	1 8 9	syl2anc	$⊢ N \in ℕ \to N \mod 2^{#_{b(N)-1=(N - 2^{#_{b} (N) - 1}) \mod 2^{#_{b} (N) - 1}}}$
11	7	nnred	$⊢ N \in ℕ \to 2^{#_{b(N)-1\inℝ}}$
12	1 11	resubcld	$⊢ N \in ℕ \to N - 2^{#_{b(N)-1\inℝ}}$
13		nnpw2blen	$⊢ N \in ℕ \to (2^{#_{b(N)-1\leqN\landN < 2^{#_{b} (N)}}})$
14	1 11	subge0d	$⊢ N \in ℕ \to (0 \leq N - 2^{#_{b(N)-1\leftrightarrow2^{#_{b} (N) - 1} \leq N}})$
15	1 11 11	ltsubadd2d	$⊢ N \in ℕ \to (N - 2^{#_{b(N)-1<2^{#_{b} (N) - 1}\leftrightarrowN < 2^{#_{b} (N) - 1} + 2^{#_{b} (N) - 1}}})$
16		2cn	$⊢ 2 \in ℂ$
17		exp1	$⊢ 2 \in ℂ \to 2^{1} = 2$
18	17	eqcomd	$⊢ 2 \in ℂ \to 2 = 2^{1}$
19	16 18	mp1i	$⊢ N \in ℕ \to 2 = 2^{1}$
20	19	oveq1d	$⊢ N \in ℕ \to 2 2^{#_{b(N)-1=2^{1} 2^{#_{b} (N) - 1}}}$
21	7	nncnd	$⊢ N \in ℕ \to 2^{#_{b(N)-1\inℂ}}$
22	21	2timesd	$⊢ N \in ℕ \to 2 2^{#_{b(N)-1=2^{#_{b} (N) - 1} + 2^{#_{b} (N) - 1}}}$
23	16	a1i	$⊢ N \in ℕ \to 2 \in ℂ$
24		1nn0	$⊢ 1 \in ℕ_{0}$
25	24	a1i	$⊢ N \in ℕ \to 1 \in ℕ_{0}$
26	23 6 25	expaddd	$⊢ N \in ℕ \to 2^{1 + #_{b(N)-1=2^{1} 2^{#_{b} (N) - 1}}}$
27		1cnd	$⊢ N \in ℕ \to 1 \in ℂ$
28	4	nncnd	$⊢ N \in ℕ \to #_{b(N)\inℂ}$
29	27 28	pncan3d	$⊢ N \in ℕ \to 1 + #_{b(N)-1=#_{b} (N)}$
30	29	oveq2d	$⊢ N \in ℕ \to 2^{1 + #_{b(N)-1=2^{#_{b} (N)}}}$
31	26 30	eqtr3d	$⊢ N \in ℕ \to 2^{1} 2^{#_{b(N)-1=2^{#_{b} (N)}}}$
32	20 22 31	3eqtr3d	$⊢ N \in ℕ \to 2^{#_{b(N)-1+2^{#_{b} (N) - 1}=2^{#_{b} (N)}}}$
33	32	breq2d	$⊢ N \in ℕ \to (N < 2^{#_{b(N)-1+2^{#_{b} (N) - 1}\leftrightarrowN < 2^{#_{b} (N)}}})$
34	15 33	bitrd	$⊢ N \in ℕ \to (N - 2^{#_{b(N)-1<2^{#_{b} (N) - 1}\leftrightarrowN < 2^{#_{b} (N)}}})$
35	14 34	anbi12d	$⊢ N \in ℕ \to ((0 \leq N - 2^{#_{b(N)-1\landN - 2^{#_{b} (N) - 1} < 2^{#_{b} (N) - 1}\leftrightarrow(2^{#_{b} (N) - 1} \leq N \land N < 2^{#_{b} (N)})}}))$
36	13 35	mpbird	$⊢ N \in ℕ \to (0 \leq N - 2^{#_{b(N)-1\landN - 2^{#_{b} (N) - 1} < 2^{#_{b} (N) - 1}}})$
37		modid	$⊢ ((N - 2^{#_{b(N)-1\inℝ\land2^{#_{b} (N) - 1} \in ℝ^{+}\land(0 \leq N - 2^{#_{b} (N) - 1} \land N - 2^{#_{b} (N) - 1} < 2^{#_{b} (N) - 1})\to(N - 2^{#_{b} (N) - 1}) \mod 2^{#_{b} (N) - 1} = N - 2^{#_{b} (N) - 1}}}))$
38	12 8 36 37	syl21anc	$⊢ N \in ℕ \to (N - 2^{#_{b(N)-1\mod2^{#_{b} (N) - 1}=N - 2^{#_{b} (N) - 1}}})$
39	10 38	eqtr2d	$⊢ N \in ℕ \to N - 2^{#_{b(N)-1=N \mod 2^{#_{b} (N) - 1}}}$
40		nncn	$⊢ N \in ℕ \to N \in ℂ$
41		nnz	$⊢ N \in ℕ \to N \in ℤ$
42	41 7	zmodcld	$⊢ N \in ℕ \to N \mod 2^{#_{b(N)-1\inℕ_{0}}}$
43	42	nn0cnd	$⊢ N \in ℕ \to N \mod 2^{#_{b(N)-1\inℂ}}$
44	40 21 43	subaddd	$⊢ N \in ℕ \to (N - 2^{#_{b(N)-1=N \mod 2^{#_{b} (N) - 1}\leftrightarrow2^{#_{b} (N) - 1} + (N \mod 2^{#_{b} (N) - 1}) = N}})$
45	39 44	mpbid	$⊢ N \in ℕ \to 2^{#_{b(N)-1+(N \mod 2^{#_{b} (N) - 1})=N}}$
46	45	eqcomd	$⊢ N \in ℕ \to N = 2^{#_{b(N)-1+(N \mod 2^{#_{b} (N) - 1})}}$

Metamath Proof Explorer

Theorem nnpw2pmod

Proof