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

Theorem 1re 8717
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 8675, 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 8686 . . 3  |-  1  =/=  0
2 ax-1cn 8675 . . . . 5  |-  1  e.  CC
3 ax-cnre 8690 . . . . 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 2420 . . . . . . . 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 8711 . . . . . . . 8  |-  0  e.  CC
8 ax-cnre 8690 . . . . . . . 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 2421 . . . . . . . . . 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 2616 . . . . . . . 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 2616 . . . . . . 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 2616 . . . . 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 2616 . . . 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 2414 . . . . . . . . . . 11  |-  ( a  =/=  c  <->  -.  a  =  c )
2019con2bii 324 . . . . . . . . . 10  |-  ( a  =  c  <->  -.  a  =/=  c )
21 df-ne 2414 . . . . . . . . . . 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 5718 . . . . . . . . 9  |-  ( b  =  d  ->  (
_i  x.  b )  =  ( _i  x.  d ) )
2725, 26oveqan12d 5729 . . . . . . . 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 2454 . . . . . 6  |-  ( ( a  +  ( _i  x.  b ) )  =/=  ( c  +  ( _i  x.  d
) )  ->  (
a  =/=  c  \/  b  =/=  d ) )
30 neeq1 2420 . . . . . . . . . 10  |-  ( x  =  a  ->  (
x  =/=  y  <->  a  =/=  y ) )
31 neeq2 2421 . . . . . . . . . 10  |-  ( y  =  c  ->  (
a  =/=  y  <->  a  =/=  c ) )
3230, 31rcla42ev 2829 . . . . . . . . 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 2420 . . . . . . . . . 10  |-  ( x  =  b  ->  (
x  =/=  y  <->  b  =/=  y ) )
36 neeq2 2421 . . . . . . . . . 10  |-  ( y  =  d  ->  (
b  =/=  y  <->  b  =/=  d ) )
3735, 36rcla42ev 2829 . . . . . . . . 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 2636 . . . 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 2634 . . 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 2272 . . . . . . . . 9  |-  ( ( x  =  0  /\  y  =  0 )  ->  x  =  y )
4645ex 425 . . . . . . . 8  |-  ( x  =  0  ->  (
y  =  0  ->  x  =  y )
)
4746necon3d 2450 . . . . . . 7  |-  ( x  =  0  ->  (
x  =/=  y  -> 
y  =/=  0 ) )
48 neeq1 2420 . . . . . . . . 9  |-  ( z  =  y  ->  (
z  =/=  0  <->  y  =/=  0 ) )
4948rcla4ev 2821 . . . . . . . 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 2420 . . . . . . . 8  |-  ( z  =  x  ->  (
z  =/=  0  <->  x  =/=  0 ) )
5554rcla4ev 2821 . . . . . . 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 2488 . . 3  |-  ( ( x  e.  RR  /\  y  e.  RR )  ->  ( x  =/=  y  ->  E. z  e.  RR  z  =/=  0 ) )
6059rexlimivv 2634 . 2  |-  ( E. x  e.  RR  E. y  e.  RR  x  =/=  y  ->  E. z  e.  RR  z  =/=  0
)
61 ax-rrecex 8689 . . . 4  |-  ( ( z  e.  RR  /\  z  =/=  0 )  ->  E. x  e.  RR  ( z  x.  x
)  =  1 )
62 remulcl 8702 . . . . . . 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 2313 . . . . . 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 2629 . . . 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 2624 . 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 2412   E.wrex 2510  (class class class)co 5710   CCcc 8615   RRcr 8616   0cc0 8617   1c1 8618   _ici 8619    + caddc 8620    x. cmul 8622
This theorem is referenced by:  0re  8718  peano2re  8865  mul02lem2  8869  addid1  8872  renegcl  8990  peano2rem  8993  0reALT  9023  0lt1  9176  0le1  9177  1le1  9276  eqneg  9360  ltp1  9474  ltm1  9476  recgt0  9480  mulgt1  9495  ltmulgt11  9496  lemulge11  9498  ltrec  9517  reclt1  9531  recgt1  9532  recgt1i  9533  recp1lt1  9534  recreclt  9535  recgt0ii  9542  ledivp1i  9562  ltdivp1i  9563  inelr  9616  cju  9622  nnssre  9630  nnge1  9652  nngt1ne1  9653  nnle1eq1  9654  nngt0  9655  nnnlt1  9656  nnrecre  9662  nnrecgt0  9663  nnsub  9664  2re  9695  3re  9697  4re  9699  5re  9701  6re  9702  7re  9703  8re  9704  9re  9705  10re  9706  2pos  9708  3pos  9710  4pos  9712  5pos  9713  6pos  9714  7pos  9715  8pos  9716  9pos  9717  10pos  9718  1lt2  9765  1lt3  9767  1lt4  9770  1lt5  9774  1lt6  9779  1lt7  9785  1lt8  9792  1lt9  9800  1lt10  9809  1ne2  9810  halflt1  9812  addltmul  9826  nnunb  9840  elnnnn0c  9888  elnnz1  9928  znnnlt1  9929  zltp1le  9946  zleltp1  9947  recnz  9966  gtndiv  9968  suprzcl  9970  uzindOLD  9985  eluzp1m1  10130  eluzp1p1  10132  eluz2b2  10169  zbtwnre  10193  rebtwnz  10194  1rp  10237  qbtwnre  10404  qbtwnxr  10405  xmulid1  10477  xmulid2  10478  xmulm1  10479  x2times  10497  xrub  10508  0elunit  10632  1elunit  10633  lincmb01cmp  10655  iccf1o  10656  xov1plusxeqvd  10658  unitssre  10659  fztpval  10723  fraclt1  10812  fracle1  10813  flbi2  10825  fladdz  10828  flhalf  10832  fldiv  10842  modid  10871  1mod  10874  seqf1olem1  10963  reexpcl  10998  reexpclz  11001  expge0  11016  expge1  11017  expgt1  11018  ltexp2a  11031  expcan  11032  ltexp2  11033  leexp2  11034  leexp2a  11035  leexp2r  11037  nnlesq  11084  bernneq  11105  bernneq2  11106  bernneq3  11107  expnbnd  11108  expnlbnd  11109  expnlbnd2  11110  expmulnbnd  11111  discr1  11115  facwordi  11180  faclbnd3  11183  faclbnd4lem1  11184  faclbnd4lem4  11187  faclbnd6  11190  facavg  11192  fzsdom2  11259  hashfun  11266  crre  11476  remim  11479  cjexp  11512  re1  11516  im1  11517  rei  11518  imi  11519  sqrlem1  11605  sqrlem2  11606  sqrlem3  11607  sqrlem4  11608  sqrlem7  11611  resqrex  11613  sqr1  11634  sqr2gt1lt2  11637  sqrm1  11638  abs1  11659  rddif  11701  absrdbnd  11702  caubnd2  11718  mulcn2  11946  reccn2  11947  rlimo1  11967  rlimno1  12004  iseraltlem2  12032  iseraltlem3  12033  iseralt  12034  o1fsum  12148  abscvgcvg  12154  climcndslem1  12182  climcndslem2  12183  flo1  12187  harmonic  12191  expcnv  12196  geolim  12200  geolim2  12201  georeclim  12202  geo2lim  12205  geomulcvg  12206  geoisumr  12208  geoisum1c  12210  geoihalfsum  12212  efcllem  12233  ere  12244  ege2le3  12245  efgt1  12270  resin4p  12292  recos4p  12293  tanhlt1  12314  tanhbnd  12315  sinbnd  12334  cosbnd  12335  sinbnd2  12336  cosbnd2  12337  ef01bndlem  12338  sin01bnd  12339  cos01bnd  12340  cos1bnd  12341  cos2bnd  12342  sinltx  12343  sin01gt0  12344  cos01gt0  12345  sin02gt0  12346  sincos1sgn  12347  eirrlem  12356  rpnnen2lem2  12368  rpnnen2lem3  12369  rpnnen2lem4  12370  rpnnen2lem9  12375  rpnnen2  12378  rpnnen  12379  ruclem6  12387  ruclem11  12392  ruclem12  12393  nthruz  12404  3dvds  12465  bitsfzolem  12499  bitsfzo  12500  bitsmod  12501  bitscmp  12503  bitsinv1lem  12506  sadcadd  12523  smuval2  12547  isprm3  12641  prmind2  12643  sqnprm  12651  coprm  12653  isprm5  12665  divdenle  12694  zsqrelqelz  12703  phibndlem  12712  fermltl  12726  odzdvds  12734  pythagtriplem3  12745  iserodd  12762  pcmpt  12814  fldivp1  12819  pcfaclem  12820  pockthi  12828  infpn2  12834  prmreclem1  12837  prmreclem5  12841  4sqlem11  12876  4sqlem12  12877  ramub1lem1  12947  2expltfac  12979  resslem  13075  rescbas  13550  rescabs  13554  odubas  14081  lt6abl  15016  pgpfaclem2  15152  abvneg  15434  abvtrivd  15440  xrsmcmn  16229  resubdrg  16255  gzrngunitlem  16268  gzrngunit  16269  znidomb  16347  thlbas  16428  leordtval2  16774  setsmsbas  17853  dscmet  17927  dscopn  17928  nrginvrcnlem  18033  nmoid  18083  idnghm  18084  tgioo  18134  blcvx  18136  xrsmopn  18150  metnrmlem1a  18194  metnrmlem1  18195  iitopon  18215  dfii2  18218  dfii3  18219  dfii5  18221  iicmp  18222  iicon  18223  iirev  18259  iirevcn  18260  iihalf1  18261  iihalf1cn  18262  iihalf2  18263  iihalf2cn  18264  elii1  18265  elii2  18266  iimulcl  18267  iimulcn  18268  icchmeo  18271  icopnfcnv  18272  icopnfhmeo  18273  iccpnfcnv  18274  iccpnfhmeo  18275  xrhmeo  18276  xrhmph  18277  icccvx  18280  evth  18289  xlebnum  18295  lebnumii  18296  htpycc  18310  reparphti  18327  pcoval1  18343  pco0  18344  pco1  18345  pcoval2  18346  pcocn  18347  pcohtpylem  18349  pcopt  18352  pcopt2  18353  pcoass  18354  pcorevlem  18356  pcorev2  18358  pi1xfrcnv  18387  nmhmcn  18433  cncmet  18576  ovolunlem1a  18687  ovoliunlem1  18693  dyadmaxlem  18784  vitalilem1  18795  vitalilem2  18796  vitalilem4  18798  vitalilem5  18799  vitali  18800  mbfneg  18837  i1f1  18877  itg11  18878  i1fsub  18895  itg1sub  18896  mbfi1fseqlem6  18907  itg2const  18927  itg2mulc  18934  itg2monolem1  18937  itg2monolem3  18939  iblcnlem1  18974  i1fibl  18994  itgitg1  18995  dveflem  19158  mvth  19171  dvlipcn  19173  lhop1lem  19192  dvcvx  19199  dvfsumlem1  19205  dvfsumlem2  19206  dvfsumlem3  19207  dvfsumlem4  19208  dvfsum2  19213  ply1remlem  19380  fta1glem2  19384  fta1blem  19386  plyeq0lem  19424  fta1lem  19519  vieta1lem2  19523  aalioulem3  19546  aalioulem4  19547  aalioulem5  19548  aaliou3lem2  19555  aaliou3lem8  19557  ulmbdd  19607  iblulm  19615  radcnvlem1  19621  radcnvlem2  19622  dvradcnv  19629  abelthlem2  19640  abelthlem3  19641  abelthlem5  19643  abelthlem7  19646  abelth  19649  abelth2  19650  reeff1olem  19654  reeff1o  19655  sinhalfpilem  19666  tangtx  19705  sincos4thpi  19713  pige3  19717  coskpi  19720  cosne0  19724  recosf1o  19729  tanregt0  19733  efif1olem3  19738  efif1olem4  19739  loge  19772  rplogcl  19790  logdivlti  19803  logno1  19815  logcnlem4  19824  logf1o2  19829  dvlog2lem  19831  advlog  19833  logtayllem  19838  logtayl  19839  logccv  19842  ang180lem1  19851  ang180lem2  19852  ang180lem3  19853  isosctrlem1  19862  isosctrlem2  19863  angpined  19871  chordthmlem4  19876  recxpcl  19890  cxplt  19909  cxple  19910  cxplea  19911  cxpsqrlem  19917  cxpsqr  19918  cxpcn3lem  19955  cxpaddlelem  19959  cxpaddle  19960  loglesqr  19966  1cubrlem  19969  atanre  20013  asinsin  20020  acosrecl  20031  atandmcj  20037  atancj  20038  atanlogaddlem  20041  atantan  20051  bndatandm  20057  atans2  20059  ressatans  20062  leibpilem2  20069  leibpi  20070  leibpisum  20071  log2tlbnd  20073  birthdaylem3  20080  birthday  20081  rlimcnp  20092  rlimcnp2  20093  efrlim  20096  cxp2limlem  20102  cxp2lim  20103  cxploglim  20104  cxploglim2  20105  divsqrsumlem  20106  divsqrsumo1  20110  cvxcl  20111  scvxcvx  20112  jensenlem2  20114  amgmlem  20116  emcllem2  20122  emcllem4  20124  emcllem6  20126  emcllem7  20127  emre  20131  emgt0  20132  harmonicbnd3  20133  harmonicubnd  20135  harmonicbnd4  20136  fsumharmonic  20137  wilthlem1  20138  wilthlem2  20139  ftalem1  20142  ftalem2  20143  ftalem5  20146  basellem3  20152  basellem9  20158  issqf  20206  cht1  20235  vma1  20236  chp1  20237  ppieq0  20246  ppiltx  20247  mumullem2  20250  fsumfldivdiaglem  20261  ppiublem1  20273  ppiub  20275  chpeq0  20279  chtublem  20282  chtub  20283  chpval2  20289  chpchtsum  20290  chpub  20291  logfacbnd3  20294  logfacrlim  20295  logexprlim  20296  mersenne  20298  perfectlem2  20301  dchrelbas4  20314  dchrinv  20332  dchr1re  20334  bcmono  20348  efexple  20352  bposlem1  20355  bposlem2  20356  bposlem5  20359  bposlem8  20362  lgslem3  20369  lgslem4  20370  lgsvalmod  20386  lgsmod  20392  lgsdir2lem1  20394  lgsdir2lem3  20396  lgsdir2lem4  20397  lgsdir2lem5  20398  lgsdirprm  20400  lgsdir  20401  lgsne0  20404  lgsabs1  20405  lgsdinn0  20411  lgseisen  20424  lgsquadlem2  20426  m1lgs  20433  2sqlem8  20443  chebbnd1lem1  20450  chebbnd1lem2  20451  chebbnd1lem3  20452  chebbnd1  20453  chtppilimlem1  20454  chtppilimlem2  20455  chtppilim  20456  chebbnd2  20458  chto1lb  20459  chpchtlim  20460  chpo1ubb  20462  vmadivsum  20463  vmadivsumb  20464  rplogsumlem1  20465  rplogsumlem2  20466  rpvmasumlem  20468  dchrisumlem3  20472  dchrmusumlema  20474  dchrmusum2  20475  dchrvmasumlem2  20479  dchrvmasumlem3  20480  dchrvmasumiflem1  20482  dchrvmasumiflem2  20483  dchrisum0flblem1  20489  dchrisum0flblem2  20490  dchrisum0fno1  20492  rpvmasum2  20493  dchrisum0re  20494  dchrisum0lema  20495  dchrisum0lem1b  20496  dchrisum0lem1  20497  dchrisum0lem2a  20498  dchrisum0lem2  20499  dchrisum0lem3  20500  rplogsum  20508  dirith2  20509  mudivsum  20511  mulogsumlem  20512  mulogsum  20513  logdivsum  20514  mulog2sumlem1  20515  mulog2sumlem2  20516  vmalogdivsum2  20519  2vmadivsumlem  20521  log2sumbnd  20525  selberglem2  20527  selbergb  20530  selberg2lem  20531  selberg2b  20533  chpdifbndlem1  20534  chpdifbnd  20536  selberg3lem1  20538  selberg3lem2  20539  selberg4lem1  20541  pntrmax  20545  pntrsumo1  20546  pntrsumbnd  20547  selberg34r  20552  selbergsb  20556  pntrlog2bndlem1  20558  pntrlog2bndlem2  20559  pntrlog2bndlem3  20560  pntrlog2bndlem4  20561  pntrlog2bndlem5  20562  pntrlog2bndlem6  20564  pntrlog2bnd  20565  pntpbnd1a  20566  pntpbnd1  20567  pntpbnd2  20568  pntibndlem1  20570  pntibndlem2a  20571  pntibndlem2  20572  pntibndlem3  20573  pntibnd  20574  pntlemd  20575  pntlemc  20576  pntlemb  20578  pntlemg  20579  pntlemr  20583  pntlemf  20586  pntlemk  20587  pntlemo  20588  pntlem3  20590  pntleml  20592  pnt  20595  abvcxp  20596  ostth2lem1  20599  qabvle  20606  padicabvf  20612  padicabvcxp  20613  ostth1  20614  ostth2lem2  20615  ostth2lem3  20616  ostth2lem4  20617  ostth2  20618  ostth3  20619  ostth  20620  ex-dif  20623  ex-in  20625  ex-pss  20628  ex-res  20641  ex-fl  20647  nv1  21072  smcnlem  21100  ipidsq  21116  nmoub3i  21181  nmlno0lem  21201  blocnilem  21212  ipasslem10  21247  ubthlem2  21280  minvecolem4  21289  htthlem  21327  hisubcomi  21513  normlem9  21527  norm-ii-i  21546  bcs2  21591  norm1  21658  nmopub2tALT  22319  nmfnleub2  22336  nmlnop0iALT  22405  nmopun  22424  unopbd  22425  hmopd  22432  nmcexi  22436  nmopadjlem  22499  nmopcoi  22505  nmopcoadji  22511  opsqrlem4  22553  pjnmopi  22558  pjbdlni  22559  stcl  22626  stge0  22634  stle1  22635  hstle1  22636  hstle  22640  hstles  22641  stge1i  22648  stlesi  22651  staddi  22656  stadd3i  22658  strlem1  22660  strlem3a  22662  strlem5  22665  jplem1  22678  cdj1i  22843  addltmulALT  22856  zetacvg  22860  subfacp1lem1  22881  subfacp1lem5  22886  subfacval2  22889  subfaclim  22890  subfacval3  22891  cvxpcon  22944  cvxscon  22945  rescon  22948  iiscon  22954  iillyscon  22955  cvmliftlem2  22988  cvmliftlem8  22994  cvmliftlem13  22998  konigsberg  23082  snmlff  23083  sinccvglem  23176  divelunit  23250  dedekind  23252  relin01  23259  fznatpl1  23263  fz0n  23267  brbtwn2  23707  colinearalglem4  23711  ax5seglem1  23730  ax5seglem2  23731  ax5seglem3  23733  ax5seglem5  23735  ax5seglem6  23736  ax5seglem9  23739  ax5seg  23740  axbtwnid  23741  axpaschlem  23742  axpasch  23743  axlowdimlem3  23746  axlowdimlem6  23749  axlowdimlem7  23750  axlowdimlem10  23753  axlowdimlem16  23759  axlowdimlem17  23760  axlowdim1  23761  axlowdim2  23762  axlowdim  23763  axeuclidlem  23764  axcontlem2  23767  axcontlem4  23769  axcontlem7  23772  bpoly4  23968  cntrset  24768  fnckle  25211  nn0prpwlem  25404  fdc  25621  incsequz  25624  geomcau  25641  totbndbnd  25679  cntotbnd  25686  heiborlem8  25708  bfplem2  25713  bfp  25714  lzenom  26015  rabren3dioph  26064  irrapxlem1  26073  irrapxlem2  26074  irrapxlem4  26076  irrapxlem5  26077  pellexlem2  26081  pellexlem5  26084  pellexlem6  26085  pell1qrge1  26121  pell1qr1  26122  elpell1qr2  26123  pell1qrgaplem  26124  pell14qrgap  26126  pell14qrgapw  26127  pellqrex  26130  pellfundre  26132  pellfundgt1  26134  pellfundlb  26135  pellfundglb  26136  pellfundex  26137  pellfund14gap  26138  pellfundrp  26139  pellfundne1  26140  rmspecsqrnq  26157  rmspecnonsq  26158  rmspecfund  26160  rmspecpos  26167  monotoddzzfi  26193  jm2.17a  26213  rmygeid  26217  acongeq  26236  jm2.23  26255  jm3.1lem2  26277  matbas  26634  lhe4.4ex1a  26712  reseccl  26912  recsccl  26913  sgn1  26938
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 1926  ax-ext 2234  ax-1cn 8675  ax-icn 8676  ax-addcl 8677  ax-mulcl 8679  ax-mulrcl 8680  ax-i2m1 8685  ax-1ne0 8686  ax-rrecex 8689  ax-cnre 8690
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 1883  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-ne 2414  df-ral 2513  df-rex 2514  df-rab 2516  df-v 2729  df-dif 3081  df-un 3083  df-in 3085  df-ss 3089  df-nul 3363  df-if 3471  df-sn 3550  df-pr 3551  df-op 3553  df-uni 3728  df-br 3921  df-opab 3975  df-xp 4594  df-cnv 4596  df-dm 4598  df-rn 4599  df-res 4600  df-ima 4601  df-fv 4608  df-ov 5713
  Copyright terms: Public domain W3C validator