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
from proveit.numbers import zero, one, num, frac
from proveit.numbers import Natural, NaturalPos, Integer, Interval, Rational, Real, RealPos, Complex
from proveit.numbers import Add, subtract, greater_eq, Less, LessEq
from proveit.numbers import Pzero, Pone, Pm, P_mAddOne, Pn
```

In [2]:

```
%begin theorems
```

In [3]:

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

Out[3]:

In [4]:

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

Out[4]:

In [5]:

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

Out[5]:

In [6]:

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

Out[6]:

In [7]:

```
nat_pos_within_nat = ProperSubset(NaturalPos, Natural)
```

Out[7]:

In [8]:

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

Out[8]:

In [9]:

```
# For Positive Natural numbers (NaturalPos)
nat_pos_membership_is_bool = Forall(x, in_bool(InSet(x, NaturalPos)))
```

Out[9]:

In [10]:

```
fold_forall_natural = Forall(P, Implies(And(Pzero,
Forall(m, P_mAddOne,
domain=Natural, condition=Pm)),
Forall(n, Pn, domain=Natural)))
```

Out[10]:

In [11]:

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

Out[11]:

In [12]:

```
%end theorems
```

These web pages were generated on 2021-01-19 by Prove-It Beta Version 0.3, licensed under the GNU Public License by Sandia Corporation.

Presented proofs are not absolutely guaranteed. For assurance, it is important to check the structure of the statement being proven, independently verify the derivation steps, track dependencies, and ensure that employed axioms are valid and properly structured. Inconsistencies may exist, unknowingly, in this system.

This material is based upon work supported by the U.S. Department of Energy, Office of Science, Office of Advanced Scientific Computing Research, under the Quantum Computing Application Teams program. Sandia National Labs is managed and operated by National Technology and Engineering Solutions of Sandia, LLC, a subsidiary of Honeywell International, Inc., for the U.S. Dept. of Energy's NNSA under contract DE-NA0003525. The views expressed above do not necessarily represent the views of the DOE or the U.S. Government.

Please send questions/comments to: wwitzel@sandia.gov.