This is an old revision of the document!


Non-negative rational number

Definition

$ \mathbb Q_+ $
$ n,m\in \mathbb N $
$ m>1 $
$ \mathbb N \cup \{r\ |\ \exists n,m\ (\ r=\langle n,m\rangle \land \mathrm{gcd}(n,m)\neq 1\ )\} $

Ramifications

Definitions

$ a,b,c,x\in \mathbb N $
$b\neq 0$
$ r,s,t \in \mathbb Q_+ $
$ a\div b:=x,\hspace{1cm}(c<b)\land (a=x\cdot b+c)$
$ \mathrm{red}(a,b):=a\div\mathrm{gcd}(a,b)$
$ \frac{a}{b} \equiv \begin{cases} \mathrm{red}(a,b) & \mathrm{if}\ \mathrm{red}(b,a)=1\\\\ \langle\mathrm{red}(a,b),\mathrm{red}(b,a)\rangle & \mathrm{else} \end{cases}$
$ \mathrm{num}\frac{a}{b}\equiv a $
$ \mathrm{den}\frac{a}{b}\equiv b $
$ r+s=\frac{\mathrm{num} r\ \cdot\ \mathrm{den} s\ +\ \mathrm{num} s\ \cdot\ \mathrm{den} r}{\mathrm{den} r\ \cdot\ \mathrm{den} s}$
$ r\cdot s=\frac{\mathrm{num} r\ \cdot\ \mathrm{num} s}{\mathrm{den} r\ \cdot\ \mathrm{den} s}$

Predicates

$r\leq s\equiv \exists t\ (s=r+t)$
$r < s\equiv s\leq r$

Reference

Wikipedia: Rational number

Mizar: ARYTM_3

Context

Set

Subset of

Link to graph
Log In
Improvements of the human condition