Metamath Proof Explorer

Theorem nnpw2p

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

Proof

Step Hyp Ref Expression
1 blennnelnn 
 |-  ( N e. NN -> ( #b ` N ) e. NN )
2 nnm1nn0 
 |-  ( ( #b ` N ) e. NN -> ( ( #b ` N ) - 1 ) e. NN0 )
3 1 2 syl 
 |-  ( N e. NN -> ( ( #b ` N ) - 1 ) e. NN0 )
4 oveq2 
 |-  ( i = ( ( #b ` N ) - 1 ) -> ( 2 ^ i ) = ( 2 ^ ( ( #b ` N ) - 1 ) ) )
5 4 oveq2d 
 |-  ( i = ( ( #b ` N ) - 1 ) -> ( 0 ..^ ( 2 ^ i ) ) = ( 0 ..^ ( 2 ^ ( ( #b ` N ) - 1 ) ) ) )
6 4 oveq1d 
 |-  ( i = ( ( #b ` N ) - 1 ) -> ( ( 2 ^ i ) + r ) = ( ( 2 ^ ( ( #b ` N ) - 1 ) ) + r ) )
7 6 eqeq2d 
 |-  ( i = ( ( #b ` N ) - 1 ) -> ( N = ( ( 2 ^ i ) + r ) <-> N = ( ( 2 ^ ( ( #b ` N ) - 1 ) ) + r ) ) )
8 5 7 rexeqbidv 
 |-  ( i = ( ( #b ` N ) - 1 ) -> ( E. r e. ( 0 ..^ ( 2 ^ i ) ) N = ( ( 2 ^ i ) + r ) <-> E. r e. ( 0 ..^ ( 2 ^ ( ( #b ` N ) - 1 ) ) ) N = ( ( 2 ^ ( ( #b ` N ) - 1 ) ) + r ) ) )
9 8 adantl 
 |-  ( ( N e. NN /\ i = ( ( #b ` N ) - 1 ) ) -> ( E. r e. ( 0 ..^ ( 2 ^ i ) ) N = ( ( 2 ^ i ) + r ) <-> E. r e. ( 0 ..^ ( 2 ^ ( ( #b ` N ) - 1 ) ) ) N = ( ( 2 ^ ( ( #b ` N ) - 1 ) ) + r ) ) )
10 nnz 
 |-  ( N e. NN -> N e. ZZ )
11 2nn 
 |-  2 e. NN
12 11 a1i 
 |-  ( N e. NN -> 2 e. NN )
13 12 3 nnexpcld 
 |-  ( N e. NN -> ( 2 ^ ( ( #b ` N ) - 1 ) ) e. NN )
14 zmodfzo 
 |-  ( ( N e. ZZ /\ ( 2 ^ ( ( #b ` N ) - 1 ) ) e. NN ) -> ( N mod ( 2 ^ ( ( #b ` N ) - 1 ) ) ) e. ( 0 ..^ ( 2 ^ ( ( #b ` N ) - 1 ) ) ) )
15 10 13 14 syl2anc 
 |-  ( N e. NN -> ( N mod ( 2 ^ ( ( #b ` N ) - 1 ) ) ) e. ( 0 ..^ ( 2 ^ ( ( #b ` N ) - 1 ) ) ) )
16 oveq2 
 |-  ( r = ( N mod ( 2 ^ ( ( #b ` N ) - 1 ) ) ) -> ( ( 2 ^ ( ( #b ` N ) - 1 ) ) + r ) = ( ( 2 ^ ( ( #b ` N ) - 1 ) ) + ( N mod ( 2 ^ ( ( #b ` N ) - 1 ) ) ) ) )
17 16 eqeq2d 
 |-  ( r = ( N mod ( 2 ^ ( ( #b ` N ) - 1 ) ) ) -> ( N = ( ( 2 ^ ( ( #b ` N ) - 1 ) ) + r ) <-> N = ( ( 2 ^ ( ( #b ` N ) - 1 ) ) + ( N mod ( 2 ^ ( ( #b ` N ) - 1 ) ) ) ) ) )
18 17 adantl 
 |-  ( ( N e. NN /\ r = ( N mod ( 2 ^ ( ( #b ` N ) - 1 ) ) ) ) -> ( N = ( ( 2 ^ ( ( #b ` N ) - 1 ) ) + r ) <-> N = ( ( 2 ^ ( ( #b ` N ) - 1 ) ) + ( N mod ( 2 ^ ( ( #b ` N ) - 1 ) ) ) ) ) )
19 nnpw2pmod 
 |-  ( N e. NN -> N = ( ( 2 ^ ( ( #b ` N ) - 1 ) ) + ( N mod ( 2 ^ ( ( #b ` N ) - 1 ) ) ) ) )
20 15 18 19 rspcedvd 
 |-  ( N e. NN -> E. r e. ( 0 ..^ ( 2 ^ ( ( #b ` N ) - 1 ) ) ) N = ( ( 2 ^ ( ( #b ` N ) - 1 ) ) + r ) )
21 3 9 20 rspcedvd 
 |-  ( N e. NN -> E. i e. NN0 E. r e. ( 0 ..^ ( 2 ^ i ) ) N = ( ( 2 ^ i ) + r ) )