Metamath Proof Explorer

Theorem bj-minftyccb

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

Ref Expression
Assertion bj-minftyccb ⊢ -∞ ∈ ℂ ‾

Proof

Step Hyp Ref Expression
1 bj-ccinftyssccbar ⊢ ℂ ∞ ⊆ ℂ ‾
2 df-bj-inftyexpi ⊢ inftyexpi = x ∈ − π π ⟼ x ℂ
3 2 funmpt2 ⊢ Fun ⁡ inftyexpi
4 pire ⊢ π ∈ ℝ
5 4 renegcli ⊢ − π ∈ ℝ
6 5 rexri ⊢ − π ∈ ℝ *
7 4 rexri ⊢ π ∈ ℝ *
8 pipos ⊢ 0 < π
9 0re ⊢ 0 ∈ ℝ
10 9 4 ltnegi ⊢ 0 < π ↔ − π < − 0
11 8 10 mpbi ⊢ − π < − 0
12 neg0 ⊢ − 0 = 0
13 11 12 breqtri ⊢ − π < 0
14 5 9 4 lttri ⊢ − π < 0 ∧ 0 < π → − π < π
15 13 8 14 mp2an ⊢ − π < π
16 ubioc1 ⊢ − π ∈ ℝ * ∧ π ∈ ℝ * ∧ − π < π → π ∈ − π π
17 6 7 15 16 mp3an ⊢ π ∈ − π π
18 opex ⊢ x ℂ ∈ V
19 18 2 dmmpti ⊢ dom ⁡ inftyexpi = − π π
20 17 19 eleqtrri ⊢ π ∈ dom ⁡ inftyexpi
21 fvelrn ⊢ Fun ⁡ inftyexpi ∧ π ∈ dom ⁡ inftyexpi → inftyexpi ⁡ π ∈ ran ⁡ inftyexpi
22 3 20 21 mp2an ⊢ inftyexpi ⁡ π ∈ ran ⁡ inftyexpi
23 df-bj-minfty ⊢ -∞ = inftyexpi ⁡ π
24 df-bj-ccinfty ⊢ ℂ ∞ = ran ⁡ inftyexpi
25 22 23 24 3eltr4i ⊢ -∞ ∈ ℂ ∞
26 1 25 sselii ⊢ -∞ ∈ ℂ ‾