Mathbox for BJ < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  bj-inftyexpidisj Structured version   Visualization version   Unicode version

Theorem bj-inftyexpidisj 31652
 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.)
Assertion
Ref Expression
bj-inftyexpidisj inftyexpi

Proof of Theorem bj-inftyexpidisj
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 opeq1 4166 . . . . 5
2 df-bj-inftyexpi 31649 . . . . 5 inftyexpi
3 opex 4664 . . . . 5
41, 2, 3fvmpt 5948 . . . 4 inftyexpi
5 opex 4664 . . . . 5
65, 2dmmpti 5707 . . . 4 inftyexpi
74, 6eleq2s 2547 . . 3 inftyexpi inftyexpi
8 cnex 9620 . . . . . . 7
98prid2 4081 . . . . . 6
10 eqid 2451 . . . . . . . 8
1110olci 393 . . . . . . 7
12 elopg 4666 . . . . . . . 8
138, 12mpan2 677 . . . . . . 7
1411, 13mpbiri 237 . . . . . 6
15 en3lp 8121 . . . . . . 7
1615bj-imn3ani 31171 . . . . . 6
179, 14, 16sylancr 669 . . . . 5
18 opprc1 4189 . . . . . 6
19 0ncn 9557 . . . . . . 7
20 eleq1 2517 . . . . . . 7
2119, 20mtbiri 305 . . . . . 6
2218, 21syl 17 . . . . 5
2317, 22pm2.61i 168 . . . 4
24 eqcom 2458 . . . . . 6 inftyexpi inftyexpi
2524biimpi 198 . . . . 5 inftyexpi inftyexpi
2625eleq1d 2513 . . . 4 inftyexpi inftyexpi
2723, 26mtbii 304 . . 3 inftyexpi inftyexpi
287, 27syl 17 . 2 inftyexpi inftyexpi
29 ndmfv 5889 . . . 4 inftyexpi inftyexpi
3029eleq1d 2513 . . 3 inftyexpi inftyexpi
3119, 30mtbiri 305 . 2 inftyexpi inftyexpi
3228, 31pm2.61i 168 1 inftyexpi
 Colors of variables: wff setvar class Syntax hints:   wn 3   wb 188   wo 370   wceq 1444   wcel 1887  cvv 3045  c0 3731  csn 3968  cpr 3970  cop 3974   cdm 4834  cfv 5582  (class class class)co 6290  cc 9537  cneg 9861  cioc 11636  cpi 14119  inftyexpi cinftyexpi 31648 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-8 1889  ax-9 1896  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431  ax-sep 4525  ax-nul 4534  ax-pow 4581  ax-pr 4639  ax-un 6583  ax-reg 8107  ax-cnex 9595 This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 986  df-3an 987  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-eu 2303  df-mo 2304  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2624  df-ral 2742  df-rex 2743  df-rab 2746  df-v 3047  df-sbc 3268  df-dif 3407  df-un 3409  df-in 3411  df-ss 3418  df-nul 3732  df-if 3882  df-sn 3969  df-pr 3971  df-tp 3973  df-op 3975  df-uni 4199  df-br 4403  df-opab 4462  df-mpt 4463  df-id 4749  df-xp 4840  df-rel 4841  df-cnv 4842  df-co 4843  df-dm 4844  df-iota 5546  df-fun 5584  df-fn 5585  df-fv 5590  df-c 9545  df-bj-inftyexpi 31649 This theorem is referenced by:  bj-ccinftydisj  31655  bj-pinftynrr  31664  bj-minftynrr  31668
 Copyright terms: Public domain W3C validator