logo

Show the Proof

In [1]:
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
Out[1]:
 step typerequirementsstatement
0instantiation1, 2, 3, 4, 5, 6  ⊢  
  : , : , :
1theorem  ⊢  
 proveit.numbers.multiplication.weak_bound_via_right_factor_bound
2instantiation173, 154, 7  ⊢  
  : , : , :
3modus ponens8, 9  ⊢  
4instantiation31, 145, 107, 10  ⊢  
  : , :
5instantiation11, 12, 13  ⊢  
  : , : , :
6instantiation43, 14  ⊢  
  : , :
7instantiation173, 15, 30  ⊢  
  : , : , :
8instantiation16  ⊢  
  : , : , :
9generalization17  ⊢  
10instantiation18, 131  ⊢  
  :
11theorem  ⊢  
 proveit.numbers.ordering.transitivity_less_eq_less_eq
12instantiation19, 20, 21, 136, 123, 22, 23, 24*  ⊢  
  : , : , : , :
13instantiation25, 26, 27, 28  ⊢  
  : , :
14instantiation29, 30  ⊢  
  :
15theorem  ⊢  
 proveit.numbers.number_sets.rational_numbers.rational_pos_within_rational
16theorem  ⊢  
 proveit.numbers.summation.summation_real_closure
17instantiation31, 145, 32, 33,  ⊢  
  : , :
18theorem  ⊢  
 proveit.numbers.number_sets.natural_numbers.nonzero_if_is_nat_pos
19theorem  ⊢  
 proveit.numbers.summation.integral_upper_bound_of_sum
20theorem  ⊢  
 proveit.numbers.functions.one_over_x_sqrd_in_mon_dec_fxns
21instantiation138, 34  ⊢  
  : , :
22instantiation35, 145, 107, 79, 80, 71*  ⊢  
  : , : , :
23instantiation36, 37  ⊢  
  : , : , :
24instantiation81, 38, 39  ⊢  
  : , : , :
25theorem  ⊢  
 proveit.numbers.integration.boundedInvSqrdIntegral
26instantiation173, 40, 41  ⊢  
  : , : , :
27instantiation65, 90, 42  ⊢  
  :
28instantiation43, 59  ⊢  
  : , :
29theorem  ⊢  
 proveit.numbers.number_sets.rational_numbers.positive_if_in_rational_pos
30instantiation44, 45, 46  ⊢  
  : , :
31theorem  ⊢  
 proveit.numbers.division.div_real_closure
32instantiation47, 48, 175,  ⊢  
  : , :
33instantiation49, 50, 51,  ⊢  
  : , :
34theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.real_pos_within_real
35theorem  ⊢  
 proveit.numbers.addition.weak_bound_via_left_term_bound
36theorem  ⊢  
 proveit.logic.sets.inclusion.fold_subset_eq
37generalization52  ⊢  
38instantiation94, 97, 175, 165, 99, 53, 56, 134, 54  ⊢  
  : , : , : , : , : , :
39instantiation55, 134, 56, 57  ⊢  
  : , : , :
40theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.rational_pos_within_real_pos
41instantiation173, 60, 131  ⊢  
  : , : , :
42instantiation58, 143, 59  ⊢  
  : , : , :
43theorem  ⊢  
 proveit.numbers.ordering.relax_less
44theorem  ⊢  
 proveit.numbers.division.div_rational_pos_closure
45instantiation173, 60, 158  ⊢  
  : , : , :
46instantiation173, 60, 74  ⊢  
  : , : , :
47theorem  ⊢  
 proveit.numbers.exponentiation.exp_real_closure_nat_power
48instantiation173, 154, 61,  ⊢  
  : , : , :
49theorem  ⊢  
 proveit.numbers.exponentiation.exp_rational_non_zero__not_zero
50instantiation173, 63, 62,  ⊢  
  : , : , :
51instantiation173, 63, 64  ⊢  
  : , : , :
52instantiation65, 66, 67,  ⊢  
  :
53instantiation111  ⊢  
  : , :
54instantiation68, 134  ⊢  
  :
55theorem  ⊢  
 proveit.numbers.addition.subtraction.add_cancel_triple_23
56instantiation173, 144, 107  ⊢  
  : , : , :
57instantiation69  ⊢  
  :
58axiom  ⊢  
 proveit.numbers.ordering.transitivity_less_less
59instantiation119, 70, 71  ⊢  
  : , : , :
60theorem  ⊢  
 proveit.numbers.number_sets.rational_numbers.nat_pos_within_rational_pos
61instantiation173, 161, 84,  ⊢  
  : , : , :
62instantiation173, 73, 72,  ⊢  
  : , : , :
63theorem  ⊢  
 proveit.numbers.number_sets.rational_numbers.nonzero_int_within_rational_nonzero
64instantiation173, 73, 74  ⊢  
  : , : , :
65theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.pos_real_is_real_pos
66instantiation75, 89, 90, 91,  ⊢  
  : , : , :
67instantiation151, 76, 77,  ⊢  
  : , : , :
68theorem  ⊢  
 proveit.numbers.negation.complex_closure
69axiom  ⊢  
 proveit.logic.equality.equals_reflexivity
70instantiation78, 107, 79, 145, 80, 152  ⊢  
  : , : , :
71instantiation81, 82, 83  ⊢  
  : , : , :
72instantiation142, 84, 85,  ⊢  
  :
73theorem  ⊢  
 proveit.numbers.number_sets.integers.nat_pos_within_nonzero_int
74theorem  ⊢  
 proveit.numbers.numerals.decimals.posnat2
75theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.all_in_interval_cc__is__real
76instantiation86, 87  ⊢  
  : , :
77instantiation88, 89, 90, 91,  ⊢  
  : , : , :
78theorem  ⊢  
 proveit.numbers.ordering.less_eq_add_right_strong
79instantiation173, 154, 92  ⊢  
  : , : , :
80instantiation93, 163, 164, 160  ⊢  
  : , : , :
81axiom  ⊢  
 proveit.logic.equality.equals_transitivity
82instantiation94, 97, 175, 165, 99, 95, 100, 129, 134  ⊢  
  : , : , : , : , : , :
83instantiation96, 165, 175, 97, 98, 99, 100, 129, 134, 101*  ⊢  
  : , : , : , : , : , :
84instantiation173, 102, 117,  ⊢  
  : , : , :
85instantiation151, 103, 104,  ⊢  
  : , : , :
86theorem  ⊢  
 proveit.numbers.addition.subtraction.pos_difference
87instantiation105, 145, 106, 107, 143, 108*  ⊢  
  : , : , :
88theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.interval_cc_lower_bound
89instantiation173, 154, 109  ⊢  
  : , : , :
90instantiation173, 154, 110  ⊢  
  : , : , :
91assumption  ⊢  
92instantiation173, 161, 164  ⊢  
  : , : , :
93theorem  ⊢  
 proveit.numbers.number_sets.integers.interval_upper_bound
94theorem  ⊢  
 proveit.numbers.addition.disassociation
95instantiation111  ⊢  
  : , :
96theorem  ⊢  
 proveit.numbers.addition.association
97axiom  ⊢  
 proveit.numbers.number_sets.natural_numbers.zero_in_nats
98instantiation111  ⊢  
  : , :
99theorem  ⊢  
 proveit.core_expr_types.tuples.tuple_len_0_typical_eq
100instantiation173, 144, 112  ⊢  
  : , : , :
101instantiation119, 113, 114  ⊢  
  : , : , :
102instantiation162, 136, 123  ⊢  
  : , :
103instantiation115, 116  ⊢  
  :
104instantiation159, 136, 123, 117,  ⊢  
  : , : , :
105theorem  ⊢  
 proveit.numbers.addition.strong_bound_via_left_term_bound
106theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.zero_is_real
107instantiation173, 154, 118  ⊢  
  : , : , :
108instantiation119, 120, 121  ⊢  
  : , : , :
109instantiation173, 161, 122  ⊢  
  : , : , :
110instantiation173, 161, 123  ⊢  
  : , : , :
111theorem  ⊢  
 proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
112instantiation124, 125, 170  ⊢  
  : , : , :
113instantiation126, 134, 127, 128  ⊢  
  : , : , :
114instantiation133, 134, 129  ⊢  
  : , :
115theorem  ⊢  
 proveit.numbers.number_sets.natural_numbers.natural_pos_is_pos
116instantiation130, 131, 158  ⊢  
  : , :
117assumption  ⊢  
118instantiation173, 161, 146  ⊢  
  : , : , :
119theorem  ⊢  
 proveit.logic.equality.sub_right_side_into
120instantiation132, 134  ⊢  
  :
121instantiation133, 134, 135  ⊢  
  : , :
122instantiation166, 136, 137  ⊢  
  : , :
123instantiation166, 167, 137  ⊢  
  : , :
124theorem  ⊢  
 proveit.logic.sets.inclusion.unfold_subset_eq
125instantiation138, 139  ⊢  
  : , :
126theorem  ⊢  
 proveit.numbers.addition.subtraction.subtract_from_add_reversed
127instantiation173, 144, 140  ⊢  
  : , : , :
128theorem  ⊢  
 proveit.numbers.numerals.decimals.add_1_1
129instantiation173, 144, 141  ⊢  
  : , : , :
130theorem  ⊢  
 proveit.numbers.addition.add_nat_pos_closure_bin
131instantiation142, 146, 143  ⊢  
  :
132theorem  ⊢  
 proveit.numbers.addition.elim_zero_right
133theorem  ⊢  
 proveit.numbers.addition.commutation
134instantiation173, 144, 145  ⊢  
  : , : , :
135theorem  ⊢  
 proveit.numbers.number_sets.complex_numbers.zero_is_complex
136instantiation166, 146, 163  ⊢  
  : , :
137instantiation173, 147, 148  ⊢  
  : , : , :
138theorem  ⊢  
 proveit.logic.sets.inclusion.relax_proper_subset
139theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.nat_pos_within_real
140instantiation173, 154, 149  ⊢  
  : , : , :
141instantiation173, 154, 150  ⊢  
  : , : , :
142theorem  ⊢  
 proveit.numbers.number_sets.integers.pos_int_is_natural_pos
143instantiation151, 152, 153  ⊢  
  : , : , :
144theorem  ⊢  
 proveit.numbers.number_sets.complex_numbers.real_within_complex
145instantiation173, 154, 155  ⊢  
  : , : , :
146instantiation173, 156, 160  ⊢  
  : , : , :
147theorem  ⊢  
 proveit.numbers.number_sets.integers.neg_int_within_int
148instantiation157, 158  ⊢  
  :
149instantiation173, 161, 172  ⊢  
  : , : , :
150instantiation173, 161, 168  ⊢  
  : , : , :
151theorem  ⊢  
 proveit.numbers.ordering.transitivity_less_less_eq
152theorem  ⊢  
 proveit.numbers.numerals.decimals.less_0_1
153instantiation159, 163, 164, 160  ⊢  
  : , : , :
154theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.rational_within_real
155instantiation173, 161, 163  ⊢  
  : , : , :
156instantiation162, 163, 164  ⊢  
  : , :
157theorem  ⊢  
 proveit.numbers.negation.int_neg_closure
158theorem  ⊢  
 proveit.numbers.numerals.decimals.posnat1
159theorem  ⊢  
 proveit.numbers.number_sets.integers.interval_lower_bound
160assumption  ⊢  
161theorem  ⊢  
 proveit.numbers.number_sets.rational_numbers.int_within_rational
162theorem  ⊢  
 proveit.numbers.number_sets.integers.int_interval_within_int
163instantiation173, 174, 165  ⊢  
  : , : , :
164instantiation166, 167, 168  ⊢  
  : , :
165theorem  ⊢  
 proveit.numbers.numerals.decimals.nat1
166theorem  ⊢  
 proveit.numbers.addition.add_int_closure_bin
167instantiation173, 169, 170  ⊢  
  : , : , :
168instantiation171, 172  ⊢  
  :
169theorem  ⊢  
 proveit.numbers.number_sets.integers.nat_pos_within_int
170theorem  ⊢  
 proveit.physics.quantum.QPE._two_pow_t_minus_one_is_nat_pos
171theorem  ⊢  
 proveit.numbers.negation.int_closure
172instantiation173, 174, 175  ⊢  
  : , : , :
173theorem  ⊢  
 proveit.logic.sets.inclusion.superset_membership_from_proper_subset
174theorem  ⊢  
 proveit.numbers.number_sets.integers.nat_within_int
175theorem  ⊢  
 proveit.numbers.numerals.decimals.nat2
*equality replacement requirements