Theorem 7cn 12230

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 12204	. 2 ⊢ 7 = (6 + 1)
2		6cn 12227	. . 3 ⊢ 6 ∈ ℂ
3		ax-1cn 11075	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11129	. 2 ⊢ (6 + 1) ∈ ℂ
5	1, 4	eqeltri 2829	1 ⊢ 7 ∈ ℂ

Syntax hints:   ∈ wcel 2113  (class class class)co 7355  ℂcc 11015  1c1 11018   + caddc 11020  6c6 12195  7c7 12196

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 2115  ax-9 2123  ax-ext 2705  ax-1cn 11075  ax-addcl 11077

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2725  df-clel 2808  df-2 12199  df-3 12200  df-4 12201  df-5 12202  df-6 12203  df-7 12204

This theorem is referenced by:  8cn  12233  8m1e7  12264  7p2e9  12292  7p3e10  12673  7t2e14  12707  7t4e28  12709  7t7e49  12712  cos2bnd  16104  23prm  17037  139prm  17042  163prm  17043  317prm  17044  631prm  17045  1259lem1  17049  1259lem2  17050  1259lem3  17051  1259lem4  17052  1259lem5  17053  1259prm  17054  2503lem1  17055  2503lem2  17056  2503lem3  17057  4001lem1  17059  4001lem4  17062  4001prm  17063  log2ublem3  26905  log2ub  26906  bclbnd  27238  bposlem8  27249  2lgslem3d  27357  ex-prmo  30460  hgt750lem  34736  hgt750lem2  34737  60lcm7e420  42176  3exp7  42219  3lexlogpow5ineq1  42220  aks4d1p1  42242  sq7  42466  235t711  42475  ex-decpmul  42476  3cubeslem3r  42844  fmtno5lem4  47718  257prm  47723  fmtno4nprmfac193  47736  fmtno5fac  47744  m3prm  47754  139prmALT  47758  127prm  47761  m7prm  47762  2exp340mod341  47895  8exp8mod9  47898