Metamath Proof Explorer

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

Proof

Step Hyp Ref Expression
1 2fveq3 
 |-  ( x = A -> ( {R ` ( 1st ` x ) ) = ( {R ` ( 1st ` A ) ) )
2 1 opeq1d 
 |-  ( x = A -> <. ( {R ` ( 1st ` x ) ) , { R. } >. = <. ( {R ` ( 1st ` A ) ) , { R. } >. )
3 df-bj-inftyexpitau 
 |-  inftyexpitau = ( x e. RR |-> <. ( {R ` ( 1st ` x ) ) , { R. } >. )
4 opex 
 |-  <. ( {R ` ( 1st ` A ) ) , { R. } >. e. _V
5 2 3 4 fvmpt 
 |-  ( A e. RR -> ( inftyexpitau ` A ) = <. ( {R ` ( 1st ` A ) ) , { R. } >. )
6 opex 
 |-  <. ( {R ` ( 1st ` y ) ) , { R. } >. e. _V
7 df-bj-inftyexpitau 
 |-  inftyexpitau = ( y e. RR |-> <. ( {R ` ( 1st ` y ) ) , { R. } >. )
8 6 7 dmmpti 
 |-  dom inftyexpitau = RR
9 5 8 eleq2s 
 |-  ( A e. dom inftyexpitau -> ( inftyexpitau ` A ) = <. ( {R ` ( 1st ` A ) ) , { R. } >. )
10 nrex1 
 |-  R. e. _V
11 bj-nsnid 
 |-  ( R. e. _V -> -. { R. } e. R. )
12 10 11 ax-mp 
 |-  -. { R. } e. R.
13 12 intnan 
 |-  -. ( ( {R ` ( 1st ` A ) ) e. R. /\ { R. } e. R. )
14 opelxp 
 |-  ( <. ( {R ` ( 1st ` A ) ) , { R. } >. e. ( R. X. R. ) <-> ( ( {R ` ( 1st ` A ) ) e. R. /\ { R. } e. R. ) )
15 13 14 mtbir 
 |-  -. <. ( {R ` ( 1st ` A ) ) , { R. } >. e. ( R. X. R. )
16 df-c 
 |-  CC = ( R. X. R. )
17 16 eleq2i 
 |-  ( <. ( {R ` ( 1st ` A ) ) , { R. } >. e. CC <-> <. ( {R ` ( 1st ` A ) ) , { R. } >. e. ( R. X. R. ) )
18 15 17 mtbir 
 |-  -. <. ( {R ` ( 1st ` A ) ) , { R. } >. e. CC
19 eqcom 
 |-  ( ( inftyexpitau ` A ) = <. ( {R ` ( 1st ` A ) ) , { R. } >. <-> <. ( {R ` ( 1st ` A ) ) , { R. } >. = ( inftyexpitau ` A ) )
20 19 biimpi 
 |-  ( ( inftyexpitau ` A ) = <. ( {R ` ( 1st ` A ) ) , { R. } >. -> <. ( {R ` ( 1st ` A ) ) , { R. } >. = ( inftyexpitau ` A ) )
21 20 eleq1d 
 |-  ( ( inftyexpitau ` A ) = <. ( {R ` ( 1st ` A ) ) , { R. } >. -> ( <. ( {R ` ( 1st ` A ) ) , { R. } >. e. CC <-> ( inftyexpitau ` A ) e. CC ) )
22 18 21 mtbii 
 |-  ( ( inftyexpitau ` A ) = <. ( {R ` ( 1st ` A ) ) , { R. } >. -> -. ( inftyexpitau ` A ) e. CC )
23 9 22 syl 
 |-  ( A e. dom inftyexpitau -> -. ( inftyexpitau ` A ) e. CC )
24 0ncn 
 |-  -. (/) e. CC
25 ndmfv 
 |-  ( -. A e. dom inftyexpitau -> ( inftyexpitau ` A ) = (/) )
26 25 eleq1d 
 |-  ( -. A e. dom inftyexpitau -> ( ( inftyexpitau ` A ) e. CC <-> (/) e. CC ) )
27 24 26 mtbiri 
 |-  ( -. A e. dom inftyexpitau -> -. ( inftyexpitau ` A ) e. CC )
28 23 27 pm2.61i 
 |-  -. ( inftyexpitau ` A ) e. CC