Metamath Proof Explorer
Table of Contents - 20.43.6. General auxiliary theorems (2)
- Logical conjunction - extension
- an4com24
- Abbreviated conjunction and disjunction of three wff's - extension
- 3an4ancom24
- 4an21
- Negated membership (alternative)
- cnelbr
- df-nelbr
- dfnelbr2
- nelbr
- nelbrim
- nelbrnel
- nelbrnelim
- The empty set - extension
- ralralimp
- Indexed union and intersection - extension
- otiunsndisjX
- Functions - extension
- fvifeq
- rnfdmpr
- imarnf1pr
- funop1
- fun2dmnopgexmpl
- opabresex0d
- opabbrfex0d
- opabresexd
- opabbrfexd
- f1oresf1orab
- f1oresf1o
- f1oresf1o2
- Maps-to notation - extension
- fvmptrab
- fvmptrabdm
- Ordering on reals - extension
- leltletr
- Subtraction - extension
- cnambpcma
- cnapbmcpd
- addsubeq0
- Ordering on reals (cont.) - extension
- leaddsuble
- 2leaddle2
- ltnltne
- p1lep2
- ltsubsubaddltsub
- zm1nn
- Imaginary and complex number properties - extension
- readdcnnred
- resubcnnred
- recnmulnred
- cndivrenred
- sqrtnegnre
- Nonnegative integers (as a subset of complex numbers) - extension
- nn0resubcl
- Integers (as a subset of complex numbers) - extension
- zgeltp1eq
- Decimal arithmetic - extension
- 1t10e1p1e11
- deccarry
- Upper sets of integers - extension
- eluzge0nn0
- Infinity and the extended real number system (cont.) - extension
- nltle2tri
- Finite intervals of integers - extension
- ssfz12
- elfz2z
- 2elfz3nn0
- fz0addcom
- 2elfz2melfz
- fz0addge0
- elfzlble
- elfzelfzlble
- Half-open integer ranges - extension
- fzopred
- fzopredsuc
- 1fzopredsuc
- el1fzopredsuc
- subsubelfzo0
- fzoopth
- 2ffzoeq
- The modulo (remainder) operation - extension
- m1mod0mod1
- elmod2
- The infinite sequence builder "seq"
- smonoord
- Finite and infinite sums - extension
- fsummsndifre
- fsumsplitsndif
- fsummmodsndifre
- fsummmodsnunz
- Extensible structures - extension
- setsidel
- setsnidel
- setsv