===== Arithmetic structure of real numbers =====
==== Set ====
| @#FFBB00: definiendum | @#FFBB00: $\langle \mathbb R,+_\mathbb{R},\cdot_\mathbb{R} \rangle$ |

| @#55EE55: postulate   | @#55EE55: $ r +_\mathbb{R} s = \{q+_\mathbb{Q}p\ |\ (q\in r)\land (p\in s)\} $ |
| @#55EE55: postulate   | @#55EE55: $ r -_\mathbb{R} s = \{q-_\mathbb{Q}p\ |\ (q\in r)\land (p\in \mathbb Q\setminus s)\} $ |
| @#55EE55: postulate   | @#55EE55: $ -_{\mathbb R}r = \{q-_\mathbb{Q}p\ |\ (p\in \mathbb Q\setminus r)\land (q<0)\} $ |

| @#55EE55: postulate   | @#55EE55: $ r\ge 0\land s\ge 0\implies r\cdot_\mathbb{R}s = \{q\cdot_\mathbb{Q}p\ |\ (q\in r)\land (p\in s)\land (q,p\ge 0)\}\cup\{q\ |\ (q\in\mathbb Q)\land (q<0)\}  $ |
| @#55EE55: postulate   | @#55EE55: $ r\ge 0\land s <  0\implies r\cdot_\mathbb{R}s = -(r\cdot_\mathbb{R}(-s))  $ |
| @#55EE55: postulate   | @#55EE55: $ r  < 0\land s\ge 0\implies r\cdot_\mathbb{R}s = -((-r)\cdot_\mathbb{R}s)  $ |
| @#55EE55: postulate   | @#55EE55: $ r  < 0\land s <  0\implies r\cdot_\mathbb{R}s = (-r)\cdot_\mathbb{R}(-s)  $ |

| @#55EE55: postulate   | @#55EE55: $ r\ge 0\land s >  0\implies r/_\mathbb{R}s = \{q/_\mathbb{Q}p\ |\ (q\in r)\land (p\in \mathbb Q\setminus s)\} $ |
| @#55EE55: postulate   | @#55EE55: $ r\ge 0\land s <  0\implies r/_\mathbb{R}s = -(r/_\mathbb{R}(-s))  $ |
| @#55EE55: postulate   | @#55EE55: $ r  < 0\land s > 0\implies r/_\mathbb{R}s = -((-r)/_\mathbb{R}s)  $ |
| @#55EE55: postulate   | @#55EE55: $ r  < 0\land s <  0\implies r/_\mathbb{R}s = (-r)/_\mathbb{R}(-s)  $ |

The operations $+_\mathbb{Q}$ and $\cdot_\mathbb{Q}$ on the right hand sides are these of [[arithmetic structure of rational numbers]].

==== Discussion ====
=== Reference ===
Wikipedia: [[http://en.wikipedia.org/wiki/Real_number|Real number]], [[http://en.wikipedia.org/wiki/Construction_of_the_real_numbers|Construction of the real numbers]]
==== Parents ====
=== Context ===
[[Real number]]
=== Element of ===
[[Field]]