# 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]¶

TBA

## 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
Rational


## Axioms ¶

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
rationals_def


## 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]:
zero_is_rational


1. TBA

We begin with …

2. TBA.

TBA

3. TBA

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.
</font>

In [8]:
q_in_Q = InSet(q, Rational)

q_in_Q:
In [9]:
q_in_Q.deduce_in_bool()

In [10]:
p_in_QPos = InSet(p, RationalPos)

p_in_QPos:
In [11]:
p_in_QPos.deduce_in_bool()

In [12]:
r_in_QNeg = InSet(p, RationalNeg)

r_in_QNeg:
In [13]:
r_in_QNeg.deduce_in_bool()

In [14]:
s_in_QNonNeg = InSet(s, RationalNonNeg)

s_in_QNonNeg:
In [15]:
s_in_QNonNeg.deduce_in_bool()

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