Theorem 4cn 12321

Description: The number 4 is a complex number. (Contributed by David A. Wheeler, 7-Jul-2016.) Reduce dependencies on axioms. (Revised by Steven Nguyen, 4-Oct-2022.)

Assertion

Ref	Expression
4cn	⊢ 4 ∈ ℂ

Proof of Theorem 4cn

Step	Hyp	Ref	Expression
1		df-4 12300	. 2 ⊢ 4 = (3 + 1)
2		3cn 12317	. . 3 ⊢ 3 ∈ ℂ
3		ax-1cn 11153	. . 3 ⊢ 1 ∈ ℂ
4	2, 3	addcli 11210	. 2 ⊢ (3 + 1) ∈ ℂ
5	1, 4	eqeltri 2859	1 ⊢ 4 ∈ ℂ

Syntax hints:   ∈ wcel 2143  (class class class)co 7410  ℂcc 11093  1c1 11096   + caddc 11098  3c3 12291  4c4 12292

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-1cn 11153  ax-addcl 11155

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-clel 2838  df-2 12298  df-3 12299  df-4 12300

This theorem is referenced by:  5cn  12324  5m1e4  12365  4p2e6  12388  4p3e7  12389  4p4e8  12390  4t2e8  12404  2t4e8  12405  4div2e2  12407  8th4div3  12459  div4p1lem1div2  12494  5p5e10  12782  4t4e16  12810  6t5e30  12818  fldiv4p1lem1div2  13864  sq4e2t8  14231  discr  14272  sqoddm1div8  14275  4bc2eq6  14361  bpoly3  16107  bpoly4  16108  cos2bnd  16239  flodddiv4  16468  6gcd4e2  16591  6lcm4e12  16669  pythagtriplem1  16871  2exp11  17144  13prm  17171  43prm  17177  83prm  17178  163prm  17180  317prm  17181  631prm  17182  1259lem1  17186  1259lem2  17187  1259lem3  17188  1259lem4  17189  1259lem5  17190  1259prm  17191  2503lem1  17192  2503lem2  17193  2503lem3  17194  2503prm  17195  4001lem1  17196  4001lem2  17197  4001lem3  17198  4001lem4  17199  4001prm  17200  cphipval2  25400  4cphipval2  25401  minveclem2  25585  minveclem3  25588  minveclem7  25594  uniioombl  25748  dveflem  26138  sincosq4sgn  26666  tan4thpi  26679  sincos6thpi  26681  ang180lem2  26975  heron  27003  quad2  27004  quad  27005  dcubic2  27009  dcubic  27011  mcubic  27012  cubic2  27013  cubic  27014  dquartlem1  27016  dquartlem2  27017  dquart  27018  quart1cl  27019  quart1lem  27020  quart1  27021  quartlem1  27022  quartlem2  27023  quartlem4  27025  quart  27026  log2cnv  27109  log2tlbnd  27110  log2ublem3  27113  log2ub  27114  bclbnd  27444  bposlem8  27455  bposlem9  27456  2lgslem3a  27560  2lgslem3b  27561  2lgslem3c  27562  2lgslem3d  27563  2lgsoddprmlem2  27573  2lgsoddprmlem3c  27576  2lgsoddprmlem3d  27577  addsqnreup  27607  addsq2nreurex  27608  pntibndlem2  27755  pntlemb  27761  ex-opab  30783  ex-exp  30801  ex-fac  30802  ex-bc  30803  ex-ind-dvds  30812  4ipval2  31060  ipidsq  31062  dipcl  31064  dipcj  31066  dip0r  31069  dipcn  31072  ip1ilem  31178  ipasslem10  31191  minvecolem2  31227  minvecolem7  31235  normpar2i  31508  polid2i  31509  lnopeq0i  32359  quad3d  33094  constrresqrtcl  34167  cos9thpiminplylem1  34172  fib5  34795  fib6  34796  hgt750lemd  35035  hgt750lem  35038  hgt750lem2  35039  quad3  36162  60gcd7e1  42792  420lcm8e840  42798  lcmineqlem23  42838  3exp7  42840  3lexlogpow5ineq1  42841  3lexlogpow2ineq2  42846  aks4d1p1p4  42858  aks4d1p1p7  42861  aks4d1p1p5  42862  aks4d1p1  42863  25or6to4  42993  4t5e20  43072  sq4  43074  235t711  43086  flt4lem5e  43408  inductionexd  44901  lhe4.4ex1a  45059  limclner  46385  stoweidlem13  46747  wallispi2lem1  46805  wallispi2lem2  46806  stirlinglem3  46810  stirlinglem10  46817  stirlinglem12  46819  sqwvfourb  46963  fouriersw  46965  sin5tlem1  47630  sin5tlem2  47631  sin5tlem3  47632  sin5tlem4  47633  cos5t  47636  goldratmolem2  47643  sinnpoly  47648  ceil5half3  48103  modm1p1ne  48133  fmtnorec4  48321  fmtno5lem4  48328  257prm  48333  fmtnofac1  48342  fmtno4prmfac  48344  fmtno5faclem1  48351  fmtno5faclem2  48352  139prmALT  48368  mod42tp1mod8  48374  3exp4mod41  48388  41prothprmlem1  48389  41prothprmlem2  48390  41prothprm  48391  ppivalnn4  48399  quad1  48405  8even  48498  2exp340mod341  48518  mogoldbb  48570  nnsum4primeseven  48585  nnsum4primesevenALTV  48586  bgoldbtbndlem2  48591  zlmodzxzequap  49299  itsclc0yqsollem1  49562  itscnhlinecirc02plem1  49582  5m4e1  50637