# Differences

This shows you the differences between two versions of the page.

 non-negative_rational_number [2013/08/12 15:22]nikolaj non-negative_rational_number [2014/03/21 11:11] (current) Both sides previous revision Previous revision 2013/09/03 00:55 nikolaj 2013/08/12 15:22 nikolaj 2013/08/12 15:11 nikolaj 2013/05/20 22:32 ben 2013/05/19 23:27 nikolaj 2013/05/19 23:16 nikolaj 2013/05/19 22:49 nikolaj 2013/05/19 22:48 nikolaj 2013/05/19 22:34 nikolaj 2013/05/19 21:45 nikolaj 2013/05/19 21:42 nikolaj created Next revision Previous revision 2013/09/03 00:55 nikolaj 2013/08/12 15:22 nikolaj 2013/08/12 15:11 nikolaj 2013/05/20 22:32 ben 2013/05/19 23:27 nikolaj 2013/05/19 23:16 nikolaj 2013/05/19 22:49 nikolaj 2013/05/19 22:48 nikolaj 2013/05/19 22:34 nikolaj 2013/05/19 21:45 nikolaj 2013/05/19 21:42 nikolaj created Line 1: Line 1: ===== Non-negative rational number ===== ===== Non-negative rational number ===== - ==== Definition ​==== + ==== Set ==== - ^ $\mathbb Q_+$ ^ + | @#FFBB00: definiendum | @#​FFBB00: ​$r \in\mathbb Q_+$ | - | $n,m\in \mathbb ​N$ | + | @#55CCEE: context ​    | @#​55CCEE: ​$r \in \mathbb ​Q$ | - | $m>​1 ​$ | + - ^ $\mathbb N \cup \{r\ |\ \exists n,m\ (\ r=\langle n,m\rangle \land \mathrm{gcd}(n,​m)\neq 1\ )\}$ ^ + | @#55EE55: postulate ​  | @#55EE55: $r \ge 0$ | - + - ==== 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$ ^ + + ==== Discussion ==== === Reference === === Reference === Wikipedia: [[http://​en.wikipedia.org/​wiki/​Rational_number|Rational number]] Wikipedia: [[http://​en.wikipedia.org/​wiki/​Rational_number|Rational number]] - + ==== Parents ​==== - Mizar: [[http://​mizar.org/​JFM/​pdf/​arytm_3.pdf|ARYTM_3]] + === Refinement of === - + [[Non-negative real number]] - ==== Context ​==== + - Set + === Subset of === === Subset of === - [[Rational ​number]], [[Non-negative real number]] + [[Rational number]]