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

Axiom ax-1cn 7201
Description: 1 is a complex number. Axiom for real and complex numbers, justified by theorem ax1cn 7161. (Contributed by NM, 1-Mar-1995.)
Assertion
Ref Expression
ax-1cn  |-  1  e.  CC

Detailed syntax breakdown of Axiom ax-1cn
StepHypRef Expression
1 c1 7114 . 2  class  1
2 cc 7111 . 2  class  CC
31, 2wcel 1434 1  wff  1  e.  CC
Colors of variables: wff set class
This axiom is referenced by:  0cn  7243  1ex  7246  mulid1  7248  mulid2  7249  1cnd  7267  muladd11  7378  1p1times  7379  peano2cn  7380  peano2cnm  7511  0reALT  7542  pncan1  7618  npcan1  7619  kcnktkm1cn  7624  ine0  7635  mulm1  7641  mulsubfacd  7659  ixi  7820  inelr  7821  muleqadd  7895  recclap  7904  recap0  7910  recidap  7911  recidap2  7912  div1  7928  1div1e1  7929  diveqap1  7930  recdivap  7943  divdivap1  7948  divdivap2  7949  recdivap2  7950  conjmulap  7954  eqneg  7957  div2negap  7960  recreclt  8115  nn1m1nn  8194  nn1suc  8195  nnaddcl  8196  nnmulcl  8197  nnsub  8214  1m1e0  8245  neg1cn  8281  neg1ne0  8283  neg1ap0  8285  negneg1e1  8286  1pneg1e0  8287  1m0e1  8289  0p1e1  8290  1p0e1  8291  2m1e1  8293  3m1e2  8295  2p2e4  8296  1p2e3  8303  3p2e5  8310  3p3e6  8311  4p2e6  8312  4p3e7  8313  4p4e8  8314  5p2e7  8315  5p3e8  8316  5p4e9  8317  6p2e8  8318  6p3e9  8319  7p2e9  8320  1t1e1  8321  3t3e9  8326  neg1mulneg1e1  8380  1mhlfehlf  8386  8th4div3  8387  halfpm6th  8388  addltmul  8404  elnn0nn  8467  peano2z  8538  zlem1lt  8558  zltlem1  8559  nnaddm1cl  8563  elz2  8570  zextlt  8590  zeo  8603  peano5uzti  8606  numsuc  8641  numltc  8653  numsucc  8667  numaddc  8675  6p5lem  8697  5p5e10  8698  6p4e10  8699  7p3e10  8702  8p2e10  8707  10m1e9  8723  4t3lem  8724  7t4e28  8738  9t11e99  8757  decbin2  8768  uzp1  8803  peano2uzr  8824  uzaddcl  8825  qreccl  8878  iccf1o  9172  fz01en  9218  fztp  9241  fzsuc2  9242  fztpval  9246  fseq1m1p1  9258  elfzp1b  9260  fzoss2  9328  fzval3  9360  fzosplitsnm1  9365  fzo0to42pr  9376  fzosplitprm1  9390  fldiv4p1lem1div2  9457  flqdiv  9473  frecfzen2  9579  nn0ennn  9585  iseqm1  9613  iseqshft2  9618  monoord2  9622  isermono  9623  expival  9645  expcl  9661  m1expcl2  9665  expclzaplem  9667  expm1t  9671  1exp  9672  mulexpzap  9683  expadd  9685  expaddzap  9687  expmul  9688  expubnd  9700  neg1sqe1  9737  irec  9741  i4  9744  binom21  9753  bernneq  9760  bernneq2  9761  facndiv  9833  faclbnd6  9838  bcnp1n  9853  bcm1k  9854  bcp1nk  9856  bcn2  9858  bcp1m1  9859  bcpasc  9860  4bc3eq4  9867  hashfz  9915  hashfzo  9916  rei  10005  imi  10006  caucvgrelemrec  10084  recan  10214  iiserex  10396  serif0  10408  3dvdsdec  10490  3dvds2dec  10491  odd2np1lem  10497  odd2np1  10498  opoe  10520  omoe  10521  opeo  10522  omeo  10523  m1exp1  10526  n2dvdsm1  10538  flodddiv4  10559  gcdmultiple  10634  sqgcd  10643  nn0seqcvgd  10648  prmind2  10727  hashdvds  10822  phiprmpw  10823  phiprm  10824  ex-fl  10841
  Copyright terms: Public domain W3C validator