Theorem 4cn 12353

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 12332	. 2 ⊢ 4 = (3 + 1)
2		3cn 12349	. . 3 ⊢ 3 ∈ ℂ
3		ax-1cn 11185	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11242	. 2 ⊢ (3 + 1) ∈ ℂ
5	1, 4	eqeltri 2856	1 ⊢ 4 ∈ ℂ

This proof depends on syntax axioms:   ∈ wcel 2145  (class class class)co 7414  ℂcc 11125  1c1 11128   + caddc 11130  3c3 12323  4c4 12324

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 2732  ax-1cn 11185  ax-addcl 11187

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2752  df-clel 2835  df-2 12330  df-3 12331  df-4 12332

This theorem is used by:  5cn  12356  5m1e4  12397  4p2e6  12420  4p3e7  12421  4p4e8  12422  4t2e8  12436  2t4e8  12437  4div2e2  12439  8th4div3  12491  div4p1lem1div2  12526  5p5e10  12815  4t4e16  12843  6t5e30  12851  fldiv4p1lem1div2  13899  sq4e2t8  14266  discr  14307  sqoddm1div8  14310  4bc2eq6  14396  bpoly3  16147  bpoly4  16148  cos2bnd  16279  flodddiv4  16508  6gcd4e2  16631  6lcm4e12  16709  pythagtriplem1  16911  2exp11  17184  13prm  17211  43prm  17217  83prm  17218  163prm  17220  317prm  17221  631prm  17222  1259lem1  17226  1259lem2  17227  1259lem3  17228  1259lem4  17229  1259lem5  17230  1259prm  17231  2503lem1  17232  2503lem2  17233  2503lem3  17234  2503prm  17235  4001lem1  17236  4001lem2  17237  4001lem3  17238  4001lem4  17239  4001prm  17240  cphipval2  25472  4cphipval2  25473  minveclem2  25657  minveclem3  25660  minveclem7  25666  uniioombl  25820  dveflem  26209  sincosq4sgn  26742  tan4thpi  26755  sincos6thpi  26756  ang180lem2  27050  heron  27078  quad2  27079  quad  27080  dcubic2  27084  dcubic  27086  mcubic  27087  cubic2  27088  cubic  27089  dquartlem1  27091  dquartlem2  27092  dquart  27093  quart1cl  27094  quart1lem  27095  quart1  27096  quartlem1  27097  quartlem2  27098  quartlem4  27100  quart  27101  log2cnv  27184  log2tlbnd  27185  log2ublem3  27188  log2ub  27189  bclbnd  27519  bposlem8  27530  bposlem9  27531  2lgslem3a  27635  2lgslem3b  27636  2lgslem3c  27637  2lgslem3d  27638  2lgsoddprmlem2  27648  2lgsoddprmlem3c  27651  2lgsoddprmlem3d  27652  addsqnreup  27682  addsq2nreurex  27683  pntibndlem2  27830  pntlemb  27836  ex-opab  30915  ex-exp  30933  ex-fac  30934  ex-bc  30935  ex-ind-dvds  30944  4ipval2  31192  ipidsq  31194  dipcl  31196  dipcj  31198  dip0r  31201  dipcn  31204  ip1ilem  31310  ipasslem10  31323  minvecolem2  31359  minvecolem7  31367  normpar2i  31640  polid2i  31641  lnopeq0i  32491  quad3d  33223  constrresqrtcl  34290  cos9thpiminplylem1  34295  fib5  34919  fib6  34920  hgt750lemd  35159  hgt750lem  35162  hgt750lem2  35163  quad3  36252  60gcd7e1  42874  420lcm8e840  42880  lcmineqlem23  42920  3exp7  42922  3lexlogpow5ineq1  42923  3lexlogpow2ineq2  42928  aks4d1p1p4  42940  aks4d1p1p7  42943  aks4d1p1p5  42944  aks4d1p1  42945  25or6to4  43075  4p4e8ALT  43128  1p5e6  43131  2p6e8  43138  4p5e9  43143  4t5e20  43169  sq4  43171  235t711  43183  flt4lem5e  43505  inductionexd  44998  lhe4.4ex1a  45156  limclner  46482  stoweidlem13  46844  wallispi2lem1  46902  wallispi2lem2  46903  stirlinglem3  46907  stirlinglem10  46914  stirlinglem12  46916  sqwvfourb  47060  fouriersw  47062  sin5tlem1  47740  sin5tlem2  47741  sin5tlem3  47742  sin5tlem4  47743  cos5t  47746  goldpolyfactor  47748  goldratmolem2  47754  goldratval  47757  sinnpoly  47762  ceil5half3  48237  modm1p1ne  48267  fmtnorec4  48455  fmtno5lem4  48462  257prm  48467  fmtnofac1  48476  fmtno4prmfac  48478  fmtno5faclem1  48485  fmtno5faclem2  48486  139prmALT  48502  mod42tp1mod8  48508  3exp4mod41  48522  41prothprmlem1  48523  41prothprmlem2  48524  41prothprm  48525  ppivalnn4  48533  quad1  48539  8even  48632  2exp340mod341  48652  mogoldbb  48704  nnsum4primeseven  48719  nnsum4primesevenALTV  48720  bgoldbtbndlem2  48725  zlmodzxzequap  49432  itsclc0yqsollem1  49695  itscnhlinecirc02plem1  49715  5m4e1  50771