Metamath Proof Explorer

Theorem nnpw2pmod

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 nnpw2pmod 
|- ( N e. NN -> N = ( ( 2 ^ ( ( #b ` N ) - 1 ) ) + ( N mod ( 2 ^ ( ( #b ` N ) - 1 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 nnre 
 |-  ( N e. NN -> N e. RR )
2 2nn 
 |-  2 e. NN
3 2 a1i 
 |-  ( N e. NN -> 2 e. NN )
4 blennnelnn 
 |-  ( N e. NN -> ( #b ` N ) e. NN )
5 nnm1nn0 
 |-  ( ( #b ` N ) e. NN -> ( ( #b ` N ) - 1 ) e. NN0 )
6 4 5 syl 
 |-  ( N e. NN -> ( ( #b ` N ) - 1 ) e. NN0 )
7 3 6 nnexpcld 
 |-  ( N e. NN -> ( 2 ^ ( ( #b ` N ) - 1 ) ) e. NN )
8 7 nnrpd 
 |-  ( N e. NN -> ( 2 ^ ( ( #b ` N ) - 1 ) ) e. RR+ )
9 modeqmodmin 
 |-  ( ( N e. RR /\ ( 2 ^ ( ( #b ` N ) - 1 ) ) e. RR+ ) -> ( N mod ( 2 ^ ( ( #b ` N ) - 1 ) ) ) = ( ( N - ( 2 ^ ( ( #b ` N ) - 1 ) ) ) mod ( 2 ^ ( ( #b ` N ) - 1 ) ) ) )
10 1 8 9 syl2anc 
 |-  ( N e. NN -> ( N mod ( 2 ^ ( ( #b ` N ) - 1 ) ) ) = ( ( N - ( 2 ^ ( ( #b ` N ) - 1 ) ) ) mod ( 2 ^ ( ( #b ` N ) - 1 ) ) ) )
11 7 nnred 
 |-  ( N e. NN -> ( 2 ^ ( ( #b ` N ) - 1 ) ) e. RR )
12 1 11 resubcld 
 |-  ( N e. NN -> ( N - ( 2 ^ ( ( #b ` N ) - 1 ) ) ) e. RR )
13 nnpw2blen 
 |-  ( N e. NN -> ( ( 2 ^ ( ( #b ` N ) - 1 ) ) <_ N /\ N < ( 2 ^ ( #b ` N ) ) ) )
14 1 11 subge0d 
 |-  ( N e. NN -> ( 0 <_ ( N - ( 2 ^ ( ( #b ` N ) - 1 ) ) ) <-> ( 2 ^ ( ( #b ` N ) - 1 ) ) <_ N ) )
15 1 11 11 ltsubadd2d 
 |-  ( N e. NN -> ( ( N - ( 2 ^ ( ( #b ` N ) - 1 ) ) ) < ( 2 ^ ( ( #b ` N ) - 1 ) ) <-> N < ( ( 2 ^ ( ( #b ` N ) - 1 ) ) + ( 2 ^ ( ( #b ` N ) - 1 ) ) ) ) )
16 2cn 
 |-  2 e. CC
17 exp1 
 |-  ( 2 e. CC -> ( 2 ^ 1 ) = 2 )
18 17 eqcomd 
 |-  ( 2 e. CC -> 2 = ( 2 ^ 1 ) )
19 16 18 mp1i 
 |-  ( N e. NN -> 2 = ( 2 ^ 1 ) )
20 19 oveq1d 
 |-  ( N e. NN -> ( 2 x. ( 2 ^ ( ( #b ` N ) - 1 ) ) ) = ( ( 2 ^ 1 ) x. ( 2 ^ ( ( #b ` N ) - 1 ) ) ) )
21 7 nncnd 
 |-  ( N e. NN -> ( 2 ^ ( ( #b ` N ) - 1 ) ) e. CC )
22 21 2timesd 
 |-  ( N e. NN -> ( 2 x. ( 2 ^ ( ( #b ` N ) - 1 ) ) ) = ( ( 2 ^ ( ( #b ` N ) - 1 ) ) + ( 2 ^ ( ( #b ` N ) - 1 ) ) ) )
23 16 a1i 
 |-  ( N e. NN -> 2 e. CC )
24 1nn0 
 |-  1 e. NN0
25 24 a1i 
 |-  ( N e. NN -> 1 e. NN0 )
26 23 6 25 expaddd 
 |-  ( N e. NN -> ( 2 ^ ( 1 + ( ( #b ` N ) - 1 ) ) ) = ( ( 2 ^ 1 ) x. ( 2 ^ ( ( #b ` N ) - 1 ) ) ) )
27 1cnd 
 |-  ( N e. NN -> 1 e. CC )
28 4 nncnd 
 |-  ( N e. NN -> ( #b ` N ) e. CC )
29 27 28 pncan3d 
 |-  ( N e. NN -> ( 1 + ( ( #b ` N ) - 1 ) ) = ( #b ` N ) )
30 29 oveq2d 
 |-  ( N e. NN -> ( 2 ^ ( 1 + ( ( #b ` N ) - 1 ) ) ) = ( 2 ^ ( #b ` N ) ) )
31 26 30 eqtr3d 
 |-  ( N e. NN -> ( ( 2 ^ 1 ) x. ( 2 ^ ( ( #b ` N ) - 1 ) ) ) = ( 2 ^ ( #b ` N ) ) )
32 20 22 31 3eqtr3d 
 |-  ( N e. NN -> ( ( 2 ^ ( ( #b ` N ) - 1 ) ) + ( 2 ^ ( ( #b ` N ) - 1 ) ) ) = ( 2 ^ ( #b ` N ) ) )
33 32 breq2d 
 |-  ( N e. NN -> ( N < ( ( 2 ^ ( ( #b ` N ) - 1 ) ) + ( 2 ^ ( ( #b ` N ) - 1 ) ) ) <-> N < ( 2 ^ ( #b ` N ) ) ) )
34 15 33 bitrd 
 |-  ( N e. NN -> ( ( N - ( 2 ^ ( ( #b ` N ) - 1 ) ) ) < ( 2 ^ ( ( #b ` N ) - 1 ) ) <-> N < ( 2 ^ ( #b ` N ) ) ) )
35 14 34 anbi12d 
 |-  ( N e. NN -> ( ( 0 <_ ( N - ( 2 ^ ( ( #b ` N ) - 1 ) ) ) /\ ( N - ( 2 ^ ( ( #b ` N ) - 1 ) ) ) < ( 2 ^ ( ( #b ` N ) - 1 ) ) ) <-> ( ( 2 ^ ( ( #b ` N ) - 1 ) ) <_ N /\ N < ( 2 ^ ( #b ` N ) ) ) ) )
36 13 35 mpbird 
 |-  ( N e. NN -> ( 0 <_ ( N - ( 2 ^ ( ( #b ` N ) - 1 ) ) ) /\ ( N - ( 2 ^ ( ( #b ` N ) - 1 ) ) ) < ( 2 ^ ( ( #b ` N ) - 1 ) ) ) )
37 modid 
 |-  ( ( ( ( N - ( 2 ^ ( ( #b ` N ) - 1 ) ) ) e. RR /\ ( 2 ^ ( ( #b ` N ) - 1 ) ) e. RR+ ) /\ ( 0 <_ ( N - ( 2 ^ ( ( #b ` N ) - 1 ) ) ) /\ ( N - ( 2 ^ ( ( #b ` N ) - 1 ) ) ) < ( 2 ^ ( ( #b ` N ) - 1 ) ) ) ) -> ( ( N - ( 2 ^ ( ( #b ` N ) - 1 ) ) ) mod ( 2 ^ ( ( #b ` N ) - 1 ) ) ) = ( N - ( 2 ^ ( ( #b ` N ) - 1 ) ) ) )
38 12 8 36 37 syl21anc 
 |-  ( N e. NN -> ( ( N - ( 2 ^ ( ( #b ` N ) - 1 ) ) ) mod ( 2 ^ ( ( #b ` N ) - 1 ) ) ) = ( N - ( 2 ^ ( ( #b ` N ) - 1 ) ) ) )
39 10 38 eqtr2d 
 |-  ( N e. NN -> ( N - ( 2 ^ ( ( #b ` N ) - 1 ) ) ) = ( N mod ( 2 ^ ( ( #b ` N ) - 1 ) ) ) )
40 nncn 
 |-  ( N e. NN -> N e. CC )
41 nnz 
 |-  ( N e. NN -> N e. ZZ )
42 41 7 zmodcld 
 |-  ( N e. NN -> ( N mod ( 2 ^ ( ( #b ` N ) - 1 ) ) ) e. NN0 )
43 42 nn0cnd 
 |-  ( N e. NN -> ( N mod ( 2 ^ ( ( #b ` N ) - 1 ) ) ) e. CC )
44 40 21 43 subaddd 
 |-  ( N e. NN -> ( ( N - ( 2 ^ ( ( #b ` N ) - 1 ) ) ) = ( N mod ( 2 ^ ( ( #b ` N ) - 1 ) ) ) <-> ( ( 2 ^ ( ( #b ` N ) - 1 ) ) + ( N mod ( 2 ^ ( ( #b ` N ) - 1 ) ) ) ) = N ) )
45 39 44 mpbid 
 |-  ( N e. NN -> ( ( 2 ^ ( ( #b ` N ) - 1 ) ) + ( N mod ( 2 ^ ( ( #b ` N ) - 1 ) ) ) ) = N )
46 45 eqcomd 
 |-  ( N e. NN -> N = ( ( 2 ^ ( ( #b ` N ) - 1 ) ) + ( N mod ( 2 ^ ( ( #b ` N ) - 1 ) ) ) ) )