Metamath Proof Explorer
Table of Contents - 5.4.13. Rational numbers (as a subset of complex numbers)
- cq
- df-q
- elq
- qmulz
- znq
- qre
- zq
- qred
- zssq
- nn0ssq
- nnssq
- qssre
- qsscn
- qex
- nnq
- qcn
- qexALT
- 1q
- qaddcl
- qnegcl
- qmulcl
- qsubcl
- qreccl
- qdivcl
- qrevaddcl
- nnrecq
- irradd
- irrmul
- elpq
- elpqb