Theorem bj-pinftyccb

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

	Ref	Expression
Assertion	bj-pinftyccb	⊢ +∞ ∈ ℂ̅

Proof

Step	Hyp	Ref	Expression
1		df-bj-pinfty	⊢ +∞ = ( +∞ei ‘ 0 )
2		bj-ccinftyssccbar	⊢ ℂ∞ ⊆ ℂ̅
3		0re	⊢ 0 ∈ ℝ
4		pipos	⊢ 0 < π
5		pire	⊢ π ∈ ℝ
6	3 5	ltnegi	⊢ ( 0 < π ↔ - π < - 0 )
7	4 6	mpbi	⊢ - π < - 0
8		neg0	⊢ - 0 = 0
9	7 8	breqtri	⊢ - π < 0
10	3 5 4	ltleii	⊢ 0 ≤ π
11	5	renegcli	⊢ - π ∈ ℝ
12	11	rexri	⊢ - π ∈ ℝ*
13		elioc2	⊢ ( ( - π ∈ ℝ* ∧ π ∈ ℝ ) → ( 0 ∈ ( - π (,] π ) ↔ ( 0 ∈ ℝ ∧ - π < 0 ∧ 0 ≤ π ) ) )
14	12 5 13	mp2an	⊢ ( 0 ∈ ( - π (,] π ) ↔ ( 0 ∈ ℝ ∧ - π < 0 ∧ 0 ≤ π ) )
15	3 9 10 14	mpbir3an	⊢ 0 ∈ ( - π (,] π )
16		bj-elccinfty	⊢ ( 0 ∈ ( - π (,] π ) → ( +∞ei ‘ 0 ) ∈ ℂ∞ )
17	15 16	ax-mp	⊢ ( +∞ei ‘ 0 ) ∈ ℂ∞
18	2 17	sselii	⊢ ( +∞ei ‘ 0 ) ∈ ℂ̅
19	1 18	eqeltri	⊢ +∞ ∈ ℂ̅