Theorem 7cn 12360

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 12334	. 2 ⊢ 7 = (6 + 1)
2		6cn 12357	. . 3 ⊢ 6 ∈ ℂ
3		ax-1cn 11213	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11267	. 2 ⊢ (6 + 1) ∈ ℂ
5	1, 4	eqeltri 2837	1 ⊢ 7 ∈ ℂ

Syntax hints:   ∈ wcel 2108  (class class class)co 7431  ℂcc 11153  1c1 11156   + caddc 11158  6c6 12325  7c7 12326

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-1cn 11213  ax-addcl 11215

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729  df-clel 2816  df-2 12329  df-3 12330  df-4 12331  df-5 12332  df-6 12333  df-7 12334

This theorem is referenced by:  8cn  12363  8m1e7  12399  7p2e9  12427  7p3e10  12808  7t2e14  12842  7t4e28  12844  7t7e49  12847  cos2bnd  16224  23prm  17156  139prm  17161  163prm  17162  317prm  17163  631prm  17164  1259lem1  17168  1259lem2  17169  1259lem3  17170  1259lem4  17171  1259lem5  17172  1259prm  17173  2503lem1  17174  2503lem2  17175  2503lem3  17176  4001lem1  17178  4001lem4  17181  4001prm  17182  log2ublem3  26991  log2ub  26992  bclbnd  27324  bposlem8  27335  2lgslem3d  27443  ex-prmo  30478  hgt750lem  34666  hgt750lem2  34667  60lcm7e420  42011  3exp7  42054  3lexlogpow5ineq1  42055  aks4d1p1  42077  sq7  42330  235t711  42339  ex-decpmul  42340  3cubeslem3r  42698  fmtno5lem4  47543  257prm  47548  fmtno4nprmfac193  47561  fmtno5fac  47569  m3prm  47579  139prmALT  47583  127prm  47586  m7prm  47587  2exp340mod341  47720  8exp8mod9  47723