Metamath Proof Explorer
Table of Contents - 5.1. Construction and axiomatization of real and complex numbers
- Dedekind-cut construction of real and complex numbers
- cnpi
- cpli
- cmi
- clti
- cplpq
- cmpq
- cltpq
- ceq
- cnq
- c1q
- cerq
- cplq
- cmq
- crq
- cltq
- cnp
- c1p
- cpp
- cmp
- cltp
- cer
- cnr
- c0r
- c1r
- cm1r
- cplr
- cmr
- cltr
- df-ni
- df-pli
- df-mi
- df-lti
- elni
- elni2
- pinn
- pion
- piord
- niex
- 0npi
- 1pi
- addpiord
- mulpiord
- mulidpi
- ltpiord
- ltsopi
- ltrelpi
- dmaddpi
- dmmulpi
- addclpi
- mulclpi
- addcompi
- addasspi
- mulcompi
- mulasspi
- distrpi
- addcanpi
- mulcanpi
- addnidpi
- ltexpi
- ltapi
- ltmpi
- 1lt2pi
- nlt1pi
- indpi
- df-plpq
- df-mpq
- df-ltpq
- df-enq
- df-nq
- df-erq
- df-plq
- df-mq
- df-1nq
- df-rq
- df-ltnq
- enqbreq
- enqbreq2
- enqer
- enqex
- nqex
- 0nnq
- elpqn
- ltrelnq
- pinq
- 1nq
- nqereu
- nqerf
- nqercl
- nqerrel
- nqerid
- enqeq
- nqereq
- addpipq2
- addpipq
- addpqnq
- mulpipq2
- mulpipq
- mulpqnq
- ordpipq
- ordpinq
- addpqf
- addclnq
- mulpqf
- mulclnq
- addnqf
- mulnqf
- addcompq
- addcomnq
- mulcompq
- mulcomnq
- adderpqlem
- mulerpqlem
- adderpq
- mulerpq
- addassnq
- mulassnq
- mulcanenq
- distrnq
- 1nqenq
- mulidnq
- recmulnq
- recidnq
- recclnq
- recrecnq
- dmrecnq
- ltsonq
- lterpq
- ltanq
- ltmnq
- 1lt2nq
- ltaddnq
- ltexnq
- halfnq
- nsmallnq
- ltbtwnnq
- ltrnq
- archnq
- df-np
- df-1p
- df-plp
- df-mp
- df-ltp
- npex
- elnp
- elnpi
- prn0
- prpssnq
- elprnq
- 0npr
- prcdnq
- prub
- prnmax
- npomex
- prnmadd
- ltrelpr
- genpv
- genpelv
- genpprecl
- genpdm
- genpn0
- genpss
- genpnnp
- genpcd
- genpnmax
- genpcl
- genpass
- plpv
- mpv
- dmplp
- dmmp
- nqpr
- 1pr
- addclprlem1
- addclprlem2
- addclpr
- mulclprlem
- mulclpr
- addcompr
- addasspr
- mulcompr
- mulasspr
- distrlem1pr
- distrlem4pr
- distrlem5pr
- distrpr
- 1idpr
- ltprord
- psslinpr
- ltsopr
- prlem934
- ltaddpr
- ltaddpr2
- ltexprlem1
- ltexprlem2
- ltexprlem3
- ltexprlem4
- ltexprlem5
- ltexprlem6
- ltexprlem7
- ltexpri
- ltaprlem
- ltapr
- addcanpr
- prlem936
- reclem2pr
- reclem3pr
- reclem4pr
- recexpr
- suplem1pr
- suplem2pr
- supexpr
- df-enr
- df-nr
- df-plr
- df-mr
- df-ltr
- df-0r
- df-1r
- df-m1r
- enrer
- nrex1
- enrbreq
- enreceq
- enrex
- ltrelsr
- addcmpblnr
- mulcmpblnrlem
- mulcmpblnr
- prsrlem1
- addsrmo
- mulsrmo
- addsrpr
- mulsrpr
- ltsrpr
- gt0srpr
- 0nsr
- 0r
- 1sr
- m1r
- addclsr
- mulclsr
- dmaddsr
- dmmulsr
- addcomsr
- addasssr
- mulcomsr
- mulasssr
- distrsr
- m1p1sr
- m1m1sr
- ltsosr
- 0lt1sr
- 1ne0sr
- 0idsr
- 1idsr
- 00sr
- ltasr
- pn0sr
- negexsr
- recexsrlem
- addgt0sr
- mulgt0sr
- sqgt0sr
- recexsr
- mappsrpr
- ltpsrpr
- map2psrpr
- supsrlem
- supsr
- cc
- cr
- cc0
- c1
- ci
- caddc
- cltrr
- cmul
- df-c
- df-0
- df-1
- df-i
- df-r
- df-add
- df-mul
- df-lt
- opelcn
- opelreal
- elreal
- elreal2
- 0ncn
- ltrelre
- addcnsr
- mulcnsr
- eqresr
- addresr
- mulresr
- ltresr
- ltresr2
- dfcnqs
- addcnsrec
- mulcnsrec
- Final derivation of real and complex number postulates
- axaddf
- axmulf
- axcnex
- axresscn
- ax1cn
- axicn
- axaddcl
- axaddrcl
- axmulcl
- axmulrcl
- axmulcom
- axaddass
- axmulass
- axdistr
- axi2m1
- ax1ne0
- ax1rid
- axrnegex
- axrrecex
- axcnre
- axpre-lttri
- axpre-lttrn
- axpre-ltadd
- axpre-mulgt0
- axpre-sup
- wuncn
- Real and complex number postulates restated as axioms
- ax-cnex
- ax-resscn
- ax-1cn
- ax-icn
- ax-addcl
- ax-addrcl
- ax-mulcl
- ax-mulrcl
- ax-mulcom
- ax-addass
- ax-mulass
- ax-distr
- ax-i2m1
- ax-1ne0
- ax-1rid
- ax-rnegex
- ax-rrecex
- ax-cnre
- ax-pre-lttri
- ax-pre-lttrn
- ax-pre-ltadd
- ax-pre-mulgt0
- ax-pre-sup
- ax-addf
- ax-mulf