![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > df-xrs | Structured version Visualization version Unicode version |
Description: The extended real number
structure. Unlike df-cnfld 18971, the extended
real numbers do not have good algebraic properties, so this is not
actually a group or anything higher, even though it has just as many
operations as df-cnfld 18971. The main interest in this structure is in
its ordering, which is complete and compact. The metric described here
is an extension of the absolute value metric, but it is not itself a
metric because ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
df-xrs |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cxrs 15398 |
. 2
![]() ![]() ![]() | |
2 | cnx 15118 |
. . . . . 6
![]() ![]() | |
3 | cbs 15121 |
. . . . . 6
![]() ![]() | |
4 | 2, 3 | cfv 5582 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() |
5 | cxr 9674 |
. . . . 5
![]() ![]() | |
6 | 4, 5 | cop 3974 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | cplusg 15190 |
. . . . . 6
![]() ![]() | |
8 | 2, 7 | cfv 5582 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() |
9 | cxad 11407 |
. . . . 5
![]() ![]() ![]() | |
10 | 8, 9 | cop 3974 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
11 | cmulr 15191 |
. . . . . 6
![]() ![]() | |
12 | 2, 11 | cfv 5582 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() |
13 | cxmu 11408 |
. . . . 5
![]() ![]() ![]() | |
14 | 12, 13 | cop 3974 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
15 | 6, 10, 14 | ctp 3972 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
16 | cts 15196 |
. . . . . 6
![]() | |
17 | 2, 16 | cfv 5582 |
. . . . 5
![]() ![]() ![]() ![]() ![]() |
18 | cle 9676 |
. . . . . 6
![]() ![]() | |
19 | cordt 15397 |
. . . . . 6
![]() | |
20 | 18, 19 | cfv 5582 |
. . . . 5
![]() ![]() ![]() ![]() ![]() |
21 | 17, 20 | cop 3974 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
22 | cple 15197 |
. . . . . 6
![]() ![]() | |
23 | 2, 22 | cfv 5582 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() |
24 | 23, 18 | cop 3974 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
25 | cds 15199 |
. . . . . 6
![]() ![]() | |
26 | 2, 25 | cfv 5582 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() |
27 | vx |
. . . . . 6
![]() ![]() | |
28 | vy |
. . . . . 6
![]() ![]() | |
29 | 27 | cv 1443 |
. . . . . . . 8
![]() ![]() |
30 | 28 | cv 1443 |
. . . . . . . 8
![]() ![]() |
31 | 29, 30, 18 | wbr 4402 |
. . . . . . 7
![]() ![]() ![]() ![]() |
32 | 29 | cxne 11406 |
. . . . . . . 8
![]() ![]() ![]() ![]() |
33 | 30, 32, 9 | co 6290 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
34 | 30 | cxne 11406 |
. . . . . . . 8
![]() ![]() ![]() ![]() |
35 | 29, 34, 9 | co 6290 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
36 | 31, 33, 35 | cif 3881 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
37 | 27, 28, 5, 5, 36 | cmpt2 6292 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
38 | 26, 37 | cop 3974 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
39 | 21, 24, 38 | ctp 3972 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
40 | 15, 39 | cun 3402 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
41 | 1, 40 | wceq 1444 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
This definition is referenced by: xrsstr 18982 xrsex 18983 xrsbas 18984 xrsadd 18985 xrsmul 18986 xrstset 18987 xrsle 18988 xrsds 19011 |
Copyright terms: Public domain | W3C validator |