Theorem 7cn 12287

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 12261	. 2 ⊢ 7 = (6 + 1)
2		6cn 12284	. . 3 ⊢ 6 ∈ ℂ
3		ax-1cn 11133	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11187	. 2 ⊢ (6 + 1) ∈ ℂ
5	1, 4	eqeltri 2825	1 ⊢ 7 ∈ ℂ

Syntax hints:   ∈ wcel 2109  (class class class)co 7390  ℂcc 11073  1c1 11076   + caddc 11078  6c6 12252  7c7 12253

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-1cn 11133  ax-addcl 11135

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2722  df-clel 2804  df-2 12256  df-3 12257  df-4 12258  df-5 12259  df-6 12260  df-7 12261

This theorem is referenced by:  8cn  12290  8m1e7  12321  7p2e9  12349  7p3e10  12731  7t2e14  12765  7t4e28  12767  7t7e49  12770  cos2bnd  16163  23prm  17096  139prm  17101  163prm  17102  317prm  17103  631prm  17104  1259lem1  17108  1259lem2  17109  1259lem3  17110  1259lem4  17111  1259lem5  17112  1259prm  17113  2503lem1  17114  2503lem2  17115  2503lem3  17116  4001lem1  17118  4001lem4  17121  4001prm  17122  log2ublem3  26865  log2ub  26866  bclbnd  27198  bposlem8  27209  2lgslem3d  27317  ex-prmo  30395  hgt750lem  34649  hgt750lem2  34650  60lcm7e420  42005  3exp7  42048  3lexlogpow5ineq1  42049  aks4d1p1  42071  sq7  42291  235t711  42300  ex-decpmul  42301  3cubeslem3r  42682  fmtno5lem4  47561  257prm  47566  fmtno4nprmfac193  47579  fmtno5fac  47587  m3prm  47597  139prmALT  47601  127prm  47604  m7prm  47605  2exp340mod341  47738  8exp8mod9  47741