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 ( ๐‘ โˆˆ โ„• โ†’ ๐‘ = ( ( 2 โ†‘ ( ( #b โ€˜ ๐‘ ) โˆ’ 1 ) ) + ( ๐‘ mod ( 2 โ†‘ ( ( #b โ€˜ ๐‘ ) โˆ’ 1 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 nnre โŠข ( ๐‘ โˆˆ โ„• โ†’ ๐‘ โˆˆ โ„ )
2 2nn โŠข 2 โˆˆ โ„•
3 2 a1i โŠข ( ๐‘ โˆˆ โ„• โ†’ 2 โˆˆ โ„• )
4 blennnelnn โŠข ( ๐‘ โˆˆ โ„• โ†’ ( #b โ€˜ ๐‘ ) โˆˆ โ„• )
5 nnm1nn0 โŠข ( ( #b โ€˜ ๐‘ ) โˆˆ โ„• โ†’ ( ( #b โ€˜ ๐‘ ) โˆ’ 1 ) โˆˆ โ„•0 )
6 4 5 syl โŠข ( ๐‘ โˆˆ โ„• โ†’ ( ( #b โ€˜ ๐‘ ) โˆ’ 1 ) โˆˆ โ„•0 )
7 3 6 nnexpcld โŠข ( ๐‘ โˆˆ โ„• โ†’ ( 2 โ†‘ ( ( #b โ€˜ ๐‘ ) โˆ’ 1 ) ) โˆˆ โ„• )
8 7 nnrpd โŠข ( ๐‘ โˆˆ โ„• โ†’ ( 2 โ†‘ ( ( #b โ€˜ ๐‘ ) โˆ’ 1 ) ) โˆˆ โ„+ )
9 modeqmodmin โŠข ( ( ๐‘ โˆˆ โ„ โˆง ( 2 โ†‘ ( ( #b โ€˜ ๐‘ ) โˆ’ 1 ) ) โˆˆ โ„+ ) โ†’ ( ๐‘ mod ( 2 โ†‘ ( ( #b โ€˜ ๐‘ ) โˆ’ 1 ) ) ) = ( ( ๐‘ โˆ’ ( 2 โ†‘ ( ( #b โ€˜ ๐‘ ) โˆ’ 1 ) ) ) mod ( 2 โ†‘ ( ( #b โ€˜ ๐‘ ) โˆ’ 1 ) ) ) )
10 1 8 9 syl2anc โŠข ( ๐‘ โˆˆ โ„• โ†’ ( ๐‘ mod ( 2 โ†‘ ( ( #b โ€˜ ๐‘ ) โˆ’ 1 ) ) ) = ( ( ๐‘ โˆ’ ( 2 โ†‘ ( ( #b โ€˜ ๐‘ ) โˆ’ 1 ) ) ) mod ( 2 โ†‘ ( ( #b โ€˜ ๐‘ ) โˆ’ 1 ) ) ) )
11 7 nnred โŠข ( ๐‘ โˆˆ โ„• โ†’ ( 2 โ†‘ ( ( #b โ€˜ ๐‘ ) โˆ’ 1 ) ) โˆˆ โ„ )
12 1 11 resubcld โŠข ( ๐‘ โˆˆ โ„• โ†’ ( ๐‘ โˆ’ ( 2 โ†‘ ( ( #b โ€˜ ๐‘ ) โˆ’ 1 ) ) ) โˆˆ โ„ )
13 nnpw2blen โŠข ( ๐‘ โˆˆ โ„• โ†’ ( ( 2 โ†‘ ( ( #b โ€˜ ๐‘ ) โˆ’ 1 ) ) โ‰ค ๐‘ โˆง ๐‘ < ( 2 โ†‘ ( #b โ€˜ ๐‘ ) ) ) )
14 1 11 subge0d โŠข ( ๐‘ โˆˆ โ„• โ†’ ( 0 โ‰ค ( ๐‘ โˆ’ ( 2 โ†‘ ( ( #b โ€˜ ๐‘ ) โˆ’ 1 ) ) ) โ†” ( 2 โ†‘ ( ( #b โ€˜ ๐‘ ) โˆ’ 1 ) ) โ‰ค ๐‘ ) )
15 1 11 11 ltsubadd2d โŠข ( ๐‘ โˆˆ โ„• โ†’ ( ( ๐‘ โˆ’ ( 2 โ†‘ ( ( #b โ€˜ ๐‘ ) โˆ’ 1 ) ) ) < ( 2 โ†‘ ( ( #b โ€˜ ๐‘ ) โˆ’ 1 ) ) โ†” ๐‘ < ( ( 2 โ†‘ ( ( #b โ€˜ ๐‘ ) โˆ’ 1 ) ) + ( 2 โ†‘ ( ( #b โ€˜ ๐‘ ) โˆ’ 1 ) ) ) ) )
16 2cn โŠข 2 โˆˆ โ„‚
17 exp1 โŠข ( 2 โˆˆ โ„‚ โ†’ ( 2 โ†‘ 1 ) = 2 )
18 17 eqcomd โŠข ( 2 โˆˆ โ„‚ โ†’ 2 = ( 2 โ†‘ 1 ) )
19 16 18 mp1i โŠข ( ๐‘ โˆˆ โ„• โ†’ 2 = ( 2 โ†‘ 1 ) )
20 19 oveq1d โŠข ( ๐‘ โˆˆ โ„• โ†’ ( 2 ยท ( 2 โ†‘ ( ( #b โ€˜ ๐‘ ) โˆ’ 1 ) ) ) = ( ( 2 โ†‘ 1 ) ยท ( 2 โ†‘ ( ( #b โ€˜ ๐‘ ) โˆ’ 1 ) ) ) )
21 7 nncnd โŠข ( ๐‘ โˆˆ โ„• โ†’ ( 2 โ†‘ ( ( #b โ€˜ ๐‘ ) โˆ’ 1 ) ) โˆˆ โ„‚ )
22 21 2timesd โŠข ( ๐‘ โˆˆ โ„• โ†’ ( 2 ยท ( 2 โ†‘ ( ( #b โ€˜ ๐‘ ) โˆ’ 1 ) ) ) = ( ( 2 โ†‘ ( ( #b โ€˜ ๐‘ ) โˆ’ 1 ) ) + ( 2 โ†‘ ( ( #b โ€˜ ๐‘ ) โˆ’ 1 ) ) ) )
23 16 a1i โŠข ( ๐‘ โˆˆ โ„• โ†’ 2 โˆˆ โ„‚ )
24 1nn0 โŠข 1 โˆˆ โ„•0
25 24 a1i โŠข ( ๐‘ โˆˆ โ„• โ†’ 1 โˆˆ โ„•0 )
26 23 6 25 expaddd โŠข ( ๐‘ โˆˆ โ„• โ†’ ( 2 โ†‘ ( 1 + ( ( #b โ€˜ ๐‘ ) โˆ’ 1 ) ) ) = ( ( 2 โ†‘ 1 ) ยท ( 2 โ†‘ ( ( #b โ€˜ ๐‘ ) โˆ’ 1 ) ) ) )
27 1cnd โŠข ( ๐‘ โˆˆ โ„• โ†’ 1 โˆˆ โ„‚ )
28 4 nncnd โŠข ( ๐‘ โˆˆ โ„• โ†’ ( #b โ€˜ ๐‘ ) โˆˆ โ„‚ )
29 27 28 pncan3d โŠข ( ๐‘ โˆˆ โ„• โ†’ ( 1 + ( ( #b โ€˜ ๐‘ ) โˆ’ 1 ) ) = ( #b โ€˜ ๐‘ ) )
30 29 oveq2d โŠข ( ๐‘ โˆˆ โ„• โ†’ ( 2 โ†‘ ( 1 + ( ( #b โ€˜ ๐‘ ) โˆ’ 1 ) ) ) = ( 2 โ†‘ ( #b โ€˜ ๐‘ ) ) )
31 26 30 eqtr3d โŠข ( ๐‘ โˆˆ โ„• โ†’ ( ( 2 โ†‘ 1 ) ยท ( 2 โ†‘ ( ( #b โ€˜ ๐‘ ) โˆ’ 1 ) ) ) = ( 2 โ†‘ ( #b โ€˜ ๐‘ ) ) )
32 20 22 31 3eqtr3d โŠข ( ๐‘ โˆˆ โ„• โ†’ ( ( 2 โ†‘ ( ( #b โ€˜ ๐‘ ) โˆ’ 1 ) ) + ( 2 โ†‘ ( ( #b โ€˜ ๐‘ ) โˆ’ 1 ) ) ) = ( 2 โ†‘ ( #b โ€˜ ๐‘ ) ) )
33 32 breq2d โŠข ( ๐‘ โˆˆ โ„• โ†’ ( ๐‘ < ( ( 2 โ†‘ ( ( #b โ€˜ ๐‘ ) โˆ’ 1 ) ) + ( 2 โ†‘ ( ( #b โ€˜ ๐‘ ) โˆ’ 1 ) ) ) โ†” ๐‘ < ( 2 โ†‘ ( #b โ€˜ ๐‘ ) ) ) )
34 15 33 bitrd โŠข ( ๐‘ โˆˆ โ„• โ†’ ( ( ๐‘ โˆ’ ( 2 โ†‘ ( ( #b โ€˜ ๐‘ ) โˆ’ 1 ) ) ) < ( 2 โ†‘ ( ( #b โ€˜ ๐‘ ) โˆ’ 1 ) ) โ†” ๐‘ < ( 2 โ†‘ ( #b โ€˜ ๐‘ ) ) ) )
35 14 34 anbi12d โŠข ( ๐‘ โˆˆ โ„• โ†’ ( ( 0 โ‰ค ( ๐‘ โˆ’ ( 2 โ†‘ ( ( #b โ€˜ ๐‘ ) โˆ’ 1 ) ) ) โˆง ( ๐‘ โˆ’ ( 2 โ†‘ ( ( #b โ€˜ ๐‘ ) โˆ’ 1 ) ) ) < ( 2 โ†‘ ( ( #b โ€˜ ๐‘ ) โˆ’ 1 ) ) ) โ†” ( ( 2 โ†‘ ( ( #b โ€˜ ๐‘ ) โˆ’ 1 ) ) โ‰ค ๐‘ โˆง ๐‘ < ( 2 โ†‘ ( #b โ€˜ ๐‘ ) ) ) ) )
36 13 35 mpbird โŠข ( ๐‘ โˆˆ โ„• โ†’ ( 0 โ‰ค ( ๐‘ โˆ’ ( 2 โ†‘ ( ( #b โ€˜ ๐‘ ) โˆ’ 1 ) ) ) โˆง ( ๐‘ โˆ’ ( 2 โ†‘ ( ( #b โ€˜ ๐‘ ) โˆ’ 1 ) ) ) < ( 2 โ†‘ ( ( #b โ€˜ ๐‘ ) โˆ’ 1 ) ) ) )
37 modid โŠข ( ( ( ( ๐‘ โˆ’ ( 2 โ†‘ ( ( #b โ€˜ ๐‘ ) โˆ’ 1 ) ) ) โˆˆ โ„ โˆง ( 2 โ†‘ ( ( #b โ€˜ ๐‘ ) โˆ’ 1 ) ) โˆˆ โ„+ ) โˆง ( 0 โ‰ค ( ๐‘ โˆ’ ( 2 โ†‘ ( ( #b โ€˜ ๐‘ ) โˆ’ 1 ) ) ) โˆง ( ๐‘ โˆ’ ( 2 โ†‘ ( ( #b โ€˜ ๐‘ ) โˆ’ 1 ) ) ) < ( 2 โ†‘ ( ( #b โ€˜ ๐‘ ) โˆ’ 1 ) ) ) ) โ†’ ( ( ๐‘ โˆ’ ( 2 โ†‘ ( ( #b โ€˜ ๐‘ ) โˆ’ 1 ) ) ) mod ( 2 โ†‘ ( ( #b โ€˜ ๐‘ ) โˆ’ 1 ) ) ) = ( ๐‘ โˆ’ ( 2 โ†‘ ( ( #b โ€˜ ๐‘ ) โˆ’ 1 ) ) ) )
38 12 8 36 37 syl21anc โŠข ( ๐‘ โˆˆ โ„• โ†’ ( ( ๐‘ โˆ’ ( 2 โ†‘ ( ( #b โ€˜ ๐‘ ) โˆ’ 1 ) ) ) mod ( 2 โ†‘ ( ( #b โ€˜ ๐‘ ) โˆ’ 1 ) ) ) = ( ๐‘ โˆ’ ( 2 โ†‘ ( ( #b โ€˜ ๐‘ ) โˆ’ 1 ) ) ) )
39 10 38 eqtr2d โŠข ( ๐‘ โˆˆ โ„• โ†’ ( ๐‘ โˆ’ ( 2 โ†‘ ( ( #b โ€˜ ๐‘ ) โˆ’ 1 ) ) ) = ( ๐‘ mod ( 2 โ†‘ ( ( #b โ€˜ ๐‘ ) โˆ’ 1 ) ) ) )
40 nncn โŠข ( ๐‘ โˆˆ โ„• โ†’ ๐‘ โˆˆ โ„‚ )
41 nnz โŠข ( ๐‘ โˆˆ โ„• โ†’ ๐‘ โˆˆ โ„ค )
42 41 7 zmodcld โŠข ( ๐‘ โˆˆ โ„• โ†’ ( ๐‘ mod ( 2 โ†‘ ( ( #b โ€˜ ๐‘ ) โˆ’ 1 ) ) ) โˆˆ โ„•0 )
43 42 nn0cnd โŠข ( ๐‘ โˆˆ โ„• โ†’ ( ๐‘ mod ( 2 โ†‘ ( ( #b โ€˜ ๐‘ ) โˆ’ 1 ) ) ) โˆˆ โ„‚ )
44 40 21 43 subaddd โŠข ( ๐‘ โˆˆ โ„• โ†’ ( ( ๐‘ โˆ’ ( 2 โ†‘ ( ( #b โ€˜ ๐‘ ) โˆ’ 1 ) ) ) = ( ๐‘ mod ( 2 โ†‘ ( ( #b โ€˜ ๐‘ ) โˆ’ 1 ) ) ) โ†” ( ( 2 โ†‘ ( ( #b โ€˜ ๐‘ ) โˆ’ 1 ) ) + ( ๐‘ mod ( 2 โ†‘ ( ( #b โ€˜ ๐‘ ) โˆ’ 1 ) ) ) ) = ๐‘ ) )
45 39 44 mpbid โŠข ( ๐‘ โˆˆ โ„• โ†’ ( ( 2 โ†‘ ( ( #b โ€˜ ๐‘ ) โˆ’ 1 ) ) + ( ๐‘ mod ( 2 โ†‘ ( ( #b โ€˜ ๐‘ ) โˆ’ 1 ) ) ) ) = ๐‘ )
46 45 eqcomd โŠข ( ๐‘ โˆˆ โ„• โ†’ ๐‘ = ( ( 2 โ†‘ ( ( #b โ€˜ ๐‘ ) โˆ’ 1 ) ) + ( ๐‘ mod ( 2 โ†‘ ( ( #b โ€˜ ๐‘ ) โˆ’ 1 ) ) ) ) )