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	$$⊢\neg inftyexpi\left(A\right)\in ℂ$$

Proof

Step	Hyp	Ref	Expression
1		opeq1	$$⊢x=A\to ⟨x,ℂ⟩=⟨A,ℂ⟩$$
2		df-bj-inftyexpi	$$⊢inftyexpi=\left(x\in \left(-\mathrm{\pi },\mathrm{\pi }\right]⟼⟨x,ℂ⟩\right)$$
3		opex	$$⊢⟨A,ℂ⟩\in \mathrm{V}$$
4	1 2 3	fvmpt	$$⊢A\in \left(-\mathrm{\pi },\mathrm{\pi }\right]\to inftyexpi\left(A\right)=⟨A,ℂ⟩$$
5		opex	$$⊢⟨x,ℂ⟩\in \mathrm{V}$$
6	5 2	dmmpti	$$⊢\mathrm{dom}inftyexpi=\left(-\mathrm{\pi },\mathrm{\pi }\right]$$
7	4 6	eleq2s	$$⊢A\in \mathrm{dom}inftyexpi\to inftyexpi\left(A\right)=⟨A,ℂ⟩$$
8		cnex	$$⊢ℂ\in \mathrm{V}$$
9	8	prid2	$$⊢ℂ\in \left\{A,ℂ\right\}$$
10		eqid	$$⊢\left\{A,ℂ\right\}=\left\{A,ℂ\right\}$$
11	10	olci	$$⊢\left(\left\{A,ℂ\right\}=\left\{A\right\}\vee \left\{A,ℂ\right\}=\left\{A,ℂ\right\}\right)$$
12		elopg	$$⊢\left(A\in \mathrm{V}\wedge ℂ\in \mathrm{V}\right)\to \left(\left\{A,ℂ\right\}\in ⟨A,ℂ⟩\leftrightarrow \left(\left\{A,ℂ\right\}=\left\{A\right\}\vee \left\{A,ℂ\right\}=\left\{A,ℂ\right\}\right)\right)$$
13	8 12	mpan2	$$⊢A\in \mathrm{V}\to \left(\left\{A,ℂ\right\}\in ⟨A,ℂ⟩\leftrightarrow \left(\left\{A,ℂ\right\}=\left\{A\right\}\vee \left\{A,ℂ\right\}=\left\{A,ℂ\right\}\right)\right)$$
14	11 13	mpbiri	$$⊢A\in \mathrm{V}\to \left\{A,ℂ\right\}\in ⟨A,ℂ⟩$$
15		en3lp	$$⊢\neg \left(ℂ\in \left\{A,ℂ\right\}\wedge \left\{A,ℂ\right\}\in ⟨A,ℂ⟩\wedge ⟨A,ℂ⟩\in ℂ\right)$$
16	15	bj-imn3ani	$$⊢\left(ℂ\in \left\{A,ℂ\right\}\wedge \left\{A,ℂ\right\}\in ⟨A,ℂ⟩\right)\to \neg ⟨A,ℂ⟩\in ℂ$$
17	9 14 16	sylancr	$$⊢A\in \mathrm{V}\to \neg ⟨A,ℂ⟩\in ℂ$$
18		opprc1	$$⊢\neg A\in \mathrm{V}\to ⟨A,ℂ⟩=\varnothing$$
19		0ncn	$$⊢\neg \varnothing \in ℂ$$
20		eleq1	$$⊢⟨A,ℂ⟩=\varnothing \to \left(⟨A,ℂ⟩\in ℂ\leftrightarrow \varnothing \in ℂ\right)$$
21	19 20	mtbiri	$$⊢⟨A,ℂ⟩=\varnothing \to \neg ⟨A,ℂ⟩\in ℂ$$
22	18 21	syl	$$⊢\neg A\in \mathrm{V}\to \neg ⟨A,ℂ⟩\in ℂ$$
23	17 22	pm2.61i	$$⊢\neg ⟨A,ℂ⟩\in ℂ$$
24		eqcom	$$⊢inftyexpi\left(A\right)=⟨A,ℂ⟩\leftrightarrow ⟨A,ℂ⟩=inftyexpi\left(A\right)$$
25	24	biimpi	$$⊢inftyexpi\left(A\right)=⟨A,ℂ⟩\to ⟨A,ℂ⟩=inftyexpi\left(A\right)$$
26	25	eleq1d	$$⊢inftyexpi\left(A\right)=⟨A,ℂ⟩\to \left(⟨A,ℂ⟩\in ℂ\leftrightarrow inftyexpi\left(A\right)\in ℂ\right)$$
27	23 26	mtbii	$$⊢inftyexpi\left(A\right)=⟨A,ℂ⟩\to \neg inftyexpi\left(A\right)\in ℂ$$
28	7 27	syl	$$⊢A\in \mathrm{dom}inftyexpi\to \neg inftyexpi\left(A\right)\in ℂ$$
29		ndmfv	$$⊢\neg A\in \mathrm{dom}inftyexpi\to inftyexpi\left(A\right)=\varnothing$$
30	29	eleq1d	$$⊢\neg A\in \mathrm{dom}inftyexpi\to \left(inftyexpi\left(A\right)\in ℂ\leftrightarrow \varnothing \in ℂ\right)$$
31	19 30	mtbiri	$$⊢\neg A\in \mathrm{dom}inftyexpi\to \neg inftyexpi\left(A\right)\in ℂ$$
32	28 31	pm2.61i	$$⊢\neg inftyexpi\left(A\right)\in ℂ$$