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, 7, 8*  ⊢  
  : , : , : , :
1theorem  ⊢  
 proveit.numbers.summation.integral_upper_bound_of_sum
2theorem  ⊢  
 proveit.numbers.functions.one_over_x_sqrd_in_mon_dec_fxns
3instantiation61, 9  ⊢  
  : , :
4reference88  ⊢  
5reference82  ⊢  
6instantiation10, 91, 67, 11, 12, 13*  ⊢  
  : , : , :
7instantiation14, 15  ⊢  
  : , : , :
8instantiation20, 16, 17  ⊢  
  : , : , :
9theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.real_pos_within_real
10theorem  ⊢  
 proveit.numbers.addition.weak_bound_via_left_term_bound
11instantiation113, 95, 18  ⊢  
  : , : , :
12instantiation19, 103, 104, 98  ⊢  
  : , : , :
13instantiation20, 21, 22  ⊢  
  : , : , :
14theorem  ⊢  
 proveit.logic.sets.inclusion.fold_subset_eq
15generalization23  ⊢  
16instantiation29, 32, 115, 105, 34, 24, 27, 86, 25  ⊢  
  : , : , : , : , : , :
17instantiation26, 86, 27, 28  ⊢  
  : , : , :
18instantiation113, 101, 104  ⊢  
  : , : , :
19theorem  ⊢  
 proveit.numbers.number_sets.integers.interval_upper_bound
20axiom  ⊢  
 proveit.logic.equality.equals_transitivity
21instantiation29, 32, 115, 105, 34, 30, 35, 54, 86  ⊢  
  : , : , : , : , : , :
22instantiation31, 105, 115, 32, 33, 34, 35, 54, 86, 36*  ⊢  
  : , : , : , : , : , :
23instantiation37, 38, 39,  ⊢  
  :
24instantiation42  ⊢  
  : , :
25instantiation40, 86  ⊢  
  :
26theorem  ⊢  
 proveit.numbers.addition.subtraction.add_cancel_triple_23
27instantiation113, 90, 67  ⊢  
  : , : , :
28instantiation41  ⊢  
  :
29theorem  ⊢  
 proveit.numbers.addition.disassociation
30instantiation42  ⊢  
  : , :
31theorem  ⊢  
 proveit.numbers.addition.association
32axiom  ⊢  
 proveit.numbers.number_sets.natural_numbers.zero_in_nats
33instantiation42  ⊢  
  : , :
34theorem  ⊢  
 proveit.core_expr_types.tuples.tuple_len_0_typical_eq
35instantiation113, 90, 43  ⊢  
  : , : , :
36instantiation78, 44, 45  ⊢  
  : , : , :
37theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.pos_real_is_real_pos
38instantiation46, 58, 59, 60,  ⊢  
  : , : , :
39instantiation75, 47, 48,  ⊢  
  : , : , :
40theorem  ⊢  
 proveit.numbers.negation.complex_closure
41axiom  ⊢  
 proveit.logic.equality.equals_reflexivity
42theorem  ⊢  
 proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
43instantiation49, 50, 110  ⊢  
  : , : , :
44instantiation51, 86, 52, 53  ⊢  
  : , : , :
45instantiation85, 86, 54  ⊢  
  : , :
46theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.all_in_interval_cc__is__real
47instantiation55, 56  ⊢  
  : , :
48instantiation57, 58, 59, 60,  ⊢  
  : , : , :
49theorem  ⊢  
 proveit.logic.sets.inclusion.unfold_subset_eq
50instantiation61, 62  ⊢  
  : , :
51theorem  ⊢  
 proveit.numbers.addition.subtraction.subtract_from_add_reversed
52instantiation113, 90, 63  ⊢  
  : , : , :
53theorem  ⊢  
 proveit.numbers.numerals.decimals.add_1_1
54instantiation113, 90, 64  ⊢  
  : , : , :
55theorem  ⊢  
 proveit.numbers.addition.subtraction.pos_difference
56instantiation65, 91, 66, 67, 68, 69*  ⊢  
  : , : , :
57theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.interval_cc_lower_bound
58instantiation113, 95, 70  ⊢  
  : , : , :
59instantiation113, 95, 71  ⊢  
  : , : , :
60assumption  ⊢  
61theorem  ⊢  
 proveit.logic.sets.inclusion.relax_proper_subset
62theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.nat_pos_within_real
63instantiation113, 95, 72  ⊢  
  : , : , :
64instantiation113, 95, 73  ⊢  
  : , : , :
65theorem  ⊢  
 proveit.numbers.addition.strong_bound_via_left_term_bound
66theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.zero_is_real
67instantiation113, 95, 74  ⊢  
  : , : , :
68instantiation75, 76, 77  ⊢  
  : , : , :
69instantiation78, 79, 80  ⊢  
  : , : , :
70instantiation113, 101, 81  ⊢  
  : , : , :
71instantiation113, 101, 82  ⊢  
  : , : , :
72instantiation113, 101, 112  ⊢  
  : , : , :
73instantiation113, 101, 108  ⊢  
  : , : , :
74instantiation113, 101, 92  ⊢  
  : , : , :
75theorem  ⊢  
 proveit.numbers.ordering.transitivity_less_less_eq
76theorem  ⊢  
 proveit.numbers.numerals.decimals.less_0_1
77instantiation83, 103, 104, 98  ⊢  
  : , : , :
78theorem  ⊢  
 proveit.logic.equality.sub_right_side_into
79instantiation84, 86  ⊢  
  :
80instantiation85, 86, 87  ⊢  
  : , :
81instantiation106, 88, 89  ⊢  
  : , :
82instantiation106, 107, 89  ⊢  
  : , :
83theorem  ⊢  
 proveit.numbers.number_sets.integers.interval_lower_bound
84theorem  ⊢  
 proveit.numbers.addition.elim_zero_right
85theorem  ⊢  
 proveit.numbers.addition.commutation
86instantiation113, 90, 91  ⊢  
  : , : , :
87theorem  ⊢  
 proveit.numbers.number_sets.complex_numbers.zero_is_complex
88instantiation106, 92, 103  ⊢  
  : , :
89instantiation113, 93, 94  ⊢  
  : , : , :
90theorem  ⊢  
 proveit.numbers.number_sets.complex_numbers.real_within_complex
91instantiation113, 95, 96  ⊢  
  : , : , :
92instantiation113, 97, 98  ⊢  
  : , : , :
93theorem  ⊢  
 proveit.numbers.number_sets.integers.neg_int_within_int
94instantiation99, 100  ⊢  
  :
95theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.rational_within_real
96instantiation113, 101, 103  ⊢  
  : , : , :
97instantiation102, 103, 104  ⊢  
  : , :
98assumption  ⊢  
99theorem  ⊢  
 proveit.numbers.negation.int_neg_closure
100theorem  ⊢  
 proveit.numbers.numerals.decimals.posnat1
101theorem  ⊢  
 proveit.numbers.number_sets.rational_numbers.int_within_rational
102theorem  ⊢  
 proveit.numbers.number_sets.integers.int_interval_within_int
103instantiation113, 114, 105  ⊢  
  : , : , :
104instantiation106, 107, 108  ⊢  
  : , :
105theorem  ⊢  
 proveit.numbers.numerals.decimals.nat1
106theorem  ⊢  
 proveit.numbers.addition.add_int_closure_bin
107instantiation113, 109, 110  ⊢  
  : , : , :
108instantiation111, 112  ⊢  
  :
109theorem  ⊢  
 proveit.numbers.number_sets.integers.nat_pos_within_int
110theorem  ⊢  
 proveit.physics.quantum.QPE._two_pow_t_minus_one_is_nat_pos
111theorem  ⊢  
 proveit.numbers.negation.int_closure
112instantiation113, 114, 115  ⊢  
  : , : , :
113theorem  ⊢  
 proveit.logic.sets.inclusion.superset_membership_from_proper_subset
114theorem  ⊢  
 proveit.numbers.number_sets.integers.nat_within_int
115theorem  ⊢  
 proveit.numbers.numerals.decimals.nat2
*equality replacement requirements