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

Theorem 1re 8791
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 8749, 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 8760 . . 3  |-  1  =/=  0
2 ax-1cn 8749 . . . . 5  |-  1  e.  CC
3 ax-cnre 8764 . . . . 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 2427 . . . . . . . 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 8785 . . . . . . . 8  |-  0  e.  CC
8 ax-cnre 8764 . . . . . . . 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 2428 . . . . . . . . . 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 2627 . . . . . . . 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 2627 . . . . . . 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 2627 . . . . 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 2627 . . . 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 2421 . . . . . . . . . . 11  |-  ( a  =/=  c  <->  -.  a  =  c )
2019con2bii 324 . . . . . . . . . 10  |-  ( a  =  c  <->  -.  a  =/=  c )
21 df-ne 2421 . . . . . . . . . . 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 5786 . . . . . . . . 9  |-  ( b  =  d  ->  (
_i  x.  b )  =  ( _i  x.  d ) )
2725, 26oveqan12d 5797 . . . . . . . 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 2461 . . . . . 6  |-  ( ( a  +  ( _i  x.  b ) )  =/=  ( c  +  ( _i  x.  d
) )  ->  (
a  =/=  c  \/  b  =/=  d ) )
30 neeq1 2427 . . . . . . . . . 10  |-  ( x  =  a  ->  (
x  =/=  y  <->  a  =/=  y ) )
31 neeq2 2428 . . . . . . . . . 10  |-  ( y  =  c  ->  (
a  =/=  y  <->  a  =/=  c ) )
3230, 31rcla42ev 2860 . . . . . . . . 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 2427 . . . . . . . . . 10  |-  ( x  =  b  ->  (
x  =/=  y  <->  b  =/=  y ) )
36 neeq2 2428 . . . . . . . . . 10  |-  ( y  =  d  ->  (
b  =/=  y  <->  b  =/=  d ) )
3735, 36rcla42ev 2860 . . . . . . . . 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 2647 . . . 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 2645 . . 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 2275 . . . . . . . . 9  |-  ( ( x  =  0  /\  y  =  0 )  ->  x  =  y )
4645ex 425 . . . . . . . 8  |-  ( x  =  0  ->  (
y  =  0  ->  x  =  y )
)
4746necon3d 2457 . . . . . . 7  |-  ( x  =  0  ->  (
x  =/=  y  -> 
y  =/=  0 ) )
48 neeq1 2427 . . . . . . . . 9  |-  ( z  =  y  ->  (
z  =/=  0  <->  y  =/=  0 ) )
4948rcla4ev 2852 . . . . . . . 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 2427 . . . . . . . 8  |-  ( z  =  x  ->  (
z  =/=  0  <->  x  =/=  0 ) )
5554rcla4ev 2852 . . . . . . 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 2495 . . 3  |-  ( ( x  e.  RR  /\  y  e.  RR )  ->  ( x  =/=  y  ->  E. z  e.  RR  z  =/=  0 ) )
6059rexlimivv 2645 . 2  |-  ( E. x  e.  RR  E. y  e.  RR  x  =/=  y  ->  E. z  e.  RR  z  =/=  0
)
61 ax-rrecex 8763 . . . 4  |-  ( ( z  e.  RR  /\  z  =/=  0 )  ->  E. x  e.  RR  ( z  x.  x
)  =  1 )
62 remulcl 8776 . . . . . . 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 2316 . . . . . 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 2640 . . . 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 2635 . 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 2419   E.wrex 2517  (class class class)co 5778   CCcc 8689   RRcr 8690   0cc0 8691   1c1 8692   _ici 8693    + caddc 8694    x. cmul 8696
This theorem is referenced by:  0re  8792  peano2re  8939  mul02lem2  8943  addid1  8946  renegcl  9064  peano2rem  9067  0reALT  9097  0lt1  9250  0le1  9251  1le1  9350  eqneg  9434  ltp1  9548  ltm1  9550  recgt0  9554  mulgt1  9569  ltmulgt11  9570  lemulge11  9572  ltrec  9591  reclt1  9605  recgt1  9606  recgt1i  9607  recp1lt1  9608  recreclt  9609  recgt0ii  9616  ledivp1i  9636  ltdivp1i  9637  inelr  9690  cju  9696  nnssre  9704  nnge1  9726  nngt1ne1  9727  nnle1eq1  9728  nngt0  9729  nnnlt1  9730  nnrecre  9736  nnrecgt0  9737  nnsub  9738  2re  9769  3re  9771  4re  9773  5re  9775  6re  9776  7re  9777  8re  9778  9re  9779  10re  9780  2pos  9782  3pos  9784  4pos  9786  5pos  9787  6pos  9788  7pos  9789  8pos  9790  9pos  9791  10pos  9792  1lt2  9839  1lt3  9841  1lt4  9844  1lt5  9848  1lt6  9853  1lt7  9859  1lt8  9866  1lt9  9874  1lt10  9883  1ne2  9884  halflt1  9886  addltmul  9900  nnunb  9914  elnnnn0c  9962  elnnz1  10002  znnnlt1  10003  zltp1le  10020  zleltp1  10021  recnz  10040  gtndiv  10042  suprzcl  10044  uzindOLD  10059  eluzp1m1  10204  eluzp1p1  10206  eluz2b2  10243  zbtwnre  10267  rebtwnz  10268  1rp  10311  qbtwnre  10478  qbtwnxr  10479  xmulid1  10551  xmulid2  10552  xmulm1  10553  x2times  10571  xrub  10582  0elunit  10706  1elunit  10707  lincmb01cmp  10729  iccf1o  10730  xov1plusxeqvd  10732  unitssre  10733  fztpval  10797  fraclt1  10886  fracle1  10887  flbi2  10899  fladdz  10902  flhalf  10906  fldiv  10916  modid  10945  1mod  10948  seqf1olem1  11037  reexpcl  11072  reexpclz  11075  expge0  11090  expge1  11091  expgt1  11092  ltexp2a  11105  expcan  11106  ltexp2  11107  leexp2  11108  leexp2a  11109  leexp2r  11111  nnlesq  11158  bernneq  11179  bernneq2  11180  bernneq3  11181  expnbnd  11182  expnlbnd  11183  expnlbnd2  11184  expmulnbnd  11185  discr1  11189  facwordi  11254  faclbnd3  11257  faclbnd4lem1  11258  faclbnd4lem4  11261  faclbnd6  11264  facavg  11266  fzsdom2  11333  hashfun  11340  crre  11550  remim  11553  cjexp  11586  re1  11590  im1  11591  rei  11592  imi  11593  sqrlem1  11679  sqrlem2  11680  sqrlem3  11681  sqrlem4  11682  sqrlem7  11685  resqrex  11687  sqr1  11708  sqr2gt1lt2  11711  sqrm1  11712  abs1  11733  rddif  11775  absrdbnd  11776  caubnd2  11792  mulcn2  12020  reccn2  12021  rlimo1  12041  rlimno1  12078  iseraltlem2  12106  iseraltlem3  12107  iseralt  12108  o1fsum  12222  abscvgcvg  12228  climcndslem1  12256  climcndslem2  12257  flo1  12261  harmonic  12265  expcnv  12270  geolim  12274  geolim2  12275  georeclim  12276  geo2lim  12279  geomulcvg  12280  geoisumr  12282  geoisum1c  12284  geoihalfsum  12286  efcllem  12307  ere  12318  ege2le3  12319  efgt1  12344  resin4p  12366  recos4p  12367  tanhlt1  12388  tanhbnd  12389  sinbnd  12408  cosbnd  12409  sinbnd2  12410  cosbnd2  12411  ef01bndlem  12412  sin01bnd  12413  cos01bnd  12414  cos1bnd  12415  cos2bnd  12416  sinltx  12417  sin01gt0  12418  cos01gt0  12419  sin02gt0  12420  sincos1sgn  12421  eirrlem  12430  rpnnen2lem2  12442  rpnnen2lem3  12443  rpnnen2lem4  12444  rpnnen2lem9  12449  rpnnen2  12452  rpnnen  12453  ruclem6  12461  ruclem11  12466  ruclem12  12467  nthruz  12478  3dvds  12539  bitsfzolem  12573  bitsfzo  12574  bitsmod  12575  bitscmp  12577  bitsinv1lem  12580  sadcadd  12597  smuval2  12621  isprm3  12715  prmind2  12717  sqnprm  12725  coprm  12727  isprm5  12739  divdenle  12768  zsqrelqelz  12777  phibndlem  12786  fermltl  12800  odzdvds  12808  pythagtriplem3  12819  iserodd  12836  pcmpt  12888  fldivp1  12893  pcfaclem  12894  pockthi  12902  infpn2  12908  prmreclem1  12911  prmreclem5  12915  4sqlem11  12950  4sqlem12  12951  ramub1lem1  13021  2expltfac  13053  resslem  13149  rescbas  13654  rescabs  13658  odubas  14185  lt6abl  15129  pgpfaclem2  15265  abvneg  15547  abvtrivd  15553  xrsmcmn  16345  resubdrg  16371  gzrngunitlem  16384  gzrngunit  16385  znidomb  16463  thlbas  16544  leordtval2  16890  setsmsbas  17969  dscmet  18043  dscopn  18044  nrginvrcnlem  18149  nmoid  18199  idnghm  18200  tgioo  18250  blcvx  18252  xrsmopn  18266  metnrmlem1a  18310  metnrmlem1  18311  iitopon  18331  dfii2  18334  dfii3  18335  dfii5  18337  iicmp  18338  iicon  18339  iirev  18375  iirevcn  18376  iihalf1  18377  iihalf1cn  18378  iihalf2  18379  iihalf2cn  18380  elii1  18381  elii2  18382  iimulcl  18383  iimulcn  18384  icchmeo  18387  icopnfcnv  18388  icopnfhmeo  18389  iccpnfcnv  18390  iccpnfhmeo  18391  xrhmeo  18392  xrhmph  18393  icccvx  18396  evth  18405  xlebnum  18411  lebnumii  18412  htpycc  18426  reparphti  18443  pcoval1  18459  pco0  18460  pco1  18461  pcoval2  18462  pcocn  18463  pcohtpylem  18465  pcopt  18468  pcopt2  18469  pcoass  18470  pcorevlem  18472  pcorev2  18474  pi1xfrcnv  18503  nmhmcn  18549  cncmet  18692  ovolunlem1a  18803  ovoliunlem1  18809  dyadmaxlem  18900  vitalilem1  18911  vitalilem2  18912  vitalilem4  18914  vitalilem5  18915  vitali  18916  mbfneg  18953  i1f1  18993  itg11  18994  i1fsub  19011  itg1sub  19012  mbfi1fseqlem6  19023  itg2const  19043  itg2mulc  19050  itg2monolem1  19053  itg2monolem3  19055  iblcnlem1  19090  i1fibl  19110  itgitg1  19111  dveflem  19274  mvth  19287  dvlipcn  19289  lhop1lem  19308  dvcvx  19315  dvfsumlem1  19321  dvfsumlem2  19322  dvfsumlem3  19323  dvfsumlem4  19324  dvfsum2  19329  ply1remlem  19496  fta1glem2  19500  fta1blem  19502  plyeq0lem  19540  fta1lem  19635  vieta1lem2  19639  aalioulem3  19662  aalioulem4  19663  aalioulem5  19664  aaliou3lem2  19671  aaliou3lem8  19673  ulmbdd  19723  iblulm  19731  radcnvlem1  19737  radcnvlem2  19738  dvradcnv  19745  abelthlem2  19756  abelthlem3  19757  abelthlem5  19759  abelthlem7  19762  abelth  19765  abelth2  19766  reeff1olem  19770  reeff1o  19771  sinhalfpilem  19782  tangtx  19821  sincos4thpi  19829  pige3  19833  coskpi  19836  cosne0  19840  recosf1o  19845  tanregt0  19849  efif1olem3  19854  efif1olem4  19855  loge  19888  rplogcl  19906  logdivlti  19919  logno1  19931  logcnlem4  19940  logf1o2  19945  dvlog2lem  19947  advlog  19949  logtayllem  19954  logtayl  19955  logccv  19958  recxpcl  19970  cxplt  19989  cxple  19990  cxplea  19991  cxpsqrlem  19997  cxpsqr  19998  cxpcn3lem  20035  cxpaddlelem  20039  cxpaddle  20040  loglesqr  20046  ang180lem1  20055  ang180lem2  20056  ang180lem3  20057  isosctrlem1  20066  isosctrlem2  20067  angpined  20075  chordthmlem4  20080  1cubrlem  20085  atanre  20129  asinsin  20136  acosrecl  20147  atandmcj  20153  atancj  20154  atanlogaddlem  20157  atantan  20167  bndatandm  20173  atans2  20175  ressatans  20178  leibpilem2  20185  leibpi  20186  leibpisum  20187  log2tlbnd  20189  birthdaylem3  20196  birthday  20197  rlimcnp  20208  rlimcnp2  20209  efrlim  20212  cxp2limlem  20218  cxp2lim  20219  cxploglim  20220  cxploglim2  20221  divsqrsumlem  20222  divsqrsumo1  20226  cvxcl  20227  scvxcvx  20228  jensenlem2  20230  amgmlem  20232  emcllem2  20238  emcllem4  20240  emcllem6  20242  emcllem7  20243  emre  20247  emgt0  20248  harmonicbnd3  20249  harmonicubnd  20251  harmonicbnd4  20252  fsumharmonic  20253  wilthlem1  20254  wilthlem2  20255  ftalem1  20258  ftalem2  20259  ftalem5  20262  basellem3  20268  basellem9  20274  issqf  20322  cht1  20351  vma1  20352  chp1  20353  ppieq0  20362  ppiltx  20363  mumullem2  20366  fsumfldivdiaglem  20377  ppiublem1  20389  ppiub  20391  chpeq0  20395  chtublem  20398  chtub  20399  chpval2  20405  chpchtsum  20406  chpub  20407  logfacbnd3  20410  logfacrlim  20411  logexprlim  20412  mersenne  20414  perfectlem2  20417  dchrelbas4  20430  dchrinv  20448  dchr1re  20450  bcmono  20464  efexple  20468  bposlem1  20471  bposlem2  20472  bposlem5  20475  bposlem8  20478  lgslem3  20485  lgslem4  20486  lgsvalmod  20502  lgsmod  20508  lgsdir2lem1  20510  lgsdir2lem3  20512  lgsdir2lem4  20513  lgsdir2lem5  20514  lgsdirprm  20516  lgsdir  20517  lgsne0  20520  lgsabs1  20521  lgsdinn0  20527  lgseisen  20540  lgsquadlem2  20542  m1lgs  20549  2sqlem8  20559  chebbnd1lem1  20566  chebbnd1lem2  20567  chebbnd1lem3  20568  chebbnd1  20569  chtppilimlem1  20570  chtppilimlem2  20571  chtppilim  20572  chebbnd2  20574  chto1lb  20575  chpchtlim  20576  chpo1ubb  20578  vmadivsum  20579  vmadivsumb  20580  rplogsumlem1  20581  rplogsumlem2  20582  rpvmasumlem  20584  dchrisumlem3  20588  dchrmusumlema  20590  dchrmusum2  20591  dchrvmasumlem2  20595  dchrvmasumlem3  20596  dchrvmasumiflem1  20598  dchrvmasumiflem2  20599  dchrisum0flblem1  20605  dchrisum0flblem2  20606  dchrisum0fno1  20608  rpvmasum2  20609  dchrisum0re  20610  dchrisum0lema  20611  dchrisum0lem1b  20612  dchrisum0lem1  20613  dchrisum0lem2a  20614  dchrisum0lem2  20615  dchrisum0lem3  20616  rplogsum  20624  dirith2  20625  mudivsum  20627  mulogsumlem  20628  mulogsum  20629  logdivsum  20630  mulog2sumlem1  20631  mulog2sumlem2  20632  vmalogdivsum2  20635  2vmadivsumlem  20637  log2sumbnd  20641  selberglem2  20643  selbergb  20646  selberg2lem  20647  selberg2b  20649  chpdifbndlem1  20650  chpdifbnd  20652  selberg3lem1  20654  selberg3lem2  20655  selberg4lem1  20657  pntrmax  20661  pntrsumo1  20662  pntrsumbnd  20663  selberg34r  20668  selbergsb  20672  pntrlog2bndlem1  20674  pntrlog2bndlem2  20675  pntrlog2bndlem3  20676  pntrlog2bndlem4  20677  pntrlog2bndlem5  20678  pntrlog2bndlem6  20680  pntrlog2bnd  20681  pntpbnd1a  20682  pntpbnd1  20683  pntpbnd2  20684  pntibndlem1  20686  pntibndlem2a  20687  pntibndlem2  20688  pntibndlem3  20689  pntibnd  20690  pntlemd  20691  pntlemc  20692  pntlemb  20694  pntlemg  20695  pntlemr  20699  pntlemf  20702  pntlemk  20703  pntlemo  20704  pntlem3  20706  pntleml  20708  pnt  20711  abvcxp  20712  ostth2lem1  20715  qabvle  20722  padicabvf  20728  padicabvcxp  20729  ostth1  20730  ostth2lem2  20731  ostth2lem3  20732  ostth2lem4  20733  ostth2  20734  ostth3  20735  ostth  20736  ex-dif  20739  ex-in  20741  ex-pss  20744  ex-res  20757  ex-fl  20763  nv1  21188  smcnlem  21216  ipidsq  21232  nmoub3i  21297  nmlno0lem  21317  blocnilem  21328  ipasslem10  21363  ubthlem2  21396  minvecolem4  21405  htthlem  21443  hisubcomi  21629  normlem9  21643  norm-ii-i  21662  bcs2  21707  norm1  21774  nmopub2tALT  22435  nmfnleub2  22452  nmlnop0iALT  22521  nmopun  22540  unopbd  22541  hmopd  22548  nmcexi  22552  nmopadjlem  22615  nmopcoi  22621  nmopcoadji  22627  opsqrlem4  22669  pjnmopi  22674  pjbdlni  22675  stcl  22742  stge0  22750  stle1  22751  hstle1  22752  hstle  22756  hstles  22757  stge1i  22764  stlesi  22767  staddi  22772  stadd3i  22774  strlem1  22776  strlem3a  22778  strlem5  22781  jplem1  22794  cdj1i  22959  addltmulALT  22972  fzsplit3  22977  ballotlem2  22994  ballotlemfc0  22998  ballotlemfcc  22999  ballotlem4  23004  ballotlemi1  23008  ballotlemic  23012  ballotlem1c  23013  ballotlemsgt1  23016  ballotlemsel1i  23018  ballotlemfrcn0  23035  zetacvg  23047  subfacp1lem1  23068  subfacp1lem5  23073  subfacval2  23076  subfaclim  23077  subfacval3  23078  cvxpcon  23131  cvxscon  23132  rescon  23135  iiscon  23141  iillyscon  23142  cvmliftlem2  23175  cvmliftlem8  23181  cvmliftlem13  23185  konigsberg  23269  snmlff  23270  sinccvglem  23363  divelunit  23437  dedekind  23439  relin01  23446  fznatpl1  23450  fz0n  23454  brbtwn2  23894  colinearalglem4  23898  ax5seglem1  23917  ax5seglem2  23918  ax5seglem3  23920  ax5seglem5  23922  ax5seglem6  23923  ax5seglem9  23926  ax5seg  23927  axbtwnid  23928  axpaschlem  23929  axpasch  23930  axlowdimlem3  23933  axlowdimlem6  23936  axlowdimlem7  23937  axlowdimlem10  23940  axlowdimlem16  23946  axlowdimlem17  23947  axlowdim1  23948  axlowdim2  23949  axlowdim  23950  axeuclidlem  23951  axcontlem2  23954  axcontlem4  23956  axcontlem7  23959  bpoly4  24155  cntrset  24955  fnckle  25398  nn0prpwlem  25591  fdc  25808  incsequz  25811  geomcau  25828  totbndbnd  25866  cntotbnd  25873  heiborlem8  25895  bfplem2  25900  bfp  25901  lzenom  26202  rabren3dioph  26251  irrapxlem1  26260  irrapxlem2  26261  irrapxlem4  26263  irrapxlem5  26264  pellexlem2  26268  pellexlem5  26271  pellexlem6  26272  pell1qrge1  26308  pell1qr1  26309  elpell1qr2  26310  pell1qrgaplem  26311  pell14qrgap  26313  pell14qrgapw  26314  pellqrex  26317  pellfundre  26319  pellfundgt1  26321  pellfundlb  26322  pellfundglb  26323  pellfundex  26324  pellfund14gap  26325  pellfundrp  26326  pellfundne1  26327  rmspecsqrnq  26344  rmspecnonsq  26345  rmspecfund  26347  rmspecpos  26354  monotoddzzfi  26380  jm2.17a  26400  rmygeid  26404  acongeq  26423  jm2.23  26442  jm3.1lem2  26464  matbas  26821  lhe4.4ex1a  26899  fmul01  27064  fmuldfeq  27067  fmul01lt1lem1  27068  fmul01lt1lem2  27069  stoweidlem1  27071  stoweidlem3  27073  stoweidlem5  27075  stoweidlem7  27077  stoweidlem10  27080  stoweidlem11  27081  stoweidlem12  27082  stoweidlem13  27083  stoweidlem14  27084  stoweidlem16  27086  stoweidlem18  27088  stoweidlem19  27089  stoweidlem20  27090  stoweidlem22  27092  stoweidlem24  27094  stoweidlem25  27095  stoweidlem26  27096  stoweidlem28  27098  stoweidlem30  27100  stoweidlem34  27104  stoweidlem36  27106  stoweidlem38  27108  stoweidlem40  27110  stoweidlem41  27111  stoweidlem42  27112  stoweidlem44  27114  stoweidlem45  27115  stoweidlem51  27121  stoweidlem59  27129  stoweidlem60  27130  stoweidlem62  27132  stoweid  27133  reseccl  27256  recsccl  27257  sgn1  27282
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 2237  ax-1cn 8749  ax-icn 8750  ax-addcl 8751  ax-mulcl 8753  ax-mulrcl 8754  ax-i2m1 8759  ax-1ne0 8760  ax-rrecex 8763  ax-cnre 8764
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 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-ne 2421  df-ral 2521  df-rex 2522  df-rab 2525  df-v 2759  df-dif 3116  df-un 3118  df-in 3120  df-ss 3127  df-nul 3417  df-if 3526  df-sn 3606  df-pr 3607  df-op 3609  df-uni 3788  df-br 3984  df-opab 4038  df-xp 4661  df-cnv 4663  df-dm 4665  df-rn 4666  df-res 4667  df-ima 4668  df-fv 4675  df-ov 5781
  Copyright terms: Public domain W3C validator