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

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

%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

zero_set_within_nat = ProperSubset(ZeroSet, Natural)

zero_set_within_nat (conjecture without proof):

interval_is_nat = Forall((a, b), Forall(n, InSet(n, Natural), 
                                       domain=Interval(a, b)), domain=Natural)

interval_is_nat (conjecture without proof):

natural_lower_bound = Forall(n, greater_eq(n, zero), domain=Natural)

natural_lower_bound (conjecture without proof):

natural_pos_lower_bound = Forall(n, greater_eq(n, one), domain=NaturalPos)

natural_pos_lower_bound (conjecture without proof):

natural_pos_is_pos = Forall(n, greater(n, zero), domain=NaturalPos)

natural_pos_is_pos (conjecture without proof):

# proven
nonzero_if_is_nat_pos = Forall(
        n,
        NotEquals(n, zero),
        domain=NaturalPos)

nonzero_if_is_nat_pos (conjecture with conjecture-based proof):

nat_pos_within_nat = ProperSubset(NaturalPos, Natural)

nat_pos_within_nat (conjecture without proof):

# In progress
# For Natural numbers
nat_membership_is_bool = Forall(x, in_bool(InSet(x, Natural)))

nat_membership_is_bool (conjecture without proof):

# 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):

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):

fold_forall_natural_pos = Forall(P, Implies(And(Pone, 
                                                 Forall(m, P_mAddOne, domain=NaturalPos, 
                                                        condition=Pm)), 
                                             Forall(n, Pn, domain=NaturalPos)))

fold_forall_natural_pos (conjecture without proof):

%end theorems

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