Theorem 7cn 12477

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 12450	. 2 ⊢ 7 = (6 + 1)
2		6cn 12474	. . 3 ⊢ 6 ∈ ℂ
3		ax-1cn 11297	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11354	. 2 ⊢ (6 + 1) ∈ ℂ
5	1, 4	eqeltri 2860	1 ⊢ 7 ∈ ℂ

This proof depends on syntax axioms:   ∈ wcel 2147  (class class class)co 7451  ℂcc 11237  1c1 11240   + caddc 11242  6c6 12441  7c7 12442

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-1cn 11297  ax-addcl 11299

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2755  df-clel 2839  df-2 12445  df-3 12446  df-4 12447  df-5 12448  df-6 12449  df-7 12450

This theorem is used by:  8cn  12480  8m1e7  12515  7p2e9  12543  7p3e10  12934  7t2e14  12968  7t4e28  12970  7t7e49  12973  cos2bnd  16400  23prm  17341  83prm  17345  139prm  17346  163prm  17347  317prm  17348  631prm  17349  1259lem1  17353  1259lem2  17354  1259lem3  17355  1259lem4  17356  1259lem5  17357  1259prm  17358  2503lem1  17359  2503lem2  17360  2503lem3  17361  4001lem1  17363  4001lem4  17366  4001prm  17367  log2ublem3  27333  log2ub  27334  bclbnd  27664  bposlem8  27675  2lgslem3d  27783  ex-prmo  31117  hgt750lem  35391  hgt750lem2  35392  60lcm7e420  43326  3exp7  43369  3lexlogpow5ineq1  43370  aks4d1p1  43392  25or6to4  43522  1p8e9  43581  sq7  43619  235t711  43628  ex-decpmul  43629  3cubeslem3r  43963  fmtno5lem4  48914  257prm  48919  fmtno4nprmfac193  48932  fmtno5fac  48940  m3prm  48950  139prmALT  48954  127prm  48957  m7prm  48958  ppivalnn4  48985  2exp340mod341  49104  8exp8mod9  49107