Theorem 7cn 11725

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 11699	. 2 ⊢ 7 = (6 + 1)
2		6cn 11722	. . 3 ⊢ 6 ∈ ℂ
3		ax-1cn 10589	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 10641	. 2 ⊢ (6 + 1) ∈ ℂ
5	1, 4	eqeltri 2909	1 ⊢ 7 ∈ ℂ

Syntax hints:   ∈ wcel 2110  (class class class)co 7150  ℂcc 10529  1c1 10532   + caddc 10534  6c6 11690  7c7 11691

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-ext 2793  ax-1cn 10589  ax-addcl 10591

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-cleq 2814  df-clel 2893  df-2 11694  df-3 11695  df-4 11696  df-5 11697  df-6 11698  df-7 11699

This theorem is referenced by:  8cn  11728  8m1e7  11764  7p2e9  11792  7p3e10  12167  7t2e14  12201  7t4e28  12203  7t7e49  12206  cos2bnd  15535  23prm  16446  139prm  16451  163prm  16452  317prm  16453  631prm  16454  1259lem1  16458  1259lem2  16459  1259lem3  16460  1259lem4  16461  1259lem5  16462  1259prm  16463  2503lem1  16464  2503lem2  16465  2503lem3  16466  4001lem1  16468  4001lem4  16471  4001prm  16472  log2ublem3  25520  log2ub  25521  bclbnd  25850  bposlem8  25861  2lgslem3d  25969  ex-prmo  28232  hgt750lem  31917  hgt750lem2  31918  235t711  39170  ex-decpmul  39171  3cubeslem3r  39277  fmtno5lem4  43712  257prm  43717  fmtno4nprmfac193  43730  fmtno5fac  43738  m3prm  43748  139prmALT  43753  127prm  43757  m7prm  43758  2exp340mod341  43892  8exp8mod9  43895