Theorem ax1cn 5334

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 5333	. 2 |- RR (_ CC
2		df-1 5307	. . 3 |- 1 = <.1R, 0R>.
3		1r 5255	. . . 4 |- 1R e. R.
4		opelreal 5314	. . . 4 |- (<.1R, 0R>. e. RR <-> 1R e. R.)
5	3, 4	mpbir 197	. . 3 |- <.1R, 0R>. e. RR
6	2, 5	eqeltri 1591	. 2 |- 1 e. RR
7	1, 6	sselii 2117	1 |- 1 e. CC

Syntax hints:   e. wcel 999  <.cop 2463  R.cnr 5058  0Rc0r 5059  1Rc1r 5060  CCcc 5297  RRcr 5298  1c1 5300

This theorem is referenced by:  0cn 5393  mulid2i 5398  peano2cn 5409  mulid2 5482  muladd11 5487  1p1timesi 5498  ine0 5499  0reALT 5506  negdii 5513  mulm1 5536  lt01 5745  ixi 5746  mulcant2i 5753  mulcant2iOLD 5754  muleqadd 5765  divmulzi 5771  divclzi 5779  reccli 5781  recclzi 5782  reccl 5783  divcan1zi 5786  divcan2zi 5787  recne0zi 5793  recidi 5795  recidzi 5796  divreci 5799  divreczi 5800  divdirzi 5812  divcan3zi 5817  div11 5822  recreci 5826  div1i 5829  div1 5830  recrec 5834  rec11i 5836  rec11r 5837  recdiv 5848  divdivmul 5853  recdiv2 5854  conjmul 5855  redivcli 5856  recgt0ii 5872  reclt1 5958  recgt1 5959  recp1lt1 5961  recreclt 5962  1nn 5994  nnaddcl 6000  nnmulcl 6001  nnleltp1 6015  nnsubi 6017  2p2e4 6062  3p2e5 6068  3p3e6 6069  4p2e6 6070  4p3e7 6071  4p4e8 6072  5p2e7 6073  5p3e8 6074  5p4e9 6075  5p5e10 6076  6p2e8 6077  6p3e9 6078  6p4e10 6079  7p2e9 6080  7p3e10 6081  8p2e10 6082  3t3e9 6085  halflt1 6091  8th4div3 6092  halfpm6th 6093  nn0ltp1le 6209  nn0ltlem1 6211  elnn0nn 6253  elnnnn0 6254  zltp1le 6263  zlem1lt 6265  zltlem1 6266  zextlt 6275  recnz 6276  gtndiv 6278  nneoi 6282  zeo 6284  zneo 6285  dfuzi 6287  uzindOLD 6293  nn0ind-raph 6299  rebtwnz 6307  qbtwnre 6331  fladdz 6356  ceim1l 6361  fldiv 6368  peano2uzr 6474  uzaddcl 6475  seq1lem2 6569  seq1m1 6578  seq1shftid 6615  seq1seqz 6630  seq0seqz 6631  seq1seq02 6632  seq1seq01 6633  seq1seq0 6634  seqz1 6636  seqzp1 6637  seqzm1 6638  seq00 6639  seq0p1 6640  seq01 6641  seqzval2 6642  expp1 6663  expcl 6670  expm1 6672  1exp 6673  mulexp 6683  recexp 6684  expadd 6685  expmul 6686  exple1 6696  expubnd 6697  sqrecii 6708  sq01 6740  bernneq 6741  bernneq2 6742  discrlem1 6746  nnesqi 6752  nn0opthlem1 6754  sqrlem1 6763  sqrlem16 6778  sqr1 6806  irec 6821  i4 6824  inelr 6825  crmuli 6830  crreczi 6831  imre 6863  re1 6912  im1 6913  rei 6914  imi 6915  absi 6968  abs1mi 6994  recan 6995  abslem2 6999  ser1absdiflem 7019  facp1 7026  facnn2 7029  facndiv 7033  facwordi 7034  faclbnd 7035  faclbnd4lem1 7038  faclbnd4lem4 7041  faclbnd6 7044  bcnp11 7055  bcnp1n 7056  bcpasc2i 7057  bcpasci 7059  fsum3 7114  fsum4 7115  fsumrev 7119  fsumcons 7128  ser1ser0i 7138  serzsplit 7146  binomlem1 7156  binomlem2 7157  binomlem4 7159  binomlem6 7161  binomi 7162  binom1pi 7163  bcxmas 7166  climsub 7220  iserzshfti 7234  iserzexi 7236  ser1consti 7261  isumnn0nn 7297  arisumilem 7315  arisumi 7316  geoseri 7324  geolimilem 7325  geolim1i 7328  georeclim 7330  geoisumr 7333  geoisum1c 7335  0.999... 7336  cvgratlem1ALT 7337  cvgratlem1 7340  fsum0diaglem2 7347  efseq1ex 7396  dfef2i 7397  eval 7399  ef0lem 7400  efseq0ex 7401  erelem2 7410  erelem6 7414  ele3lem 7416  ege2lem2 7418  ege2le3lem2 7419  ef0 7425  efaddlem5 7432  efaddlem6 7433  efaddlem14 7441  efaddlem16 7443  efsub 7461  efexp 7462  efnn0val 7463  eftlex 7468  ef1tllem 7471  ef01tllem2 7474  ef01tllem2OLD 7475  absef01tlubi 7478  eirrlem1 7479  eirrlem2 7480  eirrlem3 7481  eirrlem4 7482  eirrlem5 7483  eft0vali 7489  ef4pi 7490  efm1limi 7502  efm1legeoi 7508  efcnlem1 7510  efcnlem2 7511  reeff1olem1 7515  reeff1o 7517  efi4p 7526  efival 7538  cos2t 7554  cos2tsin 7555  cos2OLD 7556  sin01bndlem1 7559  sin01bndlem3 7561  cos01bndlem3 7563  cos1bnd 7566  cos2bnd 7567  sin01gt0 7568  demoivre 7576  nn0ennn 7589  znnen 7594  ruclem1 7602  ruclem3 7604  ruclem8 7609  ruclem30 7631  ruclem31 7632  ruclem32 7633  dscmet 8003  lmsslem 8037  bcthlem16 8099  ablmul 8215  mulid 8216  cnring 8246  vc2 8258  vcsubdir 8259  vc0 8272  vcm 8274  vcnegneg 8277  vcnegsubdi2 8278  vcsub4 8279  vcoprne 8282  invfval 8345  nvzs 8349  nvmf 8350  nvmdi 8354  nvnegneg 8355  nvsubadd 8359  nvpncan2 8360  nvaddsub4 8365  nvnncan 8367  nvm1 8376  nvdif 8377  nvpi 8378  nvmtri 8383  nvabs 8385  nvge0 8386  nvnd 8403  imsmetlem 8407  nmcnilem 8421  ipval2lem3 8439  ipval2 8441  4ipval2 8442  ipval3 8443  ipval2lem6 8445  ipid 8447  ipcl 8449  ipcj 8451  ip0r 8454  sspmval 8476  lno0 8501  lnoadd 8503  lnosub 8504  ip0i 8568  ip1ilem 8569  ip1i 8570  ip2i 8571  ipdirilem 8572  ipasslem1 8574  ipasslem2 8575  ipasslem10 8583  ipsubdir 8592  ubthlem8 8620  sinhalfpilem 8762  eulerid 8766  sin2pi 8767  cos2pi 8768  sinperlem1 8769  sinmpi 8777  cosmpi 8778  sinppi 8779  sinkpi 8780  sincosq3sgn 8789  sincosq4sgn 8790  sincos4thpi 8793  sincos6thpi 8794  abssinper 8795  efifolem2 8806  efifolem5 8809  efifolem6 8810  efif1lem5 8817  efper 8830  pilog 8851  hvsubopr 8968  hvsubcl 8970  hvsubid 8978  hv2neg 8980  hvm1neg 8984  hvaddsubval 8985  hvsub4 8989  hvaddsub12 8990  hvpncan 8991  hvaddsubass 8993  hvsubdistr1 8999  hvsubdistr2 9000  hvsubassi 9005  hvsubsub4i 9009  hv2times 9011  hvnegdii 9012  hvsubeq0i 9013  hvsubcan2i 9014  hvaddcani 9015  hvsubaddi 9016  hvaddeq0 9019  hvsubcan 9024  hvsubcan2 9025  hvsub0 9026  his2sub 9041  hisubcomi 9053  normlem0 9058  normlem9 9067  normlem7tALT 9068  norm-ii.i 9087  normsubi 9091  norm3difi 9097  normpar2i 9106  polid2i 9107  hilabl 9110  shsubcl 9172  shsubclOLD 9173  hhssabli 9215  hhssnv 9217  occllem1 9256  projlem4 9272  pjthlem14 9315  shsel3 9362  h1de2bi 9560  pjsubii 9706  pjssmii 9709  honegsubi 9805  homulid2 9809  honegneg 9815  hosubneg 9816  hosubdi 9817  honegdi 9818  honegsubdi 9819  honegsubdi2 9820  hosub4 9822  hosubsub4 9827  ho2times 9828  hosubeq0i 9835  nmopnegi 9972  lnop0 9973  lnopaddi 9978  lnopsubi 9981  lnophdi 10010  lnophmlem2 10025  lnfn0i 10054  lnfnaddi 10055  lnfnsubi 10058  bdophdi 10113  nmoptri2i 10115  hst1h 10238  sto2i 10248  stadd3i 10259  st0 10260  superpos 10365  cdj1i 10444  cdj3lem1 10445

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1003  ax-gen 1004  ax-8 1005  ax-9 1006  ax-10 1007  ax-11 1008  ax-12 1009  ax-13 1010  ax-14 1011  ax-17 1012  ax-4 1014  ax-5o 1016  ax-6o 1019  ax-9o 1164  ax-10o 1182  ax-16 1252  ax-11o 1260  ax-ext 1504  ax-rep 2748  ax-sep 2758  ax-nul 2765  ax-pow 2798  ax-pr 2835  ax-un 2922  ax-inf2 4687

This theorem depends on definitions:  df-bi 154  df-or 231  df-an 232  df-3or 788  df-3an 789  df-ex 1022  df-sb 1214  df-eu 1424  df-mo 1425  df-clab 1510  df-cleq 1515  df-clel 1518  df-ne 1634  df-ral 1696  df-rex 1697  df-reu 1698  df-rab 1699  df-v 1859  df-sbc 1989  df-csb 2052  df-dif 2100  df-un 2101  df-in 2102  df-ss 2104  df-pss 2106  df-nul 2332  df-if 2414  df-pw 2454  df-sn 2464  df-pr 2465  df-tp 2467  df-op 2468  df-uni 2558  df-int 2588  df-iun 2622  df-br 2675  df-opab 2722  df-tr 2736  df-eprel 2888  df-id 2891  df-po 2896  df-so 2906  df-fr 2974  df-we 2991  df-ord 3008  df-on 3009  df-lim 3010  df-suc 3011  df-om 3189  df-xp 3241  df-rel 3242  df-cnv 3243  df-co 3244  df-dm 3245  df-rn 3246  df-res 3247  df-ima 3248  df-fun 3249  df-fn 3250  df-f 3251  df-fv 3255  df-rdg 3990  df-opr 4023  df-oprab 4024  df-1st 4137  df-2nd 4138  df-1o 4191  df-oadd 4193  df-omul 4194  df-er 4319  df-ec 4321  df-qs 4324  df-ni 5065  df-pli 5066  df-mi 5067  df-lti 5068  df-plpq 5100  df-mpq 5101  df-enq 5102  df-nq 5103  df-plq 5104  df-mq 5105  df-rq 5106  df-ltq 5107  df-1q 5108  df-np 5151  df-1p 5152  df-plp 5153  df-enr 5231  df-nr 5232  df-0r 5236  df-1r 5237  df-c 5305  df-1 5307  df-r 5309

Copyright terms: Public domain