| | step type | requirements | statement |
|---|
| 0 | instantiation | 1, 2, 3 |  ⊢  |
| |  :  ,  : |
| 1 | theorem | | ⊢  |
| | proveit.logic.equality.rhs_via_equality |
| 2 | instantiation | 182, 4, 5 | ⊢ |
| |  :  ,  :  ,  :  |
| 3 | instantiation | 128, 6, 7*, 8*, 9* | ⊢  |
| |  :  ,  :  ,  :  |
| 4 | instantiation | 10, 218, 219, 15, 11, 12, 13* | ⊢  |
| |  :  ,  :  ,  :  ,  :  ,  :  |
| 5 | instantiation | 14, 221, 15, 123, 16*, 17*, 18* | ⊢  |
| | : , :  , : , :  , : |
| 6 | modus ponens | 19, 20 | ⊢  |
| 7 | instantiation | 62, 216 |  ⊢  |
| | :  , : |
| 8 | instantiation | 62, 216 | ⊢  |
| | :  , : |
| 9 | instantiation | 21, 22, 23, 24 | ⊢  |
| | :  , :  , :  ,  :  |
| 10 | theorem | | ⊢  |
| | proveit.linear_algebra.addition.vec_sum_split_after |
| 11 | instantiation | 25, 26 | ⊢  |
| | : , :  |
| 12 | instantiation | 27, 28, 29, 181, 30, 31*, 32* | ⊢  |
| | : , : , : |
| 13 | instantiation | 178, 33, 34 | ⊢  |
| | :  , :  ,  : |
| 14 | theorem | | ⊢  |
| | proveit.linear_algebra.addition.vec_sum_index_shift |
| 15 | instantiation | 220, 122, 222 | ⊢  |
| | :  , :  |
| 16 | instantiation | 35, 174, 36 | ⊢  |
| | : , : |
| 17 | instantiation | 178, 37, 38 | ⊢  |
| | :  , :  , : |
| 18 | instantiation | 39, 174 | ⊢  |
| | : |
| 19 | instantiation | 83, 104 | ⊢  |
| | : ,  : ,  : ,  : , :  , : , : |
| 20 | generalization | 40 | ⊢  |
| 21 | theorem | | ⊢  |
| | proveit.logic.equality.four_chain_transitivity |
| 22 | instantiation | 128, 41, 42*, 43* | ⊢  |
| | :  , :  , :  |
| 23 | instantiation | 132, 44 | ⊢  |
| | : , : |
| 24 | instantiation | 128, 45 | ⊢  |
| | :  , :  , :  |
| 25 | theorem | | ⊢  |
| | proveit.numbers.addition.subtraction.nonneg_difference |
| 26 | instantiation | 46, 168 | ⊢  |
| |  : |
| 27 | theorem | | ⊢  |
| | proveit.numbers.addition.strong_bound_via_left_term_bound |
| 28 | instantiation | 231, 209, 47 | ⊢  |
| |  :  ,  :  , : |
| 29 | theorem | | ⊢  |
| | proveit.numbers.number_sets.real_numbers.zero_is_real |
| 30 | instantiation | 48, 168 | ⊢  |
| | : |
| 31 | instantiation | 178, 49, 50 | ⊢  |
| | :  , :  , : |
| 32 | instantiation | 178, 51, 52 | ⊢  |
| | :  , :  , : |
| 33 | instantiation | 68, 192, 228, 233, 193, 69, 174, 127, 145 | ⊢  |
| | : ,  :  , : , :  , :  , :  |
| 34 | instantiation | 53, 145, 174, 54 | ⊢  |
| | : , : , : |
| 35 | theorem | | ⊢  |
| | proveit.numbers.addition.subtraction.add_cancel_basic |
| 36 | instantiation | 72 | ⊢  |
| | : |
| 37 | instantiation | 68, 192, 228, 233, 193, 55, 76, 127, 77 | ⊢  |
| | : , : , : , : , :  , :  |
| 38 | instantiation | 178, 56, 57 | ⊢  |
| | : , :  , : |
| 39 | theorem | | ⊢  |
| | proveit.numbers.negation.double_negation |
| 40 | instantiation | 182, 58, 59 | , ⊢  |
| | :  , :  , :  |
| 41 | modus ponens | 60, 61 | ⊢  |
| 42 | instantiation | 62, 216 | ⊢  |
| | :  , : |
| 43 | instantiation | 62, 216 | ⊢  |
| | :  , : |
| 44 | modus ponens | 63, 64 | ⊢  |
| 45 | instantiation | 132, 65 | ⊢  |
| | : , : |
| 46 | theorem | | ⊢  |
| | proveit.numbers.number_sets.natural_numbers.natural_pos_lower_bound |
| 47 | instantiation | 231, 214, 219 | ⊢  |
| | :  , : , : |
| 48 | theorem | | ⊢  |
| | proveit.numbers.number_sets.natural_numbers.natural_pos_is_pos |
| 49 | instantiation | 68, 233, 228, 192, 69, 193, 66, 174, 127 | ⊢  |
| | : , : , : , :  , : , : |
| 50 | instantiation | 67, 192, 228, 193, 69, 174, 127 | ⊢  |
| | : , : , : , : |
| 51 | instantiation | 68, 233, 228, 192, 69, 193, 174, 127 | ⊢  |
| | : , : , : , :  , : , : |
| 52 | instantiation | 74, 192, 228, 233, 193, 70, 174, 127, 71* | ⊢  |
| | : , : , : , : , :  , :  |
| 53 | theorem | | ⊢  |
| | proveit.numbers.addition.subtraction.add_cancel_triple_32 |
| 54 | instantiation | 72 | ⊢  |
| | : |
| 55 | instantiation | 202 | ⊢  |
| | : , : |
| 56 | instantiation | 73, 233, 192, 193, 76, 127, 77 | ⊢  |
| | : , : , : , :  , : , : , : |
| 57 | instantiation | 74, 192, 228, 233, 193, 75, 76, 77, 127, 78* | ⊢  |
| | : , : , : , : , :  , : |
| 58 | instantiation | 119, 79, 80 | , ⊢  |
| | :  , : , :  |
| 59 | instantiation | 178, 81, 82 | , ⊢  |
| | : , :  , : |
| 60 | instantiation | 83, 104 | ⊢  |
| | : , : , : , : , : , : , : |
| 61 | generalization | 84 | ⊢  |
| 62 | theorem | | ⊢  |
| | proveit.core_expr_types.conditionals.satisfied_condition_reduction |
| 63 | instantiation | 85, 104, 137, 101 | ⊢  |
| |  :  , : , : ,  :  , : ,  :  , :  , : |
| 64 | modus ponens | 86, 87 | ⊢  |
| 65 | modus ponens | 88, 89 | ⊢  |
| 66 | theorem | | ⊢  |
| | proveit.numbers.number_sets.complex_numbers.zero_is_complex |
| 67 | theorem | | ⊢  |
| | proveit.numbers.addition.elim_zero_any |
| 68 | theorem | | ⊢  |
| | proveit.numbers.addition.disassociation |
| 69 | instantiation | 202 | ⊢  |
| | : , : |
| 70 | instantiation | 202 | ⊢  |
| | : , : |
| 71 | instantiation | 132, 90, 146* | ⊢  |
| | :  , :  |
| 72 | axiom | | ⊢  |
| | proveit.logic.equality.equals_reflexivity |
| 73 | theorem | | ⊢  |
| | proveit.numbers.addition.leftward_commutation |
| 74 | theorem | | ⊢  |
| | proveit.numbers.addition.association |
| 75 | instantiation | 202 | ⊢  |
| | : , : |
| 76 | instantiation | 231, 206, 91 | ⊢  |
| | : , : , : |
| 77 | instantiation | 231, 206, 92 | ⊢  |
| | : , : , : |
| 78 | instantiation | 178, 93, 94, 95* | ⊢  |
| | :  , :  , :  |
| 79 | instantiation | 128, 96 | , ⊢  |
| | :  , :  , :  |
| 80 | instantiation | 97, 176, 161, 118 | , ⊢  |
| | :  , :  , :  |
| 81 | instantiation | 132, 98 | , ⊢  |
| | : , : |
| 82 | instantiation | 99, 230, 216 | , ⊢  |
| | :  , : |
| 83 | theorem | | ⊢  |
| | proveit.core_expr_types.lambda_maps.general_lambda_substitution |
| 84 | instantiation | 100, 140, 101 | , ⊢  |
| | : , : |
| 85 | theorem | | ⊢  |
| | proveit.linear_algebra.scalar_multiplication.distribution_over_vec_sum_with_scalar_mult |
| 86 | instantiation | 102, 104, 137 | ⊢  |
| | : , : , :  , : , : , : |
| 87 | generalization | 120 | ⊢  |
| 88 | instantiation | 103, 233, 104, 192, 137, 193 | ⊢  |
| | : , :  , : ,  : , : , : , : , : , :  , : , : |
| 89 | generalization | 105 | ⊢  |
| 90 | instantiation | 125, 192, 228, 233, 193, 106, 145, 174, 112* | ⊢  |
| | : , : , : , : , :  , : |
| 91 | instantiation | 231, 209, 107 | ⊢  |
| | : , : , : |
| 92 | instantiation | 231, 209, 108 | ⊢  |
| | : , : , : |
| 93 | instantiation | 128, 109 | ⊢  |
| | :  , : , :  |
| 94 | instantiation | 132, 110 | ⊢  |
| | : , : |
| 95 | instantiation | 178, 111, 112 | ⊢  |
| | : , :  , : |
| 96 | instantiation | 125, 113, 228, 192, 114, 115, 193, 196, 197, 200, 201, 195, 174 | , ⊢  |
| | :  , : , : , :  , :  , : |
| 97 | theorem | | ⊢  |
| | proveit.numbers.exponentiation.product_of_complex_powers |
| 98 | instantiation | 116, 117 | , ⊢  |
| | :  , :  , :  |
| 99 | theorem | | ⊢  |
| | proveit.physics.quantum.algebra.prepend_num_ket_with_one_ket |
| 100 | theorem | | ⊢  |
| | proveit.numbers.multiplication.commutation |
| 101 | instantiation | 159, 160, 118 | ⊢  |
| | : , : |
| 102 | theorem | | ⊢  |
| | proveit.linear_algebra.addition.summation_closure |
| 103 | theorem | | ⊢  |
| | proveit.linear_algebra.tensors.tensor_prod_distribution_over_summation_with_scalar_mult |
| 104 | theorem | | ⊢  |
| | proveit.numbers.numerals.decimals.posnat1 |
| 105 | instantiation | 119, 120, 121 | , ⊢  |
| | :  , :  , : |
| 106 | instantiation | 202 | ⊢  |
| | : , : |
| 107 | instantiation | 231, 214, 122 | ⊢  |
| | : , : , : |
| 108 | instantiation | 231, 214, 123 | ⊢  |
| | : , : , : |
| 109 | instantiation | 132, 124 | ⊢  |
| | : , : |
| 110 | instantiation | 125, 192, 228, 233, 193, 126, 196, 127, 174 | ⊢  |
| | : , : , : , : , :  , : |
| 111 | instantiation | 128, 129 | ⊢  |
| | :  , :  , : |
| 112 | instantiation | 130, 174 | ⊢  |
| | : |
| 113 | theorem | | ⊢  |
| | proveit.numbers.numerals.decimals.nat4 |
| 114 | instantiation | 131 | ⊢  |
| | : , :  , :  , :  |
| 115 | instantiation | 202 | ⊢  |
| | : , : |
| 116 | theorem | | ⊢  |
| | proveit.physics.quantum.algebra.num_ket_eq |
| 117 | instantiation | 132, 133 | , ⊢  |
| | : , : |
| 118 | instantiation | 182, 134, 135 | ⊢  |
| | :  , :  , : |
| 119 | theorem | | ⊢  |
| | proveit.logic.equality.sub_left_side_into |
| 120 | instantiation | 136, 137, 140, 138 | , ⊢  |
| | : , : , : , : |
| 121 | instantiation | 139, 140, 233, 192, 193, 154, 155, 157, 158 | , ⊢  |
| | : ,  : , : , : ,  :  , :  ,  : , : , : , : |
| 122 | instantiation | 141, 224, 221 | ⊢  |
| | : , : |
| 123 | instantiation | 226, 221 | ⊢  |
| | : |
| 124 | instantiation | 142, 174 | ⊢  |
| | : |
| 125 | theorem | | ⊢  |
| | proveit.numbers.multiplication.distribute_through_sum |
| 126 | instantiation | 202 | ⊢  |
| | : , : |
| 127 | instantiation | 143, 145 | ⊢  |
| | : |
| 128 | axiom | | ⊢  |
| | proveit.logic.equality.substitution |
| 129 | instantiation | 144, 145, 196, 146 | ⊢  |
| | : , : , : |
| 130 | theorem | | ⊢  |
| | proveit.numbers.multiplication.elim_one_left |
| 131 | theorem | | ⊢  |
| | proveit.numbers.numerals.decimals.tuple_len_4_typical_eq |
| 132 | theorem | | ⊢  |
| | proveit.logic.equality.equals_reversal |
| 133 | instantiation | 147, 195, 174 | , ⊢  |
| | : , : |
| 134 | instantiation | 199, 185, 148 | ⊢  |
| | :  , :  |
| 135 | instantiation | 178, 149, 150 | ⊢  |
| | : , :  , : |
| 136 | theorem | | ⊢  |
| | proveit.linear_algebra.scalar_multiplication.scalar_mult_closure |
| 137 | instantiation | 151, 166, 153, 154, 155 | ⊢  |
| | : , : , :  |
| 138 | instantiation | 152, 166, 153, 154, 155, 156, 157, 158 | , ⊢  |
| | : , : , : , :  |
| 139 | theorem | | ⊢  |
| | proveit.linear_algebra.tensors.factor_scalar_from_tensor_prod |
| 140 | instantiation | 159, 160, 161 | , ⊢  |
| | : , : |
| 141 | theorem | | ⊢  |
| | proveit.numbers.multiplication.mult_int_closure_bin |
| 142 | theorem | | ⊢  |
| | proveit.numbers.negation.mult_neg_one_left |
| 143 | theorem | | ⊢  |
| | proveit.numbers.negation.complex_closure |
| 144 | theorem | | ⊢  |
| | proveit.numbers.addition.subtraction.subtract_from_add |
| 145 | instantiation | 231, 206, 162 | ⊢  |
| | : , : , : |
| 146 | theorem | | ⊢  |
| | proveit.numbers.numerals.decimals.add_1_1 |
| 147 | theorem | | ⊢  |
| | proveit.numbers.addition.commutation |
| 148 | instantiation | 182, 163, 164 | ⊢  |
| | : , :  , : |
| 149 | instantiation | 191, 233, 186, 192, 165, 193, 185, 200, 201, 174 | ⊢  |
| | : , :  , : , :  , :  , : |
| 150 | instantiation | 191, 192, 228, 186, 193, 187, 165, 196, 197, 200, 201, 174 | ⊢  |
| | : , : , : , : , :  , : |
| 151 | theorem | | ⊢  |
| | proveit.linear_algebra.tensors.tensor_prod_of_vec_spaces_is_vec_space |
| 152 | theorem | | ⊢  |
| | proveit.linear_algebra.tensors.tensor_prod_is_in_tensor_prod_space |
| 153 | instantiation | 202 | ⊢  |
| | :  , : |
| 154 | instantiation | 167, 166 | ⊢  |
| | : |
| 155 | instantiation | 167, 168 | ⊢  |
| | : |
| 156 | instantiation | 202 | ⊢  |
| | :  , : |
| 157 | theorem | | ⊢  |
| | proveit.physics.quantum.algebra.ket_one_in_qubit_space |
| 158 | instantiation | 169, 230, 216 | , ⊢  |
| | : , : |
| 159 | theorem | | ⊢  |
| | proveit.numbers.exponentiation.exp_complex_closure |
| 160 | instantiation | 231, 206, 170 | ⊢  |
| | : , : , : |
| 161 | instantiation | 182, 171, 172 | , ⊢  |
| | : , :  , : |
| 162 | instantiation | 231, 209, 173 | ⊢  |
| | : , : , : |
| 163 | instantiation | 199, 190, 174 | ⊢  |
| | :  , : |
| 164 | instantiation | 191, 192, 228, 233, 193, 194, 200, 201, 174 | ⊢  |
| | : , : , : , : , :  , : |
| 165 | instantiation | 198 | ⊢  |
| | : , : , : |
| 166 | theorem | | ⊢  |
| | proveit.numbers.numerals.decimals.posnat2 |
| 167 | theorem | | ⊢  |
| | proveit.linear_algebra.complex_vec_set_is_vec_space |
| 168 | instantiation | 175, 228, 225 | ⊢  |
| | : , : |
| 169 | theorem | | ⊢  |
| | proveit.physics.quantum.algebra.num_ket_in_register_space |
| 170 | instantiation | 231, 211, 176 | ⊢  |
| | :  , : , : |
| 171 | instantiation | 199, 185, 177 | , ⊢  |
| | : , :  |
| 172 | instantiation | 178, 179, 180 | , ⊢  |
| | : , :  , : |
| 173 | instantiation | 231, 214, 227 | ⊢  |
| | : , : , : |
| 174 | instantiation | 231, 206, 181 | ⊢  |
| | : , : , : |
| 175 | theorem | | ⊢  |
| | proveit.numbers.exponentiation.exp_natpos_closure |
| 176 | theorem | | ⊢  |
| | proveit.numbers.number_sets.real_numbers.e_is_real_pos |
| 177 | instantiation | 182, 183, 184 | , ⊢  |
| | : , :  , : |
| 178 | axiom | | ⊢  |
| | proveit.logic.equality.equals_transitivity |
| 179 | instantiation | 191, 233, 186, 192, 188, 193, 185, 200, 201, 195 | , ⊢  |
| | : , : , : , : , :  , : |
| 180 | instantiation | 191, 192, 228, 186, 193, 187, 188, 196, 197, 200, 201, 195 | , ⊢  |
| | : , : , : , : , : , : |
| 181 | instantiation | 231, 209, 189 | ⊢  |
| | : , : , : |
| 182 | theorem | | ⊢  |
| | proveit.logic.equality.sub_right_side_into |
| 183 | instantiation | 199, 190, 195 | , ⊢  |
| | : , : |
| 184 | instantiation | 191, 192, 228, 233, 193, 194, 200, 201, 195 | , ⊢  |
| | : , : , : , : , : , : |
| 185 | instantiation | 199, 196, 197 | ⊢  |
| | : , : |
| 186 | theorem | | ⊢  |
| | proveit.numbers.numerals.decimals.nat3 |
| 187 | instantiation | 202 | ⊢  |
| | : , : |
| 188 | instantiation | 198 | ⊢  |
| | : , : , : |
| 189 | instantiation | 231, 214, 221 | ⊢  |
| | : , : , : |
| 190 | instantiation | 199, 200, 201 | ⊢  |
| | : , : |
| 191 | theorem | | ⊢  |
| | proveit.numbers.multiplication.disassociation |
| 192 | axiom | | ⊢  |
| | proveit.numbers.number_sets.natural_numbers.zero_in_nats |
| 193 | theorem | | ⊢  |
| | proveit.core_expr_types.tuples.tuple_len_0_typical_eq |
| 194 | instantiation | 202 | ⊢  |
| | : , : |
| 195 | instantiation | 231, 206, 203 | , ⊢  |
| | : , : , : |
| 196 | instantiation | 231, 206, 204 | ⊢  |
| | : , : , : |
| 197 | instantiation | 231, 206, 205 | ⊢  |
| | : , : , : |
| 198 | theorem | | ⊢  |
| | proveit.numbers.numerals.decimals.tuple_len_3_typical_eq |
| 199 | theorem | | ⊢  |
| | proveit.numbers.multiplication.mult_complex_closure_bin |
| 200 | theorem | | ⊢  |
| | proveit.numbers.number_sets.complex_numbers.i_is_complex |
| 201 | instantiation | 231, 206, 207 | ⊢  |
| | : , : , : |
| 202 | theorem | | ⊢  |
| | proveit.numbers.numerals.decimals.tuple_len_2_typical_eq |
| 203 | instantiation | 231, 209, 208 | , ⊢  |
| | : , : , : |
| 204 | instantiation | 231, 209, 210 | ⊢  |
| | : , : , : |
| 205 | instantiation | 231, 211, 212 | ⊢  |
| | : , : , : |
| 206 | theorem | | ⊢  |
| | proveit.numbers.number_sets.complex_numbers.real_within_complex |
| 207 | theorem | | ⊢  |
| | proveit.physics.quantum.QPE._phase_is_real |
| 208 | instantiation | 231, 214, 213 | , ⊢  |
| | : , : , : |
| 209 | theorem | | ⊢  |
| | proveit.numbers.number_sets.real_numbers.rational_within_real |
| 210 | instantiation | 231, 214, 224 | ⊢  |
| | : , : , : |
| 211 | theorem | | ⊢  |
| | proveit.numbers.number_sets.real_numbers.real_pos_within_real |
| 212 | theorem | | ⊢  |
| | proveit.numbers.number_sets.real_numbers.pi_is_real_pos |
| 213 | instantiation | 231, 215, 216 | , ⊢  |
| | :  , : , : |
| 214 | theorem | | ⊢  |
| | proveit.numbers.number_sets.rational_numbers.int_within_rational |
| 215 | instantiation | 217, 218, 219 | ⊢  |
| | : , : |
| 216 | assumption | | ⊢ |
| 217 | theorem | | ⊢  |
| | proveit.numbers.number_sets.integers.int_interval_within_int |
| 218 | theorem | | ⊢  |
| | proveit.numbers.number_sets.integers.zero_is_int |
| 219 | instantiation | 220, 221, 222 | ⊢  |
| | : , : |
| 220 | theorem | | ⊢  |
| | proveit.numbers.addition.add_int_closure_bin |
| 221 | instantiation | 223, 224, 225 | ⊢  |
| | : , : |
| 222 | instantiation | 226, 227 | ⊢  |
| | : |
| 223 | theorem | | ⊢  |
| | proveit.numbers.exponentiation.exp_int_closure |
| 224 | instantiation | 231, 232, 228 | ⊢  |
| | :  , : , : |
| 225 | instantiation | 231, 229, 230 | ⊢  |
| | :  , : , : |
| 226 | theorem | | ⊢  |
| | proveit.numbers.negation.int_closure |
| 227 | instantiation | 231, 232, 233 | ⊢  |
| | : , : , : |
| 228 | theorem | | ⊢  |
| | proveit.numbers.numerals.decimals.nat2 |
| 229 | theorem | | ⊢  |
| | proveit.numbers.number_sets.natural_numbers.nat_pos_within_nat |
| 230 | assumption | | ⊢ |
| 231 | theorem | | ⊢  |
| | proveit.logic.sets.inclusion.superset_membership_from_proper_subset |
| 232 | theorem | | ⊢  |
| | proveit.numbers.number_sets.integers.nat_within_int |
| 233 | theorem | | ⊢  |
| | proveit.numbers.numerals.decimals.nat1 |
| *equality replacement requirements |
