| Step |
Hyp |
Ref |
Expression |
| 1 |
|
bj-ccinftyssccbar |
|- CCinfty C_ CCbar |
| 2 |
|
df-bj-inftyexpi |
|- inftyexpi = ( x e. ( -u _pi (,] _pi ) |-> <. x , CC >. ) |
| 3 |
2
|
funmpt2 |
|- Fun inftyexpi |
| 4 |
|
pire |
|- _pi e. RR |
| 5 |
4
|
renegcli |
|- -u _pi e. RR |
| 6 |
5
|
rexri |
|- -u _pi e. RR* |
| 7 |
4
|
rexri |
|- _pi e. RR* |
| 8 |
|
pipos |
|- 0 < _pi |
| 9 |
|
0re |
|- 0 e. RR |
| 10 |
9 4
|
ltnegi |
|- ( 0 < _pi <-> -u _pi < -u 0 ) |
| 11 |
8 10
|
mpbi |
|- -u _pi < -u 0 |
| 12 |
|
neg0 |
|- -u 0 = 0 |
| 13 |
11 12
|
breqtri |
|- -u _pi < 0 |
| 14 |
5 9 4
|
lttri |
|- ( ( -u _pi < 0 /\ 0 < _pi ) -> -u _pi < _pi ) |
| 15 |
13 8 14
|
mp2an |
|- -u _pi < _pi |
| 16 |
|
ubioc1 |
|- ( ( -u _pi e. RR* /\ _pi e. RR* /\ -u _pi < _pi ) -> _pi e. ( -u _pi (,] _pi ) ) |
| 17 |
6 7 15 16
|
mp3an |
|- _pi e. ( -u _pi (,] _pi ) |
| 18 |
|
opex |
|- <. x , CC >. e. _V |
| 19 |
18 2
|
dmmpti |
|- dom inftyexpi = ( -u _pi (,] _pi ) |
| 20 |
17 19
|
eleqtrri |
|- _pi e. dom inftyexpi |
| 21 |
|
fvelrn |
|- ( ( Fun inftyexpi /\ _pi e. dom inftyexpi ) -> ( inftyexpi ` _pi ) e. ran inftyexpi ) |
| 22 |
3 20 21
|
mp2an |
|- ( inftyexpi ` _pi ) e. ran inftyexpi |
| 23 |
|
df-bj-minfty |
|- minfty = ( inftyexpi ` _pi ) |
| 24 |
|
df-bj-ccinfty |
|- CCinfty = ran inftyexpi |
| 25 |
22 23 24
|
3eltr4i |
|- minfty e. CCinfty |
| 26 |
1 25
|
sselii |
|- minfty e. CCbar |