Metamath Proof Explorer


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 Ni0r0..^2iN=2i+r

Proof

Step Hyp Ref Expression
1 nnpw2p Ni0r0..^2iN=2i+r
2 2nn 2
3 nnexpcl 2i02i
4 2 3 mpan i02i
5 elfzonn0 r0..^2ir0
6 nnnn0addcl 2ir02i+r
7 4 5 6 syl2an i0r0..^2i2i+r
8 eleq1 N=2i+rN2i+r
9 7 8 syl5ibrcom i0r0..^2iN=2i+rN
10 9 rexlimivv i0r0..^2iN=2i+rN
11 1 10 impbii Ni0r0..^2iN=2i+r