Metamath Proof Explorer
Table of Contents - 21.29. Mathbox for Steven Nguyen
- Utility theorems
- intnanrt
- ioin9i8
- jaodd
- syl3an12
- sbtd
- sbor2
- 19.9dev
- 3rspcedvdw
- 3rspcedvd
- sn-axrep5v
- sn-axprlem3
- sn-exelALT
- ss2ab1
- ssabdv
- sn-iotalem
- sn-iotalemcor
- abbi1sn
- brif2
- brif12
- pssexg
- pssn0
- psspwb
- xppss12
- coexd
- elpwbi
- imaopab
- fnsnbt
- fnimasnd
- eqresfnbd
- f1o2d2
- fmpocos
- ovmpogad
- ofun
- dfqs2
- dfqs3
- qseq12d
- qsalrel
- elmapssresd
- mapcod
- fzosumm1
- ccatcan2d
- Structures
- nelsubginvcld
- nelsubgcld
- nelsubgsubcld
- rnasclg
- frlmfielbas
- frlmfzwrd
- frlmfzowrd
- frlmfzolen
- frlmfzowrdb
- frlmfzoccat
- frlmvscadiccat
- grpasscan2d
- grpcominv1
- grpcominv2
- finsubmsubg
- imacrhmcl
- rimrcl1
- rimrcl2
- rimcnv
- rimco
- ricsym
- rictr
- riccrng1
- riccrng
- drnginvrn0d
- drngmulcanad
- drngmulcan2ad
- drnginvmuld
- ricdrng1
- ricdrng
- ricfld
- lvecgrp
- lvecring
- frlm0vald
- frlmsnic
- uvccl
- uvcn0
- pwselbasr
- pwsgprod
- psrmnd
- psrbagres
- mpllmodd
- mplringd
- mplcrngd
- mplsubrgcl
- mhmcopsr
- mhmcoaddpsr
- rhmcomulpsr
- rhmpsr
- mhmcompl
- mhmcoaddmpl
- rhmcomulmpl
- rhmmpl
- rhmpsr1
- mhmcoply1
- rhmply1
- rhmply1vr1
- ply1vscl
- rhmply1vsca
- rhmply1mon
- mplascl0
- mplascl1
- mplmapghm
- evl0
- evlscl
- evlsval3
- evlsvval
- evlsvvvallem
- evlsvvvallem2
- evlsvvval
- evlsscaval
- evlsvarval
- evlsbagval
- evlsexpval
- evlsaddval
- evlsmulval
- evlsmaprhm
- evlsevl
- evlcl
- evlvvval
- evlvvvallem
- evladdval
- evlmulval
- selvcllem1
- selvcllem2
- selvcllem3
- selvcllemh
- selvcllem4
- selvcllem5
- selvcl
- selvval2
- selvvvval
- evlselvlem
- evlselv
- selvadd
- selvmul
- fsuppind
- fsuppssindlem1
- fsuppssindlem2
- fsuppssind
- mhpind
- evlsmhpvvval
- mhphflem
- mhphf
- mhphf2
- mhphf3
- mhphf4
- Arithmetic theorems
- c0exALT
- 0cnALT3
- elre0re
- 1t1e1ALT
- remulcan2d
- readdridaddlidd
- sn-1ne2
- nnn1suc
- nnadd1com
- nnaddcom
- nnaddcomli
- nnadddir
- nnmul1com
- nnmulcom
- readdrcl2d
- mvrrsubd
- laddrotrd
- raddcom12d
- lsubrotld
- lsubcom23d
- addsubeq4com
- sqsumi
- negn0nposznnd
- sqmid3api
- decaddcom
- sqn5i
- sqn5ii
- decpmulnc
- decpmul
- sqdeccom12
- sq3deccom12
- 4t5e20
- sq9
- 235t711
- ex-decpmul
- fz1sumconst
- fz1sump1
- oddnumth
- nicomachus
- sumcubes
- pine0
- ine1
- 0tie0
- it1ei
- 1tiei
- itrere
- retire
- Exponents and divisibility
- oexpreposd
- ltexp1d
- ltexp1dd
- exp11nnd
- exp11d
- 0dvds0
- absdvdsabsb
- dvdsexpim
- gcdnn0id
- gcdle1d
- gcdle2d
- dvdsexpad
- nn0rppwr
- expgcd
- nn0expgcd
- zexpgcd
- numdenexp
- numexp
- denexp
- dvdsexpnn
- dvdsexpnn0
- dvdsexpb
- posqsqznn
- zrtelqelz
- zrtdvds
- rtprmirr
- zdivgd
- efne0d
- efsubd
- ef11d
- logccne0d
- cxp112d
- cxp111d
- cxpi11d
- logne0d
- rxp112d
- log11d
- rplog11d
- rxp11d
- Real subtraction
- cresub
- df-resub
- resubval
- renegeulemv
- renegeulem
- renegeu
- rernegcl
- renegadd
- renegid
- reneg0addlid
- resubeulem1
- resubeulem2
- resubeu
- rersubcl
- resubadd
- resubaddd
- resubf
- repncan2
- repncan3
- readdsub
- reladdrsub
- reltsub1
- reltsubadd2
- resubcan2
- resubsub4
- rennncan2
- renpncan3
- repnpcan
- reppncan
- resubidaddlidlem
- resubidaddlid
- resubdi
- re1m1e0m0
- sn-00idlem1
- sn-00idlem2
- sn-00idlem3
- sn-00id
- re0m0e0
- readdlid
- sn-addlid
- remul02
- sn-0ne2
- remul01
- resubid
- readdrid
- resubid1
- renegneg
- readdcan2
- renegid2
- remulneg2d
- sn-it0e0
- sn-negex12
- sn-negex
- sn-negex2
- sn-addcand
- sn-addrid
- sn-addcan2d
- reixi
- rei4
- sn-addid0
- sn-mul01
- sn-subeu
- sn-subcl
- sn-subf
- resubeqsub
- subresre
- addinvcom
- remulinvcom
- remullid
- sn-1ticom
- sn-mullid
- sn-it1ei
- ipiiie0
- remulcand
- sn-0tie0
- sn-mul02
- sn-ltaddpos
- sn-ltaddneg
- reposdif
- relt0neg1
- relt0neg2
- sn-addlt0d
- sn-addgt0d
- sn-nnne0
- reelznn0nn
- nn0addcom
- zaddcomlem
- zaddcom
- renegmulnnass
- nn0mulcom
- zmulcomlem
- zmulcom
- mulgt0con1dlem
- mulgt0con1d
- mulgt0con2d
- mulgt0b2d
- sn-ltmul2d
- sn-0lt1
- sn-ltp1
- reneg1lt0
- sn-inelr
- sn-itrere
- sn-retire
- cnreeu
- sn-sup2
- Projective spaces
- cprjsp
- df-prjsp
- prjspval
- prjsprel
- prjspertr
- prjsperref
- prjspersym
- prjsper
- prjspreln0
- prjspvs
- prjsprellsp
- prjspeclsp
- prjspval2
- cprjspn
- df-prjspn
- prjspnval
- prjspnerlem
- prjspnval2
- prjspner
- prjspnvs
- prjspnssbas
- prjspnn0
- 0prjspnlem
- prjspnfv01
- prjspner01
- prjspner1
- 0prjspnrel
- 0prjspn
- cprjcrv
- df-prjcrv
- prjcrvfval
- prjcrvval
- prjcrv0
- Basic reductions for Fermat's Last Theorem
- dffltz
- fltmul
- fltdiv
- flt0
- fltdvdsabdvdsc
- fltabcoprmex
- fltaccoprm
- fltbccoprm
- fltabcoprm
- infdesc
- fltne
- flt4lem
- flt4lem1
- flt4lem2
- flt4lem3
- flt4lem4
- flt4lem5
- flt4lem5elem
- flt4lem5a
- flt4lem5b
- flt4lem5c
- flt4lem5d
- flt4lem5e
- flt4lem5f
- flt4lem6
- flt4lem7
- nna4b4nsq
- fltltc
- fltnltalem
- fltnlta
- Exemplar theorems
- iddii
- bicomdALT
- elabgw
- elab2gw
- elrab2w
- ruvALT
- sn-wcdeq
- sq45
- sum9cubes
- acos1half
- aprilfools2025