Theorem 7cn 12303

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 12277	. 2 ⊢ 7 = (6 + 1)
2		6cn 12300	. . 3 ⊢ 6 ∈ ℂ
3		ax-1cn 11164	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11217	. 2 ⊢ (6 + 1) ∈ ℂ
5	1, 4	eqeltri 2821	1 ⊢ 7 ∈ ℂ

Syntax hints:   ∈ wcel 2098  (class class class)co 7401  ℂcc 11104  1c1 11107   + caddc 11109  6c6 12268  7c7 12269

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2695  ax-1cn 11164  ax-addcl 11166

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1774  df-cleq 2716  df-clel 2802  df-2 12272  df-3 12273  df-4 12274  df-5 12275  df-6 12276  df-7 12277

This theorem is referenced by:  8cn  12306  8m1e7  12342  7p2e9  12370  7p3e10  12749  7t2e14  12783  7t4e28  12785  7t7e49  12788  cos2bnd  16128  23prm  17051  139prm  17056  163prm  17057  317prm  17058  631prm  17059  1259lem1  17063  1259lem2  17064  1259lem3  17065  1259lem4  17066  1259lem5  17067  1259prm  17068  2503lem1  17069  2503lem2  17070  2503lem3  17071  4001lem1  17073  4001lem4  17076  4001prm  17077  log2ublem3  26796  log2ub  26797  bclbnd  27129  bposlem8  27140  2lgslem3d  27248  ex-prmo  30181  hgt750lem  34152  hgt750lem2  34153  60lcm7e420  41368  3exp7  41411  3lexlogpow5ineq1  41412  aks4d1p1  41434  235t711  41694  ex-decpmul  41695  3cubeslem3r  41914  fmtno5lem4  46709  257prm  46714  fmtno4nprmfac193  46727  fmtno5fac  46735  m3prm  46745  139prmALT  46749  127prm  46752  m7prm  46753  2exp340mod341  46886  8exp8mod9  46889