Theorem ax1cn 5423

Description: 1 is a complex number. Axiom 3 of 25 for real and complex numbers, derived from ZF set theory.

Assertion

Ref	Expression
ax1cn	|- 1 e. CC

Proof of Theorem ax1cn

Step	Hyp	Ref	Expression
1		axresscn 5422	. 2 |- RR (_ CC
2		df-1 5396	. . 3 |- 1 = <.1R, 0R>.
3		1r 5344	. . . 4 |- 1R e. R.
4		opelreal 5403	. . . 4 |- (<.1R, 0R>. e. RR <-> 1R e. R.)
5	3, 4	mpbir 188	. . 3 |- <.1R, 0R>. e. RR
6	2, 5	eqeltri 1587	. 2 |- 1 e. RR
7	1, 6	sselii 2118	1 |- 1 e. CC

Syntax hints:   e. wcel 994  <.cop 2469  R.cnr 5147  0Rc0r 5148  1Rc1r 5149  CCcc 5386  RRcr 5387  1c1 5389

This theorem is referenced by:  0cn 5482  mulid2i 5487  peano2cn 5498  mulid2 5571  muladd11 5576  1p1timesi 5587  ine0 5588  0reALT 5595  negdii 5602  mulm1 5625  lt01 5836  ixi 5837  mulcant2i 5843  muleqadd 5852  divmulzi 5858  divclzi 5863  reccli 5865  recclzi 5866  reccl 5867  divcan1zi 5870  divcan2zi 5871  recne0zi 5877  recidi 5879  recidzi 5880  divreci 5883  divreczi 5884  divdirzi 5895  divcan3zi 5899  div11 5904  recreci 5908  div1i 5911  div1 5912  recrec 5915  rec11i 5917  rec11r 5918  recdiv 5929  divdiv1 5934  divdiv2 5935  recdiv2 5936  conjmul 5937  redivcli 5938  recgt0ii 5954  reclt1 6043  recgt1 6044  recp1lt1 6046  recreclt 6047  1nn 6079  nnaddcl 6085  nnmulcl 6086  nnleltp1 6100  nnsubi 6102  2p2e4 6147  3p2e5 6153  3p3e6 6154  4p2e6 6155  4p3e7 6156  4p4e8 6157  5p2e7 6158  5p3e8 6159  5p4e9 6160  5p5e10 6161  6p2e8 6162  6p3e9 6163  6p4e10 6164  7p2e9 6165  7p3e10 6166  8p2e10 6167  3t3e9 6170  halflt1 6176  8th4div3 6177  halfpm6th 6178  nn0ltp1le 6295  nn0ltlem1 6297  elnn0nn 6339  elnnnn0 6340  zltp1le 6349  zlem1lt 6351  zltlem1 6352  zextlt 6361  recnz 6362  gtndiv 6364  nneoi 6368  zeo 6370  zneo 6371  dfuzi 6373  uzindOLD 6379  nn0ind-raph 6385  rebtwnz 6394  qbtwnre 6418  fladdz 6443  ceim1l 6449  fldiv 6456  peano2uzr 6575  uzaddcl 6576  fz01en 6623  cardfz 6671  seq1lem2 6675  seq1m1 6684  seq1shftid 6721  seq1seqz 6736  seq0seqz 6737  seq1seq02 6738  seq1seq01 6739  seq1seq0 6740  seqz1 6742  seqzp1 6743  seqzm1 6744  seq00 6745  seq0p1 6746  seq01 6747  seqzval2 6748  expp1 6769  expcl 6776  expm1t 6778  1exp 6779  mulexp 6788  exprec 6789  exprecOLD 6790  expadd 6791  expmul 6792  exple1 6804  expubnd 6805  sqrecii 6816  sq01 6848  bernneq 6849  bernneqOLD 6850  bernneq2 6851  discrlem1 6857  nnesqi 6863  nn0opthlem1 6865  sqrlem1 6874  sqrlem16 6889  sqr1 6917  irec 6932  i4 6935  inelr 6936  crmuli 6941  crreczi 6942  imre 6974  re1 7023  im1 7024  rei 7025  imi 7026  absi 7081  abs1mi 7107  recan 7108  abslem2 7112  ser1absdiflem 7132  facp1 7139  facnn2 7142  facndiv 7146  facwordi 7147  faclbnd 7148  faclbnd4lem1 7151  faclbnd4lem4 7154  faclbnd6 7157  bcnp11 7168  bcnp1n 7169  bcpasc2i 7170  bcpasci 7172  fsum3 7227  fsum4 7228  fsumrev 7232  fsumconst 7241  ser1ser0i 7251  serzsplit 7259  binomlem1 7269  binomlem2 7270  binomlem4 7272  binomlem6 7274  binomi 7275  binom1pi 7276  bcxmas 7279  climsub 7333  iserzshfti 7347  iserzexi 7349  ser1consti 7374  isumnn0nn 7411  arisumilem 7429  arisumi 7430  geoseri 7439  geolimilem 7440  geolim1i 7443  georeclim 7445  geoisumr 7448  geoisum1c 7450  0.999... 7451  cvgratlem1ALT 7452  cvgratlem1 7455  fsum0diaglem2 7462  efseq1ex 7511  dfef2i 7512  eval 7514  ef0lem 7515  efseq0ex 7516  erelem2 7525  erelem6 7529  ele3lem 7531  ege2lem2 7533  ege2le3lem2 7534  ef0 7540  efaddlem5 7547  efaddlem6 7548  efaddlem14 7556  efaddlem16 7558  efsub 7576  efexp 7577  efnn0val 7578  eftlex 7583  ef1tllem 7586  ef01tllem2 7589  ef01tllem2OLD 7590  absef01tlubi 7593  eirrlem1 7594  eirrlem2 7595  eirrlem3 7596  eirrlem4 7597  eirrlem5 7598  eft0vali 7606  ef4pi 7607  efm1limi 7619  efm1legeoi 7625  efcnlem1 7627  efcnlem2 7628  reeff1olem1 7632  reeff1o 7634  efi4p 7643  efival 7655  cos2t 7671  cos2tsin 7672  cos2OLD 7673  sin01bndlem1 7676  sin01bndlem3 7678  cos01bndlem3 7680  cos1bnd 7683  cos2bnd 7684  sin01gt0 7685  demoivre 7695  nn0ennn 7709  znnen 7714  ruclem1 7722  ruclem3 7724  ruclem8 7729  ruclem30 7751  ruclem31 7752  ruclem32 7753  dscmet 8129  lmsslem 8163  bcthlem16 8225  gxnn0suc 8320  gxsuc 8328  gxnn0add 8330  gxnn0mul 8333  ablmul 8372  mulid 8373  cnring 8404  vc2 8421  vcsubdir 8422  vc0 8435  vcm 8437  vcnegneg 8440  vcnegsubdi2 8441  vcsub4 8442  vcoprne 8445  invfval 8508  nvzs 8512  nvmf 8513  nvmdi 8517  nvnegneg 8518  nvsubadd 8522  nvpncan2 8523  nvaddsub4 8528  nvnncan 8530  nvm1 8539  nvdif 8540  nvpi 8541  nvmtri 8546  nvabs 8548  nvge0 8549  nvnd 8566  imsmetlem 8570  nmcnilem 8591  ipval2lem3 8609  ipval2 8611  4ipval2 8612  ipval3 8613  ipval2lem6 8615  ipid 8617  ipcl 8619  ipcj 8621  ip0r 8624  sspmval 8646  lno0 8671  lnoadd 8673  lnosub 8674  ip0i 8740  ip1ilem 8741  ip1i 8742  ip2i 8743  ipdirilem 8744  ipasslem1 8746  ipasslem2 8747  ipasslem10 8755  ipsubdir 8764  ubthlem8 8794  sinhalfpilem 8946  eulerid 8950  sin2pi 8951  cos2pi 8952  sinperlem1 8953  sinmpi 8961  cosmpi 8962  sinppi 8963  cosppi 8964  sincosq3sgn 8973  sincosq4sgn 8974  sincos4thpi 8978  sincos6thpi 8979  abssinper 8980  coskpi 8982  efifolem2 8995  efifolem5 8998  efifolem6 8999  efif1lem5 9006  efper 9019  pilog 9040  hvsubopr 9160  hvsubcl 9162  hvsubid 9170  hv2neg 9172  hvm1neg 9176  hvaddsubval 9177  hvsub4 9181  hvaddsub12 9182  hvpncan 9183  hvaddsubass 9185  hvsubdistr1 9191  hvsubdistr2 9192  hvsubassi 9197  hvsubsub4i 9201  hv2times 9203  hvnegdii 9204  hvsubeq0i 9205  hvsubcan2i 9206  hvaddcani 9207  hvsubaddi 9208  hvaddeq0 9211  hvsubcan 9217  hvsubcan2 9218  hvsub0 9219  his2sub 9234  hisubcomi 9246  normlem0 9251  normlem9 9260  normlem7tALT 9261  norm-ii.i 9280  normsubi 9284  norm3difi 9290  normpar2i 9299  polid2i 9300  hilabl 9303  shsubcl 9365  shsubclOLD 9366  hhssabli 9408  hhssnv 9410  occllem1 9449  projlem4 9465  pjthlem14 9508  shsel3 9555  h1de2bi 9753  pjsubii 9901  pjssmii 9904  honegsubi 10002  homulid2 10006  honegneg 10012  hosubneg 10013  hosubdi 10014  honegdi 10015  honegsubdi 10016  honegsubdi2 10017  hosub4 10019  hosubsub4 10024  ho2times 10025  hosubeq0i 10032  nmopnegi 10168  lnop0 10169  lnopaddi 10174  lnopsubi 10177  lnophdi 10206  lnophmlem2 10221  lnfn0i 10250  lnfnaddi 10251  lnfnsubi 10254  bdophdi 10309  nmoptri2i 10311  hst1h 10435  sto2i 10445  stadd3i 10456  st0 10457  superpos 10562  cdj1i 10642  cdj3lem1 10643  uzp1 11863  fzm1 11867  rddif 11869  absrdbnd 11870  sdc 11877  fsumlt1 11894  mettrifi2 11913  geomcau 11914  iihalf2 11937  iimulcl 11938  lincmb01cmp 11942  lincmb01icc 11943  heiborlem30 12040  heiborlem32 12042  heiborlem33 12043  bfplem6 12059  bfplem8 12061  rrndstprj2 12074  rrntotbnd 12078  ismrer1 12080  phtpycom 12092  phtpycolem2 12094  phtpycolem4 12096  phtpyco 12098

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 998  ax-gen 999  ax-8 1000  ax-9 1001  ax-10 1002  ax-11 1003  ax-12 1004  ax-13 1005  ax-14 1006  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159  ax-10o 1177  ax-16 1247  ax-11o 1255  ax-ext 1500  ax-rep 2767  ax-sep 2777  ax-nul 2784  ax-pow 2818  ax-pr 2855  ax-un 3089  ax-inf2 4770

This theorem depends on definitions:  df-bi 145  df-or 222  df-an 223  df-3or 782  df-3an 783  df-ex 1017  df-sb 1209  df-eu 1421  df-mo 1422  df-clab 1506  df-cleq 1511  df-clel 1514  df-ne 1630  df-ral 1695  df-rex 1696  df-reu 1697  df-rab 1698  df-v 1858  df-sbc 1987  df-csb 2052  df-dif 2101  df-un 2102  df-in 2103  df-ss 2105  df-pss 2107  df-nul 2333  df-if 2416  df-pw 2459  df-sn 2470  df-pr 2471  df-tp 2473  df-op 2474  df-uni 2570  df-int 2601  df-iun 2635  df-br 2693  df-opab 2741  df-tr 2755  df-eprel 2910  df-id 2913  df-po 2918  df-so 2929  df-fr 2947  df-we 2962  df-ord 2978  df-on 2979  df-lim 2980  df-suc 2981  df-om 3219  df-xp 3265  df-rel 3266  df-cnv 3267  df-co 3268  df-dm 3269  df-rn 3270  df-res 3271  df-ima 3272  df-fun 3273  df-fn 3274  df-f 3275  df-fv 3279  df-opr 4023  df-oprab 4024  df-1st 4140  df-2nd 4141  df-rdg 4233  df-1o 4269  df-oadd 4271  df-omul 4272  df-er 4401  df-ec 4403  df-qs 4406  df-ni 5154  df-pli 5155  df-mi 5156  df-lti 5157  df-plpq 5189  df-mpq 5190  df-enq 5191  df-nq 5192  df-plq 5193  df-mq 5194  df-rq 5195  df-ltq 5196  df-1q 5197  df-np 5240  df-1p 5241  df-plp 5242  df-enr 5320  df-nr 5321  df-0r 5325  df-1r 5326  df-c 5394  df-1 5396  df-r 5398

Copyright terms: Public domain