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(
        NotEquals(n, zero),
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, 
                                             Forall(m, P_mAddOne, 
                                                 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, 
                                                 Forall(m, P_mAddOne, domain=NaturalPos, 
                                             Forall(n, Pn, domain=NaturalPos)))
fold_forall_natural_pos (conjecture without proof):

In [14]:
%end theorems
These theorems may now be imported from the theory package: proveit.numbers.number_sets.natural_numbers