Theorem 4cn 12303

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 12282	. 2 ⊢ 4 = (3 + 1)
2		3cn 12299	. . 3 ⊢ 3 ∈ ℂ
3		ax-1cn 11131	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11188	. 2 ⊢ (3 + 1) ∈ ℂ
5	1, 4	eqeltri 2858	1 ⊢ 4 ∈ ℂ

Syntax hints:   ∈ wcel 2142  (class class class)co 7396  ℂcc 11071  1c1 11074   + caddc 11076  3c3 12273  4c4 12274

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734  ax-1cn 11131  ax-addcl 11133

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-cleq 2754  df-clel 2837  df-2 12280  df-3 12281  df-4 12282

This theorem is referenced by:  5cn  12306  5m1e4  12347  4p2e6  12370  4p3e7  12371  4p4e8  12372  4t2e8  12386  2t4e8  12387  4div2e2  12389  8th4div3  12441  div4p1lem1div2  12476  5p5e10  12764  4t4e16  12792  6t5e30  12800  fldiv4p1lem1div2  13845  sq4e2t8  14212  discr  14253  sqoddm1div8  14256  4bc2eq6  14342  bpoly3  16088  bpoly4  16089  cos2bnd  16220  flodddiv4  16449  6gcd4e2  16572  6lcm4e12  16650  pythagtriplem1  16852  2exp11  17125  13prm  17152  43prm  17158  163prm  17161  317prm  17162  631prm  17163  1259lem1  17167  1259lem2  17168  1259lem3  17169  1259lem4  17170  1259lem5  17171  1259prm  17172  2503lem1  17173  2503lem2  17174  2503lem3  17175  2503prm  17176  4001lem1  17177  4001lem2  17178  4001lem3  17179  4001lem4  17180  4001prm  17181  cphipval2  25303  4cphipval2  25304  minveclem2  25488  minveclem3  25491  minveclem7  25497  uniioombl  25651  dveflem  26041  sincosq4sgn  26566  tan4thpi  26579  sincos6thpi  26581  ang180lem2  26875  heron  26903  quad2  26904  quad  26905  dcubic2  26909  dcubic  26911  mcubic  26912  cubic2  26913  cubic  26914  dquartlem1  26916  dquartlem2  26917  dquart  26918  quart1cl  26919  quart1lem  26920  quart1  26921  quartlem1  26922  quartlem2  26923  quartlem4  26925  quart  26926  log2cnv  27009  log2tlbnd  27010  log2ublem3  27013  log2ub  27014  bclbnd  27344  bposlem8  27355  bposlem9  27356  2lgslem3a  27460  2lgslem3b  27461  2lgslem3c  27462  2lgslem3d  27463  2lgsoddprmlem2  27473  2lgsoddprmlem3c  27476  2lgsoddprmlem3d  27477  addsqnreup  27507  addsq2nreurex  27508  pntibndlem2  27655  pntlemb  27661  ex-opab  30634  ex-exp  30652  ex-fac  30653  ex-bc  30654  ex-ind-dvds  30663  4ipval2  30911  ipidsq  30913  dipcl  30915  dipcj  30917  dip0r  30920  dipcn  30923  ip1ilem  31029  ipasslem10  31042  minvecolem2  31078  minvecolem7  31086  normpar2i  31359  polid2i  31360  lnopeq0i  32210  quad3d  32951  constrresqrtcl  34074  cos9thpiminplylem1  34079  fib5  34702  fib6  34703  hgt750lemd  34942  hgt750lem  34945  hgt750lem2  34946  quad3  36020  60gcd7e1  42622  420lcm8e840  42628  lcmineqlem23  42668  3exp7  42670  3lexlogpow5ineq1  42671  3lexlogpow2ineq2  42676  aks4d1p1p4  42688  aks4d1p1p7  42691  aks4d1p1p5  42692  aks4d1p1  42693  4t5e20  42900  sq4  42902  235t711  42914  flt4lem5e  43238  inductionexd  44731  lhe4.4ex1a  44905  limclner  46225  stoweidlem13  46587  wallispi2lem1  46645  wallispi2lem2  46646  stirlinglem3  46650  stirlinglem10  46657  stirlinglem12  46659  sqwvfourb  46803  fouriersw  46805  sin5tlem1  47467  sin5tlem2  47468  sin5tlem3  47469  sin5tlem4  47470  cos5t  47473  goldratmolem2  47480  sinnpoly  47485  ceil5half3  47940  modm1p1ne  47970  fmtnorec4  48158  fmtno5lem4  48165  257prm  48170  fmtnofac1  48179  fmtno4prmfac  48181  fmtno5faclem1  48188  fmtno5faclem2  48189  139prmALT  48205  mod42tp1mod8  48211  3exp4mod41  48225  41prothprmlem1  48226  41prothprmlem2  48227  41prothprm  48228  ppivalnn4  48236  quad1  48242  8even  48335  2exp340mod341  48355  8exp8mod9  48358  mogoldbb  48407  nnsum4primeseven  48422  nnsum4primesevenALTV  48423  bgoldbtbndlem2  48428  zlmodzxzequap  49121  itsclc0yqsollem1  49384  itscnhlinecirc02plem1  49404  5m4e1  50418