# Theorems (or conjectures) for the theory of proveit.numbers.number_sets.rational_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, q, x
from proveit.logic import And, Equals, NotEquals, Exists, Forall, Iff, in_bool, InSet, Set, ProperSubset
from proveit.numbers import frac, GCD, Less, LessEq, greater, greater_eq
from proveit.numbers import one, zero
from proveit.numbers import (ZeroSet, Natural, NaturalPos, Integer, IntegerNonZero, IntegerNeg, IntegerNonPos,
Rational, RationalPos, RationalNeg,
RationalNonNeg, RationalNonPos, RationalNonZero, NaturalPos)

In [2]:
%begin theorems

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

In [3]:
zero_is_rational = InSet(zero, Rational)

zero_is_rational (conjecture without proof):

In [4]:
zero_is_nonneg_rational = InSet(zero, RationalNonNeg)

zero_is_nonneg_rational (conjecture without proof):

In [5]:
zero_is_nonpos_rational = InSet(zero, RationalNonPos)

zero_is_nonpos_rational (conjecture without proof):

In [6]:
zero_set_within_rational = ProperSubset(ZeroSet, Rational)

zero_set_within_rational (conjecture without proof):

In [7]:
zero_set_within_rational_nonneg = ProperSubset(ZeroSet, RationalNonNeg)

zero_set_within_rational_nonneg (conjecture without proof):

In [8]:
zero_set_within_rational_nonpos = ProperSubset(ZeroSet, RationalNonPos)

zero_set_within_rational_nonpos (conjecture without proof):

In [9]:
nat_within_rational = ProperSubset(Natural, Rational)

nat_within_rational (conjecture without proof):

In [10]:
nat_within_rational_nonneg = ProperSubset(Natural, RationalNonNeg)

nat_within_rational_nonneg (conjecture without proof):

In [11]:
nat_pos_within_rational_pos = ProperSubset(NaturalPos, RationalPos)

nat_pos_within_rational_pos (conjecture without proof):

In [12]:
nat_within_rational_nonneg = ProperSubset(Natural, RationalNonNeg)

nat_within_rational_nonneg (conjecture without proof):

(alternate proof for nat_within_rational_nonneg)
In [13]:
int_within_rational = ProperSubset(Integer, Rational)

int_within_rational (conjecture without proof):

In [14]:
nonzero_int_within_rational_nonzero = ProperSubset(IntegerNonZero, RationalNonZero)

nonzero_int_within_rational_nonzero (conjecture without proof):

In [15]:
neg_int_within_rational_neg = ProperSubset(IntegerNeg, RationalNeg)

neg_int_within_rational_neg (conjecture without proof):

In [16]:
nonpos_int_within_rational_nonpos = ProperSubset(IntegerNonPos, RationalNonPos)

nonpos_int_within_rational_nonpos (conjecture without proof):

In [17]:
rational_nonzero_within_rational = ProperSubset(RationalNonZero, Rational)

rational_nonzero_within_rational (conjecture without proof):

In [18]:
rational_pos_within_rational = ProperSubset(RationalPos, Rational)

rational_pos_within_rational (conjecture without proof):

In [19]:
rational_pos_within_rational_nonzero = ProperSubset(RationalPos, RationalNonZero)

rational_pos_within_rational_nonzero (conjecture without proof):

In [20]:
rational_neg_within_rational_nonzero = ProperSubset(RationalNeg, RationalNonZero)

rational_neg_within_rational_nonzero (conjecture without proof):

In [21]:
rational_pos_within_rational_nonneg = ProperSubset(RationalPos, RationalNonNeg)

rational_pos_within_rational_nonneg (conjecture without proof):

In [22]:
rational_neg_within_rational_nonpos = ProperSubset(RationalNeg, RationalNonPos)

rational_neg_within_rational_nonpos (conjecture without proof):

In [23]:
rational_neg_within_rational = ProperSubset(RationalNeg, Rational)

rational_neg_within_rational (conjecture without proof):

In [24]:
rational_nonneg_within_rational = ProperSubset(RationalNonNeg, Rational)

rational_nonneg_within_rational (conjecture without proof):

In [25]:
rational_nonpos_within_rational = ProperSubset(RationalNonPos, Rational)

rational_nonpos_within_rational (conjecture without proof):

In [26]:
nonzero_if_in_rational_nonzero = Forall(
q,
NotEquals(q, zero),
domain=RationalNonZero)

nonzero_if_in_rational_nonzero (conjecture without proof):

In [27]:
positive_if_in_rational_pos = Forall(
q,
greater(q, zero),
domain=RationalPos)

positive_if_in_rational_pos (conjecture without proof):

In [28]:
negative_if_in_rational_neg = Forall(
q,
Less(q, zero),
domain=RationalNeg)

negative_if_in_rational_neg (conjecture without proof):

In [29]:
nonneg_if_in_rational_nonneg = Forall(
q,
greater_eq(q, zero),
domain=RationalNonNeg)

nonneg_if_in_rational_nonneg (conjecture without proof):

In [30]:
nonpos_if_in_rational_nonpos = Forall(
q,
LessEq(q, zero),
domain=RationalNonPos)

nonpos_if_in_rational_nonpos (conjecture without proof):

In [31]:
nonzero_rational_is_rational_nonzero = Forall(
q,
InSet(q, RationalNonZero),
domain=Rational,
conditions=[NotEquals(q, zero)])

nonzero_rational_is_rational_nonzero (conjecture without proof):

In [32]:
pos_rational_is_rational_pos = Forall(
q, InSet(q, RationalPos), condition=greater(q, zero),
domain=Rational)

pos_rational_is_rational_pos (conjecture without proof):

In [33]:
nonzero_nonneg_rational_is_rational_pos = Forall(
q, InSet(q, RationalPos), condition=NotEquals(q, zero),
domain=RationalNonNeg)

nonzero_nonneg_rational_is_rational_pos (conjecture without proof):

In [34]:
neg_rational_is_rational_neg = Forall(
q,
InSet(q, RationalNeg),
domain=Rational,
conditions=[Less(q, zero)])

neg_rational_is_rational_neg (conjecture without proof):

In [35]:
nonzero_nonpos_rational_is_rational_neg = Forall(
q, InSet(q, RationalNeg),
domain=RationalNonPos, condition=NotEquals(q, zero))

nonzero_nonpos_rational_is_rational_neg (conjecture without proof):

In [36]:
nonneg_rational_is_rational_nonneg = Forall(
q,
InSet(q, RationalNonNeg),
domain=Rational,
conditions=[greater_eq(q, zero)])

nonneg_rational_is_rational_nonneg (conjecture without proof):

In [37]:
nonpos_rational_is_rational_nonpos = Forall(
q,
InSet(q, RationalNonPos),
domain=Rational,
conditions=[LessEq(q, zero)])

nonpos_rational_is_rational_nonpos (conjecture without proof):

In [38]:
nat_ratio = Forall(
q,
Exists([a,b],
Equals(q, frac(a,b)),
domains=[Natural, NaturalPos]),
domain=RationalNonNeg)

nat_ratio (conjecture without proof):

In [39]:
reduced_nat_pos_ratio = Forall(
q,
Exists([a,b],
And(Equals(q, frac(a,b)), Equals(GCD(a, b), one)),
domains=[NaturalPos, NaturalPos]),
domain=RationalPos)

reduced_nat_pos_ratio (conjecture without proof):

In [40]:
ratio_of_pos_int_is_rational_pos = Forall(
[a,b],
InSet(frac(a,b), RationalPos),
domain=NaturalPos)

ratio_of_pos_int_is_rational_pos (conjecture without proof):

A set of in_bool theorems, which are accessed by the respective NumberSets to implement their deduce_membership_in_bool() methods, covering the RationalSet and RationalPosSet NumberSet classes (defined in proveit.numbers.number_sets.rational_numbers/rationals.py):

In [41]:
rational_membership_is_bool = Forall(x, in_bool(InSet(x, Rational)))

rational_membership_is_bool (conjecture without proof):

In [42]:
rational_nonzero_membership_is_bool = Forall(x, in_bool(InSet(x, RationalNonZero)))

rational_nonzero_membership_is_bool (conjecture without proof):

In [43]:
rational_pos_membership_is_bool = Forall(x, in_bool(InSet(x, RationalPos)))

rational_pos_membership_is_bool (conjecture without proof):

In [44]:
rational_neg_membership_is_bool = Forall(x, in_bool(InSet(x, RationalNeg)))

rational_neg_membership_is_bool (conjecture without proof):

In [45]:
rational_nonneg_membership_is_bool = Forall(x, in_bool(InSet(x, RationalNonNeg)))

rational_nonneg_membership_is_bool (conjecture without proof):

In [46]:
rational_nonpos_membership_is_bool = Forall(x, in_bool(InSet(x, RationalNonPos)))

rational_nonpos_membership_is_bool (conjecture without proof):

In [47]:
%end theorems

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