Theorem axicn 5257

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 5230	. . . 4 |- i = <.0R, 1R>.
2	1	eleq1i 1536	. . 3 |- (i e. CC <-> <.0R, 1R>. e. CC)
3		1r 5177	. . . . 5 |- 1R e. R.
4	3	elisseti 1816	. . . 4 |- 1R e. V
5	4	opelcn 5235	. . 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 5176	. 2 |- 0R e. R.
8	6, 7, 3	mpbir2an 729	1 |- i e. CC

Syntax hints:   /\ wa 223   e. wcel 957  <.cop 2409  R.cnr 4980  0Rc0r 4981  1Rc1r 4982  CCcc 5219  ici 5223

This theorem is referenced by:  0cn 5315  cnegextlem2 5333  cnegext 5335  0cnALT 5337  ine0 5421  1re 5422  ixi 5668  recextlem1 5669  recextlem2 5670  recext 5671  irec 6682  i2 6683  i3 6684  i4 6685  crulem 6687  cru 6688  crutOLD 6690  crne0 6691  crmul 6692  crrecz 6693  rimul 6696  nthruc 6697  replimtOLD 6714  cjclt 6717  crret 6723  crretOLD 6724  crimt 6725  crimtOLD 6726  imret 6731  imretOLD 6732  reim0t 6733  reim0bt 6734  reim0btOLD 6735  cjcj 6736  rereb 6738  rerebOLD 6739  cjreb 6740  recj 6741  imcj 6742  readd 6743  imadd 6744  cjadd 6747  cjmul 6748  reneg 6753  renegOLD 6754  imneg 6756  imnegOLD 6757  cjneg 6758  addcj 6759  recjt 6779  imcjt 6780  rei 6785  imi 6786  cji 6788  cjreimt 6789  cjreim2t 6790  cj11t 6791  abs00 6803  abs00OLD 6804  absreimsqt 6818  absreimt 6819  absi 6842  recant 6870  recantOLD 6871  caucvg3a 7133  caucvg3aOLD 7134  caucvg3lem 7136  caucvg3lemOLD 7137  abspef01tlub 7372  sinclt 7409  cosclt 7410  resinvalt 7411  recosvalt 7412  efi4pt 7413  resin4pt 7414  recos4pt 7415  resinclt 7416  recosclt 7417  sinnegt 7420  cosnegt 7421  sin0 7422  cos0 7424  efivalt 7425  efmivalt 7426  efeult 7427  sinadd 7429  cosadd 7430  sin01bndlem2 7446  sin01bndlem3 7447  cos01bndlem2 7448  cos01bndlem3 7449  abseft 7461  demoivre 7462  demoivreALT 7463  nvpi 8279  ipval2 8343  4ipval2 8344  ipval3 8345  4ipval3 8348  ipid 8349  ipcl 8351  ipcj 8353  ip0r 8356  ip1cnilem1 8359  ip1cnilem2 8360  ip1cnilem3 8361  ip1cnilem4 8362  ip1cnilem5 8363  ip1cnilem6 8364  sspival 8383  ip1ilem 8469  ipasslem10 8483  ipasslem11 8484  sincolem 8648  sincnlem 8649  sinco 8650  sincn 8652  eulerid 8666  sinperlem1 8669  efimpi 8679  efif 8700  efif1lem4 8712  efielcircOLD 8719  efielcirc 8723  circgrp 8724  shftefif1olem 8725  eff1lem 8727  eff1i 8728  effoi 8729  efper 8731  pilog 8752  polid2 9008  polid 9009  lnopeq0lem1 9921  lnopeq0 9923  lnophmlem2 9933

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 961  ax-gen 962  ax-8 963  ax-9 964  ax-10 965  ax-11 966  ax-12 967  ax-13 968  ax-14 969  ax-17 970  ax-4 972  ax-5o 974  ax-6o 977  ax-9o 1122  ax-10o 1139  ax-16 1210  ax-11o 1218  ax-ext 1459  ax-rep 2690  ax-sep 2700  ax-nul 2707  ax-pow 2739  ax-pr 2776  ax-un 2863  ax-inf2 4612

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 775  df-3an 776  df-ex 980  df-sb 1172  df-eu 1382  df-mo 1383  df-clab 1464  df-cleq 1469  df-clel 1472  df-ne 1586  df-ral 1648  df-rex 1649  df-reu 1650  df-rab 1651  df-v 1810  df-sbc 1940  df-csb 2000  df-dif 2047  df-un 2048  df-in 2049  df-ss 2051  df-pss 2053  df-nul 2279  df-if 2360  df-pw 2400  df-sn 2410  df-pr 2411  df-tp 2413  df-op 2414  df-uni 2501  df-int 2531  df-iun 2565  df-br 2617  df-opab 2664  df-tr 2678  df-eprel 2829  df-id 2832  df-po 2837  df-so 2847  df-fr 2914  df-we 2931  df-ord 2948  df-on 2949  df-lim 2950  df-suc 2951  df-om 3129  df-xp 3181  df-rel 3182  df-cnv 3183  df-co 3184  df-dm 3185  df-rn 3186  df-res 3187  df-ima 3188  df-fun 3189  df-fn 3190  df-f 3191  df-fv 3195  df-rdg 3929  df-opr 3962  df-oprab 3963  df-1st 4076  df-2nd 4077  df-1o 4130  df-oadd 4132  df-omul 4133  df-er 4258  df-ec 4260  df-qs 4263  df-ni 4987  df-pli 4988  df-mi 4989  df-lti 4990  df-plpq 5022  df-mpq 5023  df-enq 5024  df-nq 5025  df-plq 5026  df-mq 5027  df-rq 5028  df-ltq 5029  df-1q 5030  df-np 5073  df-1p 5074  df-plp 5075  df-enr 5153  df-nr 5154  df-0r 5158  df-1r 5159  df-c 5227  df-i 5230

Copyright terms: Public domain