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