ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ax-1cn GIF version

Axiom ax-1cn 7681
Description: 1 is a complex number. Axiom for real and complex numbers, justified by theorem ax1cn 7637. (Contributed by NM, 1-Mar-1995.)
Assertion
Ref Expression
ax-1cn 1 ∈ ℂ

Detailed syntax breakdown of Axiom ax-1cn
StepHypRef Expression
1 c1 7589 . 2 class 1
2 cc 7586 . 2 class
31, 2wcel 1465 1 wff 1 ∈ ℂ
Colors of variables: wff set class
This axiom is referenced by:  0cn  7726  1ex  7729  mulid1  7731  mulid2  7732  1cnd  7750  muladd11  7863  1p1times  7864  peano2cn  7865  peano2cnm  7996  0reALT  8027  pncan1  8107  npcan1  8108  kcnktkm1cn  8113  ine0  8124  mulm1  8130  mulsubfacd  8148  ixi  8312  inelr  8313  muleqadd  8396  recclap  8406  recap0  8412  recidap  8413  recidap2  8414  div1  8430  1div1e1  8431  diveqap1  8432  recdivap  8445  divdivap1  8450  divdivap2  8451  recdivap2  8452  conjmulap  8456  eqneg  8459  div2negap  8462  recreclt  8622  nn1m1nn  8702  nn1suc  8703  nnaddcl  8704  nnmulcl  8705  nnsub  8723  1m1e0  8753  neg1cn  8789  neg1ne0  8791  neg1ap0  8793  negneg1e1  8794  1pneg1e0  8795  1m0e1  8797  0p1e1  8798  1p0e1  8800  2m1e1  8802  3m1e2  8804  2p2e4  8805  1p2e3  8812  3p2e5  8819  3p3e6  8820  4p2e6  8821  4p3e7  8822  4p4e8  8823  5p2e7  8824  5p3e8  8825  5p4e9  8826  6p2e8  8827  6p3e9  8828  7p2e9  8829  1t1e1  8830  3t3e9  8835  neg1mulneg1e1  8890  1mhlfehlf  8896  8th4div3  8897  halfpm6th  8898  addltmul  8914  elnn0nn  8977  peano2z  9048  zlem1lt  9068  zltlem1  9069  nnaddm1cl  9073  elz2  9080  zextlt  9101  zeo  9114  peano5uzti  9117  numsuc  9153  numltc  9165  numsucc  9179  numaddc  9187  6p5lem  9209  5p5e10  9210  6p4e10  9211  7p3e10  9214  8p2e10  9219  10m1e9  9235  4t3lem  9236  7t4e28  9250  9t11e99  9269  decbin2  9280  uzp1  9315  peano2uzr  9336  uzaddcl  9337  qreccl  9390  iccf1o  9742  fz01en  9788  fztp  9813  fzsuc2  9814  fztpval  9818  fseq1m1p1  9830  elfzp1b  9832  fzoss2  9904  fzval3  9936  fzosplitsnm1  9941  fzo0to42pr  9952  fzosplitprm1  9966  fldiv4p1lem1div2  10033  flqdiv  10049  frecfzen2  10155  nn0ennn  10161  seq3m1  10196  monoord2  10205  ser3mono  10206  expcl  10266  m1expcl2  10270  expclzaplem  10272  expm1t  10276  1exp  10277  mulexpzap  10288  expadd  10290  expaddzap  10292  expmul  10293  expubnd  10305  neg1sqe1  10342  irec  10347  i4  10350  binom21  10359  bernneq  10367  bernneq2  10368  facndiv  10440  faclbnd6  10445  bcnp1n  10460  bcm1k  10461  bcp1nk  10463  bcn2  10465  bcp1m1  10466  bcpasc  10467  4bc3eq4  10474  hashfz  10522  hashfzo  10523  seq3coll  10540  rei  10626  imi  10627  caucvgrelemrec  10706  recan  10836  iserex  11063  serf0  11076  fsumm1  11140  fsump1  11144  telfsumo  11190  fsumparts  11194  hashiun  11202  binomlem  11207  binom  11208  binom1p  11209  binom11  11210  binom1dif  11211  bcxmas  11213  isumsplit  11215  isum1p  11216  arisum  11222  arisum2  11223  trireciplem  11224  geosergap  11230  geolim  11235  geolim2  11236  georeclim  11237  geo2sum  11238  geo2sum2  11239  0.999...  11245  geoihalfsum  11246  mertenslemi1  11259  mertenslem2  11260  mertensabs  11261  esum  11282  ege2le3  11291  efexp  11302  efzval  11303  eftlub  11310  effsumlt  11312  ef4p  11314  tanval3ap  11335  efi4p  11338  tan0  11352  efival  11353  tanaddap  11360  cos2t  11371  cos2tsin  11372  ef01bndlem  11377  cos1bnd  11380  cos2bnd  11381  demoivreALT  11394  eirraplem  11395  3dvdsdec  11474  3dvds2dec  11475  odd2np1lem  11481  odd2np1  11482  opoe  11504  omoe  11505  opeo  11506  omeo  11507  m1exp1  11510  n2dvdsm1  11522  flodddiv4  11543  gcdmultiple  11620  sqgcd  11629  nn0seqcvgd  11634  prmind2  11713  hashdvds  11808  phiprmpw  11809  phiprm  11810  expcncf  12672  dvid  12742  dvexp  12755  dvexp2  12756  dveflem  12766  eulerid  12794  cos2pi  12796  sincosq3sgn  12820  sincosq4sgn  12821  cosq23lt0  12825  ex-fl  12833  trilpolemeq1  13129
  Copyright terms: Public domain W3C validator