Metamath Proof Explorer

Table of Contents - 21.3.5. Real and Complex Numbers

1. sgnval2
2. Complex operations - misc. additions
   1. creq0
   2. 1nei
   3. 1neg1t1neg1
   4. nnmulge
   5. submuladdd
   6. muldivdid
   7. binom2subadd
   8. cjsubd
   9. re0cj
   10. receqid
   11. pythagreim
   12. efiargd
   13. arginv
   14. argcj
   15. quad3d
3. Ordering on reals - misc additions
   1. lt2addrd
4. Extended reals - misc additions
   1. xrlelttric
   2. xaddeq0
   3. rexmul2
   4. xrinfm
   5. le2halvesd
   6. xraddge02
   7. xrge0addge
   8. xlt2addrd
   9. xrge0infss
   10. xrge0infssd
   11. xrge0addcld
   12. xrge0subcld
   13. infxrge0lb
   14. infxrge0glb
   15. infxrge0gelb
   16. xrofsup
   17. supxrnemnf
5. Extended nonnegative integers - misc additions
   1. xnn0gt0
   2. xnn01gt
   3. nn0xmulclb
   4. xnn0nn0d
   5. xnn0nnd
6. Real number intervals - misc additions
   1. joiniooico
   2. ubico
   3. xeqlelt
   4. eliccelico
   5. elicoelioo
   6. iocinioc2
   7. xrdifh
   8. iocinif
   9. difioo
   10. difico
7. Finite intervals of integers - misc additions
   1. uzssico
   2. fz2ssnn0
   3. nndiffz1
   4. ssnnssfz
   5. fzm1ne1
   6. fzspl
   7. fzdif2
   8. fzodif2
   9. fzodif1
   10. fzsplit3
   11. elfzodif0
   12. bcm1n
8. Half-open integer ranges - misc additions
   1. iundisjfi
   2. iundisj2fi
   3. iundisjcnt
   4. iundisj2cnt
   5. fzone1
   6. fzom1ne1
   7. f1ocnt
   8. fz1nnct
   9. fz1nntr
   10. fzo0opth
   11. nn0difffzod
   12. suppssnn0
9. The ` # ` (set size) function - misc additions
   1. hashunif
   2. hashxpe
   3. hashgt1
   4. hashpss
   5. hashne0
10. The greatest common divisor operator - misc. additions
    1. elq2
    2. znumd
    3. zdend
    4. numdenneg
    5. divnumden2
    6. expgt0b
11. Integers
    1. nn0split01
    2. nn0disj01
    3. nnindf
    4. nn0min
    5. subne0nn
    6. ltesubnnd
    7. fprodeq02
    8. pr01ssre
    9. fprodex01
    10. prodpr
    11. prodtp
    12. fsumub
    13. fsumiunle
12. Decimal numbers
    1. dfdec100