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