Theorem 5cn 12245

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 12223	. 2 ⊢ 5 = (4 + 1)
2		4cn 12242	. . 3 ⊢ 4 ∈ ℂ
3		ax-1cn 11096	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11150	. 2 ⊢ (4 + 1) ∈ ℂ
5	1, 4	eqeltri 2833	1 ⊢ 5 ∈ ℂ

Syntax hints:   ∈ wcel 2114  (class class class)co 7368  ℂcc 11036  1c1 11039   + caddc 11041  4c4 12214  5c5 12215

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-1cn 11096  ax-addcl 11098

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-clel 2812  df-2 12220  df-3 12221  df-4 12222  df-5 12223

This theorem is referenced by:  6cn  12248  6m1e5  12283  5p2e7  12308  5p3e8  12309  5p4e9  12310  5p5e10  12690  5t2e10  12719  5recm6rec  12762  bpoly4  15994  ef01bndlem  16121  5ndvds3  16352  5ndvds6  16353  dec5dvds  17004  dec5nprm  17006  2exp11  17029  2exp16  17030  prmlem1  17047  17prm  17056  139prm  17063  163prm  17064  317prm  17065  631prm  17066  1259lem1  17070  1259lem2  17071  1259lem3  17072  1259lem4  17073  2503lem1  17076  2503lem2  17077  2503lem3  17078  4001lem1  17080  4001lem2  17081  4001lem3  17082  4001lem4  17083  4001prm  17084  log2ublem3  26926  log2ub  26927  ppiub  27183  bclbnd  27259  bposlem4  27266  bposlem5  27267  bposlem6  27268  bposlem8  27270  bposlem9  27271  lgsdir2lem1  27304  2lgslem3c  27377  2lgsoddprmlem3d  27392  ex-fac  30538  fib6  34583  hgt750lem2  34829  12lcm5e60  42372  lcmineqlem23  42415  3lexlogpow5ineq1  42418  3lexlogpow5ineq5  42424  aks4d1p1p4  42435  aks4d1p1p6  42437  aks4d1p1p7  42438  sqn5i  42649  4t5e20  42655  sq5  42658  235t711  42669  ex-decpmul  42670  inductionexd  44505  ceil5half3  47694  fmtno5lem1  47907  fmtno5lem2  47908  257prm  47915  fmtno4prmfac193  47927  fmtno4nprmfac193  47928  flsqrt5  47948  139prmALT  47950  127prm  47953  5tcu2e40  47969  41prothprmlem2  47972  41prothprm  47973  2exp340mod341  48087  gbpart8  48122  gpg5order  48414  linevalexample  48749  ackval3012  49046  5m4e1  50150