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∈ℕ→∃i∈ℕ0∃r∈0..^2iN=2i+r

Proof

Step Hyp Ref Expression
1 blennnelnn ⊢N∈ℕ→#b ⁡ N ∈ ℕ
2 nnm1nn0 ⊢#b ⁡ N ∈ ℕ → #b ⁡N−1∈ℕ0
3 1 2 syl ⊢N∈ℕ→#b ⁡ N − 1 ∈ ℕ0
4 oveq2 ⊢i=#b ⁡ N − 1 → 2i=2#b ⁡N−1
5 4 oveq2d ⊢i=#b ⁡ N − 1 → 0..^2i=0..^2#b ⁡N−1
6 4 oveq1d ⊢i=#b ⁡ N − 1 → 2i+r=2#b ⁡N−1+r
7 6 eqeq2d ⊢i=#b ⁡ N − 1 → N=2i+r↔N=2#b ⁡N−1+r
8 5 7 rexeqbidv ⊢i=#b ⁡ N − 1 → ∃r∈0..^2iN=2i+r↔∃r∈0..^2#b ⁡N−1N=2#b ⁡N−1+r
9 8 adantl ⊢N∈ℕ∧i=#b ⁡ N − 1 → ∃r∈0..^2iN=2i+r↔∃r∈0..^2#b ⁡N−1N=2#b ⁡N−1+r
10 nnz ⊢N∈ℕ→N∈ℤ
11 2nn ⊢2∈ℕ
12 11 a1i ⊢N∈ℕ→2∈ℕ
13 12 3 nnexpcld ⊢N∈ℕ→2#b ⁡ N − 1 ∈ ℕ
14 zmodfzo ⊢N∈ℤ∧2#b ⁡ N − 1 ∈ ℕ → Nmod2#b ⁡N−1∈0..^2#b ⁡N−1
15 10 13 14 syl2anc ⊢N∈ℕ→Nmod2#b ⁡ N − 1 ∈ 0..^2#b ⁡N−1
16 oveq2 ⊢r=Nmod2#b ⁡ N − 1 → 2#b ⁡N−1+r=2#b ⁡N−1+Nmod2#b ⁡N−1
17 16 eqeq2d ⊢r=Nmod2#b ⁡ N − 1 → N=2#b ⁡N−1+r↔N=2#b ⁡N−1+Nmod2#b ⁡N−1
18 17 adantl ⊢N∈ℕ∧r=Nmod2#b ⁡ N − 1 → N=2#b ⁡N−1+r↔N=2#b ⁡N−1+Nmod2#b ⁡N−1
19 nnpw2pmod ⊢N∈ℕ→N=2#b ⁡ N − 1 + Nmod2#b ⁡N−1
20 15 18 19 rspcedvd ⊢N∈ℕ→∃r∈0..^2#b ⁡ N − 1 N=2#b ⁡N−1+r
21 3 9 20 rspcedvd ⊢N∈ℕ→∃i∈ℕ0∃r∈0..^2iN=2i+r