Theorem 5cn 12303

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 12280	. 2 ⊢ 5 = (4 + 1)
2		4cn 12300	. . 3 ⊢ 4 ∈ ℂ
3		ax-1cn 11128	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11185	. 2 ⊢ (4 + 1) ∈ ℂ
5	1, 4	eqeltri 2857	1 ⊢ 5 ∈ ℂ

Syntax hints:   ∈ wcel 2141  (class class class)co 7392  ℂcc 11068  1c1 11071   + caddc 11073  4c4 12271  5c5 12272

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-1cn 11128  ax-addcl 11130

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-cleq 2753  df-clel 2836  df-2 12277  df-3 12278  df-4 12279  df-5 12280

This theorem is referenced by:  6cn  12306  6m1e5  12345  5p2e7  12370  5p3e8  12371  5p4e9  12372  5p5e10  12761  5t2e10  12790  5recm6rec  12835  bpoly4  16072  ef01bndlem  16199  5ndvds3  16430  5ndvds6  16431  dec5dvds  17083  dec5nprm  17085  2exp11  17108  2exp16  17109  prmlem1  17126  17prm  17136  139prm  17143  163prm  17144  317prm  17145  631prm  17146  1259lem1  17150  1259lem2  17151  1259lem3  17152  1259lem4  17153  2503lem1  17156  2503lem2  17157  2503lem3  17158  4001lem1  17160  4001lem2  17161  4001lem3  17162  4001lem4  17163  4001prm  17164  log2ublem3  26990  log2ub  26991  ppiub  27245  bclbnd  27321  bposlem4  27328  bposlem5  27329  bposlem6  27330  bposlem8  27332  bposlem9  27333  lgsdir2lem1  27366  2lgslem3c  27439  2lgsoddprmlem3d  27454  ex-fac  30599  fib6  34664  hgt750lem2  34910  12lcm5e60  42589  lcmineqlem23  42632  3lexlogpow5ineq1  42635  3lexlogpow5ineq5  42641  aks4d1p1p4  42652  aks4d1p1p6  42654  aks4d1p1p7  42655  sqn5i  42858  4t5e20  42864  sq5  42867  235t711  42878  ex-decpmul  42879  inductionexd  44695  cos5t  47437  goldrasin  47440  goldracos5teq  47443  goldratmolem2  47444  ceil5half3  47904  fmtno5lem1  48126  fmtno5lem2  48127  257prm  48134  fmtno4prmfac193  48146  fmtno4nprmfac193  48147  flsqrt5  48167  139prmALT  48169  127prm  48172  5tcu2e40  48188  41prothprmlem2  48191  41prothprm  48192  2exp340mod341  48319  gbpart8  48354  gpg5order  48646  linevalexample  48981  ackval3012  49278  5m4e1  50382