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

Theorem 4cn 10942
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 10941 . 2 4 ∈ ℝ
21recni 9905 1 4 ∈ ℂ
Colors of variables: wff setvar class
Syntax hints:  wcel 1976  cc 9787  4c4 10916
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2229  ax-ext 2586  ax-resscn 9846  ax-1cn 9847  ax-icn 9848  ax-addcl 9849  ax-addrcl 9850  ax-mulcl 9851  ax-mulrcl 9852  ax-i2m1 9857  ax-1ne0 9858  ax-rrecex 9861  ax-cnre 9862
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2593  df-cleq 2599  df-clel 2602  df-nfc 2736  df-ne 2778  df-ral 2897  df-rex 2898  df-rab 2901  df-v 3171  df-dif 3539  df-un 3541  df-in 3543  df-ss 3550  df-nul 3871  df-if 4033  df-sn 4122  df-pr 4124  df-op 4128  df-uni 4364  df-br 4575  df-iota 5751  df-fv 5795  df-ov 6527  df-2 10923  df-3 10924  df-4 10925
This theorem is referenced by:  5m1e4  10983  4p2e6  11006  4p3e7  11007  4p4e8  11008  5p5e10OLD  11012  4t2e8  11025  4d2e2  11028  8th4div3  11096  div4p1lem1div2  11131  5p5e10  11425  4t4e16  11462  6t5e30  11473  fzo0to42pr  12374  fldiv4p1lem1div2  12450  sq4e2t8  12776  discr  12815  sqoddm1div8  12842  4bc3eq4  12929  4bc2eq6  12930  bpoly3  14571  bpoly4  14572  cos2bnd  14700  flodddiv4  14918  6gcd4e2  15036  6lcm4e12  15110  pythagtriplem1  15302  13prm  15604  43prm  15610  163prm  15613  317prm  15614  631prm  15615  prmo4  15616  prmo5  15617  1259lem1  15619  1259lem2  15620  1259lem3  15621  1259lem4  15622  1259lem5  15623  1259prm  15624  2503lem1  15625  2503lem2  15626  2503lem3  15627  2503prm  15628  4001lem1  15629  4001lem2  15630  4001lem3  15631  4001lem4  15632  4001prm  15633  minveclem2  22919  minveclem3  22922  minveclem7  22928  uniioombl  23077  iblitg  23255  dveflem  23460  sincosq4sgn  23971  sincos6thpi  23985  ang180lem2  24254  heron  24279  quad2  24280  quad  24281  dcubic2  24285  dcubic  24287  mcubic  24288  cubic2  24289  cubic  24290  dquartlem1  24292  dquartlem2  24293  dquart  24294  quart1cl  24295  quart1lem  24296  quart1  24297  quartlem1  24298  quartlem2  24299  quartlem4  24301  quart  24302  log2cnv  24385  log2tlbnd  24386  log2ublem3  24389  log2ub  24390  bclbnd  24719  bposlem8  24730  bposlem9  24731  2lgslem3a  24835  2lgslem3b  24836  2lgslem3c  24837  2lgslem3d  24838  2lgsoddprmlem2  24848  2lgsoddprmlem3c  24851  2lgsoddprmlem3d  24852  pntibndlem2  24994  pntlemb  25000  ex-opab  26444  ex-exp  26462  ex-fac  26463  ex-bc  26464  ex-ind-dvds  26473  4ipval2  26745  4ipval3  26749  ipidsq  26750  dipcl  26752  dipcj  26754  dip0r  26757  dipcn  26760  ip1ilem  26868  ipasslem10  26881  minvecolem2  26918  minvecolem7  26926  normpar2i  27200  polid2i  27201  lnopeq0i  28053  fib5  29597  fib6  29598  quad3  30621  inductionexd  37273  lhe4.4ex1a  37350  limclner  38519  stoweidlem13  38707  wallispi2lem1  38765  wallispi2lem2  38766  stirlinglem3  38770  stirlinglem10  38777  stirlinglem12  38779  sqwvfourb  38923  fouriersw  38925  fmtnorec4  39801  fmtno5lem4  39808  257prm  39813  fmtnofac1  39822  fmtno4prmfac  39824  fmtno5faclem1  39831  fmtno5faclem2  39832  139prmALT  39851  2exp11  39857  mod42tp1mod8  39859  3exp4mod41  39873  41prothprmlem1  39874  41prothprmlem2  39875  41prothprm  39876  8even  39962  nnsum4primeseven  40018  nnsum4primesevenALTV  40019  bgoldbtbndlem2  40024  zlmodzxzequap  42081  5m4e1  42312
  Copyright terms: Public domain W3C validator