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	|- -. ( inftyexpi ` A ) e. CC

Proof

Step	Hyp	Ref	Expression
1		opeq1	|- ( x = A -> <. x , CC >. = <. A , CC >. )
2		df-bj-inftyexpi	|- inftyexpi = ( x e. ( -u _pi (,] _pi ) |-> <. x , CC >. )
3		opex	|- <. A , CC >. e. _V
4	1 2 3	fvmpt	|- ( A e. ( -u _pi (,] _pi ) -> ( inftyexpi ` A ) = <. A , CC >. )
5		opex	|- <. x , CC >. e. _V
6	5 2	dmmpti	|- dom inftyexpi = ( -u _pi (,] _pi )
7	4 6	eleq2s	|- ( A e. dom inftyexpi -> ( inftyexpi ` A ) = <. A , CC >. )
8		cnex	|- CC e. _V
9	8	prid2	|- CC e. { A , CC }
10		eqid	|- { A , CC } = { A , CC }
11	10	olci	|- ( { A , CC } = { A } \/ { A , CC } = { A , CC } )
12		elopg	|- ( ( A e. _V /\ CC e. _V ) -> ( { A , CC } e. <. A , CC >. <-> ( { A , CC } = { A } \/ { A , CC } = { A , CC } ) ) )
13	8 12	mpan2	|- ( A e. _V -> ( { A , CC } e. <. A , CC >. <-> ( { A , CC } = { A } \/ { A , CC } = { A , CC } ) ) )
14	11 13	mpbiri	|- ( A e. _V -> { A , CC } e. <. A , CC >. )
15		en3lp	|- -. ( CC e. { A , CC } /\ { A , CC } e. <. A , CC >. /\ <. A , CC >. e. CC )
16	15	bj-imn3ani	|- ( ( CC e. { A , CC } /\ { A , CC } e. <. A , CC >. ) -> -. <. A , CC >. e. CC )
17	9 14 16	sylancr	|- ( A e. _V -> -. <. A , CC >. e. CC )
18		opprc1	|- ( -. A e. _V -> <. A , CC >. = (/) )
19		0ncn	|- -. (/) e. CC
20		eleq1	|- ( <. A , CC >. = (/) -> ( <. A , CC >. e. CC <-> (/) e. CC ) )
21	19 20	mtbiri	|- ( <. A , CC >. = (/) -> -. <. A , CC >. e. CC )
22	18 21	syl	|- ( -. A e. _V -> -. <. A , CC >. e. CC )
23	17 22	pm2.61i	|- -. <. A , CC >. e. CC
24		eqcom	|- ( ( inftyexpi ` A ) = <. A , CC >. <-> <. A , CC >. = ( inftyexpi ` A ) )
25	24	biimpi	|- ( ( inftyexpi ` A ) = <. A , CC >. -> <. A , CC >. = ( inftyexpi ` A ) )
26	25	eleq1d	|- ( ( inftyexpi ` A ) = <. A , CC >. -> ( <. A , CC >. e. CC <-> ( inftyexpi ` A ) e. CC ) )
27	23 26	mtbii	|- ( ( inftyexpi ` A ) = <. A , CC >. -> -. ( inftyexpi ` A ) e. CC )
28	7 27	syl	|- ( A e. dom inftyexpi -> -. ( inftyexpi ` A ) e. CC )
29		ndmfv	|- ( -. A e. dom inftyexpi -> ( inftyexpi ` A ) = (/) )
30	29	eleq1d	|- ( -. A e. dom inftyexpi -> ( ( inftyexpi ` A ) e. CC <-> (/) e. CC ) )
31	19 30	mtbiri	|- ( -. A e. dom inftyexpi -> -. ( inftyexpi ` A ) e. CC )
32	28 31	pm2.61i	|- -. ( inftyexpi ` A ) e. CC