Proof of proveit.numbers.numerals.decimals.nat1 theorem¶

In [1]:
import proveit
from proveit import n
from proveit.numbers import zero, one, Add
from proveit.numbers.numerals.decimals  import one_def
from proveit.numbers.number_sets.natural_numbers  import zero_in_nats, successor_in_nats
theory = proveit.Theory() # the theorem's theory

In [2]:
%proving nat1

With these allowed/disallowed theorem/theory presumptions (e.g., to avoid circular dependencies), we begin our proof of
nat1:
(see dependencies)
In [3]:
one_def

In [4]:
successor_in_nats

In [5]:
zero_plus_one__in__nats = successor_in_nats.instantiate({n:zero})

zero_plus_one__in__nats:
nat1 has been proven.  Now simply execute "%qed".

In [6]:
%qed

proveit.numbers.numerals.decimals.nat1 has been proven.

Out[6]:
step typerequirementsstatement
0instantiation1, 2, 3*
:
1axiom
proveit.numbers.number_sets.natural_numbers.successor_in_nats
2axiom
proveit.numbers.number_sets.natural_numbers.zero_in_nats
3instantiation4, 5
: , :
4theorem
proveit.logic.equality.equals_reversal
5axiom
proveit.numbers.numerals.decimals.one_def
*equality replacement requirements