# Theorems (or conjectures) for the theory of proveit.numbers.ordering¶

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.logic import (Forall, Not, Or, Equals, NotEquals, Iff, Implies,
InSet, Boolean, SubsetEq)
from proveit.numbers import (
Integer, IntegerNeg, IntegerNonZero, Natural, NaturalPos,
Rational,
Real, RealPos, RealNonNeg, RealNeg, RealNonPos, RealNonZero,
from proveit.numbers import Neg, Less, LessEq, greater, greater_eq, Min, Max
from proveit import a, b, c, d, n, x, y, z, S
from proveit.core_expr_types import a_1_to_n

%begin theorems

Defining theorems for theory 'proveit.numbers.ordering'
Subsequent end-of-cell assignments will define theorems
'%end theorems' will finalize the definitions

In [2]:
less_than_is_bool = Forall((x, y), InSet(Less(x, y), Boolean), domain=Real)

less_than_is_bool (conjecture without proof):

In [3]:
less_than_equals_is_bool = Forall((x, y), InSet(LessEq(x, y), Boolean), domain=Real)

less_than_equals_is_bool (conjecture without proof):

In [4]:
relax_less = Forall((x, y), LessEq(x, y), conditions=[Less(x, y)])

relax_less (conjecture without proof):

In [5]:
relax_equal_to_less_eq = Forall(
(x, y),
LessEq(x, y),
domain=Real,
conditions=[Equals(x, y)])

relax_equal_to_less_eq (conjecture without proof):

### Transitivity Theorems¶

#### Notice that transitivity_less_less is an axiom, not a theorem. The other transitivity theorems can be derived from that axiom.¶

In [6]:
# proven
transitivity_less_eq_less = Forall((x,y,z), Less(x, z), conditions=[LessEq(x,y), Less(y, z)])

transitivity_less_eq_less (conjecture with conjecture-based proof):

In [7]:
# proven
transitivity_less_less_eq = Forall((x,y,z), Less(x, z), conditions=[Less(x,y), LessEq(y, z)])

transitivity_less_less_eq (conjecture with conjecture-based proof):

In [8]:
transitivity_less_eq_less_eq = Forall((x,y,z), LessEq(x, z), conditions=[LessEq(x,y), LessEq(y, z)])

transitivity_less_eq_less_eq (conjecture with conjecture-based proof):

In [9]:
symmetric_less_eq = Forall((x,y), Equals(x, y), conditions=[LessEq(x,y), LessEq(y, x)])

symmetric_less_eq (conjecture without proof):

In [10]:
positive_if_real_pos = Forall(a, greater(a, zero), domain=RealPos)

positive_if_real_pos (conjecture without proof):

In [11]:
negative_if_real_neg = Forall(a, Less(a, zero), domain=RealNeg)

negative_if_real_neg (conjecture without proof):

In [12]:
non_neg_if_real_non_neg = Forall(a, greater_eq(a, zero), domain=RealNonNeg)

non_neg_if_real_non_neg (conjecture without proof):

In [13]:
non_pos_if_real_non_pos = Forall(a, LessEq(a, zero), domain=RealNonPos)

non_pos_if_real_non_pos (conjecture without proof):

In [14]:
less_than_successor = Forall(a, Less(a, Add(a, one)), domain=Real)

less_than_successor (conjecture without proof):

In [15]:
less_than_left_successor = Forall(a, Less(a, Add(one, a)), domain=Real)

less_than_left_successor (conjecture without proof):

In [16]:
less_than_an_increase = Forall((a, b), Less(a, Add(a, b)),
domains=(Real, RealPos))

less_than_an_increase (conjecture without proof):

In [17]:
less_than_an_left_increase = Forall((a, b), Less(a, Add(b, a)),
domains=(Real, RealPos))

less_than_an_left_increase (conjecture without proof):

In [18]:
less_eq_shift_add_right = Forall([a, b, c], LessEq(Add(a, c), Add(b, c)), domain=Real, conditions=[LessEq(a, b)])


In [19]:
less_eq_shift_add_left = Forall([a, b, c], LessEq(Add(c, a), Add(c, b)), domain=Real, conditions=[LessEq(a, b)])


In [20]:
less_shift_add_right = Forall([a, b, c], Less(Add(a, c), Add(b, c)), domain=Real, conditions=[Less(a, b)])


In [21]:
less_shift_add_left = Forall([a, b, c], Less(Add(c, a), Add(c, b)), domain=Real, conditions=[Less(a, b)])


In [22]:
less_add_both = Forall([a, b, c, d], Less(Add(a, c), Add(b, d)), domain=Real, conditions=[Less(a, b), LessEq(c, d)])


In [23]:
less_add_right = Forall([a, b, c], Less(a, Add(b, c)), domain=Real, conditions=[Less(a, b), LessEq(zero, c)])


In [24]:
less_add_left = Forall([a, b, c], Less(Add(a, c), b), domain=Real, conditions=[Less(a, b), LessEq(c, zero)])


In [25]:
less_add_right_weak = Forall([a, b, c], LessEq(a, Add(b, c)), domain=Real, conditions=[Less(a, b), LessEq(zero, c)])


In [26]:
less_add_left_weak = Forall([a, b, c], LessEq(Add(a, c), b), domain=Real, conditions=[Less(a, b), LessEq(c, zero)])


In [27]:
less_add_right_weak_int = Forall([a, b, c], LessEq(a, Add(b, c)), domain=Integer,
conditions=[Less(a, b), LessEq(Neg(one), c)])


In [28]:
less_add_left_weak_int = Forall([a, b, c], LessEq(Add(a, c), b), domain=Integer,
conditions=[Less(a, b), LessEq(c, one)])


In [29]:
less_eq_add_both = Forall([a, b, c, d], LessEq(Add(a, c), Add(b, d)), domain=Real, conditions=[LessEq(a, b), LessEq(c, d)])


In [30]:
less_eq_add_right = Forall([a, b, c], LessEq(a, Add(b, c)), domain=Real, conditions=[LessEq(a, b), LessEq(zero, c)])


In [31]:
less_eq_add_left = Forall([a, b, c], LessEq(Add(a, b), c), domain=Real, conditions=[LessEq(a, b), LessEq(c, zero)])


In [32]:
less_eq_add_right_strong = Forall([a, b, c], Less(a, Add(b, c)), domain=Real,
conditions=[LessEq(a, b), Less(zero, c)])


In [33]:
less_eq_add_left_strong = Forall([a, b, c], Less(Add(a, c), b), domain=Real,
conditions=[LessEq(a, b), Less(c, zero)])


In [34]:
less_is_not_eq_nat = Forall([a, b], NotEquals(a, b), domain=Natural, conditions=[Less(a, b)])

less_is_not_eq_nat (conjecture without proof):

In [35]:
less_is_not_eq_int = Forall([a, b], NotEquals(a, b), domain=Integer, conditions=[Less(a, b)])

less_is_not_eq_int (conjecture without proof):

In [36]:
less_is_not_eq_rational = Forall([a, b], NotEquals(a, b), domain=Rational, conditions=[Less(a, b)])

less_is_not_eq_rational (conjecture without proof):

In [37]:
less_is_not_eq = Forall([a, b], NotEquals(a, b), domain=Real, conditions=[Less(a, b)])

less_is_not_eq (conjecture without proof):

In [38]:
min_real_closure = Forall(n, Forall(a_1_to_n, InSet(Min(a_1_to_n), Real),
domain=Real),
domain=Natural)

min_real_closure (conjecture without proof):

In [39]:
max_real_closure = Forall(n, Forall(a_1_to_n, InSet(Max(a_1_to_n), Real),
domain=Real),
domain=Natural)

max_real_closure (conjecture without proof):

In [40]:
min_set_closure = (
Forall(S,
Forall(n,
Forall(a_1_to_n,
InSet(Min(a_1_to_n), S),
domain=S),
domain=Natural),
condition=SubsetEq(S, Real)))

min_set_closure (conjecture without proof):

In [41]:
max_set_closure = (
Forall(S,
Forall(n,
Forall(a_1_to_n,
InSet(Max(a_1_to_n), S),
domain=S),
domain=NaturalPos),
condition=SubsetEq(S, Real)))

max_set_closure (conjecture without proof):

In [42]:
not_equals_is_less_than_or_greater_than = (
Forall((a, x),
Or(Less(x, a), greater(x, a)),
domain=Real,
conditions=[NotEquals(x, a)]))

not_equals_is_less_than_or_greater_than (conjecture without proof):

In [43]:
less_complement_is_greater_eq = (
Forall((x, y), Equals(Not(Less(x, y)), LessEq(y, x)),
domain=Real))

less_complement_is_greater_eq (conjecture without proof):

In [44]:
less_eq_complement_is_greater = (
Forall((x, y), Equals(Not(LessEq(x, y)), Less(y, x)),
domain=Real))

less_eq_complement_is_greater (conjecture without proof):

In [45]:
less_from_not_less_eq = (
Forall((x, y),
Less(y, x),
domain=Real,
condition=Not(LessEq(x, y))))

less_from_not_less_eq (conjecture without proof):

In [46]:
less_eq_from_not_less = (
Forall((x, y),
LessEq(y, x),
domain=Real,
condition=Not(Less(x, y))))

less_eq_from_not_less (conjecture without proof):

In [47]:
not_less_from_less_eq = (
Forall((x, y),
Not(Less(y, x)),
domain=Real,
condition=LessEq(x, y)))

not_less_from_less_eq (conjecture without proof):

In [48]:
not_less_eq_from_less = (
Forall((x, y),
Not(LessEq(y, x)),
domain=Real,
condition=Less(x, y)))

not_less_eq_from_less (conjecture without proof):

In [49]:
less_or_greater_eq = Forall((x, y), Or(Less(x, y), greater_eq(x, y)),
domain=Real)

less_or_greater_eq (conjecture without proof):

In [50]:
less_eq_or_greater = Forall((x, y), Or(LessEq(x, y), greater(x, y)),
domain=Real)

less_eq_or_greater (conjecture without proof):

In [51]:
max_x_x_is_x = (
Forall(x,
Equals(Max(x, x), x),
domain=Real))

max_x_x_is_x (conjecture with conjecture-based proof):

In [52]:
min_x_x_is_x = (
Forall(x,
Equals(Min(x, x), x),
domain=Real))

min_x_x_is_x (conjecture with conjecture-based proof):

In [53]:
max_nat_n_zero_is_n = (
Forall(n,
Equals(Max(n, zero), n),
domain=Natural))

max_nat_n_zero_is_n (conjecture with conjecture-based proof):

In [54]:
min_nat_n_zero_is_zero = (
Forall(n,
Equals(Min(n, zero), zero),
domain=Natural))

min_nat_n_zero_is_zero (conjecture with conjecture-based proof):

In [55]:
max_bin_args_commute = (
Forall((x, y),
Equals(Max(x, y), Max(y, x)),
domain=Real))

max_bin_args_commute (conjecture with conjecture-based proof):

In [56]:
min_bin_args_commute = (
Forall((x, y),
Equals(Min(x, y), Min(y, x)),
domain=Real))

min_bin_args_commute (conjecture with conjecture-based proof):

In [57]:
max_y_ge_x = (
Forall((x, y),
Equals(Max(x, y), y),
domain=Real,
condition=greater_eq(y, x)))

max_y_ge_x (conjecture with conjecture-based proof):

In [58]:
min_y_le_x = (
Forall((x, y),
Equals(Min(x, y), y),
domain=Real,
condition=LessEq(y, x)))

min_y_le_x (conjecture with conjecture-based proof):

In [59]:
%end theorems

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