Metamath Proof Explorer


Theorem bj-minftyccb

Description: The class minfty is an extended complex number. (Contributed by BJ, 27-Jun-2019)

Ref Expression
Assertion bj-minftyccb -∞

Proof

Step Hyp Ref Expression
1 bj-ccinftyssccbar
2 df-bj-inftyexpi inftyexpi=xππx
3 2 funmpt2 Funinftyexpi
4 pire π
5 4 renegcli π
6 5 rexri π*
7 4 rexri π*
8 pipos 0<π
9 0re 0
10 9 4 ltnegi 0<ππ<0
11 8 10 mpbi π<0
12 neg0 0=0
13 11 12 breqtri π<0
14 5 9 4 lttri π<00<ππ<π
15 13 8 14 mp2an π<π
16 ubioc1 π*π*π<ππππ
17 6 7 15 16 mp3an πππ
18 opex xV
19 18 2 dmmpti dominftyexpi=ππ
20 17 19 eleqtrri πdominftyexpi
21 fvelrn Funinftyexpiπdominftyexpiinftyexpiπraninftyexpi
22 3 20 21 mp2an inftyexpiπraninftyexpi
23 df-bj-minfty -∞=inftyexpiπ
24 df-bj-ccinfty =raninftyexpi
25 22 23 24 3eltr4i -∞
26 1 25 sselii -∞