| step type | requirements | statement |
0 | instantiation | 1, 2, 3 | , , ⊢  |
| : , : , :  |
1 | reference | 58 | ⊢  |
2 | instantiation | 58, 4, 5 | , , ⊢  |
| : , : , :  |
3 | instantiation | 14, 6, 7, 8 | , , ⊢  |
| : , : , : , :  |
4 | instantiation | 28, 19, 107, 93, 20, 10, 26, 31, 32, 9 | , , ⊢  |
| : , : , : , : , : , :  |
5 | instantiation | 28, 107, 83, 19, 10, 11, 20, 26, 31, 32, 25, 34 | , , ⊢  |
| : , : , : , : , : , :  |
6 | instantiation | 12, 19, 107, 93, 20, 13, 26, 31, 32, 25, 34 | , , ⊢  |
| : , : , : , : , : , : , :  |
7 | instantiation | 14, 15, 16, 17 | , , ⊢  |
| : , : , : , :  |
8 | instantiation | 18, 19, 107, 93, 20, 21, 31, 32, 33, 62, 34 | , , ⊢  |
| : , : , : , : , : , : , :  |
9 | instantiation | 22, 25, 34 | ⊢  |
| : , :  |
10 | instantiation | 35 | ⊢  |
| : , : , :  |
11 | instantiation | 39 | ⊢  |
| : , :  |
12 | theorem | | ⊢  |
| proveit.numbers.multiplication.rightward_commutation |
13 | instantiation | 35 | ⊢  |
| : , : , :  |
14 | theorem | | ⊢  |
| proveit.logic.equality.four_chain_transitivity |
15 | instantiation | 23, 83, 93, 29, 24, 31, 32, 25, 26, 34 | , , ⊢  |
| : , : , : , : , : , :  |
16 | instantiation | 80, 27 | ⊢  |
| : , : , :  |
17 | instantiation | 28, 83, 93, 29, 30, 31, 32, 33, 62, 34 | , , ⊢  |
| : , : , : , : , : , :  |
18 | theorem | | ⊢  |
| proveit.numbers.multiplication.leftward_commutation |
19 | axiom | | ⊢  |
| proveit.numbers.number_sets.natural_numbers.zero_in_nats |
20 | theorem | | ⊢  |
| proveit.core_expr_types.tuples.tuple_len_0_typical_eq |
21 | instantiation | 35 | ⊢  |
| : , : , :  |
22 | theorem | | ⊢  |
| proveit.numbers.multiplication.mult_complex_closure_bin |
23 | theorem | | ⊢  |
| proveit.numbers.multiplication.association |
24 | instantiation | 39 | ⊢  |
| : , :  |
25 | instantiation | 40, 91, 41, 42 | ⊢  |
| : , :  |
26 | instantiation | 40, 62, 91, 36 | ⊢  |
| : , :  |
27 | instantiation | 46, 37, 38 | ⊢  |
| : , : , :  |
28 | theorem | | ⊢  |
| proveit.numbers.multiplication.disassociation |
29 | instantiation | 39 | ⊢  |
| : , :  |
30 | instantiation | 39 | ⊢  |
| : , :  |
31 | assumption | | ⊢  |
32 | assumption | | ⊢  |
33 | instantiation | 40, 54, 41, 42 | ⊢  |
| : , :  |
34 | instantiation | 43, 44, 45 | ⊢  |
| : , :  |
35 | theorem | | ⊢  |
| proveit.numbers.numerals.decimals.tuple_len_3_typical_eq |
36 | instantiation | 51, 94 | ⊢  |
| :  |
37 | instantiation | 46, 47, 48 | ⊢  |
| : , : , :  |
38 | instantiation | 80, 49 | ⊢  |
| : , : , :  |
39 | theorem | | ⊢  |
| proveit.numbers.numerals.decimals.tuple_len_2_typical_eq |
40 | theorem | | ⊢  |
| proveit.numbers.division.div_complex_closure |
41 | instantiation | 105, 98, 50 | ⊢  |
| : , : , :  |
42 | instantiation | 51, 95 | ⊢  |
| :  |
43 | theorem | | ⊢  |
| proveit.numbers.exponentiation.exp_complex_closure |
44 | assumption | | ⊢  |
45 | instantiation | 105, 98, 52 | ⊢  |
| : , : , :  |
46 | theorem | | ⊢  |
| proveit.logic.equality.sub_right_side_into |
47 | instantiation | 53, 54, 62, 55, 56, 57 | ⊢  |
| : , : , : , : , :  |
48 | instantiation | 58, 59, 60 | ⊢  |
| : , : , :  |
49 | instantiation | 61, 62 | ⊢  |
| :  |
50 | instantiation | 105, 101, 63 | ⊢  |
| : , : , :  |
51 | theorem | | ⊢  |
| proveit.numbers.number_sets.natural_numbers.nonzero_if_is_nat_pos |
52 | instantiation | 64, 65 | ⊢  |
| :  |
53 | theorem | | ⊢  |
| proveit.numbers.division.mult_frac_cancel_numer_left |
54 | instantiation | 105, 98, 65 | ⊢  |
| : , : , :  |
55 | instantiation | 105, 68, 66 | ⊢  |
| : , : , :  |
56 | instantiation | 105, 68, 67 | ⊢  |
| : , : , :  |
57 | instantiation | 105, 68, 69 | ⊢  |
| : , : , :  |
58 | axiom | | ⊢  |
| proveit.logic.equality.equals_transitivity |
59 | instantiation | 80, 70 | ⊢  |
| : , : , :  |
60 | instantiation | 80, 71 | ⊢  |
| : , : , :  |
61 | theorem | | ⊢  |
| proveit.numbers.division.frac_one_denom |
62 | instantiation | 105, 98, 72 | ⊢  |
| : , : , :  |
63 | instantiation | 105, 103, 73 | ⊢  |
| : , : , :  |
64 | theorem | | ⊢  |
| proveit.numbers.negation.real_closure |
65 | instantiation | 105, 101, 74 | ⊢  |
| : , : , :  |
66 | instantiation | 105, 77, 75 | ⊢  |
| : , : , :  |
67 | instantiation | 105, 77, 76 | ⊢  |
| : , : , :  |
68 | theorem | | ⊢  |
| proveit.numbers.number_sets.complex_numbers.real_nonzero_within_complex_nonzero |
69 | instantiation | 105, 77, 78 | ⊢  |
| : , : , :  |
70 | instantiation | 80, 79 | ⊢  |
| : , : , :  |
71 | instantiation | 80, 81 | ⊢  |
| : , : , :  |
72 | instantiation | 105, 101, 82 | ⊢  |
| : , : , :  |
73 | instantiation | 105, 106, 83 | ⊢  |
| : , : , :  |
74 | instantiation | 105, 103, 84 | ⊢  |
| : , : , :  |
75 | instantiation | 105, 87, 85 | ⊢  |
| : , : , :  |
76 | instantiation | 105, 87, 86 | ⊢  |
| : , : , :  |
77 | theorem | | ⊢  |
| proveit.numbers.number_sets.real_numbers.rational_nonzero_within_real_nonzero |
78 | instantiation | 105, 87, 88 | ⊢  |
| : , : , :  |
79 | instantiation | 89, 91 | ⊢  |
| :  |
80 | axiom | | ⊢  |
| proveit.logic.equality.substitution |
81 | instantiation | 90, 91 | ⊢  |
| :  |
82 | instantiation | 105, 103, 92 | ⊢  |
| : , : , :  |
83 | theorem | | ⊢  |
| proveit.numbers.numerals.decimals.nat2 |
84 | instantiation | 105, 106, 93 | ⊢  |
| : , : , :  |
85 | instantiation | 105, 96, 94 | ⊢  |
| : , : , :  |
86 | instantiation | 105, 96, 95 | ⊢  |
| : , : , :  |
87 | theorem | | ⊢  |
| proveit.numbers.number_sets.rational_numbers.nonzero_int_within_rational_nonzero |
88 | instantiation | 105, 96, 97 | ⊢  |
| : , : , :  |
89 | theorem | | ⊢  |
| proveit.numbers.multiplication.elim_one_left |
90 | theorem | | ⊢  |
| proveit.numbers.multiplication.elim_one_right |
91 | instantiation | 105, 98, 99 | ⊢  |
| : , : , :  |
92 | instantiation | 105, 106, 100 | ⊢  |
| : , : , :  |
93 | theorem | | ⊢  |
| proveit.numbers.numerals.decimals.nat1 |
94 | theorem | | ⊢  |
| proveit.numbers.numerals.decimals.posnat3 |
95 | theorem | | ⊢  |
| proveit.numbers.numerals.decimals.posnat2 |
96 | theorem | | ⊢  |
| proveit.numbers.number_sets.integers.nat_pos_within_nonzero_int |
97 | theorem | | ⊢  |
| proveit.numbers.numerals.decimals.posnat1 |
98 | theorem | | ⊢  |
| proveit.numbers.number_sets.complex_numbers.real_within_complex |
99 | instantiation | 105, 101, 102 | ⊢  |
| : , : , :  |
100 | theorem | | ⊢  |
| proveit.numbers.numerals.decimals.nat4 |
101 | theorem | | ⊢  |
| proveit.numbers.number_sets.real_numbers.rational_within_real |
102 | instantiation | 105, 103, 104 | ⊢  |
| : , : , :  |
103 | theorem | | ⊢  |
| proveit.numbers.number_sets.rational_numbers.int_within_rational |
104 | instantiation | 105, 106, 107 | ⊢  |
| : , : , :  |
105 | theorem | | ⊢  |
| proveit.logic.sets.inclusion.superset_membership_from_proper_subset |
106 | theorem | | ⊢  |
| proveit.numbers.number_sets.integers.nat_within_int |
107 | theorem | | ⊢  |
| proveit.numbers.numerals.decimals.nat3 |