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