Theorem 5cn 12267

Description: The number 5 is a complex number. (Contributed by David A. Wheeler, 8-Dec-2018.) Reduce dependencies on axioms. (Revised by Steven Nguyen, 4-Oct-2022.)

Assertion

Ref	Expression
5cn	⊢ 5 ∈ ℂ

Proof of Theorem 5cn

Step	Hyp	Ref	Expression
1		df-5 12245	. 2 ⊢ 5 = (4 + 1)
2		4cn 12264	. . 3 ⊢ 4 ∈ ℂ
3		ax-1cn 11094	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11149	. 2 ⊢ (4 + 1) ∈ ℂ
5	1, 4	eqeltri 2836	1 ⊢ 5 ∈ ℂ

Syntax hints:   ∈ wcel 2119  (class class class)co 7363  ℂcc 11034  1c1 11037   + caddc 11039  4c4 12236  5c5 12237

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712  ax-1cn 11094  ax-addcl 11096

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2732  df-clel 2815  df-2 12242  df-3 12243  df-4 12244  df-5 12245

This theorem is referenced by:  6cn  12270  6m1e5  12305  5p2e7  12330  5p3e8  12331  5p4e9  12332  5p5e10  12713  5t2e10  12742  5recm6rec  12785  bpoly4  16022  ef01bndlem  16149  5ndvds3  16380  5ndvds6  16381  dec5dvds  17033  dec5nprm  17035  2exp11  17058  2exp16  17059  prmlem1  17076  17prm  17085  139prm  17092  163prm  17093  317prm  17094  631prm  17095  1259lem1  17099  1259lem2  17100  1259lem3  17101  1259lem4  17102  2503lem1  17105  2503lem2  17106  2503lem3  17107  4001lem1  17109  4001lem2  17110  4001lem3  17111  4001lem4  17112  4001prm  17113  log2ublem3  26937  log2ub  26938  ppiub  27192  bclbnd  27268  bposlem4  27275  bposlem5  27276  bposlem6  27277  bposlem8  27279  bposlem9  27280  lgsdir2lem1  27313  2lgslem3c  27386  2lgsoddprmlem3d  27401  ex-fac  30546  fib6  34597  hgt750lem2  34843  12lcm5e60  42500  lcmineqlem23  42543  3lexlogpow5ineq1  42546  3lexlogpow5ineq5  42552  aks4d1p1p4  42563  aks4d1p1p6  42565  aks4d1p1p7  42566  sqn5i  42769  4t5e20  42775  sq5  42778  235t711  42789  ex-decpmul  42790  inductionexd  44606  cos5t  47349  goldrasin  47352  goldracos5teq  47355  goldratmolem2  47356  ceil5half3  47816  fmtno5lem1  48038  fmtno5lem2  48039  257prm  48046  fmtno4prmfac193  48058  fmtno4nprmfac193  48059  flsqrt5  48079  139prmALT  48081  127prm  48084  5tcu2e40  48100  41prothprmlem2  48103  41prothprm  48104  2exp340mod341  48231  gbpart8  48266  gpg5order  48558  linevalexample  48893  ackval3012  49190  5m4e1  50294