Theorem 2cn 9378

Description: The number 2 is a complex number. (Contributed by NM, 30-Jul-2004.)

Assertion

Ref	Expression
2cn	|- 2 e. CC

Proof of Theorem 2cn

Step	Hyp	Ref	Expression
1		2re 9377	. 2 |- 2 e. RR
2	1	recni 8339	1 |- 2 e. CC

This proof depends on syntax axioms:   e. wcel 2209   CCcc 8178   2c2 9358

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220  ax-resscn 8272  ax-1re 8274  ax-addrcl 8277

This proof depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-in 3226  df-ss 3233  df-2 9366

This theorem is used by:  2ex  9379  2cnd  9380  2m1e1  9425  3m1e2  9427  2p2e4  9434  times2  9436  2div2e1  9440  1p2e3  9442  3p3e6  9450  4p3e7  9452  5p3e8  9455  6p3e9  9458  2t1e2  9461  2t2e4  9462  2t3e6  9465  3t3e9  9466  2t4e8  9468  2t0e0  9469  4d2e2  9470  2cnne0  9519  1mhlfehlf  9528  8th4div3  9529  halfpm6th  9530  2mulicn  9532  2muliap0  9534  halfcl  9536  half0  9538  2halves  9539  halfaddsub  9544  div4p1lem1div2  9564  3halfnz  9748  zneo  9752  nneoor  9753  zeo  9756  7p3e10  9861  4t4e16  9885  6t3e18  9891  7t7e49  9900  8t5e40  9904  9t9e81  9915  decbin0  9926  decbin2  9927  halfthird  9929  fztpval  10501  fz0tp  10540  fz0to4untppr  10542  fzo0to3tp  10648  2tnp1ge0ge0  10751  fldiv4lem1div2  10757  expubnd  11048  sq2  11087  sq4e2t8  11089  cu2  11090  subsq2  11099  binom2sub  11105  binom3  11109  zesq  11111  fac2  11185  fac3  11186  faclbnd2  11196  bcn2  11218  4bc2eq6  11229  crre  11638  addcj  11672  imval2  11675  resqrexlemover  11792  resqrexlemcalc1  11796  resqrexlemnm  11800  resqrexlemcvg  11801  amgm2  11901  arisum  12284  arisum2  12285  geo2sum2  12301  geo2lim  12302  geoihalfsum  12308  efcllemp  12444  ege2le3  12457  tanval2ap  12499  tanval3ap  12500  efi4p  12503  efival  12518  sinadd  12522  cosadd  12523  sinmul  12530  cosmul  12531  cos2tsin  12537  ef01bndlem  12542  sin01bnd  12543  cos01bnd  12544  cos1bnd  12545  cos2bnd  12546  cos01gt0  12549  sin02gt0  12550  sin4lt0  12553  cos12dec  12554  egt2lt3  12566  odd2np1lem  12658  odd2np1  12659  ltoddhalfle  12679  halfleoddlt  12680  opoe  12681  omoe  12682  opeo  12683  omeo  12684  nno  12692  nn0o  12693  flodddiv4  12722  bits0  12734  bitsfzolem  12740  0bits  12745  bitsinv1  12748  6gcd4e2  12791  3lcm2e6woprm  12883  6lcm4e12  12884  sqrt2irrlem  12959  pythagtriplem1  13067  pythagtriplem12  13077  pythagtriplem14  13079  4sqlem11  13203  4sqlem12  13204  dec5dvds  13214  dec2nprm  13217  2exp5  13235  2exp6  13236  2exp7  13237  2exp8  13238  2exp11  13239  2exp16  13240  10nprm  13251  11prm  13252  13prm  13253  37prm  13258  43prm  13259  83prm  13260  139prm  13261  163prm  13262  317prm  13263  631prm  13264  1259lem1  13265  1259lem2  13266  1259lem3  13267  1259lem4  13268  1259lem5  13269  1259prm  13270  ballotfilem2  13280  ballotfilemth  13333  maxcncf  15807  mincncf  15808  coscn  15962  sinhalfpilem  15984  cospi  15993  ef2pi  15998  ef2kpi  15999  efper  16000  sinperlem  16001  sin2kpi  16004  cos2kpi  16005  sin2pim  16006  cos2pim  16007  ptolemy  16017  sincosq3sgn  16021  sincosq4sgn  16022  sinq12gt0  16023  cosq23lt0  16026  coseq00topi  16028  tangtx  16031  sincos4thpi  16033  sincos6thpi  16035  sincos3rdpi  16036  pigt3  16037  abssinper  16039  coskpi  16041  cosq34lt1  16043  logsqrt  16120  2logb9irrALT  16171  log2tlbndlog2  16181  log2ublem2  16183  log2ublem3  16184  log2ublog2  16185  birthdaylog2  16189  1sgm2ppw  16250  ppiqub  16254  chtublem  16256  chtqub  16257  perfect1  16259  perfectlem1  16260  perfectlem2  16261  perfect  16262  bcmax  16266  bcp1ctr  16267  bclbnd  16268  bpos1lem  16270  bpos1  16271  bposlem1  16272  bposlem2  16273  bposlem4  16275  bposlem5  16276  bposlem6  16277  bposlem8  16279  bposlem9  16280  lgsdir2lem2  16314  gausslemma2dlem6  16352  lgsquadlem1  16362  lgsquadlem2  16363  lgsquad2lem2  16367  m1lgs  16370  2lgslem3a  16378  2lgslem3b  16379  2lgslem3c  16380  2lgslem3d  16381  2lgsoddprmlem2  16391  2lgsoddprmlem3c  16394  2lgsoddprmlem3d  16395  clwwlknonex2  16846  ex-fl  16905  ex-ceil  16906  ex-exp  16907  ex-fac  16908