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

Theorem 1re 8853
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 8811, 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
Dummy variables  a 
b  c  d  x  y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ax-1ne0 8822 . . 3  |-  1  =/=  0
2 ax-1cn 8811 . . . . 5  |-  1  e.  CC
3 cnre 8850 . . . . 5  |-  ( 1  e.  CC  ->  E. a  e.  RR  E. b  e.  RR  1  =  ( a  +  ( _i  x.  b ) ) )
42, 3ax-mp 8 . . . 4  |-  E. a  e.  RR  E. b  e.  RR  1  =  ( a  +  ( _i  x.  b ) )
5 neeq1 2467 . . . . . . . 8  |-  ( 1  =  ( a  +  ( _i  x.  b
) )  ->  (
1  =/=  0  <->  (
a  +  ( _i  x.  b ) )  =/=  0 ) )
65biimpcd 215 . . . . . . 7  |-  ( 1  =/=  0  ->  (
1  =  ( a  +  ( _i  x.  b ) )  -> 
( a  +  ( _i  x.  b ) )  =/=  0 ) )
7 0cn 8847 . . . . . . . 8  |-  0  e.  CC
8 cnre 8850 . . . . . . . 8  |-  ( 0  e.  CC  ->  E. c  e.  RR  E. d  e.  RR  0  =  ( c  +  ( _i  x.  d ) ) )
97, 8ax-mp 8 . . . . . . 7  |-  E. c  e.  RR  E. d  e.  RR  0  =  ( c  +  ( _i  x.  d ) )
10 neeq2 2468 . . . . . . . . . 10  |-  ( 0  =  ( c  +  ( _i  x.  d
) )  ->  (
( a  +  ( _i  x.  b ) )  =/=  0  <->  (
a  +  ( _i  x.  b ) )  =/=  ( c  +  ( _i  x.  d
) ) ) )
1110biimpcd 215 . . . . . . . . 9  |-  ( ( a  +  ( _i  x.  b ) )  =/=  0  ->  (
0  =  ( c  +  ( _i  x.  d ) )  -> 
( a  +  ( _i  x.  b ) )  =/=  ( c  +  ( _i  x.  d ) ) ) )
1211reximdv 2667 . . . . . . . 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 2667 . . . . . . 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 58 . . . . . 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 2667 . . . . 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 2667 . . . 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 16 . . 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 476 . . . . . . . . 9  |-  ( -.  ( a  =/=  c  \/  b  =/=  d
)  <->  ( -.  a  =/=  c  /\  -.  b  =/=  d ) )
19 df-ne 2461 . . . . . . . . . . 11  |-  ( a  =/=  c  <->  -.  a  =  c )
2019con2bii 322 . . . . . . . . . 10  |-  ( a  =  c  <->  -.  a  =/=  c )
21 df-ne 2461 . . . . . . . . . . 11  |-  ( b  =/=  d  <->  -.  b  =  d )
2221con2bii 322 . . . . . . . . . 10  |-  ( b  =  d  <->  -.  b  =/=  d )
2320, 22anbi12i 678 . . . . . . . . 9  |-  ( ( a  =  c  /\  b  =  d )  <->  ( -.  a  =/=  c  /\  -.  b  =/=  d
) )
2418, 23bitr4i 243 . . . . . . . 8  |-  ( -.  ( a  =/=  c  \/  b  =/=  d
)  <->  ( a  =  c  /\  b  =  d ) )
25 id 19 . . . . . . . . 9  |-  ( a  =  c  ->  a  =  c )
26 oveq2 5882 . . . . . . . . 9  |-  ( b  =  d  ->  (
_i  x.  b )  =  ( _i  x.  d ) )
2725, 26oveqan12d 5893 . . . . . . . 8  |-  ( ( a  =  c  /\  b  =  d )  ->  ( a  +  ( _i  x.  b ) )  =  ( c  +  ( _i  x.  d ) ) )
2824, 27sylbi 187 . . . . . . 7  |-  ( -.  ( a  =/=  c  \/  b  =/=  d
)  ->  ( a  +  ( _i  x.  b ) )  =  ( c  +  ( _i  x.  d ) ) )
2928necon1ai 2501 . . . . . 6  |-  ( ( a  +  ( _i  x.  b ) )  =/=  ( c  +  ( _i  x.  d
) )  ->  (
a  =/=  c  \/  b  =/=  d ) )
30 neeq1 2467 . . . . . . . . . 10  |-  ( x  =  a  ->  (
x  =/=  y  <->  a  =/=  y ) )
31 neeq2 2468 . . . . . . . . . 10  |-  ( y  =  c  ->  (
a  =/=  y  <->  a  =/=  c ) )
3230, 31rspc2ev 2905 . . . . . . . . 9  |-  ( ( a  e.  RR  /\  c  e.  RR  /\  a  =/=  c )  ->  E. x  e.  RR  E. y  e.  RR  x  =/=  y
)
33323expia 1153 . . . . . . . 8  |-  ( ( a  e.  RR  /\  c  e.  RR )  ->  ( a  =/=  c  ->  E. x  e.  RR  E. y  e.  RR  x  =/=  y ) )
3433ad2ant2r 727 . . . . . . 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 2467 . . . . . . . . . 10  |-  ( x  =  b  ->  (
x  =/=  y  <->  b  =/=  y ) )
36 neeq2 2468 . . . . . . . . . 10  |-  ( y  =  d  ->  (
b  =/=  y  <->  b  =/=  d ) )
3735, 36rspc2ev 2905 . . . . . . . . 9  |-  ( ( b  e.  RR  /\  d  e.  RR  /\  b  =/=  d )  ->  E. x  e.  RR  E. y  e.  RR  x  =/=  y
)
38373expia 1153 . . . . . . . 8  |-  ( ( b  e.  RR  /\  d  e.  RR )  ->  ( b  =/=  d  ->  E. x  e.  RR  E. y  e.  RR  x  =/=  y ) )
3938ad2ant2l 726 . . . . . . 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 369 . . . . . 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 28 . . . . 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 2687 . . . 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 2685 . . 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 9 . 2  |-  E. x  e.  RR  E. y  e.  RR  x  =/=  y
45 eqtr3 2315 . . . . . . . . 9  |-  ( ( x  =  0  /\  y  =  0 )  ->  x  =  y )
4645ex 423 . . . . . . . 8  |-  ( x  =  0  ->  (
y  =  0  ->  x  =  y )
)
4746necon3d 2497 . . . . . . 7  |-  ( x  =  0  ->  (
x  =/=  y  -> 
y  =/=  0 ) )
48 neeq1 2467 . . . . . . . . 9  |-  ( z  =  y  ->  (
z  =/=  0  <->  y  =/=  0 ) )
4948rspcev 2897 . . . . . . . 8  |-  ( ( y  e.  RR  /\  y  =/=  0 )  ->  E. z  e.  RR  z  =/=  0 )
5049expcom 424 . . . . . . 7  |-  ( y  =/=  0  ->  (
y  e.  RR  ->  E. z  e.  RR  z  =/=  0 ) )
5147, 50syl6 29 . . . . . 6  |-  ( x  =  0  ->  (
x  =/=  y  -> 
( y  e.  RR  ->  E. z  e.  RR  z  =/=  0 ) ) )
5251com23 72 . . . . 5  |-  ( x  =  0  ->  (
y  e.  RR  ->  ( x  =/=  y  ->  E. z  e.  RR  z  =/=  0 ) ) )
5352adantld 453 . . . 4  |-  ( x  =  0  ->  (
( x  e.  RR  /\  y  e.  RR )  ->  ( x  =/=  y  ->  E. z  e.  RR  z  =/=  0
) ) )
54 neeq1 2467 . . . . . . . 8  |-  ( z  =  x  ->  (
z  =/=  0  <->  x  =/=  0 ) )
5554rspcev 2897 . . . . . . 7  |-  ( ( x  e.  RR  /\  x  =/=  0 )  ->  E. z  e.  RR  z  =/=  0 )
5655expcom 424 . . . . . 6  |-  ( x  =/=  0  ->  (
x  e.  RR  ->  E. z  e.  RR  z  =/=  0 ) )
5756adantrd 454 . . . . 5  |-  ( x  =/=  0  ->  (
( x  e.  RR  /\  y  e.  RR )  ->  E. z  e.  RR  z  =/=  0 ) )
5857a1dd 42 . . . 4  |-  ( x  =/=  0  ->  (
( x  e.  RR  /\  y  e.  RR )  ->  ( x  =/=  y  ->  E. z  e.  RR  z  =/=  0
) ) )
5953, 58pm2.61ine 2535 . . 3  |-  ( ( x  e.  RR  /\  y  e.  RR )  ->  ( x  =/=  y  ->  E. z  e.  RR  z  =/=  0 ) )
6059rexlimivv 2685 . 2  |-  ( E. x  e.  RR  E. y  e.  RR  x  =/=  y  ->  E. z  e.  RR  z  =/=  0
)
61 ax-rrecex 8825 . . . 4  |-  ( ( z  e.  RR  /\  z  =/=  0 )  ->  E. x  e.  RR  ( z  x.  x
)  =  1 )
62 remulcl 8838 . . . . . . 7  |-  ( ( z  e.  RR  /\  x  e.  RR )  ->  ( z  x.  x
)  e.  RR )
6362adantlr 695 . . . . . 6  |-  ( ( ( z  e.  RR  /\  z  =/=  0 )  /\  x  e.  RR )  ->  ( z  x.  x )  e.  RR )
64 eleq1 2356 . . . . . 6  |-  ( ( z  x.  x )  =  1  ->  (
( z  x.  x
)  e.  RR  <->  1  e.  RR ) )
6563, 64syl5ibcom 211 . . . . 5  |-  ( ( ( z  e.  RR  /\  z  =/=  0 )  /\  x  e.  RR )  ->  ( ( z  x.  x )  =  1  ->  1  e.  RR ) )
6665rexlimdva 2680 . . . 4  |-  ( ( z  e.  RR  /\  z  =/=  0 )  -> 
( E. x  e.  RR  ( z  x.  x )  =  1  ->  1  e.  RR ) )
6761, 66mpd 14 . . 3  |-  ( ( z  e.  RR  /\  z  =/=  0 )  -> 
1  e.  RR )
6867rexlimiva 2675 . 2  |-  ( E. z  e.  RR  z  =/=  0  ->  1  e.  RR )
6944, 60, 68mp2b 9 1  |-  1  e.  RR
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    \/ wo 357    /\ wa 358    = wceq 1632    e. wcel 1696    =/= wne 2459   E.wrex 2557  (class class class)co 5874   CCcc 8751   RRcr 8752   0cc0 8753   1c1 8754   _ici 8755    + caddc 8756    x. cmul 8758
This theorem is referenced by:  0re  8854  peano2re  9001  mul02lem2  9005  addid1  9008  renegcl  9126  peano2rem  9129  0reALT  9159  0lt1  9312  0le1  9313  1le1  9412  eqneg  9496  ltp1  9610  ltm1  9612  recgt0  9616  mulgt1  9631  ltmulgt11  9632  lemulge11  9634  ltrec  9653  reclt1  9667  recgt1  9668  recgt1i  9669  recp1lt1  9670  recreclt  9671  recgt0ii  9678  ledivp1i  9698  ltdivp1i  9699  inelr  9752  cju  9758  nnssre  9766  nnge1  9788  nngt1ne1  9789  nnle1eq1  9790  nngt0  9791  nnnlt1  9792  nnrecre  9798  nnrecgt0  9799  nnsub  9800  2re  9831  3re  9833  4re  9835  5re  9837  6re  9838  7re  9839  8re  9840  9re  9841  10re  9842  2pos  9844  3pos  9846  4pos  9848  5pos  9849  6pos  9850  7pos  9851  8pos  9852  9pos  9853  10pos  9854  1lt2  9902  1lt3  9904  1lt4  9907  1lt5  9911  1lt6  9916  1lt7  9922  1lt8  9929  1lt9  9937  1lt10  9946  1ne2  9947  halflt1  9949  addltmul  9963  nnunb  9977  elnnnn0c  10025  elnnz1  10065  znnnlt1  10066  zltp1le  10083  zleltp1  10084  recnz  10103  gtndiv  10105  suprzcl  10107  uzindOLD  10122  eluzp1m1  10267  eluzp1p1  10269  eluz2b2  10306  zbtwnre  10330  rebtwnz  10331  1rp  10374  qbtwnre  10542  qbtwnxr  10543  xmulid1  10615  xmulid2  10616  xmulm1  10617  x2times  10635  xrub  10646  0elunit  10770  1elunit  10771  lincmb01cmp  10793  iccf1o  10794  xov1plusxeqvd  10796  unitssre  10797  fztpval  10861  fraclt1  10950  fracle1  10951  flbi2  10963  fladdz  10966  flhalf  10970  fldiv  10980  modid  11009  1mod  11012  seqf1olem1  11101  reexpcl  11136  reexpclz  11139  expge0  11154  expge1  11155  expgt1  11156  ltexp2a  11169  expcan  11170  ltexp2  11171  leexp2  11172  leexp2a  11173  leexp2r  11175  nnlesq  11222  bernneq  11243  bernneq2  11244  bernneq3  11245  expnbnd  11246  expnlbnd  11247  expnlbnd2  11248  expmulnbnd  11249  discr1  11253  facwordi  11318  faclbnd3  11321  faclbnd4lem1  11322  faclbnd4lem4  11325  faclbnd6  11328  facavg  11330  fzsdom2  11398  hashfun  11405  crre  11615  remim  11618  cjexp  11651  re1  11655  im1  11656  rei  11657  imi  11658  sqrlem1  11744  sqrlem2  11745  sqrlem3  11746  sqrlem4  11747  sqrlem7  11750  resqrex  11752  sqr1  11773  sqr2gt1lt2  11776  sqrm1  11777  abs1  11798  rddif  11840  absrdbnd  11841  caubnd2  11857  mulcn2  12085  reccn2  12086  rlimo1  12106  rlimno1  12143  iseraltlem2  12171  iseraltlem3  12172  iseralt  12173  o1fsum  12287  abscvgcvg  12293  climcndslem1  12324  climcndslem2  12325  flo1  12329  harmonic  12333  expcnv  12338  geolim  12342  geolim2  12343  georeclim  12344  geo2lim  12347  geomulcvg  12348  geoisumr  12350  geoisum1c  12352  geoihalfsum  12354  efcllem  12375  ere  12386  ege2le3  12387  efgt1  12412  resin4p  12434  recos4p  12435  tanhlt1  12456  tanhbnd  12457  sinbnd  12476  cosbnd  12477  sinbnd2  12478  cosbnd2  12479  ef01bndlem  12480  sin01bnd  12481  cos01bnd  12482  cos1bnd  12483  cos2bnd  12484  sinltx  12485  sin01gt0  12486  cos01gt0  12487  sin02gt0  12488  sincos1sgn  12489  eirrlem  12498  rpnnen2lem2  12510  rpnnen2lem3  12511  rpnnen2lem4  12512  rpnnen2lem9  12517  rpnnen2  12520  rpnnen  12521  ruclem6  12529  ruclem11  12534  ruclem12  12535  nthruz  12546  3dvds  12607  bitsfzolem  12641  bitsfzo  12642  bitsmod  12643  bitscmp  12645  bitsinv1lem  12648  sadcadd  12665  smuval2  12689  isprm3  12783  prmind2  12785  sqnprm  12793  coprm  12795  isprm5  12807  divdenle  12836  zsqrelqelz  12845  phibndlem  12854  fermltl  12868  odzdvds  12876  pythagtriplem3  12887  iserodd  12904  pcmpt  12956  fldivp1  12961  pcfaclem  12962  pockthi  12970  infpn2  12976  prmreclem1  12979  prmreclem5  12983  4sqlem11  13018  4sqlem12  13019  ramub1lem1  13089  2expltfac  13121  resslem  13217  rescbas  13722  rescabs  13726  odubas  14253  lt6abl  15197  pgpfaclem2  15333  abvneg  15615  abvtrivd  15621  xrsmcmn  16413  resubdrg  16439  gzrngunitlem  16452  gzrngunit  16453  znidomb  16531  thlbas  16612  leordtval2  16958  setsmsbas  18037  dscmet  18111  dscopn  18112  nrginvrcnlem  18217  nmoid  18267  idnghm  18268  tgioo  18318  blcvx  18320  xrsmopn  18334  metnrmlem1a  18378  metnrmlem1  18379  iitopon  18399  dfii2  18402  dfii3  18403  dfii5  18405  iicmp  18406  iicon  18407  iirev  18443  iirevcn  18444  iihalf1  18445  iihalf1cn  18446  iihalf2  18447  iihalf2cn  18448  elii1  18449  elii2  18450  iimulcl  18451  iimulcn  18452  icchmeo  18455  icopnfcnv  18456  icopnfhmeo  18457  iccpnfcnv  18458  iccpnfhmeo  18459  xrhmeo  18460  xrhmph  18461  icccvx  18464  evth  18473  xlebnum  18479  lebnumii  18480  htpycc  18494  reparphti  18511  pcoval1  18527  pco0  18528  pco1  18529  pcoval2  18530  pcocn  18531  pcohtpylem  18533  pcopt  18536  pcopt2  18537  pcoass  18538  pcorevlem  18540  pcorev2  18542  pi1xfrcnv  18571  nmhmcn  18617  cncmet  18760  ovolunlem1a  18871  ovoliunlem1  18877  dyadmaxlem  18968  vitalilem1  18979  vitalilem2  18980  vitalilem4  18982  vitalilem5  18983  vitali  18984  mbfneg  19021  i1f1  19061  itg11  19062  i1fsub  19079  itg1sub  19080  mbfi1fseqlem6  19091  itg2const  19111  itg2mulc  19118  itg2monolem1  19121  itg2monolem3  19123  iblcnlem1  19158  i1fibl  19178  itgitg1  19179  dveflem  19342  mvth  19355  dvlipcn  19357  lhop1lem  19376  dvcvx  19383  dvfsumlem1  19389  dvfsumlem2  19390  dvfsumlem3  19391  dvfsumlem4  19392  dvfsum2  19397  ply1remlem  19564  fta1glem2  19568  fta1blem  19570  plyeq0lem  19608  fta1lem  19703  vieta1lem2  19707  aalioulem3  19730  aalioulem4  19731  aalioulem5  19732  aaliou3lem2  19739  aaliou3lem8  19741  ulmbdd  19791  iblulm  19799  radcnvlem1  19805  radcnvlem2  19806  dvradcnv  19813  abelthlem2  19824  abelthlem3  19825  abelthlem5  19827  abelthlem7  19830  abelth  19833  abelth2  19834  reeff1olem  19838  reeff1o  19839  sinhalfpilem  19850  tangtx  19889  sincos4thpi  19897  pige3  19901  coskpi  19904  cosne0  19908  recosf1o  19913  tanregt0  19917  efif1olem3  19922  efif1olem4  19923  loge  19956  rplogcl  19974  logdivlti  19987  logno1  19999  logcnlem4  20008  logf1o2  20013  dvlog2lem  20015  advlog  20017  logtayllem  20022  logtayl  20023  logccv  20026  recxpcl  20038  cxplt  20057  cxple  20058  cxplea  20059  cxpsqrlem  20065  cxpsqr  20066  cxpcn3lem  20103  cxpaddlelem  20107  cxpaddle  20108  loglesqr  20114  ang180lem1  20123  ang180lem2  20124  ang180lem3  20125  isosctrlem1  20134  isosctrlem2  20135  angpined  20143  chordthmlem4  20148  1cubrlem  20153  atanre  20197  asinsin  20204  acosrecl  20215  atandmcj  20221  atancj  20222  atanlogaddlem  20225  atantan  20235  bndatandm  20241  atans2  20243  ressatans  20246  leibpilem2  20253  leibpi  20254  leibpisum  20255  log2tlbnd  20257  birthdaylem3  20264  birthday  20265  rlimcnp  20276  rlimcnp2  20277  efrlim  20280  cxp2limlem  20286  cxp2lim  20287  cxploglim  20288  cxploglim2  20289  divsqrsumlem  20290  divsqrsumo1  20294  cvxcl  20295  scvxcvx  20296  jensenlem2  20298  amgmlem  20300  emcllem2  20306  emcllem4  20308  emcllem6  20310  emcllem7  20311  emre  20315  emgt0  20316  harmonicbnd3  20317  harmonicubnd  20319  harmonicbnd4  20320  fsumharmonic  20321  wilthlem1  20322  wilthlem2  20323  ftalem1  20326  ftalem2  20327  ftalem5  20330  basellem3  20336  basellem9  20342  issqf  20390  cht1  20419  vma1  20420  chp1  20421  ppieq0  20430  ppiltx  20431  mumullem2  20434  fsumfldivdiaglem  20445  ppiublem1  20457  ppiub  20459  chpeq0  20463  chtublem  20466  chtub  20467  chpval2  20473  chpchtsum  20474  chpub  20475  logfacbnd3  20478  logfacrlim  20479  logexprlim  20480  mersenne  20482  perfectlem2  20485  dchrelbas4  20498  dchrinv  20516  dchr1re  20518  bcmono  20532  efexple  20536  bposlem1  20539  bposlem2  20540  bposlem5  20543  bposlem8  20546  lgslem3  20553  lgslem4  20554  lgsvalmod  20570  lgsmod  20576  lgsdir2lem1  20578  lgsdir2lem3  20580  lgsdir2lem4  20581  lgsdir2lem5  20582  lgsdirprm  20584  lgsdir  20585  lgsne0  20588  lgsabs1  20589  lgsdinn0  20595  lgseisen  20608  lgsquadlem2  20610  m1lgs  20617  2sqlem8  20627  chebbnd1lem1  20634  chebbnd1lem2  20635  chebbnd1lem3  20636  chebbnd1  20637  chtppilimlem1  20638  chtppilimlem2  20639  chtppilim  20640  chebbnd2  20642  chto1lb  20643  chpchtlim  20644  chpo1ubb  20646  vmadivsum  20647  vmadivsumb  20648  rplogsumlem1  20649  rplogsumlem2  20650  rpvmasumlem  20652  dchrisumlem3  20656  dchrmusumlema  20658  dchrmusum2  20659  dchrvmasumlem2  20663  dchrvmasumlem3  20664  dchrvmasumiflem1  20666  dchrvmasumiflem2  20667  dchrisum0flblem1  20673  dchrisum0flblem2  20674  dchrisum0fno1  20676  rpvmasum2  20677  dchrisum0re  20678  dchrisum0lema  20679  dchrisum0lem1b  20680  dchrisum0lem1  20681  dchrisum0lem2a  20682  dchrisum0lem2  20683  dchrisum0lem3  20684  rplogsum  20692  dirith2  20693  mudivsum  20695  mulogsumlem  20696  mulogsum  20697  logdivsum  20698  mulog2sumlem1  20699  mulog2sumlem2  20700  vmalogdivsum2  20703  2vmadivsumlem  20705  log2sumbnd  20709  selberglem2  20711  selbergb  20714  selberg2lem  20715  selberg2b  20717  chpdifbndlem1  20718  chpdifbnd  20720  selberg3lem1  20722  selberg3lem2  20723  selberg4lem1  20725  pntrmax  20729  pntrsumo1  20730  pntrsumbnd  20731  selberg34r  20736  selbergsb  20740  pntrlog2bndlem1  20742  pntrlog2bndlem2  20743  pntrlog2bndlem3  20744  pntrlog2bndlem4  20745  pntrlog2bndlem5  20746  pntrlog2bndlem6  20748  pntrlog2bnd  20749  pntpbnd1a  20750  pntpbnd1  20751  pntpbnd2  20752  pntibndlem1  20754  pntibndlem2a  20755  pntibndlem2  20756  pntibndlem3  20757  pntibnd  20758  pntlemd  20759  pntlemc  20760  pntlemb  20762  pntlemg  20763  pntlemr  20767  pntlemf  20770  pntlemk  20771  pntlemo  20772  pntlem3  20774  pntleml  20776  pnt  20779  abvcxp  20780  ostth2lem1  20783  qabvle  20790  padicabvf  20796  padicabvcxp  20797  ostth1  20798  ostth2lem2  20799  ostth2lem3  20800  ostth2lem4  20801  ostth2  20802  ostth3  20803  ostth  20804  ex-dif  20826  ex-in  20828  ex-pss  20831  ex-res  20844  ex-fl  20850  nv1  21258  smcnlem  21286  ipidsq  21302  nmoub3i  21367  nmlno0lem  21387  blocnilem  21398  ipasslem10  21433  ubthlem2  21466  minvecolem4  21475  htthlem  21513  hisubcomi  21699  normlem9  21713  norm-ii-i  21732  bcs2  21777  norm1  21844  nmopub2tALT  22505  nmfnleub2  22522  nmlnop0iALT  22591  nmopun  22610  unopbd  22611  hmopd  22618  nmcexi  22622  nmopadjlem  22685  nmopcoi  22691  nmopcoadji  22697  opsqrlem4  22739  pjnmopi  22744  pjbdlni  22745  stcl  22812  stge0  22820  stle1  22821  hstle1  22822  hstle  22826  hstles  22827  stge1i  22834  stlesi  22837  staddi  22842  stadd3i  22844  strlem1  22846  strlem3a  22848  strlem5  22851  jplem1  22864  cdj1i  23029  addltmulALT  23042  fzsplit3  23047  ballotlem2  23063  ballotlemfc0  23067  ballotlemfcc  23068  ballotlem4  23073  ballotlemi1  23077  ballotlemic  23081  ballotlem1c  23082  ballotlemsgt1  23085  ballotlemsel1i  23087  ballotlemfrcn0  23104  xdivrec  23126  cntnevol  23191  xlt2addrd  23268  unitsscn  23295  elunitrn  23296  elunitge0  23298  unitssxrge0  23299  unitdivcld  23300  sqsscirc1  23307  xrsmulgzz  23322  xrge0iifcnv  23330  xrge0iifcv  23331  xrge0iifiso  23332  xrge0iifhom  23334  hashge1  23403  rnlogblem  23416  log2le1  23424  esumcst  23451  esumdivc  23466  hasheuni  23468  dya2ub  23590  dya2iocress  23592  dya2iocbrsiga  23593  dya2iocseg  23594  indf  23614  indfval  23615  pr01ssre  23616  indf1o  23622  prob01  23631  probvalrnd  23642  probmeasb  23648  dstrvprob  23687  dstfrvunirn  23690  dstfrvclim1  23693  coinfliprv  23698  zetacvg  23704  subfacp1lem1  23725  subfacp1lem5  23730  subfacval2  23733  subfaclim  23734  subfacval3  23735  cvxpcon  23788  cvxscon  23789  rescon  23792  iiscon  23798  iillyscon  23799  cvmliftlem2  23832  cvmliftlem8  23838  cvmliftlem13  23842  konigsberg  23926  snmlff  23927  sinccvglem  24020  divelunit  24095  dedekind  24097  relin01  24104  fznatpl1  24108  fz0n  24112  faclimlem5  24121  faclimlem6  24122  faclimlem8  24124  faclimlem9  24125  brbtwn2  24604  colinearalglem4  24608  ax5seglem1  24627  ax5seglem2  24628  ax5seglem3  24630  ax5seglem5  24632  ax5seglem6  24633  ax5seglem9  24636  ax5seg  24637  axbtwnid  24638  axpaschlem  24639  axpasch  24640  axlowdimlem3  24643  axlowdimlem6  24646  axlowdimlem7  24647  axlowdimlem10  24650  axlowdimlem16  24656  axlowdimlem17  24657  axlowdim1  24658  axlowdim2  24659  axlowdim  24660  axeuclidlem  24661  axcontlem2  24664  axcontlem4  24666  axcontlem7  24669  bpoly4  24865  itg2addnclem2  25003  itg2addnc  25004  dvreasin  25025  dvreacos  25026  areacirclem2  25027  areacirclem5  25031  cntrset  25704  fnckle  26147  nn0prpwlem  26340  fdc  26557  incsequz  26560  geomcau  26577  totbndbnd  26615  cntotbnd  26622  heiborlem8  26644  bfplem2  26649  bfp  26650  lzenom  26951  rabren3dioph  27000  irrapxlem1  27009  irrapxlem2  27010  irrapxlem4  27012  irrapxlem5  27013  pellexlem2  27017  pellexlem5  27020  pellexlem6  27021  pell1qrge1  27057  pell1qr1  27058  elpell1qr2  27059  pell1qrgaplem  27060  pell14qrgap  27062  pell14qrgapw  27063  pellqrex  27066  pellfundre  27068  pellfundgt1  27070  pellfundlb  27071  pellfundglb  27072  pellfundex  27073  pellfund14gap  27074  pellfundrp  27075  pellfundne1  27076  rmspecsqrnq  27093  rmspecnonsq  27094  rmspecfund  27096  rmspecpos  27103  monotoddzzfi  27129  jm2.17a  27149  rmygeid  27153  acongeq  27172  jm2.23  27191  jm3.1lem2  27213  matbas  27570  lhe4.4ex1a  27648  fmul01  27812  fmuldfeq  27815  fmul01lt1lem1  27816  fmul01lt1lem2  27817  climsuselem1  27835  stoweidlem1  27852  stoweidlem3  27854  stoweidlem5  27856  stoweidlem7  27858  stoweidlem10  27861  stoweidlem11  27862  stoweidlem12  27863  stoweidlem13  27864  stoweidlem14  27865  stoweidlem16  27867  stoweidlem18  27869  stoweidlem19  27870  stoweidlem20  27871  stoweidlem22  27873  stoweidlem24  27875  stoweidlem25  27876  stoweidlem26  27877  stoweidlem28  27879  stoweidlem30  27881  stoweidlem34  27885  stoweidlem36  27887  stoweidlem38  27889  stoweidlem40  27891  stoweidlem41  27892  stoweidlem42  27893  stoweidlem44  27895  stoweidlem45  27896  stoweidlem51  27902  stoweidlem59  27910  stoweidlem60  27911  stoweidlem62  27913  stoweid  27914  wallispilem3  27918  wallispilem4  27919  wallispilem5  27920  wallispi  27921  wallispi2lem1  27922  wallispi2lem2  27923  wallispi2  27924  stirlinglem1  27925  stirlinglem3  27927  stirlinglem5  27929  stirlinglem6  27930  stirlinglem7  27931  stirlinglem8  27932  stirlinglem10  27934  stirlinglem11  27935  stirlinglem12  27936  stirlinglem13  27937  stirlinglem15  27939  sigaradd  27958  f1oun2prg  28186  elfznelfzo  28212  hashgt12el  28217  hashgt12el2  28218  4fvwrd4  28219  usgraexmpldifpr  28265  spthispth  28358  constr3lem4  28392  constr3pthlem1  28400  constr3pthlem3  28402  reseccl  28476  recsccl  28477  sgn1  28502  ene1  28511
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-1cn 8811  ax-icn 8812  ax-addcl 8813  ax-mulcl 8815  ax-mulrcl 8816  ax-i2m1 8821  ax-1ne0 8822  ax-rrecex 8825  ax-cnre 8826
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-ral 2561  df-rex 2562  df-rab 2565  df-v 2803  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-sn 3659  df-pr 3660  df-op 3662  df-uni 3844  df-br 4040  df-iota 5235  df-fv 5279  df-ov 5877
  Copyright terms: Public domain W3C validator