MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  4cn Structured version   Visualization version   GIF version

Theorem 4cn 11058
Description: The number 4 is a complex number. (Contributed by David A. Wheeler, 7-Jul-2016.)
Assertion
Ref Expression
4cn 4 ∈ ℂ

Proof of Theorem 4cn
StepHypRef Expression
1 4re 11057 . 2 4 ∈ ℝ
21recni 10012 1 4 ∈ ℂ
Colors of variables: wff setvar class
Syntax hints:  wcel 1987  cc 9894  4c4 11032
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-resscn 9953  ax-1cn 9954  ax-icn 9955  ax-addcl 9956  ax-addrcl 9957  ax-mulcl 9958  ax-mulrcl 9959  ax-i2m1 9964  ax-1ne0 9965  ax-rrecex 9968  ax-cnre 9969
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2913  df-rex 2914  df-rab 2917  df-v 3192  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-nul 3898  df-if 4065  df-sn 4156  df-pr 4158  df-op 4162  df-uni 4410  df-br 4624  df-iota 5820  df-fv 5865  df-ov 6618  df-2 11039  df-3 11040  df-4 11041
This theorem is referenced by:  5m1e4  11099  4p2e6  11122  4p3e7  11123  4p4e8  11124  5p5e10OLD  11128  4t2e8  11141  4d2e2  11144  8th4div3  11212  div4p1lem1div2  11247  5p5e10  11556  4t4e16  11593  6t5e30  11604  fzo0to42pr  12512  fldiv4p1lem1div2  12592  sq4e2t8  12918  discr  12957  sqoddm1div8  12984  4bc3eq4  13071  4bc2eq6  13072  bpoly3  14733  bpoly4  14734  cos2bnd  14862  flodddiv4  15080  6gcd4e2  15198  6lcm4e12  15272  pythagtriplem1  15464  13prm  15766  43prm  15772  163prm  15775  317prm  15776  631prm  15777  prmo4  15778  prmo5  15779  1259lem1  15781  1259lem2  15782  1259lem3  15783  1259lem4  15784  1259lem5  15785  1259prm  15786  2503lem1  15787  2503lem2  15788  2503lem3  15789  2503prm  15790  4001lem1  15791  4001lem2  15792  4001lem3  15793  4001lem4  15794  4001prm  15795  cphipval2  22980  4cphipval2  22981  minveclem2  23137  minveclem3  23140  minveclem7  23146  uniioombl  23297  iblitg  23475  dveflem  23680  sincosq4sgn  24191  sincos6thpi  24205  ang180lem2  24474  heron  24499  quad2  24500  quad  24501  dcubic2  24505  dcubic  24507  mcubic  24508  cubic2  24509  cubic  24510  dquartlem1  24512  dquartlem2  24513  dquart  24514  quart1cl  24515  quart1lem  24516  quart1  24517  quartlem1  24518  quartlem2  24519  quartlem4  24521  quart  24522  log2cnv  24605  log2tlbnd  24606  log2ublem3  24609  log2ub  24610  bclbnd  24939  bposlem8  24950  bposlem9  24951  2lgslem3a  25055  2lgslem3b  25056  2lgslem3c  25057  2lgslem3d  25058  2lgsoddprmlem2  25068  2lgsoddprmlem3c  25071  2lgsoddprmlem3d  25072  pntibndlem2  25214  pntlemb  25220  ex-opab  27177  ex-exp  27195  ex-fac  27196  ex-bc  27197  ex-ind-dvds  27206  4ipval2  27451  ipidsq  27453  dipcl  27455  dipcj  27457  dip0r  27460  dipcn  27463  ip1ilem  27569  ipasslem10  27582  minvecolem2  27619  minvecolem7  27627  normpar2i  27901  polid2i  27902  lnopeq0i  28754  fib5  30290  fib6  30291  quad3  31325  inductionexd  37974  lhe4.4ex1a  38049  limclner  39319  stoweidlem13  39567  wallispi2lem1  39625  wallispi2lem2  39626  stirlinglem3  39630  stirlinglem10  39637  stirlinglem12  39639  sqwvfourb  39783  fouriersw  39785  fmtnorec4  40790  fmtno5lem4  40797  257prm  40802  fmtnofac1  40811  fmtno4prmfac  40813  fmtno5faclem1  40820  fmtno5faclem2  40821  139prmALT  40840  2exp11  40846  mod42tp1mod8  40848  3exp4mod41  40862  41prothprmlem1  40863  41prothprmlem2  40864  41prothprm  40865  8even  40951  nnsum4primeseven  41007  nnsum4primesevenALTV  41008  bgoldbtbndlem2  41013  zlmodzxzequap  41606  5m4e1  41876
  Copyright terms: Public domain W3C validator