| step type | requirements | statement |
0 | instantiation | 1, 2, 3 | , , , ⊢  |
| : , : , :  |
1 | reference | 23 | ⊢  |
2 | instantiation | 23, 4, 5 | , , , ⊢  |
| : , : , :  |
3 | instantiation | 19, 37, 38, 6, 40, 7, 8, 9, 44, 42, 26, 43 | , , , ⊢  |
| : , : , : , : , : , :  |
4 | instantiation | 10, 11, 12, 13 | , , , ⊢  |
| : , : , : , :  |
5 | instantiation | 30, 14 | , , ⊢  |
| : , : , :  |
6 | theorem | | ⊢  |
| proveit.numbers.numerals.decimals.nat3 |
7 | instantiation | 45 | ⊢  |
| : , :  |
8 | instantiation | 15 | ⊢  |
| : , : , :  |
9 | instantiation | 27, 42, 43 | , ⊢  |
| : , :  |
10 | theorem | | ⊢  |
| proveit.logic.equality.four_chain_transitivity |
11 | instantiation | 16, 37, 38, 40, 21, 20, 26, 43, 22, 42 | , , , ⊢  |
| : , : , : , : , : , :  |
12 | instantiation | 17, 37, 38, 40, 20, 18, 22, 42 | , , , ⊢  |
| : , : , : , : , : , : , :  |
13 | instantiation | 19, 38, 37, 20, 21, 40, 22, 42, 26, 43 | , , , ⊢  |
| : , : , : , : , : , :  |
14 | instantiation | 23, 24, 25 | , , ⊢  |
| : , : , :  |
15 | theorem | | ⊢  |
| proveit.numbers.numerals.decimals.tuple_len_3_typical_eq |
16 | theorem | | ⊢  |
| proveit.numbers.multiplication.association |
17 | theorem | | ⊢  |
| proveit.numbers.multiplication.rightward_commutation |
18 | instantiation | 34, 26, 43 | , ⊢  |
| : , :  |
19 | theorem | | ⊢  |
| proveit.numbers.multiplication.disassociation |
20 | instantiation | 45 | ⊢  |
| : , :  |
21 | instantiation | 45 | ⊢  |
| : , :  |
22 | instantiation | 27, 28, 29 | , , ⊢  |
| : , :  |
23 | axiom | | ⊢  |
| proveit.logic.equality.equals_transitivity |
24 | instantiation | 30, 31 | , ⊢  |
| : , : , :  |
25 | instantiation | 32, 33 | , , ⊢  |
| : , :  |
26 | assumption | | ⊢  |
27 | theorem | | ⊢  |
| proveit.numbers.addition.add_complex_closure_bin |
28 | instantiation | 34, 44, 42 | , ⊢  |
| : , :  |
29 | instantiation | 34, 43, 44 | , ⊢  |
| : , :  |
30 | axiom | | ⊢  |
| proveit.logic.equality.substitution |
31 | instantiation | 35, 44, 42 | , ⊢  |
| : , :  |
32 | theorem | | ⊢  |
| proveit.logic.equality.equals_reversal |
33 | instantiation | 36, 37, 38, 39, 40, 41, 42, 43, 44 | , , ⊢  |
| : , : , : , : , : , :  |
34 | theorem | | ⊢  |
| proveit.numbers.multiplication.mult_complex_closure_bin |
35 | theorem | | ⊢  |
| proveit.numbers.multiplication.commutation |
36 | theorem | | ⊢  |
| proveit.numbers.multiplication.distribute_through_sum |
37 | axiom | | ⊢  |
| proveit.numbers.number_sets.natural_numbers.zero_in_nats |
38 | theorem | | ⊢  |
| proveit.numbers.numerals.decimals.nat2 |
39 | theorem | | ⊢  |
| proveit.numbers.numerals.decimals.nat1 |
40 | theorem | | ⊢  |
| proveit.core_expr_types.tuples.tuple_len_0_typical_eq |
41 | instantiation | 45 | ⊢  |
| : , :  |
42 | assumption | | ⊢  |
43 | assumption | | ⊢  |
44 | assumption | | ⊢  |
45 | theorem | | ⊢  |
| proveit.numbers.numerals.decimals.tuple_len_2_typical_eq |