MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  1re Unicode version

Theorem 1re 9616
Description: is a real number. This used to be one of our postulates for complex numbers, but Eric Schmidt discovered that it could be derived from a weaker postulate, ax-1cn 9571, by exploiting properties of the imaginary unit . (Contributed by Eric Schmidt, 11-Apr-2007.) (Revised by Scott Fenton, 3-Jan-2013.)
Assertion
Ref Expression
1re

Proof of Theorem 1re
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ax-1ne0 9582 . . 3
2 ax-1cn 9571 . . . . 5
3 cnre 9613 . . . . 5
42, 3ax-mp 5 . . . 4
5 neeq1 2738 . . . . . . . 8
65biimpcd 224 . . . . . . 7
7 0cn 9609 . . . . . . . 8
8 cnre 9613 . . . . . . . 8
97, 8ax-mp 5 . . . . . . 7
10 neeq2 2740 . . . . . . . . . 10
1110biimpcd 224 . . . . . . . . 9
1211reximdv 2931 . . . . . . . 8
1312reximdv 2931 . . . . . . 7
146, 9, 13syl6mpi 62 . . . . . 6
1514reximdv 2931 . . . . 5
1615reximdv 2931 . . . 4
174, 16mpi 17 . . 3
18 ioran 490 . . . . . . . . 9
19 df-ne 2654 . . . . . . . . . . 11
2019con2bii 332 . . . . . . . . . 10
21 df-ne 2654 . . . . . . . . . . 11
2221con2bii 332 . . . . . . . . . 10
2320, 22anbi12i 697 . . . . . . . . 9
2418, 23bitr4i 252 . . . . . . . 8
25 id 22 . . . . . . . . 9
26 oveq2 6304 . . . . . . . . 9
2725, 26oveqan12d 6315 . . . . . . . 8
2824, 27sylbi 195 . . . . . . 7
2928necon1ai 2688 . . . . . 6
30 neeq1 2738 . . . . . . . . . 10
31 neeq2 2740 . . . . . . . . . 10
3230, 31rspc2ev 3221 . . . . . . . . 9
33323expia 1198 . . . . . . . 8
3433ad2ant2r 746 . . . . . . 7
35 neeq1 2738 . . . . . . . . . 10
36 neeq2 2740 . . . . . . . . . 10
3735, 36rspc2ev 3221 . . . . . . . . 9
38373expia 1198 . . . . . . . 8
3938ad2ant2l 745 . . . . . . 7
4034, 39jaod 380 . . . . . 6
4129, 40syl5 32 . . . . 5
4241rexlimdvva 2956 . . . 4
4342rexlimivv 2954 . . 3
441, 17, 43mp2b 10 . 2
45 eqtr3 2485 . . . . . . . . 9
4645ex 434 . . . . . . . 8
4746necon3d 2681 . . . . . . 7
48 neeq1 2738 . . . . . . . . 9
4948rspcev 3210 . . . . . . . 8
5049expcom 435 . . . . . . 7
5147, 50syl6 33 . . . . . 6
5251com23 78 . . . . 5
5352adantld 467 . . . 4
54 neeq1 2738 . . . . . . . 8
5554rspcev 3210 . . . . . . 7
5655expcom 435 . . . . . 6
5756adantrd 468 . . . . 5
5857a1dd 46 . . . 4
5953, 58pm2.61ine 2770 . . 3
6059rexlimivv 2954 . 2
61 ax-rrecex 9585 . . . 4
62 remulcl 9598 . . . . . . 7
6362adantlr 714 . . . . . 6
64 eleq1 2529 . . . . . 6
6563, 64syl5ibcom 220 . . . . 5
6665rexlimdva 2949 . . . 4
6761, 66mpd 15 . . 3
6867rexlimiva 2945 . 2
6944, 60, 68mp2b 10 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4  \/wo 368  /\wa 369  =wceq 1395  e.wcel 1818  =/=wne 2652  E.wrex 2808  (class class class)co 6296   cc 9511   cr 9512  0cc0 9513  1c1 9514   ci 9515   caddc 9516   cmul 9518
This theorem is referenced by:  0re  9617  1red  9632  dedekind  9765  peano2re  9774  mul02lem2  9778  addid1  9781  renegcl  9905  peano2rem  9909  0reALT  9940  0lt1  10100  0le1  10101  relin01  10102  1le1  10202  eqneg  10289  ltp1  10405  ltm1  10407  recgt0  10411  mulgt1  10426  ltmulgt11  10427  lemulge11  10429  reclt1  10465  recgt1  10466  recgt1i  10467  recp1lt1  10468  recreclt  10469  recgt0ii  10476  ledivp1i  10496  ltdivp1i  10497  inelr  10551  cju  10557  nnssre  10565  nnge1  10587  nngt1ne1  10588  nnle1eq1  10589  nngt0  10590  nnnlt1  10591  nnrecre  10597  nnrecgt0  10598  nnsub  10599  2re  10630  3re  10634  4re  10637  5re  10639  6re  10641  7re  10643  8re  10645  9re  10647  10re  10649  0le2  10651  2pos  10652  3pos  10654  4pos  10656  5pos  10658  6pos  10659  7pos  10660  8pos  10661  9pos  10662  10pos  10663  neg1rr  10665  neg1lt0  10667  1lt2  10727  1lt3  10729  1lt4  10732  1lt5  10736  1lt6  10741  1lt7  10747  1lt8  10754  1lt9  10762  1lt10  10771  1ne2  10773  1le2  10774  1le3  10777  halflt1  10782  addltmul  10799  nnunb  10816  elnnnn0c  10866  nn0ge2m1nn  10886  elnnz1  10915  znnnlt1  10916  zltp1le  10938  zleltp1  10939  nn0lt2  10952  recnz  10963  gtndiv  10965  uzindOLD  10982  eluzp1m1  11133  eluzp1p1  11135  eluz2b2  11183  zbtwnre  11209  rebtwnz  11210  1rp  11253  qbtwnxr  11428  xmulid1  11500  xmulid2  11501  xmulm1  11502  x2times  11520  xrub  11532  0elunit  11667  1elunit  11668  divelunit  11691  lincmb01cmp  11692  iccf1o  11693  xov1plusxeqvd  11695  unitssre  11696  fzpreddisj  11758  fznatpl1  11763  fztpval  11770  fraclt1  11939  fracle1  11940  flbi2  11953  fldiv  11987  modid  12020  1mod  12028  modm1p1mod0  12038  seqf1olem1  12146  reexpcl  12183  reexpclz  12186  expge0  12202  expge1  12203  expgt1  12204  bernneq  12292  bernneq2  12293  expnbnd  12295  expnlbnd  12296  expnlbnd2  12297  expmulnbnd  12298  discr1  12302  facwordi  12367  faclbnd3  12370  faclbnd4lem1  12371  faclbnd4lem4  12374  faclbnd6  12377  facavg  12379  hashv01gt1  12418  hashge1  12457  hashnn0n0nn  12458  hash1snb  12479  hashgt12el  12481  hashgt12el2  12482  hashfun  12495  hashge2el2dif  12521  f1oun2prg  12865  sgn1  12925  cjexp  12983  re1  12987  im1  12988  rei  12989  imi  12990  sqrlem1  13076  sqrlem2  13077  sqrlem3  13078  sqrlem4  13079  sqrlem7  13082  resqrex  13084  sqrt1  13105  sqrt2gt1lt2  13108  sqrtm1  13109  abs1  13130  absrdbnd  13174  caubnd2  13190  mulcn2  13418  reccn2  13419  rlimno1  13476  o1fsum  13627  expcnv  13675  geolim  13679  geolim2  13680  georeclim  13681  geomulcvg  13685  geoisumr  13687  geoisum1c  13689  geoihalfsum  13691  ere  13824  ege2le3  13825  efgt1  13851  resin4p  13873  recos4p  13874  tanhbnd  13896  sinbnd  13915  cosbnd  13916  sinbnd2  13917  cosbnd2  13918  ef01bndlem  13919  sin01bnd  13920  cos01bnd  13921  cos1bnd  13922  cos2bnd  13923  sinltx  13924  sin01gt0  13925  cos01gt0  13926  sin02gt0  13927  sincos1sgn  13928  rpnnen2lem2  13949  rpnnen2lem3  13950  rpnnen2lem4  13951  rpnnen2lem9  13956  rpnnen2  13959  ruclem6  13968  ruclem11  13973  ruclem12  13974  n2dvds1  14035  3dvds  14050  sadcadd  14108  isprm3  14226  sqnprm  14239  coprm  14241  phibndlem  14300  pythagtriplem3  14342  pcmpt  14411  fldivp1  14416  pockthi  14425  infpn2  14431  resslem  14690  oppcbas  15113  rescbas  15198  rescabs  15202  odubas  15763  lt6abl  16897  srgbinomlem4  17194  abvneg  17483  abvtrivd  17489  isnzr2hash  17912  0ringnnzr  17917  xrsmcmn  18441  xrsnsgrp  18454  gzrngunitlem  18482  gzrngunit  18483  rge0srg  18487  psgnodpmr  18626  remulg  18643  resubdrg  18644  thlbas  18727  matbas  18915  leordtval2  19713  tuslem  20770  setsmsbas  20978  dscmet  21093  dscopn  21094  nrginvrcnlem  21199  nmoid  21249  idnghm  21250  tgioo  21301  blcvx  21303  metnrmlem1a  21362  metnrmlem1  21363  iicmp  21390  iicon  21391  iirev  21429  iihalf1  21431  iihalf2  21433  iihalf2cn  21434  elii1  21435  elii2  21436  iimulcl  21437  icopnfcnv  21442  icopnfhmeo  21443  iccpnfcnv  21444  iccpnfhmeo  21445  xrhmeo  21446  xrhmph  21447  evth  21459  xlebnum  21465  lebnumii  21466  htpycc  21480  reparphti  21497  pcoval1  21513  pco1  21515  pcoval2  21516  pcocn  21517  pcohtpylem  21519  pcopt  21522  pcopt2  21523  pcoass  21524  pcorevlem  21526  nmhmcn  21603  ovolunlem1a  21907  vitalilem2  22018  vitalilem4  22020  vitalilem5  22021  vitali  22022  i1f1  22097  itg11  22098  itg2const  22147  itg2monolem1  22157  itg2monolem3  22159  dveflem  22380  dvlipcn  22395  dvcvx  22421  ply1remlem  22563  fta1blem  22569  vieta1lem2  22707  aalioulem3  22730  aalioulem5  22732  aaliou3lem2  22739  ulmbdd  22793  iblulm  22802  radcnvlem1  22808  dvradcnv  22816  abelthlem2  22827  abelthlem3  22828  abelthlem5  22830  abelthlem7  22833  abelth  22836  abelth2  22837  reeff1olem  22841  reeff1o  22842  sinhalfpilem  22856  tangtx  22898  sincos4thpi  22906  pige3  22910  coskpi  22913  recosf1o  22922  tanregt0  22926  efif1olem3  22931  efif1olem4  22932  loge  22971  logdivlti  23005  logcnlem4  23026  logf1o2  23031  dvlog2lem  23033  logtayl  23041  logccv  23044  recxpcl  23056  cxplea  23077  cxpcn3lem  23121  cxpaddlelem  23125  loglesqrt  23132  ang180lem2  23142  angpined  23161  chordthmlem4  23166  acosrecl  23234  atancj  23241  atanlogaddlem  23244  atantan  23254  atans2  23262  ressatans  23265  leibpi  23273  birthdaylem3  23283  cxp2lim  23306  cxploglim  23307  cxploglim2  23308  divsqrtsumlem  23309  cvxcl  23314  scvxcvx  23315  jensenlem2  23317  amgmlem  23319  emcllem2  23326  emcllem4  23328  emcllem6  23330  emcllem7  23331  emre  23335  emgt0  23336  harmonicbnd3  23337  harmonicubnd  23339  harmonicbnd4  23340  ftalem1  23346  ftalem2  23347  ftalem5  23350  issqf  23410  cht1  23439  chp1  23441  ppiltx  23451  mumullem2  23454  ppiublem1  23477  ppiub  23479  chtublem  23486  chtub  23487  logfacbnd3  23498  logexprlim  23500  perfectlem2  23505  dchrinv  23536  dchr1re  23538  efexple  23556  bposlem1  23559  bposlem2  23560  bposlem5  23563  bposlem8  23566  lgsdir2lem1  23598  lgsdir2lem5  23602  lgsdir  23605  lgsne0  23608  lgsabs1  23609  lgsdinn0  23615  lgseisen  23628  m1lgs  23637  chebbnd1lem3  23656  chebbnd1  23657  chtppilimlem1  23658  chtppilimlem2  23659  chtppilim  23660  chpchtlim  23664  vmadivsumb  23668  rplogsumlem2  23670  rpvmasumlem  23672  dchrmusumlema  23678  dchrmusum2  23679  dchrvmasumlem2  23683  dchrvmasumiflem1  23686  dchrisum0flblem1  23693  dchrisum0flblem2  23694  dchrisum0fno1  23696  rpvmasum2  23697  dchrisum0re  23698  dchrisum0lema  23699  dchrisum0lem1b  23700  dchrisum0lem1  23701  dchrisum0lem2a  23702  dchrisum0lem2  23703  logdivsum  23718  mulog2sumlem2  23720  2vmadivsumlem  23725  log2sumbnd  23729  selbergb  23734  selberg2b  23737  chpdifbndlem1  23738  selberg3lem1  23742  selberg3lem2  23743  selberg4lem1  23745  pntrmax  23749  pntrsumo1  23750  selbergsb  23760  pntrlog2bndlem3  23764  pntrlog2bndlem5  23766  pntpbnd1a  23770  pntpbnd2  23772  pntibndlem1  23774  pntibndlem2  23776  pntibndlem3  23777  pntibnd  23778  pntlemd  23779  pntlemc  23780  pntlemb  23782  pntlemr  23787  pntlemf  23790  pntlemk  23791  pntlemo  23792  pntlem3  23794  pntleml  23796  pnt  23799  abvcxp  23800  ostth2lem1  23803  padicabvf  23816  padicabvcxp  23817  ostth1  23818  ostth2lem2  23819  ostth2lem3  23820  ostth2lem4  23821  ostth2  23822  ostth3  23823  ostth  23824  trgcgrg  23906  ttgcontlem1  24188  brbtwn2  24208  colinearalglem4  24212  ax5seglem1  24231  ax5seglem2  24232  ax5seglem3  24234  ax5seglem5  24236  ax5seglem6  24237  ax5seglem9  24240  ax5seg  24241  axbtwnid  24242  axpaschlem  24243  axpasch  24244  axlowdimlem6  24250  axlowdimlem10  24254  axlowdimlem16  24260  axlowdim1  24262  axlowdim2  24263  axlowdim  24264  axcontlem2  24268  axcontlem4  24270  axcontlem7  24273  usgraex1elv  24397  usgraexmpldifpr  24400  spthispth  24575  constr3lem4  24647  constr3pthlem1  24655  konigsberg  24987  frgrawopreglem2  25045  frgrareg  25117  ex-dif  25144  ex-in  25146  ex-pss  25149  ex-res  25162  ex-fl  25168  nv1  25579  smcnlem  25607  ipidsq  25623  nmlno0lem  25708  norm-ii-i  26054  bcs2  26099  norm1  26167  nmopub2tALT  26828  nmfnleub2  26845  nmlnop0iALT  26914  nmopun  26933  unopbd  26934  nmopadjlem  27008  nmopcoadji  27020  pjnmopi  27067  pjbdlni  27068  stge0  27143  stle1  27144  hstle1  27145  hstle  27149  hstles  27150  stge1i  27157  stlesi  27160  staddi  27165  stadd3i  27167  strlem1  27169  strlem3a  27171  strlem5  27174  jplem1  27187  cdj1i  27352  addltmulALT  27365  xlt2addrd  27578  xdivrec  27623  xrsmulgzz  27666  xrnarchi  27728  resvbas  27822  rearchi  27832  xrge0slmod  27834  elunitrn  27879  elunitge0  27881  unitssxrge0  27882  unitdivcld  27883  xrge0iifcnv  27915  xrge0iifcv  27916  xrge0iifiso  27917  xrge0iifhom  27919  zrhre  27997  log2le1  28023  indf  28029  indfval  28030  pr01ssre  28031  esumcst  28071  hasheuni  28091  cntnevol  28199  ddemeas  28208  iwrdsplit  28326  prob01  28352  dstfrvclim1  28416  coinfliprv  28421  ballotlem2  28427  ballotlem4  28437  ballotlemi1  28441  ballotlemic  28445  sgnclre  28478  sgnnbi  28484  sgnpbi  28485  sgnmulsgp  28489  plymulx0  28504  plymulx  28505  signswch  28518  signstf  28523  signsvfn  28539  zetacvg  28557  lgamgulmlem2  28572  subfacp1lem1  28623  subfacp1lem5  28628  rescon  28691  iiscon  28697  iillyscon  28698  snmlff  28774  problem2  29020  problem3  29021  sinccvglem  29038  fz0n  29110  rerisefaccl  29139  refallfaccl  29140  sin2h  30045  cos2h  30046  tan2h  30047  itg2addnclem3  30068  asindmre  30102  dvasin  30103  dvacos  30104  dvreasin  30105  dvreacos  30106  areacirclem1  30107  fdc  30238  geomcau  30252  cntotbnd  30292  heiborlem8  30314  bfplem2  30319  bfp  30320  rabren3dioph  30749  pellexlem5  30769  pellexlem6  30770  pell1qrgaplem  30809  pell14qrgap  30811  pellqrex  30815  pellfundre  30817  pellfundlb  30820  pellfund14gap  30823  rmspecsqrtnq  30842  jm2.17a  30898  acongeq  30921  jm2.23  30938  jm3.1lem2  30960  cvgdvgrat  31194  lhe4.4ex1a  31234  binomcxplemnotnn0  31261  fprodreclf  31596  fprodge0  31597  fprodge1  31598  sumnnodd  31636  dvnprodlem3  31745  stoweidlem1  31783  stoweidlem18  31800  stoweidlem19  31801  stoweidlem26  31808  stoweidlem34  31816  stoweidlem40  31822  stoweidlem41  31823  stoweidlem59  31841  stoweid  31845  stirlinglem10  31865  stirlinglem11  31866  dirkercncflem1  31885  fourierdlem16  31905  fourierdlem21  31910  fourierdlem22  31911  fourierdlem42  31931  fourierdlem68  31957  fourierdlem83  31972  fourierdlem103  31992  sqwvfourb  32012  fouriersw  32014  etransclem23  32040  zm1nn  32325  slotsbhcdif  32559  basendxnmulrndx  32760  ene1  33168  isosctrlem1ALT  33734  bj-flbi3  34608  imo72b2  37993
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-1cn 9571  ax-icn 9572  ax-addcl 9573  ax-mulcl 9575  ax-mulrcl 9576  ax-i2m1 9581  ax-1ne0 9582  ax-rrecex 9585  ax-cnre 9586
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-uni 4250  df-br 4453  df-iota 5556  df-fv 5601  df-ov 6299
  Copyright terms: Public domain W3C validator