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

Theorem 1re 8805
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 8763, 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
StepHypRef Expression
1 ax-1ne0 8774 . . 3  |-  1  =/=  0
2 ax-1cn 8763 . . . . 5  |-  1  e.  CC
3 ax-cnre 8778 . . . . 5  |-  ( 1  e.  CC  ->  E. a  e.  RR  E. b  e.  RR  1  =  ( a  +  ( _i  x.  b ) ) )
42, 3ax-mp 10 . . . 4  |-  E. a  e.  RR  E. b  e.  RR  1  =  ( a  +  ( _i  x.  b ) )
5 neeq1 2429 . . . . . . . 8  |-  ( 1  =  ( a  +  ( _i  x.  b
) )  ->  (
1  =/=  0  <->  (
a  +  ( _i  x.  b ) )  =/=  0 ) )
65biimpcd 217 . . . . . . 7  |-  ( 1  =/=  0  ->  (
1  =  ( a  +  ( _i  x.  b ) )  -> 
( a  +  ( _i  x.  b ) )  =/=  0 ) )
7 0cn 8799 . . . . . . . 8  |-  0  e.  CC
8 ax-cnre 8778 . . . . . . . 8  |-  ( 0  e.  CC  ->  E. c  e.  RR  E. d  e.  RR  0  =  ( c  +  ( _i  x.  d ) ) )
97, 8ax-mp 10 . . . . . . 7  |-  E. c  e.  RR  E. d  e.  RR  0  =  ( c  +  ( _i  x.  d ) )
10 neeq2 2430 . . . . . . . . . 10  |-  ( 0  =  ( c  +  ( _i  x.  d
) )  ->  (
( a  +  ( _i  x.  b ) )  =/=  0  <->  (
a  +  ( _i  x.  b ) )  =/=  ( c  +  ( _i  x.  d
) ) ) )
1110biimpcd 217 . . . . . . . . 9  |-  ( ( a  +  ( _i  x.  b ) )  =/=  0  ->  (
0  =  ( c  +  ( _i  x.  d ) )  -> 
( a  +  ( _i  x.  b ) )  =/=  ( c  +  ( _i  x.  d ) ) ) )
1211reximdv 2629 . . . . . . . 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 2629 . . . . . . 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 2629 . . . . 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 2629 . . . 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 18 . . 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 478 . . . . . . . . 9  |-  ( -.  ( a  =/=  c  \/  b  =/=  d
)  <->  ( -.  a  =/=  c  /\  -.  b  =/=  d ) )
19 df-ne 2423 . . . . . . . . . . 11  |-  ( a  =/=  c  <->  -.  a  =  c )
2019con2bii 324 . . . . . . . . . 10  |-  ( a  =  c  <->  -.  a  =/=  c )
21 df-ne 2423 . . . . . . . . . . 11  |-  ( b  =/=  d  <->  -.  b  =  d )
2221con2bii 324 . . . . . . . . . 10  |-  ( b  =  d  <->  -.  b  =/=  d )
2320, 22anbi12i 681 . . . . . . . . 9  |-  ( ( a  =  c  /\  b  =  d )  <->  ( -.  a  =/=  c  /\  -.  b  =/=  d
) )
2418, 23bitr4i 245 . . . . . . . 8  |-  ( -.  ( a  =/=  c  \/  b  =/=  d
)  <->  ( a  =  c  /\  b  =  d ) )
25 id 21 . . . . . . . . 9  |-  ( a  =  c  ->  a  =  c )
26 oveq2 5800 . . . . . . . . 9  |-  ( b  =  d  ->  (
_i  x.  b )  =  ( _i  x.  d ) )
2725, 26oveqan12d 5811 . . . . . . . 8  |-  ( ( a  =  c  /\  b  =  d )  ->  ( a  +  ( _i  x.  b ) )  =  ( c  +  ( _i  x.  d ) ) )
2824, 27sylbi 189 . . . . . . 7  |-  ( -.  ( a  =/=  c  \/  b  =/=  d
)  ->  ( a  +  ( _i  x.  b ) )  =  ( c  +  ( _i  x.  d ) ) )
2928necon1ai 2463 . . . . . 6  |-  ( ( a  +  ( _i  x.  b ) )  =/=  ( c  +  ( _i  x.  d
) )  ->  (
a  =/=  c  \/  b  =/=  d ) )
30 neeq1 2429 . . . . . . . . . 10  |-  ( x  =  a  ->  (
x  =/=  y  <->  a  =/=  y ) )
31 neeq2 2430 . . . . . . . . . 10  |-  ( y  =  c  ->  (
a  =/=  y  <->  a  =/=  c ) )
3230, 31rcla42ev 2867 . . . . . . . . 9  |-  ( ( a  e.  RR  /\  c  e.  RR  /\  a  =/=  c )  ->  E. x  e.  RR  E. y  e.  RR  x  =/=  y
)
33323expia 1158 . . . . . . . 8  |-  ( ( a  e.  RR  /\  c  e.  RR )  ->  ( a  =/=  c  ->  E. x  e.  RR  E. y  e.  RR  x  =/=  y ) )
3433ad2ant2r 730 . . . . . . 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 2429 . . . . . . . . . 10  |-  ( x  =  b  ->  (
x  =/=  y  <->  b  =/=  y ) )
36 neeq2 2430 . . . . . . . . . 10  |-  ( y  =  d  ->  (
b  =/=  y  <->  b  =/=  d ) )
3735, 36rcla42ev 2867 . . . . . . . . 9  |-  ( ( b  e.  RR  /\  d  e.  RR  /\  b  =/=  d )  ->  E. x  e.  RR  E. y  e.  RR  x  =/=  y
)
38373expia 1158 . . . . . . . 8  |-  ( ( b  e.  RR  /\  d  e.  RR )  ->  ( b  =/=  d  ->  E. x  e.  RR  E. y  e.  RR  x  =/=  y ) )
3938ad2ant2l 729 . . . . . . 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 371 . . . . . 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 2649 . . . 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 2647 . . 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 11 . 2  |-  E. x  e.  RR  E. y  e.  RR  x  =/=  y
45 eqtr3 2277 . . . . . . . . 9  |-  ( ( x  =  0  /\  y  =  0 )  ->  x  =  y )
4645ex 425 . . . . . . . 8  |-  ( x  =  0  ->  (
y  =  0  ->  x  =  y )
)
4746necon3d 2459 . . . . . . 7  |-  ( x  =  0  ->  (
x  =/=  y  -> 
y  =/=  0 ) )
48 neeq1 2429 . . . . . . . . 9  |-  ( z  =  y  ->  (
z  =/=  0  <->  y  =/=  0 ) )
4948rcla4ev 2859 . . . . . . . 8  |-  ( ( y  e.  RR  /\  y  =/=  0 )  ->  E. z  e.  RR  z  =/=  0 )
5049expcom 426 . . . . . . 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 455 . . . 4  |-  ( x  =  0  ->  (
( x  e.  RR  /\  y  e.  RR )  ->  ( x  =/=  y  ->  E. z  e.  RR  z  =/=  0
) ) )
54 neeq1 2429 . . . . . . . 8  |-  ( z  =  x  ->  (
z  =/=  0  <->  x  =/=  0 ) )
5554rcla4ev 2859 . . . . . . 7  |-  ( ( x  e.  RR  /\  x  =/=  0 )  ->  E. z  e.  RR  z  =/=  0 )
5655expcom 426 . . . . . 6  |-  ( x  =/=  0  ->  (
x  e.  RR  ->  E. z  e.  RR  z  =/=  0 ) )
5756adantrd 456 . . . . 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 2497 . . 3  |-  ( ( x  e.  RR  /\  y  e.  RR )  ->  ( x  =/=  y  ->  E. z  e.  RR  z  =/=  0 ) )
6059rexlimivv 2647 . 2  |-  ( E. x  e.  RR  E. y  e.  RR  x  =/=  y  ->  E. z  e.  RR  z  =/=  0
)
61 ax-rrecex 8777 . . . 4  |-  ( ( z  e.  RR  /\  z  =/=  0 )  ->  E. x  e.  RR  ( z  x.  x
)  =  1 )
62 remulcl 8790 . . . . . . 7  |-  ( ( z  e.  RR  /\  x  e.  RR )  ->  ( z  x.  x
)  e.  RR )
6362adantlr 698 . . . . . 6  |-  ( ( ( z  e.  RR  /\  z  =/=  0 )  /\  x  e.  RR )  ->  ( z  x.  x )  e.  RR )
64 eleq1 2318 . . . . . 6  |-  ( ( z  x.  x )  =  1  ->  (
( z  x.  x
)  e.  RR  <->  1  e.  RR ) )
6563, 64syl5ibcom 213 . . . . 5  |-  ( ( ( z  e.  RR  /\  z  =/=  0 )  /\  x  e.  RR )  ->  ( ( z  x.  x )  =  1  ->  1  e.  RR ) )
6665rexlimdva 2642 . . . 4  |-  ( ( z  e.  RR  /\  z  =/=  0 )  -> 
( E. x  e.  RR  ( z  x.  x )  =  1  ->  1  e.  RR ) )
6761, 66mpd 16 . . 3  |-  ( ( z  e.  RR  /\  z  =/=  0 )  -> 
1  e.  RR )
6867rexlimiva 2637 . 2  |-  ( E. z  e.  RR  z  =/=  0  ->  1  e.  RR )
6944, 60, 68mp2b 11 1  |-  1  e.  RR
Colors of variables: wff set class
Syntax hints:   -. wn 5    -> wi 6    \/ wo 359    /\ wa 360    = wceq 1619    e. wcel 1621    =/= wne 2421   E.wrex 2519  (class class class)co 5792   CCcc 8703   RRcr 8704   0cc0 8705   1c1 8706   _ici 8707    + caddc 8708    x. cmul 8710
This theorem is referenced by:  0re  8806  peano2re  8953  mul02lem2  8957  addid1  8960  renegcl  9078  peano2rem  9081  0reALT  9111  0lt1  9264  0le1  9265  1le1  9364  eqneg  9448  ltp1  9562  ltm1  9564  recgt0  9568  mulgt1  9583  ltmulgt11  9584  lemulge11  9586  ltrec  9605  reclt1  9619  recgt1  9620  recgt1i  9621  recp1lt1  9622  recreclt  9623  recgt0ii  9630  ledivp1i  9650  ltdivp1i  9651  inelr  9704  cju  9710  nnssre  9718  nnge1  9740  nngt1ne1  9741  nnle1eq1  9742  nngt0  9743  nnnlt1  9744  nnrecre  9750  nnrecgt0  9751  nnsub  9752  2re  9783  3re  9785  4re  9787  5re  9789  6re  9790  7re  9791  8re  9792  9re  9793  10re  9794  2pos  9796  3pos  9798  4pos  9800  5pos  9801  6pos  9802  7pos  9803  8pos  9804  9pos  9805  10pos  9806  1lt2  9853  1lt3  9855  1lt4  9858  1lt5  9862  1lt6  9867  1lt7  9873  1lt8  9880  1lt9  9888  1lt10  9897  1ne2  9898  halflt1  9900  addltmul  9914  nnunb  9928  elnnnn0c  9976  elnnz1  10016  znnnlt1  10017  zltp1le  10034  zleltp1  10035  recnz  10054  gtndiv  10056  suprzcl  10058  uzindOLD  10073  eluzp1m1  10218  eluzp1p1  10220  eluz2b2  10257  zbtwnre  10281  rebtwnz  10282  1rp  10325  qbtwnre  10492  qbtwnxr  10493  xmulid1  10565  xmulid2  10566  xmulm1  10567  x2times  10585  xrub  10596  0elunit  10720  1elunit  10721  lincmb01cmp  10743  iccf1o  10744  xov1plusxeqvd  10746  unitssre  10747  fztpval  10811  fraclt1  10900  fracle1  10901  flbi2  10913  fladdz  10916  flhalf  10920  fldiv  10930  modid  10959  1mod  10962  seqf1olem1  11051  reexpcl  11086  reexpclz  11089  expge0  11104  expge1  11105  expgt1  11106  ltexp2a  11119  expcan  11120  ltexp2  11121  leexp2  11122  leexp2a  11123  leexp2r  11125  nnlesq  11172  bernneq  11193  bernneq2  11194  bernneq3  11195  expnbnd  11196  expnlbnd  11197  expnlbnd2  11198  expmulnbnd  11199  discr1  11203  facwordi  11268  faclbnd3  11271  faclbnd4lem1  11272  faclbnd4lem4  11275  faclbnd6  11278  facavg  11280  fzsdom2  11347  hashfun  11354  crre  11564  remim  11567  cjexp  11600  re1  11604  im1  11605  rei  11606  imi  11607  sqrlem1  11693  sqrlem2  11694  sqrlem3  11695  sqrlem4  11696  sqrlem7  11699  resqrex  11701  sqr1  11722  sqr2gt1lt2  11725  sqrm1  11726  abs1  11747  rddif  11789  absrdbnd  11790  caubnd2  11806  mulcn2  12034  reccn2  12035  rlimo1  12055  rlimno1  12092  iseraltlem2  12120  iseraltlem3  12121  iseralt  12122  o1fsum  12236  abscvgcvg  12242  climcndslem1  12270  climcndslem2  12271  flo1  12275  harmonic  12279  expcnv  12284  geolim  12288  geolim2  12289  georeclim  12290  geo2lim  12293  geomulcvg  12294  geoisumr  12296  geoisum1c  12298  geoihalfsum  12300  efcllem  12321  ere  12332  ege2le3  12333  efgt1  12358  resin4p  12380  recos4p  12381  tanhlt1  12402  tanhbnd  12403  sinbnd  12422  cosbnd  12423  sinbnd2  12424  cosbnd2  12425  ef01bndlem  12426  sin01bnd  12427  cos01bnd  12428  cos1bnd  12429  cos2bnd  12430  sinltx  12431  sin01gt0  12432  cos01gt0  12433  sin02gt0  12434  sincos1sgn  12435  eirrlem  12444  rpnnen2lem2  12456  rpnnen2lem3  12457  rpnnen2lem4  12458  rpnnen2lem9  12463  rpnnen2  12466  rpnnen  12467  ruclem6  12475  ruclem11  12480  ruclem12  12481  nthruz  12492  3dvds  12553  bitsfzolem  12587  bitsfzo  12588  bitsmod  12589  bitscmp  12591  bitsinv1lem  12594  sadcadd  12611  smuval2  12635  isprm3  12729  prmind2  12731  sqnprm  12739  coprm  12741  isprm5  12753  divdenle  12782  zsqrelqelz  12791  phibndlem  12800  fermltl  12814  odzdvds  12822  pythagtriplem3  12833  iserodd  12850  pcmpt  12902  fldivp1  12907  pcfaclem  12908  pockthi  12916  infpn2  12922  prmreclem1  12925  prmreclem5  12929  4sqlem11  12964  4sqlem12  12965  ramub1lem1  13035  2expltfac  13067  resslem  13163  rescbas  13668  rescabs  13672  odubas  14199  lt6abl  15143  pgpfaclem2  15279  abvneg  15561  abvtrivd  15567  xrsmcmn  16359  resubdrg  16385  gzrngunitlem  16398  gzrngunit  16399  znidomb  16477  thlbas  16558  leordtval2  16904  setsmsbas  17983  dscmet  18057  dscopn  18058  nrginvrcnlem  18163  nmoid  18213  idnghm  18214  tgioo  18264  blcvx  18266  xrsmopn  18280  metnrmlem1a  18324  metnrmlem1  18325  iitopon  18345  dfii2  18348  dfii3  18349  dfii5  18351  iicmp  18352  iicon  18353  iirev  18389  iirevcn  18390  iihalf1  18391  iihalf1cn  18392  iihalf2  18393  iihalf2cn  18394  elii1  18395  elii2  18396  iimulcl  18397  iimulcn  18398  icchmeo  18401  icopnfcnv  18402  icopnfhmeo  18403  iccpnfcnv  18404  iccpnfhmeo  18405  xrhmeo  18406  xrhmph  18407  icccvx  18410  evth  18419  xlebnum  18425  lebnumii  18426  htpycc  18440  reparphti  18457  pcoval1  18473  pco0  18474  pco1  18475  pcoval2  18476  pcocn  18477  pcohtpylem  18479  pcopt  18482  pcopt2  18483  pcoass  18484  pcorevlem  18486  pcorev2  18488  pi1xfrcnv  18517  nmhmcn  18563  cncmet  18706  ovolunlem1a  18817  ovoliunlem1  18823  dyadmaxlem  18914  vitalilem1  18925  vitalilem2  18926  vitalilem4  18928  vitalilem5  18929  vitali  18930  mbfneg  18967  i1f1  19007  itg11  19008  i1fsub  19025  itg1sub  19026  mbfi1fseqlem6  19037  itg2const  19057  itg2mulc  19064  itg2monolem1  19067  itg2monolem3  19069  iblcnlem1  19104  i1fibl  19124  itgitg1  19125  dveflem  19288  mvth  19301  dvlipcn  19303  lhop1lem  19322  dvcvx  19329  dvfsumlem1  19335  dvfsumlem2  19336  dvfsumlem3  19337  dvfsumlem4  19338  dvfsum2  19343  ply1remlem  19510  fta1glem2  19514  fta1blem  19516  plyeq0lem  19554  fta1lem  19649  vieta1lem2  19653  aalioulem3  19676  aalioulem4  19677  aalioulem5  19678  aaliou3lem2  19685  aaliou3lem8  19687  ulmbdd  19737  iblulm  19745  radcnvlem1  19751  radcnvlem2  19752  dvradcnv  19759  abelthlem2  19770  abelthlem3  19771  abelthlem5  19773  abelthlem7  19776  abelth  19779  abelth2  19780  reeff1olem  19784  reeff1o  19785  sinhalfpilem  19796  tangtx  19835  sincos4thpi  19843  pige3  19847  coskpi  19850  cosne0  19854  recosf1o  19859  tanregt0  19863  efif1olem3  19868  efif1olem4  19869  loge  19902  rplogcl  19920  logdivlti  19933  logno1  19945  logcnlem4  19954  logf1o2  19959  dvlog2lem  19961  advlog  19963  logtayllem  19968  logtayl  19969  logccv  19972  recxpcl  19984  cxplt  20003  cxple  20004  cxplea  20005  cxpsqrlem  20011  cxpsqr  20012  cxpcn3lem  20049  cxpaddlelem  20053  cxpaddle  20054  loglesqr  20060  ang180lem1  20069  ang180lem2  20070  ang180lem3  20071  isosctrlem1  20080  isosctrlem2  20081  angpined  20089  chordthmlem4  20094  1cubrlem  20099  atanre  20143  asinsin  20150  acosrecl  20161  atandmcj  20167  atancj  20168  atanlogaddlem  20171  atantan  20181  bndatandm  20187  atans2  20189  ressatans  20192  leibpilem2  20199  leibpi  20200  leibpisum  20201  log2tlbnd  20203  birthdaylem3  20210  birthday  20211  rlimcnp  20222  rlimcnp2  20223  efrlim  20226  cxp2limlem  20232  cxp2lim  20233  cxploglim  20234  cxploglim2  20235  divsqrsumlem  20236  divsqrsumo1  20240  cvxcl  20241  scvxcvx  20242  jensenlem2  20244  amgmlem  20246  emcllem2  20252  emcllem4  20254  emcllem6  20256  emcllem7  20257  emre  20261  emgt0  20262  harmonicbnd3  20263  harmonicubnd  20265  harmonicbnd4  20266  fsumharmonic  20267  wilthlem1  20268  wilthlem2  20269  ftalem1  20272  ftalem2  20273  ftalem5  20276  basellem3  20282  basellem9  20288  issqf  20336  cht1  20365  vma1  20366  chp1  20367  ppieq0  20376  ppiltx  20377  mumullem2  20380  fsumfldivdiaglem  20391  ppiublem1  20403  ppiub  20405  chpeq0  20409  chtublem  20412  chtub  20413  chpval2  20419  chpchtsum  20420  chpub  20421  logfacbnd3  20424  logfacrlim  20425  logexprlim  20426  mersenne  20428  perfectlem2  20431  dchrelbas4  20444  dchrinv  20462  dchr1re  20464  bcmono  20478  efexple  20482  bposlem1  20485  bposlem2  20486  bposlem5  20489  bposlem8  20492  lgslem3  20499  lgslem4  20500  lgsvalmod  20516  lgsmod  20522  lgsdir2lem1  20524  lgsdir2lem3  20526  lgsdir2lem4  20527  lgsdir2lem5  20528  lgsdirprm  20530  lgsdir  20531  lgsne0  20534  lgsabs1  20535  lgsdinn0  20541  lgseisen  20554  lgsquadlem2  20556  m1lgs  20563  2sqlem8  20573  chebbnd1lem1  20580  chebbnd1lem2  20581  chebbnd1lem3  20582  chebbnd1  20583  chtppilimlem1  20584  chtppilimlem2  20585  chtppilim  20586  chebbnd2  20588  chto1lb  20589  chpchtlim  20590  chpo1ubb  20592  vmadivsum  20593  vmadivsumb  20594  rplogsumlem1  20595  rplogsumlem2  20596  rpvmasumlem  20598  dchrisumlem3  20602  dchrmusumlema  20604  dchrmusum2  20605  dchrvmasumlem2  20609  dchrvmasumlem3  20610  dchrvmasumiflem1  20612  dchrvmasumiflem2  20613  dchrisum0flblem1  20619  dchrisum0flblem2  20620  dchrisum0fno1  20622  rpvmasum2  20623  dchrisum0re  20624  dchrisum0lema  20625  dchrisum0lem1b  20626  dchrisum0lem1  20627  dchrisum0lem2a  20628  dchrisum0lem2  20629  dchrisum0lem3  20630  rplogsum  20638  dirith2  20639  mudivsum  20641  mulogsumlem  20642  mulogsum  20643  logdivsum  20644  mulog2sumlem1  20645  mulog2sumlem2  20646  vmalogdivsum2  20649  2vmadivsumlem  20651  log2sumbnd  20655  selberglem2  20657  selbergb  20660  selberg2lem  20661  selberg2b  20663  chpdifbndlem1  20664  chpdifbnd  20666  selberg3lem1  20668  selberg3lem2  20669  selberg4lem1  20671  pntrmax  20675  pntrsumo1  20676  pntrsumbnd  20677  selberg34r  20682  selbergsb  20686  pntrlog2bndlem1  20688  pntrlog2bndlem2  20689  pntrlog2bndlem3  20690  pntrlog2bndlem4  20691  pntrlog2bndlem5  20692  pntrlog2bndlem6  20694  pntrlog2bnd  20695  pntpbnd1a  20696  pntpbnd1  20697  pntpbnd2  20698  pntibndlem1  20700  pntibndlem2a  20701  pntibndlem2  20702  pntibndlem3  20703  pntibnd  20704  pntlemd  20705  pntlemc  20706  pntlemb  20708  pntlemg  20709  pntlemr  20713  pntlemf  20716  pntlemk  20717  pntlemo  20718  pntlem3  20720  pntleml  20722  pnt  20725  abvcxp  20726  ostth2lem1  20729  qabvle  20736  padicabvf  20742  padicabvcxp  20743  ostth1  20744  ostth2lem2  20745  ostth2lem3  20746  ostth2lem4  20747  ostth2  20748  ostth3  20749  ostth  20750  ex-dif  20753  ex-in  20755  ex-pss  20758  ex-res  20771  ex-fl  20777  nv1  21202  smcnlem  21230  ipidsq  21246  nmoub3i  21311  nmlno0lem  21331  blocnilem  21342  ipasslem10  21377  ubthlem2  21410  minvecolem4  21419  htthlem  21457  hisubcomi  21643  normlem9  21657  norm-ii-i  21676  bcs2  21721  norm1  21788  nmopub2tALT  22449  nmfnleub2  22466  nmlnop0iALT  22535  nmopun  22554  unopbd  22555  hmopd  22562  nmcexi  22566  nmopadjlem  22629  nmopcoi  22635  nmopcoadji  22641  opsqrlem4  22683  pjnmopi  22688  pjbdlni  22689  stcl  22756  stge0  22764  stle1  22765  hstle1  22766  hstle  22770  hstles  22771  stge1i  22778  stlesi  22781  staddi  22786  stadd3i  22788  strlem1  22790  strlem3a  22792  strlem5  22795  jplem1  22808  cdj1i  22973  addltmulALT  22986  fzsplit3  22991  ballotlem2  23008  ballotlemfc0  23012  ballotlemfcc  23013  ballotlem4  23018  ballotlemi1  23022  ballotlemic  23026  ballotlem1c  23027  ballotlemsgt1  23030  ballotlemsel1i  23032  ballotlemfrcn0  23049  zetacvg  23061  subfacp1lem1  23082  subfacp1lem5  23087  subfacval2  23090  subfaclim  23091  subfacval3  23092  cvxpcon  23145  cvxscon  23146  rescon  23149  iiscon  23155  iillyscon  23156  cvmliftlem2  23189  cvmliftlem8  23195  cvmliftlem13  23199  konigsberg  23283  snmlff  23284  sinccvglem  23377  divelunit  23451  dedekind  23453  relin01  23460  fznatpl1  23464  fz0n  23468  brbtwn2  23908  colinearalglem4  23912  ax5seglem1  23931  ax5seglem2  23932  ax5seglem3  23934  ax5seglem5  23936  ax5seglem6  23937  ax5seglem9  23940  ax5seg  23941  axbtwnid  23942  axpaschlem  23943  axpasch  23944  axlowdimlem3  23947  axlowdimlem6  23950  axlowdimlem7  23951  axlowdimlem10  23954  axlowdimlem16  23960  axlowdimlem17  23961  axlowdim1  23962  axlowdim2  23963  axlowdim  23964  axeuclidlem  23965  axcontlem2  23968  axcontlem4  23970  axcontlem7  23973  bpoly4  24169  cntrset  24969  fnckle  25412  nn0prpwlem  25605  fdc  25822  incsequz  25825  geomcau  25842  totbndbnd  25880  cntotbnd  25887  heiborlem8  25909  bfplem2  25914  bfp  25915  lzenom  26216  rabren3dioph  26265  irrapxlem1  26274  irrapxlem2  26275  irrapxlem4  26277  irrapxlem5  26278  pellexlem2  26282  pellexlem5  26285  pellexlem6  26286  pell1qrge1  26322  pell1qr1  26323  elpell1qr2  26324  pell1qrgaplem  26325  pell14qrgap  26327  pell14qrgapw  26328  pellqrex  26331  pellfundre  26333  pellfundgt1  26335  pellfundlb  26336  pellfundglb  26337  pellfundex  26338  pellfund14gap  26339  pellfundrp  26340  pellfundne1  26341  rmspecsqrnq  26358  rmspecnonsq  26359  rmspecfund  26361  rmspecpos  26368  monotoddzzfi  26394  jm2.17a  26414  rmygeid  26418  acongeq  26437  jm2.23  26456  jm3.1lem2  26478  matbas  26835  lhe4.4ex1a  26913  fmul01  27078  fmuldfeq  27081  fmul01lt1lem1  27082  fmul01lt1lem2  27083  stoweidlem1  27085  stoweidlem3  27087  stoweidlem5  27089  stoweidlem7  27091  stoweidlem10  27094  stoweidlem11  27095  stoweidlem12  27096  stoweidlem13  27097  stoweidlem14  27098  stoweidlem16  27100  stoweidlem18  27102  stoweidlem19  27103  stoweidlem20  27104  stoweidlem22  27106  stoweidlem24  27108  stoweidlem25  27109  stoweidlem26  27110  stoweidlem28  27112  stoweidlem30  27114  stoweidlem34  27118  stoweidlem36  27120  stoweidlem38  27122  stoweidlem40  27124  stoweidlem41  27125  stoweidlem42  27126  stoweidlem44  27128  stoweidlem45  27129  stoweidlem51  27135  stoweidlem59  27143  stoweidlem60  27144  stoweidlem62  27146  stoweid  27147  reseccl  27272  recsccl  27273  sgn1  27298
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2239  ax-1cn 8763  ax-icn 8764  ax-addcl 8765  ax-mulcl 8767  ax-mulrcl 8768  ax-i2m1 8773  ax-1ne0 8774  ax-rrecex 8777  ax-cnre 8778
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 941  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2245  df-cleq 2251  df-clel 2254  df-nfc 2383  df-ne 2423  df-ral 2523  df-rex 2524  df-rab 2527  df-v 2765  df-dif 3130  df-un 3132  df-in 3134  df-ss 3141  df-nul 3431  df-if 3540  df-sn 3620  df-pr 3621  df-op 3623  df-uni 3802  df-br 3998  df-opab 4052  df-xp 4675  df-cnv 4677  df-dm 4679  df-rn 4680  df-res 4681  df-ima 4682  df-fv 4689  df-ov 5795
  Copyright terms: Public domain W3C validator