| step type | requirements | statement |
0 | instantiation | 1, 2, 3 | ⊢  |
| : , : , :  |
1 | reference | 4 | ⊢  |
2 | instantiation | 4, 5, 6 | ⊢  |
| : , : , :  |
3 | instantiation | 7, 8, 9 | ⊢  |
| : , : , :  |
4 | theorem | | ⊢  |
| proveit.logic.equality.sub_left_side_into |
5 | instantiation | 10, 72, 20, 13, 11 | ⊢  |
| : , : , : , : , :  |
6 | instantiation | 12, 72, 17, 20, 13, 18 | ⊢  |
| : , : , : , : , : , : , :  |
7 | axiom | | ⊢  |
| proveit.logic.equality.equals_transitivity |
8 | instantiation | 14, 72, 17, 20, 18, 15 | ⊢  |
| : , : , : , : , : , :  |
9 | instantiation | 16, 17, 71, 18 | ⊢  |
| : , : , : , : , : , : , :  |
10 | theorem | | ⊢  |
| proveit.logic.sets.enumeration.proper_subset_of_superset |
11 | instantiation | 19, 72, 20, 21, 22 | ⊢  |
| : , : , :  |
12 | theorem | | ⊢  |
| proveit.logic.sets.enumeration.leftward_permutation |
13 | instantiation | 23 | ⊢  |
| : , :  |
14 | theorem | | ⊢  |
| proveit.logic.sets.enumeration.equal_element_equality |
15 | assumption | | ⊢  |
16 | theorem | | ⊢  |
| proveit.logic.sets.enumeration.reduction_right |
17 | axiom | | ⊢  |
| proveit.numbers.number_sets.natural_numbers.zero_in_nats |
18 | theorem | | ⊢  |
| proveit.core_expr_types.tuples.tuple_len_0_typical_eq |
19 | theorem | | ⊢  |
| proveit.logic.sets.enumeration.nonmembership_fold |
20 | instantiation | 23 | ⊢  |
| : , :  |
21 | instantiation | 25, 24 | ⊢  |
| : , :  |
22 | instantiation | 25, 26 | ⊢  |
| : , :  |
23 | theorem | | ⊢  |
| proveit.numbers.numerals.decimals.tuple_len_2_typical_eq |
24 | instantiation | 28, 71, 29, 27 | ⊢  |
| : , :  |
25 | theorem | | ⊢  |
| proveit.logic.equality.not_equals_symmetry |
26 | instantiation | 28, 72, 29, 30 | ⊢  |
| : , :  |
27 | instantiation | 35, 59, 36, 31, 32, 33*, 34* | ⊢  |
| : , : , :  |
28 | theorem | | ⊢  |
| proveit.numbers.ordering.less_is_not_eq_nat |
29 | theorem | | ⊢  |
| proveit.numbers.numerals.decimals.nat5 |
30 | instantiation | 35, 60, 36, 62, 37, 38*, 39* | ⊢  |
| : , : , :  |
31 | instantiation | 73, 65, 40 | ⊢  |
| : , : , :  |
32 | instantiation | 44, 41 | ⊢  |
| :  |
33 | instantiation | 48, 42, 43 | ⊢  |
| : , : , :  |
34 | theorem | | ⊢  |
| proveit.numbers.numerals.decimals.add_4_1 |
35 | theorem | | ⊢  |
| proveit.numbers.addition.strong_bound_via_left_term_bound |
36 | theorem | | ⊢  |
| proveit.numbers.number_sets.real_numbers.zero_is_real |
37 | instantiation | 44, 45 | ⊢  |
| :  |
38 | instantiation | 48, 46, 47 | ⊢  |
| : , : , :  |
39 | instantiation | 48, 49, 50 | ⊢  |
| : , : , :  |
40 | instantiation | 73, 69, 51 | ⊢  |
| : , : , :  |
41 | theorem | | ⊢  |
| proveit.numbers.numerals.decimals.posnat4 |
42 | instantiation | 53, 52 | ⊢  |
| :  |
43 | instantiation | 55, 52, 54 | ⊢  |
| : , :  |
44 | theorem | | ⊢  |
| proveit.numbers.number_sets.natural_numbers.natural_pos_is_pos |
45 | theorem | | ⊢  |
| proveit.numbers.numerals.decimals.posnat3 |
46 | instantiation | 53, 56 | ⊢  |
| :  |
47 | instantiation | 55, 56, 54 | ⊢  |
| : , :  |
48 | theorem | | ⊢  |
| proveit.logic.equality.sub_right_side_into |
49 | theorem | | ⊢  |
| proveit.numbers.numerals.decimals.add_2_3 |
50 | instantiation | 55, 56, 57 | ⊢  |
| : , :  |
51 | instantiation | 73, 74, 58 | ⊢  |
| : , : , :  |
52 | instantiation | 73, 61, 59 | ⊢  |
| : , : , :  |
53 | theorem | | ⊢  |
| proveit.numbers.addition.elim_zero_right |
54 | theorem | | ⊢  |
| proveit.numbers.number_sets.complex_numbers.zero_is_complex |
55 | theorem | | ⊢  |
| proveit.numbers.addition.commutation |
56 | instantiation | 73, 61, 60 | ⊢  |
| : , : , :  |
57 | instantiation | 73, 61, 62 | ⊢  |
| : , : , :  |
58 | theorem | | ⊢  |
| proveit.numbers.numerals.decimals.nat4 |
59 | instantiation | 73, 65, 63 | ⊢  |
| : , : , :  |
60 | instantiation | 73, 65, 64 | ⊢  |
| : , : , :  |
61 | theorem | | ⊢  |
| proveit.numbers.number_sets.complex_numbers.real_within_complex |
62 | instantiation | 73, 65, 66 | ⊢  |
| : , : , :  |
63 | instantiation | 73, 69, 67 | ⊢  |
| : , : , :  |
64 | instantiation | 73, 69, 68 | ⊢  |
| : , : , :  |
65 | theorem | | ⊢  |
| proveit.numbers.number_sets.real_numbers.rational_within_real |
66 | instantiation | 73, 69, 70 | ⊢  |
| : , : , :  |
67 | instantiation | 73, 74, 71 | ⊢  |
| : , : , :  |
68 | instantiation | 73, 74, 72 | ⊢  |
| : , : , :  |
69 | theorem | | ⊢  |
| proveit.numbers.number_sets.rational_numbers.int_within_rational |
70 | instantiation | 73, 74, 75 | ⊢  |
| : , : , :  |
71 | theorem | | ⊢  |
| proveit.numbers.numerals.decimals.nat1 |
72 | theorem | | ⊢  |
| proveit.numbers.numerals.decimals.nat2 |
73 | theorem | | ⊢  |
| proveit.logic.sets.inclusion.superset_membership_from_proper_subset |
74 | theorem | | ⊢  |
| proveit.numbers.number_sets.integers.nat_within_int |
75 | theorem | | ⊢  |
| proveit.numbers.numerals.decimals.nat3 |
*equality replacement requirements |