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