Axiom ax-1cn 8018

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

Assertion

Ref	Expression
ax-1cn	|- 1 e. CC

Detailed syntax breakdown of Axiom ax-1cn

Step	Hyp	Ref	Expression
1		c1 7926	. 2 class 1
2		cc 7923	. 2 class CC
3	1, 2	wcel 2176	1 wff 1 e. CC

This axiom is referenced by:  0cn  8064  1ex  8067  mulrid  8069  mullid  8070  1cnd  8088  muladd11  8205  1p1times  8206  peano2cn  8207  peano2cnm  8338  0reALT  8369  pncan1  8449  npcan1  8450  kcnktkm1cn  8455  ine0  8466  mulm1  8472  mulsubfacd  8491  ixi  8656  inelr  8657  muleqadd  8741  recclap  8752  recap0  8758  recidap  8759  recidap2  8760  div1  8776  1div1e1  8777  diveqap1  8778  recdivap  8791  divdivap1  8796  divdivap2  8797  recdivap2  8798  conjmulap  8802  eqneg  8805  div2negap  8808  recreclt  8973  ofnegsub  9035  nn1m1nn  9054  nn1suc  9055  nnaddcl  9056  nnmulcl  9057  nnsub  9075  1m1e0  9105  neg1cn  9141  neg1ne0  9143  neg1ap0  9145  negneg1e1  9146  1pneg1e0  9147  1m0e1  9149  0p1e1  9150  1p0e1  9152  2m1e1  9154  3m1e2  9156  4m1e3  9157  5m1e4  9158  6m1e5  9159  7m1e6  9160  8m1e7  9161  9m1e8  9162  2p2e4  9163  1p2e3  9171  3p2e5  9178  3p3e6  9179  4p2e6  9180  4p3e7  9181  4p4e8  9182  5p2e7  9183  5p3e8  9184  5p4e9  9185  6p2e8  9186  6p3e9  9187  7p2e9  9188  1t1e1  9189  3t3e9  9194  neg1mulneg1e1  9249  1mhlfehlf  9255  8th4div3  9256  halfpm6th  9257  addltmul  9274  elnn0nn  9337  peano2z  9408  zlem1lt  9429  zltlem1  9430  nnaddm1cl  9434  elz2  9444  zextlt  9465  zeo  9478  peano5uzti  9481  numsuc  9517  numltc  9529  numsucc  9543  numaddc  9551  6p5lem  9573  5p5e10  9574  6p4e10  9575  7p3e10  9578  8p2e10  9583  10m1e9  9599  4t3lem  9600  7t4e28  9614  9t11e99  9633  decbin2  9644  halfthird  9646  5recm6rec  9647  uzp1  9682  peano2uzr  9706  uzaddcl  9707  qreccl  9763  iccf1o  10126  fz01en  10175  fztp  10200  fzsuc2  10201  fztpval  10205  fseq1m1p1  10217  elfzp1b  10219  fz0to4untppr  10246  fzoss2  10296  fzval3  10333  fzosplitsnm1  10338  fzo0to42pr  10349  fzosplitprm1  10363  fldiv4p1lem1div2  10448  flqdiv  10466  frecfzen2  10572  nn0ennn  10578  xnn0nnen  10582  seq3m1  10618  seqshft2g  10627  monoord2  10631  ser3mono  10632  seqf1oglem1  10664  seqf1oglem2  10665  expcl  10702  m1expcl2  10706  expclzaplem  10708  expm1t  10712  1exp  10713  mulexpzap  10724  expadd  10726  expaddzap  10728  expmul  10729  expubnd  10741  neg1sqe1  10779  irec  10784  i4  10787  binom21  10797  bernneq  10805  bernneq2  10806  facndiv  10884  faclbnd6  10889  bcnp1n  10904  bcm1k  10905  bcp1nk  10907  bcn2  10909  bcp1m1  10910  bcpasc  10911  4bc3eq4  10918  hashfz  10966  hashfzo  10967  seq3coll  10987  swrds1  11121  swrdlsw  11122  rei  11210  imi  11211  caucvgrelemrec  11290  recan  11420  iserex  11650  serf0  11663  fsumm1  11727  fsump1  11731  telfsumo  11777  fsumparts  11781  hashiun  11789  binomlem  11794  binom  11795  binom1p  11796  binom11  11797  binom1dif  11798  bcxmas  11800  isumsplit  11802  isum1p  11803  arisum  11809  arisum2  11810  trireciplem  11811  geosergap  11817  geolim  11822  geolim2  11823  georeclim  11824  geo2sum  11825  geo2sum2  11826  0.999...  11832  geoihalfsum  11833  mertenslemi1  11846  mertenslem2  11847  mertensabs  11848  prodf1  11853  prodfclim1  11855  prodrbdclem  11882  fproddccvg  11883  prodmodclem2a  11887  fprodntrivap  11895  prodssdc  11900  fprodssdc  11901  esum  11973  ege2le3  11982  efexp  11993  efzval  11994  eftlub  12001  effsumlt  12003  ef4p  12005  tanval3ap  12025  efi4p  12028  tan0  12042  efival  12043  tanaddap  12050  cos2t  12061  cos2tsin  12062  ef01bndlem  12067  cos1bnd  12070  cos2bnd  12071  demoivreALT  12085  eirraplem  12088  3dvds  12175  3dvdsdec  12176  3dvds2dec  12177  odd2np1lem  12183  odd2np1  12184  opoe  12206  omoe  12207  opeo  12208  omeo  12209  m1exp1  12212  n2dvdsm1  12224  flodddiv4  12247  bitsfzo  12266  gcdmultiple  12341  sqgcd  12350  nn0seqcvgd  12363  prmind2  12442  hashdvds  12543  phiprmpw  12544  phiprm  12545  eulerthlemth  12554  sumhashdc  12670  fldivp1  12671  prmpwdvds  12678  pockthlem  12679  pockthi  12681  4sqlem11  12724  4sqlem19  12732  dec5nprm  12737  mulgnndir  13487  mulgneg2  13492  cnfld1  14334  zsssubrg  14347  mulgrhm2  14372  expcncf  15081  divcncfap  15086  hovercncf  15118  dvid  15167  dvidre  15169  dvexp  15183  dvexp2  15184  dveflem  15198  plyaddlem1  15219  plymullem1  15220  dvply1  15237  reeff1olem  15243  eulerid  15274  cos2pi  15276  sincosq3sgn  15300  sincosq4sgn  15301  cosq23lt0  15305  tangtx  15310  sincos4thpi  15312  sincos6thpi  15314  pigt3  15316  abssinper  15318  coskpi  15320  cosq34lt1  15322  logdivlti  15353  rpcxpp1  15378  rpcxpsqrt  15394  rprelogbdiv  15429  binom4  15451  wilthlem1  15452  0sgm  15457  1sgmprm  15466  1sgm2ppw  15467  mersenne  15469  perfect1  15470  perfectlem1  15471  perfectlem2  15472  perfect  15473  zabsle1  15476  lgslem1  15477  lgslem2  15478  lgsfcl2  15483  lgsvalmod  15496  lgsneg  15501  lgsdilem  15504  lgsdir2lem1  15505  lgsdir2lem2  15506  lgsdir2lem3  15507  lgsdir2lem5  15509  lgsne0  15515  lgseisenlem1  15547  lgseisenlem2  15548  lgseisen  15551  lgsquadlem1  15554  lgsquadlem2  15555  lgsquad2lem1  15558  lgsquad2  15560  m1lgs  15562  2lgslem3c  15572  2lgsoddprmlem3c  15586  2lgsoddprmlem3d  15587  2sqlem10  15602  ex-fl  15661  trilpolemeq1  15979