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. sqr0lem
10. sqrt0
11. sqrlem1
12. sqrlem2
13. sqrlem3
14. sqrlem4
15. sqrlem5
16. sqrlem6
17. sqrlem7
18. 01sqrex
19. resqrex
20. sqrmo
21. resqreu
22. resqrtcl
23. resqrtthlem
24. resqrtth
25. remsqsqrt
26. sqrtge0
27. sqrtgt0
28. sqrtmul
29. sqrtle
30. sqrtlt
31. sqrt11
32. sqrt00
33. rpsqrtcl
34. sqrtdiv
35. sqrtneglem
36. sqrtneg
37. sqrtsq2
38. sqrtsq
39. sqrtmsq
40. sqrt1
41. sqrt4
42. sqrt9
43. sqrt2gt1lt2
44. sqrtm1
45. nn0sqeq1
46. absneg
47. abscl
48. abscj
49. absvalsq
50. absvalsq2
51. sqabsadd
52. sqabssub
53. absval2
54. abs0
55. absi
56. absge0
57. absrpcl
58. abs00
59. abs00ad
60. abs00bd
61. absreimsq
62. absreim
63. absmul
64. absdiv
65. absid
66. abs1
67. absnid
68. leabs
69. absor
70. absre
71. absresq
72. absmod0
73. absexp
74. absexpz
75. abssq
76. sqabs
77. absrele
78. absimle
79. max0add
80. absz
81. nn0abscl
82. zabscl
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. absltd
199. absled
200. abssubge0d
201. abssuble0d
202. absdifltd
203. absdifled
204. icodiamlt
205. abscld
206. sqrtcld
207. sqrtrege0d
208. sqsqrtd
209. msqsqrtd
210. sqr00d
211. absvalsqd
212. absvalsq2d
213. absge0d
214. absval2d
215. abs00d
216. absne0d
217. absrpcld
218. absnegd
219. abscjd
220. releabsd
221. absexpd
222. abssubd
223. absmuld
224. absdivd
225. abstrid
226. abs2difd
227. abs2dif2d
228. abs2difabsd
229. abs3difd
230. abs3lemd
231. reusq0
232. bhmafibid1cn
233. bhmafibid2cn
234. bhmafibid1
235. bhmafibid2