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

Theorem 1re 8834
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 8792, 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
Dummy variables  a  b  c  d  x  y  z are mutually distinct and distinct from all other variables.

Proof of Theorem 1re
StepHypRef Expression
1 ax-1ne0 8803 . . 3  |-  1  =/=  0
2 ax-1cn 8792 . . . . 5  |-  1  e.  CC
3 cnre 8831 . . . . 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 2457 . . . . . . . 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 8828 . . . . . . . 8  |-  0  e.  CC
8 cnre 8831 . . . . . . . 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 2458 . . . . . . . . . 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 2657 . . . . . . . 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 2657 . . . . . . 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 2657 . . . . 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 2657 . . . 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 2451 . . . . . . . . . . 11  |-  ( a  =/=  c  <->  -.  a  =  c )
2019con2bii 324 . . . . . . . . . 10  |-  ( a  =  c  <->  -.  a  =/=  c )
21 df-ne 2451 . . . . . . . . . . 11  |-  ( b  =/=  d  <->  -.  b  =  d )
2221con2bii 324 . . . . . . . . . 10  |-  ( b  =  d  <->  -.  b  =/=  d )
2320, 22anbi12i 680 . . . . . . . . 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 5829 . . . . . . . . 9  |-  ( b  =  d  ->  (
_i  x.  b )  =  ( _i  x.  d ) )
2725, 26oveqan12d 5840 . . . . . . . 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 2491 . . . . . 6  |-  ( ( a  +  ( _i  x.  b ) )  =/=  ( c  +  ( _i  x.  d
) )  ->  (
a  =/=  c  \/  b  =/=  d ) )
30 neeq1 2457 . . . . . . . . . 10  |-  ( x  =  a  ->  (
x  =/=  y  <->  a  =/=  y ) )
31 neeq2 2458 . . . . . . . . . 10  |-  ( y  =  c  ->  (
a  =/=  y  <->  a  =/=  c ) )
3230, 31rspc2ev 2895 . . . . . . . . 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 729 . . . . . . 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 2457 . . . . . . . . . 10  |-  ( x  =  b  ->  (
x  =/=  y  <->  b  =/=  y ) )
36 neeq2 2458 . . . . . . . . . 10  |-  ( y  =  d  ->  (
b  =/=  y  <->  b  =/=  d ) )
3735, 36rspc2ev 2895 . . . . . . . . 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 728 . . . . . . 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 2677 . . . 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 2675 . . 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 2305 . . . . . . . . 9  |-  ( ( x  =  0  /\  y  =  0 )  ->  x  =  y )
4645ex 425 . . . . . . . 8  |-  ( x  =  0  ->  (
y  =  0  ->  x  =  y )
)
4746necon3d 2487 . . . . . . 7  |-  ( x  =  0  ->  (
x  =/=  y  -> 
y  =/=  0 ) )
48 neeq1 2457 . . . . . . . . 9  |-  ( z  =  y  ->  (
z  =/=  0  <->  y  =/=  0 ) )
4948rspcev 2887 . . . . . . . 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 2457 . . . . . . . 8  |-  ( z  =  x  ->  (
z  =/=  0  <->  x  =/=  0 ) )
5554rspcev 2887 . . . . . . 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 2525 . . 3  |-  ( ( x  e.  RR  /\  y  e.  RR )  ->  ( x  =/=  y  ->  E. z  e.  RR  z  =/=  0 ) )
6059rexlimivv 2675 . 2  |-  ( E. x  e.  RR  E. y  e.  RR  x  =/=  y  ->  E. z  e.  RR  z  =/=  0
)
61 ax-rrecex 8806 . . . 4  |-  ( ( z  e.  RR  /\  z  =/=  0 )  ->  E. x  e.  RR  ( z  x.  x
)  =  1 )
62 remulcl 8819 . . . . . . 7  |-  ( ( z  e.  RR  /\  x  e.  RR )  ->  ( z  x.  x
)  e.  RR )
6362adantlr 697 . . . . . 6  |-  ( ( ( z  e.  RR  /\  z  =/=  0 )  /\  x  e.  RR )  ->  ( z  x.  x )  e.  RR )
64 eleq1 2346 . . . . . 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 2670 . . . 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 2665 . 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 1625    e. wcel 1687    =/= wne 2449   E.wrex 2547  (class class class)co 5821   CCcc 8732   RRcr 8733   0cc0 8734   1c1 8735   _ici 8736    + caddc 8737    x. cmul 8739
This theorem is referenced by:  0re  8835  peano2re  8982  mul02lem2  8986  addid1  8989  renegcl  9107  peano2rem  9110  0reALT  9140  0lt1  9293  0le1  9294  1le1  9393  eqneg  9477  ltp1  9591  ltm1  9593  recgt0  9597  mulgt1  9612  ltmulgt11  9613  lemulge11  9615  ltrec  9634  reclt1  9648  recgt1  9649  recgt1i  9650  recp1lt1  9651  recreclt  9652  recgt0ii  9659  ledivp1i  9679  ltdivp1i  9680  inelr  9733  cju  9739  nnssre  9747  nnge1  9769  nngt1ne1  9770  nnle1eq1  9771  nngt0  9772  nnnlt1  9773  nnrecre  9779  nnrecgt0  9780  nnsub  9781  2re  9812  3re  9814  4re  9816  5re  9818  6re  9819  7re  9820  8re  9821  9re  9822  10re  9823  2pos  9825  3pos  9827  4pos  9829  5pos  9830  6pos  9831  7pos  9832  8pos  9833  9pos  9834  10pos  9835  1lt2  9883  1lt3  9885  1lt4  9888  1lt5  9892  1lt6  9897  1lt7  9903  1lt8  9910  1lt9  9918  1lt10  9927  1ne2  9928  halflt1  9930  addltmul  9944  nnunb  9958  elnnnn0c  10006  elnnz1  10046  znnnlt1  10047  zltp1le  10064  zleltp1  10065  recnz  10084  gtndiv  10086  suprzcl  10088  uzindOLD  10103  eluzp1m1  10248  eluzp1p1  10250  eluz2b2  10287  zbtwnre  10311  rebtwnz  10312  1rp  10355  qbtwnre  10522  qbtwnxr  10523  xmulid1  10595  xmulid2  10596  xmulm1  10597  x2times  10615  xrub  10626  0elunit  10750  1elunit  10751  lincmb01cmp  10773  iccf1o  10774  xov1plusxeqvd  10776  unitssre  10777  fztpval  10841  fraclt1  10930  fracle1  10931  flbi2  10943  fladdz  10946  flhalf  10950  fldiv  10960  modid  10989  1mod  10992  seqf1olem1  11081  reexpcl  11116  reexpclz  11119  expge0  11134  expge1  11135  expgt1  11136  ltexp2a  11149  expcan  11150  ltexp2  11151  leexp2  11152  leexp2a  11153  leexp2r  11155  nnlesq  11202  bernneq  11223  bernneq2  11224  bernneq3  11225  expnbnd  11226  expnlbnd  11227  expnlbnd2  11228  expmulnbnd  11229  discr1  11233  facwordi  11298  faclbnd3  11301  faclbnd4lem1  11302  faclbnd4lem4  11305  faclbnd6  11308  facavg  11310  fzsdom2  11378  hashfun  11385  crre  11595  remim  11598  cjexp  11631  re1  11635  im1  11636  rei  11637  imi  11638  sqrlem1  11724  sqrlem2  11725  sqrlem3  11726  sqrlem4  11727  sqrlem7  11730  resqrex  11732  sqr1  11753  sqr2gt1lt2  11756  sqrm1  11757  abs1  11778  rddif  11820  absrdbnd  11821  caubnd2  11837  mulcn2  12065  reccn2  12066  rlimo1  12086  rlimno1  12123  iseraltlem2  12151  iseraltlem3  12152  iseralt  12153  o1fsum  12267  abscvgcvg  12273  climcndslem1  12304  climcndslem2  12305  flo1  12309  harmonic  12313  expcnv  12318  geolim  12322  geolim2  12323  georeclim  12324  geo2lim  12327  geomulcvg  12328  geoisumr  12330  geoisum1c  12332  geoihalfsum  12334  efcllem  12355  ere  12366  ege2le3  12367  efgt1  12392  resin4p  12414  recos4p  12415  tanhlt1  12436  tanhbnd  12437  sinbnd  12456  cosbnd  12457  sinbnd2  12458  cosbnd2  12459  ef01bndlem  12460  sin01bnd  12461  cos01bnd  12462  cos1bnd  12463  cos2bnd  12464  sinltx  12465  sin01gt0  12466  cos01gt0  12467  sin02gt0  12468  sincos1sgn  12469  eirrlem  12478  rpnnen2lem2  12490  rpnnen2lem3  12491  rpnnen2lem4  12492  rpnnen2lem9  12497  rpnnen2  12500  rpnnen  12501  ruclem6  12509  ruclem11  12514  ruclem12  12515  nthruz  12526  3dvds  12587  bitsfzolem  12621  bitsfzo  12622  bitsmod  12623  bitscmp  12625  bitsinv1lem  12628  sadcadd  12645  smuval2  12669  isprm3  12763  prmind2  12765  sqnprm  12773  coprm  12775  isprm5  12787  divdenle  12816  zsqrelqelz  12825  phibndlem  12834  fermltl  12848  odzdvds  12856  pythagtriplem3  12867  iserodd  12884  pcmpt  12936  fldivp1  12941  pcfaclem  12942  pockthi  12950  infpn2  12956  prmreclem1  12959  prmreclem5  12963  4sqlem11  12998  4sqlem12  12999  ramub1lem1  13069  2expltfac  13101  resslem  13197  rescbas  13702  rescabs  13706  odubas  14233  lt6abl  15177  pgpfaclem2  15313  abvneg  15595  abvtrivd  15601  xrsmcmn  16393  resubdrg  16419  gzrngunitlem  16432  gzrngunit  16433  znidomb  16511  thlbas  16592  leordtval2  16938  setsmsbas  18017  dscmet  18091  dscopn  18092  nrginvrcnlem  18197  nmoid  18247  idnghm  18248  tgioo  18298  blcvx  18300  xrsmopn  18314  metnrmlem1a  18358  metnrmlem1  18359  iitopon  18379  dfii2  18382  dfii3  18383  dfii5  18385  iicmp  18386  iicon  18387  iirev  18423  iirevcn  18424  iihalf1  18425  iihalf1cn  18426  iihalf2  18427  iihalf2cn  18428  elii1  18429  elii2  18430  iimulcl  18431  iimulcn  18432  icchmeo  18435  icopnfcnv  18436  icopnfhmeo  18437  iccpnfcnv  18438  iccpnfhmeo  18439  xrhmeo  18440  xrhmph  18441  icccvx  18444  evth  18453  xlebnum  18459  lebnumii  18460  htpycc  18474  reparphti  18491  pcoval1  18507  pco0  18508  pco1  18509  pcoval2  18510  pcocn  18511  pcohtpylem  18513  pcopt  18516  pcopt2  18517  pcoass  18518  pcorevlem  18520  pcorev2  18522  pi1xfrcnv  18551  nmhmcn  18597  cncmet  18740  ovolunlem1a  18851  ovoliunlem1  18857  dyadmaxlem  18948  vitalilem1  18959  vitalilem2  18960  vitalilem4  18962  vitalilem5  18963  vitali  18964  mbfneg  19001  i1f1  19041  itg11  19042  i1fsub  19059  itg1sub  19060  mbfi1fseqlem6  19071  itg2const  19091  itg2mulc  19098  itg2monolem1  19101  itg2monolem3  19103  iblcnlem1  19138  i1fibl  19158  itgitg1  19159  dveflem  19322  mvth  19335  dvlipcn  19337  lhop1lem  19356  dvcvx  19363  dvfsumlem1  19369  dvfsumlem2  19370  dvfsumlem3  19371  dvfsumlem4  19372  dvfsum2  19377  ply1remlem  19544  fta1glem2  19548  fta1blem  19550  plyeq0lem  19588  fta1lem  19683  vieta1lem2  19687  aalioulem3  19710  aalioulem4  19711  aalioulem5  19712  aaliou3lem2  19719  aaliou3lem8  19721  ulmbdd  19771  iblulm  19779  radcnvlem1  19785  radcnvlem2  19786  dvradcnv  19793  abelthlem2  19804  abelthlem3  19805  abelthlem5  19807  abelthlem7  19810  abelth  19813  abelth2  19814  reeff1olem  19818  reeff1o  19819  sinhalfpilem  19830  tangtx  19869  sincos4thpi  19877  pige3  19881  coskpi  19884  cosne0  19888  recosf1o  19893  tanregt0  19897  efif1olem3  19902  efif1olem4  19903  loge  19936  rplogcl  19954  logdivlti  19967  logno1  19979  logcnlem4  19988  logf1o2  19993  dvlog2lem  19995  advlog  19997  logtayllem  20002  logtayl  20003  logccv  20006  recxpcl  20018  cxplt  20037  cxple  20038  cxplea  20039  cxpsqrlem  20045  cxpsqr  20046  cxpcn3lem  20083  cxpaddlelem  20087  cxpaddle  20088  loglesqr  20094  ang180lem1  20103  ang180lem2  20104  ang180lem3  20105  isosctrlem1  20114  isosctrlem2  20115  angpined  20123  chordthmlem4  20128  1cubrlem  20133  atanre  20177  asinsin  20184  acosrecl  20195  atandmcj  20201  atancj  20202  atanlogaddlem  20205  atantan  20215  bndatandm  20221  atans2  20223  ressatans  20226  leibpilem2  20233  leibpi  20234  leibpisum  20235  log2tlbnd  20237  birthdaylem3  20244  birthday  20245  rlimcnp  20256  rlimcnp2  20257  efrlim  20260  cxp2limlem  20266  cxp2lim  20267  cxploglim  20268  cxploglim2  20269  divsqrsumlem  20270  divsqrsumo1  20274  cvxcl  20275  scvxcvx  20276  jensenlem2  20278  amgmlem  20280  emcllem2  20286  emcllem4  20288  emcllem6  20290  emcllem7  20291  emre  20295  emgt0  20296  harmonicbnd3  20297  harmonicubnd  20299  harmonicbnd4  20300  fsumharmonic  20301  wilthlem1  20302  wilthlem2  20303  ftalem1  20306  ftalem2  20307  ftalem5  20310  basellem3  20316  basellem9  20322  issqf  20370  cht1  20399  vma1  20400  chp1  20401  ppieq0  20410  ppiltx  20411  mumullem2  20414  fsumfldivdiaglem  20425  ppiublem1  20437  ppiub  20439  chpeq0  20443  chtublem  20446  chtub  20447  chpval2  20453  chpchtsum  20454  chpub  20455  logfacbnd3  20458  logfacrlim  20459  logexprlim  20460  mersenne  20462  perfectlem2  20465  dchrelbas4  20478  dchrinv  20496  dchr1re  20498  bcmono  20512  efexple  20516  bposlem1  20519  bposlem2  20520  bposlem5  20523  bposlem8  20526  lgslem3  20533  lgslem4  20534  lgsvalmod  20550  lgsmod  20556  lgsdir2lem1  20558  lgsdir2lem3  20560  lgsdir2lem4  20561  lgsdir2lem5  20562  lgsdirprm  20564  lgsdir  20565  lgsne0  20568  lgsabs1  20569  lgsdinn0  20575  lgseisen  20588  lgsquadlem2  20590  m1lgs  20597  2sqlem8  20607  chebbnd1lem1  20614  chebbnd1lem2  20615  chebbnd1lem3  20616  chebbnd1  20617  chtppilimlem1  20618  chtppilimlem2  20619  chtppilim  20620  chebbnd2  20622  chto1lb  20623  chpchtlim  20624  chpo1ubb  20626  vmadivsum  20627  vmadivsumb  20628  rplogsumlem1  20629  rplogsumlem2  20630  rpvmasumlem  20632  dchrisumlem3  20636  dchrmusumlema  20638  dchrmusum2  20639  dchrvmasumlem2  20643  dchrvmasumlem3  20644  dchrvmasumiflem1  20646  dchrvmasumiflem2  20647  dchrisum0flblem1  20653  dchrisum0flblem2  20654  dchrisum0fno1  20656  rpvmasum2  20657  dchrisum0re  20658  dchrisum0lema  20659  dchrisum0lem1b  20660  dchrisum0lem1  20661  dchrisum0lem2a  20662  dchrisum0lem2  20663  dchrisum0lem3  20664  rplogsum  20672  dirith2  20673  mudivsum  20675  mulogsumlem  20676  mulogsum  20677  logdivsum  20678  mulog2sumlem1  20679  mulog2sumlem2  20680  vmalogdivsum2  20683  2vmadivsumlem  20685  log2sumbnd  20689  selberglem2  20691  selbergb  20694  selberg2lem  20695  selberg2b  20697  chpdifbndlem1  20698  chpdifbnd  20700  selberg3lem1  20702  selberg3lem2  20703  selberg4lem1  20705  pntrmax  20709  pntrsumo1  20710  pntrsumbnd  20711  selberg34r  20716  selbergsb  20720  pntrlog2bndlem1  20722  pntrlog2bndlem2  20723  pntrlog2bndlem3  20724  pntrlog2bndlem4  20725  pntrlog2bndlem5  20726  pntrlog2bndlem6  20728  pntrlog2bnd  20729  pntpbnd1a  20730  pntpbnd1  20731  pntpbnd2  20732  pntibndlem1  20734  pntibndlem2a  20735  pntibndlem2  20736  pntibndlem3  20737  pntibnd  20738  pntlemd  20739  pntlemc  20740  pntlemb  20742  pntlemg  20743  pntlemr  20747  pntlemf  20750  pntlemk  20751  pntlemo  20752  pntlem3  20754  pntleml  20756  pnt  20759  abvcxp  20760  ostth2lem1  20763  qabvle  20770  padicabvf  20776  padicabvcxp  20777  ostth1  20778  ostth2lem2  20779  ostth2lem3  20780  ostth2lem4  20781  ostth2  20782  ostth3  20783  ostth  20784  ex-dif  20787  ex-in  20789  ex-pss  20792  ex-res  20805  ex-fl  20811  nv1  21236  smcnlem  21264  ipidsq  21280  nmoub3i  21345  nmlno0lem  21365  blocnilem  21376  ipasslem10  21411  ubthlem2  21444  minvecolem4  21453  htthlem  21491  hisubcomi  21677  normlem9  21691  norm-ii-i  21710  bcs2  21755  norm1  21822  nmopub2tALT  22483  nmfnleub2  22500  nmlnop0iALT  22569  nmopun  22588  unopbd  22589  hmopd  22596  nmcexi  22600  nmopadjlem  22663  nmopcoi  22669  nmopcoadji  22675  opsqrlem4  22717  pjnmopi  22722  pjbdlni  22723  stcl  22790  stge0  22798  stle1  22799  hstle1  22800  hstle  22804  hstles  22805  stge1i  22812  stlesi  22815  staddi  22820  stadd3i  22822  strlem1  22824  strlem3a  22826  strlem5  22829  jplem1  22842  cdj1i  23007  addltmulALT  23020  fzsplit3  23025  ballotlem2  23042  ballotlemfc0  23046  ballotlemfcc  23047  ballotlem4  23052  ballotlemi1  23056  ballotlemic  23060  ballotlem1c  23061  ballotlemsgt1  23064  ballotlemsel1i  23066  ballotlemfrcn0  23083  zetacvg  23095  subfacp1lem1  23116  subfacp1lem5  23121  subfacval2  23124  subfaclim  23125  subfacval3  23126  cvxpcon  23179  cvxscon  23180  rescon  23183  iiscon  23189  iillyscon  23190  cvmliftlem2  23223  cvmliftlem8  23229  cvmliftlem13  23233  konigsberg  23317  snmlff  23318  sinccvglem  23411  divelunit  23485  dedekind  23487  relin01  23494  fznatpl1  23498  fz0n  23502  brbtwn2  23942  colinearalglem4  23946  ax5seglem1  23965  ax5seglem2  23966  ax5seglem3  23968  ax5seglem5  23970  ax5seglem6  23971  ax5seglem9  23974  ax5seg  23975  axbtwnid  23976  axpaschlem  23977  axpasch  23978  axlowdimlem3  23981  axlowdimlem6  23984  axlowdimlem7  23985  axlowdimlem10  23988  axlowdimlem16  23994  axlowdimlem17  23995  axlowdim1  23996  axlowdim2  23997  axlowdim  23998  axeuclidlem  23999  axcontlem2  24002  axcontlem4  24004  axcontlem7  24007  bpoly4  24203  cntrset  25003  fnckle  25446  nn0prpwlem  25639  fdc  25856  incsequz  25859  geomcau  25876  totbndbnd  25914  cntotbnd  25921  heiborlem8  25943  bfplem2  25948  bfp  25949  lzenom  26250  rabren3dioph  26299  irrapxlem1  26308  irrapxlem2  26309  irrapxlem4  26311  irrapxlem5  26312  pellexlem2  26316  pellexlem5  26319  pellexlem6  26320  pell1qrge1  26356  pell1qr1  26357  elpell1qr2  26358  pell1qrgaplem  26359  pell14qrgap  26361  pell14qrgapw  26362  pellqrex  26365  pellfundre  26367  pellfundgt1  26369  pellfundlb  26370  pellfundglb  26371  pellfundex  26372  pellfund14gap  26373  pellfundrp  26374  pellfundne1  26375  rmspecsqrnq  26392  rmspecnonsq  26393  rmspecfund  26395  rmspecpos  26402  monotoddzzfi  26428  jm2.17a  26448  rmygeid  26452  acongeq  26471  jm2.23  26490  jm3.1lem2  26512  matbas  26869  lhe4.4ex1a  26947  fmul01  27111  fmuldfeq  27114  fmul01lt1lem1  27115  fmul01lt1lem2  27116  climsuselem1  27134  stoweidlem1  27151  stoweidlem3  27153  stoweidlem5  27155  stoweidlem7  27157  stoweidlem10  27160  stoweidlem11  27161  stoweidlem12  27162  stoweidlem13  27163  stoweidlem14  27164  stoweidlem16  27166  stoweidlem18  27168  stoweidlem19  27169  stoweidlem20  27170  stoweidlem22  27172  stoweidlem24  27174  stoweidlem25  27175  stoweidlem26  27176  stoweidlem28  27178  stoweidlem30  27180  stoweidlem34  27184  stoweidlem36  27186  stoweidlem38  27188  stoweidlem40  27190  stoweidlem41  27191  stoweidlem42  27192  stoweidlem44  27194  stoweidlem45  27195  stoweidlem51  27201  stoweidlem59  27209  stoweidlem60  27210  stoweidlem62  27212  stoweid  27213  wallispilem3  27217  wallispilem4  27218  wallispilem5  27219  wallispi  27220  wallispi2lem1  27221  wallispi2lem2  27222  wallispi2  27223  stirlinglem1  27224  stirlinglem3  27226  stirlinglem5  27228  stirlinglem6  27229  stirlinglem7  27230  stirlinglem8  27231  stirlinglem10  27233  stirlinglem11  27234  stirlinglem12  27235  stirlinglem13  27236  stirlinglem15  27238  reseccl  27485  recsccl  27486  sgn1  27511
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1638  ax-8 1646  ax-6 1706  ax-7 1711  ax-11 1718  ax-12 1870  ax-ext 2267  ax-1cn 8792  ax-icn 8793  ax-addcl 8794  ax-mulcl 8796  ax-mulrcl 8797  ax-i2m1 8802  ax-1ne0 8803  ax-rrecex 8806  ax-cnre 8807
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 938  df-tru 1312  df-ex 1531  df-nf 1534  df-sb 1633  df-clab 2273  df-cleq 2279  df-clel 2282  df-nfc 2411  df-ne 2451  df-ral 2551  df-rex 2552  df-rab 2555  df-v 2793  df-dif 3158  df-un 3160  df-in 3162  df-ss 3169  df-nul 3459  df-if 3569  df-sn 3649  df-pr 3650  df-op 3652  df-uni 3831  df-br 4027  df-opab 4081  df-xp 4696  df-cnv 4698  df-dm 4700  df-rn 4701  df-res 4702  df-ima 4703  df-fv 5231  df-ov 5824
  Copyright terms: Public domain W3C validator