Theorem 4cn 12260

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 12240	. 2 ⊢ 4 = (3 + 1)
2		3cn 12256	. . 3 ⊢ 3 ∈ ℂ
3		ax-1cn 11090	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11145	. 2 ⊢ (3 + 1) ∈ ℂ
5	1, 4	eqeltri 2833	1 ⊢ 4 ∈ ℂ

Syntax hints:   ∈ wcel 2114  (class class class)co 7361  ℂcc 11030  1c1 11033   + caddc 11035  3c3 12231  4c4 12232

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-1cn 11090  ax-addcl 11092

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-clel 2812  df-2 12238  df-3 12239  df-4 12240

This theorem is referenced by:  5cn  12263  5m1e4  12300  4p2e6  12323  4p3e7  12324  4p4e8  12325  4t2e8  12338  4div2e2  12340  8th4div3  12391  div4p1lem1div2  12426  5p5e10  12709  4t4e16  12737  6t5e30  12745  fldiv4p1lem1div2  13788  sq4e2t8  14155  discr  14196  sqoddm1div8  14199  4bc2eq6  14285  bpoly3  16017  bpoly4  16018  cos2bnd  16149  flodddiv4  16378  6gcd4e2  16501  6lcm4e12  16579  pythagtriplem1  16781  2exp11  17054  13prm  17080  43prm  17086  163prm  17089  317prm  17090  631prm  17091  1259lem1  17095  1259lem2  17096  1259lem3  17097  1259lem4  17098  1259lem5  17099  1259prm  17100  2503lem1  17101  2503lem2  17102  2503lem3  17103  2503prm  17104  4001lem1  17105  4001lem2  17106  4001lem3  17107  4001lem4  17108  4001prm  17109  cphipval2  25221  4cphipval2  25222  minveclem2  25406  minveclem3  25409  minveclem7  25415  uniioombl  25569  dveflem  25959  sincosq4sgn  26481  tan4thpi  26494  sincos6thpi  26496  ang180lem2  26790  heron  26818  quad2  26819  quad  26820  dcubic2  26824  dcubic  26826  mcubic  26827  cubic2  26828  cubic  26829  dquartlem1  26831  dquartlem2  26832  dquart  26833  quart1cl  26834  quart1lem  26835  quart1  26836  quartlem1  26837  quartlem2  26838  quartlem4  26840  quart  26841  log2cnv  26924  log2tlbnd  26925  log2ublem3  26928  log2ub  26929  bclbnd  27260  bposlem8  27271  bposlem9  27272  2lgslem3a  27376  2lgslem3b  27377  2lgslem3c  27378  2lgslem3d  27379  2lgsoddprmlem2  27389  2lgsoddprmlem3c  27392  2lgsoddprmlem3d  27393  addsqnreup  27423  addsq2nreurex  27424  pntibndlem2  27571  pntlemb  27577  ex-opab  30520  ex-exp  30538  ex-fac  30539  ex-bc  30540  ex-ind-dvds  30549  4ipval2  30797  ipidsq  30799  dipcl  30801  dipcj  30803  dip0r  30806  dipcn  30809  ip1ilem  30915  ipasslem10  30928  minvecolem2  30964  minvecolem7  30972  normpar2i  31245  polid2i  31246  lnopeq0i  32096  quad3d  32840  constrresqrtcl  33940  cos9thpiminplylem1  33945  fib5  34568  fib6  34569  hgt750lemd  34811  hgt750lem  34814  hgt750lem2  34815  quad3  35871  60gcd7e1  42461  420lcm8e840  42467  lcmineqlem23  42507  3exp7  42509  3lexlogpow5ineq1  42510  3lexlogpow2ineq2  42515  aks4d1p1p4  42527  aks4d1p1p7  42530  aks4d1p1p5  42531  aks4d1p1  42532  4t5e20  42740  sq4  42742  235t711  42754  flt4lem5e  43106  inductionexd  44603  lhe4.4ex1a  44777  limclner  46100  stoweidlem13  46462  wallispi2lem1  46520  wallispi2lem2  46521  stirlinglem3  46525  stirlinglem10  46532  stirlinglem12  46534  sqwvfourb  46678  fouriersw  46680  sin5tlem1  47340  sin5tlem2  47341  sin5tlem3  47342  sin5tlem4  47343  sinnpoly  47354  ceil5half3  47809  modm1p1ne  47839  fmtnorec4  48027  fmtno5lem4  48034  257prm  48039  fmtnofac1  48048  fmtno4prmfac  48050  fmtno5faclem1  48057  fmtno5faclem2  48058  139prmALT  48074  mod42tp1mod8  48080  3exp4mod41  48094  41prothprmlem1  48095  41prothprmlem2  48096  41prothprm  48097  ppivalnn4  48105  quad1  48111  8even  48204  2exp340mod341  48224  8exp8mod9  48227  mogoldbb  48276  nnsum4primeseven  48291  nnsum4primesevenALTV  48292  bgoldbtbndlem2  48297  zlmodzxzequap  48990  itsclc0yqsollem1  49253  itscnhlinecirc02plem1  49273  5m4e1  50287