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
0generalization1  ⊢  
1instantiation2, 3, 4, 5, 6,  ⊢  
  : , : , :
2theorem  ⊢  
 proveit.numbers.division.weak_div_from_denom_bound__all_pos
3instantiation125, 7, 8  ⊢  
  : , : , :
4instantiation10, 55, 9,  ⊢  
  :
5instantiation10, 19, 11,  ⊢  
  :
6instantiation12, 90, 19, 55, 13, 14,  ⊢  
  : , : , :
7theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.rational_nonneg_within_real_nonneg
8instantiation125, 15, 117  ⊢  
  : , : , :
9instantiation16, 75, 17, 31,  ⊢  
  : , :
10theorem  ⊢  
 proveit.numbers.exponentiation.sqrd_pos_closure
11instantiation18, 19, 47, 20,  ⊢  
  : , :
12theorem  ⊢  
 proveit.numbers.exponentiation.exp_even_neg_base_lesseq
13instantiation21, 22, 31,  ⊢  
  : , :
14instantiation23  ⊢  
  :
15theorem  ⊢  
 proveit.numbers.number_sets.rational_numbers.nat_within_rational_nonneg
16theorem  ⊢  
 proveit.numbers.ordering.less_is_not_eq_int
17theorem  ⊢  
 proveit.numbers.number_sets.integers.zero_is_int
18theorem  ⊢  
 proveit.numbers.ordering.less_is_not_eq
19instantiation24, 55, 28,  ⊢  
  : , :
20instantiation25, 26,  ⊢  
  : , :
21theorem  ⊢  
 proveit.logic.booleans.conjunction.and_if_both
22instantiation27, 55, 28, 47, 29, 30*,  ⊢  
  : , : , :
23axiom  ⊢  
 proveit.logic.equality.equals_reflexivity
24theorem  ⊢  
 proveit.numbers.addition.add_real_closure_bin
25theorem  ⊢  
 proveit.numbers.addition.subtraction.neg_difference
26instantiation97, 31, 35,  ⊢  
  : , : , :
27theorem  ⊢  
 proveit.numbers.addition.weak_bound_via_right_term_bound
28instantiation44, 34  ⊢  
  :
29instantiation32, 33, 47, 34, 35, 36, 37*, 38*  ⊢  
  : , : , :
30instantiation39, 40,  ⊢  
  :
31instantiation41, 42, 43,  ⊢  
  : , : , :
32theorem  ⊢  
 proveit.numbers.multiplication.reversed_weak_bound_via_right_factor_bound
33instantiation44, 79  ⊢  
  :
34instantiation45, 47, 79, 48  ⊢  
  : , : , :
35instantiation46, 47, 79, 48  ⊢  
  : , : , :
36instantiation49, 50  ⊢  
  : , :
37instantiation51, 52, 53  ⊢  
  : , : , :
38instantiation54, 61  ⊢  
  :
39theorem  ⊢  
 proveit.numbers.addition.elim_zero_right
40instantiation125, 91, 55,  ⊢  
  : , : , :
41theorem  ⊢  
 proveit.numbers.ordering.transitivity_less_eq_less
42instantiation56, 95, 96, 86,  ⊢  
  : , : , :
43instantiation58, 57  ⊢  
  :
44theorem  ⊢  
 proveit.numbers.negation.real_closure
45theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.all_in_interval_co__is__real
46theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.interval_co_lower_bound
47theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.zero_is_real
48theorem  ⊢  
 proveit.physics.quantum.QPE._scaled_delta_b_floor_in_interval
49theorem  ⊢  
 proveit.numbers.ordering.relax_less
50instantiation58, 59  ⊢  
  :
51axiom  ⊢  
 proveit.logic.equality.equals_transitivity
52instantiation60, 117, 127, 70, 72, 71, 61, 73, 74  ⊢  
  : , : , : , : , : , :
53instantiation62, 70, 127, 71, 72, 68, 73, 74, 63*  ⊢  
  : , : , : , : , :
54theorem  ⊢  
 proveit.numbers.multiplication.mult_zero_right
55instantiation125, 100, 64,  ⊢  
  : , : , :
56theorem  ⊢  
 proveit.numbers.number_sets.integers.interval_upper_bound
57instantiation66, 65  ⊢  
  :
58theorem  ⊢  
 proveit.numbers.number_sets.integers.negative_if_in_neg_int
59instantiation66, 78  ⊢  
  :
60theorem  ⊢  
 proveit.numbers.multiplication.disassociation
61instantiation67, 68  ⊢  
  :
62theorem  ⊢  
 proveit.numbers.multiplication.mult_neg_any
63instantiation69, 70, 127, 71, 72, 73, 74  ⊢  
  : , : , : , :
64instantiation125, 108, 75,  ⊢  
  : , : , :
65instantiation76, 77, 78  ⊢  
  : , :
66theorem  ⊢  
 proveit.numbers.negation.int_neg_closure
67theorem  ⊢  
 proveit.numbers.negation.complex_closure
68instantiation125, 91, 79  ⊢  
  : , : , :
69theorem  ⊢  
 proveit.numbers.multiplication.elim_one_any
70axiom  ⊢  
 proveit.numbers.number_sets.natural_numbers.zero_in_nats
71theorem  ⊢  
 proveit.core_expr_types.tuples.tuple_len_0_typical_eq
72instantiation80  ⊢  
  : , :
73instantiation81, 82, 83  ⊢  
  : , :
74instantiation125, 91, 84  ⊢  
  : , : , :
75instantiation125, 85, 86,  ⊢  
  : , : , :
76theorem  ⊢  
 proveit.numbers.addition.add_nat_pos_closure_bin
77instantiation87, 111, 88  ⊢  
  :
78theorem  ⊢  
 proveit.numbers.numerals.decimals.posnat1
79instantiation125, 100, 89  ⊢  
  : , : , :
80theorem  ⊢  
 proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
81theorem  ⊢  
 proveit.numbers.exponentiation.exp_complex_closure
82instantiation125, 91, 90  ⊢  
  : , : , :
83instantiation125, 91, 92  ⊢  
  : , : , :
84instantiation93, 94  ⊢  
  :
85instantiation114, 95, 96  ⊢  
  : , :
86assumption  ⊢  
87theorem  ⊢  
 proveit.numbers.number_sets.integers.pos_int_is_natural_pos
88instantiation97, 98, 99  ⊢  
  : , : , :
89instantiation125, 108, 115  ⊢  
  : , : , :
90instantiation125, 100, 101  ⊢  
  : , : , :
91theorem  ⊢  
 proveit.numbers.number_sets.complex_numbers.real_within_complex
92instantiation102, 103, 104  ⊢  
  : , : , :
93theorem  ⊢  
 proveit.physics.quantum.QPE._delta_b_is_real
94theorem  ⊢  
 proveit.physics.quantum.QPE._best_floor_is_int
95instantiation118, 105, 115  ⊢  
  : , :
96instantiation123, 106  ⊢  
  :
97theorem  ⊢  
 proveit.numbers.ordering.transitivity_less_less_eq
98theorem  ⊢  
 proveit.numbers.numerals.decimals.less_0_1
99instantiation107, 115, 116, 113  ⊢  
  : , : , :
100theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.rational_within_real
101instantiation125, 108, 124  ⊢  
  : , : , :
102theorem  ⊢  
 proveit.logic.sets.inclusion.unfold_subset_eq
103instantiation109, 110  ⊢  
  : , :
104axiom  ⊢  
 proveit.physics.quantum.QPE._t_in_natural_pos
105instantiation123, 119  ⊢  
  :
106instantiation118, 111, 115  ⊢  
  : , :
107theorem  ⊢  
 proveit.numbers.number_sets.integers.interval_lower_bound
108theorem  ⊢  
 proveit.numbers.number_sets.rational_numbers.int_within_rational
109theorem  ⊢  
 proveit.logic.sets.inclusion.relax_proper_subset
110theorem  ⊢  
 proveit.numbers.number_sets.real_numbers.nat_pos_within_real
111instantiation125, 112, 113  ⊢  
  : , : , :
112instantiation114, 115, 116  ⊢  
  : , :
113assumption  ⊢  
114theorem  ⊢  
 proveit.numbers.number_sets.integers.int_interval_within_int
115instantiation125, 126, 117  ⊢  
  : , : , :
116instantiation118, 119, 120  ⊢  
  : , :
117theorem  ⊢  
 proveit.numbers.numerals.decimals.nat1
118theorem  ⊢  
 proveit.numbers.addition.add_int_closure_bin
119instantiation125, 121, 122  ⊢  
  : , : , :
120instantiation123, 124  ⊢  
  :
121theorem  ⊢  
 proveit.numbers.number_sets.integers.nat_pos_within_int
122theorem  ⊢  
 proveit.physics.quantum.QPE._two_pow_t_minus_one_is_nat_pos
123theorem  ⊢  
 proveit.numbers.negation.int_closure
124instantiation125, 126, 127  ⊢  
  : , : , :
125theorem  ⊢  
 proveit.logic.sets.inclusion.superset_membership_from_proper_subset
126theorem  ⊢  
 proveit.numbers.number_sets.integers.nat_within_int
127theorem  ⊢  
 proveit.numbers.numerals.decimals.nat2
*equality replacement requirements