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

Theorem 4cn 10030
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 10029 . 2  |-  4  e.  RR
21recni 9058 1  |-  4  e.  CC
Colors of variables: wff set class
Syntax hints:    e. wcel 1721   CCcc 8944   4c4 10007
This theorem is referenced by:  4p2e6  10069  4p3e7  10070  4p4e8  10071  5p5e10  10075  4t2e8  10086  4d2e2  10088  8th4div3  10147  4t4e16  10411  fzo0to42pr  11141  discr  11471  cos2bnd  12744  pythagtriplem1  13145  13prm  13393  43prm  13399  163prm  13402  317prm  13403  631prm  13404  1259lem1  13405  1259lem2  13406  1259lem3  13407  1259lem4  13408  1259lem5  13409  2503lem1  13411  2503lem2  13412  2503lem3  13413  2503prm  13414  4001lem1  13415  4001lem2  13416  4001lem3  13417  4001lem4  13418  4001prm  13419  minveclem2  19280  minveclem3  19283  minveclem7  19289  uniioombl  19434  iblitg  19613  dveflem  19816  sincosq4sgn  20362  sincos6thpi  20376  ang180lem2  20605  quad2  20632  quad  20633  dcubic2  20637  dcubic  20639  mcubic  20640  cubic2  20641  cubic  20642  dquartlem1  20644  dquartlem2  20645  dquart  20646  quart1cl  20647  quart1lem  20648  quart1  20649  quartlem1  20650  quartlem2  20651  quartlem4  20653  quart  20654  log2cnv  20737  log2tlbnd  20738  log2ublem3  20741  log2ub  20742  bclbnd  21017  bposlem8  21028  pntibndlem2  21238  pntlemb  21244  ex-opab  21693  4ipval2  22157  4ipval3  22161  ipidsq  22162  dipcl  22164  dipcj  22166  dip0r  22169  dipcn  22172  ip1ilem  22280  minvecolem2  22330  minvecolem7  22338  normpar2i  22611  polid2i  22612  lnopeq0i  23463  4bc3eq4  25156  4bc2eq6  25157  bpoly3  26008  bpoly4  26009  lhe4.4ex1a  27414  stoweidlem13  27629  wallispi2lem1  27687  wallispi2lem2  27688  stirlinglem3  27692  stirlinglem8  27697  stirlinglem10  27699  stirlinglem12  27701  5m4e1  28249
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-resscn 9003  ax-1cn 9004  ax-icn 9005  ax-addcl 9006  ax-addrcl 9007  ax-mulcl 9008  ax-mulrcl 9009  ax-i2m1 9014  ax-1ne0 9015  ax-rrecex 9018  ax-cnre 9019
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-ral 2671  df-rex 2672  df-rab 2675  df-v 2918  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-uni 3976  df-br 4173  df-iota 5377  df-fv 5421  df-ov 6043  df-2 10014  df-3 10015  df-4 10016
  Copyright terms: Public domain W3C validator