logo

Show the Proof

In [1]:
import proveit
# Automation is not needed when only showing a stored proof:
proveit.defaults.automation = False # This will speed things up.
proveit.defaults.inline_pngs = False # Makes files smaller.
%show_proof
Out[1]:
 step typerequirementsstatement
0instantiation1, 2, 3  ⊢  
  : , : , :
1reference26  ⊢  
2instantiation4, 404  ⊢  
  :
3instantiation359, 5, 6, 7*  ⊢  
  : , : , :
4theorem  ⊢  
 proveit.physics.quantum.QPE._failure_upper_bound_lemma
5instantiation359, 8, 9  ⊢  
  : , : , :
6instantiation10, 387, 369, 11  ⊢  
  : , : , : , :
7instantiation294, 12, 13  ⊢  
  : , : , :
8instantiation359, 14, 15  ⊢  
  : , : , :
9instantiation16, 341, 342, 17*, 18*, 19*  ⊢  
  : , : , : , :
10theorem  ⊢  
 proveit.numbers.summation.sum_split_first
11instantiation359, 20, 21  ⊢  
  : , : , :
12instantiation145, 22  ⊢  
  : , : , :
13instantiation151, 405, 415, 334, 23, 335, 72, 24, 95, 25*  ⊢  
  : , : , : , : , : , :
14instantiation26, 27, 28  ⊢  
  : , : , :
15instantiation29, 368, 407, 381, 30*, 31*  ⊢  
  : , : , : , : , :
16theorem  ⊢  
 proveit.numbers.summation.index_negate
17instantiation179, 32  ⊢  
  :
18instantiation33, 34, 373, 35*  ⊢  
  : , :
19instantiation36, 37, 405, 165*,  ⊢  
  : , :
20instantiation38, 346, 39, 383, 40, 395  ⊢  
  : , : , :
21instantiation294, 41, 42  ⊢  
  : , : , :
22instantiation294, 43, 44  ⊢  
  : , : , :
23instantiation349  ⊢  
  : , :
24instantiation45, 351, 183  ⊢  
  : , :
25instantiation294, 46, 47  ⊢  
  : , : , :
26theorem  ⊢  
 proveit.numbers.ordering.transitivity_less_eq_less_eq
27instantiation50, 97, 48, 51, 49, 54  ⊢  
  : , : , :
28instantiation50, 97, 51, 52, 53, 54  ⊢  
  : , : , :
29theorem  ⊢  
 proveit.numbers.summation.index_shift
30instantiation294, 55, 56  ⊢  
  : , : , :
31instantiation294, 57, 58,  ⊢  
  : , : , :
32instantiation413, 382, 59  ⊢  
  : , : , :
33theorem  ⊢  
 proveit.numbers.negation.distribute_neg_through_binary_sum
34instantiation413, 382, 60  ⊢  
  : , : , :
35instantiation179, 64  ⊢  
  :
36theorem  ⊢  
 proveit.numbers.exponentiation.even_pow_is_even_fn
37instantiation413, 382, 279,  ⊢  
  : , : , :
38theorem  ⊢  
 proveit.numbers.ordering.less_eq_add_right_strong
39instantiation413, 391, 61  ⊢  
  : , : , :
40instantiation321, 402, 403, 404  ⊢  
  : , : , :
41instantiation121, 334, 415, 405, 335, 62, 64, 127, 373  ⊢  
  : , : , : , : , : , :
42instantiation93, 405, 415, 334, 63, 335, 64, 127, 373, 65*  ⊢  
  : , : , : , : , : , :
43instantiation121, 405, 415, 334, 66, 335, 183, 95  ⊢  
  : , : , : , : , : , :
44instantiation294, 67, 68  ⊢  
  : , : , :
45theorem  ⊢  
 proveit.numbers.multiplication.mult_complex_closure_bin
46instantiation314, 405, 415, 334, 69, 335, 72, 351, 183  ⊢  
  : , : , : , : , : , :
47instantiation70, 334, 415, 405, 335, 71, 72, 351, 183, 73*  ⊢  
  : , : , : , : , : , :
48instantiation286, 75, 78  ⊢  
  : , :
49instantiation74, 78, 75, 77, 76  ⊢  
  : , : , :
50theorem  ⊢  
 proveit.numbers.multiplication.weak_bound_via_right_factor_bound
51instantiation286, 77, 78  ⊢  
  : , :
52instantiation286, 77, 79  ⊢  
  : , :
53instantiation232, 77, 78, 79, 80  ⊢  
  : , : , :
54instantiation290, 81  ⊢  
  : , :
55instantiation121, 334, 415, 405, 335, 82, 83, 373, 315  ⊢  
  : , : , : , : , : , :
56instantiation123, 373, 83, 125  ⊢  
  : , : , :
57instantiation145, 84  ⊢  
  : , : , :
58instantiation294, 85, 86,  ⊢  
  : , : , :
59instantiation413, 391, 87  ⊢  
  : , : , :
60instantiation413, 391, 88  ⊢  
  : , : , :
61instantiation413, 399, 403  ⊢  
  : , : , :
62instantiation349  ⊢  
  : , :
63instantiation349  ⊢  
  : , :
64instantiation413, 382, 89  ⊢  
  : , : , :
65instantiation359, 90, 91  ⊢  
  : , : , :
66instantiation349  ⊢  
  : , :
67instantiation92, 405, 334, 335, 183, 95  ⊢  
  : , : , : , : , : , : , :
68instantiation93, 334, 415, 405, 335, 94, 183, 95, 96*  ⊢  
  : , : , : , : , : , :
69instantiation349  ⊢  
  : , :
70theorem  ⊢  
 proveit.numbers.multiplication.association
71instantiation349  ⊢  
  : , :
72instantiation413, 382, 97  ⊢  
  : , : , :
73instantiation98, 373, 351, 99, 100, 101*, 102*  ⊢  
  : , : , : , :
74theorem  ⊢  
 proveit.numbers.addition.weak_bound_via_left_term_bound
75modus ponens103, 104  ⊢  
76modus ponens105, 106  ⊢  
77modus ponens107, 108  ⊢  
78modus ponens109, 110  ⊢  
79modus ponens111, 112  ⊢  
80modus ponens113, 114  ⊢  
81instantiation115, 155  ⊢  
  :
82instantiation349  ⊢  
  : , :
83instantiation413, 382, 346  ⊢  
  : , : , :
84instantiation116, 320, 117, 118, 119, 120  ⊢  
  : , : , :
85instantiation121, 334, 415, 405, 335, 122, 124, 373, 315,  ⊢  
  : , : , : , : , : , :
86instantiation123, 373, 124, 125,  ⊢  
  : , : , :
87instantiation413, 399, 368  ⊢  
  : , : , :
88instantiation413, 399, 357  ⊢  
  : , : , :
89instantiation376, 377, 410  ⊢  
  : , : , :
90instantiation126, 373, 351, 131  ⊢  
  : , : , :
91instantiation372, 373, 127  ⊢  
  : , :
92theorem  ⊢  
 proveit.numbers.addition.leftward_commutation
93theorem  ⊢  
 proveit.numbers.addition.association
94instantiation349  ⊢  
  : , :
95instantiation413, 382, 128  ⊢  
  : , : , :
96instantiation129, 130, 131*  ⊢  
  : , :
97instantiation413, 391, 132  ⊢  
  : , : , :
98theorem  ⊢  
 proveit.numbers.division.prod_of_fracs
99instantiation413, 190, 133  ⊢  
  : , : , :
100instantiation413, 190, 134  ⊢  
  : , : , :
101instantiation135, 351  ⊢  
  :
102instantiation294, 136, 137  ⊢  
  : , : , :
103instantiation242  ⊢  
  : , : , :
104generalization138  ⊢  
105instantiation143  ⊢  
  : , : , :
106generalization139  ⊢  
107instantiation242  ⊢  
  : , : , :
108generalization140  ⊢  
109instantiation242  ⊢  
  : , : , :
110generalization141  ⊢  
111instantiation242  ⊢  
  : , : , :
112generalization142  ⊢  
113instantiation143  ⊢  
  : , : , :
114generalization144  ⊢  
115theorem  ⊢  
 proveit.numbers.number_sets.rational_numbers.positive_if_in_rational_pos
116theorem  ⊢  
 proveit.core_expr_types.tuples.tuple_eq_via_elem_eq
117instantiation349  ⊢  
  : , :
118instantiation349  ⊢  
  : , :
119instantiation145, 146  ⊢  
  : , : , :
120instantiation215  ⊢  
  :
121theorem  ⊢  
 proveit.numbers.addition.disassociation
122instantiation349  ⊢  
  : , :
123theorem  ⊢  
 proveit.numbers.addition.subtraction.add_cancel_triple_23
124instantiation413, 382, 147,  ⊢  
  : , : , :
125instantiation215  ⊢  
  :
126theorem  ⊢  
 proveit.numbers.addition.subtraction.subtract_from_add_reversed
127instantiation413, 382, 148  ⊢  
  : , : , :
128instantiation259, 383, 149, 150  ⊢  
  : , :
129theorem  ⊢  
 proveit.logic.equality.equals_reversal
130instantiation151, 334, 415, 405, 335, 152, 373, 183, 153*  ⊢  
  : , : , : , : , : , :
131theorem  ⊢  
 proveit.numbers.numerals.decimals.add_1_1
132instantiation413, 154, 155  ⊢  
  : , : , :
133instantiation413, 211, 156  ⊢  
  : , : , :
134instantiation413, 211, 157  ⊢  
  : , : , :
135theorem  ⊢  
 proveit.numbers.division.frac_one_denom
136instantiation158, 415, 159, 160, 161, 162  ⊢  
  : , : , : , :
137instantiation163, 164, 373, 165*, 166*  ⊢  
  : , : , :
138instantiation259, 383, 167, 168,  ⊢  
  : , :
139instantiation169, 170, 216, 212, 171,  ⊢  
  : , : , :
140instantiation259, 383, 172, 173,  ⊢  
  : , :
141instantiation259, 383, 174, 175,  ⊢  
  : , :
142instantiation259, 383, 176, 177,  ⊢  
  : , :
143theorem  ⊢  
 proveit.numbers.summation.weak_summation_from_summands_bound
144instantiation290, 178,  ⊢  
  : , :
145axiom  ⊢  
 proveit.logic.equality.substitution
146instantiation179, 373  ⊢  
  :
147instantiation413, 391, 180,  ⊢  
  : , : , :
148instantiation413, 391, 181  ⊢  
  : , : , :
149instantiation278, 346, 415  ⊢  
  : , :
150instantiation280, 182, 282  ⊢  
  : , :
151theorem  ⊢  
 proveit.numbers.multiplication.distribute_through_sum
152instantiation349  ⊢  
  : , :
153instantiation188, 183  ⊢  
  :
154theorem  ⊢  
 proveit.numbers.number_sets.rational_numbers.rational_pos_within_rational
155instantiation184, 219, 185  ⊢  
  : , :
156instantiation413, 299, 186  ⊢  
  : , : , :
157instantiation413, 299, 187  ⊢  
  : , : , :
158axiom  ⊢  
 proveit.core_expr_types.operations.operands_substitution
159instantiation349  ⊢  
  : , :
160instantiation349  ⊢  
  : , :
161instantiation188, 351  ⊢  
  :
162instantiation313, 189  ⊢  
  :
163theorem  ⊢  
 proveit.numbers.division.frac_cancel_left
164instantiation413, 190, 191  ⊢  
  : , : , :
165instantiation313, 351  ⊢  
  :
166theorem  ⊢  
 proveit.numbers.numerals.decimals.mult_2_2
167instantiation278, 245, 415,  ⊢  
  : , :
168instantiation199, 192,  ⊢  
  :
169theorem  ⊢  
 proveit.numbers.division.weak_div_from_denom_bound__all_pos
170instantiation413, 193, 194  ⊢  
  : , : , :
171instantiation195, 362, 245, 266, 196, 197,  ⊢  
  : , : , :
172instantiation278, 266, 415,  ⊢  
  : , :
173instantiation199, 198,  ⊢  
  :
174instantiation278, 268, 415,  ⊢  
  : , :
175instantiation199, 200,  ⊢  
  :
176instantiation278, 223, 415,  ⊢  
  : , :
177instantiation201, 239,  ⊢  
  :
178instantiation202, 203, 204, 218, 205,  ⊢  
  : , : , :
179theorem  ⊢  
 proveit.numbers.negation.double_negation
180instantiation413, 399, 206,  ⊢  
  : , : , :
181instantiation413, 399, 408  ⊢  
  : , : , :
182instantiation413, 299, 207  ⊢  
  : , : , :
183instantiation413, 382, 208  ⊢  
  : , : , :
184theorem  ⊢  
 proveit.numbers.division.div_rational_pos_closure
185instantiation413, 238, 209  ⊢  
  : , : , :
186instantiation413, 319, 209  ⊢  
  : , : , :
187instantiation413, 319, 398  ⊢  
  : , : , :
188theorem  ⊢  
 proveit.numbers.multiplication.elim_one_left
189instantiation413, 382, 210  ⊢  
  : , : , :
190theorem  ⊢  
 proveit.numbers.number_sets.complex_numbers.real_nonzero_within_complex_nonzero
191instantiation413, 211, 282  ⊢  
  : , : , :
192instantiation413, 217, 212,  ⊢  
  : , : , :
193theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.rational_nonneg_within_real_nonneg
194instantiation413, 213, 405  ⊢  
  : , : , :
195theorem  ⊢  
 proveit.numbers.exponentiation.exp_even_neg_base_lesseq
196instantiation240, 214, 283,  ⊢  
  : , :
197instantiation215  ⊢  
  :
198instantiation413, 217, 216,  ⊢  
  : , : , :
199theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.nonzero_if_in_real_nonzero
200instantiation413, 217, 218,  ⊢  
  : , : , :
201theorem  ⊢  
 proveit.numbers.number_sets.natural_numbers.nonzero_if_is_nat_pos
202theorem  ⊢  
 proveit.numbers.division.strong_div_from_denom_bound__all_pos
203instantiation413, 220, 219  ⊢  
  : , : , :
204instantiation413, 220, 221,  ⊢  
  : , : , :
205instantiation222, 362, 223, 268, 224, 225,  ⊢  
  : , : , :
206instantiation413, 226, 227,  ⊢  
  : , : , :
207instantiation413, 319, 380  ⊢  
  : , : , :
208modus ponens228, 229  ⊢  
209theorem  ⊢  
 proveit.numbers.numerals.decimals.posnat4
210instantiation413, 391, 230  ⊢  
  : , : , :
211theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.rational_nonzero_within_real_nonzero
212instantiation236, 245, 231,  ⊢  
  :
213theorem  ⊢  
 proveit.numbers.number_sets.rational_numbers.nat_within_rational_nonneg
214instantiation232, 266, 288, 345, 233, 234*,  ⊢  
  : , : , :
215axiom  ⊢  
 proveit.logic.equality.equals_reflexivity
216instantiation236, 266, 235,  ⊢  
  :
217theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.real_pos_within_real_nonzero
218instantiation236, 268, 237,  ⊢  
  :
219instantiation413, 238, 398  ⊢  
  : , : , :
220theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.rational_pos_within_real_pos
221instantiation413, 238, 239,  ⊢  
  : , : , :
222theorem  ⊢  
 proveit.numbers.exponentiation.exp_pos_less
223instantiation286, 287, 274,  ⊢  
  : , :
224instantiation240, 272, 241,  ⊢  
  : , :
225instantiation366, 320  ⊢  
  :
226instantiation400, 387, 369  ⊢  
  : , :
227assumption  ⊢  
228instantiation242  ⊢  
  : , : , :
229generalization243  ⊢  
230instantiation413, 399, 244  ⊢  
  : , : , :
231instantiation267, 245, 345, 246,  ⊢  
  : , :
232theorem  ⊢  
 proveit.numbers.addition.weak_bound_via_right_term_bound
233instantiation247, 274, 345, 308, 284, 248, 277*, 249*  ⊢  
  : , : , :
234instantiation371, 250,  ⊢  
  :
235instantiation251, 305, 252, 283,  ⊢  
  : , :
236theorem  ⊢  
 proveit.numbers.exponentiation.sqrd_pos_closure
237instantiation253, 254,  ⊢  
  : , :
238theorem  ⊢  
 proveit.numbers.number_sets.rational_numbers.nat_pos_within_rational_pos
239instantiation255, 256, 415,  ⊢  
  : , :
240theorem  ⊢  
 proveit.logic.booleans.conjunction.and_if_both
241instantiation257, 287, 274, 288, 258,  ⊢  
  : , : , :
242theorem  ⊢  
 proveit.numbers.summation.summation_real_closure
243instantiation259, 383, 260, 261,  ⊢  
  : , :
244instantiation413, 414, 262  ⊢  
  : , : , :
245instantiation286, 266, 288,  ⊢  
  : , :
246instantiation263, 264,  ⊢  
  : , :
247theorem  ⊢  
 proveit.numbers.multiplication.reversed_weak_bound_via_right_factor_bound
248instantiation290, 275  ⊢  
  : , :
249instantiation265, 315  ⊢  
  :
250instantiation413, 382, 266,  ⊢  
  : , : , :
251theorem  ⊢  
 proveit.numbers.ordering.less_is_not_eq_int
252theorem  ⊢  
 proveit.numbers.number_sets.integers.zero_is_int
253theorem  ⊢  
 proveit.logic.equality.not_equals_symmetry
254instantiation267, 345, 268, 269,  ⊢  
  : , :
255theorem  ⊢  
 proveit.numbers.exponentiation.exp_natpos_closure
256instantiation270, 271, 272,  ⊢  
  :
257theorem  ⊢  
 proveit.numbers.addition.strong_bound_via_right_term_bound
258instantiation273, 274, 308, 383, 310, 275, 276*, 277*  ⊢  
  : , : , :
259theorem  ⊢  
 proveit.numbers.division.div_real_closure
260instantiation278, 279, 415,  ⊢  
  : , :
261instantiation280, 281, 282,  ⊢  
  : , :
262theorem  ⊢  
 proveit.numbers.numerals.decimals.nat4
263theorem  ⊢  
 proveit.numbers.addition.subtraction.neg_difference
264instantiation394, 283, 284,  ⊢  
  : , : , :
265theorem  ⊢  
 proveit.numbers.multiplication.mult_zero_right
266instantiation413, 391, 285,  ⊢  
  : , : , :
267theorem  ⊢  
 proveit.numbers.ordering.less_is_not_eq
268instantiation286, 287, 288,  ⊢  
  : , :
269instantiation311, 289,  ⊢  
  : , :
270theorem  ⊢  
 proveit.numbers.number_sets.integers.nonneg_int_is_natural
271instantiation406, 326, 381,  ⊢  
  : , :
272instantiation290, 291,  ⊢  
  : , :
273theorem  ⊢  
 proveit.numbers.multiplication.reversed_strong_bound_via_right_factor_bound
274instantiation307, 383  ⊢  
  :
275instantiation322, 390  ⊢  
  :
276instantiation292, 373, 293*  ⊢  
  : , :
277instantiation294, 295, 296  ⊢  
  : , : , :
278theorem  ⊢  
 proveit.numbers.exponentiation.exp_real_closure_nat_power
279instantiation413, 391, 297,  ⊢  
  : , : , :
280theorem  ⊢  
 proveit.numbers.exponentiation.exp_rational_non_zero__not_zero
281instantiation413, 299, 298,  ⊢  
  : , : , :
282instantiation413, 299, 300  ⊢  
  : , : , :
283instantiation301, 302, 303,  ⊢  
  : , : , :
284instantiation304, 345, 383, 329  ⊢  
  : , : , :
285instantiation413, 399, 305,  ⊢  
  : , : , :
286theorem  ⊢  
 proveit.numbers.addition.add_real_closure_bin
287instantiation413, 391, 306,  ⊢  
  : , : , :
288instantiation307, 308  ⊢  
  :
289instantiation309, 310, 312,  ⊢  
  : , : , :
290theorem  ⊢  
 proveit.numbers.ordering.relax_less
291instantiation311, 312,  ⊢  
  : , :
292theorem  ⊢  
 proveit.numbers.multiplication.mult_neg_left
293instantiation313, 373  ⊢  
  :
294axiom  ⊢  
 proveit.logic.equality.equals_transitivity
295instantiation314, 405, 415, 334, 336, 335, 315, 337, 338  ⊢  
  : , : , : , : , : , :
296instantiation316, 334, 415, 335, 336, 373, 337, 338, 317*  ⊢  
  : , : , : , : , :
297instantiation413, 399, 339,  ⊢  
  : , : , :
298instantiation413, 319, 318,  ⊢  
  : , : , :
299theorem  ⊢  
 proveit.numbers.number_sets.rational_numbers.nonzero_int_within_rational_nonzero
300instantiation413, 319, 320  ⊢  
  : , : , :
301theorem  ⊢  
 proveit.numbers.ordering.transitivity_less_eq_less
302instantiation321, 341, 342, 325,  ⊢  
  : , : , :
303instantiation322, 323  ⊢  
  :
304theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.interval_co_lower_bound
305instantiation413, 324, 325,  ⊢  
  : , : , :
306instantiation413, 399, 326,  ⊢  
  : , : , :
307theorem  ⊢  
 proveit.numbers.negation.real_closure
308instantiation327, 345, 383, 329  ⊢  
  : , : , :
309axiom  ⊢  
 proveit.numbers.ordering.transitivity_less_less
310instantiation328, 345, 383, 329  ⊢  
  : , : , :
311theorem  ⊢  
 proveit.numbers.addition.subtraction.pos_difference
312instantiation394, 330, 331,  ⊢  
  : , : , :
313theorem  ⊢  
 proveit.numbers.multiplication.elim_one_right
314theorem  ⊢  
 proveit.numbers.multiplication.disassociation
315instantiation332, 373  ⊢  
  :
316theorem  ⊢  
 proveit.numbers.multiplication.mult_neg_any
317instantiation333, 334, 415, 335, 336, 337, 338  ⊢  
  : , : , : , :
318instantiation386, 339, 340,  ⊢  
  :
319theorem  ⊢  
 proveit.numbers.number_sets.integers.nat_pos_within_nonzero_int
320theorem  ⊢  
 proveit.numbers.numerals.decimals.posnat2
321theorem  ⊢  
 proveit.numbers.number_sets.integers.interval_upper_bound
322theorem  ⊢  
 proveit.numbers.number_sets.integers.negative_if_in_neg_int
323instantiation397, 367  ⊢  
  :
324instantiation400, 341, 342  ⊢  
  : , :
325assumption  ⊢  
326instantiation413, 343, 348,  ⊢  
  : , : , :
327theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.all_in_interval_co__is__real
328theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.interval_co_upper_bound
329theorem  ⊢  
 proveit.physics.quantum.QPE._scaled_delta_b_floor_in_interval
330instantiation344, 383, 345, 346, 388, 347*  ⊢  
  : , : , :
331instantiation401, 368, 407, 348,  ⊢  
  : , : , :
332theorem  ⊢  
 proveit.numbers.negation.complex_closure
333theorem  ⊢  
 proveit.numbers.multiplication.elim_one_any
334axiom  ⊢  
 proveit.numbers.number_sets.natural_numbers.zero_in_nats
335theorem  ⊢  
 proveit.core_expr_types.tuples.tuple_len_0_typical_eq
336instantiation349  ⊢  
  : , :
337instantiation350, 351, 352  ⊢  
  : , :
338instantiation413, 382, 353  ⊢  
  : , : , :
339instantiation413, 354, 370,  ⊢  
  : , : , :
340instantiation394, 355, 356,  ⊢  
  : , : , :
341instantiation406, 357, 402  ⊢  
  : , :
342instantiation411, 368  ⊢  
  :
343instantiation400, 368, 407  ⊢  
  : , :
344theorem  ⊢  
 proveit.numbers.addition.strong_bound_via_left_term_bound
345theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.zero_is_real
346instantiation413, 391, 358  ⊢  
  : , : , :
347instantiation359, 360, 361  ⊢  
  : , : , :
348assumption  ⊢  
349theorem  ⊢  
 proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
350theorem  ⊢  
 proveit.numbers.exponentiation.exp_complex_closure
351instantiation413, 382, 362  ⊢  
  : , : , :
352instantiation413, 382, 363  ⊢  
  : , : , :
353instantiation364, 365  ⊢  
  :
354instantiation400, 368, 369  ⊢  
  : , :
355instantiation366, 367  ⊢  
  :
356instantiation401, 368, 369, 370,  ⊢  
  : , : , :
357instantiation411, 407  ⊢  
  :
358instantiation413, 399, 387  ⊢  
  : , : , :
359theorem  ⊢  
 proveit.logic.equality.sub_right_side_into
360instantiation371, 373  ⊢  
  :
361instantiation372, 373, 374  ⊢  
  : , :
362instantiation413, 391, 375  ⊢  
  : , : , :
363instantiation376, 377, 378  ⊢  
  : , : , :
364theorem  ⊢  
 proveit.physics.quantum.QPE._delta_b_is_real
365theorem  ⊢  
 proveit.physics.quantum.QPE._best_floor_is_int
366theorem  ⊢  
 proveit.numbers.number_sets.natural_numbers.natural_pos_is_pos
367instantiation379, 380, 398  ⊢  
  : , :
368instantiation406, 387, 402  ⊢  
  : , :
369instantiation406, 407, 381  ⊢  
  : , :
370assumption  ⊢  
371theorem  ⊢  
 proveit.numbers.addition.elim_zero_right
372theorem  ⊢  
 proveit.numbers.addition.commutation
373instantiation413, 382, 383  ⊢  
  : , : , :
374theorem  ⊢  
 proveit.numbers.number_sets.complex_numbers.zero_is_complex
375instantiation413, 399, 412  ⊢  
  : , : , :
376theorem  ⊢  
 proveit.logic.sets.inclusion.unfold_subset_eq
377instantiation384, 385  ⊢  
  : , :
378axiom  ⊢  
 proveit.physics.quantum.QPE._t_in_natural_pos
379theorem  ⊢  
 proveit.numbers.addition.add_nat_pos_closure_bin
380instantiation386, 387, 388  ⊢  
  :
381instantiation413, 389, 390  ⊢  
  : , : , :
382theorem  ⊢  
 proveit.numbers.number_sets.complex_numbers.real_within_complex
383instantiation413, 391, 392  ⊢  
  : , : , :
384theorem  ⊢  
 proveit.logic.sets.inclusion.relax_proper_subset
385theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.nat_pos_within_real
386theorem  ⊢  
 proveit.numbers.number_sets.integers.pos_int_is_natural_pos
387instantiation413, 393, 404  ⊢  
  : , : , :
388instantiation394, 395, 396  ⊢  
  : , : , :
389theorem  ⊢  
 proveit.numbers.number_sets.integers.neg_int_within_int
390instantiation397, 398  ⊢  
  :
391theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.rational_within_real
392instantiation413, 399, 402  ⊢  
  : , : , :
393instantiation400, 402, 403  ⊢  
  : , :
394theorem  ⊢  
 proveit.numbers.ordering.transitivity_less_less_eq
395theorem  ⊢  
 proveit.numbers.numerals.decimals.less_0_1
396instantiation401, 402, 403, 404  ⊢  
  : , : , :
397theorem  ⊢  
 proveit.numbers.negation.int_neg_closure
398theorem  ⊢  
 proveit.numbers.numerals.decimals.posnat1
399theorem  ⊢  
 proveit.numbers.number_sets.rational_numbers.int_within_rational
400theorem  ⊢  
 proveit.numbers.number_sets.integers.int_interval_within_int
401theorem  ⊢  
 proveit.numbers.number_sets.integers.interval_lower_bound
402instantiation413, 414, 405  ⊢  
  : , : , :
403instantiation406, 407, 408  ⊢  
  : , :
404assumption  ⊢  
405theorem  ⊢  
 proveit.numbers.numerals.decimals.nat1
406theorem  ⊢  
 proveit.numbers.addition.add_int_closure_bin
407instantiation413, 409, 410  ⊢  
  : , : , :
408instantiation411, 412  ⊢  
  :
409theorem  ⊢  
 proveit.numbers.number_sets.integers.nat_pos_within_int
410theorem  ⊢  
 proveit.physics.quantum.QPE._two_pow_t_minus_one_is_nat_pos
411theorem  ⊢  
 proveit.numbers.negation.int_closure
412instantiation413, 414, 415  ⊢  
  : , : , :
413theorem  ⊢  
 proveit.logic.sets.inclusion.superset_membership_from_proper_subset
414theorem  ⊢  
 proveit.numbers.number_sets.integers.nat_within_int
415theorem  ⊢  
 proveit.numbers.numerals.decimals.nat2
*equality replacement requirements