Theorem bj-inftyexpidisj

Description: An element of the circle at infinity is not a complex number. (Contributed by BJ, 22-Jun-2019) This utility theorem is irrelevant and should generally not be used. (New usage is discouraged.)

	Ref	Expression
Assertion	bj-inftyexpidisj	⊢ ¬ ( +∞ei ‘ 𝐴 ) ∈ ℂ

Proof

Step	Hyp	Ref	Expression
1		opeq1	⊢ ( 𝑥 = 𝐴 → ⟨ 𝑥 , ℂ ⟩ = ⟨ 𝐴 , ℂ ⟩ )
2		df-bj-inftyexpi	⊢ +∞ei = ( 𝑥 ∈ ( - π (,] π ) ↦ ⟨ 𝑥 , ℂ ⟩ )
3		opex	⊢ ⟨ 𝐴 , ℂ ⟩ ∈ V
4	1 2 3	fvmpt	⊢ ( 𝐴 ∈ ( - π (,] π ) → ( +∞ei ‘ 𝐴 ) = ⟨ 𝐴 , ℂ ⟩ )
5		opex	⊢ ⟨ 𝑥 , ℂ ⟩ ∈ V
6	5 2	dmmpti	⊢ dom +∞ei = ( - π (,] π )
7	4 6	eleq2s	⊢ ( 𝐴 ∈ dom +∞ei → ( +∞ei ‘ 𝐴 ) = ⟨ 𝐴 , ℂ ⟩ )
8		cnex	⊢ ℂ ∈ V
9	8	prid2	⊢ ℂ ∈ { 𝐴 , ℂ }
10		eqid	⊢ { 𝐴 , ℂ } = { 𝐴 , ℂ }
11	10	olci	⊢ ( { 𝐴 , ℂ } = { 𝐴 } ∨ { 𝐴 , ℂ } = { 𝐴 , ℂ } )
12		elopg	⊢ ( ( 𝐴 ∈ V ∧ ℂ ∈ V ) → ( { 𝐴 , ℂ } ∈ ⟨ 𝐴 , ℂ ⟩ ↔ ( { 𝐴 , ℂ } = { 𝐴 } ∨ { 𝐴 , ℂ } = { 𝐴 , ℂ } ) ) )
13	8 12	mpan2	⊢ ( 𝐴 ∈ V → ( { 𝐴 , ℂ } ∈ ⟨ 𝐴 , ℂ ⟩ ↔ ( { 𝐴 , ℂ } = { 𝐴 } ∨ { 𝐴 , ℂ } = { 𝐴 , ℂ } ) ) )
14	11 13	mpbiri	⊢ ( 𝐴 ∈ V → { 𝐴 , ℂ } ∈ ⟨ 𝐴 , ℂ ⟩ )
15		en3lp	⊢ ¬ ( ℂ ∈ { 𝐴 , ℂ } ∧ { 𝐴 , ℂ } ∈ ⟨ 𝐴 , ℂ ⟩ ∧ ⟨ 𝐴 , ℂ ⟩ ∈ ℂ )
16	15	bj-imn3ani	⊢ ( ( ℂ ∈ { 𝐴 , ℂ } ∧ { 𝐴 , ℂ } ∈ ⟨ 𝐴 , ℂ ⟩ ) → ¬ ⟨ 𝐴 , ℂ ⟩ ∈ ℂ )
17	9 14 16	sylancr	⊢ ( 𝐴 ∈ V → ¬ ⟨ 𝐴 , ℂ ⟩ ∈ ℂ )
18		opprc1	⊢ ( ¬ 𝐴 ∈ V → ⟨ 𝐴 , ℂ ⟩ = ∅ )
19		0ncn	⊢ ¬ ∅ ∈ ℂ
20		eleq1	⊢ ( ⟨ 𝐴 , ℂ ⟩ = ∅ → ( ⟨ 𝐴 , ℂ ⟩ ∈ ℂ ↔ ∅ ∈ ℂ ) )
21	19 20	mtbiri	⊢ ( ⟨ 𝐴 , ℂ ⟩ = ∅ → ¬ ⟨ 𝐴 , ℂ ⟩ ∈ ℂ )
22	18 21	syl	⊢ ( ¬ 𝐴 ∈ V → ¬ ⟨ 𝐴 , ℂ ⟩ ∈ ℂ )
23	17 22	pm2.61i	⊢ ¬ ⟨ 𝐴 , ℂ ⟩ ∈ ℂ
24		eqcom	⊢ ( ( +∞ei ‘ 𝐴 ) = ⟨ 𝐴 , ℂ ⟩ ↔ ⟨ 𝐴 , ℂ ⟩ = ( +∞ei ‘ 𝐴 ) )
25	24	biimpi	⊢ ( ( +∞ei ‘ 𝐴 ) = ⟨ 𝐴 , ℂ ⟩ → ⟨ 𝐴 , ℂ ⟩ = ( +∞ei ‘ 𝐴 ) )
26	25	eleq1d	⊢ ( ( +∞ei ‘ 𝐴 ) = ⟨ 𝐴 , ℂ ⟩ → ( ⟨ 𝐴 , ℂ ⟩ ∈ ℂ ↔ ( +∞ei ‘ 𝐴 ) ∈ ℂ ) )
27	23 26	mtbii	⊢ ( ( +∞ei ‘ 𝐴 ) = ⟨ 𝐴 , ℂ ⟩ → ¬ ( +∞ei ‘ 𝐴 ) ∈ ℂ )
28	7 27	syl	⊢ ( 𝐴 ∈ dom +∞ei → ¬ ( +∞ei ‘ 𝐴 ) ∈ ℂ )
29		ndmfv	⊢ ( ¬ 𝐴 ∈ dom +∞ei → ( +∞ei ‘ 𝐴 ) = ∅ )
30	29	eleq1d	⊢ ( ¬ 𝐴 ∈ dom +∞ei → ( ( +∞ei ‘ 𝐴 ) ∈ ℂ ↔ ∅ ∈ ℂ ) )
31	19 30	mtbiri	⊢ ( ¬ 𝐴 ∈ dom +∞ei → ¬ ( +∞ei ‘ 𝐴 ) ∈ ℂ )
32	28 31	pm2.61i	⊢ ¬ ( +∞ei ‘ 𝐴 ) ∈ ℂ