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

Theorem 1re 8832
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 8790, 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
Dummy variables  a 
b  c  d  x  y  z are mutually distinct and distinct from all other variables.

Proof of Theorem 1re
StepHypRef Expression
1 ax-1ne0 8801 . . 3  |-  1  =/=  0
2 ax-1cn 8790 . . . . 5  |-  1  e.  CC
3 cnre 8829 . . . . 5  |-  ( 1  e.  CC  ->  E. a  e.  RR  E. b  e.  RR  1  =  ( a  +  ( _i  x.  b ) ) )
42, 3ax-mp 10 . . . 4  |-  E. a  e.  RR  E. b  e.  RR  1  =  ( a  +  ( _i  x.  b ) )
5 neeq1 2455 . . . . . . . 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 8826 . . . . . . . 8  |-  0  e.  CC
8 cnre 8829 . . . . . . . 8  |-  ( 0  e.  CC  ->  E. c  e.  RR  E. d  e.  RR  0  =  ( c  +  ( _i  x.  d ) ) )
97, 8ax-mp 10 . . . . . . 7  |-  E. c  e.  RR  E. d  e.  RR  0  =  ( c  +  ( _i  x.  d ) )
10 neeq2 2456 . . . . . . . . . 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 2655 . . . . . . . 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 2655 . . . . . . 7  |-  ( ( a  +  ( _i  x.  b ) )  =/=  0  ->  ( E. c  e.  RR  E. d  e.  RR  0  =  ( c  +  ( _i  x.  d
) )  ->  E. c  e.  RR  E. d  e.  RR  ( a  +  ( _i  x.  b
) )  =/=  (
c  +  ( _i  x.  d ) ) ) )
146, 9, 13syl6mpi 60 . . . . . 6  |-  ( 1  =/=  0  ->  (
1  =  ( a  +  ( _i  x.  b ) )  ->  E. c  e.  RR  E. d  e.  RR  (
a  +  ( _i  x.  b ) )  =/=  ( c  +  ( _i  x.  d
) ) ) )
1514reximdv 2655 . . . . 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 2655 . . . 4  |-  ( 1  =/=  0  ->  ( E. a  e.  RR  E. b  e.  RR  1  =  ( a  +  ( _i  x.  b
) )  ->  E. a  e.  RR  E. b  e.  RR  E. c  e.  RR  E. d  e.  RR  ( a  +  ( _i  x.  b
) )  =/=  (
c  +  ( _i  x.  d ) ) ) )
174, 16mpi 18 . . 3  |-  ( 1  =/=  0  ->  E. a  e.  RR  E. b  e.  RR  E. c  e.  RR  E. d  e.  RR  ( a  +  ( _i  x.  b
) )  =/=  (
c  +  ( _i  x.  d ) ) )
18 ioran 478 . . . . . . . . 9  |-  ( -.  ( a  =/=  c  \/  b  =/=  d
)  <->  ( -.  a  =/=  c  /\  -.  b  =/=  d ) )
19 df-ne 2449 . . . . . . . . . . 11  |-  ( a  =/=  c  <->  -.  a  =  c )
2019con2bii 324 . . . . . . . . . 10  |-  ( a  =  c  <->  -.  a  =/=  c )
21 df-ne 2449 . . . . . . . . . . 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 5827 . . . . . . . . 9  |-  ( b  =  d  ->  (
_i  x.  b )  =  ( _i  x.  d ) )
2725, 26oveqan12d 5838 . . . . . . . 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 2489 . . . . . 6  |-  ( ( a  +  ( _i  x.  b ) )  =/=  ( c  +  ( _i  x.  d
) )  ->  (
a  =/=  c  \/  b  =/=  d ) )
30 neeq1 2455 . . . . . . . . . 10  |-  ( x  =  a  ->  (
x  =/=  y  <->  a  =/=  y ) )
31 neeq2 2456 . . . . . . . . . 10  |-  ( y  =  c  ->  (
a  =/=  y  <->  a  =/=  c ) )
3230, 31rspc2ev 2893 . . . . . . . . 9  |-  ( ( a  e.  RR  /\  c  e.  RR  /\  a  =/=  c )  ->  E. x  e.  RR  E. y  e.  RR  x  =/=  y
)
33323expia 1155 . . . . . . . 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 2455 . . . . . . . . . 10  |-  ( x  =  b  ->  (
x  =/=  y  <->  b  =/=  y ) )
36 neeq2 2456 . . . . . . . . . 10  |-  ( y  =  d  ->  (
b  =/=  y  <->  b  =/=  d ) )
3735, 36rspc2ev 2893 . . . . . . . . 9  |-  ( ( b  e.  RR  /\  d  e.  RR  /\  b  =/=  d )  ->  E. x  e.  RR  E. y  e.  RR  x  =/=  y
)
38373expia 1155 . . . . . . . 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 30 . . . . 5  |-  ( ( ( a  e.  RR  /\  b  e.  RR )  /\  ( c  e.  RR  /\  d  e.  RR ) )  -> 
( ( a  +  ( _i  x.  b
) )  =/=  (
c  +  ( _i  x.  d ) )  ->  E. x  e.  RR  E. y  e.  RR  x  =/=  y ) )
4241rexlimdvva 2675 . . . 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 2673 . . 3  |-  ( E. a  e.  RR  E. b  e.  RR  E. c  e.  RR  E. d  e.  RR  ( a  +  ( _i  x.  b
) )  =/=  (
c  +  ( _i  x.  d ) )  ->  E. x  e.  RR  E. y  e.  RR  x  =/=  y )
441, 17, 43mp2b 11 . 2  |-  E. x  e.  RR  E. y  e.  RR  x  =/=  y
45 eqtr3 2303 . . . . . . . . 9  |-  ( ( x  =  0  /\  y  =  0 )  ->  x  =  y )
4645ex 425 . . . . . . . 8  |-  ( x  =  0  ->  (
y  =  0  ->  x  =  y )
)
4746necon3d 2485 . . . . . . 7  |-  ( x  =  0  ->  (
x  =/=  y  -> 
y  =/=  0 ) )
48 neeq1 2455 . . . . . . . . 9  |-  ( z  =  y  ->  (
z  =/=  0  <->  y  =/=  0 ) )
4948rspcev 2885 . . . . . . . 8  |-  ( ( y  e.  RR  /\  y  =/=  0 )  ->  E. z  e.  RR  z  =/=  0 )
5049expcom 426 . . . . . . 7  |-  ( y  =/=  0  ->  (
y  e.  RR  ->  E. z  e.  RR  z  =/=  0 ) )
5147, 50syl6 31 . . . . . 6  |-  ( x  =  0  ->  (
x  =/=  y  -> 
( y  e.  RR  ->  E. z  e.  RR  z  =/=  0 ) ) )
5251com23 74 . . . . 5  |-  ( x  =  0  ->  (
y  e.  RR  ->  ( x  =/=  y  ->  E. z  e.  RR  z  =/=  0 ) ) )
5352adantld 455 . . . 4  |-  ( x  =  0  ->  (
( x  e.  RR  /\  y  e.  RR )  ->  ( x  =/=  y  ->  E. z  e.  RR  z  =/=  0
) ) )
54 neeq1 2455 . . . . . . . 8  |-  ( z  =  x  ->  (
z  =/=  0  <->  x  =/=  0 ) )
5554rspcev 2885 . . . . . . 7  |-  ( ( x  e.  RR  /\  x  =/=  0 )  ->  E. z  e.  RR  z  =/=  0 )
5655expcom 426 . . . . . 6  |-  ( x  =/=  0  ->  (
x  e.  RR  ->  E. z  e.  RR  z  =/=  0 ) )
5756adantrd 456 . . . . 5  |-  ( x  =/=  0  ->  (
( x  e.  RR  /\  y  e.  RR )  ->  E. z  e.  RR  z  =/=  0 ) )
5857a1dd 44 . . . 4  |-  ( x  =/=  0  ->  (
( x  e.  RR  /\  y  e.  RR )  ->  ( x  =/=  y  ->  E. z  e.  RR  z  =/=  0
) ) )
5953, 58pm2.61ine 2523 . . 3  |-  ( ( x  e.  RR  /\  y  e.  RR )  ->  ( x  =/=  y  ->  E. z  e.  RR  z  =/=  0 ) )
6059rexlimivv 2673 . 2  |-  ( E. x  e.  RR  E. y  e.  RR  x  =/=  y  ->  E. z  e.  RR  z  =/=  0
)
61 ax-rrecex 8804 . . . 4  |-  ( ( z  e.  RR  /\  z  =/=  0 )  ->  E. x  e.  RR  ( z  x.  x
)  =  1 )
62 remulcl 8817 . . . . . . 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 2344 . . . . . 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 2668 . . . 4  |-  ( ( z  e.  RR  /\  z  =/=  0 )  -> 
( E. x  e.  RR  ( z  x.  x )  =  1  ->  1  e.  RR ) )
6761, 66mpd 16 . . 3  |-  ( ( z  e.  RR  /\  z  =/=  0 )  -> 
1  e.  RR )
6867rexlimiva 2663 . 2  |-  ( E. z  e.  RR  z  =/=  0  ->  1  e.  RR )
6944, 60, 68mp2b 11 1  |-  1  e.  RR
Colors of variables: wff set class
Syntax hints:   -. wn 5    -> wi 6    \/ wo 359    /\ wa 360    = wceq 1624    e. wcel 1685    =/= wne 2447   E.wrex 2545  (class class class)co 5819   CCcc 8730   RRcr 8731   0cc0 8732   1c1 8733   _ici 8734    + caddc 8735    x. cmul 8737
This theorem is referenced by:  0re  8833  peano2re  8980  mul02lem2  8984  addid1  8987  renegcl  9105  peano2rem  9108  0reALT  9138  0lt1  9291  0le1  9292  1le1  9391  eqneg  9475  ltp1  9589  ltm1  9591  recgt0  9595  mulgt1  9610  ltmulgt11  9611  lemulge11  9613  ltrec  9632  reclt1  9646  recgt1  9647  recgt1i  9648  recp1lt1  9649  recreclt  9650  recgt0ii  9657  ledivp1i  9677  ltdivp1i  9678  inelr  9731  cju  9737  nnssre  9745  nnge1  9767  nngt1ne1  9768  nnle1eq1  9769  nngt0  9770  nnnlt1  9771  nnrecre  9777  nnrecgt0  9778  nnsub  9779  2re  9810  3re  9812  4re  9814  5re  9816  6re  9817  7re  9818  8re  9819  9re  9820  10re  9821  2pos  9823  3pos  9825  4pos  9827  5pos  9828  6pos  9829  7pos  9830  8pos  9831  9pos  9832  10pos  9833  1lt2  9881  1lt3  9883  1lt4  9886  1lt5  9890  1lt6  9895  1lt7  9901  1lt8  9908  1lt9  9916  1lt10  9925  1ne2  9926  halflt1  9928  addltmul  9942  nnunb  9956  elnnnn0c  10004  elnnz1  10044  znnnlt1  10045  zltp1le  10062  zleltp1  10063  recnz  10082  gtndiv  10084  suprzcl  10086  uzindOLD  10101  eluzp1m1  10246  eluzp1p1  10248  eluz2b2  10285  zbtwnre  10309  rebtwnz  10310  1rp  10353  qbtwnre  10520  qbtwnxr  10521  xmulid1  10593  xmulid2  10594  xmulm1  10595  x2times  10613  xrub  10624  0elunit  10748  1elunit  10749  lincmb01cmp  10771  iccf1o  10772  xov1plusxeqvd  10774  unitssre  10775  fztpval  10839  fraclt1  10928  fracle1  10929  flbi2  10941  fladdz  10944  flhalf  10948  fldiv  10958  modid  10987  1mod  10990  seqf1olem1  11079  reexpcl  11114  reexpclz  11117  expge0  11132  expge1  11133  expgt1  11134  ltexp2a  11147  expcan  11148  ltexp2  11149  leexp2  11150  leexp2a  11151  leexp2r  11153  nnlesq  11200  bernneq  11221  bernneq2  11222  bernneq3  11223  expnbnd  11224  expnlbnd  11225  expnlbnd2  11226  expmulnbnd  11227  discr1  11231  facwordi  11296  faclbnd3  11299  faclbnd4lem1  11300  faclbnd4lem4  11303  faclbnd6  11306  facavg  11308  fzsdom2  11376  hashfun  11383  crre  11593  remim  11596  cjexp  11629  re1  11633  im1  11634  rei  11635  imi  11636  sqrlem1  11722  sqrlem2  11723  sqrlem3  11724  sqrlem4  11725  sqrlem7  11728  resqrex  11730  sqr1  11751  sqr2gt1lt2  11754  sqrm1  11755  abs1  11776  rddif  11818  absrdbnd  11819  caubnd2  11835  mulcn2  12063  reccn2  12064  rlimo1  12084  rlimno1  12121  iseraltlem2  12149  iseraltlem3  12150  iseralt  12151  o1fsum  12265  abscvgcvg  12271  climcndslem1  12302  climcndslem2  12303  flo1  12307  harmonic  12311  expcnv  12316  geolim  12320  geolim2  12321  georeclim  12322  geo2lim  12325  geomulcvg  12326  geoisumr  12328  geoisum1c  12330  geoihalfsum  12332  efcllem  12353  ere  12364  ege2le3  12365  efgt1  12390  resin4p  12412  recos4p  12413  tanhlt1  12434  tanhbnd  12435  sinbnd  12454  cosbnd  12455  sinbnd2  12456  cosbnd2  12457  ef01bndlem  12458  sin01bnd  12459  cos01bnd  12460  cos1bnd  12461  cos2bnd  12462  sinltx  12463  sin01gt0  12464  cos01gt0  12465  sin02gt0  12466  sincos1sgn  12467  eirrlem  12476  rpnnen2lem2  12488  rpnnen2lem3  12489  rpnnen2lem4  12490  rpnnen2lem9  12495  rpnnen2  12498  rpnnen  12499  ruclem6  12507  ruclem11  12512  ruclem12  12513  nthruz  12524  3dvds  12585  bitsfzolem  12619  bitsfzo  12620  bitsmod  12621  bitscmp  12623  bitsinv1lem  12626  sadcadd  12643  smuval2  12667  isprm3  12761  prmind2  12763  sqnprm  12771  coprm  12773  isprm5  12785  divdenle  12814  zsqrelqelz  12823  phibndlem  12832  fermltl  12846  odzdvds  12854  pythagtriplem3  12865  iserodd  12882  pcmpt  12934  fldivp1  12939  pcfaclem  12940  pockthi  12948  infpn2  12954  prmreclem1  12957  prmreclem5  12961  4sqlem11  12996  4sqlem12  12997  ramub1lem1  13067  2expltfac  13099  resslem  13195  rescbas  13700  rescabs  13704  odubas  14231  lt6abl  15175  pgpfaclem2  15311  abvneg  15593  abvtrivd  15599  xrsmcmn  16391  resubdrg  16417  gzrngunitlem  16430  gzrngunit  16431  znidomb  16509  thlbas  16590  leordtval2  16936  setsmsbas  18015  dscmet  18089  dscopn  18090  nrginvrcnlem  18195  nmoid  18245  idnghm  18246  tgioo  18296  blcvx  18298  xrsmopn  18312  metnrmlem1a  18356  metnrmlem1  18357  iitopon  18377  dfii2  18380  dfii3  18381  dfii5  18383  iicmp  18384  iicon  18385  iirev  18421  iirevcn  18422  iihalf1  18423  iihalf1cn  18424  iihalf2  18425  iihalf2cn  18426  elii1  18427  elii2  18428  iimulcl  18429  iimulcn  18430  icchmeo  18433  icopnfcnv  18434  icopnfhmeo  18435  iccpnfcnv  18436  iccpnfhmeo  18437  xrhmeo  18438  xrhmph  18439  icccvx  18442  evth  18451  xlebnum  18457  lebnumii  18458  htpycc  18472  reparphti  18489  pcoval1  18505  pco0  18506  pco1  18507  pcoval2  18508  pcocn  18509  pcohtpylem  18511  pcopt  18514  pcopt2  18515  pcoass  18516  pcorevlem  18518  pcorev2  18520  pi1xfrcnv  18549  nmhmcn  18595  cncmet  18738  ovolunlem1a  18849  ovoliunlem1  18855  dyadmaxlem  18946  vitalilem1  18957  vitalilem2  18958  vitalilem4  18960  vitalilem5  18961  vitali  18962  mbfneg  18999  i1f1  19039  itg11  19040  i1fsub  19057  itg1sub  19058  mbfi1fseqlem6  19069  itg2const  19089  itg2mulc  19096  itg2monolem1  19099  itg2monolem3  19101  iblcnlem1  19136  i1fibl  19156  itgitg1  19157  dveflem  19320  mvth  19333  dvlipcn  19335  lhop1lem  19354  dvcvx  19361  dvfsumlem1  19367  dvfsumlem2  19368  dvfsumlem3  19369  dvfsumlem4  19370  dvfsum2  19375  ply1remlem  19542  fta1glem2  19546  fta1blem  19548  plyeq0lem  19586  fta1lem  19681  vieta1lem2  19685  aalioulem3  19708  aalioulem4  19709  aalioulem5  19710  aaliou3lem2  19717  aaliou3lem8  19719  ulmbdd  19769  iblulm  19777  radcnvlem1  19783  radcnvlem2  19784  dvradcnv  19791  abelthlem2  19802  abelthlem3  19803  abelthlem5  19805  abelthlem7  19808  abelth  19811  abelth2  19812  reeff1olem  19816  reeff1o  19817  sinhalfpilem  19828  tangtx  19867  sincos4thpi  19875  pige3  19879  coskpi  19882  cosne0  19886  recosf1o  19891  tanregt0  19895  efif1olem3  19900  efif1olem4  19901  loge  19934  rplogcl  19952  logdivlti  19965  logno1  19977  logcnlem4  19986  logf1o2  19991  dvlog2lem  19993  advlog  19995  logtayllem  20000  logtayl  20001  logccv  20004  recxpcl  20016  cxplt  20035  cxple  20036  cxplea  20037  cxpsqrlem  20043  cxpsqr  20044  cxpcn3lem  20081  cxpaddlelem  20085  cxpaddle  20086  loglesqr  20092  ang180lem1  20101  ang180lem2  20102  ang180lem3  20103  isosctrlem1  20112  isosctrlem2  20113  angpined  20121  chordthmlem4  20126  1cubrlem  20131  atanre  20175  asinsin  20182  acosrecl  20193  atandmcj  20199  atancj  20200  atanlogaddlem  20203  atantan  20213  bndatandm  20219  atans2  20221  ressatans  20224  leibpilem2  20231  leibpi  20232  leibpisum  20233  log2tlbnd  20235  birthdaylem3  20242  birthday  20243  rlimcnp  20254  rlimcnp2  20255  efrlim  20258  cxp2limlem  20264  cxp2lim  20265  cxploglim  20266  cxploglim2  20267  divsqrsumlem  20268  divsqrsumo1  20272  cvxcl  20273  scvxcvx  20274  jensenlem2  20276  amgmlem  20278  emcllem2  20284  emcllem4  20286  emcllem6  20288  emcllem7  20289  emre  20293  emgt0  20294  harmonicbnd3  20295  harmonicubnd  20297  harmonicbnd4  20298  fsumharmonic  20299  wilthlem1  20300  wilthlem2  20301  ftalem1  20304  ftalem2  20305  ftalem5  20308  basellem3  20314  basellem9  20320  issqf  20368  cht1  20397  vma1  20398  chp1  20399  ppieq0  20408  ppiltx  20409  mumullem2  20412  fsumfldivdiaglem  20423  ppiublem1  20435  ppiub  20437  chpeq0  20441  chtublem  20444  chtub  20445  chpval2  20451  chpchtsum  20452  chpub  20453  logfacbnd3  20456  logfacrlim  20457  logexprlim  20458  mersenne  20460  perfectlem2  20463  dchrelbas4  20476  dchrinv  20494  dchr1re  20496  bcmono  20510  efexple  20514  bposlem1  20517  bposlem2  20518  bposlem5  20521  bposlem8  20524  lgslem3  20531  lgslem4  20532  lgsvalmod  20548  lgsmod  20554  lgsdir2lem1  20556  lgsdir2lem3  20558  lgsdir2lem4  20559  lgsdir2lem5  20560  lgsdirprm  20562  lgsdir  20563  lgsne0  20566  lgsabs1  20567  lgsdinn0  20573  lgseisen  20586  lgsquadlem2  20588  m1lgs  20595  2sqlem8  20605  chebbnd1lem1  20612  chebbnd1lem2  20613  chebbnd1lem3  20614  chebbnd1  20615  chtppilimlem1  20616  chtppilimlem2  20617  chtppilim  20618  chebbnd2  20620  chto1lb  20621  chpchtlim  20622  chpo1ubb  20624  vmadivsum  20625  vmadivsumb  20626  rplogsumlem1  20627  rplogsumlem2  20628  rpvmasumlem  20630  dchrisumlem3  20634  dchrmusumlema  20636  dchrmusum2  20637  dchrvmasumlem2  20641  dchrvmasumlem3  20642  dchrvmasumiflem1  20644  dchrvmasumiflem2  20645  dchrisum0flblem1  20651  dchrisum0flblem2  20652  dchrisum0fno1  20654  rpvmasum2  20655  dchrisum0re  20656  dchrisum0lema  20657  dchrisum0lem1b  20658  dchrisum0lem1  20659  dchrisum0lem2a  20660  dchrisum0lem2  20661  dchrisum0lem3  20662  rplogsum  20670  dirith2  20671  mudivsum  20673  mulogsumlem  20674  mulogsum  20675  logdivsum  20676  mulog2sumlem1  20677  mulog2sumlem2  20678  vmalogdivsum2  20681  2vmadivsumlem  20683  log2sumbnd  20687  selberglem2  20689  selbergb  20692  selberg2lem  20693  selberg2b  20695  chpdifbndlem1  20696  chpdifbnd  20698  selberg3lem1  20700  selberg3lem2  20701  selberg4lem1  20703  pntrmax  20707  pntrsumo1  20708  pntrsumbnd  20709  selberg34r  20714  selbergsb  20718  pntrlog2bndlem1  20720  pntrlog2bndlem2  20721  pntrlog2bndlem3  20722  pntrlog2bndlem4  20723  pntrlog2bndlem5  20724  pntrlog2bndlem6  20726  pntrlog2bnd  20727  pntpbnd1a  20728  pntpbnd1  20729  pntpbnd2  20730  pntibndlem1  20732  pntibndlem2a  20733  pntibndlem2  20734  pntibndlem3  20735  pntibnd  20736  pntlemd  20737  pntlemc  20738  pntlemb  20740  pntlemg  20741  pntlemr  20745  pntlemf  20748  pntlemk  20749  pntlemo  20750  pntlem3  20752  pntleml  20754  pnt  20757  abvcxp  20758  ostth2lem1  20761  qabvle  20768  padicabvf  20774  padicabvcxp  20775  ostth1  20776  ostth2lem2  20777  ostth2lem3  20778  ostth2lem4  20779  ostth2  20780  ostth3  20781  ostth  20782  ex-dif  20785  ex-in  20787  ex-pss  20790  ex-res  20803  ex-fl  20809  nv1  21234  smcnlem  21262  ipidsq  21278  nmoub3i  21343  nmlno0lem  21363  blocnilem  21374  ipasslem10  21409  ubthlem2  21442  minvecolem4  21451  htthlem  21489  hisubcomi  21675  normlem9  21689  norm-ii-i  21708  bcs2  21753  norm1  21820  nmopub2tALT  22481  nmfnleub2  22498  nmlnop0iALT  22567  nmopun  22586  unopbd  22587  hmopd  22594  nmcexi  22598  nmopadjlem  22661  nmopcoi  22667  nmopcoadji  22673  opsqrlem4  22715  pjnmopi  22720  pjbdlni  22721  stcl  22788  stge0  22796  stle1  22797  hstle1  22798  hstle  22802  hstles  22803  stge1i  22810  stlesi  22813  staddi  22818  stadd3i  22820  strlem1  22822  strlem3a  22824  strlem5  22827  jplem1  22840  cdj1i  23005  addltmulALT  23018  fzsplit3  23023  ballotlem2  23040  ballotlemfc0  23044  ballotlemfcc  23045  ballotlem4  23050  ballotlemi1  23054  ballotlemic  23058  ballotlem1c  23059  ballotlemsgt1  23062  ballotlemsel1i  23064  ballotlemfrcn0  23081  zetacvg  23093  subfacp1lem1  23114  subfacp1lem5  23119  subfacval2  23122  subfaclim  23123  subfacval3  23124  cvxpcon  23177  cvxscon  23178  rescon  23181  iiscon  23187  iillyscon  23188  cvmliftlem2  23221  cvmliftlem8  23227  cvmliftlem13  23231  konigsberg  23315  snmlff  23316  sinccvglem  23409  divelunit  23483  dedekind  23485  relin01  23492  fznatpl1  23496  fz0n  23500  brbtwn2  23940  colinearalglem4  23944  ax5seglem1  23963  ax5seglem2  23964  ax5seglem3  23966  ax5seglem5  23968  ax5seglem6  23969  ax5seglem9  23972  ax5seg  23973  axbtwnid  23974  axpaschlem  23975  axpasch  23976  axlowdimlem3  23979  axlowdimlem6  23982  axlowdimlem7  23983  axlowdimlem10  23986  axlowdimlem16  23992  axlowdimlem17  23993  axlowdim1  23994  axlowdim2  23995  axlowdim  23996  axeuclidlem  23997  axcontlem2  24000  axcontlem4  24002  axcontlem7  24005  bpoly4  24201  cntrset  25001  fnckle  25444  nn0prpwlem  25637  fdc  25854  incsequz  25857  geomcau  25874  totbndbnd  25912  cntotbnd  25919  heiborlem8  25941  bfplem2  25946  bfp  25947  lzenom  26248  rabren3dioph  26297  irrapxlem1  26306  irrapxlem2  26307  irrapxlem4  26309  irrapxlem5  26310  pellexlem2  26314  pellexlem5  26317  pellexlem6  26318  pell1qrge1  26354  pell1qr1  26355  elpell1qr2  26356  pell1qrgaplem  26357  pell14qrgap  26359  pell14qrgapw  26360  pellqrex  26363  pellfundre  26365  pellfundgt1  26367  pellfundlb  26368  pellfundglb  26369  pellfundex  26370  pellfund14gap  26371  pellfundrp  26372  pellfundne1  26373  rmspecsqrnq  26390  rmspecnonsq  26391  rmspecfund  26393  rmspecpos  26400  monotoddzzfi  26426  jm2.17a  26446  rmygeid  26450  acongeq  26469  jm2.23  26488  jm3.1lem2  26510  matbas  26867  lhe4.4ex1a  26945  fmul01  27109  fmuldfeq  27112  fmul01lt1lem1  27113  fmul01lt1lem2  27114  climsuselem1  27132  stoweidlem1  27149  stoweidlem3  27151  stoweidlem5  27153  stoweidlem7  27155  stoweidlem10  27158  stoweidlem11  27159  stoweidlem12  27160  stoweidlem13  27161  stoweidlem14  27162  stoweidlem16  27164  stoweidlem18  27166  stoweidlem19  27167  stoweidlem20  27168  stoweidlem22  27170  stoweidlem24  27172  stoweidlem25  27173  stoweidlem26  27174  stoweidlem28  27176  stoweidlem30  27178  stoweidlem34  27182  stoweidlem36  27184  stoweidlem38  27186  stoweidlem40  27188  stoweidlem41  27189  stoweidlem42  27190  stoweidlem44  27192  stoweidlem45  27193  stoweidlem51  27199  stoweidlem59  27207  stoweidlem60  27208  stoweidlem62  27210  stoweid  27211  wallispilem3  27215  wallispilem4  27216  wallispilem5  27217  wallispi  27218  wallispi2lem1  27219  wallispi2lem2  27220  wallispi2  27221  stirlinglem1  27222  stirlinglem3  27224  stirlinglem5  27226  stirlinglem6  27227  stirlinglem7  27228  stirlinglem8  27229  stirlinglem10  27231  stirlinglem11  27232  stirlinglem12  27233  stirlinglem13  27234  stirlinglem15  27236  reseccl  27483  recsccl  27484  sgn1  27509
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1867  ax-ext 2265  ax-1cn 8790  ax-icn 8791  ax-addcl 8792  ax-mulcl 8794  ax-mulrcl 8795  ax-i2m1 8800  ax-1ne0 8801  ax-rrecex 8804  ax-cnre 8805
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 938  df-tru 1312  df-ex 1530  df-nf 1533  df-sb 1632  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-ne 2449  df-ral 2549  df-rex 2550  df-rab 2553  df-v 2791  df-dif 3156  df-un 3158  df-in 3160  df-ss 3167  df-nul 3457  df-if 3567  df-sn 3647  df-pr 3648  df-op 3650  df-uni 3829  df-br 4025  df-opab 4079  df-xp 4694  df-cnv 4696  df-dm 4698  df-rn 4699  df-res 4700  df-ima 4701  df-fv 5229  df-ov 5822
  Copyright terms: Public domain W3C validator