| | step type | requirements | statement |
|---|
| 0 | instantiation | 1, 2, 3 |  ,  ,  ⊢  |
| |  :  ,  :  ,  :  |
| 1 | reference | 5 | ⊢  |
| 2 | instantiation | 12, 4 | , ⊢  |
| |  :  , :  , :  |
| 3 | instantiation | 5, 6, 7, 8* | , , ⊢  |
| | : , :  , :  |
| 4 | instantiation | 9, 10 | , ⊢  |
| | : , : |
| 5 | axiom | | ⊢ |
| | proveit.logic.equality.equals_transitivity |
| 6 | instantiation | 20, 56, 22, 21, 23, 59, 47, 11 | , , ⊢  |
| |  :  ,  :  ,  :  ,  :  ,  :  ,  :  ,  :  ,  : ,  :  ,  :  |
| 7 | instantiation | 12, 13 | , , ⊢  |
| | :  , :  , :  |
| 8 | instantiation | 14, 15, 16, 50, 17* | , , ⊢  |
| | :  , :  , :  , : , : |
| 9 | theorem | | ⊢  |
| | proveit.logic.equality.equals_reversal |
| 10 | modus ponens | 18, 47 | , ⊢  |
| 11 | instantiation | 19, 59, 56, 48 | , ⊢  |
| | : , : , : , : |
| 12 | axiom | | ⊢  |
| | proveit.logic.equality.substitution |
| 13 | instantiation | 20, 56, 21, 22, 23, 59, 47, 48 | , , ⊢  |
| | : , : , : , : , : , : , : , :  , : , : |
| 14 | theorem | | ⊢  |
| | proveit.linear_algebra.scalar_multiplication.doubly_scaled_as_singly_scaled |
| 15 | instantiation | 24, 31 | ⊢  |
| |  :  |
| 16 | instantiation | 33, 25, 26 | , ⊢  |
| |  :  ,  : , : |
| 17 | instantiation | 27, 50, 28* | ⊢  |
| | : , : |
| 18 | instantiation | 29, 58, 59, 56 | ⊢  |
| | : ,  : ,  :  ,  : , : , : , :  |
| 19 | theorem | | ⊢  |
| | proveit.linear_algebra.scalar_multiplication.scalar_mult_closure |
| 20 | theorem | | ⊢  |
| | proveit.linear_algebra.tensors.factor_scalar_from_tensor_prod |
| 21 | theorem | | ⊢  |
| | proveit.numbers.numerals.decimals.nat1 |
| 22 | axiom | | ⊢  |
| | proveit.numbers.number_sets.natural_numbers.zero_in_nats |
| 23 | theorem | | ⊢  |
| | proveit.core_expr_types.tuples.tuple_len_0_typical_eq |
| 24 | theorem | | ⊢  |
| | proveit.linear_algebra.complex_vec_set_is_vec_space |
| 25 | instantiation | 30, 31, 32 | ⊢  |
| |  : , : , : |
| 26 | instantiation | 33, 34, 35 | , ⊢  |
| | :  , : , : |
| 27 | axiom | | ⊢  |
| | proveit.linear_algebra.scalar_multiplication.scalar_mult_extends_number_mult |
| 28 | instantiation | 36, 50, 58, 37*, 38* | ⊢  |
| | : , : , : |
| 29 | theorem | | ⊢  |
| | proveit.linear_algebra.scalar_multiplication.distribution_over_vec_sum |
| 30 | theorem | | ⊢  |
| | proveit.logic.sets.cartesian_products.cart_exp_subset_eq |
| 31 | theorem | | ⊢  |
| | proveit.numbers.numerals.decimals.posnat9 |
| 32 | instantiation | 39, 55 | ⊢  |
| | : , : |
| 33 | theorem | | ⊢  |
| | proveit.logic.sets.inclusion.unfold_subset_eq |
| 34 | instantiation | 40, 44, 41, 62, 42* | ⊢  |
| | : , :  , :  |
| 35 | instantiation | 43, 44, 45, 59, 46, 47, 48 | , ⊢  |
| | : , : , :  , :  |
| 36 | theorem | | ⊢  |
| | proveit.numbers.exponentiation.product_of_posnat_powers |
| 37 | instantiation | 49, 50 | ⊢  |
| | : |
| 38 | theorem | | ⊢  |
| | proveit.numbers.numerals.decimals.add_1_1 |
| 39 | theorem | | ⊢  |
| | proveit.logic.sets.inclusion.relax_proper_subset |
| 40 | theorem | | ⊢  |
| | proveit.linear_algebra.tensors.tensor_prod_of_cart_exps_within_cart_exp |
| 41 | instantiation | 51 | ⊢  |
| | :  , : |
| 42 | theorem | | ⊢  |
| | proveit.numbers.numerals.decimals.mult_3_3 |
| 43 | theorem | | ⊢  |
| | proveit.linear_algebra.tensors.tensor_prod_is_in_tensor_prod_space |
| 44 | theorem | | ⊢  |
| | proveit.numbers.numerals.decimals.posnat2 |
| 45 | instantiation | 51 | ⊢  |
| | : , : |
| 46 | instantiation | 51 | ⊢  |
| | : , : |
| 47 | modus ponens | 52, 53 | ⊢  |
| 48 | assumption | | ⊢ |
| 49 | theorem | | ⊢  |
| | proveit.numbers.exponentiation.complex_x_to_first_power_is_x |
| 50 | instantiation | 54, 55, 56 | ⊢  |
| | : , : , : |
| 51 | theorem | | ⊢  |
| | proveit.numbers.numerals.decimals.tuple_len_2_typical_eq |
| 52 | instantiation | 57, 58, 59 | ⊢  |
| | : , : , : , : , : , : |
| 53 | generalization | 60 | ⊢  |
| 54 | theorem | | ⊢  |
| | proveit.logic.sets.inclusion.superset_membership_from_proper_subset |
| 55 | theorem | | ⊢  |
| | proveit.numbers.number_sets.complex_numbers.real_within_complex |
| 56 | assumption | | ⊢ |
| 57 | theorem | | ⊢  |
| | proveit.linear_algebra.addition.summation_closure |
| 58 | theorem | | ⊢  |
| | proveit.numbers.numerals.decimals.posnat1 |
| 59 | instantiation | 61, 62 | ⊢  |
| | : |
| 60 | assumption | | ⊢ |
| 61 | theorem | | ⊢  |
| | proveit.linear_algebra.real_vec_set_is_vec_space |
| 62 | theorem | | ⊢  |
| | proveit.numbers.numerals.decimals.posnat3 |
| *equality replacement requirements |
