Proof of proveit.numbers.number_sets.integers.zero_is_int theorem¶
In [1]:
import proveit
from proveit import x, A, B
from proveit.numbers import zero, Integer, Natural
from proveit.numbers.number_sets.natural_numbers import zero_in_nats
from proveit.numbers.number_sets.integers import nat_within_int
theory = proveit.Theory() # the theorem's theory
In [2]:
%proving zero_is_int
With these allowed/disallowed theorem/theory presumptions (e.g., to avoid circular dependencies), we begin our proof of
zero_is_int:
(see dependencies)
zero_is_int:
(see dependencies)
In [3]:
zero_in_nats
In [4]:
nat_within_int
In [5]:
%qed
Out[5]:
| step type | requirements | statement | ||
|---|---|---|---|---|
| 0 | instantiation | 1, 2, 3 | ⊢ | |
 :  ,  :  ,  :  | ||||
| 1 | theorem | ⊢  | ||
| proveit.logic.sets.inclusion.superset_membership_from_proper_subset | ||||
| 2 | conjecture | ⊢  | ||
| proveit.numbers.number_sets.integers.nat_within_int | ||||
| 3 | axiom | ⊢  | ||
| proveit.numbers.number_sets.natural_numbers.zero_in_nats | ||||