Metamath Proof Explorer

Theorem nnpw2pmod

Description: Every positive integer can be represented as the sum of a power of 2 and a "remainder" less than the power. (Contributed by AV, 31-May-2020)

Ref Expression
Assertion nnpw2pmod ⊢ N ∈ ℕ → N = 2 # b ⁡ N − 1 + N mod 2 # b ⁡ N − 1

Proof

Step Hyp Ref Expression
1 nnre ⊢ N ∈ ℕ → N ∈ ℝ
2 2nn ⊢ 2 ∈ ℕ
3 2 a1i ⊢ N ∈ ℕ → 2 ∈ ℕ
4 blennnelnn ⊢ N ∈ ℕ → # b ⁡ N ∈ ℕ
5 nnm1nn0 ⊢ # b ⁡ N ∈ ℕ → # b ⁡ N − 1 ∈ ℕ 0
6 4 5 syl ⊢ N ∈ ℕ → # b ⁡ N − 1 ∈ ℕ 0
7 3 6 nnexpcld ⊢ N ∈ ℕ → 2 # b ⁡ N − 1 ∈ ℕ
8 7 nnrpd ⊢ N ∈ ℕ → 2 # b ⁡ N − 1 ∈ ℝ +
9 modeqmodmin ⊢ N ∈ ℝ ∧ 2 # b ⁡ N − 1 ∈ ℝ + → N mod 2 # b ⁡ N − 1 = N − 2 # b ⁡ N − 1 mod 2 # b ⁡ N − 1
10 1 8 9 syl2anc ⊢ N ∈ ℕ → N mod 2 # b ⁡ N − 1 = N − 2 # b ⁡ N − 1 mod 2 # b ⁡ N − 1
11 7 nnred ⊢ N ∈ ℕ → 2 # b ⁡ N − 1 ∈ ℝ
12 1 11 resubcld ⊢ N ∈ ℕ → N − 2 # b ⁡ N − 1 ∈ ℝ
13 nnpw2blen ⊢ N ∈ ℕ → 2 # b ⁡ N − 1 ≤ N ∧ N < 2 # b ⁡ N
14 1 11 subge0d ⊢ N ∈ ℕ → 0 ≤ N − 2 # b ⁡ N − 1 ↔ 2 # b ⁡ N − 1 ≤ N
15 1 11 11 ltsubadd2d ⊢ N ∈ ℕ → N − 2 # b ⁡ N − 1 < 2 # b ⁡ N − 1 ↔ N < 2 # b ⁡ N − 1 + 2 # b ⁡ N − 1
16 2cn ⊢ 2 ∈ ℂ
17 exp1 ⊢ 2 ∈ ℂ → 2 1 = 2
18 17 eqcomd ⊢ 2 ∈ ℂ → 2 = 2 1
19 16 18 mp1i ⊢ N ∈ ℕ → 2 = 2 1
20 19 oveq1d ⊢ N ∈ ℕ → 2 ⁢ 2 # b ⁡ N − 1 = 2 1 ⁢ 2 # b ⁡ N − 1
21 7 nncnd ⊢ N ∈ ℕ → 2 # b ⁡ N − 1 ∈ ℂ
22 21 2timesd ⊢ N ∈ ℕ → 2 ⁢ 2 # b ⁡ N − 1 = 2 # b ⁡ N − 1 + 2 # b ⁡ N − 1
23 16 a1i ⊢ N ∈ ℕ → 2 ∈ ℂ
24 1nn0 ⊢ 1 ∈ ℕ 0
25 24 a1i ⊢ N ∈ ℕ → 1 ∈ ℕ 0
26 23 6 25 expaddd ⊢ N ∈ ℕ → 2 1 + # b ⁡ N - 1 = 2 1 ⁢ 2 # b ⁡ N − 1
27 1cnd ⊢ N ∈ ℕ → 1 ∈ ℂ
28 4 nncnd ⊢ N ∈ ℕ → # b ⁡ N ∈ ℂ
29 27 28 pncan3d ⊢ N ∈ ℕ → 1 + # b ⁡ N - 1 = # b ⁡ N
30 29 oveq2d ⊢ N ∈ ℕ → 2 1 + # b ⁡ N - 1 = 2 # b ⁡ N
31 26 30 eqtr3d ⊢ N ∈ ℕ → 2 1 ⁢ 2 # b ⁡ N − 1 = 2 # b ⁡ N
32 20 22 31 3eqtr3d ⊢ N ∈ ℕ → 2 # b ⁡ N − 1 + 2 # b ⁡ N − 1 = 2 # b ⁡ N
33 32 breq2d ⊢ N ∈ ℕ → N < 2 # b ⁡ N − 1 + 2 # b ⁡ N − 1 ↔ N < 2 # b ⁡ N
34 15 33 bitrd ⊢ N ∈ ℕ → N − 2 # b ⁡ N − 1 < 2 # b ⁡ N − 1 ↔ N < 2 # b ⁡ N
35 14 34 anbi12d ⊢ N ∈ ℕ → 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 ∈ ℕ → 0 ≤ N − 2 # b ⁡ N − 1 ∧ N − 2 # b ⁡ N − 1 < 2 # b ⁡ N − 1
37 modid ⊢ N − 2 # b ⁡ N − 1 ∈ ℝ ∧ 2 # b ⁡ N − 1 ∈ ℝ + ∧ 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 ∈ ℕ → N − 2 # b ⁡ N − 1 mod 2 # b ⁡ N − 1 = N − 2 # b ⁡ N − 1
39 10 38 eqtr2d ⊢ N ∈ ℕ → N − 2 # b ⁡ N − 1 = N mod 2 # b ⁡ N − 1
40 nncn ⊢ N ∈ ℕ → N ∈ ℂ
41 nnz ⊢ N ∈ ℕ → N ∈ ℤ
42 41 7 zmodcld ⊢ N ∈ ℕ → N mod 2 # b ⁡ N − 1 ∈ ℕ 0
43 42 nn0cnd ⊢ N ∈ ℕ → N mod 2 # b ⁡ N − 1 ∈ ℂ
44 40 21 43 subaddd ⊢ N ∈ ℕ → 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 ∈ ℕ → 2 # b ⁡ N − 1 + N mod 2 # b ⁡ N − 1 = N
46 45 eqcomd ⊢ N ∈ ℕ → N = 2 # b ⁡ N − 1 + N mod 2 # b ⁡ N − 1