| step type | requirements | statement |
0 | instantiation | 1, 2, 3 | ⊢  |
| : , : , :  |
1 | reference | 13 | ⊢  |
2 | instantiation | 19, 20, 4, 5, 6, 7 | ⊢  |
| : , : , : , :  |
3 | instantiation | 8, 9, 10, 34, 11*, 12* | ⊢  |
| : , : , :  |
4 | instantiation | 32 | ⊢  |
| : , :  |
5 | instantiation | 32 | ⊢  |
| : , :  |
6 | instantiation | 13, 14, 15 | ⊢  |
| : , : , :  |
7 | theorem | | ⊢  |
| proveit.numbers.numerals.decimals.mult_6_3 |
8 | theorem | | ⊢  |
| proveit.numbers.division.frac_cancel_left |
9 | instantiation | 97, 17, 16 | ⊢  |
| : , : , :  |
10 | instantiation | 97, 17, 18 | ⊢  |
| : , : , :  |
11 | instantiation | 42, 26 | ⊢  |
| :  |
12 | theorem | | ⊢  |
| proveit.numbers.numerals.decimals.mult_9_2 |
13 | axiom | | ⊢  |
| proveit.logic.equality.equals_transitivity |
14 | instantiation | 19, 20, 21, 22, 23, 24 | ⊢  |
| : , : , : , :  |
15 | instantiation | 25, 26, 43, 27, 28 | ⊢  |
| : , : , :  |
16 | instantiation | 97, 30, 29 | ⊢  |
| : , : , :  |
17 | theorem | | ⊢  |
| proveit.numbers.number_sets.complex_numbers.real_nonzero_within_complex_nonzero |
18 | instantiation | 97, 30, 31 | ⊢  |
| : , : , :  |
19 | axiom | | ⊢  |
| proveit.core_expr_types.operations.operands_substitution |
20 | theorem | | ⊢  |
| proveit.numbers.numerals.decimals.nat2 |
21 | instantiation | 32 | ⊢  |
| : , :  |
22 | instantiation | 32 | ⊢  |
| : , :  |
23 | theorem | | ⊢  |
| proveit.numbers.numerals.decimals.mult_5_3 |
24 | instantiation | 33, 43, 34, 35* | ⊢  |
| : , :  |
25 | theorem | | ⊢  |
| proveit.numbers.addition.subtraction.subtract_from_add |
26 | instantiation | 97, 91, 36 | ⊢  |
| : , : , :  |
27 | instantiation | 97, 91, 37 | ⊢  |
| : , : , :  |
28 | theorem | | ⊢  |
| proveit.numbers.numerals.decimals.add_9_6 |
29 | instantiation | 97, 39, 38 | ⊢  |
| : , : , :  |
30 | theorem | | ⊢  |
| proveit.numbers.number_sets.real_numbers.rational_nonzero_within_real_nonzero |
31 | instantiation | 97, 39, 40 | ⊢  |
| : , : , :  |
32 | theorem | | ⊢  |
| proveit.numbers.numerals.decimals.tuple_len_2_typical_eq |
33 | theorem | | ⊢  |
| proveit.numbers.multiplication.mult_neg_right |
34 | instantiation | 97, 91, 41 | ⊢  |
| : , : , :  |
35 | instantiation | 42, 43 | ⊢  |
| :  |
36 | instantiation | 97, 93, 44 | ⊢  |
| : , : , :  |
37 | instantiation | 97, 93, 45 | ⊢  |
| : , : , :  |
38 | instantiation | 97, 46, 73 | ⊢  |
| : , : , :  |
39 | theorem | | ⊢  |
| proveit.numbers.number_sets.rational_numbers.nonzero_int_within_rational_nonzero |
40 | instantiation | 97, 46, 47 | ⊢  |
| : , : , :  |
41 | instantiation | 97, 93, 48 | ⊢  |
| : , : , :  |
42 | theorem | | ⊢  |
| proveit.numbers.multiplication.elim_one_right |
43 | instantiation | 97, 91, 49 | ⊢  |
| : , : , :  |
44 | instantiation | 97, 95, 50 | ⊢  |
| : , : , :  |
45 | instantiation | 97, 95, 51 | ⊢  |
| : , : , :  |
46 | theorem | | ⊢  |
| proveit.numbers.number_sets.integers.nat_pos_within_nonzero_int |
47 | theorem | | ⊢  |
| proveit.numbers.numerals.decimals.posnat2 |
48 | instantiation | 97, 95, 52 | ⊢  |
| : , : , :  |
49 | instantiation | 97, 93, 53 | ⊢  |
| : , : , :  |
50 | instantiation | 97, 98, 54 | ⊢  |
| : , : , :  |
51 | instantiation | 97, 55, 56 | ⊢  |
| : , : , :  |
52 | instantiation | 97, 98, 71 | ⊢  |
| : , : , :  |
53 | instantiation | 97, 95, 57 | ⊢  |
| : , : , :  |
54 | theorem | | ⊢  |
| proveit.numbers.numerals.decimals.nat9 |
55 | theorem | | ⊢  |
| proveit.numbers.number_sets.integers.nat_pos_within_int |
56 | instantiation | 58, 71, 59, 60, 61 | ⊢  |
| : , : , :  |
57 | instantiation | 97, 98, 62 | ⊢  |
| : , : , :  |
58 | theorem | | ⊢  |
| proveit.numbers.numerals.decimals.deci_sequence_is_nat_pos |
59 | instantiation | 64, 71, 63 | ⊢  |
| :  |
60 | instantiation | 64, 99, 65 | ⊢  |
| :  |
61 | theorem | | ⊢  |
| proveit.numbers.numerals.decimals.less_0_1 |
62 | theorem | | ⊢  |
| proveit.numbers.numerals.decimals.nat6 |
63 | instantiation | 68, 66, 67 | ⊢  |
| : , :  |
64 | theorem | | ⊢  |
| proveit.numbers.numerals.decimals.n_in_digits |
65 | instantiation | 68, 69, 70 | ⊢  |
| : , :  |
66 | instantiation | 81, 71 | ⊢  |
| :  |
67 | instantiation | 72, 73 | ⊢  |
| :  |
68 | theorem | | ⊢  |
| proveit.logic.booleans.conjunction.and_if_both |
69 | instantiation | 81, 99 | ⊢  |
| :  |
70 | instantiation | 74, 92, 75, 76, 77, 78*, 79* | ⊢  |
| : , : , :  |
71 | theorem | | ⊢  |
| proveit.numbers.numerals.decimals.nat1 |
72 | theorem | | ⊢  |
| proveit.numbers.number_sets.natural_numbers.natural_pos_lower_bound |
73 | theorem | | ⊢  |
| proveit.numbers.numerals.decimals.posnat9 |
74 | theorem | | ⊢  |
| proveit.numbers.addition.weak_bound_via_left_term_bound |
75 | theorem | | ⊢  |
| proveit.numbers.number_sets.real_numbers.zero_is_real |
76 | instantiation | 97, 93, 80 | ⊢  |
| : , : , :  |
77 | instantiation | 81, 90 | ⊢  |
| :  |
78 | instantiation | 82, 83, 84 | ⊢  |
| : , : , :  |
79 | theorem | | ⊢  |
| proveit.numbers.numerals.decimals.add_4_5 |
80 | instantiation | 97, 95, 85 | ⊢  |
| : , : , :  |
81 | theorem | | ⊢  |
| proveit.numbers.number_sets.natural_numbers.natural_lower_bound |
82 | theorem | | ⊢  |
| proveit.logic.equality.sub_right_side_into |
83 | instantiation | 86, 88 | ⊢  |
| :  |
84 | instantiation | 87, 88, 89 | ⊢  |
| : , :  |
85 | instantiation | 97, 98, 90 | ⊢  |
| : , : , :  |
86 | theorem | | ⊢  |
| proveit.numbers.addition.elim_zero_right |
87 | theorem | | ⊢  |
| proveit.numbers.addition.commutation |
88 | instantiation | 97, 91, 92 | ⊢  |
| : , : , :  |
89 | theorem | | ⊢  |
| proveit.numbers.number_sets.complex_numbers.zero_is_complex |
90 | theorem | | ⊢  |
| proveit.numbers.numerals.decimals.nat4 |
91 | theorem | | ⊢  |
| proveit.numbers.number_sets.complex_numbers.real_within_complex |
92 | instantiation | 97, 93, 94 | ⊢  |
| : , : , :  |
93 | theorem | | ⊢  |
| proveit.numbers.number_sets.real_numbers.rational_within_real |
94 | instantiation | 97, 95, 96 | ⊢  |
| : , : , :  |
95 | theorem | | ⊢  |
| proveit.numbers.number_sets.rational_numbers.int_within_rational |
96 | instantiation | 97, 98, 99 | ⊢  |
| : , : , :  |
97 | theorem | | ⊢  |
| proveit.logic.sets.inclusion.superset_membership_from_proper_subset |
98 | theorem | | ⊢  |
| proveit.numbers.number_sets.integers.nat_within_int |
99 | theorem | | ⊢  |
| proveit.numbers.numerals.decimals.nat5 |
*equality replacement requirements |