logo

Theorems (or conjectures) for the theory of proveit.numbers.number_sets.real_numbers

In [1]:
import proveit
# Prepare this notebook for defining the theorems of a theory:
%theorems_notebook # Keep this at the top following 'import proveit'.
from proveit import a, b, c, n, x, y
from proveit.logic import (Implies, Forall, Iff, in_bool, InSet, 
                           Equals, NotEquals, NotInSet, Or, Set, ProperSubset)
from proveit.numbers import (num, Add, subtract, greater, greater_eq, Interval,
                             IntervalCC, IntervalCO, IntervalOC, IntervalOO,
                             Less, LessEq, Mult, Neg, number_ordering, sqrt)
from proveit.numbers import (
    zero, one, two, e, pi, ZeroSet, Complex, 
    Integer, Natural, NaturalPos, IntegerNeg, IntegerNonPos, IntegerNonZero,
    Rational, RationalNonZero, RationalPos, RationalNeg, RationalNonNeg, RationalNonPos, 
    Real, RealNonNeg, RealPos, RealNeg, RealNonPos, RealNonZero)
In [2]:
%begin theorems

Defining theorems for theory 'proveit.numbers.number_sets.real_numbers'
Subsequent end-of-cell assignments will define theorems
'%end theorems' will finalize the definitions
In [3]:
zero_is_real = InSet(zero, Real)
zero_is_real (conjecture without proof):
In [4]:
zero_is_nonneg_real = InSet(zero, RealNonNeg)
zero_is_nonneg_real (conjecture without proof):
In [5]:
zero_is_nonpos_real = InSet(zero, RealNonPos)
zero_is_nonpos_real (conjecture without proof):
In [6]:
zero_set_within_real = ProperSubset(ZeroSet, Real)
zero_set_within_real (conjecture without proof):
In [7]:
zero_set_within_real_nonneg = ProperSubset(ZeroSet, RealNonNeg)
zero_set_within_real_nonneg (conjecture without proof):
In [8]:
zero_set_within_real_nonpos = ProperSubset(ZeroSet, RealNonPos)
zero_set_within_real_nonpos (conjecture without proof):
In [9]:
int_within_real = ProperSubset(Integer, Real)
int_within_real (conjecture without proof):
In [10]:
nat_within_real = ProperSubset(Natural, Real)
nat_within_real (conjecture without proof):
In [11]:
nat_pos_within_real = ProperSubset(NaturalPos, Real)
nat_pos_within_real (conjecture without proof):
In [12]:
nat_pos_within_real_pos = ProperSubset(NaturalPos, RealPos)
nat_pos_within_real_pos (conjecture without proof):
In [13]:
nat_within_real_nonneg = ProperSubset(Natural, RealNonNeg)
nat_within_real_nonneg (conjecture without proof):
In [14]:
nat_pos_within_real_nonneg = ProperSubset(NaturalPos, RealNonNeg)
nat_pos_within_real_nonneg (conjecture without proof):
In [15]:
nonzero_int_within_real_nonzero = ProperSubset(IntegerNonZero, RealNonZero)
nonzero_int_within_real_nonzero (conjecture without proof):
In [16]:
neg_int_within_real_neg = ProperSubset(IntegerNeg, RealNeg)
neg_int_within_real_neg (conjecture without proof):
In [17]:
nonpos_int_within_real_nonpos = ProperSubset(IntegerNonPos, RealNonPos)
nonpos_int_within_real_nonpos (conjecture without proof):
In [18]:
rational_within_real = ProperSubset(Rational, Real)
rational_within_real (conjecture without proof):
In [19]:
rational_nonzero_within_real_nonzero = ProperSubset(RationalNonZero, RealNonZero)
rational_nonzero_within_real_nonzero (conjecture without proof):
In [20]:
rational_pos_within_real_pos = ProperSubset(RationalPos, RealPos)
rational_pos_within_real_pos (conjecture without proof):
In [21]:
rational_neg_within_real_neg = ProperSubset(RationalNeg, RealNeg)
rational_neg_within_real_neg (conjecture without proof):
In [22]:
rational_nonneg_within_real_nonneg = ProperSubset(RationalNonNeg, RealNonNeg)
rational_nonneg_within_real_nonneg (conjecture without proof):
In [23]:
rational_nonpos_within_real_nonpos = ProperSubset(RationalNonPos, RealNonPos)
rational_nonpos_within_real_nonpos (conjecture without proof):
In [24]:
real_nonzero_within_real = ProperSubset(RealNonZero, Real)
real_nonzero_within_real (conjecture without proof):
In [25]:
real_pos_within_real = ProperSubset(RealPos, Real)
real_pos_within_real (conjecture without proof):
In [26]:
real_pos_within_real_nonzero = ProperSubset(RealPos, RealNonZero)
real_pos_within_real_nonzero (conjecture without proof):
In [27]:
real_pos_within_real_nonneg = ProperSubset(RealPos, RealNonNeg)
real_pos_within_real_nonneg (conjecture without proof):
In [28]:
real_neg_within_real = ProperSubset(RealNeg, Real)
real_neg_within_real (conjecture without proof):
In [29]:
real_neg_within_real_nonzero = ProperSubset(RealNeg, RealNonZero)
real_neg_within_real_nonzero (conjecture without proof):
In [30]:
real_neg_within_real_nonpos = ProperSubset(RealNeg, RealNonPos)
real_neg_within_real_nonpos (conjecture without proof):
In [31]:
real_nonneg_within_real = ProperSubset(RealNonNeg, Real)
real_nonneg_within_real (conjecture without proof):
In [32]:
real_nonpos_within_real = ProperSubset(RealNonPos, Real)
real_nonpos_within_real (conjecture without proof):
In [33]:
real_nonzero_within_real = ProperSubset(RealNonZero, Real)
real_nonzero_within_real (conjecture without proof):
(alternate proof for real_nonzero_within_real)
In [34]:
nonzero_if_in_real_nonzero = Forall(x, NotEquals(x, zero), domain=RealNonZero)
nonzero_if_in_real_nonzero (conjecture without proof):
In [35]:
positive_if_in_real_pos = Forall(x, greater(x, zero), domain=RealPos)
positive_if_in_real_pos (conjecture without proof):
In [36]:
negative_if_in_real_neg = Forall(x, Less(x, zero), domain=RealNeg)
negative_if_in_real_neg (conjecture without proof):
In [37]:
nonneg_if_in_real_nonneg = Forall(x, greater_eq(x, zero), domain=RealNonNeg)
nonneg_if_in_real_nonneg (conjecture without proof):
In [38]:
nonpos_if_in_real_nonpos = Forall(x, LessEq(x, zero), domain=RealNonPos)
nonpos_if_in_real_nonpos (conjecture without proof):
In [39]:
nonpos_real_is_real_nonpos = Forall(
    a, InSet(a, RealNonPos), condition=LessEq(a, zero),
    domain=Real)
nonpos_real_is_real_nonpos (conjecture without proof):
In [40]:
pos_real_is_real_pos = Forall(a, InSet(a, RealPos), condition=greater(a, zero), domain=Real)
pos_real_is_real_pos (conjecture without proof):
In [41]:
nonzero_nonneg_real_is_real_pos = Forall(
    a, InSet(a, RealPos), condition=NotEquals(a, zero), domain=RealNonNeg)
nonzero_nonneg_real_is_real_pos (conjecture without proof):
In [42]:
neg_real_is_real_neg = Forall(a, InSet(a, RealNeg), condition=Less(a, zero), domain=Real)
neg_real_is_real_neg (conjecture without proof):
In [43]:
nonzero_nonpos_real_is_real_neg = Forall(
    a, InSet(a, RealNeg), condition=NotEquals(a, zero), domain=RealNonPos)
nonzero_nonpos_real_is_real_neg (conjecture without proof):
In [44]:
neg_is_real_neg_if_pos_is_real_pos = Forall(
    a,
    InSet(Neg(a), RealNeg),
    domain=RealPos)
neg_is_real_neg_if_pos_is_real_pos (conjecture without proof):
In [45]:
nonneg_real_is_real_nonneg = Forall(
    a, InSet(a, RealNonNeg), condition=greater_eq(a, zero),
    domain=Real)
nonneg_real_is_real_nonneg (conjecture without proof):
In [46]:
nonzero_real_is_real_nonzero = Forall(
    a, InSet(a, RealNonZero), condition=NotEquals(a, zero), 
    domain=Real)
nonzero_real_is_real_nonzero (conjecture without proof):

Non-Zero Theorems

In [47]:
positive_implies_not_zero = Forall(
    a,
    NotEquals(a, zero),
    domain=Real,
    conditions=[greater(a, zero)])
positive_implies_not_zero (conjecture without proof):
In [48]:
negative_implies_not_zero = Forall(
    a, NotEquals(a, zero),
    domain=Real,
    conditions=[Less(a, zero)])
negative_implies_not_zero (conjecture without proof):

Elements of Real Intervals are Real Numbers

In [49]:
all_in_interval_oo__is__real = Forall(
    (a, b),
    Forall(x,
           InSet(x, Real),
           domain=IntervalOO(a, b)),
    domain=Real)
all_in_interval_oo__is__real (conjecture without proof):
In [50]:
all_in_interval_co__is__real = Forall(
    (a, b),
    Forall(x,
           InSet(x, Real),
           domain=IntervalCO(a, b)),
    domain=Real)
all_in_interval_co__is__real (conjecture without proof):
In [51]:
all_in_interval_oc__is__real = Forall(
    (a, b),
    Forall(x,
           InSet(x, Real),
           domain=IntervalOC(a, b)),
    domain=Real)
all_in_interval_oc__is__real (conjecture without proof):
In [52]:
all_in_interval_cc__is__real = Forall(
    (a, b),
    Forall(x,
           InSet(x, Real),
           domain=IntervalCC(a, b)),
    domain=Real)
all_in_interval_cc__is__real (conjecture without proof):

Real Intervals are Subsets of the Real number set

In [53]:
interval_oo_within_Real = Forall(
    (a, b),
    ProperSubset(IntervalOO(a, b), Real),
    domain=Real)
interval_oo_within_Real (conjecture without proof):
In [54]:
interval_oc_within_Real = Forall(
    (a, b),
    ProperSubset(IntervalOC(a, b), Real),
    domain=Real)
interval_oc_within_Real (conjecture without proof):
In [55]:
interval_co_within_Real = Forall(
    (a, b),
    ProperSubset(IntervalCO(a, b), Real),
    domain=Real)
interval_co_within_Real (conjecture without proof):
In [56]:
interval_cc_within_Real = Forall(
    (a, b),
    ProperSubset(IntervalCC(a, b), Real),
    domain=Real)
interval_cc_within_Real (conjecture without proof):

Upper and Lower Bounds on Real Intervals

In [57]:
interval_oo_lower_bound = Forall(
    (a, b),
    Forall(x,
           Less(a, x),
           domain=IntervalOO(a, b)),
    domain=Real)
interval_oo_lower_bound (conjecture without proof):
In [58]:
interval_oo_upper_bound = Forall(
    (a, b),
    Forall(x,
           Less(x, b),
           domain=IntervalOO(a, b)),
    domain=Real)
interval_oo_upper_bound (conjecture without proof):
In [59]:
interval_co_lower_bound = Forall(
    (a, b),
    Forall(x,
           LessEq(a, x),
           domain=IntervalCO(a, b)),
    domain=Real)
interval_co_lower_bound (conjecture without proof):
In [60]:
interval_co_upper_bound = Forall(
    (a, b),
    Forall(x,
           Less(x, b),
           domain=IntervalCO(a, b)),
    domain=Real)
interval_co_upper_bound (conjecture without proof):
In [61]:
interval_oc_lower_bound = Forall(
    (a, b),
    Forall(x,
           Less(a, x),
           domain=IntervalOC(a, b)),
    domain=Real)
interval_oc_lower_bound (conjecture without proof):
In [62]:
interval_oc_upper_bound = Forall(
    (a, b),
    Forall(x,
           LessEq(x, b),
           domain=IntervalOC(a, b)),
    domain=Real)
interval_oc_upper_bound (conjecture without proof):
In [63]:
interval_cc_lower_bound = Forall(
    (a, b),
    Forall(x,
           LessEq(a, x),
           domain=IntervalCC(a, b)),
    domain=Real)
interval_cc_lower_bound (conjecture without proof):
In [64]:
interval_cc_upper_bound = Forall(
    (a, b),
    Forall(x,
           LessEq(x, b),
           domain=IntervalCC(a, b)),
    domain=Real)
interval_cc_upper_bound (conjecture without proof):

Translating Boundedness to Interval Membership

In [65]:
in_IntervalOO = Forall(
    (a, b, x),
    InSet(x, IntervalOO(a, b)),
    domain=Real,
    conditions=[number_ordering(Less(a, x), Less(x, b))])
in_IntervalOO (conjecture without proof):
In [66]:
in_IntervalCO = Forall(
    (a, b, x),
    InSet(x, IntervalCO(a, b)),
    domain=Real,
    conditions=[number_ordering(LessEq(a, x), Less(x, b))])
in_IntervalCO (conjecture without proof):
In [67]:
in_IntervalOC = Forall(
    (a, b, x),
    InSet(x, IntervalOC(a, b)),
    domain=Real,
    conditions=[number_ordering(Less(a, x), LessEq(x, b))])
in_IntervalOC (conjecture without proof):
In [68]:
in_IntervalCC = Forall(
    (a, b, x),
    InSet(x, IntervalCC(a, b)),
    domain=Real,
    conditions=[number_ordering(LessEq(a, x), LessEq(x, b))])
in_IntervalCC (conjecture without proof):

Scaling Elements of Intervals To Scaled Intervals

In [69]:
rescale_interval_oo_membership = Forall(
    (a, b, c),
    Forall(x,
           InSet(Mult(c, x), IntervalOO(Mult(c, a), Mult(c, b))),
           domain=IntervalOO(a, b)),
    domain=Real)
rescale_interval_oo_membership (conjecture without proof):
In [70]:
rescale_interval_oc_membership = Forall(
    (a, b, c),
    Forall(x,
           InSet(Mult(c, x),
                 IntervalOC(Mult(c, a), Mult(c, b))),
           domain=IntervalOC(a, b)),
    domain=Real)
rescale_interval_oc_membership (conjecture without proof):
In [71]:
rescale_interval_co_membership = Forall(
    (a, b, c),
    Forall(x,
           InSet(Mult(c, x), IntervalCO(Mult(c, a), Mult(c, b))),
           domain=IntervalCO(a, b)),
    domain=Real)
rescale_interval_co_membership (conjecture without proof):
In [72]:
rescale_interval_cc_membership = Forall(
    (a, b, c),
    Forall(x,
           InSet(Mult(c, x), IntervalCC(Mult(c, a), Mult(c, b))),
           domain=IntervalCC(a, b)),
    domain=Real)
rescale_interval_cc_membership (conjecture without proof):

Interval Relaxation Theorems

In [73]:
relax_IntervalCO = Forall(
    (a, b),
    Forall(x,
           InSet(x, IntervalCC(a, b)),
           domain=IntervalCO(a, b)),
    domain=Real)
relax_IntervalCO (conjecture without proof):
In [74]:
relax_IntervalOC = Forall(
    (a, b),
    Forall(x,
           InSet(x, IntervalCC(a, b)),
           domain=IntervalOC(a, b)),
    domain=Real)
relax_IntervalOC (conjecture without proof):
In [75]:
relax_IntervalOO_left = Forall(
    (a, b),
    Forall(x,
           InSet(x, IntervalCO(a, b)),
           domain=IntervalOO(a, b)),
    domain=Real)
relax_IntervalOO_left (conjecture without proof):
In [76]:
relax_IntervalOO_right = Forall(
    (a, b),
    Forall(x,
           InSet(x, IntervalOC(a, b)),
           domain=IntervalOO(a, b)),
    domain=Real)
relax_IntervalOO_right (conjecture without proof):
In [77]:
relax_IntervalOO_left_right = Forall(
    (a, b),
    Forall(x,
           InSet(x, IntervalCC(a, b)),
           domain=IntervalOO(a, b)),
    domain=Real)
relax_IntervalOO_left_right (conjecture without proof):
In [ ]:

Some Analogous Non-IntervalMembership Theorems

In [78]:
not_real_not_in_interval_oo = (
    Forall((a, b),
           Forall(x, NotInSet(x, IntervalOO(a, b)), domain=Complex, condition=NotInSet(x, Real)),
           domain=Real))
not_real_not_in_interval_oo (conjecture without proof):
In [79]:
not_real_not_in_interval_co = (
    Forall((a, b),
           Forall(x, NotInSet(x, IntervalCO(a, b)), domain=Complex, condition=NotInSet(x, Real)),
           domain=Real))
not_real_not_in_interval_co (conjecture without proof):
In [80]:
not_real_not_in_interval_oc = (
    Forall((a, b),
           Forall(x, NotInSet(x, IntervalOC(a, b)), domain=Complex, condition=NotInSet(x, Real)),
           domain=Real))
not_real_not_in_interval_oc (conjecture without proof):
In [81]:
not_real_not_in_interval_cc = (
    Forall((a, b),
           Forall(x, NotInSet(x, IntervalCC(a, b)), domain=Complex, condition=NotInSet(x, Real)),
           domain=Real))
not_real_not_in_interval_cc (conjecture without proof):
In [82]:
real_not_in_interval_oo = (
    Forall((a, b, x),
           NotInSet(x, IntervalOO(a, b)),
           domain=Real,
           conditions=[Or(LessEq(x, a), LessEq(b, x))]))
real_not_in_interval_oo (conjecture without proof):
In [83]:
real_not_in_interval_co = (
    Forall((a, b, x),
           NotInSet(x, IntervalCO(a, b)),
           domain=Real,
           conditions=[Or(Less(x, a), LessEq(b, x))]))
real_not_in_interval_co (conjecture without proof):
In [84]:
real_not_in_interval_oc = (
    Forall((a, b, x),
           NotInSet(x, IntervalOC(a, b)),
           domain=Real,
           conditions=[Or(LessEq(x, a), Less(b, x))]))
real_not_in_interval_oc (conjecture without proof):
In [85]:
real_not_in_interval_cc = (
    Forall((a, b, x),
           NotInSet(x, IntervalCC(a, b)),
           domain=Real,
           conditions=[Or(Less(x, a), Less(b, x))]))
real_not_in_interval_cc (conjecture without proof):
In [86]:
bounds_for_real_not_in_interval_oo = (
    Forall((a, b, x),
           Or(LessEq(x, a), LessEq(b, x)),
           domain=Real,
           conditions=[NotInSet(x, IntervalOO(a, b))]))
bounds_for_real_not_in_interval_oo (conjecture without proof):
In [87]:
bounds_for_real_not_in_interval_co = (
    Forall((a, b, x),
           Or(Less(x, a), LessEq(b, x)),
           domain=Real,
           conditions=[NotInSet(x, IntervalCO(a, b))]))
bounds_for_real_not_in_interval_co (conjecture without proof):
In [88]:
bounds_for_real_not_in_interval_oc = (
    Forall((a, b, x),
           Or(LessEq(x, a), Less(b, x)),
           domain=Real,
           conditions=[NotInSet(x, IntervalOC(a, b))]))
bounds_for_real_not_in_interval_oc (conjecture without proof):
In [89]:
bounds_for_real_not_in_interval_cc = (
    Forall((a, b, x),
           Or(Less(x, a), Less(b, x)),
           domain=Real,
           conditions=[NotInSet(x, IntervalCC(a, b))]))
bounds_for_real_not_in_interval_cc (conjecture without proof):

Misc Theorems About the Real number set

In [90]:
not_int_if_between_successive_int = Forall(
    n,
    Forall(x,
           NotInSet(x, Integer),
           domain=IntervalOO(n, Add(n, one))),
    domain=Integer)
not_int_if_between_successive_int (conjecture without proof):
In [91]:
unique_int_in_interval = Forall((a, b, x, y),
       Implies(InSet(y, IntervalOO(subtract(x, a), Add(x, b) )),
               Equals(y, x)),
       domains=[RealPos, RealPos, Integer, Integer],
       conditions=[LessEq(a, one), LessEq(b, one)])
unique_int_in_interval (conjecture without proof):
In [92]:
not_int_if_not_int_in_interval = Forall(
    n,
    Forall(x,
           NotInSet(x, Integer),
           domain=IntervalOO(subtract(n, one), Add(n, one)),
           condition=NotEquals(x, n)),
    domain=Integer)
not_int_if_not_int_in_interval (conjecture without proof):
In [93]:
not_int_if_not_int_in_interval_gen = Forall(
    (a, b),
    Forall(x,
           NotInSet(x, Integer),
           domain=IntervalOO(a, b),
           condition=NotInSet(x, Interval(Add(a, one), subtract(b, one)))),
    domain=Integer)
not_int_if_not_int_in_interval_gen (conjecture without proof):
In [94]:
from proveit.logic import Intersect, Set
from proveit.numbers import IntervalOO
unique_int_in_radius_one_open_interval = (
    Forall((a,b),
       Forall(x,
              Equals(Intersect(IntervalOO(subtract(x, a), Add(x, b)), Integer), Set(x)),
              domain=Integer),
       domain=RealPos,
       conditions=[LessEq(a, one), LessEq(b, one)])
)
unique_int_in_radius_one_open_interval (conjecture without proof):
In [95]:
e_is_real_pos = InSet(e, RealPos)
e_is_real_pos (conjecture without proof):
In [96]:
pi_is_real_pos = InSet(pi, RealPos)
pi_is_real_pos (conjecture without proof):

A set of membership_is_bool (and nonmembership_is_bool) theorems, which are accessed by the respective NumberSets to implement their deduce_membership_in_bool() methods, covering the Real, RealPos, RealNeg, RealNonNeg, RealNonPos, and RealNonZero NumberSet classes (defined in proveit.numbers.number_sets.real_numbers/reals.py), as well as the various IntervalXX intervals:

In [97]:
real_membership_is_bool = Forall(x, in_bool(InSet(x, Real)))
real_membership_is_bool (conjecture without proof):
In [98]:
real_pos_membership_is_bool = Forall(x, in_bool(InSet(x, RealPos)))
real_pos_membership_is_bool (conjecture without proof):
In [99]:
real_neg_membership_is_bool = Forall(x, in_bool(InSet(x, RealNeg)))
real_neg_membership_is_bool (conjecture without proof):
In [100]:
real_nonneg_membership_is_bool = Forall(x, in_bool(InSet(x, RealNonNeg)))
real_nonneg_membership_is_bool (conjecture without proof):
In [101]:
real_nonpos_membership_is_bool = Forall(x, in_bool(InSet(x, RealNonPos)))
real_nonpos_membership_is_bool (conjecture without proof):
In [102]:
real_nonzero_membership_is_bool = Forall(x, in_bool(InSet(x, RealNonZero)))
real_nonzero_membership_is_bool (conjecture without proof):
In [103]:
interval_oo_membership_is_bool = Forall((a, b),
       Forall(x,
              in_bool(InSet(x, IntervalOO(a, b)))),
       domain = Real)
interval_oo_membership_is_bool (conjecture without proof):
In [104]:
interval_co_membership_is_bool = Forall((a, b),
       Forall(x,
              in_bool(InSet(x, IntervalCO(a, b)))),
       domain = Real)
interval_co_membership_is_bool (conjecture without proof):
In [105]:
interval_oc_membership_is_bool = Forall((a, b),
       Forall(x,
              in_bool(InSet(x, IntervalOC(a, b)))),
       domain = Real)
interval_oc_membership_is_bool (conjecture without proof):
In [106]:
interval_cc_membership_is_bool = Forall((a, b),
       Forall(x,
              in_bool(InSet(x, IntervalCC(a, b)))),
       domain = Real)
interval_cc_membership_is_bool (conjecture without proof):
In [107]:
interval_oo_nonmembership_is_bool = Forall((a, b),
       Forall(x,
              in_bool(NotInSet(x, IntervalOO(a, b)))),
       domain = Real)
interval_oo_nonmembership_is_bool (conjecture without proof):
In [108]:
interval_co_nonmembership_is_bool = Forall((a, b),
       Forall(x,
              in_bool(NotInSet(x, IntervalCO(a, b)))),
       domain = Real)
interval_co_nonmembership_is_bool (conjecture without proof):
In [109]:
interval_oc_nonmembership_is_bool = Forall((a, b),
       Forall(x,
              in_bool(NotInSet(x, IntervalOC(a, b)))),
       domain = Real)
interval_oc_nonmembership_is_bool (conjecture without proof):
In [110]:
interval_cc_nonmembership_is_bool = Forall((a, b),
       Forall(x,
              in_bool(NotInSet(x, IntervalCC(a, b)))),
       domain = Real)
interval_cc_nonmembership_is_bool (conjecture without proof):
In [ ]:
In [111]:
pi_between_3_and_4 = number_ordering(Less(num(3), pi), Less(pi, num(4)))
pi_between_3_and_4 (conjecture without proof):
In [112]:
%end theorems

These theorems may now be imported from the theory package: proveit.numbers.number_sets.real_numbers