Theorem ax1cn 5288

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 5287	. 2 |- RR (_ CC
2		df-1 5261	. . 3 |- 1 = <.1R, 0R>.
3		1r 5209	. . . 4 |- 1R e. R.
4		opelreal 5268	. . . 4 |- (<.1R, 0R>. e. RR <-> 1R e. R.)
5	3, 4	mpbir 190	. . 3 |- <.1R, 0R>. e. RR
6	2, 5	eqeltr 1547	. 2 |- 1 e. RR
7	1, 6	sselii 2070	1 |- 1 e. CC

Syntax hints:   e. wcel 960  <.cop 2416  R.cnr 5012  0Rc0r 5013  1Rc1r 5014  CCcc 5251  RRcr 5252  1c1 5254

This theorem is referenced by:  0cn 5347  mulid2 5352  peano2cn 5363  mulid2t 5436  muladd11t 5441  1p1times 5452  ine0 5453  0reALT 5460  negdi 5467  mulm1t 5490  lt01 5699  ixi 5700  mulcant2 5707  mulcant2OLD 5708  muleqaddt 5719  divmulz 5725  divclz 5730  reccl 5732  recclz 5733  recclt 5734  divcan1z 5737  divcan2z 5738  recne0z 5745  recid 5747  recidz 5748  divrec 5751  divrecz 5752  divdirz 5763  divcan3z 5768  div11t 5773  recrec 5777  div1 5780  div1t 5781  recrect 5785  rec11 5787  rec11rt 5788  recdivt 5799  divdivmult 5804  recdiv2t 5805  conjmult 5806  redivcl 5807  recgt0i 5823  reclt1t 5907  recgt1t 5908  recp1lt1 5910  recrecltt 5911  1nn 5943  nnaddclt 5949  nnmulclt 5950  nnleltp1t 5963  nnsub 5965  2p2e4 6010  3p2e5 6016  3p3e6 6017  4p2e6 6018  4p3e7 6019  4p4e8 6020  5p2e7 6021  5p3e8 6022  5p4e9 6023  5p5e10 6024  6p2e8 6025  6p3e9 6026  6p4e10 6027  7p2e9 6028  7p3e10 6029  8p2e10 6030  3t3e9 6033  halflt1 6039  8th4div3 6040  halfpm6th 6041  nn0ltp1let 6136  nn0ltlem1t 6138  elnn0nn 6180  elnnnn0 6181  zltp1let 6190  zlem1ltt 6192  zltlem1t 6193  zextltt 6199  recnzt 6200  gtndivt 6202  nneo 6206  zeot 6208  zneo 6209  dfuz 6211  uzindOLD 6217  nn0ind-raph 6223  rebtwnz 6231  fladdzt 6253  ceim1lt 6258  fldivt 6263  qbtwnre 6286  seq1lem2 6318  seq1m1 6327  seq1shftid 6364  peano2uzr 6456  uzaddclt 6457  seq1seqz 6549  seq0seqz 6550  seq1seq02t 6551  seq1seq0t 6552  seq1seq0 6553  seqz1 6555  seqzp1 6556  seqzm1 6557  seq00 6558  seq0p1 6559  seq01 6560  seqzval2t 6561  expp1t 6582  expclt 6589  expm1t 6591  1expt 6592  mulexpt 6602  recexpt 6603  expaddt 6604  expmult 6605  exple1t 6615  expubndt 6616  sqreci 6627  sq01t 6659  bernneq 6660  bernneq2 6661  discrlem1 6664  nnesq 6670  nn0opthlem1 6672  sqrlem1 6681  sqrlem16 6696  sqr1 6724  irec 6739  i4 6742  inelr 6743  crmul 6748  crrecz 6749  imret 6781  re1 6829  im1 6830  rei 6831  imi 6832  absi 6885  abs1m 6911  recant 6912  abslem2 6916  ser1absdiflem 6936  facp1t 6943  facnn2t 6946  facndivt 6950  facwordit 6951  faclbnd 6952  faclbnd4lem1 6955  faclbnd4lem4 6958  faclbnd6 6961  bcnp11t 6972  bcnp1nt 6973  bcpasc2 6974  bcpasc 6976  fsum3 7031  fsum4 7032  fsumrev 7036  fsumconst 7045  ser1ser0 7055  serzsplit 7063  binomlem1 7073  binomlem2 7074  binomlem4 7076  binomlem6 7078  binom 7079  binom1p 7080  bcxmas 7083  climsub 7137  iserzshft 7151  iserzex 7153  ser1const 7178  isumnn0nn 7214  fnsmntlem 7232  fnsmnt 7233  geoser 7241  geolimilem 7242  geolim1i 7245  georeclim 7247  geoisumr 7250  geoisum1c 7252  0.999... 7253  cvgratlem1ALT 7254  cvgratlem1 7257  fsum0diaglem2 7264  efseq1ex 7313  dfef2 7314  eval 7316  ef0lem 7317  efseq0ex 7318  erelem2 7327  erelem6 7331  ele3lem 7333  ege2lem2 7335  ege2le3lem2 7336  ef0 7342  efaddlem5 7349  efaddlem6 7350  efaddlem14 7358  efaddlem16 7360  efsubt 7378  efexpt 7379  efnn0valt 7380  eftlext 7385  ef1tllem 7388  ef01tllem2 7391  ef01tllem2OLD 7392  absef01tlub 7395  eirrlem1 7396  eirrlem2 7397  eirrlem3 7398  eirrlem4 7399  eirrlem5 7400  eft0val 7405  ef4p 7406  efm1lim 7418  efm1legeo 7424  efcnlem1 7426  efcnlem2 7427  reeff1olem1 7431  reeff1o 7433  efi4pt 7442  efivalt 7454  cos2tt 7470  cos2tsint 7471  cos2tOLD 7472  sin01bndlem1 7475  sin01bndlem3 7477  cos01bndlem3 7479  cos1bnd 7482  cos2bnd 7483  sin01gt0 7484  demoivre 7492  nn0ennn 7505  znnen 7510  ruclem1 7518  ruclem3 7520  ruclem8 7525  ruclem30 7547  ruclem31 7548  ruclem32 7549  dscmet 7922  lmsslem 7956  bcthlem16 8018  ablmul 8134  mulid 8135  cnring 8165  vc2 8177  vcsubdir 8178  vc0 8191  vcm 8193  vcnegneg 8196  vcnegsubdi2 8197  vcsub4 8198  vcoprne 8201  invfval 8264  nvzs 8268  nvmf 8269  nvmdi 8273  nvnegneg 8274  nvsubadd 8278  nvpncan2 8279  nvaddsub4 8284  nvnncan 8286  nvm1 8295  nvdif 8296  nvpi 8297  nvmtri 8302  nvabs 8304  nvge0 8305  nvnd 8322  imsmetlem 8326  nmcnilem 8340  ipval2lem3 8358  ipval2 8360  4ipval2 8361  ipval3 8362  ipval2lem6 8364  ipid 8366  ipcl 8368  ipcj 8370  ip0r 8373  sspmval 8395  lno0 8420  lnoadd 8422  lnosub 8423  ip0i 8487  ip1ilem 8488  ip1i 8489  ip2i 8490  ipdirilem 8491  ipasslem1 8493  ipasslem2 8494  ipasslem10 8502  ipsubdir 8511  ubthlem8 8539  sinhalfpilem 8681  eulerid 8685  sin2pi 8686  cos2pi 8687  sinperlem1 8688  sinmpi 8696  cosmpi 8697  sinppi 8698  sinkpi 8699  sincosq3sgn 8708  sincosq4sgn 8709  sincos4thpi 8712  sincos6thpi 8713  abssinper 8714  efifolem2 8725  efifolem5 8728  efifolem6 8729  efif1lem5 8736  efper 8749  pilog 8770  hvsubopr 8887  hvsubclt 8889  hvsubidt 8897  hv2negt 8899  hvm1negt 8903  hvaddsubvalt 8904  hvsub4t 8908  hvaddsub12t 8909  hvpncant 8910  hvaddsubasst 8912  hvsubdistr1t 8918  hvsubdistr2t 8919  hvsubass 8924  hvsubsub4 8928  hv2timest 8930  hvnegdi 8931  hvsubeq0 8932  hvsubcan2 8933  hvaddcan 8934  hvsubadd 8935  hvaddeq0t 8938  hvsubcant 8943  hvsubcan2t 8944  hvsub0t 8945  his2subt 8960  hisubcom 8972  normlem0 8977  normlem9 8986  normlem7tALT 8987  norm-ii 9006  normsub 9010  norm3dif 9016  normpar2 9025  polid2 9026  hilabl 9029  shsubclt 9091  shsubcltOLD 9092  hhssabl 9134  hhssnv 9136  occllem1 9175  projlem4 9191  pjthlem14 9234  shsel3t 9281  h1de2b 9479  pjsub 9625  pjssm 9628  honegsub 9724  homulid2t 9728  honegnegt 9734  hosubnegt 9735  hosubdit 9736  honegdit 9737  honegsubdit 9738  honegsubdi2t 9739  hosub4t 9741  hosubsub4t 9746  ho2timest 9747  hosubeq0 9754  nmopneg 9891  lnop0t 9892  lnopadd 9897  lnopsub 9900  lnophd 9929  lnophmlem2 9944  lnfn0 9973  lnfnadd 9974  lnfnsub 9977  bdophd 10032  nmoptri2 10034  hst1ht 10157  sto2 10167  stadd3 10178  st0 10179  superpos 10284  cdj1 10363  cdj3lem1 10364

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-9 967  ax-10 968  ax-11 969  ax-12 970  ax-13 971  ax-14 972  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462  ax-rep 2699  ax-sep 2709  ax-nul 2716  ax-pow 2749  ax-pr 2786  ax-un 2873  ax-inf2 4641

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 778  df-3an 779  df-ex 983  df-sb 1174  df-eu 1384  df-mo 1385  df-clab 1467  df-cleq 1472  df-clel 1475  df-ne 1590  df-ral 1652  df-rex 1653  df-reu 1654  df-rab 1655  df-v 1815  df-sbc 1945  df-csb 2006  df-dif 2053  df-un 2054  df-in 2055  df-ss 2057  df-pss 2059  df-nul 2285  df-if 2367  df-pw 2407  df-sn 2417  df-pr 2418  df-tp 2420  df-op 2421  df-uni 2509  df-int 2539  df-iun 2573  df-br 2626  df-opab 2673  df-tr 2687  df-eprel 2839  df-id 2842  df-po 2847  df-so 2857  df-fr 2924  df-we 2941  df-ord 2958  df-on 2959  df-lim 2960  df-suc 2961  df-om 3139  df-xp 3191  df-rel 3192  df-cnv 3193  df-co 3194  df-dm 3195  df-rn 3196  df-res 3197  df-ima 3198  df-fun 3199  df-fn 3200  df-f 3201  df-fv 3205  df-rdg 3939  df-opr 3972  df-oprab 3973  df-1st 4086  df-2nd 4087  df-1o 4140  df-oadd 4142  df-omul 4143  df-er 4268  df-ec 4270  df-qs 4273  df-ni 5019  df-pli 5020  df-mi 5021  df-lti 5022  df-plpq 5054  df-mpq 5055  df-enq 5056  df-nq 5057  df-plq 5058  df-mq 5059  df-rq 5060  df-ltq 5061  df-1q 5062  df-np 5105  df-1p 5106  df-plp 5107  df-enr 5185  df-nr 5186  df-0r 5190  df-1r 5191  df-c 5259  df-1 5261  df-r 5263

Copyright terms: Public domain