Theorem 4cn 12378

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

Step	Hyp	Ref	Expression
1		df-4 12358	. 2 ⊢ 4 = (3 + 1)
2		3cn 12374	. . 3 ⊢ 3 ∈ ℂ
3		ax-1cn 11242	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11296	. 2 ⊢ (3 + 1) ∈ ℂ
5	1, 4	eqeltri 2840	1 ⊢ 4 ∈ ℂ

Syntax hints:   ∈ wcel 2108  (class class class)co 7448  ℂcc 11182  1c1 11185   + caddc 11187  3c3 12349  4c4 12350

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-1cn 11242  ax-addcl 11244

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-clel 2819  df-2 12356  df-3 12357  df-4 12358

This theorem is referenced by:  5cn  12381  5m1e4  12423  4p2e6  12446  4p3e7  12447  4p4e8  12448  4t2e8  12461  4d2e2  12463  8th4div3  12513  div4p1lem1div2  12548  5p5e10  12829  4t4e16  12857  6t5e30  12865  fldiv4p1lem1div2  13886  sq4e2t8  14248  discr  14289  sqoddm1div8  14292  4bc2eq6  14378  bpoly3  16106  bpoly4  16107  cos2bnd  16236  flodddiv4  16461  6gcd4e2  16585  6lcm4e12  16663  pythagtriplem1  16863  2exp11  17137  13prm  17163  43prm  17169  163prm  17172  317prm  17173  631prm  17174  1259lem1  17178  1259lem2  17179  1259lem3  17180  1259lem4  17181  1259lem5  17182  1259prm  17183  2503lem1  17184  2503lem2  17185  2503lem3  17186  2503prm  17187  4001lem1  17188  4001lem2  17189  4001lem3  17190  4001lem4  17191  4001prm  17192  cphipval2  25294  4cphipval2  25295  minveclem2  25479  minveclem3  25482  minveclem7  25488  uniioombl  25643  dveflem  26037  sincosq4sgn  26561  tan4thpi  26574  sincos6thpi  26576  ang180lem2  26871  heron  26899  quad2  26900  quad  26901  dcubic2  26905  dcubic  26907  mcubic  26908  cubic2  26909  cubic  26910  dquartlem1  26912  dquartlem2  26913  dquart  26914  quart1cl  26915  quart1lem  26916  quart1  26917  quartlem1  26918  quartlem2  26919  quartlem4  26921  quart  26922  log2cnv  27005  log2tlbnd  27006  log2ublem3  27009  log2ub  27010  bclbnd  27342  bposlem8  27353  bposlem9  27354  2lgslem3a  27458  2lgslem3b  27459  2lgslem3c  27460  2lgslem3d  27461  2lgsoddprmlem2  27471  2lgsoddprmlem3c  27474  2lgsoddprmlem3d  27475  addsqnreup  27505  addsq2nreurex  27506  pntibndlem2  27653  pntlemb  27659  ex-opab  30464  ex-exp  30482  ex-fac  30483  ex-bc  30484  ex-ind-dvds  30493  4ipval2  30740  ipidsq  30742  dipcl  30744  dipcj  30746  dip0r  30749  dipcn  30752  ip1ilem  30858  ipasslem10  30871  minvecolem2  30907  minvecolem7  30915  normpar2i  31188  polid2i  31189  lnopeq0i  32039  quad3d  32757  fib5  34370  fib6  34371  hgt750lemd  34625  hgt750lem  34628  hgt750lem2  34629  quad3  35638  60gcd7e1  41962  420lcm8e840  41968  lcmineqlem23  42008  3exp7  42010  3lexlogpow5ineq1  42011  3lexlogpow2ineq2  42016  aks4d1p1p4  42028  aks4d1p1p7  42031  aks4d1p1p5  42032  aks4d1p1  42033  4t5e20  42280  sq4  42281  235t711  42293  flt4lem5e  42611  inductionexd  44117  lhe4.4ex1a  44298  limclner  45572  stoweidlem13  45934  wallispi2lem1  45992  wallispi2lem2  45993  stirlinglem3  45997  stirlinglem10  46004  stirlinglem12  46006  sqwvfourb  46150  fouriersw  46152  fmtnorec4  47423  fmtno5lem4  47430  257prm  47435  fmtnofac1  47444  fmtno4prmfac  47446  fmtno5faclem1  47453  fmtno5faclem2  47454  139prmALT  47470  mod42tp1mod8  47476  3exp4mod41  47490  41prothprmlem1  47491  41prothprmlem2  47492  41prothprm  47493  quad1  47494  8even  47587  2exp340mod341  47607  8exp8mod9  47610  mogoldbb  47659  nnsum4primeseven  47674  nnsum4primesevenALTV  47675  bgoldbtbndlem2  47680  zlmodzxzequap  48228  itsclc0yqsollem1  48496  itscnhlinecirc02plem1  48516  5m4e1  48891