Proof of proveit.physics.quantum.QPE._delta_b_in_interval theorem

import proveit
theory = proveit.Theory() # the theorem's theory
from proveit import b, defaults
from proveit.logic import Forall, Set
from proveit.numbers import one, two, Add, Exp, frac, Less, LessEq, Neg, Mult
from proveit.physics.quantum.QPE import (
    _b_floor, _b_round, _best_floor_is_int, _best_round_is_int,
    _delta_b, _delta_b_floor, _delta_b_is_real, _delta_b_round,
    _scaled_delta_b_floor_in_interval, _scaled_delta_b_round_in_interval,
    _t, _t_in_natural_pos, _two_pow_t, _two_pow_t_is_nat_pos )

%proving _delta_b_in_interval

With these allowed/disallowed theorem/theory presumptions (e.g., to avoid circular dependencies), we begin our proof of
_delta_b_in_interval:
(see dependencies)

defaults.assumptions = _delta_b_in_interval.all_conditions()

defaults.assumptions:

_two_pow_t_is_nat_pos

 ⊢  

Derive interval and related bounds for $\delta_{b_f}$.

_scaled_delta_b_floor_in_interval

 ⊢  

_best_floor_is_int

 ⊢  

_delta_b_is_real

 ⊢  

_delta_b_f_is_real = _delta_b_is_real.instantiate({b: _b_floor})

_delta_b_f_is_real:  ⊢  

delta_b_f_interval_membership = (
        _scaled_delta_b_floor_in_interval.
        derive_rescaled_membership(frac(one, _two_pow_t)))

delta_b_f_interval_membership:  ⊢  

_t_in_natural_pos

 ⊢  

t_ge_one = _t_in_natural_pos.derive_element_lower_bound()

t_ge_one:  ⊢  

two_pow_t_ge_2 = _two_pow_t.deduce_bound(t_ge_one)

two_pow_t_ge_2:  ⊢  

one_over_two_pow_t_less_one_half = (
        frac(one, _two_pow_t).deduce_bound(two_pow_t_ge_2))

one_over_two_pow_t_less_one_half:  ⊢  

Now it knows that $0 \leq \delta_{b_f} \leq 1/2$ via automation which is stronger than $\delta_{b_f} \in \left(-1/2, 1/2\right]$.

Derive interval and related bounds for $\delta_{b_r}$.

_scaled_delta_b_round_in_interval

 ⊢  

_best_round_is_int

 ⊢  

_delta_b_is_real.instantiate({b: _b_round})

 ⊢  

with Mult.temporary_simplification_directives() as tmp_directives:
    tmp_directives.distribute_fractions = True
    delta_b_r_interval_membership = (
        _scaled_delta_b_round_in_interval.
        derive_rescaled_membership(frac(one, _two_pow_t)))

delta_b_r_interval_membership:  ⊢  

# for convenience
_two_pow__t_plus_one = delta_b_r_interval_membership.domain.upper_bound.denominator

_two_pow__t_plus_one:

t_less_t_plus_one = Less(_t, Add(one, _t)).prove()

t_less_t_plus_one:  ⊢  

_two_pow__t_plus_one_greater_two_pow_t = (
    _two_pow__t_plus_one.deduce_bound(t_less_t_plus_one.reversed()))

_two_pow__t_plus_one_greater_two_pow_t:  ⊢  

one_over_two_pow__t_plus_one_less_one_over_two_pow_t = (
        frac(one, Exp(two, Add(one, _t))).deduce_bound(
        _two_pow__t_plus_one_greater_two_pow_t))

one_over_two_pow__t_plus_one_less_one_over_two_pow_t:  ⊢  

And we have already established that $\frac{1}{2^t} < \frac{1}{2}$. Thus we know that $\delta_{b_r} < \frac{1}{2}$ via automation.

And it follows that $-\frac{1}{2}\le-\frac{1}{2^t}$, and thus $-\frac{1}{2}<\delta_{b_r}$ via automation.

%qed

proveit.physics.quantum.QPE._delta_b_in_interval has been proven.

	step type	requirements	statement
0	instantiation	1, 2, 3, 4, 5	⊢
	: , : , : , :
1	conjecture		⊢
	proveit.logic.sets.enumeration.true_for_each_then_true_for_all
2	reference	331	⊢
3	instantiation	270	⊢
	: , :
4	instantiation	7, 125, 243, 145, 6	⊢
	: , : , :
5	instantiation	7, 125, 243, 158, 8	⊢
	: , : , :
6	instantiation	11, 9, 10	⊢
	: , :
7	conjecture		⊢
	proveit.numbers.number_sets.real_numbers.in_IntervalOC
8	instantiation	11, 12, 13	⊢
	: , :
9	instantiation	28, 125, 58, 14, 15, 16*, 17*	⊢
	: , : , :
10	instantiation	169, 18	⊢
	: , :
11	theorem		⊢
	proveit.logic.booleans.conjunction.and_if_both
12	instantiation	35, 19, 20	⊢
	: , : , :
13	instantiation	169, 21	⊢
	: , :
14	instantiation	45, 145, 243	⊢
	: , :
15	instantiation	115, 58, 145, 243, 22, 170	⊢
	: , : , :
16	instantiation	185, 23, 24	⊢
	: , : , :
17	instantiation	266, 25, 26	⊢
	: , : , :
18	instantiation	35, 27, 143	⊢
	: , : , :
19	instantiation	28, 29, 116, 30, 94, 31*, 32*	⊢
	: , : , :
20	instantiation	33, 55, 72, 34	⊢
	: , : , :
21	instantiation	35, 36, 37	⊢
	: , : , :
22	instantiation	38, 58, 161, 44	⊢
	: , : , :
23	instantiation	39, 102	⊢
	:
24	instantiation	40, 102, 41	⊢
	: , :
25	instantiation	100, 216, 331, 334, 217, 42, 121, 219, 102	⊢
	: , : , : , : , : , :
26	instantiation	43, 219, 121, 105	⊢
	: , : , :
27	instantiation	54, 58, 161, 44	⊢
	: , : , :
28	conjecture		⊢
	proveit.numbers.addition.strong_bound_via_left_term_bound
29	instantiation	45, 125, 46	⊢
	: , :
30	instantiation	332, 319, 47	⊢
	: , : , :
31	instantiation	266, 48, 49	⊢
	: , : , :
32	instantiation	188, 50, 51, 52	⊢
	: , : , : , :
33	conjecture		⊢
	proveit.numbers.number_sets.real_numbers.interval_cc_lower_bound
34	instantiation	53, 55, 72, 56	⊢
	: , : , :
35	conjecture		⊢
	proveit.numbers.ordering.transitivity_less_less_eq
36	instantiation	54, 55, 72, 56	⊢
	: , : , :
37	instantiation	185, 57, 98	⊢
	: , : , :
38	conjecture		⊢
	proveit.numbers.number_sets.real_numbers.interval_co_lower_bound
39	conjecture		⊢
	proveit.numbers.addition.elim_zero_right
40	conjecture		⊢
	proveit.numbers.addition.commutation
41	conjecture		⊢
	proveit.numbers.number_sets.complex_numbers.zero_is_complex
42	instantiation	270	⊢
	: , :
43	conjecture		⊢
	proveit.numbers.addition.subtraction.add_cancel_triple_23
44	instantiation	73, 58, 309, 161, 59, 60*, 61*, 62*	⊢
	: , : , : , :
45	conjecture		⊢
	proveit.numbers.addition.add_real_closure_bin
46	instantiation	294, 116	⊢
	:
47	instantiation	63, 64, 141	⊢
	: , :
48	instantiation	266, 65, 66	⊢
	: , : , :
49	instantiation	266, 67, 68	⊢
	: , : , :
50	instantiation	266, 69, 70	⊢
	: , : , :
51	instantiation	127	⊢
	:
52	instantiation	150, 71	⊢
	: , :
53	conjecture		⊢
	proveit.numbers.number_sets.real_numbers.relax_IntervalCO
54	conjecture		⊢
	proveit.numbers.number_sets.real_numbers.interval_co_upper_bound
55	instantiation	294, 72	⊢
	:
56	instantiation	73, 125, 243, 161, 74, 75*, 76*, 93*	⊢
	: , : , : , :
57	instantiation	185, 77, 114	⊢
	: , : , :
58	conjecture		⊢
	proveit.numbers.number_sets.real_numbers.zero_is_real
59	conjecture		⊢
	proveit.physics.quantum.QPE._scaled_delta_b_floor_in_interval
60	instantiation	188, 78, 79, 80	⊢
	: , : , : , :
61	instantiation	81, 138	⊢
	:
62	instantiation	310, 138	⊢
	:
63	conjecture		⊢
	proveit.numbers.addition.add_rational_closure_bin
64	instantiation	162, 262	⊢
	: , :
65	instantiation	288, 149	⊢
	: , : , :
66	instantiation	288, 99	⊢
	: , : , :
67	instantiation	100, 334, 331, 216, 101, 217, 126, 102, 104	⊢
	: , : , : , : , : , :
68	instantiation	82, 126, 102, 83	⊢
	: , : , :
69	instantiation	266, 84, 85	⊢
	: , : , :
70	instantiation	266, 86, 87	⊢
	: , : , :
71	instantiation	288, 88	⊢
	: , : , :
72	instantiation	332, 319, 89	⊢
	: , : , :
73	conjecture		⊢
	proveit.numbers.number_sets.real_numbers.rescale_interval_co_membership
74	conjecture		⊢
	proveit.physics.quantum.QPE._scaled_delta_b_round_in_interval
75	instantiation	188, 90, 91, 92	⊢
	: , : , : , :
76	instantiation	296, 138, 219, 93*	⊢
	: , :
77	instantiation	169, 94	⊢
	: , :
78	instantiation	214, 334, 331, 216, 95, 217, 138, 306, 121	⊢
	: , : , : , : , : , :
79	instantiation	266, 96, 97	⊢
	: , : , :
80	instantiation	287, 121	⊢
	:
81	conjecture		⊢
	proveit.numbers.multiplication.mult_zero_right
82	conjecture		⊢
	proveit.numbers.addition.subtraction.add_cancel_triple_13
83	instantiation	127	⊢
	:
84	instantiation	288, 98	⊢
	: , : , :
85	instantiation	288, 99	⊢
	: , : , :
86	instantiation	100, 334, 331, 216, 101, 217, 219, 102, 104	⊢
	: , : , : , : , : , :
87	instantiation	103, 219, 104, 105	⊢
	: , : , :
88	instantiation	266, 106, 107	⊢
	: , : , :
89	instantiation	228, 320, 108, 109	⊢
	: , :
90	instantiation	214, 334, 331, 216, 110, 217, 138, 306, 135	⊢
	: , : , : , : , : , :
91	instantiation	266, 111, 112	⊢
	: , : , :
92	instantiation	287, 135	⊢
	:
93	instantiation	266, 113, 114	⊢
	: , : , :
94	instantiation	115, 116, 117, 118, 119, 120	⊢
	: , : , :
95	instantiation	270	⊢
	: , :
96	instantiation	133, 216, 331, 334, 217, 134, 138, 306, 121	⊢
	: , : , : , : , : , :
97	instantiation	288, 136	⊢
	: , : , :
98	instantiation	266, 122, 123	⊢
	: , : , :
99	instantiation	288, 124	⊢
	: , : , :
100	conjecture		⊢
	proveit.numbers.addition.disassociation
101	instantiation	270	⊢
	: , :
102	instantiation	332, 321, 125	⊢
	: , : , :
103	conjecture		⊢
	proveit.numbers.addition.subtraction.add_cancel_triple_12
104	instantiation	300, 126	⊢
	:
105	instantiation	127	⊢
	:
106	instantiation	288, 128	⊢
	: , : , :
107	instantiation	210, 297, 129, 130, 131*	⊢
	: , :
108	instantiation	332, 326, 132	⊢
	: , : , :
109	instantiation	295, 157	⊢
	:
110	instantiation	270	⊢
	: , :
111	instantiation	133, 216, 331, 334, 217, 134, 138, 306, 135	⊢
	: , : , : , : , : , :
112	instantiation	288, 136	⊢
	: , : , :
113	instantiation	137, 138, 219	⊢
	: , :
114	instantiation	172, 297, 241, 224, 191*, 151*	⊢
	: , : , : , :
115	conjecture		⊢
	proveit.numbers.ordering.less_eq_add_right_strong
116	instantiation	332, 319, 139	⊢
	: , : , :
117	instantiation	140, 243	⊢
	: , :
118	instantiation	332, 319, 141	⊢
	: , : , :
119	instantiation	142, 243, 161, 143, 144	⊢
	: , : , :
120	instantiation	201, 163	⊢
	:
121	instantiation	332, 321, 145	⊢
	: , : , :
122	instantiation	288, 146	⊢
	: , : , :
123	instantiation	147, 327, 318, 148*	⊢
	: , : , : , :
124	instantiation	288, 149	⊢
	: , : , :
125	instantiation	294, 243	⊢
	:
126	instantiation	152, 219, 258	⊢
	: , :
127	axiom		⊢
	proveit.logic.equality.equals_reflexivity
128	instantiation	150, 151	⊢
	: , :
129	instantiation	152, 279, 306	⊢
	: , :
130	instantiation	153, 331, 154, 241, 224	⊢
	: , :
131	instantiation	266, 155, 156	⊢
	: , : , :
132	instantiation	332, 269, 157	⊢
	: , : , :
133	conjecture		⊢
	proveit.numbers.multiplication.association
134	instantiation	270	⊢
	: , :
135	instantiation	332, 321, 158	⊢
	: , : , :
136	instantiation	185, 159, 160	⊢
	: , : , :
137	conjecture		⊢
	proveit.numbers.multiplication.commutation
138	instantiation	332, 321, 161	⊢
	: , : , :
139	instantiation	162, 262, 192	⊢
	: , :
140	conjecture		⊢
	proveit.numbers.multiplication.mult_real_closure_bin
141	instantiation	332, 283, 163	⊢
	: , : , :
142	conjecture		⊢
	proveit.numbers.multiplication.weak_bound_via_right_factor_bound
143	instantiation	164, 165, 166, 167, 168	⊢
	: , : , :
144	instantiation	169, 170	⊢
	: , :
145	instantiation	183, 171	⊢
	:
146	instantiation	172, 297, 241, 191*, 173*	⊢
	: , : , : , :
147	conjecture		⊢
	proveit.numbers.addition.rational_pair_addition
148	instantiation	266, 174, 175	⊢
	: , : , :
149	instantiation	288, 176	⊢
	: , : , :
150	theorem		⊢
	proveit.logic.equality.equals_reversal
151	instantiation	177, 279, 314, 330, 242*	⊢
	: , : , :
152	conjecture		⊢
	proveit.numbers.multiplication.mult_complex_closure_bin
153	conjecture		⊢
	proveit.numbers.multiplication.mult_not_eq_zero
154	instantiation	270	⊢
	: , :
155	instantiation	288, 178	⊢
	: , : , :
156	instantiation	266, 179, 180	⊢
	: , : , :
157	instantiation	181, 331, 182	⊢
	: , :
158	instantiation	183, 184	⊢
	:
159	instantiation	185, 186, 187	⊢
	: , : , :
160	instantiation	188, 189, 190, 191	⊢
	: , : , : , :
161	instantiation	332, 319, 192	⊢
	: , : , :
162	conjecture		⊢
	proveit.numbers.multiplication.mult_rational_closure_bin
163	instantiation	303, 304, 193	⊢
	: , :
164	conjecture		⊢
	proveit.numbers.division.weak_div_from_denom_bound__all_pos
165	instantiation	332, 194, 195	⊢
	: , : , :
166	instantiation	332, 196, 305	⊢
	: , : , :
167	instantiation	332, 196, 197	⊢
	: , : , :
168	instantiation	198, 299, 309, 322, 199, 200, 242*	⊢
	: , : , :
169	conjecture		⊢
	proveit.numbers.ordering.relax_less
170	instantiation	201, 284	⊢
	:
171	conjecture		⊢
	proveit.physics.quantum.QPE._best_floor_is_int
172	conjecture		⊢
	proveit.numbers.division.prod_of_fracs
173	conjecture		⊢
	proveit.numbers.numerals.decimals.mult_2_2
174	instantiation	250, 331, 202, 203, 204, 205	⊢
	: , : , : , :
175	instantiation	206, 207, 241, 297, 208*, 209*	⊢
	: , : , :
176	instantiation	210, 297, 306, 230, 211*	⊢
	: , :
177	conjecture		⊢
	proveit.numbers.exponentiation.product_of_posnat_powers
178	instantiation	212, 279, 306, 275, 276, 230, 213*, 257*	⊢
	: , : , :
179	instantiation	214, 334, 331, 216, 218, 217, 297, 219, 258	⊢
	: , : , : , : , : , :
180	instantiation	215, 216, 331, 217, 218, 219, 258	⊢
	: , : , : , :
181	conjecture		⊢
	proveit.numbers.exponentiation.exp_natpos_closure
182	instantiation	220, 334, 221	⊢
	: , :
183	conjecture		⊢
	proveit.physics.quantum.QPE._delta_b_is_real
184	conjecture		⊢
	proveit.physics.quantum.QPE._best_round_is_int
185	theorem		⊢
	proveit.logic.equality.sub_right_side_into
186	instantiation	222, 297, 223, 224	⊢
	: , : , : , : , :
187	instantiation	266, 225, 226	⊢
	: , : , :
188	conjecture		⊢
	proveit.logic.equality.four_chain_transitivity
189	instantiation	288, 227	⊢
	: , : , :
190	instantiation	288, 227	⊢
	: , : , :
191	instantiation	310, 297	⊢
	:
192	instantiation	228, 320, 229, 230	⊢
	: , :
193	instantiation	332, 315, 231	⊢
	: , : , :
194	conjecture		⊢
	proveit.numbers.number_sets.real_numbers.rational_nonneg_within_real_nonneg
195	instantiation	332, 232, 334	⊢
	: , : , :
196	conjecture		⊢
	proveit.numbers.number_sets.real_numbers.rational_pos_within_real_pos
197	instantiation	332, 315, 324	⊢
	: , : , :
198	conjecture		⊢
	proveit.numbers.exponentiation.exp_monotonicity_large_base_less_eq
199	conjecture		⊢
	proveit.numbers.numerals.decimals.less_1_2
200	instantiation	233, 330	⊢
	:
201	conjecture		⊢
	proveit.numbers.number_sets.rational_numbers.positive_if_in_rational_pos
202	instantiation	270	⊢
	: , :
203	instantiation	270	⊢
	: , :
204	instantiation	266, 234, 235	⊢
	: , : , :
205	conjecture		⊢
	proveit.numbers.numerals.decimals.mult_4_4
206	conjecture		⊢
	proveit.numbers.division.frac_cancel_left
207	instantiation	332, 259, 236	⊢
	: , : , :
208	instantiation	310, 237	⊢
	:
209	conjecture		⊢
	proveit.numbers.numerals.decimals.mult_8_2
210	conjecture		⊢
	proveit.numbers.division.div_as_mult
211	instantiation	266, 238, 239	⊢
	: , : , :
212	conjecture		⊢
	proveit.numbers.exponentiation.real_power_of_product
213	instantiation	240, 241, 314, 242*	⊢
	: , :
214	conjecture		⊢
	proveit.numbers.multiplication.disassociation
215	conjecture		⊢
	proveit.numbers.multiplication.elim_one_any
216	axiom		⊢
	proveit.numbers.number_sets.natural_numbers.zero_in_nats
217	conjecture		⊢
	proveit.core_expr_types.tuples.tuple_len_0_typical_eq
218	instantiation	270	⊢
	: , :
219	instantiation	332, 321, 243	⊢
	: , : , :
220	conjecture		⊢
	proveit.numbers.addition.add_nat_closure_bin
221	instantiation	332, 244, 330	⊢
	: , : , :
222	conjecture		⊢
	proveit.numbers.division.mult_frac_cancel_denom_left
223	instantiation	332, 259, 245	⊢
	: , : , :
224	instantiation	332, 259, 246	⊢
	: , : , :
225	instantiation	288, 247	⊢
	: , : , :
226	instantiation	288, 248	⊢
	: , : , :
227	instantiation	290, 297	⊢
	:
228	conjecture		⊢
	proveit.numbers.division.div_rational_closure
229	instantiation	332, 326, 249	⊢
	: , : , :
230	instantiation	295, 324	⊢
	:
231	conjecture		⊢
	proveit.numbers.numerals.decimals.posnat4
232	conjecture		⊢
	proveit.numbers.number_sets.rational_numbers.nat_within_rational_nonneg
233	conjecture		⊢
	proveit.numbers.number_sets.natural_numbers.natural_pos_lower_bound
234	instantiation	250, 331, 251, 252, 253, 254	⊢
	: , : , : , :
235	conjecture		⊢
	proveit.numbers.numerals.decimals.add_4_4
236	instantiation	332, 281, 255	⊢
	: , : , :
237	instantiation	332, 321, 256	⊢
	: , : , :
238	instantiation	288, 257	⊢
	: , : , :
239	instantiation	287, 258	⊢
	:
240	conjecture		⊢
	proveit.numbers.exponentiation.neg_power_as_div
241	instantiation	332, 259, 260	⊢
	: , : , :
242	instantiation	261, 279	⊢
	:
243	instantiation	332, 319, 262	⊢
	: , : , :
244	conjecture		⊢
	proveit.numbers.number_sets.natural_numbers.nat_pos_within_nat
245	instantiation	332, 281, 263	⊢
	: , : , :
246	instantiation	332, 281, 264	⊢
	: , : , :
247	instantiation	288, 265	⊢
	: , : , :
248	instantiation	266, 267, 268	⊢
	: , : , :
249	instantiation	332, 269, 324	⊢
	: , : , :
250	axiom		⊢
	proveit.core_expr_types.operations.operands_substitution
251	instantiation	270	⊢
	: , :
252	instantiation	270	⊢
	: , :
253	instantiation	287, 271	⊢
	:
254	instantiation	310, 271	⊢
	:
255	instantiation	332, 301, 272	⊢
	: , : , :
256	instantiation	332, 319, 273	⊢
	: , : , :
257	instantiation	274, 279, 322, 275, 276, 277*	⊢
	: , : , :
258	instantiation	278, 279, 280	⊢
	: , :
259	conjecture		⊢
	proveit.numbers.number_sets.complex_numbers.real_nonzero_within_complex_nonzero
260	instantiation	332, 281, 282	⊢
	: , : , :
261	conjecture		⊢
	proveit.numbers.exponentiation.complex_x_to_first_power_is_x
262	instantiation	332, 283, 284	⊢
	: , : , :
263	instantiation	332, 301, 285	⊢
	: , : , :
264	instantiation	332, 301, 286	⊢
	: , : , :
265	instantiation	287, 306	⊢
	:
266	axiom		⊢
	proveit.logic.equality.equals_transitivity
267	instantiation	288, 289	⊢
	: , : , :
268	instantiation	290, 306	⊢
	:
269	conjecture		⊢
	proveit.numbers.number_sets.integers.nat_pos_within_int
270	conjecture		⊢
	proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
271	instantiation	332, 321, 291	⊢
	: , : , :
272	instantiation	332, 313, 292	⊢
	: , : , :
273	instantiation	332, 326, 293	⊢
	: , : , :
274	conjecture		⊢
	proveit.numbers.exponentiation.real_power_of_real_power
275	instantiation	294, 309	⊢
	:
276	instantiation	295, 316	⊢
	:
277	instantiation	296, 311, 297, 298*	⊢
	: , :
278	conjecture		⊢
	proveit.numbers.exponentiation.exp_complex_closure
279	instantiation	332, 321, 299	⊢
	: , : , :
280	instantiation	300, 311	⊢
	:
281	conjecture		⊢
	proveit.numbers.number_sets.real_numbers.rational_nonzero_within_real_nonzero
282	instantiation	332, 301, 302	⊢
	: , : , :
283	conjecture		⊢
	proveit.numbers.number_sets.rational_numbers.rational_pos_within_rational
284	instantiation	303, 304, 305	⊢
	: , :
285	instantiation	332, 313, 314	⊢
	: , : , :
286	instantiation	332, 313, 324	⊢
	: , : , :
287	conjecture		⊢
	proveit.numbers.multiplication.elim_one_left
288	axiom		⊢
	proveit.logic.equality.substitution
289	instantiation	310, 306	⊢
	:
290	conjecture		⊢
	proveit.numbers.division.frac_one_denom
291	instantiation	332, 319, 307	⊢
	: , : , :
292	conjecture		⊢
	proveit.numbers.numerals.decimals.posnat8
293	instantiation	332, 333, 308	⊢
	: , : , :
294	conjecture		⊢
	proveit.numbers.negation.real_closure
295	conjecture		⊢
	proveit.numbers.number_sets.natural_numbers.nonzero_if_is_nat_pos
296	conjecture		⊢
	proveit.numbers.multiplication.mult_neg_right
297	instantiation	332, 321, 309	⊢
	: , : , :
298	instantiation	310, 311	⊢
	:
299	instantiation	332, 319, 312	⊢
	: , : , :
300	conjecture		⊢
	proveit.numbers.negation.complex_closure
301	conjecture		⊢
	proveit.numbers.number_sets.rational_numbers.nonzero_int_within_rational_nonzero
302	instantiation	332, 313, 316	⊢
	: , : , :
303	conjecture		⊢
	proveit.numbers.division.div_rational_pos_closure
304	instantiation	332, 315, 314	⊢
	: , : , :
305	instantiation	332, 315, 316	⊢
	: , : , :
306	instantiation	332, 321, 317	⊢
	: , : , :
307	instantiation	332, 326, 318	⊢
	: , : , :
308	conjecture		⊢
	proveit.numbers.numerals.decimals.nat8
309	instantiation	332, 319, 320	⊢
	: , : , :
310	conjecture		⊢
	proveit.numbers.multiplication.elim_one_right
311	instantiation	332, 321, 322	⊢
	: , : , :
312	instantiation	332, 326, 323	⊢
	: , : , :
313	conjecture		⊢
	proveit.numbers.number_sets.integers.nat_pos_within_nonzero_int
314	conjecture		⊢
	proveit.numbers.numerals.decimals.posnat1
315	conjecture		⊢
	proveit.numbers.number_sets.rational_numbers.nat_pos_within_rational_pos
316	conjecture		⊢
	proveit.numbers.numerals.decimals.posnat2
317	instantiation	328, 329, 324	⊢
	: , : , :
318	instantiation	332, 333, 325	⊢
	: , : , :
319	conjecture		⊢
	proveit.numbers.number_sets.real_numbers.rational_within_real
320	instantiation	332, 326, 327	⊢
	: , : , :
321	conjecture		⊢
	proveit.numbers.number_sets.complex_numbers.real_within_complex
322	instantiation	328, 329, 330	⊢
	: , : , :
323	instantiation	332, 333, 331	⊢
	: , : , :
324	conjecture		⊢
	proveit.physics.quantum.QPE._two_pow_t_is_nat_pos
325	conjecture		⊢
	proveit.numbers.numerals.decimals.nat4
326	conjecture		⊢
	proveit.numbers.number_sets.rational_numbers.int_within_rational
327	instantiation	332, 333, 334	⊢
	: , : , :
328	theorem		⊢
	proveit.logic.sets.inclusion.unfold_subset_eq
329	instantiation	335, 336	⊢
	: , :
330	axiom		⊢
	proveit.physics.quantum.QPE._t_in_natural_pos
331	conjecture		⊢
	proveit.numbers.numerals.decimals.nat2
332	theorem		⊢
	proveit.logic.sets.inclusion.superset_membership_from_proper_subset
333	conjecture		⊢
	proveit.numbers.number_sets.integers.nat_within_int
334	theorem		⊢
	proveit.numbers.numerals.decimals.nat1
335	theorem		⊢
	proveit.logic.sets.inclusion.relax_proper_subset
336	conjecture		⊢
	proveit.numbers.number_sets.real_numbers.nat_pos_within_real
*equality replacement requirements