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

Theorem 4cn 11710
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 11690 . 2 4 = (3 + 1)
2 3cn 11706 . . 3 3 ∈ ℂ
3 ax-1cn 10583 . . 3 1 ∈ ℂ
42, 3addcli 10635 . 2 (3 + 1) ∈ ℂ
51, 4eqeltri 2906 1 4 ∈ ℂ
Colors of variables: wff setvar class
Syntax hints:  wcel 2105  (class class class)co 7145  cc 10523  1c1 10526   + caddc 10528  3c3 11681  4c4 11682
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-ext 2790  ax-1cn 10583  ax-addcl 10585
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-cleq 2811  df-clel 2890  df-2 11688  df-3 11689  df-4 11690
This theorem is referenced by:  5cn  11713  5m1e4  11755  4p2e6  11778  4p3e7  11779  4p4e8  11780  4t2e8  11793  4d2e2  11795  8th4div3  11845  div4p1lem1div2  11880  5p5e10  12157  4t4e16  12185  6t5e30  12193  fldiv4p1lem1div2  13193  sq4e2t8  13550  discr  13589  sqoddm1div8  13592  4bc2eq6  13677  bpoly3  15400  bpoly4  15401  cos2bnd  15529  flodddiv4  15752  6gcd4e2  15874  6lcm4e12  15948  pythagtriplem1  16141  13prm  16437  43prm  16443  163prm  16446  317prm  16447  631prm  16448  1259lem1  16452  1259lem2  16453  1259lem3  16454  1259lem4  16455  1259lem5  16456  1259prm  16457  2503lem1  16458  2503lem2  16459  2503lem3  16460  2503prm  16461  4001lem1  16462  4001lem2  16463  4001lem3  16464  4001lem4  16465  4001prm  16466  cphipval2  23771  4cphipval2  23772  minveclem2  23956  minveclem3  23959  minveclem7  23965  uniioombl  24117  dveflem  24503  sincosq4sgn  25014  sincos6thpi  25028  ang180lem2  25315  heron  25343  quad2  25344  quad  25345  dcubic2  25349  dcubic  25351  mcubic  25352  cubic2  25353  cubic  25354  dquartlem1  25356  dquartlem2  25357  dquart  25358  quart1cl  25359  quart1lem  25360  quart1  25361  quartlem1  25362  quartlem2  25363  quartlem4  25365  quart  25366  log2cnv  25449  log2tlbnd  25450  log2ublem3  25453  log2ub  25454  bclbnd  25783  bposlem8  25794  bposlem9  25795  2lgslem3a  25899  2lgslem3b  25900  2lgslem3c  25901  2lgslem3d  25902  2lgsoddprmlem2  25912  2lgsoddprmlem3c  25915  2lgsoddprmlem3d  25916  addsqnreup  25946  addsq2nreurex  25947  pntibndlem2  26094  pntlemb  26100  ex-opab  28138  ex-exp  28156  ex-fac  28157  ex-bc  28158  ex-ind-dvds  28167  4ipval2  28412  ipidsq  28414  dipcl  28416  dipcj  28418  dip0r  28421  dipcn  28424  ip1ilem  28530  ipasslem10  28543  minvecolem2  28579  minvecolem7  28587  normpar2i  28860  polid2i  28861  lnopeq0i  29711  fib5  31562  fib6  31563  hgt750lemd  31818  hgt750lem  31821  hgt750lem2  31822  quad3  32810  235t711  39055  inductionexd  40383  lhe4.4ex1a  40538  limclner  41808  stoweidlem13  42175  wallispi2lem1  42233  wallispi2lem2  42234  stirlinglem3  42238  stirlinglem10  42245  stirlinglem12  42247  sqwvfourb  42391  fouriersw  42393  fmtnorec4  43588  fmtno5lem4  43595  257prm  43600  fmtnofac1  43609  fmtno4prmfac  43611  fmtno5faclem1  43618  fmtno5faclem2  43619  139prmALT  43636  2exp11  43642  mod42tp1mod8  43644  3exp4mod41  43658  41prothprmlem1  43659  41prothprmlem2  43660  41prothprm  43661  quad1  43662  8even  43755  2exp340mod341  43775  8exp8mod9  43778  mogoldbb  43827  nnsum4primeseven  43842  nnsum4primesevenALTV  43843  bgoldbtbndlem2  43848  zlmodzxzequap  44482  itsclc0yqsollem1  44677  itscnhlinecirc02plem1  44697  5m4e1  44826
  Copyright terms: Public domain W3C validator