Demonstrations for the theory of proveit.numbers.number_sets.rational_numbers

In [1]:
import proveit
from proveit import q, p, r, s, x

from proveit import defaults
from proveit.logic.equality import equals_reversal

from proveit.logic import Boolean, NotEquals, InSet, ProperSubset
from proveit.numbers import Less, LessEq, greater, greater_eq, zero
from proveit.numbers import (
    Natural, NaturalPos, Integer, IntegerNonZero, IntegerNeg, IntegerNonPos,
    Rational, RationalNonZero, RationalPos, RationalNeg, RationalNonNeg, RationalNonPos)
from proveit.numbers.number_sets.rational_numbers  import rationals_def
%begin demonstrations

The Rational Numbers, $\mathbb{Q}$ and Various Subsets $\mathbb{Q}^{+}$, $\mathbb{Q}^{-}$, $\mathbb{Q}^{\ge 0}$ [Under Construction]



Simple Expressions involving the Rational Numbers $\mathbb{Q}$

It is straightforward to construct expressions involving the Rational Numbers NumberSet $\mathbb{Q}$:

In [2]:
# a simple set membership claim
InSet(x, Rational)
In [3]:
ProperSubset(Natural, RationalNonNeg)

Common Attributes of the Rational Numbers NumberSet $\mathbb{Q}$

TBA Placeholder — attributes not particularly relevant for NumberSet …

In [4]:
# the Rational number set


The ``axioms`` for the Rational Numbers $\mathbb{Q}$ … can be accessed on the [rational axioms](./_axioms_.ipynb) page, and establish the definitions of the Rational numbers and various subsets of the Rational numbers.

In [5]:
# def of the Rational number set

Theorems & Conjectures

The `number/sets/rational` theory already has a substantial number of related theorems and conjectures established, covering a wide range of … The remainder can be found in the [containment theorems notebook](./\_theorems\_.ipynb).

In [6]:
from proveit.numbers.number_sets.rational_numbers import (zero_is_rational)
In [7]:


1. TBA

We begin with …

2. TBA.


3. TBA


Miscellaneous Testing

The material below was developed to test various Rational NumberSet-related methods. Some of this material could be integrated into the `_demonstrations_` page eventually and/or deleted as development continues.

<font size =3>The InSet class has a deduce_in_bool() method that eventually depends on the deduce_membership_in_bool() method of the underlying NumberSet class.

In [8]:
q_in_Q = InSet(q, Rational)
In [9]:
In [10]:
p_in_QPos = InSet(p, RationalPos)
In [11]:
In [12]:
r_in_QNeg = InSet(p, RationalNeg)
In [13]:
In [14]:
s_in_QNonNeg = InSet(s, RationalNonNeg)
In [15]:
In [ ]:
In [ ]:

Number set membership demonstrations

In [16]:
InSet(InSet(r, Rational), Boolean).prove()
In [17]:
InSet(InSet(r, RationalNonZero), Boolean).prove()
In [18]:
InSet(InSet(r, RationalPos), Boolean).prove()
In [19]:
InSet(InSet(r, RationalNeg), Boolean).prove()
In [20]:
InSet(InSet(r, RationalNonNeg), Boolean).prove()
In [21]:
InSet(InSet(r, RationalNonPos), Boolean).prove()
In [22]:
NotEquals(r, zero).prove(assumptions=[InSet(r, RationalNonZero)], 
                         conclude_automation=False) # should be side-effect
In [23]:
greater(x, zero).prove(assumptions=[InSet(x, RationalPos)], 
                       conclude_automation=False) # should be side-effect
In [24]:
Less(x, zero).prove(assumptions=[InSet(x, RationalNeg)], 
                    conclude_automation=False) # should be side-effect
In [25]:
greater_eq(x, zero).prove(assumptions=[InSet(x, RationalNonNeg)], 
                          conclude_automation=False) # should be side-effect
In [26]:
LessEq(x, zero).prove(assumptions=[InSet(x, RationalNonPos)], 
                      conclude_automation=False) # should be side-effect
In [27]:
InSet(r, RationalNonZero).prove(assumptions=[InSet(r, Rational), NotEquals(r, zero)])
In [28]:
InSet(r, RationalPos).prove(assumptions=[InSet(r, Rational), greater(r, zero)])
In [29]:
InSet(r, RationalNeg).prove(assumptions=[InSet(r, Rational), Less(r, zero)])
In [30]:
InSet(r, RationalNonNeg).prove(assumptions=[InSet(r, Rational), greater_eq(r, zero)])
In [31]:
InSet(r, RationalNonPos).prove(assumptions=[InSet(r, Rational), LessEq(r, zero)])
In [32]:
InSet(r, RationalNonNeg).prove(assumptions=[InSet(r, Natural)])
In [33]:
InSet(r, RationalPos).prove(assumptions=[InSet(r, NaturalPos)])
In [34]:
InSet(r, Rational).prove(assumptions=[InSet(r, Integer)])
In [35]:
InSet(r, RationalNonZero).prove(assumptions=[InSet(r, IntegerNonZero)])
In [36]:
InSet(r, RationalNeg).prove(assumptions=[InSet(r, IntegerNeg)])
In [37]:
InSet(r, RationalNonPos).prove(assumptions=[InSet(r, IntegerNonPos)])
In [38]:
InSet(r, Rational).prove(assumptions=[InSet(r, RationalNonZero)])
In [39]:
InSet(r, Rational).prove(assumptions=[InSet(r, RationalPos)])
In [40]:
InSet(r, RationalNonZero).prove(assumptions=[InSet(r, RationalPos)])
In [41]:
InSet(r, RationalNeg).prove(assumptions=[InSet(r, IntegerNeg)])
In [42]:
InSet(r, RationalNonNeg).prove(assumptions=[InSet(r, RationalPos)])
In [43]:
InSet(r, Rational).prove(assumptions=[InSet(r, RationalNeg)])
In [44]:
InSet(r, RationalNonZero).prove(assumptions=[InSet(r, RationalNeg)])
In [45]:
InSet(r, RationalNonPos).prove(assumptions=[InSet(r, RationalNeg)])
In [46]:
InSet(r, Rational).prove(assumptions=[InSet(r, RationalNonNeg)])
In [47]:
InSet(r, Rational).prove(assumptions=[InSet(r, RationalNonPos)])
In [48]:
%end demonstrations