Theorem 5cn 12234

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 12212	. 2 ⊢ 5 = (4 + 1)
2		4cn 12231	. . 3 ⊢ 4 ∈ ℂ
3		ax-1cn 11086	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11140	. 2 ⊢ (4 + 1) ∈ ℂ
5	1, 4	eqeltri 2824	1 ⊢ 5 ∈ ℂ

Syntax hints:   ∈ wcel 2109  (class class class)co 7353  ℂcc 11026  1c1 11029   + caddc 11031  4c4 12203  5c5 12204

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 2701  ax-1cn 11086  ax-addcl 11088

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-clel 2803  df-2 12209  df-3 12210  df-4 12211  df-5 12212

This theorem is referenced by:  6cn  12237  6m1e5  12272  5p2e7  12297  5p3e8  12298  5p4e9  12299  5p5e10  12680  5t2e10  12709  5recm6rec  12752  bpoly4  15984  ef01bndlem  16111  5ndvds3  16342  5ndvds6  16343  dec5dvds  16994  dec5nprm  16996  2exp11  17019  2exp16  17020  prmlem1  17037  17prm  17046  139prm  17053  163prm  17054  317prm  17055  631prm  17056  1259lem1  17060  1259lem2  17061  1259lem3  17062  1259lem4  17063  2503lem1  17066  2503lem2  17067  2503lem3  17068  4001lem1  17070  4001lem2  17071  4001lem3  17072  4001lem4  17073  4001prm  17074  log2ublem3  26874  log2ub  26875  ppiub  27131  bclbnd  27207  bposlem4  27214  bposlem5  27215  bposlem6  27216  bposlem8  27218  bposlem9  27219  lgsdir2lem1  27252  2lgslem3c  27325  2lgsoddprmlem3d  27340  ex-fac  30413  fib6  34373  hgt750lem2  34619  12lcm5e60  41981  lcmineqlem23  42024  3lexlogpow5ineq1  42027  3lexlogpow5ineq5  42033  aks4d1p1p4  42044  aks4d1p1p6  42046  aks4d1p1p7  42047  sqn5i  42258  4t5e20  42264  sq5  42267  235t711  42278  ex-decpmul  42279  inductionexd  44128  ceil5half3  47325  fmtno5lem1  47538  fmtno5lem2  47539  257prm  47546  fmtno4prmfac193  47558  fmtno4nprmfac193  47559  flsqrt5  47579  139prmALT  47581  127prm  47584  5tcu2e40  47600  41prothprmlem2  47603  41prothprm  47604  2exp340mod341  47718  gbpart8  47753  gpg5order  48045  linevalexample  48381  ackval3012  48678  5m4e1  49783