Theorem ax1cn 5269

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 5268	. 2 |- RR (_ CC
2		df-1 5242	. . 3 |- 1 = <.1R, 0R>.
3		1r 5190	. . . 4 |- 1R e. R.
4		opelreal 5249	. . . 4 |- (<.1R, 0R>. e. RR <-> 1R e. R.)
5	3, 4	mpbir 190	. . 3 |- <.1R, 0R>. e. RR
6	2, 5	eqeltr 1544	. 2 |- 1 e. RR
7	1, 6	sselii 2066	1 |- 1 e. CC

Syntax hints:   e. wcel 958  <.cop 2411  R.cnr 4993  0Rc0r 4994  1Rc1r 4995  CCcc 5232  RRcr 5233  1c1 5235

This theorem is referenced by:  0cn 5328  mulid2 5333  peano2cn 5344  mulid2t 5417  muladd11t 5422  1p1times 5433  ine0 5434  0reALT 5441  negdi 5448  mulm1t 5471  lt01 5680  ixi 5681  mulcant2 5688  mulcant2OLD 5689  muleqaddt 5700  divmulz 5706  divclz 5711  reccl 5713  recclz 5714  recclt 5715  divcan1z 5718  divcan2z 5719  recne0z 5731  recid 5733  recidz 5734  divrec 5737  divrecz 5738  divdirz 5749  divcan3z 5754  div11t 5765  recrec 5769  div1 5772  div1t 5773  recrect 5776  rec11 5778  rec11rt 5779  recdivt 5790  divdivmult 5795  recdiv2t 5796  conjmult 5797  redivcl 5798  recgt0i 5814  reclt1t 5898  recgt1t 5899  recp1lt1 5901  recrecltt 5902  1nn 5934  nnaddclt 5940  nnmulclt 5941  nnleltp1t 5954  nnsub 5956  2p2e4 6001  3p2e5 6007  3p3e6 6008  4p2e6 6009  4p3e7 6010  4p4e8 6011  5p2e7 6012  5p3e8 6013  5p4e9 6014  5p5e10 6015  6p2e8 6016  6p3e9 6017  6p4e10 6018  7p2e9 6019  7p3e10 6020  8p2e10 6021  3t3e9 6024  halflt1 6030  8th4div3 6031  halfpm6th 6032  nn0ltp1let 6127  nn0ltlem1t 6129  elnn0nn 6171  elnnnn0 6172  zltp1let 6181  zlem1ltt 6183  zltlem1t 6184  zextltt 6190  recnzt 6191  gtndivt 6193  nneo 6197  zeot 6199  zneo 6200  dfuz 6202  uzindOLD 6208  nn0ind-raph 6214  rebtwnz 6222  fladdzt 6244  ceim1lt 6249  qbtwnre 6278  seq1lem2 6310  seq1m1 6319  seq1shftid 6356  peano2uzr 6448  uzaddclt 6449  seq1seqz 6541  seq0seqz 6542  seq1seq02t 6543  seq1seq0t 6544  seq1seq0 6545  seqz1 6547  seqzp1 6548  seqzm1 6549  seq00 6550  seq0p1 6551  seq01 6552  seqzval2t 6553  expp1t 6574  expclt 6581  expm1t 6583  1expt 6584  mulexpt 6594  recexpt 6595  expaddt 6596  expmult 6597  exple1t 6607  expubndt 6608  sqreci 6619  sq01t 6651  bernneq 6652  bernneq2 6653  discrlem1 6656  nnesq 6662  nn0opthlem1 6664  sqrlem1 6673  sqrlem16 6688  sqr1 6716  irec 6731  i4 6734  inelr 6735  crmul 6740  crrecz 6741  imret 6773  re1 6822  im1 6823  rei 6824  imi 6825  absi 6878  abs1m 6904  recant 6905  abslem2 6909  ser1absdiflem 6929  facp1t 6936  facnn2t 6939  facndivt 6943  facwordit 6944  faclbnd 6945  faclbnd4lem1 6948  faclbnd4lem4 6951  faclbnd6 6954  bcnp11t 6965  bcnp1nt 6966  bcpasc2 6967  bcpasc 6969  fsum3 7024  fsum4 7025  fsumrev 7029  fsumconst 7038  ser1ser0 7048  serzsplit 7056  binomlem1 7066  binomlem2 7067  binomlem4 7069  binomlem6 7071  binom 7072  binom1p 7073  bcxmas 7076  climsub 7130  iserzshft 7144  iserzex 7146  ser1const 7171  isumnn0nn 7207  fnsmntlem 7225  fnsmnt 7226  geoser 7234  geolimilem 7235  geolim1i 7238  georeclim 7240  geoisumr 7243  geoisum1c 7245  0.999... 7246  cvgratlem1ALT 7247  cvgratlem1 7250  fsum0diaglem2 7257  efseq1ex 7306  dfef2 7307  eval 7309  ef0lem 7310  efseq0ex 7311  erelem2 7320  erelem6 7324  ele3lem 7326  ege2lem2 7328  ege2le3lem2 7329  ef0 7335  efaddlem5 7342  efaddlem6 7343  efaddlem14 7351  efaddlem16 7353  efsubt 7371  efexpt 7372  efnn0valt 7373  eftlext 7378  ef1tllem 7381  ef01tllem2 7384  ef01tllem2OLD 7385  absef01tlub 7388  eirrlem1 7389  eirrlem2 7390  eirrlem3 7391  eirrlem4 7392  eirrlem5 7393  eft0val 7398  ef4p 7399  efm1lim 7411  efm1legeo 7417  efcnlem1 7419  efcnlem2 7420  reeff1olem1 7424  reeff1o 7426  efi4pt 7435  efivalt 7447  cos2tt 7463  cos2tOLD 7464  sin01bndlem1 7467  sin01bndlem3 7469  cos01bndlem3 7471  cos1bnd 7474  cos2bnd 7475  sin01gt0 7476  demoivre 7484  nn0ennn 7497  znnen 7502  ruclem1 7510  ruclem3 7512  ruclem8 7517  ruclem30 7539  ruclem31 7540  ruclem32 7541  dscmet 7918  lmsslem 7952  bcthlem16 8014  ablmul 8131  mulid 8132  cnring 8162  vc2 8174  vcsubdir 8175  vc0 8188  vcm 8190  vcnegneg 8193  vcnegsubdi2 8194  vcsub4 8195  vcoprne 8198  invfval 8261  nvzs 8265  nvmf 8266  nvmdi 8270  nvnegneg 8271  nvsubadd 8275  nvpncan2 8276  nvaddsub4 8281  nvnncan 8283  nvm1 8292  nvdif 8293  nvpi 8294  nvmtri 8299  nvabs 8301  nvge0 8302  nvnd 8319  imsmetlem 8323  nmcnilem 8337  ipval2lem3 8355  ipval2 8357  4ipval2 8358  ipval3 8359  ipval2lem6 8361  ipid 8363  ipcl 8365  ipcj 8367  ip0r 8370  sspmval 8392  lno0 8417  lnoadd 8419  lnosub 8420  ip0i 8484  ip1ilem 8485  ip1i 8486  ip2i 8487  ipdirilem 8488  ipasslem1 8490  ipasslem2 8491  ipasslem10 8499  ipsubdir 8508  ubthlem8 8536  sinhalfpilem 8679  eulerid 8683  sin2pi 8684  cos2pi 8685  sinperlem1 8686  sinmpi 8694  cosmpi 8695  sinppi 8696  sinkpi 8697  sincosq3sgn 8706  sincosq4sgn 8707  sincos4thpi 8710  sincos6thpi 8711  abssinper 8712  efifolem2 8723  efifolem5 8726  efifolem6 8727  efif1lem5 8734  efper 8747  pilog 8768  hvsubopr 8885  hvsubclt 8887  hvsubidt 8895  hv2negt 8897  hvm1negt 8901  hvaddsubvalt 8902  hvsub4t 8906  hvaddsub12t 8907  hvpncant 8908  hvaddsubasst 8910  hvsubdistr1t 8916  hvsubdistr2t 8917  hvsubass 8922  hvsubsub4 8926  hv2timest 8928  hvnegdi 8929  hvsubeq0 8930  hvsubcan2 8931  hvaddcan 8932  hvsubadd 8933  hvaddeq0t 8936  hvsubcant 8941  hvsubcan2t 8942  hvsub0t 8943  his2subt 8958  hisubcom 8970  normlem0 8975  normlem9 8984  normlem7tALT 8985  norm-ii 9004  normsub 9008  norm3dif 9014  normpar2 9023  polid2 9024  hilabl 9027  shsubclt 9089  shsubcltOLD 9090  hhssabl 9132  hhssnv 9134  occllem1 9173  projlem4 9189  pjthlem14 9232  shsel3t 9279  h1de2b 9477  pjsub 9623  pjssm 9626  honegsub 9722  homulid2t 9726  honegnegt 9732  hosubnegt 9733  hosubdit 9734  honegdit 9735  honegsubdit 9736  honegsubdi2t 9737  hosub4t 9739  hosubsub4t 9744  ho2timest 9745  hosubeq0 9752  nmopneg 9889  lnop0t 9890  lnopadd 9895  lnopsub 9898  lnophd 9927  lnophmlem2 9942  lnfn0 9971  lnfnadd 9972  lnfnsub 9975  bdophd 10030  nmoptri2 10032  hst1ht 10154  sto2 10164  stadd3 10175  st0 10176  superpos 10281  cdj1 10360  cdj3lem1 10361

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-9 965  ax-10 966  ax-11 967  ax-12 968  ax-13 969  ax-14 970  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459  ax-rep 2693  ax-sep 2703  ax-nul 2710  ax-pow 2742  ax-pr 2779  ax-un 2866  ax-inf2 4625

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 776  df-3an 777  df-ex 981  df-sb 1172  df-eu 1382  df-mo 1383  df-clab 1464  df-cleq 1469  df-clel 1472  df-ne 1587  df-ral 1649  df-rex 1650  df-reu 1651  df-rab 1652  df-v 1812  df-sbc 1942  df-csb 2002  df-dif 2049  df-un 2050  df-in 2051  df-ss 2053  df-pss 2055  df-nul 2281  df-if 2362  df-pw 2402  df-sn 2412  df-pr 2413  df-tp 2415  df-op 2416  df-uni 2504  df-int 2534  df-iun 2568  df-br 2620  df-opab 2667  df-tr 2681  df-eprel 2832  df-id 2835  df-po 2840  df-so 2850  df-fr 2917  df-we 2934  df-ord 2951  df-on 2952  df-lim 2953  df-suc 2954  df-om 3132  df-xp 3184  df-rel 3185  df-cnv 3186  df-co 3187  df-dm 3188  df-rn 3189  df-res 3190  df-ima 3191  df-fun 3192  df-fn 3193  df-f 3194  df-fv 3198  df-rdg 3932  df-opr 3965  df-oprab 3966  df-1st 4079  df-2nd 4080  df-1o 4133  df-oadd 4135  df-omul 4136  df-er 4261  df-ec 4263  df-qs 4266  df-ni 5000  df-pli 5001  df-mi 5002  df-lti 5003  df-plpq 5035  df-mpq 5036  df-enq 5037  df-nq 5038  df-plq 5039  df-mq 5040  df-rq 5041  df-ltq 5042  df-1q 5043  df-np 5086  df-1p 5087  df-plp 5088  df-enr 5166  df-nr 5167  df-0r 5171  df-1r 5172  df-c 5240  df-1 5242  df-r 5244

Copyright terms: Public domain