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

Theorem 1re 8837
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 8795, 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 8806 . . 3  |-  1  =/=  0
2 ax-1cn 8795 . . . . 5  |-  1  e.  CC
3 cnre 8834 . . . . 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 2454 . . . . . . . 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 8831 . . . . . . . 8  |-  0  e.  CC
8 cnre 8834 . . . . . . . 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 2455 . . . . . . . . . 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 2654 . . . . . . . 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 2654 . . . . . . 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 2654 . . . . 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 2654 . . . 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 2448 . . . . . . . . . . 11  |-  ( a  =/=  c  <->  -.  a  =  c )
2019con2bii 322 . . . . . . . . . 10  |-  ( a  =  c  <->  -.  a  =/=  c )
21 df-ne 2448 . . . . . . . . . . 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 5866 . . . . . . . . 9  |-  ( b  =  d  ->  (
_i  x.  b )  =  ( _i  x.  d ) )
2725, 26oveqan12d 5877 . . . . . . . 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 2488 . . . . . 6  |-  ( ( a  +  ( _i  x.  b ) )  =/=  ( c  +  ( _i  x.  d
) )  ->  (
a  =/=  c  \/  b  =/=  d ) )
30 neeq1 2454 . . . . . . . . . 10  |-  ( x  =  a  ->  (
x  =/=  y  <->  a  =/=  y ) )
31 neeq2 2455 . . . . . . . . . 10  |-  ( y  =  c  ->  (
a  =/=  y  <->  a  =/=  c ) )
3230, 31rspc2ev 2892 . . . . . . . . 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 2454 . . . . . . . . . 10  |-  ( x  =  b  ->  (
x  =/=  y  <->  b  =/=  y ) )
36 neeq2 2455 . . . . . . . . . 10  |-  ( y  =  d  ->  (
b  =/=  y  <->  b  =/=  d ) )
3735, 36rspc2ev 2892 . . . . . . . . 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 2674 . . . 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 2672 . . 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 2302 . . . . . . . . 9  |-  ( ( x  =  0  /\  y  =  0 )  ->  x  =  y )
4645ex 423 . . . . . . . 8  |-  ( x  =  0  ->  (
y  =  0  ->  x  =  y )
)
4746necon3d 2484 . . . . . . 7  |-  ( x  =  0  ->  (
x  =/=  y  -> 
y  =/=  0 ) )
48 neeq1 2454 . . . . . . . . 9  |-  ( z  =  y  ->  (
z  =/=  0  <->  y  =/=  0 ) )
4948rspcev 2884 . . . . . . . 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 2454 . . . . . . . 8  |-  ( z  =  x  ->  (
z  =/=  0  <->  x  =/=  0 ) )
5554rspcev 2884 . . . . . . 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 2522 . . 3  |-  ( ( x  e.  RR  /\  y  e.  RR )  ->  ( x  =/=  y  ->  E. z  e.  RR  z  =/=  0 ) )
6059rexlimivv 2672 . 2  |-  ( E. x  e.  RR  E. y  e.  RR  x  =/=  y  ->  E. z  e.  RR  z  =/=  0
)
61 ax-rrecex 8809 . . . 4  |-  ( ( z  e.  RR  /\  z  =/=  0 )  ->  E. x  e.  RR  ( z  x.  x
)  =  1 )
62 remulcl 8822 . . . . . . 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 2343 . . . . . 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 2667 . . . 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 2662 . 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 1623    e. wcel 1684    =/= wne 2446   E.wrex 2544  (class class class)co 5858   CCcc 8735   RRcr 8736   0cc0 8737   1c1 8738   _ici 8739    + caddc 8740    x. cmul 8742
This theorem is referenced by:  0re  8838  peano2re  8985  mul02lem2  8989  addid1  8992  renegcl  9110  peano2rem  9113  0reALT  9143  0lt1  9296  0le1  9297  1le1  9396  eqneg  9480  ltp1  9594  ltm1  9596  recgt0  9600  mulgt1  9615  ltmulgt11  9616  lemulge11  9618  ltrec  9637  reclt1  9651  recgt1  9652  recgt1i  9653  recp1lt1  9654  recreclt  9655  recgt0ii  9662  ledivp1i  9682  ltdivp1i  9683  inelr  9736  cju  9742  nnssre  9750  nnge1  9772  nngt1ne1  9773  nnle1eq1  9774  nngt0  9775  nnnlt1  9776  nnrecre  9782  nnrecgt0  9783  nnsub  9784  2re  9815  3re  9817  4re  9819  5re  9821  6re  9822  7re  9823  8re  9824  9re  9825  10re  9826  2pos  9828  3pos  9830  4pos  9832  5pos  9833  6pos  9834  7pos  9835  8pos  9836  9pos  9837  10pos  9838  1lt2  9886  1lt3  9888  1lt4  9891  1lt5  9895  1lt6  9900  1lt7  9906  1lt8  9913  1lt9  9921  1lt10  9930  1ne2  9931  halflt1  9933  addltmul  9947  nnunb  9961  elnnnn0c  10009  elnnz1  10049  znnnlt1  10050  zltp1le  10067  zleltp1  10068  recnz  10087  gtndiv  10089  suprzcl  10091  uzindOLD  10106  eluzp1m1  10251  eluzp1p1  10253  eluz2b2  10290  zbtwnre  10314  rebtwnz  10315  1rp  10358  qbtwnre  10526  qbtwnxr  10527  xmulid1  10599  xmulid2  10600  xmulm1  10601  x2times  10619  xrub  10630  0elunit  10754  1elunit  10755  lincmb01cmp  10777  iccf1o  10778  xov1plusxeqvd  10780  unitssre  10781  fztpval  10845  fraclt1  10934  fracle1  10935  flbi2  10947  fladdz  10950  flhalf  10954  fldiv  10964  modid  10993  1mod  10996  seqf1olem1  11085  reexpcl  11120  reexpclz  11123  expge0  11138  expge1  11139  expgt1  11140  ltexp2a  11153  expcan  11154  ltexp2  11155  leexp2  11156  leexp2a  11157  leexp2r  11159  nnlesq  11206  bernneq  11227  bernneq2  11228  bernneq3  11229  expnbnd  11230  expnlbnd  11231  expnlbnd2  11232  expmulnbnd  11233  discr1  11237  facwordi  11302  faclbnd3  11305  faclbnd4lem1  11306  faclbnd4lem4  11309  faclbnd6  11312  facavg  11314  fzsdom2  11382  hashfun  11389  crre  11599  remim  11602  cjexp  11635  re1  11639  im1  11640  rei  11641  imi  11642  sqrlem1  11728  sqrlem2  11729  sqrlem3  11730  sqrlem4  11731  sqrlem7  11734  resqrex  11736  sqr1  11757  sqr2gt1lt2  11760  sqrm1  11761  abs1  11782  rddif  11824  absrdbnd  11825  caubnd2  11841  mulcn2  12069  reccn2  12070  rlimo1  12090  rlimno1  12127  iseraltlem2  12155  iseraltlem3  12156  iseralt  12157  o1fsum  12271  abscvgcvg  12277  climcndslem1  12308  climcndslem2  12309  flo1  12313  harmonic  12317  expcnv  12322  geolim  12326  geolim2  12327  georeclim  12328  geo2lim  12331  geomulcvg  12332  geoisumr  12334  geoisum1c  12336  geoihalfsum  12338  efcllem  12359  ere  12370  ege2le3  12371  efgt1  12396  resin4p  12418  recos4p  12419  tanhlt1  12440  tanhbnd  12441  sinbnd  12460  cosbnd  12461  sinbnd2  12462  cosbnd2  12463  ef01bndlem  12464  sin01bnd  12465  cos01bnd  12466  cos1bnd  12467  cos2bnd  12468  sinltx  12469  sin01gt0  12470  cos01gt0  12471  sin02gt0  12472  sincos1sgn  12473  eirrlem  12482  rpnnen2lem2  12494  rpnnen2lem3  12495  rpnnen2lem4  12496  rpnnen2lem9  12501  rpnnen2  12504  rpnnen  12505  ruclem6  12513  ruclem11  12518  ruclem12  12519  nthruz  12530  3dvds  12591  bitsfzolem  12625  bitsfzo  12626  bitsmod  12627  bitscmp  12629  bitsinv1lem  12632  sadcadd  12649  smuval2  12673  isprm3  12767  prmind2  12769  sqnprm  12777  coprm  12779  isprm5  12791  divdenle  12820  zsqrelqelz  12829  phibndlem  12838  fermltl  12852  odzdvds  12860  pythagtriplem3  12871  iserodd  12888  pcmpt  12940  fldivp1  12945  pcfaclem  12946  pockthi  12954  infpn2  12960  prmreclem1  12963  prmreclem5  12967  4sqlem11  13002  4sqlem12  13003  ramub1lem1  13073  2expltfac  13105  resslem  13201  rescbas  13706  rescabs  13710  odubas  14237  lt6abl  15181  pgpfaclem2  15317  abvneg  15599  abvtrivd  15605  xrsmcmn  16397  resubdrg  16423  gzrngunitlem  16436  gzrngunit  16437  znidomb  16515  thlbas  16596  leordtval2  16942  setsmsbas  18021  dscmet  18095  dscopn  18096  nrginvrcnlem  18201  nmoid  18251  idnghm  18252  tgioo  18302  blcvx  18304  xrsmopn  18318  metnrmlem1a  18362  metnrmlem1  18363  iitopon  18383  dfii2  18386  dfii3  18387  dfii5  18389  iicmp  18390  iicon  18391  iirev  18427  iirevcn  18428  iihalf1  18429  iihalf1cn  18430  iihalf2  18431  iihalf2cn  18432  elii1  18433  elii2  18434  iimulcl  18435  iimulcn  18436  icchmeo  18439  icopnfcnv  18440  icopnfhmeo  18441  iccpnfcnv  18442  iccpnfhmeo  18443  xrhmeo  18444  xrhmph  18445  icccvx  18448  evth  18457  xlebnum  18463  lebnumii  18464  htpycc  18478  reparphti  18495  pcoval1  18511  pco0  18512  pco1  18513  pcoval2  18514  pcocn  18515  pcohtpylem  18517  pcopt  18520  pcopt2  18521  pcoass  18522  pcorevlem  18524  pcorev2  18526  pi1xfrcnv  18555  nmhmcn  18601  cncmet  18744  ovolunlem1a  18855  ovoliunlem1  18861  dyadmaxlem  18952  vitalilem1  18963  vitalilem2  18964  vitalilem4  18966  vitalilem5  18967  vitali  18968  mbfneg  19005  i1f1  19045  itg11  19046  i1fsub  19063  itg1sub  19064  mbfi1fseqlem6  19075  itg2const  19095  itg2mulc  19102  itg2monolem1  19105  itg2monolem3  19107  iblcnlem1  19142  i1fibl  19162  itgitg1  19163  dveflem  19326  mvth  19339  dvlipcn  19341  lhop1lem  19360  dvcvx  19367  dvfsumlem1  19373  dvfsumlem2  19374  dvfsumlem3  19375  dvfsumlem4  19376  dvfsum2  19381  ply1remlem  19548  fta1glem2  19552  fta1blem  19554  plyeq0lem  19592  fta1lem  19687  vieta1lem2  19691  aalioulem3  19714  aalioulem4  19715  aalioulem5  19716  aaliou3lem2  19723  aaliou3lem8  19725  ulmbdd  19775  iblulm  19783  radcnvlem1  19789  radcnvlem2  19790  dvradcnv  19797  abelthlem2  19808  abelthlem3  19809  abelthlem5  19811  abelthlem7  19814  abelth  19817  abelth2  19818  reeff1olem  19822  reeff1o  19823  sinhalfpilem  19834  tangtx  19873  sincos4thpi  19881  pige3  19885  coskpi  19888  cosne0  19892  recosf1o  19897  tanregt0  19901  efif1olem3  19906  efif1olem4  19907  loge  19940  rplogcl  19958  logdivlti  19971  logno1  19983  logcnlem4  19992  logf1o2  19997  dvlog2lem  19999  advlog  20001  logtayllem  20006  logtayl  20007  logccv  20010  recxpcl  20022  cxplt  20041  cxple  20042  cxplea  20043  cxpsqrlem  20049  cxpsqr  20050  cxpcn3lem  20087  cxpaddlelem  20091  cxpaddle  20092  loglesqr  20098  ang180lem1  20107  ang180lem2  20108  ang180lem3  20109  isosctrlem1  20118  isosctrlem2  20119  angpined  20127  chordthmlem4  20132  1cubrlem  20137  atanre  20181  asinsin  20188  acosrecl  20199  atandmcj  20205  atancj  20206  atanlogaddlem  20209  atantan  20219  bndatandm  20225  atans2  20227  ressatans  20230  leibpilem2  20237  leibpi  20238  leibpisum  20239  log2tlbnd  20241  birthdaylem3  20248  birthday  20249  rlimcnp  20260  rlimcnp2  20261  efrlim  20264  cxp2limlem  20270  cxp2lim  20271  cxploglim  20272  cxploglim2  20273  divsqrsumlem  20274  divsqrsumo1  20278  cvxcl  20279  scvxcvx  20280  jensenlem2  20282  amgmlem  20284  emcllem2  20290  emcllem4  20292  emcllem6  20294  emcllem7  20295  emre  20299  emgt0  20300  harmonicbnd3  20301  harmonicubnd  20303  harmonicbnd4  20304  fsumharmonic  20305  wilthlem1  20306  wilthlem2  20307  ftalem1  20310  ftalem2  20311  ftalem5  20314  basellem3  20320  basellem9  20326  issqf  20374  cht1  20403  vma1  20404  chp1  20405  ppieq0  20414  ppiltx  20415  mumullem2  20418  fsumfldivdiaglem  20429  ppiublem1  20441  ppiub  20443  chpeq0  20447  chtublem  20450  chtub  20451  chpval2  20457  chpchtsum  20458  chpub  20459  logfacbnd3  20462  logfacrlim  20463  logexprlim  20464  mersenne  20466  perfectlem2  20469  dchrelbas4  20482  dchrinv  20500  dchr1re  20502  bcmono  20516  efexple  20520  bposlem1  20523  bposlem2  20524  bposlem5  20527  bposlem8  20530  lgslem3  20537  lgslem4  20538  lgsvalmod  20554  lgsmod  20560  lgsdir2lem1  20562  lgsdir2lem3  20564  lgsdir2lem4  20565  lgsdir2lem5  20566  lgsdirprm  20568  lgsdir  20569  lgsne0  20572  lgsabs1  20573  lgsdinn0  20579  lgseisen  20592  lgsquadlem2  20594  m1lgs  20601  2sqlem8  20611  chebbnd1lem1  20618  chebbnd1lem2  20619  chebbnd1lem3  20620  chebbnd1  20621  chtppilimlem1  20622  chtppilimlem2  20623  chtppilim  20624  chebbnd2  20626  chto1lb  20627  chpchtlim  20628  chpo1ubb  20630  vmadivsum  20631  vmadivsumb  20632  rplogsumlem1  20633  rplogsumlem2  20634  rpvmasumlem  20636  dchrisumlem3  20640  dchrmusumlema  20642  dchrmusum2  20643  dchrvmasumlem2  20647  dchrvmasumlem3  20648  dchrvmasumiflem1  20650  dchrvmasumiflem2  20651  dchrisum0flblem1  20657  dchrisum0flblem2  20658  dchrisum0fno1  20660  rpvmasum2  20661  dchrisum0re  20662  dchrisum0lema  20663  dchrisum0lem1b  20664  dchrisum0lem1  20665  dchrisum0lem2a  20666  dchrisum0lem2  20667  dchrisum0lem3  20668  rplogsum  20676  dirith2  20677  mudivsum  20679  mulogsumlem  20680  mulogsum  20681  logdivsum  20682  mulog2sumlem1  20683  mulog2sumlem2  20684  vmalogdivsum2  20687  2vmadivsumlem  20689  log2sumbnd  20693  selberglem2  20695  selbergb  20698  selberg2lem  20699  selberg2b  20701  chpdifbndlem1  20702  chpdifbnd  20704  selberg3lem1  20706  selberg3lem2  20707  selberg4lem1  20709  pntrmax  20713  pntrsumo1  20714  pntrsumbnd  20715  selberg34r  20720  selbergsb  20724  pntrlog2bndlem1  20726  pntrlog2bndlem2  20727  pntrlog2bndlem3  20728  pntrlog2bndlem4  20729  pntrlog2bndlem5  20730  pntrlog2bndlem6  20732  pntrlog2bnd  20733  pntpbnd1a  20734  pntpbnd1  20735  pntpbnd2  20736  pntibndlem1  20738  pntibndlem2a  20739  pntibndlem2  20740  pntibndlem3  20741  pntibnd  20742  pntlemd  20743  pntlemc  20744  pntlemb  20746  pntlemg  20747  pntlemr  20751  pntlemf  20754  pntlemk  20755  pntlemo  20756  pntlem3  20758  pntleml  20760  pnt  20763  abvcxp  20764  ostth2lem1  20767  qabvle  20774  padicabvf  20780  padicabvcxp  20781  ostth1  20782  ostth2lem2  20783  ostth2lem3  20784  ostth2lem4  20785  ostth2  20786  ostth3  20787  ostth  20788  ex-dif  20810  ex-in  20812  ex-pss  20815  ex-res  20828  ex-fl  20834  nv1  21242  smcnlem  21270  ipidsq  21286  nmoub3i  21351  nmlno0lem  21371  blocnilem  21382  ipasslem10  21417  ubthlem2  21450  minvecolem4  21459  htthlem  21497  hisubcomi  21683  normlem9  21697  norm-ii-i  21716  bcs2  21761  norm1  21828  nmopub2tALT  22489  nmfnleub2  22506  nmlnop0iALT  22575  nmopun  22594  unopbd  22595  hmopd  22602  nmcexi  22606  nmopadjlem  22669  nmopcoi  22675  nmopcoadji  22681  opsqrlem4  22723  pjnmopi  22728  pjbdlni  22729  stcl  22796  stge0  22804  stle1  22805  hstle1  22806  hstle  22810  hstles  22811  stge1i  22818  stlesi  22821  staddi  22826  stadd3i  22828  strlem1  22830  strlem3a  22832  strlem5  22835  jplem1  22848  cdj1i  23013  addltmulALT  23026  fzsplit3  23031  ballotlem2  23047  ballotlemfc0  23051  ballotlemfcc  23052  ballotlem4  23057  ballotlemi1  23061  ballotlemic  23065  ballotlem1c  23066  ballotlemsgt1  23069  ballotlemsel1i  23071  ballotlemfrcn0  23088  xdivrec  23110  cntnevol  23175  xlt2addrd  23253  unitsscn  23280  elunitrn  23281  elunitge0  23283  unitssxrge0  23284  unitdivcld  23285  sqsscirc1  23292  xrsmulgzz  23307  xrge0iifcnv  23315  xrge0iifcv  23316  xrge0iifiso  23317  xrge0iifhom  23319  hashge1  23388  rnlogblem  23401  log2le1  23409  esumcst  23436  esumdivc  23451  hasheuni  23453  dya2ub  23575  dya2iocress  23577  dya2iocbrsiga  23578  dya2iocseg  23579  indf  23599  indfval  23600  pr01ssre  23601  indf1o  23607  prob01  23616  probvalrnd  23627  probmeasb  23633  dstrvprob  23672  dstfrvunirn  23675  dstfrvclim1  23678  coinfliprv  23683  zetacvg  23689  subfacp1lem1  23710  subfacp1lem5  23715  subfacval2  23718  subfaclim  23719  subfacval3  23720  cvxpcon  23773  cvxscon  23774  rescon  23777  iiscon  23783  iillyscon  23784  cvmliftlem2  23817  cvmliftlem8  23823  cvmliftlem13  23827  konigsberg  23911  snmlff  23912  sinccvglem  24005  divelunit  24080  dedekind  24082  relin01  24089  fznatpl1  24093  fz0n  24097  brbtwn2  24533  colinearalglem4  24537  ax5seglem1  24556  ax5seglem2  24557  ax5seglem3  24559  ax5seglem5  24561  ax5seglem6  24562  ax5seglem9  24565  ax5seg  24566  axbtwnid  24567  axpaschlem  24568  axpasch  24569  axlowdimlem3  24572  axlowdimlem6  24575  axlowdimlem7  24576  axlowdimlem10  24579  axlowdimlem16  24585  axlowdimlem17  24586  axlowdim1  24587  axlowdim2  24588  axlowdim  24589  axeuclidlem  24590  axcontlem2  24593  axcontlem4  24595  axcontlem7  24598  bpoly4  24794  dvreasin  24923  dvreacos  24924  areacirclem2  24925  areacirclem5  24929  cntrset  25602  fnckle  26045  nn0prpwlem  26238  fdc  26455  incsequz  26458  geomcau  26475  totbndbnd  26513  cntotbnd  26520  heiborlem8  26542  bfplem2  26547  bfp  26548  lzenom  26849  rabren3dioph  26898  irrapxlem1  26907  irrapxlem2  26908  irrapxlem4  26910  irrapxlem5  26911  pellexlem2  26915  pellexlem5  26918  pellexlem6  26919  pell1qrge1  26955  pell1qr1  26956  elpell1qr2  26957  pell1qrgaplem  26958  pell14qrgap  26960  pell14qrgapw  26961  pellqrex  26964  pellfundre  26966  pellfundgt1  26968  pellfundlb  26969  pellfundglb  26970  pellfundex  26971  pellfund14gap  26972  pellfundrp  26973  pellfundne1  26974  rmspecsqrnq  26991  rmspecnonsq  26992  rmspecfund  26994  rmspecpos  27001  monotoddzzfi  27027  jm2.17a  27047  rmygeid  27051  acongeq  27070  jm2.23  27089  jm3.1lem2  27111  matbas  27468  lhe4.4ex1a  27546  fmul01  27710  fmuldfeq  27713  fmul01lt1lem1  27714  fmul01lt1lem2  27715  climsuselem1  27733  stoweidlem1  27750  stoweidlem3  27752  stoweidlem5  27754  stoweidlem7  27756  stoweidlem10  27759  stoweidlem11  27760  stoweidlem12  27761  stoweidlem13  27762  stoweidlem14  27763  stoweidlem16  27765  stoweidlem18  27767  stoweidlem19  27768  stoweidlem20  27769  stoweidlem22  27771  stoweidlem24  27773  stoweidlem25  27774  stoweidlem26  27775  stoweidlem28  27777  stoweidlem30  27779  stoweidlem34  27783  stoweidlem36  27785  stoweidlem38  27787  stoweidlem40  27789  stoweidlem41  27790  stoweidlem42  27791  stoweidlem44  27793  stoweidlem45  27794  stoweidlem51  27800  stoweidlem59  27808  stoweidlem60  27809  stoweidlem62  27811  stoweid  27812  wallispilem3  27816  wallispilem4  27817  wallispilem5  27818  wallispi  27819  wallispi2lem1  27820  wallispi2lem2  27821  wallispi2  27822  stirlinglem1  27823  stirlinglem3  27825  stirlinglem5  27827  stirlinglem6  27828  stirlinglem7  27829  stirlinglem8  27830  stirlinglem10  27832  stirlinglem11  27833  stirlinglem12  27834  stirlinglem13  27835  stirlinglem15  27837  sigaradd  27856  f1oun2prg  28076  usgraexmpldifpr  28132  reseccl  28223  recsccl  28224  sgn1  28249
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-1cn 8795  ax-icn 8796  ax-addcl 8797  ax-mulcl 8799  ax-mulrcl 8800  ax-i2m1 8805  ax-1ne0 8806  ax-rrecex 8809  ax-cnre 8810
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-br 4024  df-iota 5219  df-fv 5263  df-ov 5861
  Copyright terms: Public domain W3C validator