Metamath Proof Explorer

Table of Contents - 20.43.22. Complexity theory

1. Auxiliary theorems
   1. suppdm
   2. eluz2cnn0n1
   3. divge1b
   4. divgt1b
   5. ltsubaddb
   6. ltsubsubb
   7. ltsubadd2b
   8. divsub1dir
   9. expnegico01
   10. elfzolborelfzop1
   11. pw2m1lepw2m1
   12. zgtp1leeq
   13. flsubz
2. The modulo (remainder) operation (extension)
   1. fldivmod
   2. mod0mul
   3. modn0mul
   4. m1modmmod
   5. difmodm1lt
3. Even and odd integers
   1. nn0onn0ex
   2. nn0enn0ex
   3. nnennex
   4. nneop
   5. nneom
   6. nn0eo
   7. nnpw2even
   8. zefldiv2
   9. zofldiv2
   10. nn0ofldiv2
   11. flnn0div2ge
   12. flnn0ohalf
4. The natural logarithm on complex numbers (extension)
   1. logcxp0
   2. regt1loggt0
5. Division of functions
   1. cfdiv
   2. df-fdiv
   3. fdivval
   4. fdivmpt
   5. fdivmptf
   6. refdivmptf
   7. fdivpm
   8. refdivpm
   9. fdivmptfv
   10. refdivmptfv
6. Upper bounds
   1. cbigo
   2. df-bigo
   3. bigoval
   4. elbigofrcl
   5. elbigo
   6. elbigo2
   7. elbigo2r
   8. elbigof
   9. elbigodm
   10. elbigoimp
   11. elbigolo1
7. Logarithm to an arbitrary base (extension)
   1. rege1logbrege0
   2. rege1logbzge0
   3. fllogbd
   4. relogbmulbexp
   5. relogbdivb
   6. logbge0b
   7. logblt1b
8. The binary logarithm
   1. fldivexpfllog2
   2. nnlog2ge0lt1
   3. logbpw2m1
   4. fllog2
9. Binary length
   1. cblen
   2. df-blen
   3. blenval
   4. blen0
   5. blenn0
   6. blenre
   7. blennn
   8. blennnelnn
   9. blennn0elnn
   10. blenpw2
   11. blenpw2m1
   12. nnpw2blen
   13. nnpw2blenfzo
   14. nnpw2blenfzo2
   15. nnpw2pmod
   16. blen1
   17. blen2
   18. nnpw2p
   19. nnpw2pb
   20. blen1b
   21. blennnt2
   22. nnolog2flm1
   23. blennn0em1
   24. blennngt2o2
   25. blengt1fldiv2p1
   26. blennn0e2
10. Digits
    1. cdig
    2. df-dig
    3. digfval
    4. digval
    5. digvalnn0
    6. nn0digval
    7. dignn0fr
    8. dignn0ldlem
    9. dignnld
    10. dig2nn0ld
    11. dig2nn1st
    12. dig0
    13. digexp
    14. dig1
    15. 0dig1
    16. 0dig2pr01
    17. dig2nn0
    18. 0dig2nn0e
    19. 0dig2nn0o
    20. dig2bits
11. Nonnegative integer as sum of its shifted digits
    1. dignn0flhalflem1
    2. dignn0flhalflem2
    3. dignn0ehalf
    4. dignn0flhalf
    5. nn0sumshdiglemA
    6. nn0sumshdiglemB
    7. nn0sumshdiglem1
    8. nn0sumshdiglem2
    9. nn0sumshdig
12. Algorithms for the multiplication of nonnegative integers
    1. nn0mulfsum
    2. nn0mullong