Metamath Proof Explorer

Table of Contents - 20.27. Mathbox for Steven Nguyen

1. ${
   1. ioin9i8
   2. jaodd
   3. nsb
   4. sbn1
   5. sbor2
   6. sn-elabg
   7. 3rspcedvd
   8. rabeqcda
   9. rabdif
   10. sn-axrep5v
   11. sn-axprlem3
   12. sn-el
   13. sn-dtru
   14. pssexg
   15. pssn0
   16. psspwb
   17. xppss12
   18. elpwbi
   19. opelxpii
   20. iunsn
   21. imaopab
   22. fnsnbt
   23. fnimasnd
   24. dfqs2
   25. dfqs3
   26. qseq12d
   27. qsalrel
   28. fzosumm1
   29. ccatcan2d
   30. nelsubginvcld
   31. nelsubgcld
   32. nelsubgsubcld
   33. rnasclg
   34. selvval2lem1
   35. selvval2lem2
   36. selvval2lem3
   37. selvval2lemn
   38. selvval2lem4
   39. selvval2lem5
   40. selvcl
   41. frlmfielbas
   42. frlmfzwrd
   43. frlmfzowrd
   44. frlmfzolen
   45. frlmfzowrdb
   46. frlmfzoccat
   47. frlmvscadiccat
   48. lvecgrp
   49. lvecring
   50. lmhmlvec
   51. frlmsnic
   52. uvccl
   53. uvcn0
2. Arithmetic theorems
   1. c0exALT
   2. 0cnALT3
   3. elre0re
   4. 1t1e1ALT
   5. remulcan2d
   6. readdid1addid2d
   7. sn-1ne2
   8. nnn1suc
   9. nnadd1com
   10. nnaddcom
   11. nnaddcomli
   12. nnadddir
   13. nnmul1com
   14. nnmulcom
   15. addsubeq4com
   16. sqsumi
   17. negn0nposznnd
   18. sqmid3api
   19. decaddcom
   20. sqn5i
   21. sqn5ii
   22. decpmulnc
   23. decpmul
   24. sqdeccom12
   25. sq3deccom12
   26. 235t711
   27. ex-decpmul
3. Exponents
   1. oexpreposd
   2. cxpgt0d
   3. dvdsexpim
   4. nn0rppwr
   5. expgcd
   6. nn0expgcd
   7. zexpgcd
   8. numdenexp
   9. numexp
   10. denexp
   11. exp11d
   12. ltexp1d
   13. ltexp1dd
   14. zrtelqelz
   15. zrtdvds
   16. rtprmirr
4. Real subtraction
   1. cresub
   2. df-resub
   3. resubval
   4. renegeulemv
   5. renegeulem
   6. renegeu
   7. rernegcl
   8. renegadd
   9. renegid
   10. reneg0addid2
   11. resubeulem1
   12. resubeulem2
   13. resubeu
   14. rersubcl
   15. resubadd
   16. resubaddd
   17. resubf
   18. repncan2
   19. repncan3
   20. readdsub
   21. reladdrsub
   22. reltsub1
   23. reltsubadd2
   24. resubcan2
   25. resubsub4
   26. rennncan2
   27. renpncan3
   28. repnpcan
   29. reppncan
   30. resubidaddid1lem
   31. resubidaddid1
   32. resubdi
   33. re1m1e0m0
   34. sn-00idlem1
   35. sn-00idlem2
   36. sn-00idlem3
   37. sn-00id
   38. re0m0e0
   39. readdid2
   40. sn-addid2
   41. remul02
   42. sn-0ne2
   43. remul01
   44. resubid
   45. readdid1
   46. resubid1
   47. renegneg
   48. readdcan2
   49. sn-ltaddpos
   50. relt0neg1
   51. relt0neg2
   52. sn-0lt1
   53. sn-ltp1
   54. remulinvcom
   55. remulid2
   56. remulcand
5. Looking at a corner in 3D space, one can see three right angles. It is
   1. cprjsp
   2. df-prjsp
   3. prjspval
   4. prjsprel
   5. prjspertr
   6. prjsperref
   7. prjspersym
   8. prjsper
   9. prjspreln0
   10. prjspvs
   11. prjsprellsp
   12. prjspeclsp
   13. prjspval2
   14. cprjspn
   15. df-prjspn
   16. prjspnval
   17. prjspnval2
   18. 0prjspnlem
   19. 0prjspnrel
   20. 0prjspn
6. $( TODO:
   1. dffltz
   2. fltne
   3. fltltc
   4. fltnltalem
   5. fltnlta