Metamath Proof Explorer
Table of Contents - 21.42.3. Ordering on real numbers - Real and complex numbers basic operations
- sub2times
- nnxrd
- nnxr
- abssubrp
- elfzfzo
- oddfl
- abscosbd
- mul13d
- negpilt0
- dstregt0
- subadd4b
- xrlttri5d
- neglt
- zltlesub
- divlt0gt0d
- subsub23d
- 2timesgt
- reopn
- sub31
- nnne1ge2
- lefldiveq
- negsubdi3d
- ltdiv2dd
- abssinbd
- halffl
- monoords
- hashssle
- lttri5d
- fzisoeu
- lt3addmuld
- absnpncan2d
- fperiodmullem
- fperiodmul
- upbdrech
- lt4addmuld
- absnpncan3d
- upbdrech2
- ssfiunibd
- fzdifsuc2
- fzsscn
- divcan8d
- dmmcand
- fzssre
- bccld
- leadd12dd
- fzssnn0
- xreqle
- xaddlidd
- xadd0ge
- elfzolem1
- xrgtned
- xrleneltd
- xaddcomd
- supxrre3
- uzfissfz
- xleadd2d
- suprltrp
- xleadd1d
- xreqled
- xrgepnfd
- xrge0nemnfd
- supxrgere
- iuneqfzuzlem
- iuneqfzuz
- xle2addd
- supxrgelem
- supxrge
- suplesup
- infxrglb
- xadd0ge2
- nepnfltpnf
- ltadd12dd
- nemnftgtmnft
- xrgtso
- rpex
- xrge0ge0
- xrssre
- ssuzfz
- absfun
- infrpge
- xrlexaddrp
- supsubc
- xralrple2
- nnuzdisj
- ltdivgt1
- xrltned
- nnsplit
- divdiv3d
- abslt2sqd
- qenom
- qct
- xrltnled
- lenlteq
- xrred
- rr2sscn2
- infxr
- infxrunb2
- infxrbnd2
- infleinflem1
- infleinflem2
- infleinf
- xralrple4
- xralrple3
- eluzelzd
- suplesup2
- recnnltrp
- nnn0
- fzct
- rpgtrecnn
- fzossuz
- infxrrefi
- xrralrecnnle
- fzoct
- frexr
- nnrecrp
- reclt0d
- lt0neg1dd
- infxrcld
- xrralrecnnge
- reclt0
- ltmulneg
- allbutfi
- ltdiv23neg
- xreqnltd
- mnfnre2
- zssxr
- fisupclrnmpt
- supxrunb3
- elfzod
- fimaxre4
- ren0
- eluzelz2
- resabs2d
- uzid2
- supxrleubrnmpt
- uzssre2
- uzssd
- eluzd
- infxrlbrnmpt2
- xrre4
- uz0
- eluzelz2d
- infleinf2
- unb2ltle
- uzidd2
- uzssd2
- rexabslelem
- rexabsle
- allbutfiinf
- supxrrernmpt
- suprleubrnmpt
- infrnmptle
- infxrunb3
- uzn0d
- uzssd3
- rexabsle2
- infxrunb3rnmpt
- supxrre3rnmpt
- uzublem
- uzub
- ssrexr
- supxrmnf2
- supxrcli
- uzid3
- infxrlesupxr
- xnegeqd
- xnegrecl
- xnegnegi
- xnegeqi
- nfxnegd
- xnegnegd
- uzred
- xnegcli
- supminfrnmpt
- infxrpnf
- infxrrnmptcl
- leneg2d
- supxrltinfxr
- max1d
- supxrleubrnmptf
- nleltd
- zxrd
- infxrgelbrnmpt
- rphalfltd
- uzssz2
- leneg3d
- max2d
- uzn0bi
- xnegrecl2
- nfxneg
- uzxrd
- infxrpnf2
- supminfxr
- infrpgernmpt
- xnegre
- xnegrecl2d
- uzxr
- supminfxr2
- xnegred
- supminfxrrnmpt
- min1d
- min2d
- pnfged
- xrnpnfmnf
- uzsscn
- absimnre
- uzsscn2
- xrtgcntopre
- absimlere
- rpssxr
- monoordxrv
- monoordxr
- monoord2xrv
- monoord2xr
- xrpnf
- xlenegcon1
- xlenegcon2
- pimxrneun
- caucvgbf
- cvgcau
- cvgcaule
- rexanuz2nf