Theorem nnpw2pb

Description: A number is a positive integer iff it 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	nnpw2pb	$$⊢N\in \mathbb{N}\leftrightarrow \exists i\in {\mathbb{N}}_0\exists r\in \left(0..^2^i\right)N=2^i+r$$

Proof

Step	Hyp	Ref	Expression
1		nnpw2p	$$⊢N\in \mathbb{N}\to \exists i\in {\mathbb{N}}_0\exists r\in \left(0..^2^i\right)N=2^i+r$$
2		2nn	$$⊢2\in \mathbb{N}$$
3		nnexpcl	$$⊢\left(2\in \mathbb{N}\wedge i\in {\mathbb{N}}_0\right)\to 2^i\in \mathbb{N}$$
4	2 3	mpan	$$⊢i\in {\mathbb{N}}_0\to 2^i\in \mathbb{N}$$
5		elfzonn0	$$⊢r\in \left(0..^2^i\right)\to r\in {\mathbb{N}}_0$$
6		nnnn0addcl	$$⊢\left(2^i\in \mathbb{N}\wedge r\in {\mathbb{N}}_0\right)\to 2^i+r\in \mathbb{N}$$
7	4 5 6	syl2an	$$⊢\left(i\in {\mathbb{N}}_0\wedge r\in \left(0..^2^i\right)\right)\to 2^i+r\in \mathbb{N}$$
8		eleq1	$$⊢N=2^i+r\to \left(N\in \mathbb{N}\leftrightarrow 2^i+r\in \mathbb{N}\right)$$
9	7 8	syl5ibrcom	$$⊢\left(i\in {\mathbb{N}}_0\wedge r\in \left(0..^2^i\right)\right)\to \left(N=2^i+r\to N\in \mathbb{N}\right)$$
10	9	rexlimivv	$$⊢\exists i\in {\mathbb{N}}_0\exists r\in \left(0..^2^i\right)N=2^i+r\to N\in \mathbb{N}$$
11	1 10	impbii	$$⊢N\in \mathbb{N}\leftrightarrow \exists i\in {\mathbb{N}}_0\exists r\in \left(0..^2^i\right)N=2^i+r$$