Theorem 5cn 12333

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 12311	. 2 ⊢ 5 = (4 + 1)
2		4cn 12330	. . 3 ⊢ 4 ∈ ℂ
3		ax-1cn 11192	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11246	. 2 ⊢ (4 + 1) ∈ ℂ
5	1, 4	eqeltri 2831	1 ⊢ 5 ∈ ℂ

Syntax hints:   ∈ wcel 2109  (class class class)co 7410  ℂcc 11132  1c1 11135   + caddc 11137  4c4 12302  5c5 12303

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708  ax-1cn 11192  ax-addcl 11194

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2728  df-clel 2810  df-2 12308  df-3 12309  df-4 12310  df-5 12311

This theorem is referenced by:  6cn  12336  6m1e5  12376  5p2e7  12401  5p3e8  12402  5p4e9  12403  5p5e10  12784  5t2e10  12813  5recm6rec  12856  bpoly4  16080  ef01bndlem  16207  5ndvds3  16437  5ndvds6  16438  dec5dvds  17089  dec5nprm  17091  2exp11  17114  2exp16  17115  prmlem1  17132  17prm  17141  139prm  17148  163prm  17149  317prm  17150  631prm  17151  1259lem1  17155  1259lem2  17156  1259lem3  17157  1259lem4  17158  2503lem1  17161  2503lem2  17162  2503lem3  17163  4001lem1  17165  4001lem2  17166  4001lem3  17167  4001lem4  17168  4001prm  17169  log2ublem3  26915  log2ub  26916  ppiub  27172  bclbnd  27248  bposlem4  27255  bposlem5  27256  bposlem6  27257  bposlem8  27259  bposlem9  27260  lgsdir2lem1  27293  2lgslem3c  27366  2lgsoddprmlem3d  27381  ex-fac  30437  fib6  34443  hgt750lem2  34689  12lcm5e60  42026  lcmineqlem23  42069  3lexlogpow5ineq1  42072  3lexlogpow5ineq5  42078  aks4d1p1p4  42089  aks4d1p1p6  42091  aks4d1p1p7  42092  sqn5i  42302  4t5e20  42308  sq5  42310  235t711  42321  ex-decpmul  42322  inductionexd  44146  ceil5half3  47336  fmtno5lem1  47534  fmtno5lem2  47535  257prm  47542  fmtno4prmfac193  47554  fmtno4nprmfac193  47555  flsqrt5  47575  139prmALT  47577  127prm  47580  5tcu2e40  47596  41prothprmlem2  47599  41prothprm  47600  2exp340mod341  47714  gbpart8  47749  gpg5order  48031  linevalexample  48338  ackval3012  48639  5m4e1  49628