Theorem 4cn 12354

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 12333	. 2 ⊢ 4 = (3 + 1)
2		3cn 12350	. . 3 ⊢ 3 ∈ ℂ
3		ax-1cn 11186	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11243	. 2 ⊢ (3 + 1) ∈ ℂ
5	1, 4	eqeltri 2858	1 ⊢ 4 ∈ ℂ

This proof depends on syntax axioms:   ∈ wcel 2145  (class class class)co 7417  ℂcc 11126  1c1 11129   + caddc 11131  3c3 12324  4c4 12325

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734  ax-1cn 11186  ax-addcl 11188

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2754  df-clel 2837  df-2 12331  df-3 12332  df-4 12333

This theorem is used by:  5cn  12357  5m1e4  12398  4p2e6  12421  4p3e7  12422  4p4e8  12423  4t2e8  12437  2t4e8  12438  4div2e2  12440  8th4div3  12492  div4p1lem1div2  12527  5p5e10  12816  4t4e16  12844  6t5e30  12852  fldiv4p1lem1div2  13900  sq4e2t8  14267  discr  14308  sqoddm1div8  14311  4bc2eq6  14397  bpoly3  16150  bpoly4  16151  cos2bnd  16282  flodddiv4  16511  6gcd4e2  16634  6lcm4e12  16712  pythagtriplem1  16914  2exp11  17187  13prm  17214  43prm  17220  83prm  17221  163prm  17223  317prm  17224  631prm  17225  1259lem1  17229  1259lem2  17230  1259lem3  17231  1259lem4  17232  1259lem5  17233  1259prm  17234  2503lem1  17235  2503lem2  17236  2503lem3  17237  2503prm  17238  4001lem1  17239  4001lem2  17240  4001lem3  17241  4001lem4  17242  4001prm  17243  cphipval2  25475  4cphipval2  25476  minveclem2  25660  minveclem3  25663  minveclem7  25669  uniioombl  25823  dveflem  26213  sincosq4sgn  26746  tan4thpi  26759  sincos6thpi  26761  ang180lem2  27055  heron  27083  quad2  27084  quad  27085  dcubic2  27089  dcubic  27091  mcubic  27092  cubic2  27093  cubic  27094  dquartlem1  27096  dquartlem2  27097  dquart  27098  quart1cl  27099  quart1lem  27100  quart1  27101  quartlem1  27102  quartlem2  27103  quartlem4  27105  quart  27106  log2cnv  27189  log2tlbnd  27190  log2ublem3  27193  log2ub  27194  bclbnd  27524  bposlem8  27535  bposlem9  27536  2lgslem3a  27640  2lgslem3b  27641  2lgslem3c  27642  2lgslem3d  27643  2lgsoddprmlem2  27653  2lgsoddprmlem3c  27656  2lgsoddprmlem3d  27657  addsqnreup  27687  addsq2nreurex  27688  pntibndlem2  27835  pntlemb  27841  ex-opab  30920  ex-exp  30938  ex-fac  30939  ex-bc  30940  ex-ind-dvds  30949  4ipval2  31197  ipidsq  31199  dipcl  31201  dipcj  31203  dip0r  31206  dipcn  31209  ip1ilem  31315  ipasslem10  31328  minvecolem2  31364  minvecolem7  31372  normpar2i  31645  polid2i  31646  lnopeq0i  32496  quad3d  33228  constrresqrtcl  34295  cos9thpiminplylem1  34300  fib5  34924  fib6  34925  hgt750lemd  35164  hgt750lem  35167  hgt750lem2  35168  quad3  36257  60gcd7e1  42879  420lcm8e840  42885  lcmineqlem23  42925  3exp7  42927  3lexlogpow5ineq1  42928  3lexlogpow2ineq2  42933  aks4d1p1p4  42945  aks4d1p1p7  42948  aks4d1p1p5  42949  aks4d1p1  42950  25or6to4  43080  4p4e8ALT  43133  1p5e6  43136  2p6e8  43143  4p5e9  43148  4t5e20  43174  sq4  43176  235t711  43188  flt4lem5e  43510  inductionexd  45003  lhe4.4ex1a  45161  limclner  46487  stoweidlem13  46849  wallispi2lem1  46907  wallispi2lem2  46908  stirlinglem3  46912  stirlinglem10  46919  stirlinglem12  46921  sqwvfourb  47065  fouriersw  47067  sin5tlem1  47745  sin5tlem2  47746  sin5tlem3  47747  sin5tlem4  47748  cos5t  47751  goldpolyfactor  47753  goldratmolem2  47759  goldratval  47762  sinnpoly  47767  ceil5half3  48242  modm1p1ne  48272  fmtnorec4  48460  fmtno5lem4  48467  257prm  48472  fmtnofac1  48481  fmtno4prmfac  48483  fmtno5faclem1  48490  fmtno5faclem2  48491  139prmALT  48507  mod42tp1mod8  48513  3exp4mod41  48527  41prothprmlem1  48528  41prothprmlem2  48529  41prothprm  48530  ppivalnn4  48538  quad1  48544  8even  48637  2exp340mod341  48657  mogoldbb  48709  nnsum4primeseven  48724  nnsum4primesevenALTV  48725  bgoldbtbndlem2  48730  zlmodzxzequap  49437  itsclc0yqsollem1  49700  itscnhlinecirc02plem1  49720  5m4e1  50776