Theorem 5cn 11465

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 11441	. 2 ⊢ 5 = (4 + 1)
2		4cn 11461	. . 3 ⊢ 4 ∈ ℂ
3		ax-1cn 10330	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 10383	. 2 ⊢ (4 + 1) ∈ ℂ
5	1, 4	eqeltri 2855	1 ⊢ 5 ∈ ℂ

Syntax hints:   ∈ wcel 2107  (class class class)co 6922  ℂcc 10270  1c1 10273   + caddc 10275  4c4 11432  5c5 11433

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-ext 2754  ax-1cn 10330  ax-addcl 10332

This theorem depends on definitions:  df-bi 199  df-an 387  df-ex 1824  df-cleq 2770  df-clel 2774  df-2 11438  df-3 11439  df-4 11440  df-5 11441

This theorem is referenced by:  6cn  11469  6m1e5  11513  5p2e7  11538  5p3e8  11539  5p4e9  11540  5p5e10  11918  5t2e10  11947  5recm6rec  11991  bpoly4  15192  ef01bndlem  15316  dec5dvds  16172  dec5nprm  16174  2exp16  16196  prmlem1  16213  17prm  16222  139prm  16229  163prm  16230  317prm  16231  631prm  16232  1259lem1  16236  1259lem2  16237  1259lem3  16238  1259lem4  16239  2503lem1  16242  2503lem2  16243  2503lem3  16244  4001lem1  16246  4001lem2  16247  4001lem3  16248  4001lem4  16249  4001prm  16250  log2ublem3  25127  log2ub  25128  ppiublem2  25380  ppiub  25381  bclbnd  25457  bposlem4  25464  bposlem5  25465  bposlem6  25466  bposlem8  25468  bposlem9  25469  lgsdir2lem1  25502  2lgslem3c  25575  2lgsoddprmlem3d  25590  ex-fac  27883  fib6  31067  hgt750lem2  31332  sqn5i  38153  235t711  38159  ex-decpmul  38160  inductionexd  39413  fmtno5lem1  42490  fmtno5lem2  42491  257prm  42498  fmtno4prmfac193  42510  fmtno4nprmfac193  42511  flsqrt5  42534  139prmALT  42536  127prm  42540  2exp11  42542  5tcu2e40  42557  41prothprmlem2  42560  41prothprm  42561  gbpart8  42685  linevalexample  43203  5m4e1  43653