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. abslt
83. absle
84. abssubne0
85. absdiflt
86. absdifle
87. elicc4abs
88. lenegsq
89. releabs
90. recval
91. absidm
92. absgt0
93. nnabscl
94. abssub
95. abssubge0
96. abssuble0
97. absmax
98. abstri
99. abs3dif
100. abs2dif
101. abs2dif2
102. abs2difabs
103. abs1m
104. recan
105. absf
106. abs3lem
107. abslem2
108. rddif
109. absrdbnd
110. fzomaxdiflem
111. fzomaxdif
112. uzin2
113. rexanuz
114. rexanre
115. rexfiuz
116. rexuz3
117. rexanuz2
118. r19.29uz
119. r19.2uz
120. rexuzre
121. rexico
122. cau3lem
123. cau3
124. cau4
125. caubnd2
126. caubnd
127. sqreulem
128. sqreu
129. sqrtcl
130. sqrtthlem
131. sqrtf
132. sqrtth
133. sqrtrege0
134. eqsqrtor
135. eqsqrtd
136. eqsqrt2d
137. amgm2
138. sqrtthi
139. sqrtcli
140. sqrtgt0i
141. sqrtmsqi
142. sqrtsqi
143. sqsqrti
144. sqrtge0i
145. absidi
146. absnidi
147. leabsi
148. absori
149. absrei
150. sqrtpclii
151. sqrtgt0ii
152. sqrt11i
153. sqrtmuli
154. sqrtmulii
155. sqrtmsq2i
156. sqrtlei
157. sqrtlti
158. abslti
159. abslei
160. cnsqrt00
161. absvalsqi
162. absvalsq2i
163. abscli
164. absge0i
165. absval2i
166. abs00i
167. absgt0i
168. absnegi
169. abscji
170. releabsi
171. abssubi
172. absmuli
173. sqabsaddi
174. sqabssubi
175. absdivzi
176. abstrii
177. abs3difi
178. abs3lemi
179. rpsqrtcld
180. sqrtgt0d
181. absnidd
182. leabsd
183. absord
184. absred
185. resqrtcld
186. sqrtmsqd
187. sqrtsqd
188. sqrtge0d
189. sqrtnegd
190. absidd
191. sqrtdivd
192. sqrtmuld
193. sqrtsq2d
194. sqrtled
195. sqrtltd
196. sqr11d
197. absltd
198. absled
199. abssubge0d
200. abssuble0d
201. absdifltd
202. absdifled
203. icodiamlt
204. abscld
205. sqrtcld
206. sqrtrege0d
207. sqsqrtd
208. msqsqrtd
209. sqr00d
210. absvalsqd
211. absvalsq2d
212. absge0d
213. absval2d
214. abs00d
215. absne0d
216. absrpcld
217. absnegd
218. abscjd
219. releabsd
220. absexpd
221. abssubd
222. absmuld
223. absdivd
224. abstrid
225. abs2difd
226. abs2dif2d
227. abs2difabsd
228. abs3difd
229. abs3lemd
230. reusq0
231. bhmafibid1cn
232. bhmafibid2cn
233. bhmafibid1
234. bhmafibid2