Theorem bj-inftyexpitaudisj

Description: An element of the circle at infinity is not a complex number. (Contributed by BJ, 4-Feb-2023)

	Ref	Expression
Assertion	bj-inftyexpitaudisj	$$⊢\neg {\mathrm{+\infty e}}^{i\tau }\left(A\right)\in ℂ$$

Proof

Step	Hyp	Ref	Expression
1		2fveq3	$$⊢x=A\to {\{}_R\left(1^{st}\left(x\right)\right)={\{}_R\left(1^{st}\left(A\right)\right)$$
2	1	opeq1d	$$⊢x=A\to ⟨{\{}_R\left(1^{st}\left(x\right)\right),\left\{𝑹\right\}⟩=⟨{\{}_R\left(1^{st}\left(A\right)\right),\left\{𝑹\right\}⟩$$
3		df-bj-inftyexpitau	$$⊢{\mathrm{+\infty e}}^{i\tau }=\left(x\in ℝ⟼⟨{\{}_R\left(1^{st}\left(x\right)\right),\left\{𝑹\right\}⟩\right)$$
4		opex	$$⊢⟨{\{}_R\left(1^{st}\left(A\right)\right),\left\{𝑹\right\}⟩\in \mathrm{V}$$
5	2 3 4	fvmpt	$$⊢A\in ℝ\to {\mathrm{+\infty e}}^{i\tau }\left(A\right)=⟨{\{}_R\left(1^{st}\left(A\right)\right),\left\{𝑹\right\}⟩$$
6		opex	$$⊢⟨{\{}_R\left(1^{st}\left(y\right)\right),\left\{𝑹\right\}⟩\in \mathrm{V}$$
7		df-bj-inftyexpitau	$$⊢{\mathrm{+\infty e}}^{i\tau }=\left(y\in ℝ⟼⟨{\{}_R\left(1^{st}\left(y\right)\right),\left\{𝑹\right\}⟩\right)$$
8	6 7	dmmpti	$$⊢\mathrm{dom}{\mathrm{+\infty e}}^{i\tau }=ℝ$$
9	5 8	eleq2s	$$⊢A\in \mathrm{dom}{\mathrm{+\infty e}}^{i\tau }\to {\mathrm{+\infty e}}^{i\tau }\left(A\right)=⟨{\{}_R\left(1^{st}\left(A\right)\right),\left\{𝑹\right\}⟩$$
10		nrex1	$$⊢𝑹\in \mathrm{V}$$
11		bj-nsnid	$$⊢𝑹\in \mathrm{V}\to \neg \left\{𝑹\right\}\in 𝑹$$
12	10 11	ax-mp	$$⊢\neg \left\{𝑹\right\}\in 𝑹$$
13	12	intnan	$$⊢\neg \left({\{}_R\left(1^{st}\left(A\right)\right)\in 𝑹\wedge \left\{𝑹\right\}\in 𝑹\right)$$
14		opelxp	$$⊢⟨{\{}_R\left(1^{st}\left(A\right)\right),\left\{𝑹\right\}⟩\in \left(𝑹\times 𝑹\right)\leftrightarrow \left({\{}_R\left(1^{st}\left(A\right)\right)\in 𝑹\wedge \left\{𝑹\right\}\in 𝑹\right)$$
15	13 14	mtbir	$$⊢\neg ⟨{\{}_R\left(1^{st}\left(A\right)\right),\left\{𝑹\right\}⟩\in \left(𝑹\times 𝑹\right)$$
16		df-c	$$⊢ℂ=𝑹\times 𝑹$$
17	16	eleq2i	$$⊢⟨{\{}_R\left(1^{st}\left(A\right)\right),\left\{𝑹\right\}⟩\in ℂ\leftrightarrow ⟨{\{}_R\left(1^{st}\left(A\right)\right),\left\{𝑹\right\}⟩\in \left(𝑹\times 𝑹\right)$$
18	15 17	mtbir	$$⊢\neg ⟨{\{}_R\left(1^{st}\left(A\right)\right),\left\{𝑹\right\}⟩\in ℂ$$
19		eqcom	$$⊢{\mathrm{+\infty e}}^{i\tau }\left(A\right)=⟨{\{}_R\left(1^{st}\left(A\right)\right),\left\{𝑹\right\}⟩\leftrightarrow ⟨{\{}_R\left(1^{st}\left(A\right)\right),\left\{𝑹\right\}⟩={\mathrm{+\infty e}}^{i\tau }\left(A\right)$$
20	19	biimpi	$$⊢{\mathrm{+\infty e}}^{i\tau }\left(A\right)=⟨{\{}_R\left(1^{st}\left(A\right)\right),\left\{𝑹\right\}⟩\to ⟨{\{}_R\left(1^{st}\left(A\right)\right),\left\{𝑹\right\}⟩={\mathrm{+\infty e}}^{i\tau }\left(A\right)$$
21	20	eleq1d	$$⊢{\mathrm{+\infty e}}^{i\tau }\left(A\right)=⟨{\{}_R\left(1^{st}\left(A\right)\right),\left\{𝑹\right\}⟩\to \left(⟨{\{}_R\left(1^{st}\left(A\right)\right),\left\{𝑹\right\}⟩\in ℂ\leftrightarrow {\mathrm{+\infty e}}^{i\tau }\left(A\right)\in ℂ\right)$$
22	18 21	mtbii	$$⊢{\mathrm{+\infty e}}^{i\tau }\left(A\right)=⟨{\{}_R\left(1^{st}\left(A\right)\right),\left\{𝑹\right\}⟩\to \neg {\mathrm{+\infty e}}^{i\tau }\left(A\right)\in ℂ$$
23	9 22	syl	$$⊢A\in \mathrm{dom}{\mathrm{+\infty e}}^{i\tau }\to \neg {\mathrm{+\infty e}}^{i\tau }\left(A\right)\in ℂ$$
24		0ncn	$$⊢\neg \varnothing \in ℂ$$
25		ndmfv	$$⊢\neg A\in \mathrm{dom}{\mathrm{+\infty e}}^{i\tau }\to {\mathrm{+\infty e}}^{i\tau }\left(A\right)=\varnothing$$
26	25	eleq1d	$$⊢\neg A\in \mathrm{dom}{\mathrm{+\infty e}}^{i\tau }\to \left({\mathrm{+\infty e}}^{i\tau }\left(A\right)\in ℂ\leftrightarrow \varnothing \in ℂ\right)$$
27	24 26	mtbiri	$$⊢\neg A\in \mathrm{dom}{\mathrm{+\infty e}}^{i\tau }\to \neg {\mathrm{+\infty e}}^{i\tau }\left(A\right)\in ℂ$$
28	23 27	pm2.61i	$$⊢\neg {\mathrm{+\infty e}}^{i\tau }\left(A\right)\in ℂ$$