Theorem 5cn 12281

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 12259	. 2 ⊢ 5 = (4 + 1)
2		4cn 12278	. . 3 ⊢ 4 ∈ ℂ
3		ax-1cn 11133	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11187	. 2 ⊢ (4 + 1) ∈ ℂ
5	1, 4	eqeltri 2825	1 ⊢ 5 ∈ ℂ

Syntax hints:   ∈ wcel 2109  (class class class)co 7390  ℂcc 11073  1c1 11076   + caddc 11078  4c4 12250  5c5 12251

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 2702  ax-1cn 11133  ax-addcl 11135

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2722  df-clel 2804  df-2 12256  df-3 12257  df-4 12258  df-5 12259

This theorem is referenced by:  6cn  12284  6m1e5  12319  5p2e7  12344  5p3e8  12345  5p4e9  12346  5p5e10  12727  5t2e10  12756  5recm6rec  12799  bpoly4  16032  ef01bndlem  16159  5ndvds3  16390  5ndvds6  16391  dec5dvds  17042  dec5nprm  17044  2exp11  17067  2exp16  17068  prmlem1  17085  17prm  17094  139prm  17101  163prm  17102  317prm  17103  631prm  17104  1259lem1  17108  1259lem2  17109  1259lem3  17110  1259lem4  17111  2503lem1  17114  2503lem2  17115  2503lem3  17116  4001lem1  17118  4001lem2  17119  4001lem3  17120  4001lem4  17121  4001prm  17122  log2ublem3  26865  log2ub  26866  ppiub  27122  bclbnd  27198  bposlem4  27205  bposlem5  27206  bposlem6  27207  bposlem8  27209  bposlem9  27210  lgsdir2lem1  27243  2lgslem3c  27316  2lgsoddprmlem3d  27331  ex-fac  30387  fib6  34404  hgt750lem2  34650  12lcm5e60  42003  lcmineqlem23  42046  3lexlogpow5ineq1  42049  3lexlogpow5ineq5  42055  aks4d1p1p4  42066  aks4d1p1p6  42068  aks4d1p1p7  42069  sqn5i  42280  4t5e20  42286  sq5  42289  235t711  42300  ex-decpmul  42301  inductionexd  44151  ceil5half3  47345  fmtno5lem1  47558  fmtno5lem2  47559  257prm  47566  fmtno4prmfac193  47578  fmtno4nprmfac193  47579  flsqrt5  47599  139prmALT  47601  127prm  47604  5tcu2e40  47620  41prothprmlem2  47623  41prothprm  47624  2exp340mod341  47738  gbpart8  47773  gpg5order  48055  linevalexample  48388  ackval3012  48685  5m4e1  49790