Axiom ax-1cn 8272

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

This axiom is used by:  0cn  8318  1ex  8321  mulrid  8323  mullid  8324  1cnd  8342  muladd11  8459  1p1times  8460  peano2cn  8461  peano2cnm  8592  0reALT  8623  pncan1  8704  npcan1  8705  kcnktkm1cn  8710  ine0  8721  mulm1  8727  mulsubfacd  8746  ixi  8911  inelr  8912  muleqadd  8998  recclap  9009  recap0  9015  recidap  9016  recidap2  9017  div1  9033  1div1e1  9034  diveqap1  9035  recdivap  9048  divdivap1  9053  divdivap2  9054  recdivap2  9055  conjmulap  9059  eqneg  9062  div2negap  9065  recreclt  9230  ofnegsub  9292  nn1m1nn  9322  nn1suc  9323  nnaddcl  9324  nnmulcl  9325  nnsub  9343  1m1e0  9373  neg1cn  9409  neg1ne0  9411  neg1ap0  9413  negneg1e1  9414  1pneg1e0  9415  1m0e1  9417  0p1e1  9418  1p0e1  9420  2m1e1  9422  3m1e2  9424  4m1e3  9425  5m1e4  9426  6m1e5  9427  7m1e6  9428  8m1e7  9429  9m1e8  9430  2p2e4  9431  1p2e3  9439  3p2e5  9446  3p3e6  9447  4p2e6  9448  4p3e7  9449  4p4e8  9450  5p2e7  9451  5p3e8  9452  5p4e9  9453  6p2e8  9454  6p3e9  9455  7p2e9  9456  1t1e1  9457  3t3e9  9462  neg1mulneg1e1  9517  1mhlfehlf  9523  8th4div3  9524  halfpm6th  9525  addltmul  9542  elnn0nn  9605  peano2z  9680  zlem1lt  9701  zltlem1  9702  nnaddm1cl  9706  elz2  9716  zextlt  9738  zeo  9751  peano5uzti  9754  numsuc  9790  numltc  9802  numsucc  9816  numaddc  9824  6p5lem  9846  5p5e10  9847  6p4e10  9848  7p3e10  9851  8p2e10  9856  10m1e9  9872  4t3lem  9873  7t4e28  9887  9t11e99  9906  decbin2  9917  halfthird  9919  5recm6rec  9920  uzp1  9956  peano2uzr  9985  uzaddcl  9986  qreccl  10042  iccf1o  10407  fz01en  10459  fztp  10485  fzsuc2  10486  fztpval  10490  fseq1m1p1  10502  elfzp1b  10504  fz0to4untppr  10531  fzoss2  10581  fzval3  10622  fzosplitsnm1  10627  fzo0to42pr  10638  fzosplitprm1  10653  fldiv4p1lem1div2  10740  flqdiv  10758  frecfzen2  10864  nn0ennn  10870  xnn0nnen  10874  seq3m1  10910  seqshft2g  10919  monoord2  10923  ser3mono  10924  seqf1oglem1  10956  seqf1oglem2  10957  expcl  10994  m1expcl2  10998  expclzaplem  11000  expm1t  11004  1exp  11005  mulexpzap  11016  expadd  11018  expaddzap  11020  expmul  11021  expubnd  11033  neg1sqe1  11071  irec  11076  i4  11079  binom21  11089  bernneq  11098  bernneq2  11099  facndiv  11177  faclbnd6  11182  bcnp1n  11197  bcm1k  11198  bcp1nk  11200  bcn2  11202  bcp1m1  11203  bcpasc  11204  4bc3eq4  11212  hashfz  11262  hashfzo  11263  hashfibclem  11282  hashf1  11287  seq3coll  11294  swrds1  11440  swrdlsw  11441  wrdind  11494  wrd2ind  11495  rei  11665  imi  11666  caucvgrelemrec  11745  recan  11875  iserex  12105  serf0  12118  fsumm1  12183  fsump1  12187  telfsumo  12233  fsumparts  12237  hashiun  12245  binomlem  12250  binom  12251  binom1p  12252  binom11  12253  binom1dif  12254  bcxmas  12256  isumsplit  12258  isum1p  12259  arisum  12265  arisum2  12266  trireciplem  12267  geosergap  12273  geolim  12278  geolim2  12279  georeclim  12280  geo2sum  12281  geo2sum2  12282  0.999...  12288  geoihalfsum  12289  mertenslemi1  12302  mertenslem2  12303  mertensabs  12304  prodf1  12309  prodfclim1  12311  prodrbdclem  12338  fproddccvg  12339  prodmodclem2a  12343  fprodntrivap  12351  prodssdc  12356  fprodssdc  12357  esum  12429  ege2le3  12438  efexp  12449  efzval  12450  eftlub  12457  effsumlt  12459  ef4p  12461  tanval3ap  12481  efi4p  12484  tan0  12498  efival  12499  tanaddap  12506  cos2t  12517  cos2tsin  12518  ef01bndlem  12523  cos1bnd  12526  cos2bnd  12527  demoivreALT  12541  eirraplem  12544  3dvds  12631  3dvdsdec  12632  3dvds2dec  12633  odd2np1lem  12639  odd2np1  12640  opoe  12662  omoe  12663  opeo  12664  omeo  12665  m1exp1  12668  n2dvdsm1  12680  flodddiv4  12703  bitsfzo  12722  gcdmultiple  12797  sqgcd  12806  nn0seqcvgd  12819  prmind2  12898  hashdvds  12999  phiprmpw  13000  phiprm  13001  eulerthlemth  13010  sumhashdc  13126  fldivp1  13127  prmpwdvds  13134  pockthlem  13135  pockthi  13137  4sqlem11  13180  4sqlem19  13188  dec5nprm  13193  ballotfilem2  13228  mulgnndir  13954  mulgneg2  13959  cnfld1  14909  zsssubrg  14922  mulgrhm2  14945  expcncf  15710  divcncfap  15715  hovercncf  15747  dvid  15796  dvidre  15798  dvexp  15812  dvexp2  15813  dveflem  15827  plyaddlem1  15848  plymullem1  15849  dvply1  15866  reeff1olem  15872  eulerid  15903  cos2pi  15905  sincosq3sgn  15929  sincosq4sgn  15930  cosq23lt0  15934  tangtx  15939  sincos4thpi  15941  sincos6thpi  15943  pigt3  15945  abssinper  15947  coskpi  15949  cosq34lt1  15951  logdivlti  15982  rpcxpp1  16008  rpcxpsqrt  16024  rprelogbdiv  16059  binom4  16081  log2tlbndlog2  16082  log2ublem3  16085  log2ublog2  16086  birthdaylem2  16088  birthdaylog2  16090  wilthlem1  16094  0sgm  16099  1sgmprm  16108  1sgm2ppw  16109  mersenne  16111  perfect1  16112  perfectlem1  16113  perfectlem2  16114  perfect  16115  zabsle1  16118  lgslem1  16119  lgslem2  16120  lgsfcl2  16125  lgsvalmod  16138  lgsneg  16143  lgsdilem  16146  lgsdir2lem1  16147  lgsdir2lem2  16148  lgsdir2lem3  16149  lgsdir2lem5  16151  lgsne0  16157  lgseisenlem1  16189  lgseisenlem2  16190  lgseisen  16193  lgsquadlem1  16196  lgsquadlem2  16197  lgsquad2lem1  16200  lgsquad2  16202  m1lgs  16204  2lgslem3c  16214  2lgsoddprmlem3c  16228  2lgsoddprmlem3d  16229  2sqlem10  16244  clwwlknonex2lem2  16679  ex-fl  16739  trilpolemeq1  17089