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

Theorem 1re 8770
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 8728, 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 8739 . . 3  |-  1  =/=  0
2 ax-1cn 8728 . . . . 5  |-  1  e.  CC
3 ax-cnre 8743 . . . . 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 8764 . . . . . . . 8  |-  0  e.  CC
8 ax-cnre 8743 . . . . . . . 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 2625 . . . . . . . 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 2625 . . . . . . 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 2625 . . . . 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 2625 . . . 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 5765 . . . . . . . . 9  |-  ( b  =  d  ->  (
_i  x.  b )  =  ( _i  x.  d ) )
2725, 26oveqan12d 5776 . . . . . . . 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 2843 . . . . . . . . 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 2843 . . . . . . . . 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 2645 . . . 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 2643 . . 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 2835 . . . . . . . 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 2835 . . . . . . 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 2643 . 2  |-  ( E. x  e.  RR  E. y  e.  RR  x  =/=  y  ->  E. z  e.  RR  z  =/=  0
)
61 ax-rrecex 8742 . . . 4  |-  ( ( z  e.  RR  /\  z  =/=  0 )  ->  E. x  e.  RR  ( z  x.  x
)  =  1 )
62 remulcl 8755 . . . . . . 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 2638 . . . 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 2633 . 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 5757   CCcc 8668   RRcr 8669   0cc0 8670   1c1 8671   _ici 8672    + caddc 8673    x. cmul 8675
This theorem is referenced by:  0re  8771  peano2re  8918  mul02lem2  8922  addid1  8925  renegcl  9043  peano2rem  9046  0reALT  9076  0lt1  9229  0le1  9230  1le1  9329  eqneg  9413  ltp1  9527  ltm1  9529  recgt0  9533  mulgt1  9548  ltmulgt11  9549  lemulge11  9551  ltrec  9570  reclt1  9584  recgt1  9585  recgt1i  9586  recp1lt1  9587  recreclt  9588  recgt0ii  9595  ledivp1i  9615  ltdivp1i  9616  inelr  9669  cju  9675  nnssre  9683  nnge1  9705  nngt1ne1  9706  nnle1eq1  9707  nngt0  9708  nnnlt1  9709  nnrecre  9715  nnrecgt0  9716  nnsub  9717  2re  9748  3re  9750  4re  9752  5re  9754  6re  9755  7re  9756  8re  9757  9re  9758  10re  9759  2pos  9761  3pos  9763  4pos  9765  5pos  9766  6pos  9767  7pos  9768  8pos  9769  9pos  9770  10pos  9771  1lt2  9818  1lt3  9820  1lt4  9823  1lt5  9827  1lt6  9832  1lt7  9838  1lt8  9845  1lt9  9853  1lt10  9862  1ne2  9863  halflt1  9865  addltmul  9879  nnunb  9893  elnnnn0c  9941  elnnz1  9981  znnnlt1  9982  zltp1le  9999  zleltp1  10000  recnz  10019  gtndiv  10021  suprzcl  10023  uzindOLD  10038  eluzp1m1  10183  eluzp1p1  10185  eluz2b2  10222  zbtwnre  10246  rebtwnz  10247  1rp  10290  qbtwnre  10457  qbtwnxr  10458  xmulid1  10530  xmulid2  10531  xmulm1  10532  x2times  10550  xrub  10561  0elunit  10685  1elunit  10686  lincmb01cmp  10708  iccf1o  10709  xov1plusxeqvd  10711  unitssre  10712  fztpval  10776  fraclt1  10865  fracle1  10866  flbi2  10878  fladdz  10881  flhalf  10885  fldiv  10895  modid  10924  1mod  10927  seqf1olem1  11016  reexpcl  11051  reexpclz  11054  expge0  11069  expge1  11070  expgt1  11071  ltexp2a  11084  expcan  11085  ltexp2  11086  leexp2  11087  leexp2a  11088  leexp2r  11090  nnlesq  11137  bernneq  11158  bernneq2  11159  bernneq3  11160  expnbnd  11161  expnlbnd  11162  expnlbnd2  11163  expmulnbnd  11164  discr1  11168  facwordi  11233  faclbnd3  11236  faclbnd4lem1  11237  faclbnd4lem4  11240  faclbnd6  11243  facavg  11245  fzsdom2  11312  hashfun  11319  crre  11529  remim  11532  cjexp  11565  re1  11569  im1  11570  rei  11571  imi  11572  sqrlem1  11658  sqrlem2  11659  sqrlem3  11660  sqrlem4  11661  sqrlem7  11664  resqrex  11666  sqr1  11687  sqr2gt1lt2  11690  sqrm1  11691  abs1  11712  rddif  11754  absrdbnd  11755  caubnd2  11771  mulcn2  11999  reccn2  12000  rlimo1  12020  rlimno1  12057  iseraltlem2  12085  iseraltlem3  12086  iseralt  12087  o1fsum  12201  abscvgcvg  12207  climcndslem1  12235  climcndslem2  12236  flo1  12240  harmonic  12244  expcnv  12249  geolim  12253  geolim2  12254  georeclim  12255  geo2lim  12258  geomulcvg  12259  geoisumr  12261  geoisum1c  12263  geoihalfsum  12265  efcllem  12286  ere  12297  ege2le3  12298  efgt1  12323  resin4p  12345  recos4p  12346  tanhlt1  12367  tanhbnd  12368  sinbnd  12387  cosbnd  12388  sinbnd2  12389  cosbnd2  12390  ef01bndlem  12391  sin01bnd  12392  cos01bnd  12393  cos1bnd  12394  cos2bnd  12395  sinltx  12396  sin01gt0  12397  cos01gt0  12398  sin02gt0  12399  sincos1sgn  12400  eirrlem  12409  rpnnen2lem2  12421  rpnnen2lem3  12422  rpnnen2lem4  12423  rpnnen2lem9  12428  rpnnen2  12431  rpnnen  12432  ruclem6  12440  ruclem11  12445  ruclem12  12446  nthruz  12457  3dvds  12518  bitsfzolem  12552  bitsfzo  12553  bitsmod  12554  bitscmp  12556  bitsinv1lem  12559  sadcadd  12576  smuval2  12600  isprm3  12694  prmind2  12696  sqnprm  12704  coprm  12706  isprm5  12718  divdenle  12747  zsqrelqelz  12756  phibndlem  12765  fermltl  12779  odzdvds  12787  pythagtriplem3  12798  iserodd  12815  pcmpt  12867  fldivp1  12872  pcfaclem  12873  pockthi  12881  infpn2  12887  prmreclem1  12890  prmreclem5  12894  4sqlem11  12929  4sqlem12  12930  ramub1lem1  13000  2expltfac  13032  resslem  13128  rescbas  13633  rescabs  13637  odubas  14164  lt6abl  15108  pgpfaclem2  15244  abvneg  15526  abvtrivd  15532  xrsmcmn  16324  resubdrg  16350  gzrngunitlem  16363  gzrngunit  16364  znidomb  16442  thlbas  16523  leordtval2  16869  setsmsbas  17948  dscmet  18022  dscopn  18023  nrginvrcnlem  18128  nmoid  18178  idnghm  18179  tgioo  18229  blcvx  18231  xrsmopn  18245  metnrmlem1a  18289  metnrmlem1  18290  iitopon  18310  dfii2  18313  dfii3  18314  dfii5  18316  iicmp  18317  iicon  18318  iirev  18354  iirevcn  18355  iihalf1  18356  iihalf1cn  18357  iihalf2  18358  iihalf2cn  18359  elii1  18360  elii2  18361  iimulcl  18362  iimulcn  18363  icchmeo  18366  icopnfcnv  18367  icopnfhmeo  18368  iccpnfcnv  18369  iccpnfhmeo  18370  xrhmeo  18371  xrhmph  18372  icccvx  18375  evth  18384  xlebnum  18390  lebnumii  18391  htpycc  18405  reparphti  18422  pcoval1  18438  pco0  18439  pco1  18440  pcoval2  18441  pcocn  18442  pcohtpylem  18444  pcopt  18447  pcopt2  18448  pcoass  18449  pcorevlem  18451  pcorev2  18453  pi1xfrcnv  18482  nmhmcn  18528  cncmet  18671  ovolunlem1a  18782  ovoliunlem1  18788  dyadmaxlem  18879  vitalilem1  18890  vitalilem2  18891  vitalilem4  18893  vitalilem5  18894  vitali  18895  mbfneg  18932  i1f1  18972  itg11  18973  i1fsub  18990  itg1sub  18991  mbfi1fseqlem6  19002  itg2const  19022  itg2mulc  19029  itg2monolem1  19032  itg2monolem3  19034  iblcnlem1  19069  i1fibl  19089  itgitg1  19090  dveflem  19253  mvth  19266  dvlipcn  19268  lhop1lem  19287  dvcvx  19294  dvfsumlem1  19300  dvfsumlem2  19301  dvfsumlem3  19302  dvfsumlem4  19303  dvfsum2  19308  ply1remlem  19475  fta1glem2  19479  fta1blem  19481  plyeq0lem  19519  fta1lem  19614  vieta1lem2  19618  aalioulem3  19641  aalioulem4  19642  aalioulem5  19643  aaliou3lem2  19650  aaliou3lem8  19652  ulmbdd  19702  iblulm  19710  radcnvlem1  19716  radcnvlem2  19717  dvradcnv  19724  abelthlem2  19735  abelthlem3  19736  abelthlem5  19738  abelthlem7  19741  abelth  19744  abelth2  19745  reeff1olem  19749  reeff1o  19750  sinhalfpilem  19761  tangtx  19800  sincos4thpi  19808  pige3  19812  coskpi  19815  cosne0  19819  recosf1o  19824  tanregt0  19828  efif1olem3  19833  efif1olem4  19834  loge  19867  rplogcl  19885  logdivlti  19898  logno1  19910  logcnlem4  19919  logf1o2  19924  dvlog2lem  19926  advlog  19928  logtayllem  19933  logtayl  19934  logccv  19937  recxpcl  19949  cxplt  19968  cxple  19969  cxplea  19970  cxpsqrlem  19976  cxpsqr  19977  cxpcn3lem  20014  cxpaddlelem  20018  cxpaddle  20019  loglesqr  20025  ang180lem1  20034  ang180lem2  20035  ang180lem3  20036  isosctrlem1  20045  isosctrlem2  20046  angpined  20054  chordthmlem4  20059  1cubrlem  20064  atanre  20108  asinsin  20115  acosrecl  20126  atandmcj  20132  atancj  20133  atanlogaddlem  20136  atantan  20146  bndatandm  20152  atans2  20154  ressatans  20157  leibpilem2  20164  leibpi  20165  leibpisum  20166  log2tlbnd  20168  birthdaylem3  20175  birthday  20176  rlimcnp  20187  rlimcnp2  20188  efrlim  20191  cxp2limlem  20197  cxp2lim  20198  cxploglim  20199  cxploglim2  20200  divsqrsumlem  20201  divsqrsumo1  20205  cvxcl  20206  scvxcvx  20207  jensenlem2  20209  amgmlem  20211  emcllem2  20217  emcllem4  20219  emcllem6  20221  emcllem7  20222  emre  20226  emgt0  20227  harmonicbnd3  20228  harmonicubnd  20230  harmonicbnd4  20231  fsumharmonic  20232  wilthlem1  20233  wilthlem2  20234  ftalem1  20237  ftalem2  20238  ftalem5  20241  basellem3  20247  basellem9  20253  issqf  20301  cht1  20330  vma1  20331  chp1  20332  ppieq0  20341  ppiltx  20342  mumullem2  20345  fsumfldivdiaglem  20356  ppiublem1  20368  ppiub  20370  chpeq0  20374  chtublem  20377  chtub  20378  chpval2  20384  chpchtsum  20385  chpub  20386  logfacbnd3  20389  logfacrlim  20390  logexprlim  20391  mersenne  20393  perfectlem2  20396  dchrelbas4  20409  dchrinv  20427  dchr1re  20429  bcmono  20443  efexple  20447  bposlem1  20450  bposlem2  20451  bposlem5  20454  bposlem8  20457  lgslem3  20464  lgslem4  20465  lgsvalmod  20481  lgsmod  20487  lgsdir2lem1  20489  lgsdir2lem3  20491  lgsdir2lem4  20492  lgsdir2lem5  20493  lgsdirprm  20495  lgsdir  20496  lgsne0  20499  lgsabs1  20500  lgsdinn0  20506  lgseisen  20519  lgsquadlem2  20521  m1lgs  20528  2sqlem8  20538  chebbnd1lem1  20545  chebbnd1lem2  20546  chebbnd1lem3  20547  chebbnd1  20548  chtppilimlem1  20549  chtppilimlem2  20550  chtppilim  20551  chebbnd2  20553  chto1lb  20554  chpchtlim  20555  chpo1ubb  20557  vmadivsum  20558  vmadivsumb  20559  rplogsumlem1  20560  rplogsumlem2  20561  rpvmasumlem  20563  dchrisumlem3  20567  dchrmusumlema  20569  dchrmusum2  20570  dchrvmasumlem2  20574  dchrvmasumlem3  20575  dchrvmasumiflem1  20577  dchrvmasumiflem2  20578  dchrisum0flblem1  20584  dchrisum0flblem2  20585  dchrisum0fno1  20587  rpvmasum2  20588  dchrisum0re  20589  dchrisum0lema  20590  dchrisum0lem1b  20591  dchrisum0lem1  20592  dchrisum0lem2a  20593  dchrisum0lem2  20594  dchrisum0lem3  20595  rplogsum  20603  dirith2  20604  mudivsum  20606  mulogsumlem  20607  mulogsum  20608  logdivsum  20609  mulog2sumlem1  20610  mulog2sumlem2  20611  vmalogdivsum2  20614  2vmadivsumlem  20616  log2sumbnd  20620  selberglem2  20622  selbergb  20625  selberg2lem  20626  selberg2b  20628  chpdifbndlem1  20629  chpdifbnd  20631  selberg3lem1  20633  selberg3lem2  20634  selberg4lem1  20636  pntrmax  20640  pntrsumo1  20641  pntrsumbnd  20642  selberg34r  20647  selbergsb  20651  pntrlog2bndlem1  20653  pntrlog2bndlem2  20654  pntrlog2bndlem3  20655  pntrlog2bndlem4  20656  pntrlog2bndlem5  20657  pntrlog2bndlem6  20659  pntrlog2bnd  20660  pntpbnd1a  20661  pntpbnd1  20662  pntpbnd2  20663  pntibndlem1  20665  pntibndlem2a  20666  pntibndlem2  20667  pntibndlem3  20668  pntibnd  20669  pntlemd  20670  pntlemc  20671  pntlemb  20673  pntlemg  20674  pntlemr  20678  pntlemf  20681  pntlemk  20682  pntlemo  20683  pntlem3  20685  pntleml  20687  pnt  20690  abvcxp  20691  ostth2lem1  20694  qabvle  20701  padicabvf  20707  padicabvcxp  20708  ostth1  20709  ostth2lem2  20710  ostth2lem3  20711  ostth2lem4  20712  ostth2  20713  ostth3  20714  ostth  20715  ex-dif  20718  ex-in  20720  ex-pss  20723  ex-res  20736  ex-fl  20742  nv1  21167  smcnlem  21195  ipidsq  21211  nmoub3i  21276  nmlno0lem  21296  blocnilem  21307  ipasslem10  21342  ubthlem2  21375  minvecolem4  21384  htthlem  21422  hisubcomi  21608  normlem9  21622  norm-ii-i  21641  bcs2  21686  norm1  21753  nmopub2tALT  22414  nmfnleub2  22431  nmlnop0iALT  22500  nmopun  22519  unopbd  22520  hmopd  22527  nmcexi  22531  nmopadjlem  22594  nmopcoi  22600  nmopcoadji  22606  opsqrlem4  22648  pjnmopi  22653  pjbdlni  22654  stcl  22721  stge0  22729  stle1  22730  hstle1  22731  hstle  22735  hstles  22736  stge1i  22743  stlesi  22746  staddi  22751  stadd3i  22753  strlem1  22755  strlem3a  22757  strlem5  22760  jplem1  22773  cdj1i  22938  addltmulALT  22951  fzsplit3  22956  ballotlem2  22973  ballotlemfc0  22977  ballotlemfcc  22978  ballotlem4  22983  ballotlemi1  22987  ballotlemic  22991  ballotlem1c  22992  ballotlemsgt1  22995  ballotlemsel1i  22997  ballotlemfrcn0  23014  zetacvg  23026  subfacp1lem1  23047  subfacp1lem5  23052  subfacval2  23055  subfaclim  23056  subfacval3  23057  cvxpcon  23110  cvxscon  23111  rescon  23114  iiscon  23120  iillyscon  23121  cvmliftlem2  23154  cvmliftlem8  23160  cvmliftlem13  23164  konigsberg  23248  snmlff  23249  sinccvglem  23342  divelunit  23416  dedekind  23418  relin01  23425  fznatpl1  23429  fz0n  23433  brbtwn2  23873  colinearalglem4  23877  ax5seglem1  23896  ax5seglem2  23897  ax5seglem3  23899  ax5seglem5  23901  ax5seglem6  23902  ax5seglem9  23905  ax5seg  23906  axbtwnid  23907  axpaschlem  23908  axpasch  23909  axlowdimlem3  23912  axlowdimlem6  23915  axlowdimlem7  23916  axlowdimlem10  23919  axlowdimlem16  23925  axlowdimlem17  23926  axlowdim1  23927  axlowdim2  23928  axlowdim  23929  axeuclidlem  23930  axcontlem2  23933  axcontlem4  23935  axcontlem7  23938  bpoly4  24134  cntrset  24934  fnckle  25377  nn0prpwlem  25570  fdc  25787  incsequz  25790  geomcau  25807  totbndbnd  25845  cntotbnd  25852  heiborlem8  25874  bfplem2  25879  bfp  25880  lzenom  26181  rabren3dioph  26230  irrapxlem1  26239  irrapxlem2  26240  irrapxlem4  26242  irrapxlem5  26243  pellexlem2  26247  pellexlem5  26250  pellexlem6  26251  pell1qrge1  26287  pell1qr1  26288  elpell1qr2  26289  pell1qrgaplem  26290  pell14qrgap  26292  pell14qrgapw  26293  pellqrex  26296  pellfundre  26298  pellfundgt1  26300  pellfundlb  26301  pellfundglb  26302  pellfundex  26303  pellfund14gap  26304  pellfundrp  26305  pellfundne1  26306  rmspecsqrnq  26323  rmspecnonsq  26324  rmspecfund  26326  rmspecpos  26333  monotoddzzfi  26359  jm2.17a  26379  rmygeid  26383  acongeq  26402  jm2.23  26421  jm3.1lem2  26443  matbas  26800  lhe4.4ex1a  26878  fmul01  27043  fmuldfeq  27046  fmul01lt1lem1  27047  fmul01lt1lem2  27048  stoweidlem1  27050  stoweidlem3  27052  stoweidlem5  27054  stoweidlem7  27056  stoweidlem10  27059  stoweidlem11  27060  stoweidlem12  27061  stoweidlem13  27062  stoweidlem14  27063  stoweidlem16  27065  stoweidlem18  27067  stoweidlem19  27068  stoweidlem20  27069  stoweidlem22  27071  stoweidlem24  27073  stoweidlem25  27074  stoweidlem26  27075  stoweidlem28  27077  stoweidlem30  27079  stoweidlem34  27083  stoweidlem36  27085  stoweidlem38  27087  stoweidlem40  27089  stoweidlem41  27090  stoweidlem42  27091  stoweidlem44  27093  stoweidlem45  27094  stoweidlem51  27100  stoweidlem59  27108  stoweidlem60  27109  stoweidlem62  27111  stoweid  27112  reseccl  27235  recsccl  27236  sgn1  27261
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 8728  ax-icn 8729  ax-addcl 8730  ax-mulcl 8732  ax-mulrcl 8733  ax-i2m1 8738  ax-1ne0 8739  ax-rrecex 8742  ax-cnre 8743
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 2520  df-rex 2521  df-rab 2523  df-v 2742  df-dif 3097  df-un 3099  df-in 3101  df-ss 3108  df-nul 3398  df-if 3507  df-sn 3587  df-pr 3588  df-op 3590  df-uni 3769  df-br 3964  df-opab 4018  df-xp 4640  df-cnv 4642  df-dm 4644  df-rn 4645  df-res 4646  df-ima 4647  df-fv 4654  df-ov 5760
  Copyright terms: Public domain W3C validator