Theorem 5cn 12330

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 12308	. 2 ⊢ 5 = (4 + 1)
2		4cn 12327	. . 3 ⊢ 4 ∈ ℂ
3		ax-1cn 11196	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11250	. 2 ⊢ (4 + 1) ∈ ℂ
5	1, 4	eqeltri 2821	1 ⊢ 5 ∈ ℂ

Syntax hints:   ∈ wcel 2098  (class class class)co 7417  ℂcc 11136  1c1 11139   + caddc 11141  4c4 12299  5c5 12300

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696  ax-1cn 11196  ax-addcl 11198

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-cleq 2717  df-clel 2802  df-2 12305  df-3 12306  df-4 12307  df-5 12308

This theorem is referenced by:  6cn  12333  6m1e5  12373  5p2e7  12398  5p3e8  12399  5p4e9  12400  5p5e10  12778  5t2e10  12807  5recm6rec  12851  bpoly4  16035  ef01bndlem  16160  dec5dvds  17032  dec5nprm  17034  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  26910  log2ub  26911  ppiub  27167  bclbnd  27243  bposlem4  27250  bposlem5  27251  bposlem6  27252  bposlem8  27254  bposlem9  27255  lgsdir2lem1  27288  2lgslem3c  27361  2lgsoddprmlem3d  27376  ex-fac  30317  fib6  34096  hgt750lem2  34354  12lcm5e60  41548  lcmineqlem23  41591  3lexlogpow5ineq1  41594  3lexlogpow5ineq5  41600  aks4d1p1p4  41611  aks4d1p1p6  41613  aks4d1p1p7  41614  sqn5i  41924  4t5e20  41930  235t711  41932  ex-decpmul  41933  inductionexd  43650  fmtno5lem1  46956  fmtno5lem2  46957  257prm  46964  fmtno4prmfac193  46976  fmtno4nprmfac193  46977  flsqrt5  46997  139prmALT  46999  127prm  47002  5tcu2e40  47018  41prothprmlem2  47021  41prothprm  47022  2exp340mod341  47136  gbpart8  47171  linevalexample  47575  ackval3012  47877  5m4e1  48342