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 ) ) ) ) )