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	, ,  ⊢
	: , :
1	reference	17	⊢
2	instantiation	4, 5, 6, 7	, ,  ⊢
	: , : , :
3	reference	73	⊢
4	theorem		⊢
	proveit.logic.sets.unification.membership_folding
5	theorem		⊢
	proveit.numbers.numerals.decimals.posnat2
6	instantiation	63	⊢
	: , :
7	instantiation	21, 8, 9	, ,  ⊢
	: , :
8	instantiation	10, 11	, ,  ⊢
	: , :
9	instantiation	12, 20, 109, 85, 13	, ,  ⊢
	: , : , :
10	theorem		⊢
	proveit.logic.sets.membership.unfold_not_in_set
11	instantiation	14, 98, 15, 85, 16	, ,  ⊢
	: , : , :
12	theorem		⊢
	proveit.numbers.number_sets.integers.in_interval
13	instantiation	17, 18, 19	, ,  ⊢
	: , :
14	theorem		⊢
	proveit.numbers.number_sets.integers.int_not_in_interval
15	instantiation	111, 20	⊢
	:
16	instantiation	21, 22, 23	, ,  ⊢
	: , :
17	theorem		⊢
	proveit.logic.booleans.conjunction.and_if_both
18	instantiation	24, 76, 49, 25, 26, 27*, 28*	, ,  ⊢
	: , : , :
19	instantiation	29, 98, 109, 93	⊢
	: , : , :
20	instantiation	107, 91, 106	⊢
	: , :
21	theorem		⊢
	proveit.logic.booleans.disjunction.or_if_only_right
22	instantiation	30, 31, 66, 32	⊢
	: , :
23	instantiation	94, 33, 89	,  ⊢
	: , : , :
24	theorem		⊢
	proveit.numbers.addition.weak_bound_via_left_term_bound
25	instantiation	34, 66, 35	,  ⊢
	: , :
26	instantiation	36, 37	, ,  ⊢
	:
27	instantiation	38, 39, 65	⊢
	: , :
28	instantiation	40, 41, 42	,  ⊢
	: , : , :
29	theorem		⊢
	proveit.numbers.number_sets.integers.interval_upper_bound
30	theorem		⊢
	proveit.numbers.ordering.not_less_from_less_eq
31	instantiation	115, 83, 43	⊢
	: , : , :
32	instantiation	101, 98, 109, 93	⊢
	: , : , :
33	instantiation	44, 45	⊢
	:
34	theorem		⊢
	proveit.numbers.addition.add_real_closure_bin
35	instantiation	46, 76	⊢
	:
36	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.natural_pos_lower_bound
37	instantiation	86, 47, 48	, ,  ⊢
	:
38	theorem		⊢
	proveit.numbers.addition.commutation
39	instantiation	115, 75, 49	⊢
	: , : , :
40	axiom		⊢
	proveit.logic.equality.equals_transitivity
41	instantiation	50, 51, 117, 110, 52, 53, 56, 54, 65	,  ⊢
	: , : , : , : , : , :
42	instantiation	55, 65, 56, 57	,  ⊢
	: , : , :
43	instantiation	115, 90, 98	⊢
	: , : , :
44	theorem		⊢
	proveit.numbers.number_sets.integers.negative_if_in_neg_int
45	instantiation	78, 58	⊢
	:
46	theorem		⊢
	proveit.numbers.negation.real_closure
47	instantiation	107, 85, 59	,  ⊢
	: , :
48	instantiation	60, 61	,  ⊢
	: , :
49	instantiation	115, 83, 62	⊢
	: , : , :
50	theorem		⊢
	proveit.numbers.addition.disassociation
51	axiom		⊢
	proveit.numbers.number_sets.natural_numbers.zero_in_nats
52	theorem		⊢
	proveit.core_expr_types.tuples.tuple_len_0_typical_eq
53	instantiation	63	⊢
	: , :
54	instantiation	64, 65	⊢
	:
55	theorem		⊢
	proveit.numbers.addition.subtraction.add_cancel_triple_32
56	instantiation	115, 75, 66	⊢
	: , : , :
57	instantiation	67	⊢
	:
58	instantiation	68, 79, 69	⊢
	: , :
59	instantiation	115, 70, 71	⊢
	: , : , :
60	theorem		⊢
	proveit.numbers.addition.subtraction.pos_difference
61	instantiation	72, 73, 74	,  ⊢
	: , : , :
62	instantiation	115, 90, 106	⊢
	: , : , :
63	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
64	theorem		⊢
	proveit.numbers.negation.complex_closure
65	instantiation	115, 75, 76	⊢
	: , : , :
66	instantiation	115, 83, 77	⊢
	: , : , :
67	axiom		⊢
	proveit.logic.equality.equals_reflexivity
68	theorem		⊢
	proveit.numbers.addition.add_nat_pos_closure_bin
69	theorem		⊢
	proveit.numbers.numerals.decimals.posnat1
70	theorem		⊢
	proveit.numbers.number_sets.integers.neg_int_within_int
71	instantiation	78, 79	⊢
	:
72	theorem		⊢
	proveit.logic.equality.sub_right_side_into
73	instantiation	80, 100	⊢
	: , :
74	instantiation	81, 93, 82*	,  ⊢
	:
75	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.real_within_complex
76	instantiation	115, 83, 84	⊢
	: , : , :
77	instantiation	115, 90, 85	⊢
	: , : , :
78	theorem		⊢
	proveit.numbers.negation.int_neg_closure
79	instantiation	86, 91, 87	⊢
	:
80	theorem		⊢
	proveit.logic.booleans.conjunction.right_from_and
81	theorem		⊢
	proveit.physics.quantum.QPE._modabs_in_full_domain_simp
82	instantiation	88, 89	⊢
	:
83	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_within_real
84	instantiation	115, 90, 91	⊢
	: , : , :
85	instantiation	115, 92, 93	⊢
	: , : , :
86	theorem		⊢
	proveit.numbers.number_sets.integers.pos_int_is_natural_pos
87	instantiation	94, 95, 96	⊢
	: , : , :
88	theorem		⊢
	proveit.numbers.absolute_value.abs_non_neg_elim
89	assumption		⊢
90	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.int_within_rational
91	instantiation	115, 97, 102	⊢
	: , : , :
92	instantiation	103, 98, 109	⊢
	: , :
93	instantiation	99, 100	⊢
	: , :
94	theorem		⊢
	proveit.numbers.ordering.transitivity_less_less_eq
95	theorem		⊢
	proveit.numbers.numerals.decimals.less_0_1
96	instantiation	101, 106, 104, 102	⊢
	: , : , :
97	instantiation	103, 106, 104	⊢
	: , :
98	instantiation	107, 105, 106	⊢
	: , :
99	theorem		⊢
	proveit.logic.booleans.conjunction.left_from_and
100	assumption		⊢
101	theorem		⊢
	proveit.numbers.number_sets.integers.interval_lower_bound
102	assumption		⊢
103	theorem		⊢
	proveit.numbers.number_sets.integers.int_interval_within_int
104	instantiation	107, 109, 108	⊢
	: , :
105	instantiation	111, 109	⊢
	:
106	instantiation	115, 116, 110	⊢
	: , : , :
107	theorem		⊢
	proveit.numbers.addition.add_int_closure_bin
108	instantiation	111, 112	⊢
	:
109	instantiation	115, 113, 114	⊢
	: , : , :
110	theorem		⊢
	proveit.numbers.numerals.decimals.nat1
111	theorem		⊢
	proveit.numbers.negation.int_closure
112	instantiation	115, 116, 117	⊢
	: , : , :
113	theorem		⊢
	proveit.numbers.number_sets.integers.nat_pos_within_int
114	theorem		⊢
	proveit.physics.quantum.QPE._two_pow_t_minus_one_is_nat_pos
115	theorem		⊢
	proveit.logic.sets.inclusion.superset_membership_from_proper_subset
116	theorem		⊢
	proveit.numbers.number_sets.integers.nat_within_int
117	theorem		⊢
	proveit.numbers.numerals.decimals.nat2
*equality replacement requirements