Metamath Proof Explorer

Theorem bj-elccinfty

Description: A lemma for infinite extended complex numbers. (Contributed by BJ, 27-Jun-2019)

Ref Expression
Assertion bj-elccinfty ⊢ A ∈ − π π → inftyexpi ⁡ A ∈ ℂ ∞

Proof

Step Hyp Ref Expression
1 df-bj-inftyexpi ⊢ inftyexpi = x ∈ − π π ⟼ x ℂ
2 1 funmpt2 ⊢ Fun ⁡ inftyexpi
3 2 jctl ⊢ A ∈ dom ⁡ inftyexpi → Fun ⁡ inftyexpi ∧ A ∈ dom ⁡ inftyexpi
4 opex ⊢ x ℂ ∈ V
5 4 1 dmmpti ⊢ dom ⁡ inftyexpi = − π π
6 5 eqcomi ⊢ − π π = dom ⁡ inftyexpi
7 3 6 eleq2s ⊢ A ∈ − π π → Fun ⁡ inftyexpi ∧ A ∈ dom ⁡ inftyexpi
8 fvelrn ⊢ Fun ⁡ inftyexpi ∧ A ∈ dom ⁡ inftyexpi → inftyexpi ⁡ A ∈ ran ⁡ inftyexpi
9 df-bj-ccinfty ⊢ ℂ ∞ = ran ⁡ inftyexpi
10 9 eqcomi ⊢ ran ⁡ inftyexpi = ℂ ∞
11 10 eleq2i ⊢ inftyexpi ⁡ A ∈ ran ⁡ inftyexpi ↔ inftyexpi ⁡ A ∈ ℂ ∞
12 11 biimpi ⊢ inftyexpi ⁡ A ∈ ran ⁡ inftyexpi → inftyexpi ⁡ A ∈ ℂ ∞
13 7 8 12 3syl ⊢ A ∈ − π π → inftyexpi ⁡ A ∈ ℂ ∞