Theorem 7cn 12214

Description: The number 7 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
7cn	⊢ 7 ∈ ℂ

Proof of Theorem 7cn

Step	Hyp	Ref	Expression
1		df-7 12188	. 2 ⊢ 7 = (6 + 1)
2		6cn 12211	. . 3 ⊢ 6 ∈ ℂ
3		ax-1cn 11059	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11113	. 2 ⊢ (6 + 1) ∈ ℂ
5	1, 4	eqeltri 2827	1 ⊢ 7 ∈ ℂ

Syntax hints:   ∈ wcel 2111  (class class class)co 7341  ℂcc 10999  1c1 11002   + caddc 11004  6c6 12179  7c7 12180

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-1cn 11059  ax-addcl 11061

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723  df-clel 2806  df-2 12183  df-3 12184  df-4 12185  df-5 12186  df-6 12187  df-7 12188

This theorem is referenced by:  8cn  12217  8m1e7  12248  7p2e9  12276  7p3e10  12658  7t2e14  12692  7t4e28  12694  7t7e49  12697  cos2bnd  16092  23prm  17025  139prm  17030  163prm  17031  317prm  17032  631prm  17033  1259lem1  17037  1259lem2  17038  1259lem3  17039  1259lem4  17040  1259lem5  17041  1259prm  17042  2503lem1  17043  2503lem2  17044  2503lem3  17045  4001lem1  17047  4001lem4  17050  4001prm  17051  log2ublem3  26880  log2ub  26881  bclbnd  27213  bposlem8  27224  2lgslem3d  27332  ex-prmo  30431  hgt750lem  34656  hgt750lem2  34657  60lcm7e420  42043  3exp7  42086  3lexlogpow5ineq1  42087  aks4d1p1  42109  sq7  42329  235t711  42338  ex-decpmul  42339  3cubeslem3r  42720  fmtno5lem4  47587  257prm  47592  fmtno4nprmfac193  47605  fmtno5fac  47613  m3prm  47623  139prmALT  47627  127prm  47630  m7prm  47631  2exp340mod341  47764  8exp8mod9  47767