Description: The class minfty is an extended complex number. (Contributed by BJ, 27-Jun-2019)
Ref | Expression | ||
---|---|---|---|
Assertion | bj-minftyccb | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bj-ccinftyssccbar | |
|
2 | df-bj-inftyexpi | |
|
3 | 2 | funmpt2 | |
4 | pire | |
|
5 | 4 | renegcli | |
6 | 5 | rexri | |
7 | 4 | rexri | |
8 | pipos | |
|
9 | 0re | |
|
10 | 9 4 | ltnegi | |
11 | 8 10 | mpbi | |
12 | neg0 | |
|
13 | 11 12 | breqtri | |
14 | 5 9 4 | lttri | |
15 | 13 8 14 | mp2an | |
16 | ubioc1 | |
|
17 | 6 7 15 16 | mp3an | |
18 | opex | |
|
19 | 18 2 | dmmpti | |
20 | 17 19 | eleqtrri | |
21 | fvelrn | |
|
22 | 3 20 21 | mp2an | |
23 | df-bj-minfty | |
|
24 | df-bj-ccinfty | |
|
25 | 22 23 24 | 3eltr4i | |
26 | 1 25 | sselii | |