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

Theorem 4cn 10076
Description: The number 4 is a complex number. (Contributed by David A. Wheeler, 7-Jul-2016.)
Assertion
Ref Expression
4cn  |-  4  e.  CC

Proof of Theorem 4cn
StepHypRef Expression
1 4re 10075 . 2  |-  4  e.  RR
21recni 9104 1  |-  4  e.  CC
Colors of variables: wff set class
Syntax hints:    e. wcel 1726   CCcc 8990   4c4 10053
This theorem is referenced by:  4p2e6  10115  4p3e7  10116  4p4e8  10117  5p5e10  10121  4t2e8  10132  4d2e2  10134  8th4div3  10193  4t4e16  10457  fzo0to42pr  11188  discr  11518  cos2bnd  12791  pythagtriplem1  13192  13prm  13440  43prm  13446  163prm  13449  317prm  13450  631prm  13451  1259lem1  13452  1259lem2  13453  1259lem3  13454  1259lem4  13455  1259lem5  13456  2503lem1  13458  2503lem2  13459  2503lem3  13460  2503prm  13461  4001lem1  13462  4001lem2  13463  4001lem3  13464  4001lem4  13465  4001prm  13466  minveclem2  19329  minveclem3  19332  minveclem7  19338  uniioombl  19483  iblitg  19662  dveflem  19865  sincosq4sgn  20411  sincos6thpi  20425  ang180lem2  20654  quad2  20681  quad  20682  dcubic2  20686  dcubic  20688  mcubic  20689  cubic2  20690  cubic  20691  dquartlem1  20693  dquartlem2  20694  dquart  20695  quart1cl  20696  quart1lem  20697  quart1  20698  quartlem1  20699  quartlem2  20700  quartlem4  20702  quart  20703  log2cnv  20786  log2tlbnd  20787  log2ublem3  20790  log2ub  20791  bclbnd  21066  bposlem8  21077  pntibndlem2  21287  pntlemb  21293  ex-opab  21742  4ipval2  22206  4ipval3  22210  ipidsq  22211  dipcl  22213  dipcj  22215  dip0r  22218  dipcn  22221  ip1ilem  22329  minvecolem2  22379  minvecolem7  22387  normpar2i  22660  polid2i  22661  lnopeq0i  23512  4bc3eq4  25205  4bc2eq6  25206  bpoly3  26106  bpoly4  26107  lhe4.4ex1a  27525  stoweidlem13  27740  wallispi2lem1  27798  wallispi2lem2  27799  stirlinglem3  27803  stirlinglem8  27808  stirlinglem10  27810  stirlinglem12  27812  5m4e1  28597
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-resscn 9049  ax-1cn 9050  ax-icn 9051  ax-addcl 9052  ax-addrcl 9053  ax-mulcl 9054  ax-mulrcl 9055  ax-i2m1 9060  ax-1ne0 9061  ax-rrecex 9064  ax-cnre 9065
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2712  df-rex 2713  df-rab 2716  df-v 2960  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-nul 3631  df-if 3742  df-sn 3822  df-pr 3823  df-op 3825  df-uni 4018  df-br 4215  df-iota 5420  df-fv 5464  df-ov 6086  df-2 10060  df-3 10061  df-4 10062
  Copyright terms: Public domain W3C validator