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 e. NN <-> E. i e. NN0 E. r e. ( 0 ..^ ( 2 ^ i ) ) N = ( ( 2 ^ i ) + r ) )

Proof

Step	Hyp	Ref	Expression
1		nnpw2p	|- ( N e. NN -> E. i e. NN0 E. r e. ( 0 ..^ ( 2 ^ i ) ) N = ( ( 2 ^ i ) + r ) )
2		2nn	|- 2 e. NN
3		nnexpcl	|- ( ( 2 e. NN /\ i e. NN0 ) -> ( 2 ^ i ) e. NN )
4	2 3	mpan	|- ( i e. NN0 -> ( 2 ^ i ) e. NN )
5		elfzonn0	|- ( r e. ( 0 ..^ ( 2 ^ i ) ) -> r e. NN0 )
6		nnnn0addcl	|- ( ( ( 2 ^ i ) e. NN /\ r e. NN0 ) -> ( ( 2 ^ i ) + r ) e. NN )
7	4 5 6	syl2an	|- ( ( i e. NN0 /\ r e. ( 0 ..^ ( 2 ^ i ) ) ) -> ( ( 2 ^ i ) + r ) e. NN )
8		eleq1	|- ( N = ( ( 2 ^ i ) + r ) -> ( N e. NN <-> ( ( 2 ^ i ) + r ) e. NN ) )
9	7 8	syl5ibrcom	|- ( ( i e. NN0 /\ r e. ( 0 ..^ ( 2 ^ i ) ) ) -> ( N = ( ( 2 ^ i ) + r ) -> N e. NN ) )
10	9	rexlimivv	|- ( E. i e. NN0 E. r e. ( 0 ..^ ( 2 ^ i ) ) N = ( ( 2 ^ i ) + r ) -> N e. NN )
11	1 10	impbii	|- ( N e. NN <-> E. i e. NN0 E. r e. ( 0 ..^ ( 2 ^ i ) ) N = ( ( 2 ^ i ) + r ) )