Theorem 4cn 12349

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 12329	. 2 ⊢ 4 = (3 + 1)
2		3cn 12345	. . 3 ⊢ 3 ∈ ℂ
3		ax-1cn 11211	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11265	. 2 ⊢ (3 + 1) ∈ ℂ
5	1, 4	eqeltri 2835	1 ⊢ 4 ∈ ℂ

Syntax hints:   ∈ wcel 2106  (class class class)co 7431  ℂcc 11151  1c1 11154   + caddc 11156  3c3 12320  4c4 12321

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706  ax-1cn 11211  ax-addcl 11213

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-cleq 2727  df-clel 2814  df-2 12327  df-3 12328  df-4 12329

This theorem is referenced by:  5cn  12352  5m1e4  12394  4p2e6  12417  4p3e7  12418  4p4e8  12419  4t2e8  12432  4d2e2  12434  8th4div3  12484  div4p1lem1div2  12519  5p5e10  12802  4t4e16  12830  6t5e30  12838  fldiv4p1lem1div2  13872  sq4e2t8  14235  discr  14276  sqoddm1div8  14279  4bc2eq6  14365  bpoly3  16091  bpoly4  16092  cos2bnd  16221  flodddiv4  16449  6gcd4e2  16572  6lcm4e12  16650  pythagtriplem1  16850  2exp11  17124  13prm  17150  43prm  17156  163prm  17159  317prm  17160  631prm  17161  1259lem1  17165  1259lem2  17166  1259lem3  17167  1259lem4  17168  1259lem5  17169  1259prm  17170  2503lem1  17171  2503lem2  17172  2503lem3  17173  2503prm  17174  4001lem1  17175  4001lem2  17176  4001lem3  17177  4001lem4  17178  4001prm  17179  cphipval2  25289  4cphipval2  25290  minveclem2  25474  minveclem3  25477  minveclem7  25483  uniioombl  25638  dveflem  26032  sincosq4sgn  26558  tan4thpi  26571  sincos6thpi  26573  ang180lem2  26868  heron  26896  quad2  26897  quad  26898  dcubic2  26902  dcubic  26904  mcubic  26905  cubic2  26906  cubic  26907  dquartlem1  26909  dquartlem2  26910  dquart  26911  quart1cl  26912  quart1lem  26913  quart1  26914  quartlem1  26915  quartlem2  26916  quartlem4  26918  quart  26919  log2cnv  27002  log2tlbnd  27003  log2ublem3  27006  log2ub  27007  bclbnd  27339  bposlem8  27350  bposlem9  27351  2lgslem3a  27455  2lgslem3b  27456  2lgslem3c  27457  2lgslem3d  27458  2lgsoddprmlem2  27468  2lgsoddprmlem3c  27471  2lgsoddprmlem3d  27472  addsqnreup  27502  addsq2nreurex  27503  pntibndlem2  27650  pntlemb  27656  ex-opab  30461  ex-exp  30479  ex-fac  30480  ex-bc  30481  ex-ind-dvds  30490  4ipval2  30737  ipidsq  30739  dipcl  30741  dipcj  30743  dip0r  30746  dipcn  30749  ip1ilem  30855  ipasslem10  30868  minvecolem2  30904  minvecolem7  30912  normpar2i  31185  polid2i  31186  lnopeq0i  32036  quad3d  32761  fib5  34387  fib6  34388  hgt750lemd  34642  hgt750lem  34645  hgt750lem2  34646  quad3  35655  60gcd7e1  41987  420lcm8e840  41993  lcmineqlem23  42033  3exp7  42035  3lexlogpow5ineq1  42036  3lexlogpow2ineq2  42041  aks4d1p1p4  42053  aks4d1p1p7  42056  aks4d1p1p5  42057  aks4d1p1  42058  4t5e20  42305  sq4  42306  235t711  42318  flt4lem5e  42643  inductionexd  44145  lhe4.4ex1a  44325  limclner  45607  stoweidlem13  45969  wallispi2lem1  46027  wallispi2lem2  46028  stirlinglem3  46032  stirlinglem10  46039  stirlinglem12  46041  sqwvfourb  46185  fouriersw  46187  ceil5half3  47280  fmtnorec4  47474  fmtno5lem4  47481  257prm  47486  fmtnofac1  47495  fmtno4prmfac  47497  fmtno5faclem1  47504  fmtno5faclem2  47505  139prmALT  47521  mod42tp1mod8  47527  3exp4mod41  47541  41prothprmlem1  47542  41prothprmlem2  47543  41prothprm  47544  quad1  47545  8even  47638  2exp340mod341  47658  8exp8mod9  47661  mogoldbb  47710  nnsum4primeseven  47725  nnsum4primesevenALTV  47726  bgoldbtbndlem2  47731  zlmodzxzequap  48345  itsclc0yqsollem1  48612  itscnhlinecirc02plem1  48632  5m4e1  49028