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, 5, 6, 7, 8, 9, 10	⊢
	: , : , : , :
1	theorem		⊢
	proveit.physics.quantum.circuits.qcircuit_neq
2	reference	46	⊢
3	reference	64	⊢
4	instantiation	78, 11, 13, 14	⊢
	: , : , : , :
5	instantiation	78, 12, 13, 14	⊢
	: , : , : , :
6	instantiation	78, 15, 20, 21	⊢
	: , : , : , :
7	instantiation	78, 16, 20, 21	⊢
	: , : , : , :
8	instantiation	78, 17, 20, 21	⊢
	: , : , : , :
9	instantiation	78, 18, 20, 21	⊢
	: , : , : , :
10	instantiation	78, 19, 20, 21	⊢
	: , : , : , :
11	instantiation	37, 23, 22, 25, 26, 40, 41, 34, 27*	⊢
	: , : , : , :
12	instantiation	37, 23, 24, 25, 26, 40, 41, 34, 27*	⊢
	: , : , : , :
13	instantiation	94, 28	⊢
	: , :
14	instantiation	94, 29	⊢
	: , :
15	instantiation	37, 38, 30, 112, 101, 40, 41, 57*, 104*	⊢
	: , : , : , :
16	instantiation	37, 38, 31, 32, 33, 40, 34, 57*, 58*	⊢
	: , : , : , :
17	instantiation	37, 38, 35, 112, 101, 40, 41, 57*, 104*	⊢
	: , : , : , :
18	instantiation	37, 38, 36, 112, 101, 40, 41, 57*, 104*	⊢
	: , : , : , :
19	instantiation	37, 38, 39, 112, 101, 40, 41, 57*, 104*	⊢
	: , : , : , :
20	instantiation	131	⊢
	:
21	instantiation	94, 42	⊢
	: , :
22	instantiation	65	⊢
	: , : , : , : , : , : , : , :
23	theorem		⊢
	proveit.numbers.numerals.decimals.posnat8
24	instantiation	65	⊢
	: , : , : , : , : , : , : , :
25	instantiation	65	⊢
	: , : , : , : , : , : , : , :
26	instantiation	65	⊢
	: , : , : , : , : , : , : , :
27	instantiation	150, 43, 44	⊢
	: , : , :
28	instantiation	109, 171, 168, 136, 101, 137, 93, 129, 125	⊢
	: , : , : , : , : , :
29	instantiation	45, 46, 47, 52	⊢
	: , : , :
30	instantiation	146	⊢
	: , :
31	instantiation	146	⊢
	: , :
32	instantiation	146	⊢
	: , :
33	instantiation	146	⊢
	: , :
34	instantiation	49, 50, 58	⊢
	: , : , :
35	instantiation	146	⊢
	: , :
36	instantiation	146	⊢
	: , :
37	theorem		⊢
	proveit.core_expr_types.tuples.general_len
38	theorem		⊢
	proveit.numbers.numerals.decimals.posnat2
39	instantiation	146	⊢
	: , :
40	instantiation	49, 48, 57	⊢
	: , : , :
41	instantiation	49, 50, 104	⊢
	: , : , :
42	instantiation	51, 52	⊢
	: , :
43	instantiation	53, 54, 55, 56, 57, 104, 58	⊢
	: , : , : , :
44	instantiation	78, 59, 60, 61	⊢
	: , : , : , :
45	theorem		⊢
	proveit.core_expr_types.tuples.len_of_ranges_with_repeated_indices_from_1
46	theorem		⊢
	proveit.numbers.numerals.decimals.posnat4
47	instantiation	62, 144	⊢
	: , :
48	instantiation	169, 63, 155	⊢
	: , : , :
49	theorem		⊢
	proveit.logic.equality.sub_left_side_into
50	instantiation	169, 63, 145	⊢
	: , : , :
51	theorem		⊢
	proveit.core_expr_types.tuples.range_from1_len
52	instantiation	169, 63, 64	⊢
	: , : , :
53	axiom		⊢
	proveit.core_expr_types.operations.operands_substitution
54	theorem		⊢
	proveit.numbers.numerals.decimals.nat8
55	instantiation	65	⊢
	: , : , : , : , : , : , : , :
56	instantiation	65	⊢
	: , : , : , : , : , : , : , :
57	instantiation	120, 140, 129, 121	⊢
	: , : , :
58	instantiation	150, 66, 67	⊢
	: , : , :
59	instantiation	78, 68, 69, 70	⊢
	: , : , : , :
60	instantiation	135, 136, 144, 137, 71, 73, 129, 125, 72*	⊢
	: , : , : , : , : , :
61	instantiation	135, 171, 144, 136, 73, 137, 74, 125, 75*	⊢
	: , : , : , : , : , :
62	theorem		⊢
	proveit.core_expr_types.tuples.range_from1_len_typical_eq
63	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.nat_pos_within_nat
64	instantiation	76, 155, 145	⊢
	: , :
65	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_8_typical_eq
66	instantiation	160, 77	⊢
	: , : , :
67	instantiation	78, 79, 80, 81	⊢
	: , : , : , :
68	instantiation	87, 171, 82, 83, 129, 125	⊢
	: , : , : , : , : , : , :
69	instantiation	87, 168, 88, 84, 85, 86, 129, 125	⊢
	: , : , : , : , : , : , :
70	instantiation	87, 88, 171, 89, 90, 129, 125	⊢
	: , : , : , : , : , : , :
71	instantiation	123	⊢
	: , : , : , :
72	instantiation	94, 91, 96*	⊢
	: , :
73	instantiation	123	⊢
	: , : , : , :
74	instantiation	92, 93, 129	⊢
	: , :
75	instantiation	94, 95, 96*	⊢
	: , :
76	theorem		⊢
	proveit.numbers.addition.add_nat_pos_closure_bin
77	instantiation	97, 129, 140	⊢
	: , :
78	theorem		⊢
	proveit.logic.equality.four_chain_transitivity
79	instantiation	100, 136, 168, 137, 101, 98, 129, 125, 99, 140	⊢
	: , : , : , : , : , :
80	instantiation	100, 168, 171, 101, 102, 129, 125, 115, 118, 140	⊢
	: , : , : , : , : , :
81	instantiation	150, 103, 104	⊢
	: , : , :
82	theorem		⊢
	proveit.numbers.numerals.decimals.nat5
83	instantiation	105	⊢
	: , : , : , : , :
84	instantiation	146	⊢
	: , :
85	instantiation	146	⊢
	: , :
86	instantiation	106	⊢
	: , : , :
87	theorem		⊢
	proveit.numbers.addition.leftward_commutation
88	theorem		⊢
	proveit.numbers.numerals.decimals.nat3
89	instantiation	106	⊢
	: , : , :
90	instantiation	106	⊢
	: , : , :
91	instantiation	109, 136, 144, 171, 137, 110, 140, 129, 107*	⊢
	: , : , : , : , : , :
92	theorem		⊢
	proveit.numbers.multiplication.mult_complex_closure_bin
93	instantiation	169, 148, 108	⊢
	: , : , :
94	theorem		⊢
	proveit.logic.equality.equals_reversal
95	instantiation	109, 136, 144, 171, 137, 110, 140, 125, 111*	⊢
	: , : , : , : , : , :
96	instantiation	135, 136, 168, 137, 112, 140, 113*	⊢
	: , : , : , : , : , :
97	theorem		⊢
	proveit.numbers.negation.distribute_neg_through_binary_sum
98	instantiation	146	⊢
	: , :
99	instantiation	114, 115, 118	⊢
	: , :
100	theorem		⊢
	proveit.numbers.addition.disassociation
101	instantiation	146	⊢
	: , :
102	instantiation	146	⊢
	: , :
103	instantiation	116, 136, 171, 168, 137, 117, 129, 125, 118, 140, 119	⊢
	: , : , : , : , : , : , : , :
104	instantiation	120, 140, 125, 121	⊢
	: , : , :
105	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_5_typical_eq
106	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_3_typical_eq
107	instantiation	124, 129	⊢
	:
108	instantiation	169, 158, 122	⊢
	: , : , :
109	theorem		⊢
	proveit.numbers.multiplication.distribute_through_sum
110	instantiation	123	⊢
	: , : , : , :
111	instantiation	124, 125	⊢
	:
112	instantiation	146	⊢
	: , :
113	instantiation	150, 126, 127	⊢
	: , : , :
114	theorem		⊢
	proveit.numbers.addition.add_complex_closure_bin
115	instantiation	128, 129	⊢
	:
116	theorem		⊢
	proveit.numbers.addition.subtraction.add_cancel_general
117	instantiation	146	⊢
	: , :
118	instantiation	169, 148, 130	⊢
	: , : , :
119	instantiation	131	⊢
	:
120	theorem		⊢
	proveit.numbers.addition.subtraction.add_cancel_triple_32
121	instantiation	131	⊢
	:
122	instantiation	169, 166, 132	⊢
	: , : , :
123	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_4_typical_eq
124	theorem		⊢
	proveit.numbers.multiplication.elim_one_left
125	instantiation	169, 148, 133	⊢
	: , : , :
126	instantiation	160, 134	⊢
	: , : , :
127	instantiation	135, 136, 168, 171, 137, 138, 139, 140, 141*	⊢
	: , : , : , : , : , :
128	theorem		⊢
	proveit.numbers.negation.complex_closure
129	instantiation	169, 148, 142	⊢
	: , : , :
130	instantiation	169, 158, 143	⊢
	: , : , :
131	axiom		⊢
	proveit.logic.equality.equals_reflexivity
132	instantiation	169, 170, 144	⊢
	: , : , :
133	instantiation	153, 154, 145	⊢
	: , : , :
134	theorem		⊢
	proveit.numbers.numerals.decimals.add_1_1
135	theorem		⊢
	proveit.numbers.addition.association
136	axiom		⊢
	proveit.numbers.number_sets.natural_numbers.zero_in_nats
137	theorem		⊢
	proveit.core_expr_types.tuples.tuple_len_0_typical_eq
138	instantiation	146	⊢
	: , :
139	instantiation	169, 148, 147	⊢
	: , : , :
140	instantiation	169, 148, 149	⊢
	: , : , :
141	instantiation	150, 151, 152	⊢
	: , : , :
142	instantiation	153, 154, 155	⊢
	: , : , :
143	instantiation	169, 166, 156	⊢
	: , : , :
144	theorem		⊢
	proveit.numbers.numerals.decimals.nat4
145	axiom		⊢
	proveit.physics.quantum.QPE._s_in_nat_pos
146	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
147	instantiation	169, 158, 157	⊢
	: , : , :
148	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.real_within_complex
149	instantiation	169, 158, 159	⊢
	: , : , :
150	axiom		⊢
	proveit.logic.equality.equals_transitivity
151	instantiation	160, 161	⊢
	: , : , :
152	theorem		⊢
	proveit.numbers.numerals.decimals.add_3_1
153	theorem		⊢
	proveit.logic.sets.inclusion.unfold_subset_eq
154	instantiation	162, 163	⊢
	: , :
155	axiom		⊢
	proveit.physics.quantum.QPE._t_in_natural_pos
156	instantiation	164, 167	⊢
	:
157	instantiation	169, 166, 165	⊢
	: , : , :
158	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_within_real
159	instantiation	169, 166, 167	⊢
	: , : , :
160	axiom		⊢
	proveit.logic.equality.substitution
161	theorem		⊢
	proveit.numbers.numerals.decimals.add_2_1
162	theorem		⊢
	proveit.logic.sets.inclusion.relax_proper_subset
163	theorem		⊢
	proveit.numbers.number_sets.real_numbers.nat_pos_within_real
164	theorem		⊢
	proveit.numbers.negation.int_closure
165	instantiation	169, 170, 168	⊢
	: , : , :
166	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.int_within_rational
167	instantiation	169, 170, 171	⊢
	: , : , :
168	theorem		⊢
	proveit.numbers.numerals.decimals.nat2
169	theorem		⊢
	proveit.logic.sets.inclusion.superset_membership_from_proper_subset
170	theorem		⊢
	proveit.numbers.number_sets.integers.nat_within_int
171	theorem		⊢
	proveit.numbers.numerals.decimals.nat1
*equality replacement requirements