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

Theorem 1re 9092
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 9050, 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 9061 . . 3  |-  1  =/=  0
2 ax-1cn 9050 . . . . 5  |-  1  e.  CC
3 cnre 9089 . . . . 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 2611 . . . . . . . 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 9086 . . . . . . . 8  |-  0  e.  CC
8 cnre 9089 . . . . . . . 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 2612 . . . . . . . . . 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 2819 . . . . . . . 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 2819 . . . . . . 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 2819 . . . . 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 2819 . . . 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 2603 . . . . . . . . . . 11  |-  ( a  =/=  c  <->  -.  a  =  c )
2019con2bii 324 . . . . . . . . . 10  |-  ( a  =  c  <->  -.  a  =/=  c )
21 df-ne 2603 . . . . . . . . . . 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 6091 . . . . . . . . 9  |-  ( b  =  d  ->  (
_i  x.  b )  =  ( _i  x.  d ) )
2725, 26oveqan12d 6102 . . . . . . . 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 2648 . . . . . 6  |-  ( ( a  +  ( _i  x.  b ) )  =/=  ( c  +  ( _i  x.  d
) )  ->  (
a  =/=  c  \/  b  =/=  d ) )
30 neeq1 2611 . . . . . . . . . 10  |-  ( x  =  a  ->  (
x  =/=  y  <->  a  =/=  y ) )
31 neeq2 2612 . . . . . . . . . 10  |-  ( y  =  c  ->  (
a  =/=  y  <->  a  =/=  c ) )
3230, 31rspc2ev 3062 . . . . . . . . 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 2611 . . . . . . . . . 10  |-  ( x  =  b  ->  (
x  =/=  y  <->  b  =/=  y ) )
36 neeq2 2612 . . . . . . . . . 10  |-  ( y  =  d  ->  (
b  =/=  y  <->  b  =/=  d ) )
3735, 36rspc2ev 3062 . . . . . . . . 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 2839 . . . 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 2837 . . 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 2457 . . . . . . . . 9  |-  ( ( x  =  0  /\  y  =  0 )  ->  x  =  y )
4645ex 425 . . . . . . . 8  |-  ( x  =  0  ->  (
y  =  0  ->  x  =  y )
)
4746necon3d 2641 . . . . . . 7  |-  ( x  =  0  ->  (
x  =/=  y  -> 
y  =/=  0 ) )
48 neeq1 2611 . . . . . . . . 9  |-  ( z  =  y  ->  (
z  =/=  0  <->  y  =/=  0 ) )
4948rspcev 3054 . . . . . . . 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 2611 . . . . . . . 8  |-  ( z  =  x  ->  (
z  =/=  0  <->  x  =/=  0 ) )
5554rspcev 3054 . . . . . . 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 2682 . . 3  |-  ( ( x  e.  RR  /\  y  e.  RR )  ->  ( x  =/=  y  ->  E. z  e.  RR  z  =/=  0 ) )
6059rexlimivv 2837 . 2  |-  ( E. x  e.  RR  E. y  e.  RR  x  =/=  y  ->  E. z  e.  RR  z  =/=  0
)
61 ax-rrecex 9064 . . . 4  |-  ( ( z  e.  RR  /\  z  =/=  0 )  ->  E. x  e.  RR  ( z  x.  x
)  =  1 )
62 remulcl 9077 . . . . . . 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 2498 . . . . . 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 2832 . . . 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 2827 . 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 2601   E.wrex 2708  (class class class)co 6083   CCcc 8990   RRcr 8991   0cc0 8992   1c1 8993   _ici 8994    + caddc 8995    x. cmul 8997
This theorem is referenced by:  0re  9093  peano2re  9241  mul02lem2  9245  addid1  9248  renegcl  9366  peano2rem  9369  0reALT  9399  0lt1  9552  0le1  9553  1le1  9652  eqneg  9736  ltp1  9850  ltm1  9852  recgt0  9856  mulgt1  9871  ltmulgt11  9872  lemulge11  9874  ltrec  9893  reclt1  9907  recgt1  9908  recgt1i  9909  recp1lt1  9910  recreclt  9911  recgt0ii  9918  ledivp1i  9938  ltdivp1i  9939  inelr  9992  cju  9998  nnssre  10006  nnge1  10028  nngt1ne1  10029  nnle1eq1  10030  nngt0  10031  nnnlt1  10032  nnrecre  10038  nnrecgt0  10039  nnsub  10040  2re  10071  3re  10073  4re  10075  5re  10077  6re  10078  7re  10079  8re  10080  9re  10081  10re  10082  2pos  10084  3pos  10086  4pos  10088  5pos  10089  6pos  10090  7pos  10091  8pos  10092  9pos  10093  10pos  10094  1lt2  10144  1lt3  10146  1lt4  10149  1lt5  10153  1lt6  10158  1lt7  10164  1lt8  10171  1lt9  10179  1lt10  10188  1ne2  10189  halflt1  10191  addltmul  10205  nnunb  10219  elnnnn0c  10267  elnnz1  10309  znnnlt1  10310  zltp1le  10327  zleltp1  10328  recnz  10347  gtndiv  10349  suprzcl  10351  uzindOLD  10366  eluzp1m1  10511  eluzp1p1  10513  eluz2b2  10550  zbtwnre  10574  rebtwnz  10575  1rp  10618  qbtwnre  10787  qbtwnxr  10788  xmulid1  10860  xmulid2  10861  xmulm1  10862  x2times  10880  xrub  10892  0elunit  11017  1elunit  11018  lincmb01cmp  11040  iccf1o  11041  xov1plusxeqvd  11043  unitssre  11044  fztpval  11109  4fvwrd4  11123  elfznelfzo  11194  elfznelfzob  11195  fraclt1  11213  fracle1  11214  flbi2  11226  fladdz  11229  flhalf  11233  fldiv  11243  modid  11272  1mod  11275  seqf1olem1  11364  reexpcl  11400  reexpclz  11403  expge0  11418  expge1  11419  expgt1  11420  ltexp2a  11433  expcan  11434  ltexp2  11435  leexp2  11436  leexp2a  11437  leexp2r  11439  nnlesq  11486  bernneq  11507  bernneq2  11508  bernneq3  11509  expnbnd  11510  expnlbnd  11511  expnlbnd2  11512  expmulnbnd  11513  discr1  11517  facwordi  11582  faclbnd3  11585  faclbnd4lem1  11586  faclbnd4lem4  11589  faclbnd6  11592  facavg  11594  hashv01gt1  11631  hashge1  11665  hashnn0n0nn  11666  hash1snb  11683  hashgt12el  11684  hashgt12el2  11685  fzsdom2  11695  hashfun  11702  brfi1uzind  11717  f1oun2prg  11866  crre  11921  remim  11924  cjexp  11957  re1  11961  im1  11962  rei  11963  imi  11964  sqrlem1  12050  sqrlem2  12051  sqrlem3  12052  sqrlem4  12053  sqrlem7  12056  resqrex  12058  sqr1  12079  sqr2gt1lt2  12082  sqrm1  12083  abs1  12104  rddif  12146  absrdbnd  12147  caubnd2  12163  mulcn2  12391  reccn2  12392  rlimo1  12412  rlimno1  12449  iseraltlem2  12478  iseraltlem3  12479  iseralt  12480  o1fsum  12594  abscvgcvg  12600  climcndslem1  12631  climcndslem2  12632  flo1  12636  harmonic  12640  expcnv  12645  geolim  12649  geolim2  12650  georeclim  12651  geo2lim  12654  geomulcvg  12655  geoisumr  12657  geoisum1c  12659  geoihalfsum  12661  efcllem  12682  ere  12693  ege2le3  12694  efgt1  12719  resin4p  12741  recos4p  12742  tanhlt1  12763  tanhbnd  12764  sinbnd  12783  cosbnd  12784  sinbnd2  12785  cosbnd2  12786  ef01bndlem  12787  sin01bnd  12788  cos01bnd  12789  cos1bnd  12790  cos2bnd  12791  sinltx  12792  sin01gt0  12793  cos01gt0  12794  sin02gt0  12795  sincos1sgn  12796  eirrlem  12805  rpnnen2lem2  12817  rpnnen2lem3  12818  rpnnen2lem4  12819  rpnnen2lem9  12824  rpnnen2  12827  ruclem6  12836  ruclem11  12841  ruclem12  12842  nthruz  12853  3dvds  12914  bitsfzolem  12948  bitsfzo  12949  bitsmod  12950  bitscmp  12952  bitsinv1lem  12955  sadcadd  12972  smuval2  12996  isprm3  13090  prmind2  13092  sqnprm  13100  coprm  13102  isprm5  13114  divdenle  13143  zsqrelqelz  13152  phibndlem  13161  fermltl  13175  odzdvds  13183  pythagtriplem3  13194  iserodd  13211  pcmpt  13263  fldivp1  13268  pcfaclem  13269  pockthi  13277  infpn2  13283  prmreclem1  13286  prmreclem5  13290  4sqlem11  13325  4sqlem12  13326  ramub1lem1  13396  2expltfac  13428  resslem  13524  oppcbas  13946  rescbas  14031  rescabs  14035  odubas  14562  lt6abl  15506  pgpfaclem2  15642  abvneg  15924  abvtrivd  15930  xrsmcmn  16726  resubdrg  16752  gzrngunitlem  16765  gzrngunit  16766  znidomb  16844  thlbas  16925  leordtval2  17278  tuslem  18299  setsmsbas  18507  dscmet  18622  dscopn  18623  nrginvrcnlem  18728  nmoid  18778  idnghm  18779  tgioo  18829  blcvx  18831  xrsmopn  18845  metnrmlem1a  18890  metnrmlem1  18891  iicmp  18918  iicon  18919  iirev  18956  iihalf1  18958  iihalf1cn  18959  iihalf2  18960  iihalf2cn  18961  elii1  18962  elii2  18963  iimulcl  18964  icopnfcnv  18969  icopnfhmeo  18970  iccpnfcnv  18971  iccpnfhmeo  18972  xrhmeo  18973  xrhmph  18974  evth  18986  xlebnum  18992  lebnumii  18993  htpycc  19007  reparphti  19024  pcoval1  19040  pco0  19041  pco1  19042  pcoval2  19043  pcocn  19044  pcohtpylem  19046  pcopt  19049  pcopt2  19050  pcoass  19051  pcorevlem  19053  nmhmcn  19130  cncmet  19277  ovolunlem1a  19394  ovoliunlem1  19400  dyadmaxlem  19491  vitalilem2  19503  vitalilem4  19505  vitalilem5  19506  vitali  19507  mbfneg  19544  i1f1  19584  itg11  19585  i1fsub  19602  itg1sub  19603  mbfi1fseqlem6  19614  itg2const  19634  itg2mulc  19641  itg2monolem1  19644  itg2monolem3  19646  iblcnlem1  19681  i1fibl  19701  itgitg1  19702  dveflem  19865  mvth  19878  dvlipcn  19880  lhop1lem  19899  dvcvx  19906  dvfsumlem1  19912  dvfsumlem2  19913  dvfsumlem3  19914  dvfsumlem4  19915  dvfsum2  19920  ply1remlem  20087  fta1glem2  20091  fta1blem  20093  plyeq0lem  20131  fta1lem  20226  vieta1lem2  20230  aalioulem3  20253  aalioulem4  20254  aalioulem5  20255  aaliou3lem2  20262  aaliou3lem8  20264  ulmbdd  20316  iblulm  20325  radcnvlem1  20331  radcnvlem2  20332  dvradcnv  20339  abelthlem2  20350  abelthlem3  20351  abelthlem5  20353  abelthlem7  20356  abelth  20359  abelth2  20360  reeff1olem  20364  reeff1o  20365  sinhalfpilem  20376  tangtx  20415  sincos4thpi  20423  pige3  20427  coskpi  20430  cosne0  20434  recosf1o  20439  tanregt0  20443  efif1olem3  20448  efif1olem4  20449  loge  20483  rplogcl  20501  logdivlti  20517  logno1  20529  logcnlem4  20538  logf1o2  20543  dvlog2lem  20545  advlog  20547  logtayllem  20552  logtayl  20553  logccv  20556  recxpcl  20568  cxplt  20587  cxple  20588  cxplea  20589  cxpsqrlem  20595  cxpsqr  20596  cxpcn3lem  20633  cxpaddlelem  20637  cxpaddle  20638  loglesqr  20644  ang180lem1  20653  ang180lem2  20654  ang180lem3  20655  isosctrlem1  20664  isosctrlem2  20665  angpined  20673  chordthmlem4  20678  1cubrlem  20683  atanre  20727  asinsin  20734  acosrecl  20745  atandmcj  20751  atancj  20752  atanlogaddlem  20755  atantan  20765  bndatandm  20771  atans2  20773  ressatans  20776  leibpilem2  20783  leibpi  20784  leibpisum  20785  log2tlbnd  20787  birthdaylem3  20794  birthday  20795  rlimcnp  20806  rlimcnp2  20807  efrlim  20810  cxp2limlem  20816  cxp2lim  20817  cxploglim  20818  cxploglim2  20819  divsqrsumlem  20820  divsqrsumo1  20824  cvxcl  20825  scvxcvx  20826  jensenlem2  20828  amgmlem  20830  logdiflbnd  20835  emcllem2  20837  emcllem4  20839  emcllem6  20841  emcllem7  20842  emre  20846  emgt0  20847  harmonicbnd3  20848  harmonicubnd  20850  harmonicbnd4  20851  fsumharmonic  20852  wilthlem1  20853  wilthlem2  20854  ftalem1  20857  ftalem2  20858  ftalem5  20861  basellem3  20867  basellem9  20873  issqf  20921  cht1  20950  vma1  20951  chp1  20952  ppieq0  20961  ppiltx  20962  mumullem2  20965  fsumfldivdiaglem  20976  ppiublem1  20988  ppiub  20990  chpeq0  20994  chtublem  20997  chtub  20998  chpval2  21004  chpchtsum  21005  chpub  21006  logfacbnd3  21009  logfacrlim  21010  logexprlim  21011  mersenne  21013  perfectlem2  21016  dchrelbas4  21029  dchrinv  21047  dchr1re  21049  bcmono  21063  efexple  21067  bposlem1  21070  bposlem2  21071  bposlem5  21074  bposlem8  21077  lgslem3  21084  lgslem4  21085  lgsvalmod  21101  lgsmod  21107  lgsdir2lem1  21109  lgsdir2lem3  21111  lgsdir2lem4  21112  lgsdir2lem5  21113  lgsdirprm  21115  lgsdir  21116  lgsne0  21119  lgsabs1  21120  lgsdinn0  21126  lgseisen  21139  lgsquadlem2  21141  m1lgs  21148  2sqlem8  21158  chebbnd1lem1  21165  chebbnd1lem2  21166  chebbnd1lem3  21167  chebbnd1  21168  chtppilimlem1  21169  chtppilimlem2  21170  chtppilim  21171  chebbnd2  21173  chto1lb  21174  chpchtlim  21175  chpo1ubb  21177  vmadivsum  21178  vmadivsumb  21179  rplogsumlem1  21180  rplogsumlem2  21181  rpvmasumlem  21183  dchrisumlem3  21187  dchrmusumlema  21189  dchrmusum2  21190  dchrvmasumlem2  21194  dchrvmasumlem3  21195  dchrvmasumiflem1  21197  dchrvmasumiflem2  21198  dchrisum0flblem1  21204  dchrisum0flblem2  21205  dchrisum0fno1  21207  rpvmasum2  21208  dchrisum0re  21209  dchrisum0lema  21210  dchrisum0lem1b  21211  dchrisum0lem1  21212  dchrisum0lem2a  21213  dchrisum0lem2  21214  dchrisum0lem3  21215  rplogsum  21223  dirith2  21224  mudivsum  21226  mulogsumlem  21227  mulogsum  21228  logdivsum  21229  mulog2sumlem1  21230  mulog2sumlem2  21231  vmalogdivsum2  21234  2vmadivsumlem  21236  log2sumbnd  21240  selberglem2  21242  selbergb  21245  selberg2lem  21246  selberg2b  21248  chpdifbndlem1  21249  chpdifbnd  21251  selberg3lem1  21253  selberg3lem2  21254  selberg4lem1  21256  pntrmax  21260  pntrsumo1  21261  pntrsumbnd  21262  selberg34r  21267  selbergsb  21271  pntrlog2bndlem1  21273  pntrlog2bndlem2  21274  pntrlog2bndlem3  21275  pntrlog2bndlem4  21276  pntrlog2bndlem5  21277  pntrlog2bndlem6  21279  pntrlog2bnd  21280  pntpbnd1a  21281  pntpbnd1  21282  pntpbnd2  21283  pntibndlem1  21285  pntibndlem2a  21286  pntibndlem2  21287  pntibndlem3  21288  pntibnd  21289  pntlemd  21290  pntlemc  21291  pntlemb  21293  pntlemg  21294  pntlemr  21298  pntlemf  21301  pntlemk  21302  pntlemo  21303  pntlem3  21305  pntleml  21307  pnt  21310  abvcxp  21311  ostth2lem1  21314  qabvle  21321  padicabvf  21327  padicabvcxp  21328  ostth1  21329  ostth2lem2  21330  ostth2lem3  21331  ostth2lem4  21332  ostth2  21333  ostth3  21334  ostth  21335  usgraex1elv  21418  usgraexmpldifpr  21421  spthispth  21575  constr3lem4  21636  constr3pthlem1  21644  constr3pthlem3  21646  konigsberg  21711  ex-dif  21733  ex-in  21735  ex-pss  21738  ex-res  21751  ex-fl  21757  nv1  22167  smcnlem  22195  ipidsq  22211  nmoub3i  22276  nmlno0lem  22296  blocnilem  22307  ipasslem10  22342  ubthlem2  22375  minvecolem4  22384  htthlem  22422  hisubcomi  22608  normlem9  22622  norm-ii-i  22641  bcs2  22686  norm1  22753  nmopub2tALT  23414  nmfnleub2  23431  nmlnop0iALT  23500  nmopun  23519  unopbd  23520  hmopd  23527  nmcexi  23531  nmopadjlem  23594  nmopcoi  23600  nmopcoadji  23606  opsqrlem4  23648  pjnmopi  23653  pjbdlni  23654  stge0  23729  stle1  23730  hstle1  23731  hstle  23735  hstles  23736  stge1i  23743  stlesi  23746  staddi  23751  stadd3i  23753  strlem1  23755  strlem3a  23757  strlem5  23760  jplem1  23773  cdj1i  23938  addltmulALT  23951  xlt2addrd  24126  fzsplit3  24152  xdivrec  24175  xrsmulgzz  24202  xrnarchi  24256  remulg  24272  elunitrn  24297  elunitge0  24299  unitssxrge0  24300  unitdivcld  24301  sqsscirc1  24308  xrge0iifcnv  24321  xrge0iifcv  24322  xrge0iifiso  24323  xrge0iifhom  24325  zrhre  24387  rnlogblem  24401  log2le1  24409  indf  24415  indfval  24416  pr01ssre  24417  indf1o  24423  esumcst  24457  esumdivc  24475  hasheuni  24477  cntnevol  24584  dya2ub  24622  dya2iocress  24626  dya2iocbrsiga  24627  dya2icobrsiga  24628  dya2icoseg  24629  dya2iocucvr  24636  sxbrsigalem2  24638  prob01  24673  probmeasb  24690  dstrvprob  24731  dstfrvunirn  24734  dstfrvclim1  24737  coinfliprv  24742  ballotlem2  24748  ballotlemfc0  24752  ballotlemfcc  24753  ballotlem4  24758  ballotlemi1  24762  ballotlemic  24766  ballotlem1c  24767  ballotlemsgt1  24770  ballotlemsel1i  24772  ballotlemfrcn0  24789  zetacvg  24801  lgamgulmlem2  24816  lgamgulmlem3  24817  lgamgulmlem4  24818  lgamgulmlem5  24819  lgamgulmlem6  24820  lgamcvg2  24841  regamcl  24847  subfacp1lem1  24867  subfacp1lem5  24872  subfacval2  24875  subfaclim  24876  subfacval3  24877  rescon  24935  iiscon  24941  iillyscon  24942  cvmliftlem2  24975  cvmliftlem13  24985  snmlff  25018  sinccvglem  25111  divelunit  25187  dedekind  25189  relin01  25196  fznatpl1  25200  fz0n  25204  fprodrecl  25281  rerisefaccl  25335  refallfaccl  25336  risefall0lem  25344  binomfallfaclem2  25358  faclim  25367  brbtwn2  25846  colinearalglem4  25850  ax5seglem1  25869  ax5seglem2  25870  ax5seglem3  25872  ax5seglem5  25874  ax5seglem6  25875  ax5seglem9  25878  ax5seg  25879  axbtwnid  25880  axpaschlem  25881  axpasch  25882  axlowdimlem3  25885  axlowdimlem6  25888  axlowdimlem7  25889  axlowdimlem10  25892  axlowdimlem16  25898  axlowdimlem17  25899  axlowdim1  25900  axlowdim2  25901  axlowdim  25902  axcontlem2  25906  axcontlem4  25908  axcontlem7  25911  bpoly4  26107  itg2addnclem2  26259  itg2addnclem3  26260  ftc1anclem5  26286  dvreasin  26292  dvreacos  26293  areacirclem1  26294  areacirclem4  26297  nn0prpwlem  26327  fdc  26451  incsequz  26454  geomcau  26467  totbndbnd  26500  cntotbnd  26507  heiborlem8  26529  bfplem2  26534  bfp  26535  lzenom  26830  rabren3dioph  26878  irrapxlem1  26887  irrapxlem2  26888  irrapxlem4  26890  irrapxlem5  26891  pellexlem2  26895  pellexlem5  26898  pellexlem6  26899  pell1qrge1  26935  pell1qr1  26936  elpell1qr2  26937  pell1qrgaplem  26938  pell14qrgap  26940  pell14qrgapw  26941  pellqrex  26944  pellfundre  26946  pellfundgt1  26948  pellfundlb  26949  pellfundglb  26950  pellfundex  26951  pellfund14gap  26952  pellfundrp  26953  pellfundne1  26954  rmspecsqrnq  26971  rmspecnonsq  26972  rmspecfund  26974  rmspecpos  26981  monotoddzzfi  27007  jm2.17a  27027  rmygeid  27031  acongeq  27050  jm2.23  27069  jm3.1lem2  27091  matbas  27447  lhe4.4ex1a  27525  fmul01  27688  fmul01lt1lem1  27692  fmul01lt1lem2  27693  climsuselem1  27711  stoweidlem1  27728  stoweidlem5  27732  stoweidlem7  27734  stoweidlem10  27737  stoweidlem11  27738  stoweidlem12  27739  stoweidlem13  27740  stoweidlem14  27741  stoweidlem16  27743  stoweidlem18  27745  stoweidlem19  27746  stoweidlem20  27747  stoweidlem22  27749  stoweidlem24  27751  stoweidlem25  27752  stoweidlem26  27753  stoweidlem28  27755  stoweidlem34  27761  stoweidlem36  27763  stoweidlem38  27765  stoweidlem40  27767  stoweidlem41  27768  stoweidlem42  27769  stoweidlem45  27772  stoweidlem51  27778  stoweidlem59  27786  stoweidlem60  27787  stoweid  27790  wallispilem3  27794  wallispilem4  27795  wallispilem5  27796  wallispi  27797  wallispi2lem1  27798  wallispi2lem2  27799  wallispi2  27800  stirlinglem1  27801  stirlinglem3  27803  stirlinglem5  27805  stirlinglem6  27806  stirlinglem7  27807  stirlinglem8  27808  stirlinglem10  27810  stirlinglem11  27811  stirlinglem12  27812  stirlinglem13  27813  stirlinglem15  27815  sigaradd  27834  2eluzge1  28113  ubmelm1fzo  28138  ltdifltdiv  28159  euhash1  28178  modprm0  28250  cshwidxn  28269  swrdtrcfvl  28287  usgra2pthlem1  28336  frgrawopreglem2  28496  reseccl  28558  recsccl  28559  sgn1  28584  ene1  28593  isosctrlem1ALT  29108
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 2419  ax-1cn 9050  ax-icn 9051  ax-addcl 9052  ax-mulcl 9054  ax-mulrcl 9055  ax-i2m1 9060  ax-1ne0 9061  ax-rrecex 9064  ax-cnre 9065
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 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2712  df-rex 2713  df-rab 2716  df-v 2960  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-nul 3631  df-if 3742  df-sn 3822  df-pr 3823  df-op 3825  df-uni 4018  df-br 4215  df-iota 5420  df-fv 5464  df-ov 6086
  Copyright terms: Public domain W3C validator