Metamath Proof Explorer

Table of Contents - 21.50.6. General auxiliary theorems (2)

1. Logical conjunction - extension
   1. an4com24
2. Abbreviated conjunction and disjunction of three wff's - extension
   1. 3an4ancom24
   2. 4an21
3. Negated membership (alternative)
   1. cnelbr
   2. df-nelbr
   3. dfnelbr2
   4. nelbr
   5. nelbrim
   6. nelbrnel
   7. nelbrnelim
4. The empty set - extension
   1. ralralimp
5. Indexed union and intersection - extension
   1. otiunsndisjX
6. Functions - extension
   1. fvifeq
   2. rnfdmpr
   3. imarnf1pr
   4. funop1
   5. fun2dmnopgexmpl
   6. opabresex0d
   7. opabbrfex0d
   8. opabresexd
   9. opabbrfexd
   10. f1oresf1orab
   11. f1oresf1o
   12. f1oresf1o2
7. Maps-to notation - extension
   1. fvmptrab
   2. fvmptrabdm
8. Subtraction - extension
   1. cnambpcma
   2. cnapbmcpd
   3. addsubeq0
9. Ordering on reals (cont.) - extension
   1. leaddsuble
   2. 2leaddle2
   3. ltnltne
   4. p1lep2
   5. ltsubsubaddltsub
   6. zm1nn
10. Imaginary and complex number properties - extension
    1. readdcnnred
    2. resubcnnred
    3. recnmulnred
    4. cndivrenred
    5. sqrtnegnre
11. Nonnegative integers (as a subset of complex numbers) - extension
    1. nn0resubcl
12. Integers (as a subset of complex numbers) - extension
    1. zgeltp1eq
13. Decimal arithmetic - extension
    1. 1t10e1p1e11
    2. deccarry
14. Upper sets of integers - extension
    1. eluzge0nn0
15. Infinity and the extended real number system (cont.) - extension
    1. nltle2tri
16. Finite intervals of integers - extension
    1. ssfz12
    2. elfz2z
    3. 2elfz3nn0
    4. fz0addcom
    5. 2elfz2melfz
    6. fz0addge0
    7. elfzlble
    8. elfzelfzlble
17. Half-open integer ranges - extension
    1. fzopred
    2. fzopredsuc
    3. 1fzopredsuc
    4. el1fzopredsuc
    5. subsubelfzo0
    6. 2ffzoeq
18. The floor and ceiling functions - extension
    1. 2ltceilhalf
    2. ceilhalfgt1
    3. ceilhalfelfzo1
    4. gpgedgvtx1lem
    5. 2tceilhalfelfzo1
    6. ceilbi
    7. ceilhalf1
    8. rehalfge1
    9. ceilhalfnn
    10. 1elfzo1ceilhalf1
19. The modulo (remainder) operation - extension
    1. fldivmod
    2. ceildivmod
    3. ceil5half3
    4. submodaddmod
    5. difltmodne
    6. zplusmodne
    7. addmodne
    8. plusmod5ne
    9. zp1modne
    10. p1modne
    11. m1modne
    12. minusmod5ne
    13. submodlt
    14. submodneaddmod
    15. m1modnep2mod
    16. minusmodnep2tmod
    17. m1mod0mod1
    18. elmod2
    19. mod0mul
    20. modn0mul
    21. m1modmmod
    22. difmodm1lt
    23. 8mod5e3
    24. modmkpkne
    25. modmknepk
    26. modlt0b
    27. mod2addne
    28. modm1nep1
    29. modm2nep1
    30. modp2nep1
    31. modm1nep2
    32. modm1nem2
    33. modm1p1ne
20. The infinite sequence builder "seq"
    1. smonoord
21. Finite and infinite sums - extension
    1. fsummsndifre
    2. fsumsplitsndif
    3. fsummmodsndifre
    4. fsummmodsnunz
22. Extensible structures - extension
    1. setsidel
    2. setsnidel
    3. setsv