Theorem 5cn 12210

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 12188	. 2 ⊢ 5 = (4 + 1)
2		4cn 12207	. . 3 ⊢ 4 ∈ ℂ
3		ax-1cn 11061	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11115	. 2 ⊢ (4 + 1) ∈ ℂ
5	1, 4	eqeltri 2827	1 ⊢ 5 ∈ ℂ

Syntax hints:   ∈ wcel 2111  (class class class)co 7346  ℂcc 11001  1c1 11004   + caddc 11006  4c4 12179  5c5 12180

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-1cn 11061  ax-addcl 11063

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723  df-clel 2806  df-2 12185  df-3 12186  df-4 12187  df-5 12188

This theorem is referenced by:  6cn  12213  6m1e5  12248  5p2e7  12273  5p3e8  12274  5p4e9  12275  5p5e10  12656  5t2e10  12685  5recm6rec  12728  bpoly4  15963  ef01bndlem  16090  5ndvds3  16321  5ndvds6  16322  dec5dvds  16973  dec5nprm  16975  2exp11  16998  2exp16  16999  prmlem1  17016  17prm  17025  139prm  17032  163prm  17033  317prm  17034  631prm  17035  1259lem1  17039  1259lem2  17040  1259lem3  17041  1259lem4  17042  2503lem1  17045  2503lem2  17046  2503lem3  17047  4001lem1  17049  4001lem2  17050  4001lem3  17051  4001lem4  17052  4001prm  17053  log2ublem3  26883  log2ub  26884  ppiub  27140  bclbnd  27216  bposlem4  27223  bposlem5  27224  bposlem6  27225  bposlem8  27227  bposlem9  27228  lgsdir2lem1  27261  2lgslem3c  27334  2lgsoddprmlem3d  27349  ex-fac  30426  fib6  34414  hgt750lem2  34660  12lcm5e60  42040  lcmineqlem23  42083  3lexlogpow5ineq1  42086  3lexlogpow5ineq5  42092  aks4d1p1p4  42103  aks4d1p1p6  42105  aks4d1p1p7  42106  sqn5i  42317  4t5e20  42323  sq5  42326  235t711  42337  ex-decpmul  42338  inductionexd  44187  ceil5half3  47370  fmtno5lem1  47583  fmtno5lem2  47584  257prm  47591  fmtno4prmfac193  47603  fmtno4nprmfac193  47604  flsqrt5  47624  139prmALT  47626  127prm  47629  5tcu2e40  47645  41prothprmlem2  47648  41prothprm  47649  2exp340mod341  47763  gbpart8  47798  gpg5order  48090  linevalexample  48426  ackval3012  48723  5m4e1  49828