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

Theorem 4cn 12245
Description: The number 4 is a complex number. (Contributed by David A. Wheeler, 7-Jul-2016.) Reduce dependencies on axioms. (Revised by Steven Nguyen, 4-Oct-2022.)
Assertion
Ref Expression
4cn 4 ∈ ℂ

Proof of Theorem 4cn
StepHypRef Expression
1 df-4 12225 . 2 4 = (3 + 1)
2 3cn 12241 . . 3 3 ∈ ℂ
3 ax-1cn 11116 . . 3 1 ∈ ℂ
42, 3addcli 11168 . 2 (3 + 1) ∈ ℂ
51, 4eqeltri 2834 1 4 ∈ ℂ
Colors of variables: wff setvar class
Syntax hints:  wcel 2107  (class class class)co 7362  cc 11056  1c1 11059   + caddc 11061  3c3 12216  4c4 12217
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708  ax-1cn 11116  ax-addcl 11118
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2729  df-clel 2815  df-2 12223  df-3 12224  df-4 12225
This theorem is referenced by:  5cn  12248  5m1e4  12290  4p2e6  12313  4p3e7  12314  4p4e8  12315  4t2e8  12328  4d2e2  12330  8th4div3  12380  div4p1lem1div2  12415  5p5e10  12696  4t4e16  12724  6t5e30  12732  fldiv4p1lem1div2  13747  sq4e2t8  14110  discr  14150  sqoddm1div8  14153  4bc2eq6  14236  bpoly3  15948  bpoly4  15949  cos2bnd  16077  flodddiv4  16302  6gcd4e2  16426  6lcm4e12  16499  pythagtriplem1  16695  2exp11  16969  13prm  16995  43prm  17001  163prm  17004  317prm  17005  631prm  17006  1259lem1  17010  1259lem2  17011  1259lem3  17012  1259lem4  17013  1259lem5  17014  1259prm  17015  2503lem1  17016  2503lem2  17017  2503lem3  17018  2503prm  17019  4001lem1  17020  4001lem2  17021  4001lem3  17022  4001lem4  17023  4001prm  17024  cphipval2  24621  4cphipval2  24622  minveclem2  24806  minveclem3  24809  minveclem7  24815  uniioombl  24969  dveflem  25359  sincosq4sgn  25874  sincos6thpi  25888  ang180lem2  26176  heron  26204  quad2  26205  quad  26206  dcubic2  26210  dcubic  26212  mcubic  26213  cubic2  26214  cubic  26215  dquartlem1  26217  dquartlem2  26218  dquart  26219  quart1cl  26220  quart1lem  26221  quart1  26222  quartlem1  26223  quartlem2  26224  quartlem4  26226  quart  26227  log2cnv  26310  log2tlbnd  26311  log2ublem3  26314  log2ub  26315  bclbnd  26644  bposlem8  26655  bposlem9  26656  2lgslem3a  26760  2lgslem3b  26761  2lgslem3c  26762  2lgslem3d  26763  2lgsoddprmlem2  26773  2lgsoddprmlem3c  26776  2lgsoddprmlem3d  26777  addsqnreup  26807  addsq2nreurex  26808  pntibndlem2  26955  pntlemb  26961  ex-opab  29418  ex-exp  29436  ex-fac  29437  ex-bc  29438  ex-ind-dvds  29447  4ipval2  29692  ipidsq  29694  dipcl  29696  dipcj  29698  dip0r  29701  dipcn  29704  ip1ilem  29810  ipasslem10  29823  minvecolem2  29859  minvecolem7  29867  normpar2i  30140  polid2i  30141  lnopeq0i  30991  fib5  33045  fib6  33046  hgt750lemd  33301  hgt750lem  33304  hgt750lem2  33305  quad3  34298  60gcd7e1  40491  420lcm8e840  40497  lcmineqlem23  40537  3exp7  40539  3lexlogpow5ineq1  40540  3lexlogpow2ineq2  40545  aks4d1p1p4  40557  aks4d1p1p7  40560  aks4d1p1p5  40561  aks4d1p1  40562  235t711  40834  flt4lem5e  41023  inductionexd  42501  lhe4.4ex1a  42683  limclner  43966  stoweidlem13  44328  wallispi2lem1  44386  wallispi2lem2  44387  stirlinglem3  44391  stirlinglem10  44398  stirlinglem12  44400  sqwvfourb  44544  fouriersw  44546  fmtnorec4  45815  fmtno5lem4  45822  257prm  45827  fmtnofac1  45836  fmtno4prmfac  45838  fmtno5faclem1  45845  fmtno5faclem2  45846  139prmALT  45862  mod42tp1mod8  45868  3exp4mod41  45882  41prothprmlem1  45883  41prothprmlem2  45884  41prothprm  45885  quad1  45886  8even  45979  2exp340mod341  45999  8exp8mod9  46002  mogoldbb  46051  nnsum4primeseven  46066  nnsum4primesevenALTV  46067  bgoldbtbndlem2  46072  zlmodzxzequap  46654  itsclc0yqsollem1  46922  itscnhlinecirc02plem1  46942  5m4e1  47318
  Copyright terms: Public domain W3C validator