Theorem bj-pinftyccb

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

	Ref	Expression
Assertion	bj-pinftyccb	|- pinfty e. CCbar

Proof

Step	Hyp	Ref	Expression
1		df-bj-pinfty	|- pinfty = ( inftyexpi ` 0 )
2		bj-ccinftyssccbar	|- CCinfty C_ CCbar
3		0re	|- 0 e. RR
4		pipos	|- 0 < _pi
5		pire	|- _pi e. RR
6	3 5	ltnegi	|- ( 0 < _pi <-> -u _pi < -u 0 )
7	4 6	mpbi	|- -u _pi < -u 0
8		neg0	|- -u 0 = 0
9	7 8	breqtri	|- -u _pi < 0
10	3 5 4	ltleii	|- 0 <_ _pi
11	5	renegcli	|- -u _pi e. RR
12	11	rexri	|- -u _pi e. RR*
13		elioc2	|- ( ( -u _pi e. RR* /\ _pi e. RR ) -> ( 0 e. ( -u _pi (,] _pi ) <-> ( 0 e. RR /\ -u _pi < 0 /\ 0 <_ _pi ) ) )
14	12 5 13	mp2an	|- ( 0 e. ( -u _pi (,] _pi ) <-> ( 0 e. RR /\ -u _pi < 0 /\ 0 <_ _pi ) )
15	3 9 10 14	mpbir3an	|- 0 e. ( -u _pi (,] _pi )
16		bj-elccinfty	|- ( 0 e. ( -u _pi (,] _pi ) -> ( inftyexpi ` 0 ) e. CCinfty )
17	15 16	ax-mp	|- ( inftyexpi ` 0 ) e. CCinfty
18	2 17	sselii	|- ( inftyexpi ` 0 ) e. CCbar
19	1 18	eqeltri	|- pinfty e. CCbar