Theorem 7cn 12357

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 12331	. 2 ⊢ 7 = (6 + 1)
2		6cn 12354	. . 3 ⊢ 6 ∈ ℂ
3		ax-1cn 11210	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11264	. 2 ⊢ (6 + 1) ∈ ℂ
5	1, 4	eqeltri 2834	1 ⊢ 7 ∈ ℂ

Syntax hints:   ∈ wcel 2105  (class class class)co 7430  ℂcc 11150  1c1 11153   + caddc 11155  6c6 12322  7c7 12323

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-1cn 11210  ax-addcl 11212

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-cleq 2726  df-clel 2813  df-2 12326  df-3 12327  df-4 12328  df-5 12329  df-6 12330  df-7 12331

This theorem is referenced by:  8cn  12360  8m1e7  12396  7p2e9  12424  7p3e10  12805  7t2e14  12839  7t4e28  12841  7t7e49  12844  cos2bnd  16220  23prm  17152  139prm  17157  163prm  17158  317prm  17159  631prm  17160  1259lem1  17164  1259lem2  17165  1259lem3  17166  1259lem4  17167  1259lem5  17168  1259prm  17169  2503lem1  17170  2503lem2  17171  2503lem3  17172  4001lem1  17174  4001lem4  17177  4001prm  17178  log2ublem3  27005  log2ub  27006  bclbnd  27338  bposlem8  27349  2lgslem3d  27457  ex-prmo  30487  hgt750lem  34644  hgt750lem2  34645  60lcm7e420  41991  3exp7  42034  3lexlogpow5ineq1  42035  aks4d1p1  42057  sq7  42308  235t711  42317  ex-decpmul  42318  3cubeslem3r  42674  fmtno5lem4  47480  257prm  47485  fmtno4nprmfac193  47498  fmtno5fac  47506  m3prm  47516  139prmALT  47520  127prm  47523  m7prm  47524  2exp340mod341  47657  8exp8mod9  47660