# 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=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),
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),
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
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)])
)


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