Show the Proof

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

	step type	requirements	statement
0	instantiation	1, 2, 3, 4	⊢
	: , :
1	theorem		⊢
	proveit.numbers.rounding.ceil_increasing_less_eq
2	instantiation	5, 70, 8, 6	⊢
	: , :
3	instantiation	5, 70, 9, 6	⊢
	: , :
4	instantiation	7, 70, 8, 9, 10, 21	⊢
	: , : , :
5	theorem		⊢
	proveit.numbers.logarithms.log_real_pos_real_closure
6	instantiation	11, 12	⊢
	: , :
7	theorem		⊢
	proveit.numbers.logarithms.log_increasing_less_eq
8	instantiation	36, 13, 70, 24	⊢
	: , :
9	instantiation	14, 70, 26	⊢
	: , :
10	instantiation	15, 65, 16, 17, 18, 19*	⊢
	: , : , :
11	theorem		⊢
	proveit.logic.equality.not_equals_symmetry
12	instantiation	20, 94, 87, 21	⊢
	: , :
13	instantiation	92, 74, 22	⊢
	: , : , :
14	theorem		⊢
	proveit.numbers.addition.add_real_pos_closure_bin
15	theorem		⊢
	proveit.numbers.addition.weak_bound_via_right_term_bound
16	instantiation	23, 85, 65, 24	⊢
	: , :
17	instantiation	92, 25, 26	⊢
	: , : , :
18	instantiation	27, 28, 64, 70, 29	⊢
	: , : , :
19	instantiation	30, 79, 91, 31*, 32*, 33*	⊢
	: , : , : , :
20	theorem		⊢
	proveit.numbers.ordering.less_is_not_eq_nat
21	theorem		⊢
	proveit.numbers.numerals.decimals.less_1_2
22	instantiation	92, 80, 34	⊢
	: , : , :
23	theorem		⊢
	proveit.numbers.division.div_real_closure
24	instantiation	35, 81	⊢
	:
25	theorem		⊢
	proveit.numbers.number_sets.real_numbers.real_pos_within_real
26	instantiation	36, 37, 64, 38	⊢
	: , :
27	theorem		⊢
	proveit.numbers.division.weak_div_from_denom_bound__all_pos
28	instantiation	92, 39, 40	⊢
	: , : , :
29	instantiation	41, 65, 77, 85, 42, 43, 44*	⊢
	: , : , :
30	theorem		⊢
	proveit.numbers.addition.rational_pair_addition
31	instantiation	45, 56	⊢
	:
32	instantiation	46, 47, 48	⊢
	: , : , :
33	instantiation	49, 56	⊢
	:
34	theorem		⊢
	proveit.numbers.numerals.decimals.posnat5
35	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.nonzero_if_is_nat_pos
36	theorem		⊢
	proveit.numbers.division.div_real_pos_closure
37	instantiation	92, 74, 50	⊢
	: , : , :
38	instantiation	51, 52	⊢
	:
39	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_nonneg_within_real_nonneg
40	instantiation	92, 53, 94	⊢
	: , : , :
41	theorem		⊢
	proveit.numbers.multiplication.weak_bound_via_right_factor_bound
42	instantiation	54, 84, 85, 86	⊢
	: , : , :
43	instantiation	55, 87	⊢
	:
44	instantiation	67, 56	⊢
	:
45	theorem		⊢
	proveit.numbers.division.frac_one_denom
46	axiom		⊢
	proveit.logic.equality.equals_transitivity
47	instantiation	57, 87, 58, 59, 60, 61	⊢
	: , : , : , :
48	theorem		⊢
	proveit.numbers.numerals.decimals.add_4_1
49	theorem		⊢
	proveit.numbers.multiplication.elim_one_left
50	instantiation	92, 80, 62	⊢
	: , : , :
51	theorem		⊢
	proveit.numbers.number_sets.real_numbers.nonzero_if_in_real_nonzero
52	instantiation	92, 63, 64	⊢
	: , : , :
53	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.nat_within_rational_nonneg
54	theorem		⊢
	proveit.numbers.number_sets.real_numbers.interval_oc_upper_bound
55	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.natural_lower_bound
56	instantiation	92, 73, 65	⊢
	: , : , :
57	axiom		⊢
	proveit.core_expr_types.operations.operands_substitution
58	instantiation	66	⊢
	: , :
59	instantiation	66	⊢
	: , :
60	theorem		⊢
	proveit.numbers.numerals.decimals.mult_2_2
61	instantiation	67, 68	⊢
	:
62	theorem		⊢
	proveit.numbers.numerals.decimals.posnat1
63	theorem		⊢
	proveit.numbers.number_sets.real_numbers.real_pos_within_real_nonzero
64	instantiation	69, 70, 71	⊢
	: , :
65	instantiation	92, 88, 72	⊢
	: , : , :
66	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
67	theorem		⊢
	proveit.numbers.multiplication.elim_one_right
68	instantiation	92, 73, 85	⊢
	: , : , :
69	theorem		⊢
	proveit.numbers.multiplication.mult_real_pos_closure_bin
70	instantiation	92, 74, 75	⊢
	: , : , :
71	instantiation	76, 77, 78	⊢
	:
72	instantiation	92, 90, 79	⊢
	: , : , :
73	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.real_within_complex
74	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_pos_within_real_pos
75	instantiation	92, 80, 81	⊢
	: , : , :
76	theorem		⊢
	proveit.numbers.number_sets.real_numbers.pos_real_is_real_pos
77	instantiation	82, 84, 85, 86	⊢
	: , : , :
78	instantiation	83, 84, 85, 86	⊢
	: , : , :
79	instantiation	92, 93, 87	⊢
	: , : , :
80	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.nat_pos_within_rational_pos
81	theorem		⊢
	proveit.numbers.numerals.decimals.posnat2
82	theorem		⊢
	proveit.numbers.number_sets.real_numbers.all_in_interval_oc__is__real
83	theorem		⊢
	proveit.numbers.number_sets.real_numbers.interval_oc_lower_bound
84	theorem		⊢
	proveit.numbers.number_sets.real_numbers.zero_is_real
85	instantiation	92, 88, 89	⊢
	: , : , :
86	axiom		⊢
	proveit.physics.quantum.QPE._eps_in_interval
87	theorem		⊢
	proveit.numbers.numerals.decimals.nat2
88	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_within_real
89	instantiation	92, 90, 91	⊢
	: , : , :
90	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.int_within_rational
91	instantiation	92, 93, 94	⊢
	: , : , :
92	theorem		⊢
	proveit.logic.sets.inclusion.superset_membership_from_proper_subset
93	theorem		⊢
	proveit.numbers.number_sets.integers.nat_within_int
94	theorem		⊢
	proveit.numbers.numerals.decimals.nat1
*equality replacement requirements