Theorem nnpw2pb

Description: A number is a positive integer iff it 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	nnpw2pb	⊢ ( 𝑁 ∈ ℕ ↔ ∃ 𝑖 ∈ ℕ0 ∃ 𝑟 ∈ ( 0 ..^ ( 2 ↑ 𝑖 ) ) 𝑁 = ( ( 2 ↑ 𝑖 ) + 𝑟 ) )

Proof

Step	Hyp	Ref	Expression
1		nnpw2p	⊢ ( 𝑁 ∈ ℕ → ∃ 𝑖 ∈ ℕ0 ∃ 𝑟 ∈ ( 0 ..^ ( 2 ↑ 𝑖 ) ) 𝑁 = ( ( 2 ↑ 𝑖 ) + 𝑟 ) )
2		2nn	⊢ 2 ∈ ℕ
3		nnexpcl	⊢ ( ( 2 ∈ ℕ ∧ 𝑖 ∈ ℕ0 ) → ( 2 ↑ 𝑖 ) ∈ ℕ )
4	2 3	mpan	⊢ ( 𝑖 ∈ ℕ0 → ( 2 ↑ 𝑖 ) ∈ ℕ )
5		elfzonn0	⊢ ( 𝑟 ∈ ( 0 ..^ ( 2 ↑ 𝑖 ) ) → 𝑟 ∈ ℕ0 )
6		nnnn0addcl	⊢ ( ( ( 2 ↑ 𝑖 ) ∈ ℕ ∧ 𝑟 ∈ ℕ0 ) → ( ( 2 ↑ 𝑖 ) + 𝑟 ) ∈ ℕ )
7	4 5 6	syl2an	⊢ ( ( 𝑖 ∈ ℕ0 ∧ 𝑟 ∈ ( 0 ..^ ( 2 ↑ 𝑖 ) ) ) → ( ( 2 ↑ 𝑖 ) + 𝑟 ) ∈ ℕ )
8		eleq1	⊢ ( 𝑁 = ( ( 2 ↑ 𝑖 ) + 𝑟 ) → ( 𝑁 ∈ ℕ ↔ ( ( 2 ↑ 𝑖 ) + 𝑟 ) ∈ ℕ ) )
9	7 8	syl5ibrcom	⊢ ( ( 𝑖 ∈ ℕ0 ∧ 𝑟 ∈ ( 0 ..^ ( 2 ↑ 𝑖 ) ) ) → ( 𝑁 = ( ( 2 ↑ 𝑖 ) + 𝑟 ) → 𝑁 ∈ ℕ ) )
10	9	rexlimivv	⊢ ( ∃ 𝑖 ∈ ℕ0 ∃ 𝑟 ∈ ( 0 ..^ ( 2 ↑ 𝑖 ) ) 𝑁 = ( ( 2 ↑ 𝑖 ) + 𝑟 ) → 𝑁 ∈ ℕ )
11	1 10	impbii	⊢ ( 𝑁 ∈ ℕ ↔ ∃ 𝑖 ∈ ℕ0 ∃ 𝑟 ∈ ( 0 ..^ ( 2 ↑ 𝑖 ) ) 𝑁 = ( ( 2 ↑ 𝑖 ) + 𝑟 ) )