bj-pinftyccb

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

		Ref	Expression
	Assertion	bj-pinftyccb	$⊢ +\infty \in \overline{ℂ}$

Step	Hyp	Ref	Expression
1		df-bj-pinfty	$⊢ +\infty = inftyexpi (0)$
2		bj-ccinftyssccbar	$⊢ ℂ_{\infty} \subseteq \overline{ℂ}$
3		0re	$⊢ 0 \in ℝ$
4		pipos	$⊢ 0 < π$
5		pire	$⊢ π \in ℝ$
6	3 5	ltnegi	$⊢ 0 < π \leftrightarrow - π < - 0$
7	4 6	mpbi	$⊢ - π < - 0$
8		neg0	$⊢ - 0 = 0$
9	7 8	breqtri	$⊢ - π < 0$
10	3 5 4	ltleii	$⊢ 0 \leq π$
11	5	renegcli	$⊢ - π \in ℝ$
12	11	rexri	$⊢ - π \in ℝ^{*}$
13		elioc2	$⊢ (- π \in ℝ^{*} \land π \in ℝ) \to (0 \in (- π, π] \leftrightarrow (0 \in ℝ \land - π < 0 \land 0 \leq π))$
14	12 5 13	mp2an	$⊢ 0 \in (- π, π] \leftrightarrow (0 \in ℝ \land - π < 0 \land 0 \leq π)$
15	3 9 10 14	mpbir3an	$⊢ 0 \in (- π, π]$
16		bj-elccinfty	$⊢ 0 \in (- π, π] \to inftyexpi (0) \in ℂ_{\infty}$
17	15 16	ax-mp	$⊢ inftyexpi (0) \in ℂ_{\infty}$
18	2 17	sselii	$⊢ inftyexpi (0) \in \overline{ℂ}$
19	1 18	eqeltri	$⊢ +\infty \in \overline{ℂ}$

Metamath Proof Explorer