Theorem ax1cn 5249

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 5248	. 2 |- RR (_ CC
2		df-1 5222	. . 3 |- 1 = <.1R, 0R>.
3		1r 5170	. . . 4 |- 1R e. R.
4		opelreal 5229	. . . 4 |- (<.1R, 0R>. e. RR <-> 1R e. R.)
5	3, 4	mpbir 190	. . 3 |- <.1R, 0R>. e. RR
6	2, 5	eqeltr 1541	. 2 |- 1 e. RR
7	1, 6	sselii 2062	1 |- 1 e. CC

Syntax hints:   e. wcel 956  <.cop 2407  R.cnr 4973  0Rc0r 4974  1Rc1r 4975  CCcc 5212  RRcr 5213  1c1 5215

This theorem is referenced by:  0cn 5308  mulid2 5313  peano2cn 5324  mulid2t 5397  muladd11t 5402  1p1times 5413  ine0 5414  0reALT 5421  negdi 5428  mulm1t 5451  lt01 5661  ixi 5662  mulcant2 5668  muleqaddt 5677  divmulz 5683  divclz 5688  reccl 5690  recclz 5691  recclt 5692  divcan1z 5695  divcan2z 5696  recne0z 5702  recid 5704  recidz 5705  divrec 5708  divrecz 5709  divdirz 5720  divcan3z 5724  div11t 5729  recrec 5733  div1 5736  div1t 5737  recrect 5740  rec11 5742  rec11rt 5743  recdivt 5754  divdivmult 5759  recdiv2t 5760  conjmult 5761  redivcl 5762  recgt0i 5778  reclt1t 5854  recgt1t 5855  recp1lt1 5857  recrecltt 5858  1nn 5890  nnaddclt 5896  nnmulclt 5897  nnleltp1t 5909  nnsub 5911  2p2e4 5956  3p2e5 5962  3p3e6 5963  4p2e6 5964  4p3e7 5965  4p4e8 5966  5p2e7 5967  5p3e8 5968  5p4e9 5969  5p5e10 5970  6p2e8 5971  6p3e9 5972  6p4e10 5973  7p2e9 5974  7p3e10 5975  8p2e10 5976  3t3e9 5979  halflt1 5985  8th4div3 5986  halfpm6th 5987  nn0ltp1let 6082  nn0ltlem1t 6084  elnn0nn 6126  elnnnn0 6127  zltp1let 6136  zlem1ltt 6138  zltlem1t 6139  zextltt 6145  recnzt 6146  gtndivt 6148  nneo 6152  zeot 6154  zneo 6155  zneoOLD 6156  dfuz 6158  uzindOLD 6164  nn0ind-raph 6170  rebtwnz 6178  fladdzt 6195  ceim1lt 6200  qbtwnre 6224  seq1lem2 6255  seq1m1 6264  seq1shftid 6301  peano2uzr 6388  uzaddclt 6389  seq1seqz 6481  seq0seqz 6482  seq1seq02t 6483  seq1seq0t 6484  seq1seq0 6485  seqz1 6487  seqzp1 6488  seqzm1 6489  seq00 6490  seq0p1 6491  seq01 6492  seqzval2t 6493  expp1t 6514  expclt 6521  expm1t 6523  1expt 6524  mulexpt 6533  recexpt 6534  expaddt 6535  expmult 6536  exple1t 6546  expubndt 6547  sqreci 6557  sq01t 6590  bernneq 6591  bernneq2 6592  discrlem1 6594  nnesq 6600  nn0opthlem1 6602  sqrlem1 6611  sqrlem16 6626  sqr1 6654  irec 6669  i4 6672  inelr 6673  crmul 6679  crrecz 6680  imret 6718  re1 6765  im1 6766  rei 6767  imi 6768  absi 6823  abs1m 6849  recant 6850  abslem2 6854  ser1absdiflem 6874  facp1t 6881  facnn2t 6884  facndivt 6888  facwordit 6889  faclbnd 6890  faclbnd4lem1 6893  faclbnd4lem4 6896  faclbnd6 6899  bcnp11t 6911  bcnp1nt 6912  bcpasc2 6913  bcpasc 6915  fsum3 6970  fsum4 6971  fsumrev 6975  fsumconst 6984  ser1ser0 6994  serzsplit 7002  binomlem1 7012  binomlem2 7013  binomlem4 7015  binomlem6 7017  binom 7018  binom1p 7019  bcxmas 7022  climsub 7074  iserzshft 7088  iserzex 7090  ser1const 7115  isumnn0nn 7150  fnsmntlem 7168  fnsmnt 7169  geoser 7177  geolimilem 7178  geolim1i 7181  georeclim 7183  geoisumr 7186  geoisum1c 7188  0.999... 7189  cvgratlem1ALT 7190  cvgratlem1 7193  fsum0diaglem2 7200  efseq1ex 7256  dfef2 7257  eval 7259  ef0lem 7260  efseq0ex 7261  erelem2 7270  erelem6 7274  ele3lem 7276  ege2lem2 7278  ege2le3lem2 7279  ef0 7285  efaddlem5 7292  efaddlem6 7293  efaddlem14 7301  efaddlem16 7303  efsubt 7321  efexpt 7322  efnn0valt 7323  eftlext 7328  ef1tllem 7331  ef01tllem2 7334  absef01tlub 7337  eirrlem1 7338  eirrlem2 7339  eirrlem3 7340  eirrlem4 7341  eirrlem5 7342  eft0val 7347  ef4p 7348  efm1lim 7359  efm1legeo 7365  efcnlem1 7367  efcnlem2 7368  reeff1olem1 7372  reeff1olem1OLD 7374  reeff1o 7376  efi4pt 7385  efivalt 7397  cos2tt 7413  cos2tOLD 7414  sin01bndlem1 7417  sin01bndlem3 7419  cos01bndlem3 7421  cos1bnd 7424  cos2bnd 7425  sin01gt0 7426  demoivre 7434  nn0ennn 7447  znnen 7453  ruclem1 7461  ruclem3 7463  ruclem8 7468  ruclem30 7490  ruclem31 7491  ruclem32 7492  dscmet 7870  lmsslem 7903  bcthlem16 7964  ablmul 8083  mulid 8084  cnring 8114  vc2 8126  vcsubdir 8127  vc0 8140  vcm 8142  vcnegneg 8145  vcnegsubdi2 8146  vcsub4 8147  vcoprne 8150  invfval 8213  nvzs 8217  nvmf 8218  nvmdi 8222  nvnegneg 8223  nvsubadd 8227  nvpncan2 8228  nvaddsub4 8233  nvnncan 8235  nvm1 8244  nvdif 8245  nvpi 8246  nvmtri 8251  nvabs 8253  nvge0 8254  nvnd 8270  imsmetlem 8274  nmcnilem 8285  ipval2lem3 8302  ipval2 8304  4ipval2 8305  ipval3 8306  ipval2lem6 8308  ipid 8310  ipcl 8312  ipcj 8314  ip0r 8317  sspmval 8339  lno0 8364  lnosub 8366  ip0i 8428  ip1ilem 8429  ip1i 8430  ip2i 8431  ipdirilem 8432  ipasslem1 8434  ipasslem2 8435  ipasslem10 8443  ipsubdir 8452  ubthlem8 8480  sinhalfpilem 8617  eulerid 8621  sin2pi 8622  cos2pi 8623  sinperlem1 8624  sinmpi 8632  cosmpi 8633  sincosq3sgn 8642  sincosq4sgn 8643  sincos4thpi 8646  sincos6thpi 8647  efifolem2 8657  efifolem5 8660  efifolem6 8661  efif1lem5 8668  circcltOLD 8675  circgrpOLD 8677  efper 8686  pilog 8707  hvsubopr 8824  hvsubclt 8826  hvsubidt 8834  hv2negt 8836  hvm1negt 8840  hvaddsubvalt 8841  hvsub4t 8845  hvaddsub12t 8846  hvpncant 8847  hvaddsubasst 8849  hvsubdistr1t 8855  hvsubdistr2t 8856  hvsubass 8861  hvsubsub4 8865  hv2timest 8867  hvnegdi 8868  hvsubeq0 8869  hvsubcan2 8870  hvaddcan 8871  hvsubadd 8872  hvaddeq0t 8875  hvsubcant 8880  hvsubcan2t 8881  hvsub0t 8882  his2subt 8897  hisubcom 8909  normlem0 8914  normlem9 8923  normlem7tALT 8924  norm-ii 8943  normsub 8947  norm3dif 8953  normpar2 8962  polid2 8963  hilabl 8966  shsubclt 9028  shsubcltOLD 9029  hhssabl 9071  hhssnv 9073  occllem1 9112  projlem4 9128  pjthlem14 9170  shsel3t 9217  h1de2b 9415  h1de2bOLD 9416  pjsub 9563  pjssm 9566  honegsub 9662  homulid2t 9666  honegnegt 9672  hosubnegt 9673  hosubdit 9674  honegdit 9675  honegsubdit 9676  honegsubdi2t 9677  hosub4t 9679  hosubsub4t 9684  ho2timest 9685  hosubeq0 9692  nmopneg 9828  lnop0t 9829  lnopadd 9834  lnopsub 9837  lnophd 9865  lnophmlem2 9880  lnfn0 9909  lnfnadd 9910  lnfnsub 9913  bdophd 9968  nmoptri2 9970  hst1ht 10092  sto2 10102  stadd3 10113  st0 10114  superpos 10218  cdj1 10294  cdj3lem1 10295

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-9 963  ax-10 964  ax-11 965  ax-12 966  ax-13 967  ax-14 968  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457  ax-rep 2688  ax-sep 2698  ax-nul 2705  ax-pow 2737  ax-pr 2774  ax-un 2861  ax-inf2 4605

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 775  df-3an 776  df-ex 979  df-sb 1170  df-eu 1380  df-mo 1381  df-clab 1462  df-cleq 1467  df-clel 1470  df-ne 1584  df-ral 1646  df-rex 1647  df-reu 1648  df-rab 1649  df-v 1808  df-sbc 1938  df-csb 1998  df-dif 2045  df-un 2046  df-in 2047  df-ss 2049  df-pss 2051  df-nul 2277  df-if 2358  df-pw 2398  df-sn 2408  df-pr 2409  df-tp 2411  df-op 2412  df-uni 2499  df-int 2529  df-iun 2563  df-br 2615  df-opab 2662  df-tr 2676  df-eprel 2827  df-id 2830  df-po 2835  df-so 2845  df-fr 2912  df-we 2929  df-ord 2946  df-on 2947  df-lim 2948  df-suc 2949  df-om 3127  df-xp 3179  df-rel 3180  df-cnv 3181  df-co 3182  df-dm 3183  df-rn 3184  df-res 3185  df-ima 3186  df-fun 3187  df-fn 3188  df-f 3189  df-fv 3193  df-rdg 3923  df-opr 3956  df-oprab 3957  df-1st 4069  df-2nd 4070  df-1o 4123  df-oadd 4125  df-omul 4126  df-er 4251  df-ec 4253  df-qs 4256  df-ni 4980  df-pli 4981  df-mi 4982  df-lti 4983  df-plpq 5015  df-mpq 5016  df-enq 5017  df-nq 5018  df-plq 5019  df-mq 5020  df-rq 5021  df-ltq 5022  df-1q 5023  df-np 5066  df-1p 5067  df-plp 5068  df-enr 5146  df-nr 5147  df-0r 5151  df-1r 5152  df-c 5220  df-1 5222  df-r 5224

Copyright terms: Public domain