Metamath Proof Explorer

Table of Contents - 5.9. Elementary real and complex functions

The "shift" operation
1. cshi
2. df-shft
3. shftlem
4. shftuz
5. shftfval
6. shftdm
7. shftfib
8. shftfn
9. shftval
10. shftval2
11. shftval3
12. shftval4
13. shftval5
14. shftf
15. 2shfti
16. shftidt2
17. shftidt
18. shftcan1
19. shftcan2
20. seqshft
Signum (sgn or sign) function
1. csgn
2. df-sgn
3. sgnval
4. sgn0
5. sgnp
6. sgnrrp
7. sgn1
8. sgnpnf
9. sgnn
10. sgnmnf
Real and imaginary parts; conjugate
1. ccj
2. cre
3. cim
4. df-cj
5. df-re
6. df-im
7. cjval
8. cjth
9. cjf
10. cjcl
11. reval
12. imval
13. imre
14. reim
15. recl
16. imcl
17. ref
18. imf
19. crre
20. crim
21. replim
22. remim
23. reim0
24. reim0b
25. rereb
26. mulre
27. rere
28. cjreb
29. recj
30. reneg
31. readd
32. resub
33. remullem
34. remul
35. remul2
36. rediv
37. imcj
38. imneg
39. imadd
40. imsub
41. immul
42. immul2
43. imdiv
44. cjre
45. cjcj
46. cjadd
47. cjmul
48. ipcnval
49. cjmulrcl
50. cjmulval
51. cjmulge0
52. cjneg
53. addcj
54. cjsub
55. cjexp
56. imval2
57. re0
58. im0
59. re1
60. im1
61. rei
62. imi
63. cj0
64. cji
65. cjreim
66. cjreim2
67. cj11
68. cjne0
69. cjdiv
70. cnrecnv
71. sqeqd
72. recli
73. imcli
74. cjcli
75. replimi
76. cjcji
77. reim0bi
78. rerebi
79. cjrebi
80. recji
81. imcji
82. cjmulrcli
83. cjmulvali
84. cjmulge0i
85. renegi
86. imnegi
87. cjnegi
88. addcji
89. readdi
90. imaddi
91. remuli
92. immuli
93. cjaddi
94. cjmuli
95. ipcni
96. cjdivi
97. crrei
98. crimi
99. recld
100. imcld
101. cjcld
102. replimd
103. remimd
104. cjcjd
105. reim0bd
106. rerebd
107. cjrebd
108. cjne0d
109. recjd
110. imcjd
111. cjmulrcld
112. cjmulvald
113. cjmulge0d
114. renegd
115. imnegd
116. cjnegd
117. addcjd
118. cjexpd
119. readdd
120. imaddd
121. resubd
122. imsubd
123. remuld
124. immuld
125. cjaddd
126. cjmuld
127. ipcnd
128. cjdivd
129. rered
130. reim0d
131. cjred
132. remul2d
133. immul2d
134. redivd
135. imdivd
136. crred
137. crimd
Square root; absolute value
1. csqrt
2. cabs
3. df-sqrt
4. df-abs
5. sqrtval
6. absval
7. rennim
8. cnpart
9. sqrt0
10. 01sqrexlem1
11. 01sqrexlem2
12. 01sqrexlem3
13. 01sqrexlem4
14. 01sqrexlem5
15. 01sqrexlem6
16. 01sqrexlem7
17. 01sqrex
18. resqrex
19. sqrmo
20. resqreu
21. resqrtcl
22. resqrtthlem
23. resqrtth
24. remsqsqrt
25. sqrtge0
26. sqrtgt0
27. sqrtmul
28. sqrtle
29. sqrtlt
30. sqrt11
31. sqrt00
32. rpsqrtcl
33. sqrtdiv
34. sqrtneglem
35. sqrtneg
36. sqrtsq2
37. sqrtsq
38. sqrtmsq
39. sqrt1
40. sqrt4
41. sqrt9
42. sqrt2gt1lt2
43. sqrtm1
44. nn0sqeq1
45. absneg
46. abscl
47. abscj
48. absvalsq
49. absvalsq2
50. sqabsadd
51. sqabssub
52. absval2
53. abs0
54. absi
55. absge0
56. absrpcl
57. abs00
58. abs00ad
59. abs00bd
60. absreimsq
61. absreim
62. absmul
63. absdiv
64. absid
65. abs1
66. absnid
67. leabs
68. absor
69. absre
70. absresq
71. absmod0
72. absexp
73. absexpz
74. abssq
75. sqabs
76. absrele
77. absimle
78. max0add
79. absz
80. nn0abscl
81. zabscl
82. zabs0b
83. abslt
84. absle
85. abssubne0
86. absdiflt
87. absdifle
88. elicc4abs
89. lenegsq
90. releabs
91. recval
92. absidm
93. absgt0
94. nnabscl
95. abssub
96. abssubge0
97. abssuble0
98. absmax
99. abstri
100. abs3dif
101. abs2dif
102. abs2dif2
103. abs2difabs
104. abs1m
105. recan
106. absf
107. abs3lem
108. abslem2
109. rddif
110. absrdbnd
111. fzomaxdiflem
112. fzomaxdif
113. uzin2
114. rexanuz
115. rexanre
116. rexfiuz
117. rexuz3
118. rexanuz2
119. r19.29uz
120. r19.2uz
121. rexuzre
122. rexico
123. cau3lem
124. cau3
125. cau4
126. caubnd2
127. caubnd
128. sqreulem
129. sqreu
130. sqrtcl
131. sqrtthlem
132. sqrtf
133. sqrtth
134. sqrtrege0
135. eqsqrtor
136. eqsqrtd
137. eqsqrt2d
138. amgm2
139. sqrtthi
140. sqrtcli
141. sqrtgt0i
142. sqrtmsqi
143. sqrtsqi
144. sqsqrti
145. sqrtge0i
146. absidi
147. absnidi
148. leabsi
149. absori
150. absrei
151. sqrtpclii
152. sqrtgt0ii
153. sqrt11i
154. sqrtmuli
155. sqrtmulii
156. sqrtmsq2i
157. sqrtlei
158. sqrtlti
159. abslti
160. abslei
161. cnsqrt00
162. absvalsqi
163. absvalsq2i
164. abscli
165. absge0i
166. absval2i
167. abs00i
168. absgt0i
169. absnegi
170. abscji
171. releabsi
172. abssubi
173. absmuli
174. sqabsaddi
175. sqabssubi
176. absdivzi
177. abstrii
178. abs3difi
179. abs3lemi
180. rpsqrtcld
181. sqrtgt0d
182. absnidd
183. leabsd
184. absord
185. absred
186. resqrtcld
187. sqrtmsqd
188. sqrtsqd
189. sqrtge0d
190. sqrtnegd
191. absidd
192. sqrtdivd
193. sqrtmuld
194. sqrtsq2d
195. sqrtled
196. sqrtltd
197. sqr11d
198. nn0absid
199. nn0absidi
200. absltd
201. absled
202. abssubge0d
203. abssuble0d
204. absdifltd
205. absdifled
206. icodiamlt
207. abscld
208. sqrtcld
209. sqrtrege0d
210. sqsqrtd
211. msqsqrtd
212. sqr00d
213. absvalsqd
214. absvalsq2d
215. absge0d
216. absval2d
217. abs00d
218. absne0d
219. absrpcld
220. absnegd
221. abscjd
222. releabsd
223. absexpd
224. abssubd
225. absmuld
226. absdivd
227. abstrid
228. abs2difd
229. abs2dif2d
230. abs2difabsd
231. abs3difd
232. abs3lemd
233. reusq0
234. bhmafibid1cn
235. bhmafibid2cn
236. bhmafibid1
237. bhmafibid2