Theorem 7cn 12330

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 12304	. 2 ⊢ 7 = (6 + 1)
2		6cn 12327	. . 3 ⊢ 6 ∈ ℂ
3		ax-1cn 11190	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11244	. 2 ⊢ (6 + 1) ∈ ℂ
5	1, 4	eqeltri 2824	1 ⊢ 7 ∈ ℂ

Syntax hints:   ∈ wcel 2099  (class class class)co 7414  ℂcc 11130  1c1 11133   + caddc 11135  6c6 12295  7c7 12296

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2698  ax-1cn 11190  ax-addcl 11192

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1775  df-cleq 2719  df-clel 2805  df-2 12299  df-3 12300  df-4 12301  df-5 12302  df-6 12303  df-7 12304

This theorem is referenced by:  8cn  12333  8m1e7  12369  7p2e9  12397  7p3e10  12776  7t2e14  12810  7t4e28  12812  7t7e49  12815  cos2bnd  16158  23prm  17081  139prm  17086  163prm  17087  317prm  17088  631prm  17089  1259lem1  17093  1259lem2  17094  1259lem3  17095  1259lem4  17096  1259lem5  17097  1259prm  17098  2503lem1  17099  2503lem2  17100  2503lem3  17101  4001lem1  17103  4001lem4  17106  4001prm  17107  log2ublem3  26873  log2ub  26874  bclbnd  27206  bposlem8  27217  2lgslem3d  27325  ex-prmo  30262  hgt750lem  34273  hgt750lem2  34274  60lcm7e420  41470  3exp7  41513  3lexlogpow5ineq1  41514  aks4d1p1  41536  235t711  41839  ex-decpmul  41840  3cubeslem3r  42079  fmtno5lem4  46868  257prm  46873  fmtno4nprmfac193  46886  fmtno5fac  46894  m3prm  46904  139prmALT  46908  127prm  46911  m7prm  46912  2exp340mod341  47045  8exp8mod9  47048