Theorem axicn 5193

Description: i is a complex number. Axiom 4 of 25 for real and complex numbers, derived from ZF set theory.

Assertion

Ref	Expression
axicn	|- i e. CC

Proof of Theorem axicn

Step	Hyp	Ref	Expression
1		df-i 5166	. . . 4 |- i = <.0R, 1R>.
2	1	eleq1i 1513	. . 3 |- (i e. CC <-> <.0R, 1R>. e. CC)
3		1r 5113	. . . . 5 |- 1R e. R.
4	3	elisseti 1793	. . . 4 |- 1R e. V
5	4	opelcn 5171	. . 3 |- (<.0R, 1R>. e. CC <-> (0R e. R. /\ 1R e. R.))
6	2, 5	bitr 173	. 2 |- (i e. CC <-> (0R e. R. /\ 1R e. R.))
7		0r 5112	. 2 |- 0R e. R.
8	6, 7, 3	mpbir2an 727	1 |- i e. CC

Syntax hints:   /\ wa 223   e. wcel 1105  <.cop 2382  R.cnr 4916  0Rc0r 4917  1Rc1r 4918  CCcc 5155  ici 5159

This theorem is referenced by:  0cn 5251  cnegextlem2 5269  cnegext 5271  0cnALT 5273  ine0 5357  1re 5358  ixi 5605  recextlem1 5606  recextlem2 5607  recext 5608  irec 6612  i2 6613  i3 6614  i4 6615  crulem 6617  cru 6618  crutOLD 6620  crne0 6621  crmul 6622  crrecz 6623  rimul 6626  nthruc 6627  replimtOLD 6644  cjclt 6647  crret 6653  crretOLD 6654  crimt 6655  crimtOLD 6656  imret 6661  reim0t 6662  reim0bt 6663  cjcj 6664  rereb 6666  cjreb 6667  recj 6668  imcj 6669  readd 6670  imadd 6671  cjadd 6674  cjmul 6675  reneg 6680  imneg 6682  cjneg 6683  addcj 6684  recjt 6704  imcjt 6705  rei 6710  imi 6711  cji 6713  cjreimt 6714  cjreim2t 6715  cj11t 6716  abs00 6728  absreimsqt 6742  absreimt 6743  absi 6766  recant 6793  caucvg3a 7051  caucvg3lem 7053  abspef01tlub 7287  sinclt 7324  cosclt 7325  resinvalt 7326  recosvalt 7327  efi4pt 7328  resin4pt 7329  recos4pt 7330  resinclt 7331  recosclt 7332  sinnegt 7335  cosnegt 7336  sin0 7337  cos0 7339  efivalt 7340  efmivalt 7341  efeult 7342  sinadd 7344  cosadd 7345  sin01bndlem2 7361  sin01bndlem3 7362  cos01bndlem2 7363  cos01bndlem3 7364  abseft 7376  demoivre 7377  demoivreALT 7378  nvpi 8170  ipval2 8226  4ipval2 8227  ipval3 8228  4ipval3 8231  ipid 8232  ipcl 8234  ipcj 8236  ip0r 8239  ip1cnilem1 8242  ip1cnilem2 8243  ip1cnilem3 8244  ip1cnilem4 8245  ip1cnilem5 8246  ip1cnilem6 8247  sspival 8266  ip1ilem 8351  ipasslem10 8365  ipasslem11 8366  sincolem 8497  sincnlem 8498  sinco 8499  sincn 8501  eulerid 8515  sinperlem1 8518  efimpi 8528  efif 8549  efif1lem4 8561  efielcircOLD 8568  efielcirc 8572  circgrp 8573  shftefif1olem 8574  shftefif1olemOLD 8575  eff1lem 8577  eff1i 8578  effoi 8579  effoiOLD 8580  efper 8582  pilog 8603  polid2 9173  polid 9174  lnopeq0lem1 10059  lnopeq0 10061  lnophmlem2 10071

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-4 951  ax-5 952  ax-6 953  ax-7 954  ax-gen 955  ax-8 1101  ax-9 1102  ax-10 1103  ax-12 1104  ax-13 1107  ax-14 1108  ax-11 1180  ax-17 1190  ax-16 1194  ax-11o 1202  ax-ext 1436  ax-rep 2661  ax-sep 2671  ax-nul 2678  ax-pow 2710  ax-pr 2747  ax-un 2830  ax-inf2 4549

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 773  df-3an 774  df-ex 957  df-sb 1155  df-eu 1359  df-mo 1360  df-clab 1441  df-cleq 1446  df-clel 1449  df-ne 1563  df-ral 1625  df-rex 1626  df-reu 1627  df-rab 1628  df-v 1787  df-sbc 1913  df-csb 1973  df-dif 2020  df-un 2021  df-in 2022  df-ss 2024  df-pss 2026  df-nul 2252  df-if 2333  df-pw 2373  df-sn 2383  df-pr 2384  df-tp 2386  df-op 2387  df-uni 2472  df-int 2502  df-iun 2536  df-br 2588  df-opab 2635  df-tr 2649  df-eprel 2794  df-id 2797  df-po 2804  df-so 2814  df-fr 2880  df-we 2897  df-ord 2914  df-on 2915  df-lim 2916  df-suc 2917  df-om 3095  df-xp 3147  df-rel 3148  df-cnv 3149  df-co 3150  df-dm 3151  df-rn 3152  df-res 3153  df-ima 3154  df-fun 3155  df-fn 3156  df-f 3157  df-fv 3161  df-rdg 3871  df-opr 3904  df-oprab 3905  df-1st 4017  df-2nd 4018  df-1o 4071  df-oadd 4073  df-omul 4074  df-er 4199  df-ec 4201  df-qs 4204  df-ni 4923  df-pli 4924  df-mi 4925  df-lti 4926  df-plpq 4958  df-mpq 4959  df-enq 4960  df-nq 4961  df-plq 4962  df-mq 4963  df-rq 4964  df-ltq 4965  df-1q 4966  df-np 5009  df-1p 5010  df-plp 5011  df-enr 5089  df-nr 5090  df-0r 5094  df-1r 5095  df-c 5163  df-i 5166

Copyright terms: Public domain