Axiom ax-1cn 7991

Description: 1 is a complex number. Axiom for real and complex numbers, justified by Theorem ax1cn 7947. (Contributed by NM, 1-Mar-1995.)

Assertion

Ref	Expression
ax-1cn	⊢ 1 ∈ ℂ

Detailed syntax breakdown of Axiom ax-1cn

Step	Hyp	Ref	Expression
1		c1 7899	. 2 class 1
2		cc 7896	. 2 class ℂ
3	1, 2	wcel 2167	1 wff 1 ∈ ℂ

This axiom is referenced by:  0cn  8037  1ex  8040  mulrid  8042  mullid  8043  1cnd  8061  muladd11  8178  1p1times  8179  peano2cn  8180  peano2cnm  8311  0reALT  8342  pncan1  8422  npcan1  8423  kcnktkm1cn  8428  ine0  8439  mulm1  8445  mulsubfacd  8464  ixi  8629  inelr  8630  muleqadd  8714  recclap  8725  recap0  8731  recidap  8732  recidap2  8733  div1  8749  1div1e1  8750  diveqap1  8751  recdivap  8764  divdivap1  8769  divdivap2  8770  recdivap2  8771  conjmulap  8775  eqneg  8778  div2negap  8781  recreclt  8946  ofnegsub  9008  nn1m1nn  9027  nn1suc  9028  nnaddcl  9029  nnmulcl  9030  nnsub  9048  1m1e0  9078  neg1cn  9114  neg1ne0  9116  neg1ap0  9118  negneg1e1  9119  1pneg1e0  9120  1m0e1  9122  0p1e1  9123  1p0e1  9125  2m1e1  9127  3m1e2  9129  4m1e3  9130  5m1e4  9131  6m1e5  9132  7m1e6  9133  8m1e7  9134  9m1e8  9135  2p2e4  9136  1p2e3  9144  3p2e5  9151  3p3e6  9152  4p2e6  9153  4p3e7  9154  4p4e8  9155  5p2e7  9156  5p3e8  9157  5p4e9  9158  6p2e8  9159  6p3e9  9160  7p2e9  9161  1t1e1  9162  3t3e9  9167  neg1mulneg1e1  9222  1mhlfehlf  9228  8th4div3  9229  halfpm6th  9230  addltmul  9247  elnn0nn  9310  peano2z  9381  zlem1lt  9401  zltlem1  9402  nnaddm1cl  9406  elz2  9416  zextlt  9437  zeo  9450  peano5uzti  9453  numsuc  9489  numltc  9501  numsucc  9515  numaddc  9523  6p5lem  9545  5p5e10  9546  6p4e10  9547  7p3e10  9550  8p2e10  9555  10m1e9  9571  4t3lem  9572  7t4e28  9586  9t11e99  9605  decbin2  9616  halfthird  9618  5recm6rec  9619  uzp1  9654  peano2uzr  9678  uzaddcl  9679  qreccl  9735  iccf1o  10098  fz01en  10147  fztp  10172  fzsuc2  10173  fztpval  10177  fseq1m1p1  10189  elfzp1b  10191  fz0to4untppr  10218  fzoss2  10267  fzval3  10299  fzosplitsnm1  10304  fzo0to42pr  10315  fzosplitprm1  10329  fldiv4p1lem1div2  10414  flqdiv  10432  frecfzen2  10538  nn0ennn  10544  xnn0nnen  10548  seq3m1  10584  seqshft2g  10593  monoord2  10597  ser3mono  10598  seqf1oglem1  10630  seqf1oglem2  10631  expcl  10668  m1expcl2  10672  expclzaplem  10674  expm1t  10678  1exp  10679  mulexpzap  10690  expadd  10692  expaddzap  10694  expmul  10695  expubnd  10707  neg1sqe1  10745  irec  10750  i4  10753  binom21  10763  bernneq  10771  bernneq2  10772  facndiv  10850  faclbnd6  10855  bcnp1n  10870  bcm1k  10871  bcp1nk  10873  bcn2  10875  bcp1m1  10876  bcpasc  10877  4bc3eq4  10884  hashfz  10932  hashfzo  10933  seq3coll  10953  rei  11083  imi  11084  caucvgrelemrec  11163  recan  11293  iserex  11523  serf0  11536  fsumm1  11600  fsump1  11604  telfsumo  11650  fsumparts  11654  hashiun  11662  binomlem  11667  binom  11668  binom1p  11669  binom11  11670  binom1dif  11671  bcxmas  11673  isumsplit  11675  isum1p  11676  arisum  11682  arisum2  11683  trireciplem  11684  geosergap  11690  geolim  11695  geolim2  11696  georeclim  11697  geo2sum  11698  geo2sum2  11699  0.999...  11705  geoihalfsum  11706  mertenslemi1  11719  mertenslem2  11720  mertensabs  11721  prodf1  11726  prodfclim1  11728  prodrbdclem  11755  fproddccvg  11756  prodmodclem2a  11760  fprodntrivap  11768  prodssdc  11773  fprodssdc  11774  esum  11846  ege2le3  11855  efexp  11866  efzval  11867  eftlub  11874  effsumlt  11876  ef4p  11878  tanval3ap  11898  efi4p  11901  tan0  11915  efival  11916  tanaddap  11923  cos2t  11934  cos2tsin  11935  ef01bndlem  11940  cos1bnd  11943  cos2bnd  11944  demoivreALT  11958  eirraplem  11961  3dvds  12048  3dvdsdec  12049  3dvds2dec  12050  odd2np1lem  12056  odd2np1  12057  opoe  12079  omoe  12080  opeo  12081  omeo  12082  m1exp1  12085  n2dvdsm1  12097  flodddiv4  12120  bitsfzo  12139  gcdmultiple  12214  sqgcd  12223  nn0seqcvgd  12236  prmind2  12315  hashdvds  12416  phiprmpw  12417  phiprm  12418  eulerthlemth  12427  sumhashdc  12543  fldivp1  12544  prmpwdvds  12551  pockthlem  12552  pockthi  12554  4sqlem11  12597  4sqlem19  12605  dec5nprm  12610  mulgnndir  13359  mulgneg2  13364  cnfld1  14206  zsssubrg  14219  mulgrhm2  14244  expcncf  14953  divcncfap  14958  hovercncf  14990  dvid  15039  dvidre  15041  dvexp  15055  dvexp2  15056  dveflem  15070  plyaddlem1  15091  plymullem1  15092  dvply1  15109  reeff1olem  15115  eulerid  15146  cos2pi  15148  sincosq3sgn  15172  sincosq4sgn  15173  cosq23lt0  15177  tangtx  15182  sincos4thpi  15184  sincos6thpi  15186  pigt3  15188  abssinper  15190  coskpi  15192  cosq34lt1  15194  logdivlti  15225  rpcxpp1  15250  rpcxpsqrt  15266  rprelogbdiv  15301  binom4  15323  wilthlem1  15324  0sgm  15329  1sgmprm  15338  1sgm2ppw  15339  mersenne  15341  perfect1  15342  perfectlem1  15343  perfectlem2  15344  perfect  15345  zabsle1  15348  lgslem1  15349  lgslem2  15350  lgsfcl2  15355  lgsvalmod  15368  lgsneg  15373  lgsdilem  15376  lgsdir2lem1  15377  lgsdir2lem2  15378  lgsdir2lem3  15379  lgsdir2lem5  15381  lgsne0  15387  lgseisenlem1  15419  lgseisenlem2  15420  lgseisen  15423  lgsquadlem1  15426  lgsquadlem2  15427  lgsquad2lem1  15430  lgsquad2  15432  m1lgs  15434  2lgslem3c  15444  2lgsoddprmlem3c  15458  2lgsoddprmlem3d  15459  2sqlem10  15474  ex-fl  15479  trilpolemeq1  15797