Axiom ax-1cn 8088

Description: 1 is a complex number. Axiom for real and complex numbers, justified by Theorem ax1cn 8044. (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 7996	. 2 class 1
2		cc 7993	. 2 class CC
3	1, 2	wcel 2200	1 wff 1 e. CC

This axiom is referenced by:  0cn  8134  1ex  8137  mulrid  8139  mullid  8140  1cnd  8158  muladd11  8275  1p1times  8276  peano2cn  8277  peano2cnm  8408  0reALT  8439  pncan1  8519  npcan1  8520  kcnktkm1cn  8525  ine0  8536  mulm1  8542  mulsubfacd  8561  ixi  8726  inelr  8727  muleqadd  8811  recclap  8822  recap0  8828  recidap  8829  recidap2  8830  div1  8846  1div1e1  8847  diveqap1  8848  recdivap  8861  divdivap1  8866  divdivap2  8867  recdivap2  8868  conjmulap  8872  eqneg  8875  div2negap  8878  recreclt  9043  ofnegsub  9105  nn1m1nn  9124  nn1suc  9125  nnaddcl  9126  nnmulcl  9127  nnsub  9145  1m1e0  9175  neg1cn  9211  neg1ne0  9213  neg1ap0  9215  negneg1e1  9216  1pneg1e0  9217  1m0e1  9219  0p1e1  9220  1p0e1  9222  2m1e1  9224  3m1e2  9226  4m1e3  9227  5m1e4  9228  6m1e5  9229  7m1e6  9230  8m1e7  9231  9m1e8  9232  2p2e4  9233  1p2e3  9241  3p2e5  9248  3p3e6  9249  4p2e6  9250  4p3e7  9251  4p4e8  9252  5p2e7  9253  5p3e8  9254  5p4e9  9255  6p2e8  9256  6p3e9  9257  7p2e9  9258  1t1e1  9259  3t3e9  9264  neg1mulneg1e1  9319  1mhlfehlf  9325  8th4div3  9326  halfpm6th  9327  addltmul  9344  elnn0nn  9407  peano2z  9478  zlem1lt  9499  zltlem1  9500  nnaddm1cl  9504  elz2  9514  zextlt  9535  zeo  9548  peano5uzti  9551  numsuc  9587  numltc  9599  numsucc  9613  numaddc  9621  6p5lem  9643  5p5e10  9644  6p4e10  9645  7p3e10  9648  8p2e10  9653  10m1e9  9669  4t3lem  9670  7t4e28  9684  9t11e99  9703  decbin2  9714  halfthird  9716  5recm6rec  9717  uzp1  9752  peano2uzr  9776  uzaddcl  9777  qreccl  9833  iccf1o  10196  fz01en  10245  fztp  10270  fzsuc2  10271  fztpval  10275  fseq1m1p1  10287  elfzp1b  10289  fz0to4untppr  10316  fzoss2  10366  fzval3  10405  fzosplitsnm1  10410  fzo0to42pr  10421  fzosplitprm1  10435  fldiv4p1lem1div2  10520  flqdiv  10538  frecfzen2  10644  nn0ennn  10650  xnn0nnen  10654  seq3m1  10690  seqshft2g  10699  monoord2  10703  ser3mono  10704  seqf1oglem1  10736  seqf1oglem2  10737  expcl  10774  m1expcl2  10778  expclzaplem  10780  expm1t  10784  1exp  10785  mulexpzap  10796  expadd  10798  expaddzap  10800  expmul  10801  expubnd  10813  neg1sqe1  10851  irec  10856  i4  10859  binom21  10869  bernneq  10877  bernneq2  10878  facndiv  10956  faclbnd6  10961  bcnp1n  10976  bcm1k  10977  bcp1nk  10979  bcn2  10981  bcp1m1  10982  bcpasc  10983  4bc3eq4  10990  hashfz  11038  hashfzo  11039  seq3coll  11059  swrds1  11195  swrdlsw  11196  wrdind  11249  wrd2ind  11250  rei  11405  imi  11406  caucvgrelemrec  11485  recan  11615  iserex  11845  serf0  11858  fsumm1  11922  fsump1  11926  telfsumo  11972  fsumparts  11976  hashiun  11984  binomlem  11989  binom  11990  binom1p  11991  binom11  11992  binom1dif  11993  bcxmas  11995  isumsplit  11997  isum1p  11998  arisum  12004  arisum2  12005  trireciplem  12006  geosergap  12012  geolim  12017  geolim2  12018  georeclim  12019  geo2sum  12020  geo2sum2  12021  0.999...  12027  geoihalfsum  12028  mertenslemi1  12041  mertenslem2  12042  mertensabs  12043  prodf1  12048  prodfclim1  12050  prodrbdclem  12077  fproddccvg  12078  prodmodclem2a  12082  fprodntrivap  12090  prodssdc  12095  fprodssdc  12096  esum  12168  ege2le3  12177  efexp  12188  efzval  12189  eftlub  12196  effsumlt  12198  ef4p  12200  tanval3ap  12220  efi4p  12223  tan0  12237  efival  12238  tanaddap  12245  cos2t  12256  cos2tsin  12257  ef01bndlem  12262  cos1bnd  12265  cos2bnd  12266  demoivreALT  12280  eirraplem  12283  3dvds  12370  3dvdsdec  12371  3dvds2dec  12372  odd2np1lem  12378  odd2np1  12379  opoe  12401  omoe  12402  opeo  12403  omeo  12404  m1exp1  12407  n2dvdsm1  12419  flodddiv4  12442  bitsfzo  12461  gcdmultiple  12536  sqgcd  12545  nn0seqcvgd  12558  prmind2  12637  hashdvds  12738  phiprmpw  12739  phiprm  12740  eulerthlemth  12749  sumhashdc  12865  fldivp1  12866  prmpwdvds  12873  pockthlem  12874  pockthi  12876  4sqlem11  12919  4sqlem19  12927  dec5nprm  12932  mulgnndir  13683  mulgneg2  13688  cnfld1  14530  zsssubrg  14543  mulgrhm2  14568  expcncf  15277  divcncfap  15282  hovercncf  15314  dvid  15363  dvidre  15365  dvexp  15379  dvexp2  15380  dveflem  15394  plyaddlem1  15415  plymullem1  15416  dvply1  15433  reeff1olem  15439  eulerid  15470  cos2pi  15472  sincosq3sgn  15496  sincosq4sgn  15497  cosq23lt0  15501  tangtx  15506  sincos4thpi  15508  sincos6thpi  15510  pigt3  15512  abssinper  15514  coskpi  15516  cosq34lt1  15518  logdivlti  15549  rpcxpp1  15574  rpcxpsqrt  15590  rprelogbdiv  15625  binom4  15647  wilthlem1  15648  0sgm  15653  1sgmprm  15662  1sgm2ppw  15663  mersenne  15665  perfect1  15666  perfectlem1  15667  perfectlem2  15668  perfect  15669  zabsle1  15672  lgslem1  15673  lgslem2  15674  lgsfcl2  15679  lgsvalmod  15692  lgsneg  15697  lgsdilem  15700  lgsdir2lem1  15701  lgsdir2lem2  15702  lgsdir2lem3  15703  lgsdir2lem5  15705  lgsne0  15711  lgseisenlem1  15743  lgseisenlem2  15744  lgseisen  15747  lgsquadlem1  15750  lgsquadlem2  15751  lgsquad2lem1  15754  lgsquad2  15756  m1lgs  15758  2lgslem3c  15768  2lgsoddprmlem3c  15782  2lgsoddprmlem3d  15783  2sqlem10  15798  ex-fl  16047  trilpolemeq1  16367