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

Theorem 1re 9091
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 9049, 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 9060 . . 3  |-  1  =/=  0
2 ax-1cn 9049 . . . . 5  |-  1  e.  CC
3 cnre 9088 . . . . 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 2610 . . . . . . . 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 9085 . . . . . . . 8  |-  0  e.  CC
8 cnre 9088 . . . . . . . 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 2611 . . . . . . . . . 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 2818 . . . . . . . 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 2818 . . . . . . 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 61 . . . . . 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 2818 . . . . 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 2818 . . . 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 17 . . 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 2602 . . . . . . . . . . 11  |-  ( a  =/=  c  <->  -.  a  =  c )
2019con2bii 324 . . . . . . . . . 10  |-  ( a  =  c  <->  -.  a  =/=  c )
21 df-ne 2602 . . . . . . . . . . 11  |-  ( b  =/=  d  <->  -.  b  =  d )
2221con2bii 324 . . . . . . . . . 10  |-  ( b  =  d  <->  -.  b  =/=  d )
2320, 22anbi12i 680 . . . . . . . . 9  |-  ( ( a  =  c  /\  b  =  d )  <->  ( -.  a  =/=  c  /\  -.  b  =/=  d
) )
2418, 23bitr4i 245 . . . . . . . 8  |-  ( -.  ( a  =/=  c  \/  b  =/=  d
)  <->  ( a  =  c  /\  b  =  d ) )
25 id 21 . . . . . . . . 9  |-  ( a  =  c  ->  a  =  c )
26 oveq2 6090 . . . . . . . . 9  |-  ( b  =  d  ->  (
_i  x.  b )  =  ( _i  x.  d ) )
2725, 26oveqan12d 6101 . . . . . . . 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 2647 . . . . . 6  |-  ( ( a  +  ( _i  x.  b ) )  =/=  ( c  +  ( _i  x.  d
) )  ->  (
a  =/=  c  \/  b  =/=  d ) )
30 neeq1 2610 . . . . . . . . . 10  |-  ( x  =  a  ->  (
x  =/=  y  <->  a  =/=  y ) )
31 neeq2 2611 . . . . . . . . . 10  |-  ( y  =  c  ->  (
a  =/=  y  <->  a  =/=  c ) )
3230, 31rspc2ev 3061 . . . . . . . . 9  |-  ( ( a  e.  RR  /\  c  e.  RR  /\  a  =/=  c )  ->  E. x  e.  RR  E. y  e.  RR  x  =/=  y
)
33323expia 1156 . . . . . . . 8  |-  ( ( a  e.  RR  /\  c  e.  RR )  ->  ( a  =/=  c  ->  E. x  e.  RR  E. y  e.  RR  x  =/=  y ) )
3433ad2ant2r 729 . . . . . . 7  |-  ( ( ( a  e.  RR  /\  b  e.  RR )  /\  ( c  e.  RR  /\  d  e.  RR ) )  -> 
( a  =/=  c  ->  E. x  e.  RR  E. y  e.  RR  x  =/=  y ) )
35 neeq1 2610 . . . . . . . . . 10  |-  ( x  =  b  ->  (
x  =/=  y  <->  b  =/=  y ) )
36 neeq2 2611 . . . . . . . . . 10  |-  ( y  =  d  ->  (
b  =/=  y  <->  b  =/=  d ) )
3735, 36rspc2ev 3061 . . . . . . . . 9  |-  ( ( b  e.  RR  /\  d  e.  RR  /\  b  =/=  d )  ->  E. x  e.  RR  E. y  e.  RR  x  =/=  y
)
38373expia 1156 . . . . . . . 8  |-  ( ( b  e.  RR  /\  d  e.  RR )  ->  ( b  =/=  d  ->  E. x  e.  RR  E. y  e.  RR  x  =/=  y ) )
3938ad2ant2l 728 . . . . . . 7  |-  ( ( ( a  e.  RR  /\  b  e.  RR )  /\  ( c  e.  RR  /\  d  e.  RR ) )  -> 
( b  =/=  d  ->  E. x  e.  RR  E. y  e.  RR  x  =/=  y ) )
4034, 39jaod 371 . . . . . 6  |-  ( ( ( a  e.  RR  /\  b  e.  RR )  /\  ( c  e.  RR  /\  d  e.  RR ) )  -> 
( ( a  =/=  c  \/  b  =/=  d )  ->  E. x  e.  RR  E. y  e.  RR  x  =/=  y
) )
4129, 40syl5 31 . . . . 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 2838 . . . 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 2836 . . 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 10 . 2  |-  E. x  e.  RR  E. y  e.  RR  x  =/=  y
45 eqtr3 2456 . . . . . . . . 9  |-  ( ( x  =  0  /\  y  =  0 )  ->  x  =  y )
4645ex 425 . . . . . . . 8  |-  ( x  =  0  ->  (
y  =  0  ->  x  =  y )
)
4746necon3d 2640 . . . . . . 7  |-  ( x  =  0  ->  (
x  =/=  y  -> 
y  =/=  0 ) )
48 neeq1 2610 . . . . . . . . 9  |-  ( z  =  y  ->  (
z  =/=  0  <->  y  =/=  0 ) )
4948rspcev 3053 . . . . . . . 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 32 . . . . . 6  |-  ( x  =  0  ->  (
x  =/=  y  -> 
( y  e.  RR  ->  E. z  e.  RR  z  =/=  0 ) ) )
5251com23 75 . . . . 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 2610 . . . . . . . 8  |-  ( z  =  x  ->  (
z  =/=  0  <->  x  =/=  0 ) )
5554rspcev 3053 . . . . . . 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 45 . . . 4  |-  ( x  =/=  0  ->  (
( x  e.  RR  /\  y  e.  RR )  ->  ( x  =/=  y  ->  E. z  e.  RR  z  =/=  0
) ) )
5953, 58pm2.61ine 2681 . . 3  |-  ( ( x  e.  RR  /\  y  e.  RR )  ->  ( x  =/=  y  ->  E. z  e.  RR  z  =/=  0 ) )
6059rexlimivv 2836 . 2  |-  ( E. x  e.  RR  E. y  e.  RR  x  =/=  y  ->  E. z  e.  RR  z  =/=  0
)
61 ax-rrecex 9063 . . . 4  |-  ( ( z  e.  RR  /\  z  =/=  0 )  ->  E. x  e.  RR  ( z  x.  x
)  =  1 )
62 remulcl 9076 . . . . . . 7  |-  ( ( z  e.  RR  /\  x  e.  RR )  ->  ( z  x.  x
)  e.  RR )
6362adantlr 697 . . . . . 6  |-  ( ( ( z  e.  RR  /\  z  =/=  0 )  /\  x  e.  RR )  ->  ( z  x.  x )  e.  RR )
64 eleq1 2497 . . . . . 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 2831 . . . 4  |-  ( ( z  e.  RR  /\  z  =/=  0 )  -> 
( E. x  e.  RR  ( z  x.  x )  =  1  ->  1  e.  RR ) )
6761, 66mpd 15 . . 3  |-  ( ( z  e.  RR  /\  z  =/=  0 )  -> 
1  e.  RR )
6867rexlimiva 2826 . 2  |-  ( E. z  e.  RR  z  =/=  0  ->  1  e.  RR )
6944, 60, 68mp2b 10 1  |-  1  e.  RR
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    \/ wo 359    /\ wa 360    = wceq 1653    e. wcel 1726    =/= wne 2600   E.wrex 2707  (class class class)co 6082   CCcc 8989   RRcr 8990   0cc0 8991   1c1 8992   _ici 8993    + caddc 8994    x. cmul 8996
This theorem is referenced by:  0re  9092  peano2re  9240  mul02lem2  9244  addid1  9247  renegcl  9365  peano2rem  9368  0reALT  9398  0lt1  9551  0le1  9552  1le1  9651  eqneg  9735  ltp1  9849  ltm1  9851  recgt0  9855  mulgt1  9870  ltmulgt11  9871  lemulge11  9873  ltrec  9892  reclt1  9906  recgt1  9907  recgt1i  9908  recp1lt1  9909  recreclt  9910  recgt0ii  9917  ledivp1i  9937  ltdivp1i  9938  inelr  9991  cju  9997  nnssre  10005  nnge1  10027  nngt1ne1  10028  nnle1eq1  10029  nngt0  10030  nnnlt1  10031  nnrecre  10037  nnrecgt0  10038  nnsub  10039  2re  10070  3re  10072  4re  10074  5re  10076  6re  10077  7re  10078  8re  10079  9re  10080  10re  10081  2pos  10083  3pos  10085  4pos  10087  5pos  10088  6pos  10089  7pos  10090  8pos  10091  9pos  10092  10pos  10093  1lt2  10143  1lt3  10145  1lt4  10148  1lt5  10152  1lt6  10157  1lt7  10163  1lt8  10170  1lt9  10178  1lt10  10187  1ne2  10188  halflt1  10190  addltmul  10204  nnunb  10218  elnnnn0c  10266  elnnz1  10308  znnnlt1  10309  zltp1le  10326  zleltp1  10327  recnz  10346  gtndiv  10348  suprzcl  10350  uzindOLD  10365  eluzp1m1  10510  eluzp1p1  10512  eluz2b2  10549  zbtwnre  10573  rebtwnz  10574  1rp  10617  qbtwnre  10786  qbtwnxr  10787  xmulid1  10859  xmulid2  10860  xmulm1  10861  x2times  10879  xrub  10891  0elunit  11016  1elunit  11017  lincmb01cmp  11039  iccf1o  11040  xov1plusxeqvd  11042  unitssre  11043  fztpval  11108  4fvwrd4  11122  elfznelfzo  11193  elfznelfzob  11194  fraclt1  11212  fracle1  11213  flbi2  11225  fladdz  11228  flhalf  11232  fldiv  11242  modid  11271  1mod  11274  seqf1olem1  11363  reexpcl  11399  reexpclz  11402  expge0  11417  expge1  11418  expgt1  11419  ltexp2a  11432  expcan  11433  ltexp2  11434  leexp2  11435  leexp2a  11436  leexp2r  11438  nnlesq  11485  bernneq  11506  bernneq2  11507  bernneq3  11508  expnbnd  11509  expnlbnd  11510  expnlbnd2  11511  expmulnbnd  11512  discr1  11516  facwordi  11581  faclbnd3  11584  faclbnd4lem1  11585  faclbnd4lem4  11588  faclbnd6  11591  facavg  11593  hashv01gt1  11630  hashge1  11664  hashnn0n0nn  11665  hash1snb  11682  hashgt12el  11683  hashgt12el2  11684  fzsdom2  11694  hashfun  11701  brfi1uzind  11716  f1oun2prg  11865  crre  11920  remim  11923  cjexp  11956  re1  11960  im1  11961  rei  11962  imi  11963  sqrlem1  12049  sqrlem2  12050  sqrlem3  12051  sqrlem4  12052  sqrlem7  12055  resqrex  12057  sqr1  12078  sqr2gt1lt2  12081  sqrm1  12082  abs1  12103  rddif  12145  absrdbnd  12146  caubnd2  12162  mulcn2  12390  reccn2  12391  rlimo1  12411  rlimno1  12448  iseraltlem2  12477  iseraltlem3  12478  iseralt  12479  o1fsum  12593  abscvgcvg  12599  climcndslem1  12630  climcndslem2  12631  flo1  12635  harmonic  12639  expcnv  12644  geolim  12648  geolim2  12649  georeclim  12650  geo2lim  12653  geomulcvg  12654  geoisumr  12656  geoisum1c  12658  geoihalfsum  12660  efcllem  12681  ere  12692  ege2le3  12693  efgt1  12718  resin4p  12740  recos4p  12741  tanhlt1  12762  tanhbnd  12763  sinbnd  12782  cosbnd  12783  sinbnd2  12784  cosbnd2  12785  ef01bndlem  12786  sin01bnd  12787  cos01bnd  12788  cos1bnd  12789  cos2bnd  12790  sinltx  12791  sin01gt0  12792  cos01gt0  12793  sin02gt0  12794  sincos1sgn  12795  eirrlem  12804  rpnnen2lem2  12816  rpnnen2lem3  12817  rpnnen2lem4  12818  rpnnen2lem9  12823  rpnnen2  12826  ruclem6  12835  ruclem11  12840  ruclem12  12841  nthruz  12852  3dvds  12913  bitsfzolem  12947  bitsfzo  12948  bitsmod  12949  bitscmp  12951  bitsinv1lem  12954  sadcadd  12971  smuval2  12995  isprm3  13089  prmind2  13091  sqnprm  13099  coprm  13101  isprm5  13113  divdenle  13142  zsqrelqelz  13151  phibndlem  13160  fermltl  13174  odzdvds  13182  pythagtriplem3  13193  iserodd  13210  pcmpt  13262  fldivp1  13267  pcfaclem  13268  pockthi  13276  infpn2  13282  prmreclem1  13285  prmreclem5  13289  4sqlem11  13324  4sqlem12  13325  ramub1lem1  13395  2expltfac  13427  resslem  13523  oppcbas  13945  rescbas  14030  rescabs  14034  odubas  14561  lt6abl  15505  pgpfaclem2  15641  abvneg  15923  abvtrivd  15929  xrsmcmn  16725  resubdrg  16751  gzrngunitlem  16764  gzrngunit  16765  znidomb  16843  thlbas  16924  leordtval2  17277  tuslem  18298  setsmsbas  18506  dscmet  18621  dscopn  18622  nrginvrcnlem  18727  nmoid  18777  idnghm  18778  tgioo  18828  blcvx  18830  xrsmopn  18844  metnrmlem1a  18889  metnrmlem1  18890  iicmp  18917  iicon  18918  iirev  18955  iihalf1  18957  iihalf1cn  18958  iihalf2  18959  iihalf2cn  18960  elii1  18961  elii2  18962  iimulcl  18963  icopnfcnv  18968  icopnfhmeo  18969  iccpnfcnv  18970  iccpnfhmeo  18971  xrhmeo  18972  xrhmph  18973  evth  18985  xlebnum  18991  lebnumii  18992  htpycc  19006  reparphti  19023  pcoval1  19039  pco0  19040  pco1  19041  pcoval2  19042  pcocn  19043  pcohtpylem  19045  pcopt  19048  pcopt2  19049  pcoass  19050  pcorevlem  19052  nmhmcn  19129  cncmet  19276  ovolunlem1a  19393  ovoliunlem1  19399  dyadmaxlem  19490  vitalilem2  19502  vitalilem4  19504  vitalilem5  19505  vitali  19506  mbfneg  19543  i1f1  19583  itg11  19584  i1fsub  19601  itg1sub  19602  mbfi1fseqlem6  19613  itg2const  19633  itg2mulc  19640  itg2monolem1  19643  itg2monolem3  19645  iblcnlem1  19680  i1fibl  19700  itgitg1  19701  dveflem  19864  mvth  19877  dvlipcn  19879  lhop1lem  19898  dvcvx  19905  dvfsumlem1  19911  dvfsumlem2  19912  dvfsumlem3  19913  dvfsumlem4  19914  dvfsum2  19919  ply1remlem  20086  fta1glem2  20090  fta1blem  20092  plyeq0lem  20130  fta1lem  20225  vieta1lem2  20229  aalioulem3  20252  aalioulem4  20253  aalioulem5  20254  aaliou3lem2  20261  aaliou3lem8  20263  ulmbdd  20315  iblulm  20324  radcnvlem1  20330  radcnvlem2  20331  dvradcnv  20338  abelthlem2  20349  abelthlem3  20350  abelthlem5  20352  abelthlem7  20355  abelth  20358  abelth2  20359  reeff1olem  20363  reeff1o  20364  sinhalfpilem  20375  tangtx  20414  sincos4thpi  20422  pige3  20426  coskpi  20429  cosne0  20433  recosf1o  20438  tanregt0  20442  efif1olem3  20447  efif1olem4  20448  loge  20482  rplogcl  20500  logdivlti  20516  logno1  20528  logcnlem4  20537  logf1o2  20542  dvlog2lem  20544  advlog  20546  logtayllem  20551  logtayl  20552  logccv  20555  recxpcl  20567  cxplt  20586  cxple  20587  cxplea  20588  cxpsqrlem  20594  cxpsqr  20595  cxpcn3lem  20632  cxpaddlelem  20636  cxpaddle  20637  loglesqr  20643  ang180lem1  20652  ang180lem2  20653  ang180lem3  20654  isosctrlem1  20663  isosctrlem2  20664  angpined  20672  chordthmlem4  20677  1cubrlem  20682  atanre  20726  asinsin  20733  acosrecl  20744  atandmcj  20750  atancj  20751  atanlogaddlem  20754  atantan  20764  bndatandm  20770  atans2  20772  ressatans  20775  leibpilem2  20782  leibpi  20783  leibpisum  20784  log2tlbnd  20786  birthdaylem3  20793  birthday  20794  rlimcnp  20805  rlimcnp2  20806  efrlim  20809  cxp2limlem  20815  cxp2lim  20816  cxploglim  20817  cxploglim2  20818  divsqrsumlem  20819  divsqrsumo1  20823  cvxcl  20824  scvxcvx  20825  jensenlem2  20827  amgmlem  20829  logdiflbnd  20834  emcllem2  20836  emcllem4  20838  emcllem6  20840  emcllem7  20841  emre  20845  emgt0  20846  harmonicbnd3  20847  harmonicubnd  20849  harmonicbnd4  20850  fsumharmonic  20851  wilthlem1  20852  wilthlem2  20853  ftalem1  20856  ftalem2  20857  ftalem5  20860  basellem3  20866  basellem9  20872  issqf  20920  cht1  20949  vma1  20950  chp1  20951  ppieq0  20960  ppiltx  20961  mumullem2  20964  fsumfldivdiaglem  20975  ppiublem1  20987  ppiub  20989  chpeq0  20993  chtublem  20996  chtub  20997  chpval2  21003  chpchtsum  21004  chpub  21005  logfacbnd3  21008  logfacrlim  21009  logexprlim  21010  mersenne  21012  perfectlem2  21015  dchrelbas4  21028  dchrinv  21046  dchr1re  21048  bcmono  21062  efexple  21066  bposlem1  21069  bposlem2  21070  bposlem5  21073  bposlem8  21076  lgslem3  21083  lgslem4  21084  lgsvalmod  21100  lgsmod  21106  lgsdir2lem1  21108  lgsdir2lem3  21110  lgsdir2lem4  21111  lgsdir2lem5  21112  lgsdirprm  21114  lgsdir  21115  lgsne0  21118  lgsabs1  21119  lgsdinn0  21125  lgseisen  21138  lgsquadlem2  21140  m1lgs  21147  2sqlem8  21157  chebbnd1lem1  21164  chebbnd1lem2  21165  chebbnd1lem3  21166  chebbnd1  21167  chtppilimlem1  21168  chtppilimlem2  21169  chtppilim  21170  chebbnd2  21172  chto1lb  21173  chpchtlim  21174  chpo1ubb  21176  vmadivsum  21177  vmadivsumb  21178  rplogsumlem1  21179  rplogsumlem2  21180  rpvmasumlem  21182  dchrisumlem3  21186  dchrmusumlema  21188  dchrmusum2  21189  dchrvmasumlem2  21193  dchrvmasumlem3  21194  dchrvmasumiflem1  21196  dchrvmasumiflem2  21197  dchrisum0flblem1  21203  dchrisum0flblem2  21204  dchrisum0fno1  21206  rpvmasum2  21207  dchrisum0re  21208  dchrisum0lema  21209  dchrisum0lem1b  21210  dchrisum0lem1  21211  dchrisum0lem2a  21212  dchrisum0lem2  21213  dchrisum0lem3  21214  rplogsum  21222  dirith2  21223  mudivsum  21225  mulogsumlem  21226  mulogsum  21227  logdivsum  21228  mulog2sumlem1  21229  mulog2sumlem2  21230  vmalogdivsum2  21233  2vmadivsumlem  21235  log2sumbnd  21239  selberglem2  21241  selbergb  21244  selberg2lem  21245  selberg2b  21247  chpdifbndlem1  21248  chpdifbnd  21250  selberg3lem1  21252  selberg3lem2  21253  selberg4lem1  21255  pntrmax  21259  pntrsumo1  21260  pntrsumbnd  21261  selberg34r  21266  selbergsb  21270  pntrlog2bndlem1  21272  pntrlog2bndlem2  21273  pntrlog2bndlem3  21274  pntrlog2bndlem4  21275  pntrlog2bndlem5  21276  pntrlog2bndlem6  21278  pntrlog2bnd  21279  pntpbnd1a  21280  pntpbnd1  21281  pntpbnd2  21282  pntibndlem1  21284  pntibndlem2a  21285  pntibndlem2  21286  pntibndlem3  21287  pntibnd  21288  pntlemd  21289  pntlemc  21290  pntlemb  21292  pntlemg  21293  pntlemr  21297  pntlemf  21300  pntlemk  21301  pntlemo  21302  pntlem3  21304  pntleml  21306  pnt  21309  abvcxp  21310  ostth2lem1  21313  qabvle  21320  padicabvf  21326  padicabvcxp  21327  ostth1  21328  ostth2lem2  21329  ostth2lem3  21330  ostth2lem4  21331  ostth2  21332  ostth3  21333  ostth  21334  usgraex1elv  21417  usgraexmpldifpr  21420  spthispth  21574  constr3lem4  21635  constr3pthlem1  21643  constr3pthlem3  21645  konigsberg  21710  ex-dif  21732  ex-in  21734  ex-pss  21737  ex-res  21750  ex-fl  21756  nv1  22166  smcnlem  22194  ipidsq  22210  nmoub3i  22275  nmlno0lem  22295  blocnilem  22306  ipasslem10  22341  ubthlem2  22374  minvecolem4  22383  htthlem  22421  hisubcomi  22607  normlem9  22621  norm-ii-i  22640  bcs2  22685  norm1  22752  nmopub2tALT  23413  nmfnleub2  23430  nmlnop0iALT  23499  nmopun  23518  unopbd  23519  hmopd  23526  nmcexi  23530  nmopadjlem  23593  nmopcoi  23599  nmopcoadji  23605  opsqrlem4  23647  pjnmopi  23652  pjbdlni  23653  stge0  23728  stle1  23729  hstle1  23730  hstle  23734  hstles  23735  stge1i  23742  stlesi  23745  staddi  23750  stadd3i  23752  strlem1  23754  strlem3a  23756  strlem5  23759  jplem1  23772  cdj1i  23937  addltmulALT  23950  xlt2addrd  24125  fzsplit3  24151  xdivrec  24174  xrsmulgzz  24201  xrnarchi  24255  remulg  24271  elunitrn  24296  elunitge0  24298  unitssxrge0  24299  unitdivcld  24300  sqsscirc1  24307  xrge0iifcnv  24320  xrge0iifcv  24321  xrge0iifiso  24322  xrge0iifhom  24324  zrhre  24386  rnlogblem  24400  log2le1  24408  indf  24414  indfval  24415  pr01ssre  24416  indf1o  24422  esumcst  24456  esumdivc  24474  hasheuni  24476  cntnevol  24583  dya2ub  24621  dya2iocress  24625  dya2iocbrsiga  24626  dya2icobrsiga  24627  dya2icoseg  24628  dya2iocucvr  24635  sxbrsigalem2  24637  prob01  24672  probmeasb  24689  dstrvprob  24730  dstfrvunirn  24733  dstfrvclim1  24736  coinfliprv  24741  ballotlem2  24747  ballotlemfc0  24751  ballotlemfcc  24752  ballotlem4  24757  ballotlemi1  24761  ballotlemic  24765  ballotlem1c  24766  ballotlemsgt1  24769  ballotlemsel1i  24771  ballotlemfrcn0  24788  zetacvg  24800  lgamgulmlem2  24815  lgamgulmlem3  24816  lgamgulmlem4  24817  lgamgulmlem5  24818  lgamgulmlem6  24819  lgamcvg2  24840  regamcl  24846  subfacp1lem1  24866  subfacp1lem5  24871  subfacval2  24874  subfaclim  24875  subfacval3  24876  rescon  24934  iiscon  24940  iillyscon  24941  cvmliftlem2  24974  cvmliftlem13  24984  snmlff  25017  sinccvglem  25110  divelunit  25186  dedekind  25188  relin01  25195  fznatpl1  25199  fz0n  25203  fprodrecl  25280  rerisefaccl  25334  refallfaccl  25335  risefall0lem  25343  binomfallfaclem2  25357  faclim  25366  brbtwn2  25845  colinearalglem4  25849  ax5seglem1  25868  ax5seglem2  25869  ax5seglem3  25871  ax5seglem5  25873  ax5seglem6  25874  ax5seglem9  25877  ax5seg  25878  axbtwnid  25879  axpaschlem  25880  axpasch  25881  axlowdimlem3  25884  axlowdimlem6  25887  axlowdimlem7  25888  axlowdimlem10  25891  axlowdimlem16  25897  axlowdimlem17  25898  axlowdim1  25899  axlowdim2  25900  axlowdim  25901  axcontlem2  25905  axcontlem4  25907  axcontlem7  25910  bpoly4  26106  itg2addnclem2  26258  itg2addnclem3  26259  ftc1anclem5  26285  dvreasin  26291  dvreacos  26292  areacirclem1  26293  areacirclem4  26296  nn0prpwlem  26326  fdc  26450  incsequz  26453  geomcau  26466  totbndbnd  26499  cntotbnd  26506  heiborlem8  26528  bfplem2  26533  bfp  26534  lzenom  26829  rabren3dioph  26877  irrapxlem1  26886  irrapxlem2  26887  irrapxlem4  26889  irrapxlem5  26890  pellexlem2  26894  pellexlem5  26897  pellexlem6  26898  pell1qrge1  26934  pell1qr1  26935  elpell1qr2  26936  pell1qrgaplem  26937  pell14qrgap  26939  pell14qrgapw  26940  pellqrex  26943  pellfundre  26945  pellfundgt1  26947  pellfundlb  26948  pellfundglb  26949  pellfundex  26950  pellfund14gap  26951  pellfundrp  26952  pellfundne1  26953  rmspecsqrnq  26970  rmspecnonsq  26971  rmspecfund  26973  rmspecpos  26980  monotoddzzfi  27006  jm2.17a  27026  rmygeid  27030  acongeq  27049  jm2.23  27068  jm3.1lem2  27090  matbas  27446  lhe4.4ex1a  27524  fmul01  27687  fmul01lt1lem1  27691  fmul01lt1lem2  27692  climsuselem1  27710  stoweidlem1  27727  stoweidlem5  27731  stoweidlem7  27733  stoweidlem10  27736  stoweidlem11  27737  stoweidlem12  27738  stoweidlem13  27739  stoweidlem14  27740  stoweidlem16  27742  stoweidlem18  27744  stoweidlem19  27745  stoweidlem20  27746  stoweidlem22  27748  stoweidlem24  27750  stoweidlem25  27751  stoweidlem26  27752  stoweidlem28  27754  stoweidlem34  27760  stoweidlem36  27762  stoweidlem38  27764  stoweidlem40  27766  stoweidlem41  27767  stoweidlem42  27768  stoweidlem45  27771  stoweidlem51  27777  stoweidlem59  27785  stoweidlem60  27786  stoweid  27789  wallispilem3  27793  wallispilem4  27794  wallispilem5  27795  wallispi  27796  wallispi2lem1  27797  wallispi2lem2  27798  wallispi2  27799  stirlinglem1  27800  stirlinglem3  27802  stirlinglem5  27804  stirlinglem6  27805  stirlinglem7  27806  stirlinglem8  27807  stirlinglem10  27809  stirlinglem11  27810  stirlinglem12  27811  stirlinglem13  27812  stirlinglem15  27814  sigaradd  27833  2eluzge1  28103  ubmelm1fzo  28128  ltdifltdiv  28149  euhash1  28168  modprm0  28229  cshwidxn  28248  swrdtrcfvl  28266  usgra2pthlem1  28311  frgrawopreglem2  28435  reseccl  28497  recsccl  28498  sgn1  28523  ene1  28532  isosctrlem1ALT  29047
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2418  ax-1cn 9049  ax-icn 9050  ax-addcl 9051  ax-mulcl 9053  ax-mulrcl 9054  ax-i2m1 9059  ax-1ne0 9060  ax-rrecex 9063  ax-cnre 9064
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2424  df-cleq 2430  df-clel 2433  df-nfc 2562  df-ne 2602  df-ral 2711  df-rex 2712  df-rab 2715  df-v 2959  df-dif 3324  df-un 3326  df-in 3328  df-ss 3335  df-nul 3630  df-if 3741  df-sn 3821  df-pr 3822  df-op 3824  df-uni 4017  df-br 4214  df-iota 5419  df-fv 5463  df-ov 6085
  Copyright terms: Public domain W3C validator