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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nnpw2p | |
|
2 | 2nn | |
|
3 | nnexpcl | |
|
4 | 2 3 | mpan | |
5 | elfzonn0 | |
|
6 | nnnn0addcl | |
|
7 | 4 5 6 | syl2an | |
8 | eleq1 | |
|
9 | 7 8 | syl5ibrcom | |
10 | 9 | rexlimivv | |
11 | 1 10 | impbii | |