Theorem 5cn 12320

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 12297	. 2 ⊢ 5 = (4 + 1)
2		4cn 12317	. . 3 ⊢ 4 ∈ ℂ
3		ax-1cn 11146	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11203	. 2 ⊢ (4 + 1) ∈ ℂ
5	1, 4	eqeltri 2861	1 ⊢ 5 ∈ ℂ

Syntax hints:   ∈ wcel 2145  (class class class)co 7400  ℂcc 11086  1c1 11089   + caddc 11091  4c4 12288  5c5 12289

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737  ax-1cn 11146  ax-addcl 11148

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-cleq 2757  df-clel 2840  df-2 12294  df-3 12295  df-4 12296  df-5 12297

This theorem is referenced by:  6cn  12323  6m1e5  12362  5p2e7  12387  5p3e8  12388  5p4e9  12389  5p5e10  12778  5t2e10  12807  5recm6rec  12852  bpoly4  16103  ef01bndlem  16230  5ndvds3  16461  5ndvds6  16462  dec5dvds  17114  dec5nprm  17116  2exp11  17139  2exp16  17140  prmlem1  17157  17prm  17167  139prm  17174  163prm  17175  317prm  17176  631prm  17177  1259lem1  17181  1259lem2  17182  1259lem3  17183  1259lem4  17184  2503lem1  17187  2503lem2  17188  2503lem3  17189  4001lem1  17191  4001lem2  17192  4001lem3  17193  4001lem4  17194  4001prm  17195  log2ublem3  27071  log2ub  27072  ppiub  27326  bclbnd  27402  bposlem4  27409  bposlem5  27410  bposlem6  27411  bposlem8  27413  bposlem9  27414  lgsdir2lem1  27447  2lgslem3c  27520  2lgsoddprmlem3d  27535  ex-fac  30711  fib6  34713  hgt750lem2  34956  12lcm5e60  42637  lcmineqlem23  42680  3lexlogpow5ineq1  42683  3lexlogpow5ineq5  42689  aks4d1p1p4  42700  aks4d1p1p6  42702  aks4d1p1p7  42703  sqn5i  42906  4t5e20  42912  sq5  42915  235t711  42926  ex-decpmul  42927  inductionexd  44743  cos5t  47471  goldrasin  47474  goldracos5teq  47477  goldratmolem2  47478  ceil5half3  47938  fmtno5lem1  48160  fmtno5lem2  48161  257prm  48168  fmtno4prmfac193  48180  fmtno4nprmfac193  48181  flsqrt5  48201  139prmALT  48203  127prm  48206  5tcu2e40  48222  41prothprmlem2  48225  41prothprm  48226  2exp340mod341  48353  gbpart8  48388  gpg5order  48680  linevalexample  49026  ackval3012  49323  5m4e1  50426