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 ..^ 2 i N = 2 i + 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 → 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 → ∃ r ∈ 0 ..^ 2 i N = 2 i + r ↔ ∃ r ∈ 0 ..^ 2 # b ⁡ N − 1 N = 2 # b ⁡ N − 1 + r
9 8 adantl ⊢ N ∈ ℕ ∧ i = # b ⁡ N − 1 → ∃ r ∈ 0 ..^ 2 i N = 2 i + r ↔ ∃ r ∈ 0 ..^ 2 # b ⁡ N − 1 N = 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 ∈ ℕ → N mod 2 # b ⁡ N − 1 ∈ 0 ..^ 2 # b ⁡ N − 1
15 10 13 14 syl2anc ⊢ N ∈ ℕ → N mod 2 # b ⁡ N − 1 ∈ 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 ∈ ℕ ∧ 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 ∈ ℕ → N = 2 # b ⁡ N − 1 + N mod 2 # 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 ..^ 2 i N = 2 i + r