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

Theorem 1re 9046
Description:  1 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 9004, by exploiting properties of the imaginary unit  _i. (Contributed by Eric Schmidt, 11-Apr-2007.) (Revised by Scott Fenton, 3-Jan-2013.)
Assertion
Ref Expression
1re  |-  1  e.  RR

Proof of Theorem 1re
Dummy variables  a 
b  c  d  x  y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ax-1ne0 9015 . . 3  |-  1  =/=  0
2 ax-1cn 9004 . . . . 5  |-  1  e.  CC
3 cnre 9043 . . . . 5  |-  ( 1  e.  CC  ->  E. a  e.  RR  E. b  e.  RR  1  =  ( a  +  ( _i  x.  b ) ) )
42, 3ax-mp 8 . . . 4  |-  E. a  e.  RR  E. b  e.  RR  1  =  ( a  +  ( _i  x.  b ) )
5 neeq1 2575 . . . . . . . 8  |-  ( 1  =  ( a  +  ( _i  x.  b
) )  ->  (
1  =/=  0  <->  (
a  +  ( _i  x.  b ) )  =/=  0 ) )
65biimpcd 216 . . . . . . 7  |-  ( 1  =/=  0  ->  (
1  =  ( a  +  ( _i  x.  b ) )  -> 
( a  +  ( _i  x.  b ) )  =/=  0 ) )
7 0cn 9040 . . . . . . . 8  |-  0  e.  CC
8 cnre 9043 . . . . . . . 8  |-  ( 0  e.  CC  ->  E. c  e.  RR  E. d  e.  RR  0  =  ( c  +  ( _i  x.  d ) ) )
97, 8ax-mp 8 . . . . . . 7  |-  E. c  e.  RR  E. d  e.  RR  0  =  ( c  +  ( _i  x.  d ) )
10 neeq2 2576 . . . . . . . . . 10  |-  ( 0  =  ( c  +  ( _i  x.  d
) )  ->  (
( a  +  ( _i  x.  b ) )  =/=  0  <->  (
a  +  ( _i  x.  b ) )  =/=  ( c  +  ( _i  x.  d
) ) ) )
1110biimpcd 216 . . . . . . . . 9  |-  ( ( a  +  ( _i  x.  b ) )  =/=  0  ->  (
0  =  ( c  +  ( _i  x.  d ) )  -> 
( a  +  ( _i  x.  b ) )  =/=  ( c  +  ( _i  x.  d ) ) ) )
1211reximdv 2777 . . . . . . . 8  |-  ( ( a  +  ( _i  x.  b ) )  =/=  0  ->  ( E. d  e.  RR  0  =  ( c  +  ( _i  x.  d ) )  ->  E. d  e.  RR  ( a  +  ( _i  x.  b ) )  =/=  ( c  +  ( _i  x.  d ) ) ) )
1312reximdv 2777 . . . . . . 7  |-  ( ( a  +  ( _i  x.  b ) )  =/=  0  ->  ( E. c  e.  RR  E. d  e.  RR  0  =  ( c  +  ( _i  x.  d
) )  ->  E. c  e.  RR  E. d  e.  RR  ( a  +  ( _i  x.  b
) )  =/=  (
c  +  ( _i  x.  d ) ) ) )
146, 9, 13syl6mpi 60 . . . . . 6  |-  ( 1  =/=  0  ->  (
1  =  ( a  +  ( _i  x.  b ) )  ->  E. c  e.  RR  E. d  e.  RR  (
a  +  ( _i  x.  b ) )  =/=  ( c  +  ( _i  x.  d
) ) ) )
1514reximdv 2777 . . . . 5  |-  ( 1  =/=  0  ->  ( E. b  e.  RR  1  =  ( a  +  ( _i  x.  b ) )  ->  E. b  e.  RR  E. c  e.  RR  E. d  e.  RR  (
a  +  ( _i  x.  b ) )  =/=  ( c  +  ( _i  x.  d
) ) ) )
1615reximdv 2777 . . . 4  |-  ( 1  =/=  0  ->  ( E. a  e.  RR  E. b  e.  RR  1  =  ( a  +  ( _i  x.  b
) )  ->  E. a  e.  RR  E. b  e.  RR  E. c  e.  RR  E. d  e.  RR  ( a  +  ( _i  x.  b
) )  =/=  (
c  +  ( _i  x.  d ) ) ) )
174, 16mpi 17 . . 3  |-  ( 1  =/=  0  ->  E. a  e.  RR  E. b  e.  RR  E. c  e.  RR  E. d  e.  RR  ( a  +  ( _i  x.  b
) )  =/=  (
c  +  ( _i  x.  d ) ) )
18 ioran 477 . . . . . . . . 9  |-  ( -.  ( a  =/=  c  \/  b  =/=  d
)  <->  ( -.  a  =/=  c  /\  -.  b  =/=  d ) )
19 df-ne 2569 . . . . . . . . . . 11  |-  ( a  =/=  c  <->  -.  a  =  c )
2019con2bii 323 . . . . . . . . . 10  |-  ( a  =  c  <->  -.  a  =/=  c )
21 df-ne 2569 . . . . . . . . . . 11  |-  ( b  =/=  d  <->  -.  b  =  d )
2221con2bii 323 . . . . . . . . . 10  |-  ( b  =  d  <->  -.  b  =/=  d )
2320, 22anbi12i 679 . . . . . . . . 9  |-  ( ( a  =  c  /\  b  =  d )  <->  ( -.  a  =/=  c  /\  -.  b  =/=  d
) )
2418, 23bitr4i 244 . . . . . . . 8  |-  ( -.  ( a  =/=  c  \/  b  =/=  d
)  <->  ( a  =  c  /\  b  =  d ) )
25 id 20 . . . . . . . . 9  |-  ( a  =  c  ->  a  =  c )
26 oveq2 6048 . . . . . . . . 9  |-  ( b  =  d  ->  (
_i  x.  b )  =  ( _i  x.  d ) )
2725, 26oveqan12d 6059 . . . . . . . 8  |-  ( ( a  =  c  /\  b  =  d )  ->  ( a  +  ( _i  x.  b ) )  =  ( c  +  ( _i  x.  d ) ) )
2824, 27sylbi 188 . . . . . . 7  |-  ( -.  ( a  =/=  c  \/  b  =/=  d
)  ->  ( a  +  ( _i  x.  b ) )  =  ( c  +  ( _i  x.  d ) ) )
2928necon1ai 2609 . . . . . 6  |-  ( ( a  +  ( _i  x.  b ) )  =/=  ( c  +  ( _i  x.  d
) )  ->  (
a  =/=  c  \/  b  =/=  d ) )
30 neeq1 2575 . . . . . . . . . 10  |-  ( x  =  a  ->  (
x  =/=  y  <->  a  =/=  y ) )
31 neeq2 2576 . . . . . . . . . 10  |-  ( y  =  c  ->  (
a  =/=  y  <->  a  =/=  c ) )
3230, 31rspc2ev 3020 . . . . . . . . 9  |-  ( ( a  e.  RR  /\  c  e.  RR  /\  a  =/=  c )  ->  E. x  e.  RR  E. y  e.  RR  x  =/=  y
)
33323expia 1155 . . . . . . . 8  |-  ( ( a  e.  RR  /\  c  e.  RR )  ->  ( a  =/=  c  ->  E. x  e.  RR  E. y  e.  RR  x  =/=  y ) )
3433ad2ant2r 728 . . . . . . 7  |-  ( ( ( a  e.  RR  /\  b  e.  RR )  /\  ( c  e.  RR  /\  d  e.  RR ) )  -> 
( a  =/=  c  ->  E. x  e.  RR  E. y  e.  RR  x  =/=  y ) )
35 neeq1 2575 . . . . . . . . . 10  |-  ( x  =  b  ->  (
x  =/=  y  <->  b  =/=  y ) )
36 neeq2 2576 . . . . . . . . . 10  |-  ( y  =  d  ->  (
b  =/=  y  <->  b  =/=  d ) )
3735, 36rspc2ev 3020 . . . . . . . . 9  |-  ( ( b  e.  RR  /\  d  e.  RR  /\  b  =/=  d )  ->  E. x  e.  RR  E. y  e.  RR  x  =/=  y
)
38373expia 1155 . . . . . . . 8  |-  ( ( b  e.  RR  /\  d  e.  RR )  ->  ( b  =/=  d  ->  E. x  e.  RR  E. y  e.  RR  x  =/=  y ) )
3938ad2ant2l 727 . . . . . . 7  |-  ( ( ( a  e.  RR  /\  b  e.  RR )  /\  ( c  e.  RR  /\  d  e.  RR ) )  -> 
( b  =/=  d  ->  E. x  e.  RR  E. y  e.  RR  x  =/=  y ) )
4034, 39jaod 370 . . . . . 6  |-  ( ( ( a  e.  RR  /\  b  e.  RR )  /\  ( c  e.  RR  /\  d  e.  RR ) )  -> 
( ( a  =/=  c  \/  b  =/=  d )  ->  E. x  e.  RR  E. y  e.  RR  x  =/=  y
) )
4129, 40syl5 30 . . . . 5  |-  ( ( ( a  e.  RR  /\  b  e.  RR )  /\  ( c  e.  RR  /\  d  e.  RR ) )  -> 
( ( a  +  ( _i  x.  b
) )  =/=  (
c  +  ( _i  x.  d ) )  ->  E. x  e.  RR  E. y  e.  RR  x  =/=  y ) )
4241rexlimdvva 2797 . . . 4  |-  ( ( a  e.  RR  /\  b  e.  RR )  ->  ( E. c  e.  RR  E. d  e.  RR  ( a  +  ( _i  x.  b
) )  =/=  (
c  +  ( _i  x.  d ) )  ->  E. x  e.  RR  E. y  e.  RR  x  =/=  y ) )
4342rexlimivv 2795 . . 3  |-  ( E. a  e.  RR  E. b  e.  RR  E. c  e.  RR  E. d  e.  RR  ( a  +  ( _i  x.  b
) )  =/=  (
c  +  ( _i  x.  d ) )  ->  E. x  e.  RR  E. y  e.  RR  x  =/=  y )
441, 17, 43mp2b 10 . 2  |-  E. x  e.  RR  E. y  e.  RR  x  =/=  y
45 eqtr3 2423 . . . . . . . . 9  |-  ( ( x  =  0  /\  y  =  0 )  ->  x  =  y )
4645ex 424 . . . . . . . 8  |-  ( x  =  0  ->  (
y  =  0  ->  x  =  y )
)
4746necon3d 2605 . . . . . . 7  |-  ( x  =  0  ->  (
x  =/=  y  -> 
y  =/=  0 ) )
48 neeq1 2575 . . . . . . . . 9  |-  ( z  =  y  ->  (
z  =/=  0  <->  y  =/=  0 ) )
4948rspcev 3012 . . . . . . . 8  |-  ( ( y  e.  RR  /\  y  =/=  0 )  ->  E. z  e.  RR  z  =/=  0 )
5049expcom 425 . . . . . . 7  |-  ( y  =/=  0  ->  (
y  e.  RR  ->  E. z  e.  RR  z  =/=  0 ) )
5147, 50syl6 31 . . . . . 6  |-  ( x  =  0  ->  (
x  =/=  y  -> 
( y  e.  RR  ->  E. z  e.  RR  z  =/=  0 ) ) )
5251com23 74 . . . . 5  |-  ( x  =  0  ->  (
y  e.  RR  ->  ( x  =/=  y  ->  E. z  e.  RR  z  =/=  0 ) ) )
5352adantld 454 . . . 4  |-  ( x  =  0  ->  (
( x  e.  RR  /\  y  e.  RR )  ->  ( x  =/=  y  ->  E. z  e.  RR  z  =/=  0
) ) )
54 neeq1 2575 . . . . . . . 8  |-  ( z  =  x  ->  (
z  =/=  0  <->  x  =/=  0 ) )
5554rspcev 3012 . . . . . . 7  |-  ( ( x  e.  RR  /\  x  =/=  0 )  ->  E. z  e.  RR  z  =/=  0 )
5655expcom 425 . . . . . 6  |-  ( x  =/=  0  ->  (
x  e.  RR  ->  E. z  e.  RR  z  =/=  0 ) )
5756adantrd 455 . . . . 5  |-  ( x  =/=  0  ->  (
( x  e.  RR  /\  y  e.  RR )  ->  E. z  e.  RR  z  =/=  0 ) )
5857a1dd 44 . . . 4  |-  ( x  =/=  0  ->  (
( x  e.  RR  /\  y  e.  RR )  ->  ( x  =/=  y  ->  E. z  e.  RR  z  =/=  0
) ) )
5953, 58pm2.61ine 2643 . . 3  |-  ( ( x  e.  RR  /\  y  e.  RR )  ->  ( x  =/=  y  ->  E. z  e.  RR  z  =/=  0 ) )
6059rexlimivv 2795 . 2  |-  ( E. x  e.  RR  E. y  e.  RR  x  =/=  y  ->  E. z  e.  RR  z  =/=  0
)
61 ax-rrecex 9018 . . . 4  |-  ( ( z  e.  RR  /\  z  =/=  0 )  ->  E. x  e.  RR  ( z  x.  x
)  =  1 )
62 remulcl 9031 . . . . . . 7  |-  ( ( z  e.  RR  /\  x  e.  RR )  ->  ( z  x.  x
)  e.  RR )
6362adantlr 696 . . . . . 6  |-  ( ( ( z  e.  RR  /\  z  =/=  0 )  /\  x  e.  RR )  ->  ( z  x.  x )  e.  RR )
64 eleq1 2464 . . . . . 6  |-  ( ( z  x.  x )  =  1  ->  (
( z  x.  x
)  e.  RR  <->  1  e.  RR ) )
6563, 64syl5ibcom 212 . . . . 5  |-  ( ( ( z  e.  RR  /\  z  =/=  0 )  /\  x  e.  RR )  ->  ( ( z  x.  x )  =  1  ->  1  e.  RR ) )
6665rexlimdva 2790 . . . 4  |-  ( ( z  e.  RR  /\  z  =/=  0 )  -> 
( E. x  e.  RR  ( z  x.  x )  =  1  ->  1  e.  RR ) )
6761, 66mpd 15 . . 3  |-  ( ( z  e.  RR  /\  z  =/=  0 )  -> 
1  e.  RR )
6867rexlimiva 2785 . 2  |-  ( E. z  e.  RR  z  =/=  0  ->  1  e.  RR )
6944, 60, 68mp2b 10 1  |-  1  e.  RR
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    \/ wo 358    /\ wa 359    = wceq 1649    e. wcel 1721    =/= wne 2567   E.wrex 2667  (class class class)co 6040   CCcc 8944   RRcr 8945   0cc0 8946   1c1 8947   _ici 8948    + caddc 8949    x. cmul 8951
This theorem is referenced by:  0re  9047  peano2re  9195  mul02lem2  9199  addid1  9202  renegcl  9320  peano2rem  9323  0reALT  9353  0lt1  9506  0le1  9507  1le1  9606  eqneg  9690  ltp1  9804  ltm1  9806  recgt0  9810  mulgt1  9825  ltmulgt11  9826  lemulge11  9828  ltrec  9847  reclt1  9861  recgt1  9862  recgt1i  9863  recp1lt1  9864  recreclt  9865  recgt0ii  9872  ledivp1i  9892  ltdivp1i  9893  inelr  9946  cju  9952  nnssre  9960  nnge1  9982  nngt1ne1  9983  nnle1eq1  9984  nngt0  9985  nnnlt1  9986  nnrecre  9992  nnrecgt0  9993  nnsub  9994  2re  10025  3re  10027  4re  10029  5re  10031  6re  10032  7re  10033  8re  10034  9re  10035  10re  10036  2pos  10038  3pos  10040  4pos  10042  5pos  10043  6pos  10044  7pos  10045  8pos  10046  9pos  10047  10pos  10048  1lt2  10098  1lt3  10100  1lt4  10103  1lt5  10107  1lt6  10112  1lt7  10118  1lt8  10125  1lt9  10133  1lt10  10142  1ne2  10143  halflt1  10145  addltmul  10159  nnunb  10173  elnnnn0c  10221  elnnz1  10263  znnnlt1  10264  zltp1le  10281  zleltp1  10282  recnz  10301  gtndiv  10303  suprzcl  10305  uzindOLD  10320  eluzp1m1  10465  eluzp1p1  10467  eluz2b2  10504  zbtwnre  10528  rebtwnz  10529  1rp  10572  qbtwnre  10741  qbtwnxr  10742  xmulid1  10814  xmulid2  10815  xmulm1  10816  x2times  10834  xrub  10846  0elunit  10971  1elunit  10972  lincmb01cmp  10994  iccf1o  10995  xov1plusxeqvd  10997  unitssre  10998  fztpval  11063  4fvwrd4  11076  elfznelfzo  11147  elfznelfzob  11148  fraclt1  11166  fracle1  11167  flbi2  11179  fladdz  11182  flhalf  11186  fldiv  11196  modid  11225  1mod  11228  seqf1olem1  11317  reexpcl  11353  reexpclz  11356  expge0  11371  expge1  11372  expgt1  11373  ltexp2a  11386  expcan  11387  ltexp2  11388  leexp2  11389  leexp2a  11390  leexp2r  11392  nnlesq  11439  bernneq  11460  bernneq2  11461  bernneq3  11462  expnbnd  11463  expnlbnd  11464  expnlbnd2  11465  expmulnbnd  11466  discr1  11470  facwordi  11535  faclbnd3  11538  faclbnd4lem1  11539  faclbnd4lem4  11542  faclbnd6  11545  facavg  11547  hashv01gt1  11584  hashge1  11618  hashnn0n0nn  11619  hash1snb  11636  hashgt12el  11637  hashgt12el2  11638  fzsdom2  11648  hashfun  11655  brfi1uzind  11670  f1oun2prg  11819  crre  11874  remim  11877  cjexp  11910  re1  11914  im1  11915  rei  11916  imi  11917  sqrlem1  12003  sqrlem2  12004  sqrlem3  12005  sqrlem4  12006  sqrlem7  12009  resqrex  12011  sqr1  12032  sqr2gt1lt2  12035  sqrm1  12036  abs1  12057  rddif  12099  absrdbnd  12100  caubnd2  12116  mulcn2  12344  reccn2  12345  rlimo1  12365  rlimno1  12402  iseraltlem2  12431  iseraltlem3  12432  iseralt  12433  o1fsum  12547  abscvgcvg  12553  climcndslem1  12584  climcndslem2  12585  flo1  12589  harmonic  12593  expcnv  12598  geolim  12602  geolim2  12603  georeclim  12604  geo2lim  12607  geomulcvg  12608  geoisumr  12610  geoisum1c  12612  geoihalfsum  12614  efcllem  12635  ere  12646  ege2le3  12647  efgt1  12672  resin4p  12694  recos4p  12695  tanhlt1  12716  tanhbnd  12717  sinbnd  12736  cosbnd  12737  sinbnd2  12738  cosbnd2  12739  ef01bndlem  12740  sin01bnd  12741  cos01bnd  12742  cos1bnd  12743  cos2bnd  12744  sinltx  12745  sin01gt0  12746  cos01gt0  12747  sin02gt0  12748  sincos1sgn  12749  eirrlem  12758  rpnnen2lem2  12770  rpnnen2lem3  12771  rpnnen2lem4  12772  rpnnen2lem9  12777  rpnnen2  12780  ruclem6  12789  ruclem11  12794  ruclem12  12795  nthruz  12806  3dvds  12867  bitsfzolem  12901  bitsfzo  12902  bitsmod  12903  bitscmp  12905  bitsinv1lem  12908  sadcadd  12925  smuval2  12949  isprm3  13043  prmind2  13045  sqnprm  13053  coprm  13055  isprm5  13067  divdenle  13096  zsqrelqelz  13105  phibndlem  13114  fermltl  13128  odzdvds  13136  pythagtriplem3  13147  iserodd  13164  pcmpt  13216  fldivp1  13221  pcfaclem  13222  pockthi  13230  infpn2  13236  prmreclem1  13239  prmreclem5  13243  4sqlem11  13278  4sqlem12  13279  ramub1lem1  13349  2expltfac  13381  resslem  13477  oppcbas  13899  rescbas  13984  rescabs  13988  odubas  14515  lt6abl  15459  pgpfaclem2  15595  abvneg  15877  abvtrivd  15883  xrsmcmn  16679  resubdrg  16705  gzrngunitlem  16718  gzrngunit  16719  znidomb  16797  thlbas  16878  leordtval2  17230  tuslem  18250  setsmsbas  18458  dscmet  18573  dscopn  18574  nrginvrcnlem  18679  nmoid  18729  idnghm  18730  tgioo  18780  blcvx  18782  xrsmopn  18796  metnrmlem1a  18841  metnrmlem1  18842  iicmp  18869  iicon  18870  iirev  18907  iihalf1  18909  iihalf1cn  18910  iihalf2  18911  iihalf2cn  18912  elii1  18913  elii2  18914  iimulcl  18915  icopnfcnv  18920  icopnfhmeo  18921  iccpnfcnv  18922  iccpnfhmeo  18923  xrhmeo  18924  xrhmph  18925  evth  18937  xlebnum  18943  lebnumii  18944  htpycc  18958  reparphti  18975  pcoval1  18991  pco0  18992  pco1  18993  pcoval2  18994  pcocn  18995  pcohtpylem  18997  pcopt  19000  pcopt2  19001  pcoass  19002  pcorevlem  19004  nmhmcn  19081  cncmet  19228  ovolunlem1a  19345  ovoliunlem1  19351  dyadmaxlem  19442  vitalilem2  19454  vitalilem4  19456  vitalilem5  19457  vitali  19458  mbfneg  19495  i1f1  19535  itg11  19536  i1fsub  19553  itg1sub  19554  mbfi1fseqlem6  19565  itg2const  19585  itg2mulc  19592  itg2monolem1  19595  itg2monolem3  19597  iblcnlem1  19632  i1fibl  19652  itgitg1  19653  dveflem  19816  mvth  19829  dvlipcn  19831  lhop1lem  19850  dvcvx  19857  dvfsumlem1  19863  dvfsumlem2  19864  dvfsumlem3  19865  dvfsumlem4  19866  dvfsum2  19871  ply1remlem  20038  fta1glem2  20042  fta1blem  20044  plyeq0lem  20082  fta1lem  20177  vieta1lem2  20181  aalioulem3  20204  aalioulem4  20205  aalioulem5  20206  aaliou3lem2  20213  aaliou3lem8  20215  ulmbdd  20267  iblulm  20276  radcnvlem1  20282  radcnvlem2  20283  dvradcnv  20290  abelthlem2  20301  abelthlem3  20302  abelthlem5  20304  abelthlem7  20307  abelth  20310  abelth2  20311  reeff1olem  20315  reeff1o  20316  sinhalfpilem  20327  tangtx  20366  sincos4thpi  20374  pige3  20378  coskpi  20381  cosne0  20385  recosf1o  20390  tanregt0  20394  efif1olem3  20399  efif1olem4  20400  loge  20434  rplogcl  20452  logdivlti  20468  logno1  20480  logcnlem4  20489  logf1o2  20494  dvlog2lem  20496  advlog  20498  logtayllem  20503  logtayl  20504  logccv  20507  recxpcl  20519  cxplt  20538  cxple  20539  cxplea  20540  cxpsqrlem  20546  cxpsqr  20547  cxpcn3lem  20584  cxpaddlelem  20588  cxpaddle  20589  loglesqr  20595  ang180lem1  20604  ang180lem2  20605  ang180lem3  20606  isosctrlem1  20615  isosctrlem2  20616  angpined  20624  chordthmlem4  20629  1cubrlem  20634  atanre  20678  asinsin  20685  acosrecl  20696  atandmcj  20702  atancj  20703  atanlogaddlem  20706  atantan  20716  bndatandm  20722  atans2  20724  ressatans  20727  leibpilem2  20734  leibpi  20735  leibpisum  20736  log2tlbnd  20738  birthdaylem3  20745  birthday  20746  rlimcnp  20757  rlimcnp2  20758  efrlim  20761  cxp2limlem  20767  cxp2lim  20768  cxploglim  20769  cxploglim2  20770  divsqrsumlem  20771  divsqrsumo1  20775  cvxcl  20776  scvxcvx  20777  jensenlem2  20779  amgmlem  20781  logdiflbnd  20786  emcllem2  20788  emcllem4  20790  emcllem6  20792  emcllem7  20793  emre  20797  emgt0  20798  harmonicbnd3  20799  harmonicubnd  20801  harmonicbnd4  20802  fsumharmonic  20803  wilthlem1  20804  wilthlem2  20805  ftalem1  20808  ftalem2  20809  ftalem5  20812  basellem3  20818  basellem9  20824  issqf  20872  cht1  20901  vma1  20902  chp1  20903  ppieq0  20912  ppiltx  20913  mumullem2  20916  fsumfldivdiaglem  20927  ppiublem1  20939  ppiub  20941  chpeq0  20945  chtublem  20948  chtub  20949  chpval2  20955  chpchtsum  20956  chpub  20957  logfacbnd3  20960  logfacrlim  20961  logexprlim  20962  mersenne  20964  perfectlem2  20967  dchrelbas4  20980  dchrinv  20998  dchr1re  21000  bcmono  21014  efexple  21018  bposlem1  21021  bposlem2  21022  bposlem5  21025  bposlem8  21028  lgslem3  21035  lgslem4  21036  lgsvalmod  21052  lgsmod  21058  lgsdir2lem1  21060  lgsdir2lem3  21062  lgsdir2lem4  21063  lgsdir2lem5  21064  lgsdirprm  21066  lgsdir  21067  lgsne0  21070  lgsabs1  21071  lgsdinn0  21077  lgseisen  21090  lgsquadlem2  21092  m1lgs  21099  2sqlem8  21109  chebbnd1lem1  21116  chebbnd1lem2  21117  chebbnd1lem3  21118  chebbnd1  21119  chtppilimlem1  21120  chtppilimlem2  21121  chtppilim  21122  chebbnd2  21124  chto1lb  21125  chpchtlim  21126  chpo1ubb  21128  vmadivsum  21129  vmadivsumb  21130  rplogsumlem1  21131  rplogsumlem2  21132  rpvmasumlem  21134  dchrisumlem3  21138  dchrmusumlema  21140  dchrmusum2  21141  dchrvmasumlem2  21145  dchrvmasumlem3  21146  dchrvmasumiflem1  21148  dchrvmasumiflem2  21149  dchrisum0flblem1  21155  dchrisum0flblem2  21156  dchrisum0fno1  21158  rpvmasum2  21159  dchrisum0re  21160  dchrisum0lema  21161  dchrisum0lem1b  21162  dchrisum0lem1  21163  dchrisum0lem2a  21164  dchrisum0lem2  21165  dchrisum0lem3  21166  rplogsum  21174  dirith2  21175  mudivsum  21177  mulogsumlem  21178  mulogsum  21179  logdivsum  21180  mulog2sumlem1  21181  mulog2sumlem2  21182  vmalogdivsum2  21185  2vmadivsumlem  21187  log2sumbnd  21191  selberglem2  21193  selbergb  21196  selberg2lem  21197  selberg2b  21199  chpdifbndlem1  21200  chpdifbnd  21202  selberg3lem1  21204  selberg3lem2  21205  selberg4lem1  21207  pntrmax  21211  pntrsumo1  21212  pntrsumbnd  21213  selberg34r  21218  selbergsb  21222  pntrlog2bndlem1  21224  pntrlog2bndlem2  21225  pntrlog2bndlem3  21226  pntrlog2bndlem4  21227  pntrlog2bndlem5  21228  pntrlog2bndlem6  21230  pntrlog2bnd  21231  pntpbnd1a  21232  pntpbnd1  21233  pntpbnd2  21234  pntibndlem1  21236  pntibndlem2a  21237  pntibndlem2  21238  pntibndlem3  21239  pntibnd  21240  pntlemd  21241  pntlemc  21242  pntlemb  21244  pntlemg  21245  pntlemr  21249  pntlemf  21252  pntlemk  21253  pntlemo  21254  pntlem3  21256  pntleml  21258  pnt  21261  abvcxp  21262  ostth2lem1  21265  qabvle  21272  padicabvf  21278  padicabvcxp  21279  ostth1  21280  ostth2lem2  21281  ostth2lem3  21282  ostth2lem4  21283  ostth2  21284  ostth3  21285  ostth  21286  usgraex1elv  21369  usgraexmpldifpr  21372  spthispth  21526  constr3lem4  21587  constr3pthlem1  21595  constr3pthlem3  21597  konigsberg  21662  ex-dif  21684  ex-in  21686  ex-pss  21689  ex-res  21702  ex-fl  21708  nv1  22118  smcnlem  22146  ipidsq  22162  nmoub3i  22227  nmlno0lem  22247  blocnilem  22258  ipasslem10  22293  ubthlem2  22326  minvecolem4  22335  htthlem  22373  hisubcomi  22559  normlem9  22573  norm-ii-i  22592  bcs2  22637  norm1  22704  nmopub2tALT  23365  nmfnleub2  23382  nmlnop0iALT  23451  nmopun  23470  unopbd  23471  hmopd  23478  nmcexi  23482  nmopadjlem  23545  nmopcoi  23551  nmopcoadji  23557  opsqrlem4  23599  pjnmopi  23604  pjbdlni  23605  stge0  23680  stle1  23681  hstle1  23682  hstle  23686  hstles  23687  stge1i  23694  stlesi  23697  staddi  23702  stadd3i  23704  strlem1  23706  strlem3a  23708  strlem5  23711  jplem1  23724  cdj1i  23889  addltmulALT  23902  xlt2addrd  24077  fzsplit3  24103  xdivrec  24126  xrsmulgzz  24153  xrnarchi  24207  remulg  24223  elunitrn  24248  elunitge0  24250  unitssxrge0  24251  unitdivcld  24252  sqsscirc1  24259  xrge0iifcnv  24272  xrge0iifcv  24273  xrge0iifiso  24274  xrge0iifhom  24276  zrhre  24338  rnlogblem  24352  log2le1  24360  indf  24366  indfval  24367  pr01ssre  24368  indf1o  24374  esumcst  24408  esumdivc  24426  hasheuni  24428  cntnevol  24535  dya2ub  24573  dya2iocress  24577  dya2iocbrsiga  24578  dya2icobrsiga  24579  dya2icoseg  24580  dya2iocucvr  24587  sxbrsigalem2  24589  prob01  24624  probmeasb  24641  dstrvprob  24682  dstfrvunirn  24685  dstfrvclim1  24688  coinfliprv  24693  ballotlem2  24699  ballotlemfc0  24703  ballotlemfcc  24704  ballotlem4  24709  ballotlemi1  24713  ballotlemic  24717  ballotlem1c  24718  ballotlemsgt1  24721  ballotlemsel1i  24723  ballotlemfrcn0  24740  zetacvg  24752  lgamgulmlem2  24767  lgamgulmlem3  24768  lgamgulmlem4  24769  lgamgulmlem5  24770  lgamgulmlem6  24771  lgamcvg2  24792  regamcl  24798  subfacp1lem1  24818  subfacp1lem5  24823  subfacval2  24826  subfaclim  24827  subfacval3  24828  rescon  24886  iiscon  24892  iillyscon  24893  cvmliftlem2  24926  cvmliftlem13  24936  snmlff  24969  sinccvglem  25062  divelunit  25138  dedekind  25140  relin01  25147  fznatpl1  25151  fz0n  25155  fprodrecl  25232  rerisefaccl  25285  refallfaccl  25286  risefall0lem  25294  binomfallfaclem2  25307  faclim  25313  brbtwn2  25748  colinearalglem4  25752  ax5seglem1  25771  ax5seglem2  25772  ax5seglem3  25774  ax5seglem5  25776  ax5seglem6  25777  ax5seglem9  25780  ax5seg  25781  axbtwnid  25782  axpaschlem  25783  axpasch  25784  axlowdimlem3  25787  axlowdimlem6  25790  axlowdimlem7  25791  axlowdimlem10  25794  axlowdimlem16  25800  axlowdimlem17  25801  axlowdim1  25802  axlowdim2  25803  axlowdim  25804  axcontlem2  25808  axcontlem4  25810  axcontlem7  25813  bpoly4  26009  itg2addnclem2  26156  itg2addnclem3  26157  dvreasin  26179  dvreacos  26180  areacirclem2  26181  areacirclem5  26185  nn0prpwlem  26215  fdc  26339  incsequz  26342  geomcau  26355  totbndbnd  26388  cntotbnd  26395  heiborlem8  26417  bfplem2  26422  bfp  26423  lzenom  26718  rabren3dioph  26766  irrapxlem1  26775  irrapxlem2  26776  irrapxlem4  26778  irrapxlem5  26779  pellexlem2  26783  pellexlem5  26786  pellexlem6  26787  pell1qrge1  26823  pell1qr1  26824  elpell1qr2  26825  pell1qrgaplem  26826  pell14qrgap  26828  pell14qrgapw  26829  pellqrex  26832  pellfundre  26834  pellfundgt1  26836  pellfundlb  26837  pellfundglb  26838  pellfundex  26839  pellfund14gap  26840  pellfundrp  26841  pellfundne1  26842  rmspecsqrnq  26859  rmspecnonsq  26860  rmspecfund  26862  rmspecpos  26869  monotoddzzfi  26895  jm2.17a  26915  rmygeid  26919  acongeq  26938  jm2.23  26957  jm3.1lem2  26979  matbas  27336  lhe4.4ex1a  27414  fmul01  27577  fmul01lt1lem1  27581  fmul01lt1lem2  27582  climsuselem1  27600  stoweidlem1  27617  stoweidlem5  27621  stoweidlem7  27623  stoweidlem10  27626  stoweidlem11  27627  stoweidlem12  27628  stoweidlem13  27629  stoweidlem14  27630  stoweidlem16  27632  stoweidlem18  27634  stoweidlem19  27635  stoweidlem20  27636  stoweidlem22  27638  stoweidlem24  27640  stoweidlem25  27641  stoweidlem26  27642  stoweidlem28  27644  stoweidlem34  27650  stoweidlem36  27652  stoweidlem38  27654  stoweidlem40  27656  stoweidlem41  27657  stoweidlem42  27658  stoweidlem45  27661  stoweidlem51  27667  stoweidlem59  27675  stoweidlem60  27676  stoweid  27679  wallispilem3  27683  wallispilem4  27684  wallispilem5  27685  wallispi  27686  wallispi2lem1  27687  wallispi2lem2  27688  wallispi2  27689  stirlinglem1  27690  stirlinglem3  27692  stirlinglem5  27694  stirlinglem6  27695  stirlinglem7  27696  stirlinglem8  27697  stirlinglem10  27699  stirlinglem11  27700  stirlinglem12  27701  stirlinglem13  27702  stirlinglem15  27704  sigaradd  27723  ubmelm1fzo  27987  euhash1  27998  usgra2pthlem1  28040  frgrawopreglem2  28148  reseccl  28210  recsccl  28211  sgn1  28236  ene1  28245
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-1cn 9004  ax-icn 9005  ax-addcl 9006  ax-mulcl 9008  ax-mulrcl 9009  ax-i2m1 9014  ax-1ne0 9015  ax-rrecex 9018  ax-cnre 9019
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-ral 2671  df-rex 2672  df-rab 2675  df-v 2918  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-uni 3976  df-br 4173  df-iota 5377  df-fv 5421  df-ov 6043
  Copyright terms: Public domain W3C validator