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.logic.booleans.disjunction.or_if_left
2	instantiation	6, 59, 10, 5	⊢
	: , :
3	instantiation	6, 36, 7, 8	⊢
	: , :
4	instantiation	9, 59, 10, 11	, ,  ⊢
	: , :
5	modus ponens	12, 13	⊢
6	theorem		⊢
	proveit.logic.booleans.disjunction.closure
7	instantiation	17, 14	⊢
	: , :
8	modus ponens	15, 16	⊢
9	theorem		⊢
	proveit.logic.booleans.disjunction.any_if_all
10	instantiation	17, 18	⊢
	: , :
11	modus ponens	19, 20	, ,  ⊢
12	instantiation	26, 52, 53, 27	⊢
	: , : , : , :
13	generalization	21	⊢
14	instantiation	57, 25, 36	⊢
	: , : , :
15	instantiation	26, 52, 22, 23	⊢
	: , : , : , :
16	generalization	24	⊢
17	theorem		⊢
	proveit.core_expr_types.tuples.range_from1_len_typical_eq
18	instantiation	57, 25, 59	⊢
	: , : , :
19	instantiation	26, 52, 53, 27	⊢
	: , : , : , :
20	generalization	28	, ,  ⊢
21	instantiation	30	⊢
	: , :
22	instantiation	57, 58, 36	⊢
	: , : , :
23	instantiation	31, 29	⊢
	:
24	instantiation	30	⊢
	: , :
25	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.nat_pos_within_nat
26	theorem		⊢
	proveit.logic.booleans.conjunction.conjunction_from_quantification
27	instantiation	31, 32	⊢
	:
28	instantiation	33, 34, 35	, , ,  ⊢
	: , : , : , :
29	instantiation	37, 36, 38	⊢
	: , :
30	theorem		⊢
	proveit.logic.equality.not_equals_is_bool
31	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.natural_pos_lower_bound
32	instantiation	37, 59, 38	⊢
	: , :
33	theorem		⊢
	proveit.physics.quantum.circuits.qcircuit_output_part_neq
34	instantiation	39, 40, 41	⊢
	:
35	instantiation	42, 59, 43, 44, 45	, ,  ⊢
	: , : , :
36	axiom		⊢
	proveit.physics.quantum.QPE._s_in_nat_pos
37	theorem		⊢
	proveit.numbers.addition.add_nat_pos_closure_bin
38	theorem		⊢
	proveit.numbers.numerals.decimals.posnat1
39	theorem		⊢
	proveit.numbers.number_sets.integers.pos_int_is_natural_pos
40	instantiation	57, 46, 54	⊢
	: , : , :
41	instantiation	47, 48, 49	⊢
	: , : , :
42	theorem		⊢
	proveit.physics.quantum.algebra.num_ket_neq
43	assumption		⊢
44	assumption		⊢
45	assumption		⊢
46	instantiation	50, 52, 53	⊢
	: , :
47	theorem		⊢
	proveit.numbers.ordering.transitivity_less_less_eq
48	theorem		⊢
	proveit.numbers.numerals.decimals.less_0_1
49	instantiation	51, 52, 53, 54	⊢
	: , : , :
50	theorem		⊢
	proveit.numbers.number_sets.integers.int_interval_within_int
51	theorem		⊢
	proveit.numbers.number_sets.integers.interval_lower_bound
52	instantiation	57, 55, 56	⊢
	: , : , :
53	instantiation	57, 58, 59	⊢
	: , : , :
54	assumption		⊢
55	theorem		⊢
	proveit.numbers.number_sets.integers.nat_within_int
56	theorem		⊢
	proveit.numbers.numerals.decimals.nat1
57	theorem		⊢
	proveit.logic.sets.inclusion.superset_membership_from_proper_subset
58	theorem		⊢
	proveit.numbers.number_sets.integers.nat_pos_within_int
59	axiom		⊢
	proveit.physics.quantum.QPE._t_in_natural_pos