![]() |
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 19048, 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 19048. 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 15476 |
. 2
![]() ![]() ![]() | |
2 | cnx 15196 |
. . . . . 6
![]() ![]() | |
3 | cbs 15199 |
. . . . . 6
![]() ![]() | |
4 | 2, 3 | cfv 5589 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() |
5 | cxr 9692 |
. . . . 5
![]() ![]() | |
6 | 4, 5 | cop 3965 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | cplusg 15268 |
. . . . . 6
![]() ![]() | |
8 | 2, 7 | cfv 5589 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() |
9 | cxad 11430 |
. . . . 5
![]() ![]() ![]() | |
10 | 8, 9 | cop 3965 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
11 | cmulr 15269 |
. . . . . 6
![]() ![]() | |
12 | 2, 11 | cfv 5589 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() |
13 | cxmu 11431 |
. . . . 5
![]() ![]() ![]() | |
14 | 12, 13 | cop 3965 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
15 | 6, 10, 14 | ctp 3963 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
16 | cts 15274 |
. . . . . 6
![]() | |
17 | 2, 16 | cfv 5589 |
. . . . 5
![]() ![]() ![]() ![]() ![]() |
18 | cle 9694 |
. . . . . 6
![]() ![]() | |
19 | cordt 15475 |
. . . . . 6
![]() | |
20 | 18, 19 | cfv 5589 |
. . . . 5
![]() ![]() ![]() ![]() ![]() |
21 | 17, 20 | cop 3965 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
22 | cple 15275 |
. . . . . 6
![]() ![]() | |
23 | 2, 22 | cfv 5589 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() |
24 | 23, 18 | cop 3965 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
25 | cds 15277 |
. . . . . 6
![]() ![]() | |
26 | 2, 25 | cfv 5589 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() |
27 | vx |
. . . . . 6
![]() ![]() | |
28 | vy |
. . . . . 6
![]() ![]() | |
29 | 27 | cv 1451 |
. . . . . . . 8
![]() ![]() |
30 | 28 | cv 1451 |
. . . . . . . 8
![]() ![]() |
31 | 29, 30, 18 | wbr 4395 |
. . . . . . 7
![]() ![]() ![]() ![]() |
32 | 29 | cxne 11429 |
. . . . . . . 8
![]() ![]() ![]() ![]() |
33 | 30, 32, 9 | co 6308 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
34 | 30 | cxne 11429 |
. . . . . . . 8
![]() ![]() ![]() ![]() |
35 | 29, 34, 9 | co 6308 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
36 | 31, 33, 35 | cif 3872 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
37 | 27, 28, 5, 5, 36 | cmpt2 6310 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
38 | 26, 37 | cop 3965 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
39 | 21, 24, 38 | ctp 3963 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
40 | 15, 39 | cun 3388 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
41 | 1, 40 | wceq 1452 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
This definition is referenced by: xrsstr 19059 xrsex 19060 xrsbas 19061 xrsadd 19062 xrsmul 19063 xrstset 19064 xrsle 19065 xrsds 19088 |
Copyright terms: Public domain | W3C validator |