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

Theorem 1re 8714
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 8672, 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 8683 . . 3  |-  1  =/=  0
2 ax-1cn 8672 . . . . 5  |-  1  e.  CC
3 ax-cnre 8687 . . . . 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 8708 . . . . . . . 8  |-  0  e.  CC
8 ax-cnre 8687 . . . . . . . 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 2614 . . . . . . . 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 2614 . . . . . . 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 2614 . . . . 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 2614 . . . 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 5715 . . . . . . . . 9  |-  ( b  =  d  ->  (
_i  x.  b )  =  ( _i  x.  d ) )
2725, 26oveqan12d 5726 . . . . . . . 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 2827 . . . . . . . . 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 2827 . . . . . . . . 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 2634 . . . 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 2632 . . 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 2819 . . . . . . . 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 2819 . . . . . . 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 2486 . . 3  |-  ( ( x  e.  RR  /\  y  e.  RR )  ->  ( x  =/=  y  ->  E. z  e.  RR  z  =/=  0 ) )
6059rexlimivv 2632 . 2  |-  ( E. x  e.  RR  E. y  e.  RR  x  =/=  y  ->  E. z  e.  RR  z  =/=  0
)
61 ax-rrecex 8686 . . . 4  |-  ( ( z  e.  RR  /\  z  =/=  0 )  ->  E. x  e.  RR  ( z  x.  x
)  =  1 )
62 remulcl 8699 . . . . . . 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 2627 . . . 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 2622 . 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 2508  (class class class)co 5707   CCcc 8612   RRcr 8613   0cc0 8614   1c1 8615   _ici 8616    + caddc 8617    x. cmul 8619
This theorem is referenced by:  0re  8715  peano2re  8861  mul02lem2  8865  addid1  8868  renegcl  8982  peano2rem  8985  0reALT  9015  0lt1  9157  0le1  9158  1le1  9256  eqneg  9336  ltp1  9442  ltm1  9444  recgt0  9448  mulgt1  9463  ltmulgt11  9464  lemulge11  9466  ltrec  9485  reclt1  9499  recgt1  9500  recgt1i  9501  recp1lt1  9502  recreclt  9503  recgt0ii  9510  ledivp1i  9530  ltdivp1i  9531  inelr  9584  cju  9590  nnssre  9598  nnge1  9620  nngt1ne1  9621  nnle1eq1  9622  nngt0  9623  nnnlt1  9624  nnrecre  9630  nnrecgt0  9631  nnsub  9632  2re  9663  3re  9665  4re  9667  5re  9669  6re  9670  7re  9671  8re  9672  9re  9673  10re  9674  2pos  9676  3pos  9678  4pos  9680  5pos  9681  6pos  9682  7pos  9683  8pos  9684  9pos  9685  10pos  9686  1lt2  9733  1lt3  9735  1lt4  9738  1lt5  9742  1lt6  9747  1lt7  9753  1lt8  9760  1lt9  9768  1lt10  9777  1ne2  9778  halflt1  9780  addltmul  9794  nnunb  9807  elnnnn0c  9855  elnnz1  9895  znnnlt1  9896  zltp1le  9913  zleltp1  9914  recnz  9933  gtndiv  9935  suprzcl  9937  uzindOLD  9952  eluzp1m1  10097  eluzp1p1  10099  eluz2b2  10136  zbtwnre  10160  rebtwnz  10161  1rp  10204  qbtwnre  10371  qbtwnxr  10372  xmulid1  10444  xmulid2  10445  xmulm1  10446  x2times  10464  xrub  10475  0elunit  10599  1elunit  10600  lincmb01cmp  10622  iccf1o  10623  fztpval  10688  fraclt1  10777  fracle1  10778  flbi2  10790  fladdz  10793  flhalf  10797  fldiv  10807  modid  10836  1mod  10839  seqf1olem1  10928  reexpcl  10963  reexpclz  10966  expge0  10981  expge1  10982  expgt1  10983  ltexp2a  10996  expcan  10997  ltexp2  10998  leexp2  10999  leexp2a  11000  leexp2r  11002  nnlesq  11048  bernneq  11069  bernneq2  11070  bernneq3  11071  expnbnd  11072  expnlbnd  11073  expnlbnd2  11074  expmulnbnd  11075  discr1  11079  facwordi  11144  faclbnd3  11147  faclbnd4lem1  11148  faclbnd4lem4  11151  faclbnd6  11154  facavg  11156  fzsdom2  11223  hashfun  11230  crre  11440  remim  11443  cjexp  11476  re1  11480  im1  11481  rei  11482  imi  11483  sqrlem1  11569  sqrlem2  11570  sqrlem3  11571  sqrlem4  11572  sqrlem7  11575  resqrex  11577  sqr1  11598  sqr2gt1lt2  11601  sqrm1  11602  abs1  11621  rddif  11663  absrdbnd  11664  caubnd2  11680  mulcn2  11908  reccn2  11909  rlimo1  11929  rlimno1  11966  iseraltlem2  11994  iseraltlem3  11995  iseralt  11996  o1fsum  12110  abscvgcvg  12116  climcndslem1  12144  climcndslem2  12145  flo1  12149  harmonic  12153  expcnv  12158  geolim  12162  geolim2  12163  georeclim  12164  geo2lim  12167  geomulcvg  12168  geoisumr  12170  geoisum1c  12172  geoihalfsum  12174  efcllem  12195  ere  12206  ege2le3  12207  efgt1  12232  resin4p  12254  recos4p  12255  tanhlt1  12276  tanhbnd  12277  sinbnd  12296  cosbnd  12297  sinbnd2  12298  cosbnd2  12299  ef01bndlem  12300  sin01bnd  12301  cos01bnd  12302  cos1bnd  12303  cos2bnd  12304  sinltx  12305  sin01gt0  12306  cos01gt0  12307  sin02gt0  12308  sincos1sgn  12309  eirrlem  12318  rpnnen2lem2  12330  rpnnen2lem3  12331  rpnnen2lem4  12332  rpnnen2lem9  12337  rpnnen2  12340  rpnnen  12341  ruclem6  12349  ruclem11  12354  ruclem12  12355  nthruz  12366  3dvds  12427  bitsfzolem  12461  bitsfzo  12462  bitsmod  12463  bitscmp  12465  bitsinv1lem  12468  sadcadd  12485  smuval2  12509  isprm3  12603  prmind2  12605  sqnprm  12613  coprm  12615  isprm5  12627  divdenle  12656  zsqrelqelz  12665  phibndlem  12674  fermltl  12688  odzdvds  12696  pythagtriplem3  12707  iserodd  12724  pcmpt  12776  fldivp1  12781  pcfaclem  12782  pockthi  12790  infpn2  12796  prmreclem1  12799  prmreclem5  12803  4sqlem11  12838  4sqlem12  12839  ramub1lem1  12909  2expltfac  12941  resslem  13037  rescbas  13512  rescabs  13516  odubas  14043  lt6abl  14978  pgpfaclem2  15114  abvneg  15396  abvtrivd  15402  xrsmcmn  16191  resubdrg  16217  gzrngunitlem  16230  gzrngunit  16231  znidomb  16309  thlbas  16390  leordtval2  16736  setsmsbas  17815  dscmet  17889  dscopn  17890  nrginvrcnlem  17995  nmoid  18045  idnghm  18046  tgioo  18096  blcvx  18098  xrsmopn  18112  metnrmlem1a  18156  metnrmlem1  18157  iitopon  18177  dfii2  18180  dfii3  18181  dfii5  18183  iicmp  18184  iicon  18185  iirev  18221  iirevcn  18222  iihalf1  18223  iihalf1cn  18224  iihalf2  18225  iihalf2cn  18226  elii1  18227  elii2  18228  iimulcl  18229  iimulcn  18230  icchmeo  18233  icopnfcnv  18234  icopnfhmeo  18235  iccpnfcnv  18236  iccpnfhmeo  18237  xrhmeo  18238  xrhmph  18239  icccvx  18242  evth  18251  xlebnum  18257  lebnumii  18258  htpycc  18272  reparphti  18289  pcoval1  18305  pco0  18306  pco1  18307  pcoval2  18308  pcocn  18309  pcohtpylem  18311  pcopt  18314  pcopt2  18315  pcoass  18316  pcorevlem  18318  pcorev2  18320  pi1xfrcnv  18349  nmhmcn  18395  cncmet  18538  ovolunlem1a  18649  ovoliunlem1  18655  dyadmaxlem  18746  vitalilem1  18757  vitalilem2  18758  vitalilem4  18760  vitalilem5  18761  vitali  18762  mbfneg  18799  i1f1  18839  itg11  18840  i1fsub  18857  itg1sub  18858  mbfi1fseqlem6  18869  itg2const  18889  itg2mulc  18896  itg2monolem1  18899  itg2monolem3  18901  iblcnlem1  18936  i1fibl  18956  itgitg1  18957  dveflem  19120  mvth  19133  dvlipcn  19135  lhop1lem  19154  dvcvx  19161  dvfsumlem1  19167  dvfsumlem2  19168  dvfsumlem3  19169  dvfsumlem4  19170  dvfsum2  19175  ply1remlem  19342  fta1glem2  19346  fta1blem  19348  plyeq0lem  19386  fta1lem  19481  vieta1lem2  19485  aalioulem3  19508  aalioulem4  19509  aalioulem5  19510  aaliou3lem2  19517  aaliou3lem8  19519  ulmbdd  19569  iblulm  19577  radcnvlem1  19583  radcnvlem2  19584  dvradcnv  19591  abelthlem2  19602  abelthlem3  19603  abelthlem5  19605  abelthlem7  19608  abelth  19611  abelth2  19612  reeff1olem  19616  reeff1o  19617  sinhalfpilem  19628  tangtx  19663  sincos4thpi  19671  pige3  19675  coskpi  19678  cosne0  19682  recosf1o  19687  tanregt0  19691  efif1olem3  19695  efif1olem4  19696  loge  19726  rplogcl  19744  logdivlti  19755  logno1  19767  logcnlem4  19776  logf1o2  19781  dvlog2lem  19783  advlog  19785  logtayllem  19790  logtayl  19791  logccv  19794  ang180lem1  19798  ang180lem2  19799  ang180lem3  19800  isosctrlem1  19809  isosctrlem2  19810  recxpcl  19824  cxplt  19843  cxple  19844  cxplea  19845  cxpsqrlem  19851  cxpsqr  19852  cxpcn3lem  19889  cxpaddlelem  19893  cxpaddle  19894  loglesqr  19900  1cubrlem  19903  atanre  19947  asinsin  19954  acosrecl  19965  atandmcj  19971  atancj  19972  atanlogaddlem  19975  atantan  19985  bndatandm  19991  atans2  19993  ressatans  19996  leibpilem2  20003  leibpi  20004  leibpisum  20005  log2tlbnd  20007  birthdaylem3  20014  birthday  20015  rlimcnp  20026  rlimcnp2  20027  efrlim  20030  cxp2limlem  20036  cxp2lim  20037  cxploglim  20038  cxploglim2  20039  divsqrsumlem  20040  divsqrsumo1  20044  cvxcl  20045  scvxcvx  20046  jensenlem2  20048  amgmlem  20050  emcllem2  20056  emcllem4  20058  emcllem6  20060  emcllem7  20061  emre  20065  emgt0  20066  harmonicbnd3  20067  harmonicubnd  20069  harmonicbnd4  20070  fsumharmonic  20071  wilthlem1  20072  wilthlem2  20073  ftalem1  20076  ftalem2  20077  ftalem5  20080  basellem3  20086  basellem9  20092  issqf  20140  cht1  20169  vma1  20170  chp1  20171  ppieq0  20180  ppiltx  20181  mumullem2  20184  fsumfldivdiaglem  20195  ppiublem1  20207  ppiub  20209  chpeq0  20213  chtublem  20216  chtub  20217  chpval2  20223  chpchtsum  20224  chpub  20225  logfacbnd3  20228  logfacrlim  20229  logexprlim  20230  mersenne  20232  perfectlem2  20235  dchrelbas4  20248  dchrinv  20266  dchr1re  20268  bcmono  20282  efexple  20286  bposlem1  20289  bposlem2  20290  bposlem5  20293  bposlem8  20296  lgslem3  20303  lgslem4  20304  lgsvalmod  20320  lgsmod  20326  lgsdir2lem1  20328  lgsdir2lem3  20330  lgsdir2lem4  20331  lgsdir2lem5  20332  lgsdirprm  20334  lgsdir  20335  lgsne0  20338  lgsabs1  20339  lgsdinn0  20345  lgseisen  20358  lgsquadlem2  20360  m1lgs  20367  2sqlem8  20377  chebbnd1lem1  20384  chebbnd1lem2  20385  chebbnd1lem3  20386  chebbnd1  20387  chtppilimlem1  20388  chtppilimlem2  20389  chtppilim  20390  chebbnd2  20392  chto1lb  20393  chpchtlim  20394  chpo1ubb  20396  vmadivsum  20397  vmadivsumb  20398  rplogsumlem1  20399  rplogsumlem2  20400  rpvmasumlem  20402  dchrisumlem3  20406  dchrmusumlema  20408  dchrmusum2  20409  dchrvmasumlem2  20413  dchrvmasumlem3  20414  dchrvmasumiflem1  20416  dchrvmasumiflem2  20417  dchrisum0flblem1  20423  dchrisum0flblem2  20424  dchrisum0fno1  20426  rpvmasum2  20427  dchrisum0re  20428  dchrisum0lema  20429  dchrisum0lem1b  20430  dchrisum0lem1  20431  dchrisum0lem2a  20432  dchrisum0lem2  20433  dchrisum0lem3  20434  rplogsum  20442  dirith2  20443  mudivsum  20445  mulogsumlem  20446  mulogsum  20447  logdivsum  20448  mulog2sumlem1  20449  mulog2sumlem2  20450  vmalogdivsum2  20453  2vmadivsumlem  20455  log2sumbnd  20459  selberglem2  20461  selbergb  20464  selberg2lem  20465  selberg2b  20467  chpdifbndlem1  20468  chpdifbnd  20470  selberg3lem1  20472  selberg3lem2  20473  selberg4lem1  20475  pntrmax  20479  pntrsumo1  20480  pntrsumbnd  20481  selberg34r  20486  selbergsb  20490  pntrlog2bndlem1  20492  pntrlog2bndlem2  20493  pntrlog2bndlem3  20494  pntrlog2bndlem4  20495  pntrlog2bndlem5  20496  pntrlog2bndlem6  20498  pntrlog2bnd  20499  pntpbnd1a  20500  pntpbnd1  20501  pntpbnd2  20502  pntibndlem1  20504  pntibndlem2a  20505  pntibndlem2  20506  pntibndlem3  20507  pntibnd  20508  pntlemd  20509  pntlemc  20510  pntlemb  20512  pntlemg  20513  pntlemr  20517  pntlemf  20520  pntlemk  20521  pntlemo  20522  pntlem3  20524  pntleml  20526  pnt  20529  abvcxp  20530  ostth2lem1  20533  qabvle  20540  padicabvf  20546  padicabvcxp  20547  ostth1  20548  ostth2lem2  20549  ostth2lem3  20550  ostth2lem4  20551  ostth2  20552  ostth3  20553  ostth  20554  ex-dif  20557  ex-in  20559  ex-pss  20562  ex-res  20575  ex-fl  20581  nv1  21001  smcnlem  21029  ipidsq  21045  nmoub3i  21110  nmlno0lem  21130  blocnilem  21141  ipasslem10  21176  ubthlem2  21209  minvecolem4  21218  htthlem  21256  hisubcomi  21442  normlem9  21456  norm-ii-i  21475  bcs2  21520  norm1  21587  nmopub2tALT  22248  nmfnleub2  22265  nmlnop0iALT  22334  nmopun  22353  unopbd  22354  hmopd  22361  nmcexi  22365  nmopadjlem  22428  nmopcoi  22434  nmopcoadji  22440  opsqrlem4  22482  pjnmopi  22487  pjbdlni  22488  stcl  22555  stge0  22563  stle1  22564  hstle1  22565  hstle  22569  hstles  22570  stge1i  22577  stlesi  22580  staddi  22585  stadd3i  22587  strlem1  22589  strlem3a  22591  strlem5  22594  jplem1  22607  cdj1i  22772  addltmulALT  22785  zetacvg  22789  subfacp1lem1  22810  subfacp1lem5  22815  subfacval2  22818  subfaclim  22819  subfacval3  22820  cvxpcon  22873  cvxscon  22874  rescon  22877  iiscon  22883  iillyscon  22884  cvmliftlem2  22917  cvmliftlem8  22923  cvmliftlem13  22927  konigsberg  23011  snmlff  23012  sinccvglem  23105  divelunit  23179  dedekind  23181  relin01  23188  fznatpl1  23192  fz0n  23196  brbtwn2  23636  colinearalglem4  23640  ax5seglem1  23659  ax5seglem2  23660  ax5seglem3  23662  ax5seglem5  23664  ax5seglem6  23665  ax5seglem9  23668  ax5seg  23669  axbtwnid  23670  axpaschlem  23671  axpasch  23672  axlowdimlem3  23675  axlowdimlem6  23678  axlowdimlem7  23679  axlowdimlem10  23682  axlowdimlem16  23688  axlowdimlem17  23689  axlowdim1  23690  axlowdim2  23691  axlowdim  23692  axeuclidlem  23693  axcontlem2  23696  axcontlem4  23698  axcontlem7  23701  bpoly4  23897  cntrset  24697  fnckle  25140  nn0prpwlem  25333  fdc  25550  incsequz  25553  geomcau  25570  totbndbnd  25608  cntotbnd  25615  heiborlem8  25637  bfplem2  25642  bfp  25643  lzenom  25944  rabren3dioph  25993  irrapxlem1  26002  irrapxlem2  26003  irrapxlem4  26005  irrapxlem5  26006  pellexlem2  26010  pellexlem5  26013  pellexlem6  26014  pell1qrge1  26050  pell1qr1  26051  elpell1qr2  26052  pell1qrgaplem  26053  pell14qrgap  26055  pell14qrgapw  26056  pellqrex  26059  pellfundre  26061  pellfundgt1  26063  pellfundlb  26064  pellfundglb  26065  pellfundex  26066  pellfund14gap  26067  pellfundrp  26068  pellfundne1  26069  rmspecsqrnq  26086  rmspecnonsq  26087  rmspecfund  26089  rmspecpos  26096  monotoddzzfi  26122  jm2.17a  26142  rmygeid  26146  acongeq  26165  jm2.23  26184  jm3.1lem2  26206  matbas  26563  lhe4.4ex1a  26641  reseccl  26850  recsccl  26851  sgn1  26876
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 8672  ax-icn 8673  ax-addcl 8674  ax-mulcl 8676  ax-mulrcl 8677  ax-i2m1 8682  ax-1ne0 8683  ax-rrecex 8686  ax-cnre 8687
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 2511  df-rex 2512  df-rab 2514  df-v 2727  df-dif 3078  df-un 3080  df-in 3082  df-ss 3086  df-nul 3360  df-if 3468  df-sn 3547  df-pr 3548  df-op 3550  df-uni 3725  df-br 3918  df-opab 3972  df-xp 4591  df-cnv 4593  df-dm 4595  df-rn 4596  df-res 4597  df-ima 4598  df-fv 4605  df-ov 5710
  Copyright terms: Public domain W3C validator