Theorem 5cn 12233

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 12211	. 2 ⊢ 5 = (4 + 1)
2		4cn 12230	. . 3 ⊢ 4 ∈ ℂ
3		ax-1cn 11084	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11138	. 2 ⊢ (4 + 1) ∈ ℂ
5	1, 4	eqeltri 2832	1 ⊢ 5 ∈ ℂ

Syntax hints:   ∈ wcel 2113  (class class class)co 7358  ℂcc 11024  1c1 11027   + caddc 11029  4c4 12202  5c5 12203

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 2115  ax-9 2123  ax-ext 2708  ax-1cn 11084  ax-addcl 11086

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2728  df-clel 2811  df-2 12208  df-3 12209  df-4 12210  df-5 12211

This theorem is referenced by:  6cn  12236  6m1e5  12271  5p2e7  12296  5p3e8  12297  5p4e9  12298  5p5e10  12678  5t2e10  12707  5recm6rec  12750  bpoly4  15982  ef01bndlem  16109  5ndvds3  16340  5ndvds6  16341  dec5dvds  16992  dec5nprm  16994  2exp11  17017  2exp16  17018  prmlem1  17035  17prm  17044  139prm  17051  163prm  17052  317prm  17053  631prm  17054  1259lem1  17058  1259lem2  17059  1259lem3  17060  1259lem4  17061  2503lem1  17064  2503lem2  17065  2503lem3  17066  4001lem1  17068  4001lem2  17069  4001lem3  17070  4001lem4  17071  4001prm  17072  log2ublem3  26914  log2ub  26915  ppiub  27171  bclbnd  27247  bposlem4  27254  bposlem5  27255  bposlem6  27256  bposlem8  27258  bposlem9  27259  lgsdir2lem1  27292  2lgslem3c  27365  2lgsoddprmlem3d  27380  ex-fac  30526  fib6  34563  hgt750lem2  34809  12lcm5e60  42258  lcmineqlem23  42301  3lexlogpow5ineq1  42304  3lexlogpow5ineq5  42310  aks4d1p1p4  42321  aks4d1p1p6  42323  aks4d1p1p7  42324  sqn5i  42536  4t5e20  42542  sq5  42545  235t711  42556  ex-decpmul  42557  inductionexd  44392  ceil5half3  47582  fmtno5lem1  47795  fmtno5lem2  47796  257prm  47803  fmtno4prmfac193  47815  fmtno4nprmfac193  47816  flsqrt5  47836  139prmALT  47838  127prm  47841  5tcu2e40  47857  41prothprmlem2  47860  41prothprm  47861  2exp340mod341  47975  gbpart8  48010  gpg5order  48302  linevalexample  48637  ackval3012  48934  5m4e1  50038