Theorem 5cn 12381

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 12359	. 2 ⊢ 5 = (4 + 1)
2		4cn 12378	. . 3 ⊢ 4 ∈ ℂ
3		ax-1cn 11242	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11296	. 2 ⊢ (4 + 1) ∈ ℂ
5	1, 4	eqeltri 2840	1 ⊢ 5 ∈ ℂ

Syntax hints:   ∈ wcel 2108  (class class class)co 7448  ℂcc 11182  1c1 11185   + caddc 11187  4c4 12350  5c5 12351

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-1cn 11242  ax-addcl 11244

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-clel 2819  df-2 12356  df-3 12357  df-4 12358  df-5 12359

This theorem is referenced by:  6cn  12384  6m1e5  12424  5p2e7  12449  5p3e8  12450  5p4e9  12451  5p5e10  12829  5t2e10  12858  5recm6rec  12902  bpoly4  16107  ef01bndlem  16232  dec5dvds  17111  dec5nprm  17113  2exp11  17137  2exp16  17138  prmlem1  17155  17prm  17164  139prm  17171  163prm  17172  317prm  17173  631prm  17174  1259lem1  17178  1259lem2  17179  1259lem3  17180  1259lem4  17181  2503lem1  17184  2503lem2  17185  2503lem3  17186  4001lem1  17188  4001lem2  17189  4001lem3  17190  4001lem4  17191  4001prm  17192  log2ublem3  27009  log2ub  27010  ppiub  27266  bclbnd  27342  bposlem4  27349  bposlem5  27350  bposlem6  27351  bposlem8  27353  bposlem9  27354  lgsdir2lem1  27387  2lgslem3c  27460  2lgsoddprmlem3d  27475  ex-fac  30483  fib6  34371  hgt750lem2  34629  12lcm5e60  41965  lcmineqlem23  42008  3lexlogpow5ineq1  42011  3lexlogpow5ineq5  42017  aks4d1p1p4  42028  aks4d1p1p6  42030  aks4d1p1p7  42031  sqn5i  42274  4t5e20  42280  sq5  42282  235t711  42293  ex-decpmul  42294  inductionexd  44117  fmtno5lem1  47427  fmtno5lem2  47428  257prm  47435  fmtno4prmfac193  47447  fmtno4nprmfac193  47448  flsqrt5  47468  139prmALT  47470  127prm  47473  5tcu2e40  47489  41prothprmlem2  47492  41prothprm  47493  2exp340mod341  47607  gbpart8  47642  linevalexample  48124  ackval3012  48426  5m4e1  48891