Library ▹ Essentials ▹ Numbers ▹ Natural numbers
  • ℕ
  • Positional notation
  • +
  • (0) + n = n  if n ∈ ℕ
  • (m+1) + n = ((m + n)+1)  if m, n ∈ ℕ
  • (n+1) = n + 1  if n ∈ ℕ
  • (l + m) + n = l + (m + n)  if l, m, n ∈ ℕ
  • + is associative
  • m + n = n + m  if m, n ∈ ℕ
  • + is commutative
  • m + n = 0  ⇒  m = n = 0  if m, n ∈ ℕ
  • a + c = b + c  ⇒  a = b  if a, b, c ∈ ℕ
  • m + n = m  ⇒  n = 0  if m, n ∈ ℕ
  • ≤
  • <
  • ≤ is a total order
  • a < b ≤ c  ⇒  a < c  if a, b, c ∈ ℕ
  • a ≤ b < c  ⇒  a < c  if a, b, c ∈ ℕ
  • n ≥ 0  if n ∈ ℕ
  • n ≤ 0  ⇒  n = 0  if n ∈ ℕ
  • n + 1 > n  if n ∈ ℕ
  • Subsets
  • ∃ m ∈ M : m is a ≤-greatest element of M  if M ⊆ ℕ, k ∈ ℕ, f : ℕ≤k ↔ M is a bijection
  • M is finite  ⇔  M is empty or ∃ m ∈ M : m is a ≤-greatest element of M  ⇔  M is empty or ∃! m ∈ M : m is a ≤-greatest element of M  ⇔  ∃ a ∈ ℕ : M ⊆ ℕ≤a  ⇔  ∃ b ∈ ℕ : M ⊆ ℕ<b  if M ⊆ ℕ
  • −
  • ⋅
  • n ⋅ 1 = n  if n ∈ ℕ
  • ⋅ is associative
  • ⋅ is commutative
  • ⋅ is distributive over +
  • a ⋅ c = b ⋅ c  ⇒  a = b  if a, b ∈ ℕ, c ∈ ℕ+
  • ∣
  • Divℕ(n)
  • m ∣ n  ⇒  m ≤ n  if m, n ∈ ℕ+
  • a ∣ b  ⇒  [a ∣ c  ⇔  a ∣ (b + c)]  if a ∈ ℕ+, b ∈ ℕ, c ∈ ℕ
  • even/odd
  • ∕
  • mn
  • p(0), [∀ m ∈ ℕ s.t. p(m) : p(m + 1)]  ⇒  p(n)  if p is a property on ℕ, n ∈ ℕ
  • 0 ∈ M and ∀ m ∈ M : m + 1 ∈ M  ⇔  ∀ n ∈ ℕ s.t. ℕ<n ⊆ M : n ∈ M  ⇔  M = ℕ  if M ⊆ ℕ
  • ≤ is a well-order
  • min
  • min
  • max
  • max
  • Sequences
  • n!
  • (n!)n ∈ ℕ starts with (1, 1, 2, 6, 24, 120, 720, 5040, 40320, 362880, 3628800, 39916800, 479001600, 6227020800, 87178291200, 1307674368000, 20922789888000, 355687428096000, 6402373705728000, 121645100408832000, 2432902008176640000, 51090942171709440000, 1124000727777607680000)
  • (nk)
  • (nk) = n!∕(k! ⋅ (n − k)!)  if n ∈ ℕ, k ∈ ℕ≤n
  • Iterated operators
  • Prime numbers
  • coprime
  • m and m ⋅ n are not coprime  if m, n ∈ ℕ>1
[View Source]