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

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)

%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

zero_is_rational = InSet(zero, Rational)

zero_is_rational (conjecture without proof):

zero_is_nonneg_rational = InSet(zero, RationalNonNeg)

zero_is_nonneg_rational (conjecture without proof):

zero_is_nonpos_rational = InSet(zero, RationalNonPos)

zero_is_nonpos_rational (conjecture without proof):

zero_set_within_rational = ProperSubset(ZeroSet, Rational)

zero_set_within_rational (conjecture without proof):

zero_set_within_rational_nonneg = ProperSubset(ZeroSet, RationalNonNeg)

zero_set_within_rational_nonneg (conjecture without proof):

zero_set_within_rational_nonpos = ProperSubset(ZeroSet, RationalNonPos)

zero_set_within_rational_nonpos (conjecture without proof):

nat_within_rational = ProperSubset(Natural, Rational)

nat_within_rational (conjecture without proof):

nat_within_rational_nonneg = ProperSubset(Natural, RationalNonNeg)

nat_within_rational_nonneg (conjecture without proof):

nat_pos_within_rational_pos = ProperSubset(NaturalPos, RationalPos)

nat_pos_within_rational_pos (conjecture without proof):

nat_within_rational_nonneg = ProperSubset(Natural, RationalNonNeg)

nat_within_rational_nonneg (conjecture without proof):

(alternate proof for nat_within_rational_nonneg)

int_within_rational = ProperSubset(Integer, Rational)

int_within_rational (conjecture without proof):

nonzero_int_within_rational_nonzero = ProperSubset(IntegerNonZero, RationalNonZero)

nonzero_int_within_rational_nonzero (conjecture without proof):

neg_int_within_rational_neg = ProperSubset(IntegerNeg, RationalNeg)

neg_int_within_rational_neg (conjecture without proof):

nonpos_int_within_rational_nonpos = ProperSubset(IntegerNonPos, RationalNonPos)

nonpos_int_within_rational_nonpos (conjecture without proof):

rational_nonzero_within_rational = ProperSubset(RationalNonZero, Rational)

rational_nonzero_within_rational (conjecture without proof):

rational_pos_within_rational = ProperSubset(RationalPos, Rational)

rational_pos_within_rational (conjecture without proof):

rational_pos_within_rational_nonzero = ProperSubset(RationalPos, RationalNonZero)

rational_pos_within_rational_nonzero (conjecture without proof):

rational_neg_within_rational_nonzero = ProperSubset(RationalNeg, RationalNonZero)

rational_neg_within_rational_nonzero (conjecture without proof):

rational_pos_within_rational_nonneg = ProperSubset(RationalPos, RationalNonNeg)

rational_pos_within_rational_nonneg (conjecture without proof):

rational_neg_within_rational_nonpos = ProperSubset(RationalNeg, RationalNonPos)

rational_neg_within_rational_nonpos (conjecture without proof):

rational_neg_within_rational = ProperSubset(RationalNeg, Rational)

rational_neg_within_rational (conjecture without proof):

rational_nonneg_within_rational = ProperSubset(RationalNonNeg, Rational)

rational_nonneg_within_rational (conjecture without proof):

rational_nonpos_within_rational = ProperSubset(RationalNonPos, Rational)

rational_nonpos_within_rational (conjecture without proof):

nonzero_if_in_rational_nonzero = Forall(
    q,
    NotEquals(q, zero),
    domain=RationalNonZero)

nonzero_if_in_rational_nonzero (conjecture without proof):

positive_if_in_rational_pos = Forall(
    q,
    greater(q, zero),
    domain=RationalPos)

positive_if_in_rational_pos (conjecture without proof):

negative_if_in_rational_neg = Forall(
    q,
    Less(q, zero),
    domain=RationalNeg)

negative_if_in_rational_neg (conjecture without proof):

nonneg_if_in_rational_nonneg = Forall(
    q,
    greater_eq(q, zero),
    domain=RationalNonNeg)

nonneg_if_in_rational_nonneg (conjecture without proof):

nonpos_if_in_rational_nonpos = Forall(
    q,
    LessEq(q, zero),
    domain=RationalNonPos)

nonpos_if_in_rational_nonpos (conjecture without proof):

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

nonzero_rational_is_rational_nonzero (conjecture without proof):

pos_rational_is_rational_pos = Forall(
        q, InSet(q, RationalPos), condition=greater(q, zero),
        domain=Rational)

pos_rational_is_rational_pos (conjecture without proof):

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):

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

neg_rational_is_rational_neg (conjecture without proof):

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):

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):

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

nonpos_rational_is_rational_nonpos (conjecture without proof):

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

nat_ratio (conjecture without proof):

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):

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):

rational_membership_is_bool = Forall(x, in_bool(InSet(x, Rational)))

rational_membership_is_bool (conjecture without proof):

rational_nonzero_membership_is_bool = Forall(x, in_bool(InSet(x, RationalNonZero)))

rational_nonzero_membership_is_bool (conjecture without proof):

rational_pos_membership_is_bool = Forall(x, in_bool(InSet(x, RationalPos)))

rational_pos_membership_is_bool (conjecture without proof):

rational_neg_membership_is_bool = Forall(x, in_bool(InSet(x, RationalNeg)))

rational_neg_membership_is_bool (conjecture without proof):

rational_nonneg_membership_is_bool = Forall(x, in_bool(InSet(x, RationalNonNeg)))

rational_nonneg_membership_is_bool (conjecture without proof):

rational_nonpos_membership_is_bool = Forall(x, in_bool(InSet(x, RationalNonPos)))

rational_nonpos_membership_is_bool (conjecture without proof):

%end theorems

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