| step type | requirements | statement |
0 | instantiation | 1, 2, 3, 4, 5* | ⊢ |
| : , : |
1 | theorem | | ⊢ |
| proveit.numbers.absolute_value.abs_eq |
2 | instantiation | 6, 7 | ⊢ |
| : |
3 | instantiation | 286, 11, 12 | ⊢ |
| : , : |
4 | instantiation | 337, 8, 9 | ⊢ |
| : , : , : |
5 | instantiation | 360, 491, 10, 11, 12, 13*, 14* | ⊢ |
| : , : |
6 | theorem | | ⊢ |
| proveit.physics.quantum.QPE._alpha_are_complex |
7 | instantiation | 15, 499, 484 | ⊢ |
| : , : |
8 | instantiation | 337, 16, 17, 18* | ⊢ |
| : , : , : |
9 | instantiation | 19, 61, 62, 20, 21, 22, 23*, 24* | ⊢ |
| : , : , : , : |
10 | instantiation | 492 | ⊢ |
| : , : |
11 | instantiation | 509, 501, 25 | ⊢ |
| : , : , : |
12 | instantiation | 88, 28, 29, 30 | ⊢ |
| : , : |
13 | instantiation | 389, 26 | ⊢ |
| : |
14 | instantiation | 27, 28, 29, 30, 31* | ⊢ |
| : , : |
15 | theorem | | ⊢ |
| proveit.numbers.modular.mod_natpos_in_interval |
16 | instantiation | 32, 499 | ⊢ |
| : |
17 | instantiation | 33, 499 | ⊢ |
| : |
18 | instantiation | 453, 34, 35 | ⊢ |
| : , : , : |
19 | theorem | | ⊢ |
| proveit.numbers.summation.gen_finite_geom_sum |
20 | theorem | | ⊢ |
| proveit.numbers.number_sets.integers.zero_is_int |
21 | instantiation | 36, 37, 485 | ⊢ |
| : , : |
22 | instantiation | 38, 39 | ⊢ |
| : , : |
23 | instantiation | 346, 61 | ⊢ |
| : |
24 | instantiation | 453, 40, 41 | ⊢ |
| : , : , : |
25 | instantiation | 509, 505, 42 | ⊢ |
| : , : , : |
26 | instantiation | 422, 43 | ⊢ |
| : , : |
27 | theorem | | ⊢ |
| proveit.numbers.absolute_value.abs_frac |
28 | instantiation | 45, 417, 44 | ⊢ |
| : , : |
29 | instantiation | 45, 417, 46 | ⊢ |
| : , : |
30 | instantiation | 47, 48 | ⊢ |
| : , : |
31 | instantiation | 453, 49, 50 | ⊢ |
| : , : , : |
32 | theorem | | ⊢ |
| proveit.physics.quantum.QPE._alpha_m_mod_as_geometric_sum |
33 | theorem | | ⊢ |
| proveit.physics.quantum.QPE._phase_from_best_with_delta_b |
34 | instantiation | 405, 406, 511, 504, 407, 51, 69, 469, 52 | ⊢ |
| : , : , : , : , : , : |
35 | instantiation | 53, 69, 469, 54 | ⊢ |
| : , : , : |
36 | theorem | | ⊢ |
| proveit.numbers.addition.add_int_closure_bin |
37 | instantiation | 509, 55, 484 | ⊢ |
| : , : , : |
38 | theorem | | ⊢ |
| proveit.numbers.addition.subtraction.nonneg_difference |
39 | instantiation | 439, 484 | ⊢ |
| : |
40 | instantiation | 461, 56 | ⊢ |
| : , : , : |
41 | instantiation | 57, 176, 75, 411, 58* | ⊢ |
| : , : , : |
42 | instantiation | 509, 424, 59 | ⊢ |
| : , : , : |
43 | instantiation | 307, 59 | ⊢ |
| : |
44 | instantiation | 218, 60 | ⊢ |
| : |
45 | theorem | | ⊢ |
| proveit.numbers.addition.add_complex_closure_bin |
46 | instantiation | 218, 61 | ⊢ |
| : |
47 | theorem | | ⊢ |
| proveit.numbers.addition.subtraction.nonzero_difference_if_different |
48 | instantiation | 110, 62 | ⊢ |
| : , : |
49 | instantiation | 475, 511, 63, 64, 65, 66 | ⊢ |
| : , : , : , : |
50 | instantiation | 180, 370, 67, 68 | ⊢ |
| : , : , : |
51 | instantiation | 492 | ⊢ |
| : , : |
52 | instantiation | 218, 69 | ⊢ |
| : |
53 | theorem | | ⊢ |
| proveit.numbers.addition.subtraction.add_cancel_triple_13 |
54 | instantiation | 444 | ⊢ |
| : |
55 | theorem | | ⊢ |
| proveit.numbers.number_sets.integers.nat_pos_within_int |
56 | instantiation | 453, 70, 71 | ⊢ |
| : , : , : |
57 | theorem | | ⊢ |
| proveit.numbers.exponentiation.complex_power_of_complex_power |
58 | instantiation | 330, 406, 503, 504, 407, 72, 495, 353, 191, 469, 411 | ⊢ |
| : , : , : , : , : , : |
59 | instantiation | 450, 451, 73 | ⊢ |
| : , : |
60 | instantiation | 316, 128, 74 | ⊢ |
| : , : |
61 | instantiation | 316, 128, 75 | ⊢ |
| : , : |
62 | instantiation | 298, 76, 77 | ⊢ |
| : , : , : |
63 | instantiation | 492 | ⊢ |
| : , : |
64 | instantiation | 492 | ⊢ |
| : , : |
65 | instantiation | 81, 279, 78, 82*, 79*, 80* | ⊢ |
| : , : |
66 | instantiation | 81, 279, 98, 82*, 83*, 84* | ⊢ |
| : , : |
67 | instantiation | 468, 85, 86 | ⊢ |
| : |
68 | instantiation | 509, 501, 87 | ⊢ |
| : , : , : |
69 | instantiation | 88, 89, 411, 90 | ⊢ |
| : , : |
70 | instantiation | 405, 406, 511, 504, 407, 91, 411, 409, 417 | ⊢ |
| : , : , : , : , : , : |
71 | instantiation | 92, 417, 411, 412 | ⊢ |
| : , : , : |
72 | instantiation | 211 | ⊢ |
| : , : , : , : |
73 | instantiation | 509, 474, 484 | ⊢ |
| : , : , : |
74 | instantiation | 337, 93, 94 | ⊢ |
| : , : , : |
75 | instantiation | 337, 95, 96 | ⊢ |
| : , : , : |
76 | instantiation | 97, 98, 99, 100* | ⊢ |
| : |
77 | instantiation | 461, 101 | ⊢ |
| : , : , : |
78 | instantiation | 337, 251, 231 | ⊢ |
| : , : , : |
79 | instantiation | 283, 102 | ⊢ |
| : , : |
80 | instantiation | 453, 103, 104 | ⊢ |
| : , : , : |
81 | theorem | | ⊢ |
| proveit.trigonometry.complex_unit_circle_chord_length |
82 | instantiation | 453, 105, 106 | ⊢ |
| : , : , : |
83 | instantiation | 283, 107 | ⊢ |
| : , : |
84 | instantiation | 453, 108, 109 | ⊢ |
| : , : , : |
85 | instantiation | 509, 501, 134 | ⊢ |
| : , : , : |
86 | instantiation | 110, 111 | ⊢ |
| : , : |
87 | instantiation | 112, 113 | ⊢ |
| : |
88 | theorem | | ⊢ |
| proveit.numbers.division.div_complex_closure |
89 | instantiation | 509, 501, 114 | ⊢ |
| : , : , : |
90 | instantiation | 490, 484 | ⊢ |
| : |
91 | instantiation | 492 | ⊢ |
| : , : |
92 | theorem | | ⊢ |
| proveit.numbers.addition.subtraction.add_cancel_triple_32 |
93 | instantiation | 286, 271, 115 | ⊢ |
| : , : |
94 | instantiation | 453, 116, 117 | ⊢ |
| : , : , : |
95 | instantiation | 286, 271, 161 | ⊢ |
| : , : |
96 | instantiation | 453, 118, 119 | ⊢ |
| : , : , : |
97 | theorem | | ⊢ |
| proveit.numbers.exponentiation.unit_complex_polar_num_neq_one |
98 | instantiation | 337, 255, 239 | ⊢ |
| : , : , : |
99 | instantiation | 298, 120, 121 | ⊢ |
| : , : , : |
100 | instantiation | 283, 122 | ⊢ |
| : , : |
101 | instantiation | 267, 511, 504, 406, 272, 407, 495, 353, 191, 469 | ⊢ |
| : , : , : , : , : , : , : |
102 | instantiation | 461, 123 | ⊢ |
| : , : , : |
103 | instantiation | 461, 124 | ⊢ |
| : , : , : |
104 | instantiation | 453, 125, 126 | ⊢ |
| : , : , : |
105 | instantiation | 461, 127 | ⊢ |
| : , : , : |
106 | instantiation | 346, 128 | ⊢ |
| : |
107 | instantiation | 461, 129 | ⊢ |
| : , : , : |
108 | instantiation | 461, 130 | ⊢ |
| : , : , : |
109 | instantiation | 453, 131, 132 | ⊢ |
| : , : , : |
110 | theorem | | ⊢ |
| proveit.logic.equality.not_equals_symmetry |
111 | instantiation | 133, 279, 134, 135 | ⊢ |
| : , : |
112 | theorem | | ⊢ |
| proveit.trigonometry.real_closure |
113 | instantiation | 337, 216, 198 | ⊢ |
| : , : , : |
114 | instantiation | 509, 505, 136 | ⊢ |
| : , : , : |
115 | instantiation | 337, 137, 138 | ⊢ |
| : , : , : |
116 | instantiation | 330, 504, 288, 406, 139, 407, 271, 191, 469, 411 | ⊢ |
| : , : , : , : , : , : |
117 | instantiation | 330, 406, 511, 288, 407, 272, 139, 495, 353, 191, 469, 411 | ⊢ |
| : , : , : , : , : , : |
118 | instantiation | 330, 504, 511, 406, 162, 407, 271, 191, 469 | ⊢ |
| : , : , : , : , : , : |
119 | instantiation | 330, 406, 511, 407, 272, 162, 495, 353, 191, 469 | ⊢ |
| : , : , : , : , : , : |
120 | instantiation | 140, 141, 142, 186, 184 | ⊢ |
| : , : |
121 | instantiation | 340, 143, 418, 144 | ⊢ |
| : , : , : , : |
122 | instantiation | 461, 145 | ⊢ |
| : , : , : |
123 | instantiation | 453, 146, 147 | ⊢ |
| : , : , : |
124 | instantiation | 453, 148, 149 | ⊢ |
| : , : , : |
125 | instantiation | 453, 150, 151 | ⊢ |
| : , : , : |
126 | instantiation | 462, 175 | ⊢ |
| : |
127 | instantiation | 333, 191 | ⊢ |
| : |
128 | instantiation | 509, 501, 152 | ⊢ |
| : , : , : |
129 | instantiation | 453, 153, 171 | ⊢ |
| : , : , : |
130 | instantiation | 453, 154, 155 | ⊢ |
| : , : , : |
131 | instantiation | 453, 156, 157 | ⊢ |
| : , : , : |
132 | instantiation | 462, 181 | ⊢ |
| : |
133 | theorem | | ⊢ |
| proveit.numbers.ordering.less_is_not_eq |
134 | instantiation | 158, 279, 472, 160 | ⊢ |
| : , : , : |
135 | instantiation | 159, 279, 472, 160 | ⊢ |
| : , : , : |
136 | instantiation | 509, 507, 499 | ⊢ |
| : , : , : |
137 | instantiation | 286, 161, 411 | ⊢ |
| : , : |
138 | instantiation | 330, 406, 511, 504, 407, 162, 191, 469, 411 | ⊢ |
| : , : , : , : , : , : |
139 | instantiation | 315 | ⊢ |
| : , : , : |
140 | theorem | | ⊢ |
| proveit.logic.booleans.disjunction.right_if_not_left |
141 | instantiation | 163, 164 | ⊢ |
| : |
142 | instantiation | 165, 166 | ⊢ |
| : , : |
143 | instantiation | 167, 219, 271, 168, 169* | ⊢ |
| : , : |
144 | instantiation | 444 | ⊢ |
| : |
145 | instantiation | 453, 170, 171 | ⊢ |
| : , : , : |
146 | instantiation | 267, 406, 511, 407, 272, 273, 495, 353, 191, 469, 411 | ⊢ |
| : , : , : , : , : , : , : |
147 | instantiation | 287, 504, 503, 406, 193, 407, 191, 495, 353, 469, 411 | ⊢ |
| : , : , : , : , : , : |
148 | instantiation | 461, 172 | ⊢ |
| : , : , : |
149 | instantiation | 386, 210, 173* | ⊢ |
| : |
150 | instantiation | 461, 174 | ⊢ |
| : , : , : |
151 | instantiation | 180, 370, 369, 175, 479* | ⊢ |
| : , : , : |
152 | instantiation | 509, 414, 176 | ⊢ |
| : , : , : |
153 | instantiation | 267, 406, 511, 504, 407, 272, 495, 353, 191, 469 | ⊢ |
| : , : , : , : , : , : , : |
154 | instantiation | 461, 177 | ⊢ |
| : , : , : |
155 | instantiation | 386, 219, 178* | ⊢ |
| : |
156 | instantiation | 461, 179 | ⊢ |
| : , : , : |
157 | instantiation | 180, 370, 369, 181, 479* | ⊢ |
| : , : , : |
158 | theorem | | ⊢ |
| proveit.numbers.number_sets.real_numbers.all_in_interval_oc__is__real |
159 | theorem | | ⊢ |
| proveit.numbers.number_sets.real_numbers.interval_oc_lower_bound |
160 | instantiation | 182, 183 | ⊢ |
| : |
161 | instantiation | 286, 191, 469 | ⊢ |
| : , : |
162 | instantiation | 492 | ⊢ |
| : , : |
163 | axiom | | ⊢ |
| proveit.logic.booleans.negation.operand_is_bool |
164 | instantiation | 185, 184 | ⊢ |
| : |
165 | axiom | | ⊢ |
| proveit.logic.booleans.disjunction.right_in_bool |
166 | instantiation | 185, 186 | ⊢ |
| : |
167 | theorem | | ⊢ |
| proveit.numbers.division.div_as_mult |
168 | instantiation | 187, 511, 272, 370, 188 | ⊢ |
| : , : |
169 | instantiation | 453, 189, 190 | ⊢ |
| : , : , : |
170 | instantiation | 267, 406, 288, 407, 264, 495, 353, 469, 191 | ⊢ |
| : , : , : , : , : , : , : |
171 | instantiation | 287, 504, 288, 406, 264, 407, 191, 495, 353, 469 | ⊢ |
| : , : , : , : , : , : |
172 | instantiation | 309, 192 | ⊢ |
| : |
173 | instantiation | 360, 457, 193, 495, 353, 469, 411, 194* | ⊢ |
| : , : |
174 | instantiation | 453, 195, 196 | ⊢ |
| : , : , : |
175 | instantiation | 337, 197, 198 | ⊢ |
| : , : , : |
176 | theorem | | ⊢ |
| proveit.numbers.number_sets.real_numbers.e_is_real_pos |
177 | instantiation | 309, 199 | ⊢ |
| : |
178 | instantiation | 360, 200, 264, 495, 353, 469, 234*, 235* | ⊢ |
| : , : |
179 | instantiation | 287, 504, 511, 406, 214, 407, 495, 353, 354 | ⊢ |
| : , : , : , : , : , : |
180 | theorem | | ⊢ |
| proveit.numbers.division.frac_cancel_left |
181 | instantiation | 509, 501, 202 | ⊢ |
| : , : , : |
182 | theorem | | ⊢ |
| proveit.trigonometry.sine_pos_interval |
183 | instantiation | 201, 279, 383, 202, 203 | ⊢ |
| : , : , : |
184 | instantiation | 204, 470 | ⊢ |
| : , : |
185 | theorem | | ⊢ |
| proveit.logic.booleans.in_bool_if_true |
186 | instantiation | 205, 206 | ⊢ |
| : |
187 | theorem | | ⊢ |
| proveit.numbers.multiplication.mult_not_eq_zero |
188 | instantiation | 509, 395, 320 | ⊢ |
| : , : , : |
189 | instantiation | 461, 207 | ⊢ |
| : , : , : |
190 | instantiation | 453, 208, 209 | ⊢ |
| : , : , : |
191 | theorem | | ⊢ |
| proveit.numbers.number_sets.complex_numbers.i_is_complex |
192 | instantiation | 218, 210 | ⊢ |
| : |
193 | instantiation | 211 | ⊢ |
| : , : , : , : |
194 | instantiation | 453, 212, 213 | ⊢ |
| : , : , : |
195 | instantiation | 267, 406, 504, 511, 407, 214, 411, 495, 353, 354 | ⊢ |
| : , : , : , : , : , : , : |
196 | instantiation | 287, 504, 288, 406, 215, 407, 495, 411, 353, 354 | ⊢ |
| : , : , : , : , : , : |
197 | instantiation | 509, 501, 216 | ⊢ |
| : , : , : |
198 | instantiation | 330, 406, 511, 504, 407, 217, 411, 353, 354 | ⊢ |
| : , : , : , : , : , : |
199 | instantiation | 218, 219 | ⊢ |
| : |
200 | theorem | | ⊢ |
| proveit.numbers.numerals.decimals.posnat3 |
201 | theorem | | ⊢ |
| proveit.numbers.number_sets.real_numbers.in_IntervalOO |
202 | instantiation | 509, 414, 240 | ⊢ |
| : , : , : |
203 | instantiation | 220, 221, 222 | ⊢ |
| : , : |
204 | theorem | | ⊢ |
| proveit.logic.equality.unfold_not_equals |
205 | theorem | | ⊢ |
| proveit.physics.quantum.QPE._delta_b_is_zero_or_non_int |
206 | instantiation | 223, 504, 406, 407 | ⊢ |
| : , : , : , : , : |
207 | instantiation | 224, 495, 353, 442, 473, 294, 225* | ⊢ |
| : , : , : |
208 | instantiation | 453, 226, 227 | ⊢ |
| : , : , : |
209 | instantiation | 453, 228, 229 | ⊢ |
| : , : , : |
210 | instantiation | 337, 230, 231 | ⊢ |
| : , : , : |
211 | theorem | | ⊢ |
| proveit.numbers.numerals.decimals.tuple_len_4_typical_eq |
212 | instantiation | 475, 288, 232, 233, 234, 235, 362 | ⊢ |
| : , : , : , : |
213 | instantiation | 267, 406, 288, 407, 236, 495, 353, 354, 411 | ⊢ |
| : , : , : , : , : , : , : |
214 | instantiation | 492 | ⊢ |
| : , : |
215 | instantiation | 315 | ⊢ |
| : , : , : |
216 | instantiation | 364, 237, 384 | ⊢ |
| : , : |
217 | instantiation | 492 | ⊢ |
| : , : |
218 | theorem | | ⊢ |
| proveit.numbers.negation.complex_closure |
219 | instantiation | 337, 238, 239 | ⊢ |
| : , : , : |
220 | theorem | | ⊢ |
| proveit.logic.booleans.conjunction.and_if_both |
221 | instantiation | 363, 240 | ⊢ |
| : |
222 | instantiation | 241, 242, 243 | ⊢ |
| : , : , : |
223 | theorem | | ⊢ |
| proveit.logic.sets.enumeration.in_enumerated_set |
224 | theorem | | ⊢ |
| proveit.numbers.exponentiation.real_power_of_product |
225 | instantiation | 244, 370, 481, 404* | ⊢ |
| : , : |
226 | instantiation | 453, 245, 246 | ⊢ |
| : , : , : |
227 | instantiation | 453, 247, 248 | ⊢ |
| : , : , : |
228 | instantiation | 352, 406, 288, 407, 290, 353, 469, 291 | ⊢ |
| : , : , : , : |
229 | instantiation | 453, 249, 250 | ⊢ |
| : , : , : |
230 | instantiation | 509, 501, 251 | ⊢ |
| : , : , : |
231 | instantiation | 453, 252, 253 | ⊢ |
| : , : , : |
232 | instantiation | 315 | ⊢ |
| : , : , : |
233 | instantiation | 315 | ⊢ |
| : , : , : |
234 | instantiation | 389, 254 | ⊢ |
| : |
235 | instantiation | 389, 304 | ⊢ |
| : |
236 | instantiation | 315 | ⊢ |
| : , : , : |
237 | instantiation | 364, 443, 383 | ⊢ |
| : , : |
238 | instantiation | 509, 501, 255 | ⊢ |
| : , : , : |
239 | instantiation | 330, 406, 511, 504, 407, 272, 495, 353, 469 | ⊢ |
| : , : , : , : , : , : |
240 | instantiation | 256, 413, 415 | ⊢ |
| : , : |
241 | axiom | | ⊢ |
| proveit.numbers.ordering.transitivity_less_less |
242 | instantiation | 337, 257, 300 | ⊢ |
| : , : , : |
243 | instantiation | 347, 335, 258, 259, 260*, 261* | ⊢ |
| : , : , : |
244 | theorem | | ⊢ |
| proveit.numbers.exponentiation.neg_power_as_div |
245 | instantiation | 330, 406, 288, 504, 407, 264, 495, 353, 469, 262 | ⊢ |
| : , : , : , : , : , : |
246 | instantiation | 330, 288, 511, 406, 264, 263, 407, 495, 353, 469, 334, 291 | ⊢ |
| : , : , : , : , : , : |
247 | instantiation | 267, 406, 288, 504, 407, 264, 495, 353, 469, 334, 291 | ⊢ |
| : , : , : , : , : , : , : |
248 | instantiation | 453, 265, 266 | ⊢ |
| : , : , : |
249 | instantiation | 267, 504, 406, 407, 353, 469, 291 | ⊢ |
| : , : , : , : , : , : , : |
250 | instantiation | 287, 406, 511, 504, 407, 268, 353, 291, 469, 269* | ⊢ |
| : , : , : , : , : , : |
251 | instantiation | 364, 297, 270 | ⊢ |
| : , : |
252 | instantiation | 330, 504, 511, 406, 273, 407, 271, 469, 411 | ⊢ |
| : , : , : , : , : , : |
253 | instantiation | 330, 406, 511, 407, 272, 273, 495, 353, 469, 411 | ⊢ |
| : , : , : , : , : , : |
254 | instantiation | 274, 511 | ⊢ |
| : |
255 | instantiation | 364, 297, 488 | ⊢ |
| : , : |
256 | theorem | | ⊢ |
| proveit.numbers.multiplication.mult_real_pos_closure_bin |
257 | instantiation | 275, 276, 277 | ⊢ |
| : , : , : |
258 | instantiation | 364, 365, 279 | ⊢ |
| : , : |
259 | instantiation | 278, 365, 279, 383, 329, 280 | ⊢ |
| : , : , : |
260 | instantiation | 453, 281, 282 | ⊢ |
| : , : , : |
261 | instantiation | 283, 284, 285* | ⊢ |
| : , : |
262 | instantiation | 286, 334, 291 | ⊢ |
| : , : |
263 | instantiation | 492 | ⊢ |
| : , : |
264 | instantiation | 315 | ⊢ |
| : , : , : |
265 | instantiation | 287, 406, 511, 288, 407, 289, 290, 334, 495, 353, 469, 291 | ⊢ |
| : , : , : , : , : , : |
266 | instantiation | 461, 292 | ⊢ |
| : , : , : |
267 | theorem | | ⊢ |
| proveit.numbers.multiplication.leftward_commutation |
268 | instantiation | 492 | ⊢ |
| : , : |
269 | instantiation | 293, 353, 472, 442, 294, 295*, 296* | ⊢ |
| : , : , : |
270 | instantiation | 364, 488, 443 | ⊢ |
| : , : |
271 | instantiation | 509, 501, 297 | ⊢ |
| : , : , : |
272 | instantiation | 492 | ⊢ |
| : , : |
273 | instantiation | 492 | ⊢ |
| : , : |
274 | theorem | | ⊢ |
| proveit.numbers.number_sets.natural_numbers.natural_lower_bound |
275 | theorem | | ⊢ |
| proveit.numbers.ordering.transitivity_less_less_eq |
276 | instantiation | 298, 299, 300 | ⊢ |
| : , : , : |
277 | instantiation | 301, 383, 302, 448, 303, 304, 305*, 306* | ⊢ |
| : , : , : |
278 | theorem | | ⊢ |
| proveit.numbers.multiplication.strong_bound_via_right_factor_bound |
279 | theorem | | ⊢ |
| proveit.numbers.number_sets.real_numbers.zero_is_real |
280 | instantiation | 307, 425 | ⊢ |
| : |
281 | instantiation | 461, 308 | ⊢ |
| : , : , : |
282 | instantiation | 309, 310 | ⊢ |
| : |
283 | theorem | | ⊢ |
| proveit.logic.equality.equals_reversal |
284 | instantiation | 311, 406, 511, 504, 407, 312, 334, 353 | ⊢ |
| : , : , : , : , : , : |
285 | instantiation | 453, 313, 314 | ⊢ |
| : , : , : |
286 | theorem | | ⊢ |
| proveit.numbers.multiplication.mult_complex_closure_bin |
287 | theorem | | ⊢ |
| proveit.numbers.multiplication.association |
288 | theorem | | ⊢ |
| proveit.numbers.numerals.decimals.nat3 |
289 | instantiation | 492 | ⊢ |
| : , : |
290 | instantiation | 315 | ⊢ |
| : , : , : |
291 | instantiation | 316, 353, 409 | ⊢ |
| : , : |
292 | instantiation | 337, 317, 318 | ⊢ |
| : , : , : |
293 | theorem | | ⊢ |
| proveit.numbers.exponentiation.product_of_real_powers |
294 | instantiation | 319, 320 | ⊢ |
| : |
295 | instantiation | 441, 353 | ⊢ |
| : |
296 | instantiation | 453, 321, 322 | ⊢ |
| : , : , : |
297 | instantiation | 364, 502, 383 | ⊢ |
| : , : |
298 | theorem | | ⊢ |
| proveit.logic.equality.sub_left_side_into |
299 | instantiation | 323, 504, 413, 415, 324, 325* | ⊢ |
| : , : , : , : , : , : |
300 | instantiation | 461, 326 | ⊢ |
| : , : , : |
301 | theorem | | ⊢ |
| proveit.numbers.multiplication.weak_bound_via_right_factor_bound |
302 | instantiation | 364, 443, 384 | ⊢ |
| : , : |
303 | instantiation | 337, 327, 328 | ⊢ |
| : , : , : |
304 | instantiation | 422, 329 | ⊢ |
| : , : |
305 | instantiation | 330, 504, 511, 406, 331, 407, 353, 411, 354 | ⊢ |
| : , : , : , : , : , : |
306 | instantiation | 332, 353, 334 | ⊢ |
| : , : |
307 | theorem | | ⊢ |
| proveit.numbers.number_sets.rational_numbers.positive_if_in_rational_pos |
308 | instantiation | 333, 334 | ⊢ |
| : |
309 | theorem | | ⊢ |
| proveit.numbers.addition.elim_zero_left |
310 | instantiation | 509, 501, 335 | ⊢ |
| : , : , : |
311 | theorem | | ⊢ |
| proveit.numbers.multiplication.distribute_through_sum |
312 | instantiation | 492 | ⊢ |
| : , : |
313 | instantiation | 461, 336 | ⊢ |
| : , : , : |
314 | instantiation | 493, 353 | ⊢ |
| : |
315 | theorem | | ⊢ |
| proveit.numbers.numerals.decimals.tuple_len_3_typical_eq |
316 | theorem | | ⊢ |
| proveit.numbers.exponentiation.exp_complex_closure |
317 | instantiation | 337, 338, 339 | ⊢ |
| : , : , : |
318 | instantiation | 340, 341, 342, 343 | ⊢ |
| : , : , : , : |
319 | theorem | | ⊢ |
| proveit.numbers.number_sets.real_numbers.nonzero_if_in_real_nonzero |
320 | instantiation | 509, 344, 413 | ⊢ |
| : , : , : |
321 | instantiation | 461, 345 | ⊢ |
| : , : , : |
322 | instantiation | 346, 353 | ⊢ |
| : |
323 | theorem | | ⊢ |
| proveit.numbers.multiplication.strong_bound_via_factor_bound |
324 | instantiation | 347, 442, 502, 348, 349, 350*, 351* | ⊢ |
| : , : , : |
325 | instantiation | 352, 504, 353, 354 | ⊢ |
| : , : , : , : |
326 | instantiation | 453, 355, 356 | ⊢ |
| : , : , : |
327 | instantiation | 357, 358, 359 | ⊢ |
| : , : |
328 | instantiation | 360, 491, 361, 411, 469, 362* | ⊢ |
| : , : |
329 | instantiation | 363, 413 | ⊢ |
| : |
330 | theorem | | ⊢ |
| proveit.numbers.multiplication.disassociation |
331 | instantiation | 492 | ⊢ |
| : , : |
332 | theorem | | ⊢ |
| proveit.numbers.multiplication.commutation |
333 | theorem | | ⊢ |
| proveit.numbers.multiplication.mult_zero_right |
334 | instantiation | 509, 501, 448 | ⊢ |
| : , : , : |
335 | instantiation | 364, 365, 383 | ⊢ |
| : , : |
336 | instantiation | 366, 500, 508, 367* | ⊢ |
| : , : , : , : |
337 | theorem | | ⊢ |
| proveit.logic.equality.sub_right_side_into |
338 | instantiation | 368, 417, 369, 370 | ⊢ |
| : , : , : , : , : |
339 | instantiation | 453, 371, 372 | ⊢ |
| : , : , : |
340 | theorem | | ⊢ |
| proveit.logic.equality.four_chain_transitivity |
341 | instantiation | 461, 373 | ⊢ |
| : , : , : |
342 | instantiation | 461, 373 | ⊢ |
| : , : , : |
343 | instantiation | 494, 417 | ⊢ |
| : |
344 | theorem | | ⊢ |
| proveit.numbers.number_sets.real_numbers.real_pos_within_real_nonzero |
345 | instantiation | 374, 417, 412 | ⊢ |
| : , : |
346 | theorem | | ⊢ |
| proveit.numbers.exponentiation.exp_zero_eq_one |
347 | theorem | | ⊢ |
| proveit.numbers.addition.strong_bound_via_left_term_bound |
348 | instantiation | 509, 505, 375 | ⊢ |
| : , : , : |
349 | instantiation | 376, 502, 443, 472, 377, 378 | ⊢ |
| : , : , : |
350 | instantiation | 379, 417, 495, 380 | ⊢ |
| : , : , : |
351 | instantiation | 453, 381, 382 | ⊢ |
| : , : , : |
352 | theorem | | ⊢ |
| proveit.numbers.multiplication.elim_one_any |
353 | instantiation | 509, 501, 383 | ⊢ |
| : , : , : |
354 | instantiation | 509, 501, 384 | ⊢ |
| : , : , : |
355 | instantiation | 461, 385 | ⊢ |
| : , : , : |
356 | instantiation | 386, 469 | ⊢ |
| : |
357 | theorem | | ⊢ |
| proveit.numbers.absolute_value.weak_upper_bound |
358 | instantiation | 387, 420, 448, 421 | ⊢ |
| : , : , : |
359 | instantiation | 422, 388 | ⊢ |
| : , : |
360 | theorem | | ⊢ |
| proveit.numbers.absolute_value.abs_prod |
361 | instantiation | 492 | ⊢ |
| : , : |
362 | instantiation | 389, 390 | ⊢ |
| : |
363 | theorem | | ⊢ |
| proveit.numbers.number_sets.real_numbers.positive_if_in_real_pos |
364 | theorem | | ⊢ |
| proveit.numbers.multiplication.mult_real_closure_bin |
365 | instantiation | 509, 505, 391 | ⊢ |
| : , : , : |
366 | theorem | | ⊢ |
| proveit.numbers.addition.rational_pair_addition |
367 | instantiation | 453, 392, 393 | ⊢ |
| : , : , : |
368 | theorem | | ⊢ |
| proveit.numbers.division.mult_frac_cancel_denom_left |
369 | instantiation | 509, 395, 394 | ⊢ |
| : , : , : |
370 | instantiation | 509, 395, 396 | ⊢ |
| : , : , : |
371 | instantiation | 461, 397 | ⊢ |
| : , : , : |
372 | instantiation | 461, 398 | ⊢ |
| : , : , : |
373 | instantiation | 462, 417 | ⊢ |
| : |
374 | theorem | | ⊢ |
| proveit.numbers.addition.subtraction.add_cancel_basic |
375 | instantiation | 509, 507, 399 | ⊢ |
| : , : , : |
376 | theorem | | ⊢ |
| proveit.numbers.ordering.less_eq_add_right_strong |
377 | instantiation | 400, 502, 472, 401, 402, 403, 404* | ⊢ |
| : , : , : |
378 | theorem | | ⊢ |
| proveit.numbers.numerals.decimals.less_0_1 |
379 | theorem | | ⊢ |
| proveit.numbers.addition.subtraction.subtract_from_add |
380 | theorem | | ⊢ |
| proveit.numbers.numerals.decimals.add_1_1 |
381 | instantiation | 405, 406, 511, 504, 407, 408, 411, 417, 409 | ⊢ |
| : , : , : , : , : , : |
382 | instantiation | 410, 417, 411, 412 | ⊢ |
| : , : , : |
383 | instantiation | 509, 414, 413 | ⊢ |
| : , : , : |
384 | instantiation | 509, 414, 415 | ⊢ |
| : , : , : |
385 | instantiation | 416, 417, 469, 418* | ⊢ |
| : , : |
386 | theorem | | ⊢ |
| proveit.numbers.absolute_value.abs_even |
387 | theorem | | ⊢ |
| proveit.numbers.number_sets.real_numbers.interval_co_lower_bound |
388 | instantiation | 419, 420, 448, 421 | ⊢ |
| : , : , : |
389 | theorem | | ⊢ |
| proveit.numbers.absolute_value.abs_non_neg_elim |
390 | instantiation | 422, 423 | ⊢ |
| : , : |
391 | instantiation | 509, 424, 425 | ⊢ |
| : , : , : |
392 | instantiation | 475, 511, 426, 427, 428, 429 | ⊢ |
| : , : , : , : |
393 | instantiation | 430, 431, 432 | ⊢ |
| : |
394 | instantiation | 509, 434, 433 | ⊢ |
| : , : , : |
395 | theorem | | ⊢ |
| proveit.numbers.number_sets.complex_numbers.real_nonzero_within_complex_nonzero |
396 | instantiation | 509, 434, 435 | ⊢ |
| : , : , : |
397 | instantiation | 461, 478 | ⊢ |
| : , : , : |
398 | instantiation | 453, 436, 437 | ⊢ |
| : , : , : |
399 | instantiation | 509, 510, 438 | ⊢ |
| : , : , : |
400 | theorem | | ⊢ |
| proveit.numbers.exponentiation.exp_monotonicity_large_base_less_eq |
401 | instantiation | 466, 467, 440 | ⊢ |
| : , : , : |
402 | theorem | | ⊢ |
| proveit.numbers.numerals.decimals.less_1_2 |
403 | instantiation | 439, 440 | ⊢ |
| : |
404 | instantiation | 441, 495 | ⊢ |
| : |
405 | theorem | | ⊢ |
| proveit.numbers.addition.disassociation |
406 | axiom | | ⊢ |
| proveit.numbers.number_sets.natural_numbers.zero_in_nats |
407 | theorem | | ⊢ |
| proveit.core_expr_types.tuples.tuple_len_0_typical_eq |
408 | instantiation | 492 | ⊢ |
| : , : |
409 | instantiation | 509, 501, 442 | ⊢ |
| : , : , : |
410 | theorem | | ⊢ |
| proveit.numbers.addition.subtraction.add_cancel_triple_23 |
411 | instantiation | 509, 501, 443 | ⊢ |
| : , : , : |
412 | instantiation | 444 | ⊢ |
| : |
413 | theorem | | ⊢ |
| proveit.numbers.number_sets.real_numbers.pi_is_real_pos |
414 | theorem | | ⊢ |
| proveit.numbers.number_sets.real_numbers.real_pos_within_real |
415 | instantiation | 445, 446 | ⊢ |
| : |
416 | theorem | | ⊢ |
| proveit.numbers.multiplication.mult_neg_left |
417 | instantiation | 509, 501, 472 | ⊢ |
| : , : , : |
418 | instantiation | 493, 469 | ⊢ |
| : |
419 | theorem | | ⊢ |
| proveit.numbers.number_sets.real_numbers.interval_co_upper_bound |
420 | instantiation | 447, 448 | ⊢ |
| : |
421 | theorem | | ⊢ |
| proveit.physics.quantum.QPE._scaled_delta_b_round_in_interval |
422 | theorem | | ⊢ |
| proveit.numbers.ordering.relax_less |
423 | instantiation | 449, 484 | ⊢ |
| : |
424 | theorem | | ⊢ |
| proveit.numbers.number_sets.rational_numbers.rational_pos_within_rational |
425 | instantiation | 450, 451, 452 | ⊢ |
| : , : |
426 | instantiation | 492 | ⊢ |
| : , : |
427 | instantiation | 492 | ⊢ |
| : , : |
428 | instantiation | 453, 454, 455 | ⊢ |
| : , : , : |
429 | theorem | | ⊢ |
| proveit.numbers.numerals.decimals.mult_2_2 |
430 | theorem | | ⊢ |
| proveit.numbers.division.frac_cancel_complete |
431 | instantiation | 509, 501, 456 | ⊢ |
| : , : , : |
432 | instantiation | 490, 457 | ⊢ |
| : |
433 | instantiation | 509, 459, 458 | ⊢ |
| : , : , : |
434 | theorem | | ⊢ |
| proveit.numbers.number_sets.real_numbers.rational_nonzero_within_real_nonzero |
435 | instantiation | 509, 459, 460 | ⊢ |
| : , : , : |
436 | instantiation | 461, 479 | ⊢ |
| : , : , : |
437 | instantiation | 462, 495 | ⊢ |
| : |
438 | instantiation | 463, 464, 504 | ⊢ |
| : , : |
439 | theorem | | ⊢ |
| proveit.numbers.number_sets.natural_numbers.natural_pos_lower_bound |
440 | axiom | | ⊢ |
| proveit.physics.quantum.QPE._t_in_natural_pos |
441 | theorem | | ⊢ |
| proveit.numbers.exponentiation.complex_x_to_first_power_is_x |
442 | instantiation | 509, 505, 465 | ⊢ |
| : , : , : |
443 | instantiation | 466, 467, 484 | ⊢ |
| : , : , : |
444 | axiom | | ⊢ |
| proveit.logic.equality.equals_reflexivity |
445 | theorem | | ⊢ |
| proveit.numbers.absolute_value.abs_nonzero_closure |
446 | instantiation | 468, 469, 470 | ⊢ |
| : |
447 | theorem | | ⊢ |
| proveit.numbers.negation.real_closure |
448 | instantiation | 471, 472, 502, 473 | ⊢ |
| : , : |
449 | theorem | | ⊢ |
| proveit.numbers.number_sets.natural_numbers.natural_pos_is_pos |
450 | theorem | | ⊢ |
| proveit.numbers.division.div_rational_pos_closure |
451 | instantiation | 509, 474, 481 | ⊢ |
| : , : , : |
452 | instantiation | 509, 474, 491 | ⊢ |
| : , : , : |
453 | axiom | | ⊢ |
| proveit.logic.equality.equals_transitivity |
454 | instantiation | 475, 511, 476, 477, 478, 479 | ⊢ |
| : , : , : , : |
455 | theorem | | ⊢ |
| proveit.numbers.numerals.decimals.add_2_2 |
456 | instantiation | 509, 505, 480 | ⊢ |
| : , : , : |
457 | theorem | | ⊢ |
| proveit.numbers.numerals.decimals.posnat4 |
458 | instantiation | 509, 482, 481 | ⊢ |
| : , : , : |
459 | theorem | | ⊢ |
| proveit.numbers.number_sets.rational_numbers.nonzero_int_within_rational_nonzero |
460 | instantiation | 509, 482, 491 | ⊢ |
| : , : , : |
461 | axiom | | ⊢ |
| proveit.logic.equality.substitution |
462 | theorem | | ⊢ |
| proveit.numbers.division.frac_one_denom |
463 | theorem | | ⊢ |
| proveit.numbers.addition.add_nat_closure_bin |
464 | instantiation | 509, 483, 484 | ⊢ |
| : , : , : |
465 | instantiation | 509, 507, 485 | ⊢ |
| : , : , : |
466 | theorem | | ⊢ |
| proveit.logic.sets.inclusion.unfold_subset_eq |
467 | instantiation | 486, 487 | ⊢ |
| : , : |
468 | theorem | | ⊢ |
| proveit.numbers.number_sets.complex_numbers.nonzero_complex_is_complex_nonzero |
469 | instantiation | 509, 501, 488 | ⊢ |
| : , : , : |
470 | assumption | | ⊢ |
471 | theorem | | ⊢ |
| proveit.numbers.division.div_real_closure |
472 | instantiation | 509, 505, 489 | ⊢ |
| : , : , : |
473 | instantiation | 490, 491 | ⊢ |
| : |
474 | theorem | | ⊢ |
| proveit.numbers.number_sets.rational_numbers.nat_pos_within_rational_pos |
475 | axiom | | ⊢ |
| proveit.core_expr_types.operations.operands_substitution |
476 | instantiation | 492 | ⊢ |
| : , : |
477 | instantiation | 492 | ⊢ |
| : , : |
478 | instantiation | 493, 495 | ⊢ |
| : |
479 | instantiation | 494, 495 | ⊢ |
| : |
480 | instantiation | 509, 507, 496 | ⊢ |
| : , : , : |
481 | theorem | | ⊢ |
| proveit.numbers.numerals.decimals.posnat1 |
482 | theorem | | ⊢ |
| proveit.numbers.number_sets.integers.nat_pos_within_nonzero_int |
483 | theorem | | ⊢ |
| proveit.numbers.number_sets.natural_numbers.nat_pos_within_nat |
484 | theorem | | ⊢ |
| proveit.physics.quantum.QPE._two_pow_t_is_nat_pos |
485 | instantiation | 497, 500 | ⊢ |
| : |
486 | theorem | | ⊢ |
| proveit.logic.sets.inclusion.relax_proper_subset |
487 | theorem | | ⊢ |
| proveit.numbers.number_sets.real_numbers.nat_pos_within_real |
488 | instantiation | 498, 499 | ⊢ |
| : |
489 | instantiation | 509, 507, 500 | ⊢ |
| : , : , : |
490 | theorem | | ⊢ |
| proveit.numbers.number_sets.natural_numbers.nonzero_if_is_nat_pos |
491 | theorem | | ⊢ |
| proveit.numbers.numerals.decimals.posnat2 |
492 | theorem | | ⊢ |
| proveit.numbers.numerals.decimals.tuple_len_2_typical_eq |
493 | theorem | | ⊢ |
| proveit.numbers.multiplication.elim_one_left |
494 | theorem | | ⊢ |
| proveit.numbers.multiplication.elim_one_right |
495 | instantiation | 509, 501, 502 | ⊢ |
| : , : , : |
496 | instantiation | 509, 510, 503 | ⊢ |
| : , : , : |
497 | theorem | | ⊢ |
| proveit.numbers.negation.int_closure |
498 | theorem | | ⊢ |
| proveit.physics.quantum.QPE._delta_b_is_real |
499 | theorem | | ⊢ |
| proveit.physics.quantum.QPE._best_round_is_int |
500 | instantiation | 509, 510, 504 | ⊢ |
| : , : , : |
501 | theorem | | ⊢ |
| proveit.numbers.number_sets.complex_numbers.real_within_complex |
502 | instantiation | 509, 505, 506 | ⊢ |
| : , : , : |
503 | theorem | | ⊢ |
| proveit.numbers.numerals.decimals.nat4 |
504 | theorem | | ⊢ |
| proveit.numbers.numerals.decimals.nat1 |
505 | theorem | | ⊢ |
| proveit.numbers.number_sets.real_numbers.rational_within_real |
506 | instantiation | 509, 507, 508 | ⊢ |
| : , : , : |
507 | theorem | | ⊢ |
| proveit.numbers.number_sets.rational_numbers.int_within_rational |
508 | instantiation | 509, 510, 511 | ⊢ |
| : , : , : |
509 | theorem | | ⊢ |
| proveit.logic.sets.inclusion.superset_membership_from_proper_subset |
510 | theorem | | ⊢ |
| proveit.numbers.number_sets.integers.nat_within_int |
511 | theorem | | ⊢ |
| proveit.numbers.numerals.decimals.nat2 |
*equality replacement requirements |