Metamath Proof Explorer

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 ⊢ +∞ = inftyexpi ⁡ 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 ∈ − π π → inftyexpi ⁡ 0 ∈ ℂ ∞
17 15 16 ax-mp ⊢ inftyexpi ⁡ 0 ∈ ℂ ∞
18 2 17 sselii ⊢ inftyexpi ⁡ 0 ∈ ℂ ‾
19 1 18 eqeltri ⊢ +∞ ∈ ℂ ‾