Metamath Proof Explorer
Table of Contents - 5.5.2. Infinity and the extended real number system (cont.)
- cxne
- cxad
- cxmu
- df-xneg
- df-xadd
- df-xmul
- ltxr
- elxr
- xrnemnf
- xrnepnf
- xrltnr
- ltpnf
- ltpnfd
- 0ltpnf
- mnflt
- mnfltd
- mnflt0
- mnfltpnf
- mnfltxr
- pnfnlt
- nltmnf
- pnfge
- xnn0n0n1ge2b
- 0lepnf
- xnn0ge0
- mnfle
- xrltnsym
- xrltnsym2
- xrlttri
- xrlttr
- xrltso
- xrlttri2
- xrlttri3
- xrleloe
- xrleltne
- xrltlen
- dfle2
- dflt2
- xrltle
- xrltled
- xrleid
- xrleidd
- xrletri
- xrletri3
- xrletrid
- xrlelttr
- xrltletr
- xrletr
- xrlttrd
- xrlelttrd
- xrltletrd
- xrletrd
- xrltne
- nltpnft
- xgepnf
- ngtmnft
- xlemnf
- xrrebnd
- xrre
- xrre2
- xrre3
- ge0gtmnf
- ge0nemnf
- xrrege0
- xrmax1
- xrmax2
- xrmin1
- xrmin2
- xrmaxeq
- xrmineq
- xrmaxlt
- xrltmin
- xrmaxle
- xrlemin
- max1
- max1ALT
- max2
- 2resupmax
- min1
- min2
- maxle
- lemin
- maxlt
- ltmin
- lemaxle
- max0sub
- ifle
- z2ge
- qbtwnre
- qbtwnxr
- qsqueeze
- qextltlem
- qextlt
- qextle
- xralrple
- alrple
- xnegeq
- xnegex
- xnegpnf
- xnegmnf
- rexneg
- xneg0
- xnegcl
- xnegneg
- xneg11
- xltnegi
- xltneg
- xleneg
- xlt0neg1
- xlt0neg2
- xle0neg1
- xle0neg2
- xaddval
- xaddf
- xmulval
- xaddpnf1
- xaddpnf2
- xaddmnf1
- xaddmnf2
- pnfaddmnf
- mnfaddpnf
- rexadd
- rexsub
- rexaddd
- xnn0xaddcl
- xaddnemnf
- xaddnepnf
- xnegid
- xaddcl
- xaddcom
- xaddid1
- xaddid2
- xaddid1d
- xnn0lem1lt
- xnn0lenn0nn0
- xnn0le2is012
- xnn0xadd0
- xnegdi
- xaddass
- xaddass2
- xpncan
- xnpcan
- xleadd1a
- xleadd2a
- xleadd1
- xltadd1
- xltadd2
- xaddge0
- xle2add
- xlt2add
- xsubge0
- xposdif
- xlesubadd
- xmullem
- xmullem2
- xmulcom
- xmul01
- xmul02
- xmulneg1
- xmulneg2
- rexmul
- xmulf
- xmulcl
- xmulpnf1
- xmulpnf2
- xmulmnf1
- xmulmnf2
- xmulpnf1n
- xmulid1
- xmulid2
- xmulm1
- xmulasslem2
- xmulgt0
- xmulge0
- xmulasslem
- xmulasslem3
- xmulass
- xlemul1a
- xlemul2a
- xlemul1
- xlemul2
- xltmul1
- xltmul2
- xadddilem
- xadddi
- xadddir
- xadddi2
- xadddi2r
- x2times
- xnegcld
- xaddcld
- xmulcld
- xadd4d
- xnn0add4d