# Theorems (or conjectures) for the theory of proveit.numbers.number_sets.natural_numbers¶

In [1]:
import proveit
# Prepare this notebook for defining the theorems of a theory:
%theorems_notebook # Keep this at the top following 'import proveit'.
from proveit import Operation
from proveit import a, b, m, n, x, P
from proveit.logic import And, Equals, NotEquals, Forall, Implies, in_bool, InSet, ProperSubset, Set
from proveit.numbers import zero, one, num, frac
from proveit.numbers import ZeroSet, Natural, NaturalPos, Integer, Interval, Rational, Real, RealPos, Complex
from proveit.numbers import Add, subtract, greater, greater_eq, Less, LessEq
from proveit.numbers import Pzero, Pone, Pm, P_mAddOne, Pn

In [2]:
%begin theorems

Defining theorems for theory 'proveit.numbers.number_sets.natural_numbers'
Subsequent end-of-cell assignments will define theorems
'%end theorems' will finalize the definitions

In [3]:
zero_set_within_nat = ProperSubset(ZeroSet, Natural)

zero_set_within_nat (conjecture without proof):

In [4]:
interval_is_nat = Forall((a, b), Forall(n, InSet(n, Natural),
domain=Interval(a, b)), domain=Natural)

interval_is_nat (conjecture without proof):

In [5]:
natural_lower_bound = Forall(n, greater_eq(n, zero), domain=Natural)

natural_lower_bound (conjecture without proof):

In [6]:
natural_pos_lower_bound = Forall(n, greater_eq(n, one), domain=NaturalPos)

natural_pos_lower_bound (conjecture without proof):

In [7]:
natural_pos_is_pos = Forall(n, greater(n, zero), domain=NaturalPos)

natural_pos_is_pos (conjecture without proof):

In [8]:
# proven
nonzero_if_is_nat_pos = Forall(
n,
NotEquals(n, zero),
domain=NaturalPos)

nonzero_if_is_nat_pos (conjecture with conjecture-based proof):

In [9]:
nat_pos_within_nat = ProperSubset(NaturalPos, Natural)

nat_pos_within_nat (conjecture without proof):

In [10]:
# In progress
# For Natural numbers
nat_membership_is_bool = Forall(x, in_bool(InSet(x, Natural)))

nat_membership_is_bool (conjecture without proof):

In [11]:
# For Positive Natural numbers (NaturalPos)
nat_pos_membership_is_bool = Forall(x, in_bool(InSet(x, NaturalPos)))

nat_pos_membership_is_bool (conjecture without proof):

In [12]:
fold_forall_natural = Forall(P, Implies(And(Pzero,
domain=Natural, condition=Pm)),
Forall(n, Pn, domain=Natural)))

fold_forall_natural (conjecture without proof):

In [13]:
fold_forall_natural_pos = Forall(P, Implies(And(Pone,

%end theorems

These theorems may now be imported from the theory package: proveit.numbers.number_sets.natural_numbers