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

import proveit
theory = proveit.Theory() # the theorem's theory
from proveit import a, b # used in an instantiation dict
from proveit.numbers import (
        zero, one, two, Add, frac, greater, Integer, Mult,
        NaturalPos, Neg, Real, subtract)
from proveit.physics.quantum.QPE import (
        _e_domain, _eps_in_interval, _e_value, _e_value_ge_two,
        _n, _n_ge_two, _n_in_natural_pos, _t, _t_in_natural_pos, _t_req)

%proving _e_value_in_e_domain

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

_n_in_natural_pos

 ⊢  

_t_in_natural_pos

 ⊢  

_n_ge_two

 ⊢  

_t_req

 ⊢  

_eps_in_interval

 ⊢  

bound_01 = _t_req.right_add_both_sides(Neg(_n))

bound_01:  ⊢  

_eps_le_one = _eps_in_interval.derive_element_upper_bound()

_eps_le_one:  ⊢  

greater(Add(two, frac(one, two)), zero).prove()

 ⊢  

bound_02 = bound_01.rhs.deduce_bound(_eps_le_one)

bound_02:  ⊢  

bound_03 = bound_01.apply_transitivity(bound_02)

bound_03:  ⊢  

from proveit.numbers.logarithms import log_base_large_a_greater_one
log_base_large_a_greater_one

 ⊢  

_a_sub, _b_sub = (
    bound_03.rhs.operand.base,
    bound_03.rhs.operand.antilog)
log_base_2_of_stuff_greater_than_one = log_base_large_a_greater_one.instantiate(
    {a: _a_sub, b: _b_sub})

log_base_2_of_stuff_greater_than_one:  ⊢  

bound_04 = bound_03.rhs.deduce_bound(log_base_2_of_stuff_greater_than_one)

bound_04:  ⊢  

bound_05 = bound_03.apply_transitivity(bound_04)

bound_05:  ⊢  

_e_value_ge_two

 ⊢  

_n_ge_two

 ⊢  

bound_06 = _e_value.deduce_bound(_n_ge_two)

bound_06:  ⊢  

bound_07 = bound_06.add_right(bound_06.rhs)

bound_07:  ⊢  

_e_value_in_e_domain may now be readily provable (assuming required theorems are usable).  Simply execute "%qed".

%qed

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

	step type	requirements	statement
0	instantiation	1, 2, 3, 4, 5	⊢
	: , : , :
1	conjecture		⊢
	proveit.numbers.number_sets.integers.in_interval
2	reference	316	⊢
3	instantiation	110, 6, 112	⊢
	: , :
4	instantiation	110, 7, 31	⊢
	: , :
5	instantiation	170, 8, 9	⊢
	: , :
6	instantiation	10, 280, 11	⊢
	: , :
7	instantiation	317, 116, 12	⊢
	: , : , :
8	instantiation	158, 90, 264, 13, 14, 15*, 16*	⊢
	: , : , :
9	instantiation	17, 18, 19	⊢
	: , : , :
10	conjecture		⊢
	proveit.numbers.exponentiation.exp_int_closure
11	instantiation	103, 20, 21	⊢
	:
12	instantiation	59, 290, 67	⊢
	: , :
13	instantiation	177, 26, 311	⊢
	: , :
14	instantiation	126, 264, 26, 311, 22, 23	⊢
	: , : , :
15	instantiation	24, 272, 251, 142	⊢
	: , : , :
16	instantiation	224, 25	⊢
	: , : , :
17	theorem		⊢
	proveit.logic.equality.sub_right_side_into
18	instantiation	126, 26, 60, 27, 28, 29*	⊢
	: , : , :
19	instantiation	224, 30	⊢
	: , : , :
20	instantiation	110, 111, 31	⊢
	: , :
21	instantiation	113, 32	⊢
	: , :
22	conjecture		⊢
	proveit.physics.quantum.QPE._e_value_ge_two
23	instantiation	250, 319	⊢
	:
24	conjecture		⊢
	proveit.numbers.addition.subtraction.subtract_from_add
25	instantiation	245, 33, 34	⊢
	: , : , :
26	instantiation	177, 57, 90	⊢
	: , :
27	instantiation	158, 90, 57, 92, 35	⊢
	: , : , :
28	instantiation	158, 90, 311, 92, 36, 37*	⊢
	: , : , :
29	instantiation	136, 38, 39, 40	⊢
	: , : , : , :
30	instantiation	224, 41	⊢
	: , : , :
31	instantiation	317, 117, 42	⊢
	: , : , :
32	instantiation	47, 200	⊢
	:
33	instantiation	191, 192, 290, 319, 193, 43, 44, 65, 272	⊢
	: , : , : , : , : , :
34	instantiation	168, 272, 44, 50	⊢
	: , : , :
35	instantiation	45, 264, 127, 86, 291, 46	⊢
	: , : , :
36	instantiation	47, 48	⊢
	:
37	instantiation	49, 272, 50	⊢
	: , :
38	instantiation	191, 192, 290, 319, 193, 52, 84, 65, 51	⊢
	: , : , : , : , : , :
39	instantiation	191, 290, 192, 52, 193, 84, 65	⊢
	: , : , : , : , : , :
40	instantiation	136, 53, 54, 55	⊢
	: , : , : , :
41	instantiation	56, 65, 169	⊢
	: , :
42	instantiation	121, 295	⊢
	:
43	instantiation	270	⊢
	: , :
44	instantiation	317, 279, 57	⊢
	: , : , :
45	conjecture		⊢
	proveit.numbers.exponentiation.exp_monotonicity_large_base_less_eq
46	instantiation	187, 179, 217, 178, 58	⊢
	: , : , :
47	conjecture		⊢
	proveit.numbers.number_sets.natural_numbers.natural_pos_lower_bound
48	instantiation	59, 290, 99	⊢
	: , :
49	conjecture		⊢
	proveit.numbers.addition.subtraction.add_cancel_basic
50	instantiation	219	⊢
	:
51	instantiation	317, 279, 60	⊢
	: , : , :
52	instantiation	270	⊢
	: , :
53	instantiation	106, 319, 84, 65	⊢
	: , : , : , : , : , : , :
54	instantiation	107, 192, 290, 193, 61, 63, 84, 65, 62*	⊢
	: , : , : , : , : , :
55	instantiation	107, 319, 290, 192, 63, 193, 64, 65, 66*	⊢
	: , : , : , : , : , :
56	conjecture		⊢
	proveit.numbers.addition.commutation
57	instantiation	98, 264, 67	⊢
	: , :
58	instantiation	68, 264, 240, 119	⊢
	: , :
59	conjecture		⊢
	proveit.numbers.exponentiation.exp_natpos_closure
60	instantiation	177, 92, 90	⊢
	: , :
61	instantiation	270	⊢
	: , :
62	instantiation	69, 70, 71*	⊢
	: , :
63	instantiation	270	⊢
	: , :
64	instantiation	72, 251, 73	⊢
	: , :
65	instantiation	164, 272	⊢
	:
66	instantiation	74, 272, 251, 142	⊢
	: , : , :
67	instantiation	103, 75, 76	⊢
	:
68	conjecture		⊢
	proveit.numbers.negation.negated_weak_bound
69	theorem		⊢
	proveit.logic.equality.equals_reversal
70	instantiation	77, 192, 290, 319, 193, 78, 272, 84, 79*	⊢
	: , : , : , : , : , :
71	instantiation	245, 80, 81	⊢
	: , : , :
72	conjecture		⊢
	proveit.numbers.exponentiation.exp_complex_closure
73	instantiation	317, 279, 82	⊢
	: , : , :
74	conjecture		⊢
	proveit.numbers.addition.subtraction.negated_add
75	instantiation	110, 111, 83	⊢
	: , :
76	instantiation	113, 120	⊢
	: , :
77	conjecture		⊢
	proveit.numbers.multiplication.distribute_through_sum
78	instantiation	270	⊢
	: , :
79	instantiation	238, 84	⊢
	:
80	instantiation	224, 142	⊢
	: , : , :
81	instantiation	85, 251, 311, 86, 87, 88*, 89*	⊢
	: , : , :
82	instantiation	177, 90, 179	⊢
	: , :
83	instantiation	317, 117, 91	⊢
	: , : , :
84	instantiation	317, 279, 92	⊢
	: , : , :
85	conjecture		⊢
	proveit.numbers.exponentiation.product_of_real_powers
86	instantiation	317, 313, 93	⊢
	: , : , :
87	instantiation	94, 307	⊢
	:
88	instantiation	95, 251	⊢
	:
89	instantiation	245, 96, 97	⊢
	: , : , :
90	instantiation	239, 311	⊢
	:
91	instantiation	121, 256	⊢
	:
92	instantiation	98, 264, 99	⊢
	: , :
93	instantiation	317, 315, 104	⊢
	: , : , :
94	conjecture		⊢
	proveit.numbers.number_sets.natural_numbers.nonzero_if_is_nat_pos
95	conjecture		⊢
	proveit.numbers.exponentiation.complex_x_to_first_power_is_x
96	instantiation	191, 319, 290, 192, 100, 193, 272, 169, 150	⊢
	: , : , : , : , : , :
97	instantiation	245, 101, 102	⊢
	: , : , :
98	conjecture		⊢
	proveit.numbers.exponentiation.exp_real_closure_nat_power
99	instantiation	103, 104, 105	⊢
	:
100	instantiation	270	⊢
	: , :
101	instantiation	106, 319, 192, 193, 272, 169, 150	⊢
	: , : , : , : , : , : , :
102	instantiation	107, 192, 290, 319, 193, 108, 272, 150, 169, 109*	⊢
	: , : , : , : , : , :
103	conjecture		⊢
	proveit.numbers.number_sets.integers.nonneg_int_is_natural
104	instantiation	110, 111, 112	⊢
	: , :
105	instantiation	113, 114	⊢
	: , :
106	conjecture		⊢
	proveit.numbers.addition.leftward_commutation
107	conjecture		⊢
	proveit.numbers.addition.association
108	instantiation	270	⊢
	: , :
109	instantiation	115, 272, 251, 142	⊢
	: , : , :
110	conjecture		⊢
	proveit.numbers.addition.add_int_closure_bin
111	instantiation	317, 116, 200	⊢
	: , : , :
112	instantiation	317, 117, 118	⊢
	: , : , :
113	conjecture		⊢
	proveit.numbers.addition.subtraction.nonneg_difference
114	instantiation	143, 119, 120	⊢
	: , : , :
115	conjecture		⊢
	proveit.numbers.addition.subtraction.subtract_from_add_reversed
116	conjecture		⊢
	proveit.numbers.number_sets.integers.nat_pos_within_int
117	conjecture		⊢
	proveit.numbers.number_sets.integers.neg_int_within_int
118	instantiation	121, 307	⊢
	:
119	axiom		⊢
	proveit.physics.quantum.QPE._n_ge_two
120	instantiation	158, 162, 264, 122, 123, 124*, 125*	⊢
	: , : , :
121	conjecture		⊢
	proveit.numbers.negation.int_neg_closure
122	instantiation	177, 127, 264	⊢
	: , :
123	instantiation	126, 264, 127, 128, 234	⊢
	: , : , :
124	instantiation	245, 129, 130	⊢
	: , : , :
125	instantiation	245, 131, 132	⊢
	: , : , :
126	conjecture		⊢
	proveit.numbers.ordering.less_eq_add_right
127	instantiation	177, 179, 217	⊢
	: , :
128	instantiation	143, 133, 134	⊢
	: , : , :
129	instantiation	191, 319, 290, 192, 149, 193, 251, 197, 150	⊢
	: , : , : , : , : , :
130	instantiation	196, 251, 197, 167	⊢
	: , : , :
131	instantiation	224, 135	⊢
	: , : , :
132	instantiation	136, 137, 138, 139	⊢
	: , : , : , :
133	instantiation	140, 316, 156, 141, 142*	⊢
	: , :
134	instantiation	143, 144, 145	⊢
	: , : , :
135	instantiation	191, 192, 290, 319, 193, 166, 169, 195, 251	⊢
	: , : , : , : , : , :
136	conjecture		⊢
	proveit.logic.equality.four_chain_transitivity
137	instantiation	191, 192, 147, 319, 193, 148, 169, 195, 251, 146	⊢
	: , : , : , : , : , :
138	instantiation	191, 147, 290, 192, 148, 149, 193, 169, 195, 251, 197, 150	⊢
	: , : , : , : , : , :
139	instantiation	245, 151, 152	⊢
	: , : , :
140	conjecture		⊢
	proveit.numbers.rounding.ceil_of_real_above_int
141	instantiation	153, 299, 173, 154	⊢
	: , :
142	conjecture		⊢
	proveit.numbers.numerals.decimals.add_1_1
143	conjecture		⊢
	proveit.numbers.ordering.transitivity_less_eq_less_eq
144	instantiation	155, 156, 268, 157	⊢
	: , :
145	instantiation	158, 217, 159, 179, 160, 161*	⊢
	: , : , :
146	instantiation	317, 279, 162	⊢
	: , : , :
147	conjecture		⊢
	proveit.numbers.numerals.decimals.nat3
148	instantiation	163	⊢
	: , : , :
149	instantiation	270	⊢
	: , :
150	instantiation	164, 251	⊢
	:
151	instantiation	165, 290, 319, 192, 166, 193, 169, 195, 251, 197, 167	⊢
	: , : , : , : , : , : , : , :
152	instantiation	168, 197, 169, 199	⊢
	: , : , :
153	conjecture		⊢
	proveit.numbers.logarithms.log_base_large_a_greater_one
154	instantiation	170, 291, 171	⊢
	: , :
155	conjecture		⊢
	proveit.numbers.rounding.ceil_increasing_less_eq
156	instantiation	274, 299, 173, 276	⊢
	: , :
157	instantiation	172, 299, 173, 275, 174, 291	⊢
	: , : , :
158	conjecture		⊢
	proveit.numbers.addition.weak_bound_via_left_term_bound
159	instantiation	177, 240, 218	⊢
	: , :
160	axiom		⊢
	proveit.physics.quantum.QPE._t_req
161	instantiation	245, 175, 176	⊢
	: , : , :
162	instantiation	177, 240, 178	⊢
	: , :
163	conjecture		⊢
	proveit.numbers.numerals.decimals.tuple_len_3_typical_eq
164	conjecture		⊢
	proveit.numbers.negation.complex_closure
165	conjecture		⊢
	proveit.numbers.addition.subtraction.add_cancel_general
166	instantiation	270	⊢
	: , :
167	instantiation	219	⊢
	:
168	conjecture		⊢
	proveit.numbers.addition.subtraction.add_cancel_triple_32
169	instantiation	317, 279, 179	⊢
	: , : , :
170	theorem		⊢
	proveit.logic.booleans.conjunction.and_if_both
171	instantiation	180, 264, 181, 182, 183, 184*, 185*	⊢
	: , : , :
172	conjecture		⊢
	proveit.numbers.logarithms.log_increasing_less_eq
173	instantiation	317, 301, 186	⊢
	: , : , :
174	instantiation	187, 264, 258, 188, 189, 190*	⊢
	: , : , :
175	instantiation	191, 192, 290, 319, 193, 194, 197, 198, 195	⊢
	: , : , : , : , : , :
176	instantiation	196, 197, 198, 199	⊢
	: , : , :
177	conjecture		⊢
	proveit.numbers.addition.add_real_closure_bin
178	instantiation	239, 264	⊢
	:
179	instantiation	254, 255, 200	⊢
	: , : , :
180	conjecture		⊢
	proveit.numbers.addition.strong_bound_via_left_term_bound
181	instantiation	201, 258, 310	⊢
	: , :
182	instantiation	317, 313, 202	⊢
	: , : , :
183	instantiation	203, 258, 310, 311, 204, 205	⊢
	: , : , :
184	instantiation	245, 206, 207	⊢
	: , : , :
185	instantiation	245, 208, 209	⊢
	: , : , :
186	instantiation	285, 210, 302	⊢
	: , :
187	conjecture		⊢
	proveit.numbers.addition.weak_bound_via_right_term_bound
188	instantiation	317, 211, 282	⊢
	: , : , :
189	instantiation	212, 213, 297, 299, 214	⊢
	: , : , :
190	instantiation	226, 280, 316, 227*, 215*, 216*	⊢
	: , : , : , :
191	conjecture		⊢
	proveit.numbers.addition.disassociation
192	axiom		⊢
	proveit.numbers.number_sets.natural_numbers.zero_in_nats
193	conjecture		⊢
	proveit.core_expr_types.tuples.tuple_len_0_typical_eq
194	instantiation	270	⊢
	: , :
195	instantiation	317, 279, 217	⊢
	: , : , :
196	conjecture		⊢
	proveit.numbers.addition.subtraction.add_cancel_triple_13
197	instantiation	317, 279, 240	⊢
	: , : , :
198	instantiation	317, 279, 218	⊢
	: , : , :
199	instantiation	219	⊢
	:
200	axiom		⊢
	proveit.physics.quantum.QPE._t_in_natural_pos
201	conjecture		⊢
	proveit.numbers.multiplication.mult_real_closure_bin
202	instantiation	220, 269, 314	⊢
	: , :
203	conjecture		⊢
	proveit.numbers.multiplication.strong_bound_via_right_factor_bound
204	conjecture		⊢
	proveit.numbers.numerals.decimals.less_0_1
205	instantiation	221, 278	⊢
	:
206	instantiation	224, 222	⊢
	: , : , :
207	instantiation	223, 251	⊢
	:
208	instantiation	224, 225	⊢
	: , : , :
209	instantiation	226, 316, 280, 227*, 228*, 235*	⊢
	: , : , : , :
210	instantiation	317, 306, 229	⊢
	: , : , :
211	conjecture		⊢
	proveit.numbers.number_sets.real_numbers.real_pos_within_real
212	conjecture		⊢
	proveit.numbers.division.weak_div_from_denom_bound__all_pos
213	instantiation	317, 230, 231	⊢
	: , : , :
214	instantiation	232, 264, 304, 311, 233, 234, 235*	⊢
	: , : , :
215	instantiation	245, 236, 237	⊢
	: , : , :
216	instantiation	238, 251	⊢
	:
217	instantiation	239, 240	⊢
	:
218	instantiation	317, 313, 241	⊢
	: , : , :
219	axiom		⊢
	proveit.logic.equality.equals_reflexivity
220	conjecture		⊢
	proveit.numbers.multiplication.mult_rational_closure_bin
221	conjecture		⊢
	proveit.numbers.number_sets.rational_numbers.positive_if_in_rational_pos
222	instantiation	242, 243	⊢
	:
223	conjecture		⊢
	proveit.numbers.addition.elim_zero_left
224	axiom		⊢
	proveit.logic.equality.substitution
225	instantiation	271, 243	⊢
	:
226	conjecture		⊢
	proveit.numbers.addition.rational_pair_addition
227	instantiation	244, 251	⊢
	:
228	instantiation	245, 246, 247	⊢
	: , : , :
229	conjecture		⊢
	proveit.numbers.numerals.decimals.posnat5
230	conjecture		⊢
	proveit.numbers.number_sets.real_numbers.rational_nonneg_within_real_nonneg
231	instantiation	317, 248, 319	⊢
	: , : , :
232	conjecture		⊢
	proveit.numbers.multiplication.weak_bound_via_right_factor_bound
233	instantiation	249, 310, 311, 312	⊢
	: , : , :
234	instantiation	250, 290	⊢
	:
235	instantiation	271, 251	⊢
	:
236	instantiation	259, 290, 252, 253, 263, 262	⊢
	: , : , : , :
237	conjecture		⊢
	proveit.numbers.numerals.decimals.add_4_1
238	conjecture		⊢
	proveit.numbers.multiplication.elim_one_left
239	conjecture		⊢
	proveit.numbers.negation.real_closure
240	instantiation	254, 255, 256	⊢
	: , : , :
241	instantiation	317, 315, 257	⊢
	: , : , :
242	conjecture		⊢
	proveit.numbers.multiplication.mult_zero_right
243	instantiation	317, 279, 258	⊢
	: , : , :
244	conjecture		⊢
	proveit.numbers.division.frac_one_denom
245	axiom		⊢
	proveit.logic.equality.equals_transitivity
246	instantiation	259, 290, 260, 261, 262, 263	⊢
	: , : , : , :
247	conjecture		⊢
	proveit.numbers.numerals.decimals.add_1_4
248	conjecture		⊢
	proveit.numbers.number_sets.rational_numbers.nat_within_rational_nonneg
249	conjecture		⊢
	proveit.numbers.number_sets.real_numbers.interval_oc_upper_bound
250	conjecture		⊢
	proveit.numbers.number_sets.natural_numbers.natural_lower_bound
251	instantiation	317, 279, 264	⊢
	: , : , :
252	instantiation	270	⊢
	: , :
253	instantiation	270	⊢
	: , :
254	theorem		⊢
	proveit.logic.sets.inclusion.unfold_subset_eq
255	instantiation	265, 266	⊢
	: , :
256	axiom		⊢
	proveit.physics.quantum.QPE._n_in_natural_pos
257	instantiation	267, 268	⊢
	:
258	instantiation	317, 313, 269	⊢
	: , : , :
259	axiom		⊢
	proveit.core_expr_types.operations.operands_substitution
260	instantiation	270	⊢
	: , :
261	instantiation	270	⊢
	: , :
262	instantiation	271, 272	⊢
	:
263	conjecture		⊢
	proveit.numbers.numerals.decimals.mult_2_2
264	instantiation	317, 313, 273	⊢
	: , : , :
265	theorem		⊢
	proveit.logic.sets.inclusion.relax_proper_subset
266	conjecture		⊢
	proveit.numbers.number_sets.real_numbers.nat_pos_within_real
267	axiom		⊢
	proveit.numbers.rounding.ceil_is_an_int
268	instantiation	274, 299, 275, 276	⊢
	: , :
269	instantiation	317, 277, 278	⊢
	: , : , :
270	conjecture		⊢
	proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
271	conjecture		⊢
	proveit.numbers.multiplication.elim_one_right
272	instantiation	317, 279, 311	⊢
	: , : , :
273	instantiation	317, 315, 280	⊢
	: , : , :
274	conjecture		⊢
	proveit.numbers.logarithms.log_real_pos_real_closure
275	instantiation	281, 299, 282	⊢
	: , :
276	instantiation	283, 284	⊢
	: , :
277	conjecture		⊢
	proveit.numbers.number_sets.rational_numbers.rational_pos_within_rational
278	instantiation	285, 292, 302	⊢
	: , :
279	conjecture		⊢
	proveit.numbers.number_sets.complex_numbers.real_within_complex
280	instantiation	317, 318, 290	⊢
	: , : , :
281	conjecture		⊢
	proveit.numbers.addition.add_real_pos_closure_bin
282	instantiation	286, 287, 297, 288	⊢
	: , :
283	theorem		⊢
	proveit.logic.equality.not_equals_symmetry
284	instantiation	289, 319, 290, 291	⊢
	: , :
285	conjecture		⊢
	proveit.numbers.division.div_rational_pos_closure
286	conjecture		⊢
	proveit.numbers.division.div_real_pos_closure
287	instantiation	317, 301, 292	⊢
	: , : , :
288	instantiation	293, 294	⊢
	:
289	conjecture		⊢
	proveit.numbers.ordering.less_is_not_eq_nat
290	conjecture		⊢
	proveit.numbers.numerals.decimals.nat2
291	conjecture		⊢
	proveit.numbers.numerals.decimals.less_1_2
292	instantiation	317, 306, 295	⊢
	: , : , :
293	conjecture		⊢
	proveit.numbers.number_sets.real_numbers.nonzero_if_in_real_nonzero
294	instantiation	317, 296, 297	⊢
	: , : , :
295	conjecture		⊢
	proveit.numbers.numerals.decimals.posnat1
296	conjecture		⊢
	proveit.numbers.number_sets.real_numbers.real_pos_within_real_nonzero
297	instantiation	298, 299, 300	⊢
	: , :
298	conjecture		⊢
	proveit.numbers.multiplication.mult_real_pos_closure_bin
299	instantiation	317, 301, 302	⊢
	: , : , :
300	instantiation	303, 304, 305	⊢
	:
301	conjecture		⊢
	proveit.numbers.number_sets.real_numbers.rational_pos_within_real_pos
302	instantiation	317, 306, 307	⊢
	: , : , :
303	conjecture		⊢
	proveit.numbers.number_sets.real_numbers.pos_real_is_real_pos
304	instantiation	308, 310, 311, 312	⊢
	: , : , :
305	instantiation	309, 310, 311, 312	⊢
	: , : , :
306	conjecture		⊢
	proveit.numbers.number_sets.rational_numbers.nat_pos_within_rational_pos
307	conjecture		⊢
	proveit.numbers.numerals.decimals.posnat2
308	conjecture		⊢
	proveit.numbers.number_sets.real_numbers.all_in_interval_oc__is__real
309	conjecture		⊢
	proveit.numbers.number_sets.real_numbers.interval_oc_lower_bound
310	conjecture		⊢
	proveit.numbers.number_sets.real_numbers.zero_is_real
311	instantiation	317, 313, 314	⊢
	: , : , :
312	axiom		⊢
	proveit.physics.quantum.QPE._eps_in_interval
313	conjecture		⊢
	proveit.numbers.number_sets.real_numbers.rational_within_real
314	instantiation	317, 315, 316	⊢
	: , : , :
315	conjecture		⊢
	proveit.numbers.number_sets.rational_numbers.int_within_rational
316	instantiation	317, 318, 319	⊢
	: , : , :
317	theorem		⊢
	proveit.logic.sets.inclusion.superset_membership_from_proper_subset
318	conjecture		⊢
	proveit.numbers.number_sets.integers.nat_within_int
319	theorem		⊢
	proveit.numbers.numerals.decimals.nat1
*equality replacement requirements