Theorem 4cn 11710

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 11690	. 2 ⊢ 4 = (3 + 1)
2		3cn 11706	. . 3 ⊢ 3 ∈ ℂ
3		ax-1cn 10584	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 10636	. 2 ⊢ (3 + 1) ∈ ℂ
5	1, 4	eqeltri 2886	1 ⊢ 4 ∈ ℂ

Syntax hints:   ∈ wcel 2111  (class class class)co 7135  ℂcc 10524  1c1 10527   + caddc 10529  3c3 11681  4c4 11682

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770  ax-1cn 10584  ax-addcl 10586

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2791  df-clel 2870  df-2 11688  df-3 11689  df-4 11690

This theorem is referenced by:  5cn  11713  5m1e4  11755  4p2e6  11778  4p3e7  11779  4p4e8  11780  4t2e8  11793  4d2e2  11795  8th4div3  11845  div4p1lem1div2  11880  5p5e10  12157  4t4e16  12185  6t5e30  12193  fldiv4p1lem1div2  13200  sq4e2t8  13558  discr  13597  sqoddm1div8  13600  4bc2eq6  13685  bpoly3  15404  bpoly4  15405  cos2bnd  15533  flodddiv4  15754  6gcd4e2  15876  6lcm4e12  15950  pythagtriplem1  16143  13prm  16441  43prm  16447  163prm  16450  317prm  16451  631prm  16452  1259lem1  16456  1259lem2  16457  1259lem3  16458  1259lem4  16459  1259lem5  16460  1259prm  16461  2503lem1  16462  2503lem2  16463  2503lem3  16464  2503prm  16465  4001lem1  16466  4001lem2  16467  4001lem3  16468  4001lem4  16469  4001prm  16470  cphipval2  23845  4cphipval2  23846  minveclem2  24030  minveclem3  24033  minveclem7  24039  uniioombl  24193  dveflem  24582  sincosq4sgn  25094  sincos6thpi  25108  ang180lem2  25396  heron  25424  quad2  25425  quad  25426  dcubic2  25430  dcubic  25432  mcubic  25433  cubic2  25434  cubic  25435  dquartlem1  25437  dquartlem2  25438  dquart  25439  quart1cl  25440  quart1lem  25441  quart1  25442  quartlem1  25443  quartlem2  25444  quartlem4  25446  quart  25447  log2cnv  25530  log2tlbnd  25531  log2ublem3  25534  log2ub  25535  bclbnd  25864  bposlem8  25875  bposlem9  25876  2lgslem3a  25980  2lgslem3b  25981  2lgslem3c  25982  2lgslem3d  25983  2lgsoddprmlem2  25993  2lgsoddprmlem3c  25996  2lgsoddprmlem3d  25997  addsqnreup  26027  addsq2nreurex  26028  pntibndlem2  26175  pntlemb  26181  ex-opab  28217  ex-exp  28235  ex-fac  28236  ex-bc  28237  ex-ind-dvds  28246  4ipval2  28491  ipidsq  28493  dipcl  28495  dipcj  28497  dip0r  28500  dipcn  28503  ip1ilem  28609  ipasslem10  28622  minvecolem2  28658  minvecolem7  28666  normpar2i  28939  polid2i  28940  lnopeq0i  29790  fib5  31773  fib6  31774  hgt750lemd  32029  hgt750lem  32032  hgt750lem2  32033  quad3  33026  60gcd7e1  39293  420lcm8e840  39299  lcmineqlem23  39339  3lexlogpow5ineq1  39341  235t711  39485  inductionexd  40858  lhe4.4ex1a  41033  limclner  42293  stoweidlem13  42655  wallispi2lem1  42713  wallispi2lem2  42714  stirlinglem3  42718  stirlinglem10  42725  stirlinglem12  42727  sqwvfourb  42871  fouriersw  42873  fmtnorec4  44066  fmtno5lem4  44073  257prm  44078  fmtnofac1  44087  fmtno4prmfac  44089  fmtno5faclem1  44096  fmtno5faclem2  44097  139prmALT  44113  2exp11  44118  mod42tp1mod8  44120  3exp4mod41  44134  41prothprmlem1  44135  41prothprmlem2  44136  41prothprm  44137  quad1  44138  8even  44231  2exp340mod341  44251  8exp8mod9  44254  mogoldbb  44303  nnsum4primeseven  44318  nnsum4primesevenALTV  44319  bgoldbtbndlem2  44324  zlmodzxzequap  44908  itsclc0yqsollem1  45176  itscnhlinecirc02plem1  45196  5m4e1  45325