# Proof of proveit.numbers.number_sets.integers.nonneg_int_is_natural theorem¶

In [1]:
import proveit
from proveit import defaults
from proveit import a, m, n, x, A, B
from proveit.core_expr_types import A_1_to_m
from proveit.numbers import zero, num, Neg, NaturalPos, Integer, greater, Natural, greater_eq
from proveit.logic import NotInSet, SetOfAll, InSet, Implies, And
from proveit.logic.sets.unification import membership_unfolding
from proveit.numbers.number_sets.natural_numbers  import natural_pos_def
from proveit.numbers.number_sets.integers  import integers_def
theory = proveit.Theory() # the theorem's theory

In [2]:
%proving nonneg_int_is_natural

With these allowed/disallowed theorem/theory presumptions (e.g., to avoid circular dependencies), we begin our proof of
nonneg_int_is_natural:
(see dependencies)
nonneg_int_is_natural may now be readily provable (assuming required theorems are usable).  Simply execute "%qed".

In [3]:
# defaults.assumptions = nonneg_int_is_natural.conditions

In [4]:
# integers_def

In [5]:
# int_union = integers_def.expr.rhs

In [6]:
# int_union.operands

In [7]:
# membership_unfolding

In [8]:
# spec1 = membership_unfolding.instantiate({x:a, m:num(2), A:int_union.operands}, assumptions = [InSet(m, NaturalPos), *defaults.assumptions])

In [9]:
# a_in_int = defaults.assumptions[0]

In [10]:
# a_elem_union = Implies(And(a_in_int, integers_def.expr),InSet(a,int_union))

In [11]:
# new_assumpt = [defaults.assumptions]+ [integers_def.expr]