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 ( 𝐴 ∈ ( - π (,] π ) → ( +∞ei𝐴 ) ∈ ℂ )

Proof

Step Hyp Ref Expression
1 df-bj-inftyexpi +∞ei = ( 𝑥 ∈ ( - π (,] π ) ↦ ⟨ 𝑥 , ℂ ⟩ )
2 1 funmpt2 Fun +∞ei
3 2 jctl ( 𝐴 ∈ dom +∞ei → ( Fun +∞ei𝐴 ∈ dom +∞ei ) )
4 opex 𝑥 , ℂ ⟩ ∈ V
5 4 1 dmmpti dom +∞ei = ( - π (,] π )
6 5 eqcomi ( - π (,] π ) = dom +∞ei
7 3 6 eleq2s ( 𝐴 ∈ ( - π (,] π ) → ( Fun +∞ei𝐴 ∈ dom +∞ei ) )
8 fvelrn ( ( Fun +∞ei𝐴 ∈ dom +∞ei ) → ( +∞ei𝐴 ) ∈ ran +∞ei )
9 df-bj-ccinfty = ran +∞ei
10 9 eqcomi ran +∞ei = ℂ
11 10 eleq2i ( ( +∞ei𝐴 ) ∈ ran +∞ei ↔ ( +∞ei𝐴 ) ∈ ℂ )
12 11 biimpi ( ( +∞ei𝐴 ) ∈ ran +∞ei → ( +∞ei𝐴 ) ∈ ℂ )
13 7 8 12 3syl ( 𝐴 ∈ ( - π (,] π ) → ( +∞ei𝐴 ) ∈ ℂ )