Metamath Proof Explorer

Theorem nnpw2p

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 nnpw2p ( 𝑁 ∈ ℕ → ∃ 𝑖 ∈ ℕ0 ∃ 𝑟 ∈ ( 0 ..^ ( 2 ↑ 𝑖 ) ) 𝑁 = ( ( 2 ↑ 𝑖 ) + 𝑟 ) )

Proof

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