Axiom ax-1cn 8115

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

This axiom is referenced by:  0cn  8161  1ex  8164  mulrid  8166  mullid  8167  1cnd  8185  muladd11  8302  1p1times  8303  peano2cn  8304  peano2cnm  8435  0reALT  8466  pncan1  8546  npcan1  8547  kcnktkm1cn  8552  ine0  8563  mulm1  8569  mulsubfacd  8588  ixi  8753  inelr  8754  muleqadd  8838  recclap  8849  recap0  8855  recidap  8856  recidap2  8857  div1  8873  1div1e1  8874  diveqap1  8875  recdivap  8888  divdivap1  8893  divdivap2  8894  recdivap2  8895  conjmulap  8899  eqneg  8902  div2negap  8905  recreclt  9070  ofnegsub  9132  nn1m1nn  9151  nn1suc  9152  nnaddcl  9153  nnmulcl  9154  nnsub  9172  1m1e0  9202  neg1cn  9238  neg1ne0  9240  neg1ap0  9242  negneg1e1  9243  1pneg1e0  9244  1m0e1  9246  0p1e1  9247  1p0e1  9249  2m1e1  9251  3m1e2  9253  4m1e3  9254  5m1e4  9255  6m1e5  9256  7m1e6  9257  8m1e7  9258  9m1e8  9259  2p2e4  9260  1p2e3  9268  3p2e5  9275  3p3e6  9276  4p2e6  9277  4p3e7  9278  4p4e8  9279  5p2e7  9280  5p3e8  9281  5p4e9  9282  6p2e8  9283  6p3e9  9284  7p2e9  9285  1t1e1  9286  3t3e9  9291  neg1mulneg1e1  9346  1mhlfehlf  9352  8th4div3  9353  halfpm6th  9354  addltmul  9371  elnn0nn  9434  peano2z  9505  zlem1lt  9526  zltlem1  9527  nnaddm1cl  9531  elz2  9541  zextlt  9562  zeo  9575  peano5uzti  9578  numsuc  9614  numltc  9626  numsucc  9640  numaddc  9648  6p5lem  9670  5p5e10  9671  6p4e10  9672  7p3e10  9675  8p2e10  9680  10m1e9  9696  4t3lem  9697  7t4e28  9711  9t11e99  9730  decbin2  9741  halfthird  9743  5recm6rec  9744  uzp1  9780  peano2uzr  9809  uzaddcl  9810  qreccl  9866  iccf1o  10229  fz01en  10278  fztp  10303  fzsuc2  10304  fztpval  10308  fseq1m1p1  10320  elfzp1b  10322  fz0to4untppr  10349  fzoss2  10399  fzval3  10439  fzosplitsnm1  10444  fzo0to42pr  10455  fzosplitprm1  10470  fldiv4p1lem1div2  10555  flqdiv  10573  frecfzen2  10679  nn0ennn  10685  xnn0nnen  10689  seq3m1  10725  seqshft2g  10734  monoord2  10738  ser3mono  10739  seqf1oglem1  10771  seqf1oglem2  10772  expcl  10809  m1expcl2  10813  expclzaplem  10815  expm1t  10819  1exp  10820  mulexpzap  10831  expadd  10833  expaddzap  10835  expmul  10836  expubnd  10848  neg1sqe1  10886  irec  10891  i4  10894  binom21  10904  bernneq  10912  bernneq2  10913  facndiv  10991  faclbnd6  10996  bcnp1n  11011  bcm1k  11012  bcp1nk  11014  bcn2  11016  bcp1m1  11017  bcpasc  11018  4bc3eq4  11025  hashfz  11075  hashfzo  11076  seq3coll  11096  swrds1  11239  swrdlsw  11240  wrdind  11293  wrd2ind  11294  rei  11450  imi  11451  caucvgrelemrec  11530  recan  11660  iserex  11890  serf0  11903  fsumm1  11967  fsump1  11971  telfsumo  12017  fsumparts  12021  hashiun  12029  binomlem  12034  binom  12035  binom1p  12036  binom11  12037  binom1dif  12038  bcxmas  12040  isumsplit  12042  isum1p  12043  arisum  12049  arisum2  12050  trireciplem  12051  geosergap  12057  geolim  12062  geolim2  12063  georeclim  12064  geo2sum  12065  geo2sum2  12066  0.999...  12072  geoihalfsum  12073  mertenslemi1  12086  mertenslem2  12087  mertensabs  12088  prodf1  12093  prodfclim1  12095  prodrbdclem  12122  fproddccvg  12123  prodmodclem2a  12127  fprodntrivap  12135  prodssdc  12140  fprodssdc  12141  esum  12213  ege2le3  12222  efexp  12233  efzval  12234  eftlub  12241  effsumlt  12243  ef4p  12245  tanval3ap  12265  efi4p  12268  tan0  12282  efival  12283  tanaddap  12290  cos2t  12301  cos2tsin  12302  ef01bndlem  12307  cos1bnd  12310  cos2bnd  12311  demoivreALT  12325  eirraplem  12328  3dvds  12415  3dvdsdec  12416  3dvds2dec  12417  odd2np1lem  12423  odd2np1  12424  opoe  12446  omoe  12447  opeo  12448  omeo  12449  m1exp1  12452  n2dvdsm1  12464  flodddiv4  12487  bitsfzo  12506  gcdmultiple  12581  sqgcd  12590  nn0seqcvgd  12603  prmind2  12682  hashdvds  12783  phiprmpw  12784  phiprm  12785  eulerthlemth  12794  sumhashdc  12910  fldivp1  12911  prmpwdvds  12918  pockthlem  12919  pockthi  12921  4sqlem11  12964  4sqlem19  12972  dec5nprm  12977  mulgnndir  13728  mulgneg2  13733  cnfld1  14576  zsssubrg  14589  mulgrhm2  14614  expcncf  15323  divcncfap  15328  hovercncf  15360  dvid  15409  dvidre  15411  dvexp  15425  dvexp2  15426  dveflem  15440  plyaddlem1  15461  plymullem1  15462  dvply1  15479  reeff1olem  15485  eulerid  15516  cos2pi  15518  sincosq3sgn  15542  sincosq4sgn  15543  cosq23lt0  15547  tangtx  15552  sincos4thpi  15554  sincos6thpi  15556  pigt3  15558  abssinper  15560  coskpi  15562  cosq34lt1  15564  logdivlti  15595  rpcxpp1  15620  rpcxpsqrt  15636  rprelogbdiv  15671  binom4  15693  wilthlem1  15694  0sgm  15699  1sgmprm  15708  1sgm2ppw  15709  mersenne  15711  perfect1  15712  perfectlem1  15713  perfectlem2  15714  perfect  15715  zabsle1  15718  lgslem1  15719  lgslem2  15720  lgsfcl2  15725  lgsvalmod  15738  lgsneg  15743  lgsdilem  15746  lgsdir2lem1  15747  lgsdir2lem2  15748  lgsdir2lem3  15749  lgsdir2lem5  15751  lgsne0  15757  lgseisenlem1  15789  lgseisenlem2  15790  lgseisen  15793  lgsquadlem1  15796  lgsquadlem2  15797  lgsquad2lem1  15800  lgsquad2  15802  m1lgs  15804  2lgslem3c  15814  2lgsoddprmlem3c  15828  2lgsoddprmlem3d  15829  2sqlem10  15844  clwwlknonex2lem2  16233  ex-fl  16257  trilpolemeq1  16580