| step type | requirements | statement |
0 | generalization | 1 | ⊢  |
1 | instantiation | 410, 2, 5 | ⊢  |
| : , : , :  |
2 | instantiation | 361, 3, 4, 5 | ⊢  |
| : , : , : , :  |
3 | instantiation | 335, 6, 7 | ⊢  |
| : , : , :  |
4 | instantiation | 335, 8, 9 | ⊢  |
| : , : , :  |
5 | instantiation | 376, 10 | ⊢  |
| : , : , :  |
6 | instantiation | 11, 426 | ⊢  |
| :  |
7 | instantiation | 12, 45, 13, 224, 222*, 14* | ⊢  |
| : , : , : , : , : , : , : , :  |
8 | instantiation | 335, 15, 16 | ⊢  |
| : , : , :  |
9 | modus ponens | 17, 18 | ⊢  |
10 | instantiation | 376, 19 | ⊢  |
| : , : , :  |
11 | axiom | | ⊢  |
| proveit.physics.quantum.QPE._fail_def |
12 | conjecture | | ⊢  |
| proveit.statistics.prob_of_all_events_transformation |
13 | instantiation | 88, 20 | ⊢  |
| : , :  |
14 | instantiation | 21, 347, 444, 349, 22, 79, 23, 24* | ⊢  |
| : , : , : , : , : , :  |
15 | instantiation | 335, 25, 26 | ⊢  |
| : , : , :  |
16 | instantiation | 44, 45, 27, 28*, 43*, 29* | ⊢  |
| : , : , : , : , :  |
17 | instantiation | 53, 389 | ⊢  |
| : , : , : , : , : , :  |
18 | generalization | 30 | ⊢  |
19 | modus ponens | 31, 32 | ⊢  |
20 | instantiation | 118, 225 | ⊢  |
| : , : , :  |
21 | conjecture | | ⊢  |
| proveit.numbers.modular.redundant_mod_elimination_in_sum_in_modabs |
22 | instantiation | 450, 437, 33 | ⊢  |
| : , : , :  |
23 | instantiation | 450, 34, 35 | ⊢  |
| : , : , :  |
24 | instantiation | 329, 36, 37 | ⊢  |
| : , : , :  |
25 | instantiation | 38, 45, 39, 40, 41, 71, 42*, 48*, 43* | ⊢  |
| : , : , : , : , : , : , : , :  |
26 | instantiation | 44, 45, 46, 47*, 48*, 49* | ⊢  |
| : , : , : , : , :  |
27 | instantiation | 69, 64, 71 | ⊢  |
| : , : , : , :  |
28 | instantiation | 72, 50 | , ⊢  |
| :  |
29 | instantiation | 74, 444, 347, 349 | ⊢  |
| : , : , : , : , :  |
30 | instantiation | 51, 52 | ⊢  |
| : , : , :  |
31 | instantiation | 53, 389 | ⊢  |
| : , : , : , : , : , :  |
32 | generalization | 54 | ⊢  |
33 | instantiation | 450, 445, 55 | ⊢  |
| : , : , :  |
34 | conjecture | | ⊢  |
| proveit.numbers.number_sets.real_numbers.rational_pos_within_real_pos |
35 | instantiation | 450, 56, 252 | ⊢  |
| : , : , :  |
36 | instantiation | 346, 347, 452, 444, 349, 57, 59, 60, 58 | ⊢  |
| : , : , : , : , : , :  |
37 | instantiation | 180, 59, 60, 61 | ⊢  |
| : , : , :  |
38 | conjecture | | ⊢  |
| proveit.statistics.prob_of_disjoint_events_is_prob_sum |
39 | instantiation | 62, 428, 63, 70, 64 | ⊢  |
| : , : , :  |
40 | instantiation | 350 | ⊢  |
| :  |
41 | instantiation | 65, 338, 339, 355, 442, 66 | ⊢  |
| : , : , : , :  |
42 | instantiation | 67, 68 | , ⊢  |
| :  |
43 | instantiation | 74, 444, 347, 349 | ⊢  |
| : , : , : , : , :  |
44 | conjecture | | ⊢  |
| proveit.statistics.prob_of_all_as_sum |
45 | conjecture | | ⊢  |
| proveit.physics.quantum.QPE._Omega_is_sample_space |
46 | instantiation | 69, 70, 71 | ⊢  |
| : , : , : , :  |
47 | instantiation | 72, 73 | , ⊢  |
| :  |
48 | instantiation | 74, 444, 347, 349 | ⊢  |
| : , : , : , : , :  |
49 | instantiation | 74, 444, 347, 349 | ⊢  |
| : , : , : , : , :  |
50 | instantiation | 90, 300, 75 | , ⊢  |
| : , :  |
51 | axiom | | ⊢  |
| proveit.core_expr_types.conditionals.condition_replacement |
52 | instantiation | 76, 426 | ⊢  |
| :  |
53 | axiom | | ⊢  |
| proveit.core_expr_types.lambda_maps.lambda_substitution |
54 | instantiation | 77, 78 | ⊢  |
| : , : , :  |
55 | instantiation | 441, 300, 301 | ⊢  |
| : , :  |
56 | conjecture | | ⊢  |
| proveit.numbers.number_sets.rational_numbers.nat_pos_within_rational_pos |
57 | instantiation | 370 | ⊢  |
| : , :  |
58 | instantiation | 450, 430, 79 | ⊢  |
| : , : , :  |
59 | instantiation | 450, 430, 94 | ⊢  |
| : , : , :  |
60 | instantiation | 450, 430, 80 | ⊢  |
| : , : , :  |
61 | instantiation | 350 | ⊢  |
| :  |
62 | conjecture | | ⊢  |
| proveit.logic.sets.unification.union_inclusion |
63 | instantiation | 370 | ⊢  |
| : , :  |
64 | instantiation | 86, 338, 355, 442, 81 | ⊢  |
| : , : , : , :  |
65 | conjecture | | ⊢  |
| proveit.numbers.number_sets.integers.disjoint_intervals |
66 | instantiation | 113, 366, 82, 116, 83, 98 | ⊢  |
| : , :  |
67 | axiom | | ⊢  |
| proveit.logic.booleans.eq_true_intro |
68 | instantiation | 410, 84, 85 | , ⊢  |
| : , : , :  |
69 | conjecture | | ⊢  |
| proveit.logic.sets.functions.injections.subset_injection |
70 | instantiation | 86, 338, 339, 442, 87 | ⊢  |
| : , : , : , :  |
71 | instantiation | 88, 89 | ⊢  |
| : , :  |
72 | conjecture | | ⊢  |
| proveit.physics.quantum.QPE._outcome_prob |
73 | instantiation | 90, 300, 304 | , ⊢  |
| : , :  |
74 | conjecture | | ⊢  |
| proveit.core_expr_types.conditionals.true_condition_elimination |
75 | instantiation | 450, 91, 92 | , ⊢  |
| : , : , :  |
76 | conjecture | | ⊢  |
| proveit.physics.quantum.QPE._fail_sum_prob_conds_equiv_lemma |
77 | conjecture | | ⊢  |
| proveit.core_expr_types.conditionals.condition_substitution |
78 | instantiation | 376, 93 | ⊢  |
| : , : , :  |
79 | instantiation | 178, 94 | ⊢  |
| :  |
80 | instantiation | 450, 437, 95 | ⊢  |
| : , : , :  |
81 | instantiation | 113, 366, 96, 97, 98, 99 | ⊢  |
| : , :  |
82 | instantiation | 378 | ⊢  |
| : , : , :  |
83 | instantiation | 104, 327, 129, 100, 101, 102*, 103* | ⊢  |
| : , : , :  |
84 | instantiation | 104, 105, 268, 106, 107, 108*, 109* | , ⊢  |
| : , : , :  |
85 | instantiation | 110, 111, 112* | , ⊢  |
| :  |
86 | conjecture | | ⊢  |
| proveit.numbers.number_sets.integers.interval_subset_eq |
87 | instantiation | 113, 366, 114, 115, 116, 117 | ⊢  |
| : , :  |
88 | theorem | | ⊢  |
| proveit.logic.booleans.conjunction.left_from_and |
89 | instantiation | 118, 119 | ⊢  |
| : , : , :  |
90 | conjecture | | ⊢  |
| proveit.physics.quantum.QPE._mod_add_closure |
91 | instantiation | 434, 355, 442 | ⊢  |
| : , :  |
92 | assumption | | ⊢  |
93 | instantiation | 376, 239 | ⊢  |
| : , : , :  |
94 | instantiation | 450, 437, 120 | ⊢  |
| : , : , :  |
95 | instantiation | 450, 445, 301 | ⊢  |
| : , : , :  |
96 | instantiation | 378 | ⊢  |
| : , : , :  |
97 | instantiation | 121, 122, 123 | ⊢  |
| : , : , :  |
98 | instantiation | 156, 420, 342, 124, 125, 126* | ⊢  |
| : , : , :  |
99 | instantiation | 147, 157, 127 | ⊢  |
| : , :  |
100 | instantiation | 162, 235, 431 | ⊢  |
| : , :  |
101 | instantiation | 128, 129, 235, 431, 130, 131 | ⊢  |
| : , : , :  |
102 | instantiation | 374, 132 | ⊢  |
| : , :  |
103 | instantiation | 361, 133, 134, 135 | ⊢  |
| : , : , : , :  |
104 | conjecture | | ⊢  |
| proveit.numbers.addition.strong_bound_via_left_term_bound |
105 | instantiation | 162, 342, 136 | , ⊢  |
| : , :  |
106 | instantiation | 162, 138, 420 | ⊢  |
| : , :  |
107 | instantiation | 137, 268, 138, 420, 270, 357 | , ⊢  |
| : , : , :  |
108 | instantiation | 329, 139, 140 | , ⊢  |
| : , : , :  |
109 | instantiation | 329, 141, 142 | , ⊢  |
| : , : , :  |
110 | conjecture | | ⊢  |
| proveit.physics.quantum.QPE._modabs_in_full_domain_simp |
111 | instantiation | 143, 338, 442, 304, 144 | , ⊢  |
| : , : , :  |
112 | instantiation | 145, 146 | , ⊢  |
| :  |
113 | conjecture | | ⊢  |
| proveit.logic.booleans.conjunction.and_if_all |
114 | instantiation | 378 | ⊢  |
| : , : , :  |
115 | instantiation | 147, 148, 149 | ⊢  |
| : , :  |
116 | instantiation | 156, 150, 342, 164, 165, 151*, 152* | ⊢  |
| : , : , :  |
117 | instantiation | 214, 153 | ⊢  |
| : , :  |
118 | conjecture | | ⊢  |
| proveit.logic.sets.functions.bijections.membership_unfolding |
119 | instantiation | 154, 155 | ⊢  |
| : , : , :  |
120 | instantiation | 450, 445, 300 | ⊢  |
| : , : , :  |
121 | conjecture | | ⊢  |
| proveit.numbers.ordering.transitivity_less_eq_less_eq |
122 | instantiation | 156, 226, 420, 157, 158, 159*, 160* | ⊢  |
| : , : , :  |
123 | instantiation | 214, 161 | ⊢  |
| : , :  |
124 | instantiation | 162, 164, 420 | ⊢  |
| : , :  |
125 | instantiation | 163, 342, 164, 420, 165, 166 | ⊢  |
| : , : , :  |
126 | instantiation | 361, 167, 334, 168 | ⊢  |
| : , : , : , :  |
127 | instantiation | 350 | ⊢  |
| :  |
128 | conjecture | | ⊢  |
| proveit.numbers.ordering.less_add_right |
129 | instantiation | 260, 431, 170 | ⊢  |
| : , :  |
130 | instantiation | 169, 431, 170, 342, 341, 171 | ⊢  |
| : , : , :  |
131 | instantiation | 201, 452 | ⊢  |
| :  |
132 | instantiation | 361, 239, 172, 173 | ⊢  |
| : , : , : , :  |
133 | instantiation | 346, 347, 452, 444, 349, 174, 207, 423, 309 | ⊢  |
| : , : , : , : , : , :  |
134 | instantiation | 346, 452, 347, 174, 323, 349, 207, 423, 369, 385 | ⊢  |
| : , : , : , : , : , :  |
135 | instantiation | 361, 175, 176, 177 | ⊢  |
| : , : , : , :  |
136 | instantiation | 178, 268 | , ⊢  |
| :  |
137 | conjecture | | ⊢  |
| proveit.numbers.ordering.less_eq_add_right_strong |
138 | instantiation | 450, 437, 179 | ⊢  |
| : , : , :  |
139 | instantiation | 346, 444, 452, 347, 211, 349, 242, 325, 213 | , ⊢  |
| : , : , : , : , : , :  |
140 | instantiation | 180, 242, 325, 181 | , ⊢  |
| : , : , :  |
141 | instantiation | 376, 182 | ⊢  |
| : , : , :  |
142 | instantiation | 329, 183, 184 | , ⊢  |
| : , : , :  |
143 | conjecture | | ⊢  |
| proveit.numbers.number_sets.integers.in_interval |
144 | instantiation | 223, 185, 186 | , ⊢  |
| : , :  |
145 | conjecture | | ⊢  |
| proveit.numbers.absolute_value.abs_neg_elim |
146 | instantiation | 214, 244 | , ⊢  |
| : , :  |
147 | conjecture | | ⊢  |
| proveit.numbers.ordering.relax_equal_to_less_eq |
148 | instantiation | 450, 437, 187 | ⊢  |
| : , : , :  |
149 | instantiation | 350 | ⊢  |
| :  |
150 | instantiation | 188, 366, 189, 226, 420, 381 | ⊢  |
| : , :  |
151 | instantiation | 361, 190, 191, 192 | ⊢  |
| : , : , : , :  |
152 | instantiation | 374, 193 | ⊢  |
| : , :  |
153 | instantiation | 243, 271, 245 | ⊢  |
| : , : , :  |
154 | conjecture | | ⊢  |
| proveit.logic.sets.functions.bijections.elim_domain_condition |
155 | modus ponens | 194, 195 | ⊢  |
156 | conjecture | | ⊢  |
| proveit.numbers.addition.weak_bound_via_left_term_bound |
157 | instantiation | 403, 404, 447 | ⊢  |
| : , : , :  |
158 | instantiation | 196, 447 | ⊢  |
| :  |
159 | instantiation | 383, 409, 197 | ⊢  |
| : , :  |
160 | instantiation | 329, 198, 199 | ⊢  |
| : , : , :  |
161 | instantiation | 272, 306 | ⊢  |
| :  |
162 | conjecture | | ⊢  |
| proveit.numbers.addition.add_real_closure_bin |
163 | conjecture | | ⊢  |
| proveit.numbers.ordering.less_eq_add_right |
164 | instantiation | 450, 437, 200 | ⊢  |
| : , : , :  |
165 | instantiation | 290, 436, 435, 426 | ⊢  |
| : , : , :  |
166 | instantiation | 201, 444 | ⊢  |
| :  |
167 | instantiation | 329, 202, 203 | ⊢  |
| : , : , :  |
168 | instantiation | 374, 344 | ⊢  |
| : , :  |
169 | conjecture | | ⊢  |
| proveit.numbers.multiplication.strong_bound_via_right_factor_bound |
170 | conjecture | | ⊢  |
| proveit.numbers.number_sets.real_numbers.zero_is_real |
171 | instantiation | 272, 428 | ⊢  |
| :  |
172 | instantiation | 350 | ⊢  |
| :  |
173 | instantiation | 374, 204 | ⊢  |
| : , :  |
174 | instantiation | 370 | ⊢  |
| : , :  |
175 | instantiation | 205, 444, 207, 423, 369, 385 | ⊢  |
| : , : , : , : , : , : , :  |
176 | instantiation | 314, 347, 452, 349, 206, 286, 207, 369, 423, 385, 208* | ⊢  |
| : , : , : , : , : , :  |
177 | instantiation | 314, 444, 452, 347, 286, 349, 325, 423, 385, 287* | ⊢  |
| : , : , : , : , : , :  |
178 | conjecture | | ⊢  |
| proveit.numbers.negation.real_closure |
179 | instantiation | 450, 445, 339 | ⊢  |
| : , : , :  |
180 | conjecture | | ⊢  |
| proveit.numbers.addition.subtraction.add_cancel_triple_13 |
181 | instantiation | 350 | ⊢  |
| :  |
182 | instantiation | 329, 209, 210 | ⊢  |
| : , : , :  |
183 | instantiation | 346, 444, 452, 347, 211, 349, 369, 325, 213 | , ⊢  |
| : , : , : , : , : , :  |
184 | instantiation | 212, 325, 213, 326 | , ⊢  |
| : , : , :  |
185 | instantiation | 372, 338, 339, 320 | , ⊢  |
| : , : , :  |
186 | instantiation | 214, 215 | , ⊢  |
| : , :  |
187 | instantiation | 450, 445, 338 | ⊢  |
| : , : , :  |
188 | conjecture | | ⊢  |
| proveit.numbers.addition.add_real_closure |
189 | instantiation | 378 | ⊢  |
| : , : , :  |
190 | instantiation | 329, 216, 217 | ⊢  |
| : , : , :  |
191 | instantiation | 350 | ⊢  |
| :  |
192 | instantiation | 374, 218 | ⊢  |
| : , :  |
193 | instantiation | 361, 239, 219, 220 | ⊢  |
| : , : , : , :  |
194 | instantiation | 221, 222* | ⊢  |
| : , : , : , : , : , :  |
195 | instantiation | 223, 224, 225 | ⊢  |
| : , :  |
196 | conjecture | | ⊢  |
| proveit.numbers.number_sets.natural_numbers.natural_pos_lower_bound |
197 | instantiation | 450, 430, 226 | ⊢  |
| : , : , :  |
198 | instantiation | 329, 227, 228 | ⊢  |
| : , : , :  |
199 | instantiation | 229, 380, 334 | ⊢  |
| : , :  |
200 | instantiation | 450, 445, 435 | ⊢  |
| : , : , :  |
201 | conjecture | | ⊢  |
| proveit.numbers.number_sets.natural_numbers.natural_lower_bound |
202 | instantiation | 376, 230 | ⊢  |
| : , : , :  |
203 | instantiation | 329, 231, 232 | ⊢  |
| : , : , :  |
204 | instantiation | 329, 233, 234 | ⊢  |
| : , : , :  |
205 | conjecture | | ⊢  |
| proveit.numbers.addition.leftward_commutation |
206 | instantiation | 370 | ⊢  |
| : , :  |
207 | instantiation | 450, 430, 235 | ⊢  |
| : , : , :  |
208 | instantiation | 329, 236, 237, 238* | ⊢  |
| : , : , :  |
209 | instantiation | 376, 239 | ⊢  |
| : , : , :  |
210 | instantiation | 329, 240, 241 | ⊢  |
| : , : , :  |
211 | instantiation | 370 | ⊢  |
| : , :  |
212 | conjecture | | ⊢  |
| proveit.numbers.addition.subtraction.add_cancel_triple_21 |
213 | instantiation | 379, 242 | , ⊢  |
| :  |
214 | conjecture | | ⊢  |
| proveit.numbers.ordering.relax_less |
215 | instantiation | 243, 244, 245 | , ⊢  |
| : , : , :  |
216 | instantiation | 376, 311 | ⊢  |
| : , : , :  |
217 | instantiation | 329, 246, 247 | ⊢  |
| : , : , :  |
218 | instantiation | 376, 328 | ⊢  |
| : , : , :  |
219 | instantiation | 374, 248 | ⊢  |
| : , :  |
220 | instantiation | 374, 249 | ⊢  |
| : , :  |
221 | conjecture | | ⊢  |
| proveit.logic.sets.functions.bijections.bijection_transitivity |
222 | instantiation | 376, 250 | ⊢  |
| : , : , :  |
223 | theorem | | ⊢  |
| proveit.logic.booleans.conjunction.and_if_both |
224 | instantiation | 251, 252, 338, 442, 300 | ⊢  |
| : , : , : , : , :  |
225 | conjecture | | ⊢  |
| proveit.physics.quantum.QPE._sample_space_bijection |
226 | instantiation | 450, 437, 253 | ⊢  |
| : , : , :  |
227 | instantiation | 376, 344 | ⊢  |
| : , : , :  |
228 | instantiation | 376, 328 | ⊢  |
| : , : , :  |
229 | conjecture | | ⊢  |
| proveit.numbers.addition.subtraction.add_cancel_basic |
230 | instantiation | 329, 254, 255 | ⊢  |
| : , : , :  |
231 | instantiation | 346, 347, 452, 444, 349, 256, 380, 385, 409 | ⊢  |
| : , : , : , : , : , :  |
232 | instantiation | 266, 409, 380, 267 | ⊢  |
| : , : , :  |
233 | instantiation | 376, 257 | ⊢  |
| : , : , :  |
234 | instantiation | 329, 258, 259 | ⊢  |
| : , : , :  |
235 | instantiation | 260, 431, 342 | ⊢  |
| : , :  |
236 | instantiation | 376, 261 | ⊢  |
| : , : , :  |
237 | instantiation | 374, 262 | ⊢  |
| : , :  |
238 | instantiation | 329, 263, 264 | ⊢  |
| : , : , :  |
239 | instantiation | 265, 325, 409 | ⊢  |
| : , :  |
240 | instantiation | 346, 347, 452, 444, 349, 323, 369, 385, 409 | ⊢  |
| : , : , : , : , : , :  |
241 | instantiation | 266, 409, 369, 267 | ⊢  |
| : , : , :  |
242 | instantiation | 450, 430, 268 | , ⊢  |
| : , : , :  |
243 | axiom | | ⊢  |
| proveit.numbers.ordering.transitivity_less_less |
244 | instantiation | 269, 270, 271 | , ⊢  |
| : , : , :  |
245 | instantiation | 272, 447 | ⊢  |
| :  |
246 | instantiation | 346, 444, 366, 347, 367, 349, 325, 368, 409, 369 | ⊢  |
| : , : , : , : , : , :  |
247 | instantiation | 332, 347, 452, 349, 273, 325, 368, 409, 326 | ⊢  |
| : , : , : , : , : , : , : , :  |
248 | instantiation | 303, 309, 325, 385, 274 | ⊢  |
| : , : , :  |
249 | instantiation | 329, 275, 276 | ⊢  |
| : , : , :  |
250 | instantiation | 374, 277 | ⊢  |
| : , :  |
251 | conjecture | | ⊢  |
| proveit.numbers.modular.interval_left_shift_bijection |
252 | instantiation | 278, 452, 433 | ⊢  |
| : , :  |
253 | instantiation | 450, 445, 354 | ⊢  |
| : , : , :  |
254 | instantiation | 376, 310 | ⊢  |
| : , : , :  |
255 | instantiation | 329, 279, 280 | ⊢  |
| : , : , :  |
256 | instantiation | 370 | ⊢  |
| : , :  |
257 | instantiation | 281, 423 | ⊢  |
| :  |
258 | instantiation | 346, 444, 452, 347, 323, 349, 282, 369, 385 | ⊢  |
| : , : , : , : , : , :  |
259 | instantiation | 283, 347, 452, 349, 323, 369, 385 | ⊢  |
| : , : , : , :  |
260 | conjecture | | ⊢  |
| proveit.numbers.multiplication.mult_real_closure_bin |
261 | instantiation | 374, 284 | ⊢  |
| : , :  |
262 | instantiation | 285, 347, 452, 444, 349, 286, 423, 385, 325 | ⊢  |
| : , : , : , : , : , :  |
263 | instantiation | 376, 287 | ⊢  |
| : , : , :  |
264 | instantiation | 288, 325 | ⊢  |
| :  |
265 | conjecture | | ⊢  |
| proveit.numbers.negation.distribute_neg_through_binary_sum |
266 | conjecture | | ⊢  |
| proveit.numbers.addition.subtraction.add_cancel_triple_32 |
267 | instantiation | 350 | ⊢  |
| :  |
268 | instantiation | 450, 437, 289 | , ⊢  |
| : , : , :  |
269 | conjecture | | ⊢  |
| proveit.numbers.ordering.transitivity_less_eq_less |
270 | instantiation | 290, 338, 339, 320 | , ⊢  |
| : , : , :  |
271 | instantiation | 291, 292 | ⊢  |
| :  |
272 | conjecture | | ⊢  |
| proveit.numbers.number_sets.natural_numbers.natural_pos_is_pos |
273 | instantiation | 370 | ⊢  |
| : , :  |
274 | instantiation | 335, 293, 294 | ⊢  |
| : , : , :  |
275 | instantiation | 329, 295, 296 | ⊢  |
| : , : , :  |
276 | instantiation | 329, 297, 298 | ⊢  |
| : , : , :  |
277 | instantiation | 299, 300, 301 | ⊢  |
| : , :  |
278 | conjecture | | ⊢  |
| proveit.numbers.exponentiation.exp_natpos_closure |
279 | instantiation | 346, 347, 452, 444, 349, 348, 380, 353, 409 | ⊢  |
| : , : , : , : , : , :  |
280 | instantiation | 314, 444, 452, 347, 315, 349, 380, 353, 409, 316* | ⊢  |
| : , : , : , : , : , :  |
281 | conjecture | | ⊢  |
| proveit.numbers.multiplication.mult_zero_right |
282 | conjecture | | ⊢  |
| proveit.numbers.number_sets.complex_numbers.zero_is_complex |
283 | conjecture | | ⊢  |
| proveit.numbers.addition.elim_zero_any |
284 | instantiation | 302, 325 | ⊢  |
| :  |
285 | conjecture | | ⊢  |
| proveit.numbers.multiplication.distribute_through_sum |
286 | instantiation | 370 | ⊢  |
| : , :  |
287 | instantiation | 303, 409, 423, 352 | ⊢  |
| : , : , :  |
288 | conjecture | | ⊢  |
| proveit.numbers.multiplication.elim_one_left |
289 | instantiation | 450, 445, 304 | , ⊢  |
| : , : , :  |
290 | conjecture | | ⊢  |
| proveit.numbers.number_sets.integers.interval_upper_bound |
291 | conjecture | | ⊢  |
| proveit.numbers.number_sets.integers.negative_if_in_neg_int |
292 | instantiation | 305, 306 | ⊢  |
| :  |
293 | instantiation | 329, 307, 308 | ⊢  |
| : , : , :  |
294 | instantiation | 383, 325, 309 | ⊢  |
| : , :  |
295 | instantiation | 376, 310 | ⊢  |
| : , : , :  |
296 | instantiation | 376, 311 | ⊢  |
| : , : , :  |
297 | instantiation | 329, 312, 313 | ⊢  |
| : , : , :  |
298 | instantiation | 314, 347, 452, 444, 349, 315, 353, 409, 369, 316* | ⊢  |
| : , : , : , : , : , :  |
299 | axiom | | ⊢  |
| proveit.physics.quantum.QPE._mod_add_def |
300 | conjecture | | ⊢  |
| proveit.physics.quantum.QPE._best_floor_is_int |
301 | instantiation | 450, 317, 318 | ⊢  |
| : , : , :  |
302 | conjecture | | ⊢  |
| proveit.numbers.negation.mult_neg_one_left |
303 | conjecture | | ⊢  |
| proveit.numbers.addition.subtraction.subtract_from_add |
304 | instantiation | 450, 319, 320 | , ⊢  |
| : , : , :  |
305 | conjecture | | ⊢  |
| proveit.numbers.negation.int_neg_closure |
306 | instantiation | 321, 322, 389 | ⊢  |
| : , :  |
307 | instantiation | 346, 444, 452, 347, 323, 349, 325, 369, 385 | ⊢  |
| : , : , : , : , : , :  |
308 | instantiation | 324, 325, 385, 326 | ⊢  |
| : , : , :  |
309 | instantiation | 450, 430, 327 | ⊢  |
| : , : , :  |
310 | instantiation | 376, 344 | ⊢  |
| : , : , :  |
311 | instantiation | 376, 328 | ⊢  |
| : , : , :  |
312 | instantiation | 329, 330, 331 | ⊢  |
| : , : , :  |
313 | instantiation | 332, 347, 444, 452, 349, 333, 380, 353, 409, 369, 334 | ⊢  |
| : , : , : , : , : , : , : , :  |
314 | conjecture | | ⊢  |
| proveit.numbers.addition.association |
315 | instantiation | 370 | ⊢  |
| : , :  |
316 | instantiation | 335, 336, 337 | ⊢  |
| : , : , :  |
317 | instantiation | 434, 338, 442 | ⊢  |
| : , :  |
318 | assumption | | ⊢  |
319 | instantiation | 434, 338, 339 | ⊢  |
| : , :  |
320 | assumption | | ⊢  |
321 | conjecture | | ⊢  |
| proveit.numbers.addition.add_nat_pos_closure_bin |
322 | instantiation | 340, 414, 341 | ⊢  |
| :  |
323 | instantiation | 370 | ⊢  |
| : , :  |
324 | conjecture | | ⊢  |
| proveit.numbers.addition.subtraction.add_cancel_triple_12 |
325 | instantiation | 450, 430, 342 | ⊢  |
| : , : , :  |
326 | instantiation | 350 | ⊢  |
| :  |
327 | instantiation | 450, 437, 343 | ⊢  |
| : , : , :  |
328 | instantiation | 376, 344 | ⊢  |
| : , : , :  |
329 | axiom | | ⊢  |
| proveit.logic.equality.equals_transitivity |
330 | instantiation | 346, 347, 452, 444, 349, 348, 380, 353, 345 | ⊢  |
| : , : , : , : , : , :  |
331 | instantiation | 346, 452, 366, 347, 348, 367, 349, 380, 353, 368, 409, 369 | ⊢  |
| : , : , : , : , : , :  |
332 | conjecture | | ⊢  |
| proveit.numbers.addition.subtraction.add_cancel_general |
333 | instantiation | 370 | ⊢  |
| : , :  |
334 | instantiation | 350 | ⊢  |
| :  |
335 | theorem | | ⊢  |
| proveit.logic.equality.sub_right_side_into |
336 | instantiation | 351, 409, 423, 352 | ⊢  |
| : , : , :  |
337 | instantiation | 383, 409, 353 | ⊢  |
| : , :  |
338 | instantiation | 441, 354, 436 | ⊢  |
| : , :  |
339 | instantiation | 448, 355 | ⊢  |
| :  |
340 | conjecture | | ⊢  |
| proveit.numbers.number_sets.integers.pos_int_is_natural_pos |
341 | instantiation | 356, 357, 358 | ⊢  |
| : , : , :  |
342 | instantiation | 450, 437, 359 | ⊢  |
| : , : , :  |
343 | instantiation | 450, 445, 360 | ⊢  |
| : , : , :  |
344 | instantiation | 361, 362, 363, 364 | ⊢  |
| : , : , : , :  |
345 | instantiation | 365, 366, 367, 368, 409, 369 | ⊢  |
| : , :  |
346 | conjecture | | ⊢  |
| proveit.numbers.addition.disassociation |
347 | axiom | | ⊢  |
| proveit.numbers.number_sets.natural_numbers.zero_in_nats |
348 | instantiation | 370 | ⊢  |
| : , :  |
349 | conjecture | | ⊢  |
| proveit.core_expr_types.tuples.tuple_len_0_typical_eq |
350 | axiom | | ⊢  |
| proveit.logic.equality.equals_reflexivity |
351 | conjecture | | ⊢  |
| proveit.numbers.addition.subtraction.subtract_from_add_reversed |
352 | conjecture | | ⊢  |
| proveit.numbers.numerals.decimals.add_1_1 |
353 | instantiation | 450, 430, 371 | ⊢  |
| : , : , :  |
354 | instantiation | 448, 442 | ⊢  |
| :  |
355 | instantiation | 441, 414, 436 | ⊢  |
| : , :  |
356 | conjecture | | ⊢  |
| proveit.numbers.ordering.transitivity_less_less_eq |
357 | conjecture | | ⊢  |
| proveit.numbers.numerals.decimals.less_0_1 |
358 | instantiation | 372, 436, 435, 426 | ⊢  |
| : , : , :  |
359 | instantiation | 450, 445, 414 | ⊢  |
| : , : , :  |
360 | instantiation | 441, 402, 417 | ⊢  |
| : , :  |
361 | conjecture | | ⊢  |
| proveit.logic.equality.four_chain_transitivity |
362 | instantiation | 376, 373 | ⊢  |
| : , : , :  |
363 | instantiation | 374, 375 | ⊢  |
| : , :  |
364 | instantiation | 376, 377 | ⊢  |
| : , : , :  |
365 | conjecture | | ⊢  |
| proveit.numbers.addition.add_complex_closure |
366 | conjecture | | ⊢  |
| proveit.numbers.numerals.decimals.nat3 |
367 | instantiation | 378 | ⊢  |
| : , : , :  |
368 | instantiation | 379, 380 | ⊢  |
| :  |
369 | instantiation | 450, 430, 381 | ⊢  |
| : , : , :  |
370 | conjecture | | ⊢  |
| proveit.numbers.numerals.decimals.tuple_len_2_typical_eq |
371 | instantiation | 450, 437, 382 | ⊢  |
| : , : , :  |
372 | conjecture | | ⊢  |
| proveit.numbers.number_sets.integers.interval_lower_bound |
373 | instantiation | 383, 384, 385 | ⊢  |
| : , :  |
374 | theorem | | ⊢  |
| proveit.logic.equality.equals_reversal |
375 | instantiation | 386, 423, 395, 394, 411 | ⊢  |
| : , : , :  |
376 | axiom | | ⊢  |
| proveit.logic.equality.substitution |
377 | instantiation | 387, 388, 389 | ⊢  |
| : , :  |
378 | conjecture | | ⊢  |
| proveit.numbers.numerals.decimals.tuple_len_3_typical_eq |
379 | conjecture | | ⊢  |
| proveit.numbers.negation.complex_closure |
380 | instantiation | 390, 391, 392 | ⊢  |
| : , :  |
381 | instantiation | 450, 437, 393 | ⊢  |
| : , : , :  |
382 | instantiation | 450, 445, 443 | ⊢  |
| : , : , :  |
383 | conjecture | | ⊢  |
| proveit.numbers.addition.commutation |
384 | instantiation | 450, 430, 394 | ⊢  |
| : , : , :  |
385 | instantiation | 450, 430, 395 | ⊢  |
| : , : , :  |
386 | conjecture | | ⊢  |
| proveit.numbers.exponentiation.product_of_real_powers |
387 | conjecture | | ⊢  |
| proveit.numbers.exponentiation.neg_power_as_div |
388 | instantiation | 450, 396, 397 | ⊢  |
| : , : , :  |
389 | conjecture | | ⊢  |
| proveit.numbers.numerals.decimals.posnat1 |
390 | conjecture | | ⊢  |
| proveit.numbers.multiplication.mult_complex_closure_bin |
391 | instantiation | 398, 409, 399, 400 | ⊢  |
| : , :  |
392 | instantiation | 450, 430, 401 | ⊢  |
| : , : , :  |
393 | instantiation | 450, 445, 402 | ⊢  |
| : , : , :  |
394 | instantiation | 403, 404, 440 | ⊢  |
| : , : , :  |
395 | instantiation | 450, 437, 405 | ⊢  |
| : , : , :  |
396 | conjecture | | ⊢  |
| proveit.numbers.number_sets.complex_numbers.real_nonzero_within_complex_nonzero |
397 | instantiation | 450, 406, 407 | ⊢  |
| : , : , :  |
398 | conjecture | | ⊢  |
| proveit.numbers.division.div_complex_closure |
399 | instantiation | 408, 423, 409 | ⊢  |
| : , :  |
400 | instantiation | 410, 411, 412 | ⊢  |
| : , : , :  |
401 | instantiation | 450, 437, 413 | ⊢  |
| : , : , :  |
402 | instantiation | 448, 414 | ⊢  |
| :  |
403 | theorem | | ⊢  |
| proveit.logic.sets.inclusion.unfold_subset_eq |
404 | instantiation | 415, 416 | ⊢  |
| : , :  |
405 | instantiation | 450, 445, 417 | ⊢  |
| : , : , :  |
406 | conjecture | | ⊢  |
| proveit.numbers.number_sets.real_numbers.rational_nonzero_within_real_nonzero |
407 | instantiation | 450, 418, 419 | ⊢  |
| : , : , :  |
408 | conjecture | | ⊢  |
| proveit.numbers.exponentiation.exp_complex_closure |
409 | instantiation | 450, 430, 420 | ⊢  |
| : , : , :  |
410 | theorem | | ⊢  |
| proveit.logic.equality.sub_left_side_into |
411 | instantiation | 421, 428 | ⊢  |
| :  |
412 | instantiation | 422, 423 | ⊢  |
| :  |
413 | instantiation | 450, 445, 424 | ⊢  |
| : , : , :  |
414 | instantiation | 450, 425, 426 | ⊢  |
| : , : , :  |
415 | theorem | | ⊢  |
| proveit.logic.sets.inclusion.relax_proper_subset |
416 | conjecture | | ⊢  |
| proveit.numbers.number_sets.real_numbers.nat_pos_within_real |
417 | instantiation | 448, 436 | ⊢  |
| :  |
418 | conjecture | | ⊢  |
| proveit.numbers.number_sets.rational_numbers.nonzero_int_within_rational_nonzero |
419 | instantiation | 450, 427, 428 | ⊢  |
| : , : , :  |
420 | instantiation | 450, 437, 429 | ⊢  |
| : , : , :  |
421 | conjecture | | ⊢  |
| proveit.numbers.number_sets.natural_numbers.nonzero_if_is_nat_pos |
422 | conjecture | | ⊢  |
| proveit.numbers.exponentiation.complex_x_to_first_power_is_x |
423 | instantiation | 450, 430, 431 | ⊢  |
| : , : , :  |
424 | instantiation | 432, 449, 433 | ⊢  |
| : , :  |
425 | instantiation | 434, 436, 435 | ⊢  |
| : , :  |
426 | assumption | | ⊢  |
427 | conjecture | | ⊢  |
| proveit.numbers.number_sets.integers.nat_pos_within_nonzero_int |
428 | conjecture | | ⊢  |
| proveit.numbers.numerals.decimals.posnat2 |
429 | instantiation | 450, 445, 436 | ⊢  |
| : , : , :  |
430 | conjecture | | ⊢  |
| proveit.numbers.number_sets.complex_numbers.real_within_complex |
431 | instantiation | 450, 437, 438 | ⊢  |
| : , : , :  |
432 | conjecture | | ⊢  |
| proveit.numbers.exponentiation.exp_int_closure |
433 | instantiation | 450, 439, 440 | ⊢  |
| : , : , :  |
434 | conjecture | | ⊢  |
| proveit.numbers.number_sets.integers.int_interval_within_int |
435 | instantiation | 441, 442, 443 | ⊢  |
| : , :  |
436 | instantiation | 450, 451, 444 | ⊢  |
| : , : , :  |
437 | conjecture | | ⊢  |
| proveit.numbers.number_sets.real_numbers.rational_within_real |
438 | instantiation | 450, 445, 449 | ⊢  |
| : , : , :  |
439 | conjecture | | ⊢  |
| proveit.numbers.number_sets.natural_numbers.nat_pos_within_nat |
440 | axiom | | ⊢  |
| proveit.physics.quantum.QPE._t_in_natural_pos |
441 | conjecture | | ⊢  |
| proveit.numbers.addition.add_int_closure_bin |
442 | instantiation | 450, 446, 447 | ⊢  |
| : , : , :  |
443 | instantiation | 448, 449 | ⊢  |
| :  |
444 | theorem | | ⊢  |
| proveit.numbers.numerals.decimals.nat1 |
445 | conjecture | | ⊢  |
| proveit.numbers.number_sets.rational_numbers.int_within_rational |
446 | conjecture | | ⊢  |
| proveit.numbers.number_sets.integers.nat_pos_within_int |
447 | conjecture | | ⊢  |
| proveit.physics.quantum.QPE._two_pow_t_minus_one_is_nat_pos |
448 | conjecture | | ⊢  |
| proveit.numbers.negation.int_closure |
449 | instantiation | 450, 451, 452 | ⊢  |
| : , : , :  |
450 | theorem | | ⊢  |
| proveit.logic.sets.inclusion.superset_membership_from_proper_subset |
451 | conjecture | | ⊢  |
| proveit.numbers.number_sets.integers.nat_within_int |
452 | theorem | | ⊢  |
| proveit.numbers.numerals.decimals.nat2 |
*equality replacement requirements |