Metamath Proof Explorer

Table of Contents - 21.31. Mathbox for Steven Nguyen

Utility theorems
1. jarrii
2. intnanrt
3. ioin9i8
4. jaodd
5. syl3an12
6. exbiii
7. sbtd
8. sbor2
9. sbalexi
10. nfalh
11. nfe2
12. nfale2
13. 19.9dev
14. 3rspcedvd
15. sn-axrep5v
16. sn-axprlem3
17. sn-exelALT
18. ssabdv
19. sn-iotalem
20. sn-iotalemcor
21. abbi1sn
22. brif2
23. brif12
24. pssexg
25. pssn0
26. psspwb
27. xppss12
28. elpwbi
29. imaopab
30. eqresfnbd
31. fmpocos
32. ovmpogad
33. ofun
34. dfqs3
35. qseq12d
36. qsalrel
37. supinf
38. mapcod
39. fisdomnn
40. ltex
41. leex
42. subex
43. absex
44. cjex
45. fzosumm1
46. ccatcan2d
Arithmetic theorems
1. c0exALT
2. 0cnALT3
3. elre0re
4. lttrii
5. remulcan2d
6. readdridaddlidd
7. 1p3e4
8. 5ne0
9. 6ne0
10. 7ne0
11. 8ne0
12. 9ne0
13. sn-1ne2
14. nnn1suc
15. readdrcl2d
16. mvrrsubd
17. laddrotrd
18. raddswap12d
19. lsubrotld
20. rsubrotld
21. lsubswap23d
22. addsubeq4com
23. sqsumi
24. negn0nposznnd
25. sqmid3api
26. decaddcom
27. sqn5i
28. sqn5ii
29. decpmulnc
30. decpmul
31. sqdeccom12
32. sq3deccom12
33. 4t5e20
34. 3rdpwhole
35. sq4
36. sq5
37. sq6
38. sq7
39. sq8
40. sq9
41. rpsscn
42. 4rp
43. 6rp
44. 7rp
45. 8rp
46. 9rp
47. 235t711
48. ex-decpmul
49. eluzp1
50. sn-eluzp1l
51. fz1sumconst
52. fz1sump1
53. oddnumth
54. nicomachus
55. sumcubes
56. ine1
57. 0tie0
58. it1ei
59. 1tiei
60. itrere
61. retire
62. iocioodisjd
63. rpabsid
Exponents and divisibility
1. oexpreposd
2. explt1d
3. expeq1d
4. expeqidd
5. exp11d
6. 0dvds0
7. absdvdsabsb
8. gcdnn0id
9. gcdle1d
10. gcdle2d
11. dvdsexpad
12. dvdsexpnn
13. dvdsexpnn0
14. dvdsexpb
15. posqsqznn
16. zdivgd
17. efsubd
18. ef11d
19. logccne0d
20. cxp112d
21. cxp111d
22. cxpi11d
23. logne0d
24. rxp112d
25. log11d
26. rplog11d
27. rxp11d
Trigonometry and Calculus
1. tanhalfpim
2. sinpim
3. cospim
4. tan3rdpi
5. sin2t3rdpi
6. cos2t3rdpi
7. sin4t3rdpi
8. cos4t3rdpi
9. asin1half
10. acos1half
11. dvun
12. redvmptabs
13. readvrec2
14. readvrec
15. resuppsinopn
16. readvcot
Independence of ax-mulcom
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. sn-remul0ord
45. resubid
46. readdrid
47. resubid1
48. renegneg
49. readdcan2
50. renegid2
51. remulneg2d
52. sn-it0e0
53. sn-negex12
54. sn-negex
55. sn-negex2
56. sn-addcand
57. sn-addrid
58. sn-addcan2d
59. reixi
60. rei4
61. sn-addid0
62. sn-mul01
63. sn-subeu
64. sn-subcl
65. sn-subf
66. resubeqsub
67. subresre
68. addinvcom
69. remulinvcom
70. remullid
71. sn-1ticom
72. sn-mullid
73. sn-it1ei
74. ipiiie0
75. remulcand
76. crediv
77. df-rediv
78. redivvald
79. rediveud
80. sn-redivcld
81. redivmuld
82. redivmul2d
83. redivcan2d
84. redivcan3d
85. rediveq0d
86. redivne0bd
87. rediveq1d
88. sn-rediv1d
89. sn-rediv0d
90. sn-redividd
91. sn-rereccld
92. rerecne0d
93. rerecidd
94. rerecid2d
95. rerecrecd
96. redivrec2d
97. rediv23d
98. redivdird
99. rediv11d
100. sn-0tie0
101. sn-mul02
102. sn-ltaddpos
103. sn-ltaddneg
104. reposdif
105. relt0neg1
106. relt0neg2
107. sn-addlt0d
108. sn-addgt0d
109. sn-nnne0
110. reelznn0nn
111. nn0addcom
112. zaddcomlem
113. zaddcom
114. renegmulnnass
115. nn0mulcom
116. zmulcomlem
117. zmulcom
118. mulgt0con1dlem
119. mulgt0con1d
120. mulgt0con2d
121. mulgt0b1d
122. sn-ltmul2d
123. sn-ltmulgt11d
124. sn-0lt1
125. sn-ltp1
126. sn-recgt0d
127. mulgt0b2d
128. sn-mulgt1d
129. reneg1lt0
130. sn-reclt0d
131. mulltgt0d
132. mullt0b1d
133. mullt0b2d
134. sn-mullt0d
135. sn-msqgt0d
136. sn-inelr
137. sn-itrere
138. sn-retire
139. cnreeu
140. sn-sup2
141. sn-sup3d
142. sn-suprcld
143. sn-suprubd
Structures
1. sn-base0
2. nelsubginvcld
3. nelsubgcld
4. nelsubgsubcld
5. rnasclg
6. frlmfielbas
7. frlmfzwrd
8. frlmfzowrd
9. frlmfzolen
10. frlmfzowrdb
11. frlmfzoccat
12. frlmvscadiccat
13. grpasscan2d
14. grpcominv1
15. grpcominv2
16. finsubmsubg
17. opprmndb
18. opprgrpb
19. opprablb
20. imacrhmcl
21. rimco
22. rictr
23. riccrng1
24. riccrng
25. domnexpgn0cl
26. drnginvrn0d
27. drngmullcan
28. drngmulrcan
29. drnginvmuld
30. ricdrng1
31. ricdrng
32. ricfld
33. asclf1
34. abvexp
35. fimgmcyclem
36. fimgmcyc
37. fidomncyc
38. fiabv
39. lvecgrp
40. lvecring
41. frlm0vald
42. frlmsnic
43. uvccl
44. uvcn0
45. psrmnd
46. mhmcopsr
47. mhmcoaddpsr
48. rhmcomulpsr
49. rhmpsr
50. rhmpsr1
51. evl0
52. evlsbagval
53. evlvvvallem
54. evlselvlem
55. evlselv
56. fsuppind
57. fsuppssindlem1
58. fsuppssindlem2
59. fsuppssind
60. mhpind
61. evlsmhpvvval
62. mhphflem
63. mhphf
64. mhphf2
65. mhphf3
66. mhphf4
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. alan
4. exor
5. rexor
6. ruvALT
7. sn-wcdeq
8. sq45
9. sum9cubes
10. sn-isghm
11. aprilfools2025
12. Standard replacements of ax-10 , ax-11 , ax-12