Metamath Proof Explorer

Table of Contents - 21.29. Mathbox for Steven Nguyen

Utility theorems
1. intnanrt
2. ioin9i8
3. jaodd
4. syl3an12
5. sbtd
6. sbor2
7. 19.9dev
8. 3rspcedvdw
9. 3rspcedvd
10. sn-axrep5v
11. sn-axprlem3
12. sn-exelALT
13. ss2ab1
14. ssabdv
15. sn-iotalem
16. sn-iotalemcor
17. abbi1sn
18. brif2
19. brif12
20. pssexg
21. pssn0
22. psspwb
23. xppss12
24. coexd
25. elpwbi
26. imaopab
27. fnsnbt
28. fnimasnd
29. eqresfnbd
30. f1o2d2
31. fmpocos
32. ovmpogad
33. ofun
34. dfqs2
35. dfqs3
36. qseq12d
37. qsalrel
38. elmapssresd
39. mapcod
40. fzosumm1
41. ccatcan2d
Structures
1. nelsubginvcld
2. nelsubgcld
3. nelsubgsubcld
4. rnasclg
5. frlmfielbas
6. frlmfzwrd
7. frlmfzowrd
8. frlmfzolen
9. frlmfzowrdb
10. frlmfzoccat
11. frlmvscadiccat
12. grpasscan2d
13. grpcominv1
14. grpcominv2
15. finsubmsubg
16. imacrhmcl
17. rimrcl1
18. rimrcl2
19. rimcnv
20. rimco
21. ricsym
22. rictr
23. riccrng1
24. riccrng
25. drnginvrn0d
26. drngmulcanad
27. drngmulcan2ad
28. drnginvmuld
29. ricdrng1
30. ricdrng
31. ricfld
32. lvecgrp
33. lvecring
34. frlm0vald
35. frlmsnic
36. uvccl
37. uvcn0
38. pwselbasr
39. pwsgprod
40. psrmnd
41. psrbagres
42. mpllmodd
43. mplringd
44. mplcrngd
45. mplsubrgcl
46. mhmcopsr
47. mhmcoaddpsr
48. rhmcomulpsr
49. rhmpsr
50. mhmcompl
51. mhmcoaddmpl
52. rhmcomulmpl
53. rhmmpl
54. rhmpsr1
55. mhmcoply1
56. rhmply1
57. rhmply1vr1
58. ply1vscl
59. rhmply1vsca
60. rhmply1mon
61. mplascl0
62. mplascl1
63. mplmapghm
64. evl0
65. evlscl
66. evlsval3
67. evlsvval
68. evlsvvvallem
69. evlsvvvallem2
70. evlsvvval
71. evlsscaval
72. evlsvarval
73. evlsbagval
74. evlsexpval
75. evlsaddval
76. evlsmulval
77. evlsmaprhm
78. evlsevl
79. evlcl
80. evlvvval
81. evlvvvallem
82. evladdval
83. evlmulval
84. selvcllem1
85. selvcllem2
86. selvcllem3
87. selvcllemh
88. selvcllem4
89. selvcllem5
90. selvcl
91. selvval2
92. selvvvval
93. evlselvlem
94. evlselv
95. selvadd
96. selvmul
97. fsuppind
98. fsuppssindlem1
99. fsuppssindlem2
100. fsuppssind
101. mhpind
102. evlsmhpvvval
103. mhphflem
104. mhphf
105. mhphf2
106. mhphf3
107. mhphf4
Arithmetic theorems
1. c0exALT
2. 0cnALT3
3. elre0re
4. 1t1e1ALT
5. remulcan2d
6. readdridaddlidd
7. sn-1ne2
8. nnn1suc
9. nnadd1com
10. nnaddcom
11. nnaddcomli
12. nnadddir
13. nnmul1com
14. nnmulcom
15. readdrcl2d
16. mvrrsubd
17. laddrotrd
18. raddcom12d
19. lsubrotld
20. lsubcom23d
21. addsubeq4com
22. sqsumi
23. negn0nposznnd
24. sqmid3api
25. decaddcom
26. sqn5i
27. sqn5ii
28. decpmulnc
29. decpmul
30. sqdeccom12
31. sq3deccom12
32. 4t5e20
33. sq9
34. 235t711
35. ex-decpmul
36. fz1sumconst
37. fz1sump1
38. oddnumth
39. nicomachus
40. sumcubes
41. pine0
42. ine1
43. 0tie0
44. it1ei
45. 1tiei
46. itrere
47. retire
Exponents and divisibility
1. oexpreposd
2. ltexp1d
3. ltexp1dd
4. exp11nnd
5. exp11d
6. 0dvds0
7. absdvdsabsb
8. dvdsexpim
9. gcdnn0id
10. gcdle1d
11. gcdle2d
12. dvdsexpad
13. nn0rppwr
14. expgcd
15. nn0expgcd
16. zexpgcd
17. numdenexp
18. numexp
19. denexp
20. dvdsexpnn
21. dvdsexpnn0
22. dvdsexpb
23. posqsqznn
24. zrtelqelz
25. zrtdvds
26. rtprmirr
27. zdivgd
28. efne0d
29. efsubd
30. ef11d
31. logccne0d
32. cxp112d
33. cxp111d
34. cxpi11d
35. logne0d
36. rxp112d
37. log11d
38. rplog11d
39. rxp11d
Real subtraction
1. cresub
2. df-resub
3. resubval
4. renegeulemv
5. renegeulem
6. renegeu
7. rernegcl
8. renegadd
9. renegid
10. reneg0addlid
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. resubidaddlidlem
31. resubidaddlid
32. resubdi
33. re1m1e0m0
34. sn-00idlem1
35. sn-00idlem2
36. sn-00idlem3
37. sn-00id
38. re0m0e0
39. readdlid
40. sn-addlid
41. remul02
42. sn-0ne2
43. remul01
44. resubid
45. readdrid
46. resubid1
47. renegneg
48. readdcan2
49. renegid2
50. remulneg2d
51. sn-it0e0
52. sn-negex12
53. sn-negex
54. sn-negex2
55. sn-addcand
56. sn-addrid
57. sn-addcan2d
58. reixi
59. rei4
60. sn-addid0
61. sn-mul01
62. sn-subeu
63. sn-subcl
64. sn-subf
65. resubeqsub
66. subresre
67. addinvcom
68. remulinvcom
69. remullid
70. sn-1ticom
71. sn-mullid
72. sn-it1ei
73. ipiiie0
74. remulcand
75. sn-0tie0
76. sn-mul02
77. sn-ltaddpos
78. sn-ltaddneg
79. reposdif
80. relt0neg1
81. relt0neg2
82. sn-addlt0d
83. sn-addgt0d
84. sn-nnne0
85. reelznn0nn
86. nn0addcom
87. zaddcomlem
88. zaddcom
89. renegmulnnass
90. nn0mulcom
91. zmulcomlem
92. zmulcom
93. mulgt0con1dlem
94. mulgt0con1d
95. mulgt0con2d
96. mulgt0b2d
97. sn-ltmul2d
98. sn-0lt1
99. sn-ltp1
100. reneg1lt0
101. sn-inelr
102. sn-itrere
103. sn-retire
104. cnreeu
105. sn-sup2
Projective spaces
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. prjspnerlem
18. prjspnval2
19. prjspner
20. prjspnvs
21. prjspnssbas
22. prjspnn0
23. 0prjspnlem
24. prjspnfv01
25. prjspner01
26. prjspner1
27. 0prjspnrel
28. 0prjspn
29. cprjcrv
30. df-prjcrv
31. prjcrvfval
32. prjcrvval
33. prjcrv0
Basic reductions for Fermat's Last Theorem
1. dffltz
2. fltmul
3. fltdiv
4. flt0
5. fltdvdsabdvdsc
6. fltabcoprmex
7. fltaccoprm
8. fltbccoprm
9. fltabcoprm
10. infdesc
11. fltne
12. flt4lem
13. flt4lem1
14. flt4lem2
15. flt4lem3
16. flt4lem4
17. flt4lem5
18. flt4lem5elem
19. flt4lem5a
20. flt4lem5b
21. flt4lem5c
22. flt4lem5d
23. flt4lem5e
24. flt4lem5f
25. flt4lem6
26. flt4lem7
27. nna4b4nsq
28. fltltc
29. fltnltalem
30. fltnlta
Exemplar theorems
1. iddii
2. bicomdALT
3. elabgw
4. elab2gw
5. elrab2w
6. ruvALT
7. sn-wcdeq
8. sq45
9. sum9cubes
10. acos1half
11. aprilfools2025