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

Theorem 1re 9727
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 9682, 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 ∈ ℝ

Proof of Theorem 1re
Dummy variables 𝑎 𝑏 𝑐 𝑑 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ax-1ne0 9693 . . 3 1 ≠ 0
2 ax-1cn 9682 . . . . 5 1 ∈ ℂ
3 cnre 9724 . . . . 5 (1 ∈ ℂ → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)))
42, 3ax-mp 5 . . . 4 𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏))
5 neeq1 2739 . . . . . . . 8 (1 = (𝑎 + (i · 𝑏)) → (1 ≠ 0 ↔ (𝑎 + (i · 𝑏)) ≠ 0))
65biimpcd 234 . . . . . . 7 (1 ≠ 0 → (1 = (𝑎 + (i · 𝑏)) → (𝑎 + (i · 𝑏)) ≠ 0))
7 0cn 9720 . . . . . . . 8 0 ∈ ℂ
8 cnre 9724 . . . . . . . 8 (0 ∈ ℂ → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)))
97, 8ax-mp 5 . . . . . . 7 𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑))
10 neeq2 2740 . . . . . . . . . 10 (0 = (𝑐 + (i · 𝑑)) → ((𝑎 + (i · 𝑏)) ≠ 0 ↔ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
1110biimpcd 234 . . . . . . . . 9 ((𝑎 + (i · 𝑏)) ≠ 0 → (0 = (𝑐 + (i · 𝑑)) → (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
1211reximdv 2892 . . . . . . . 8 ((𝑎 + (i · 𝑏)) ≠ 0 → (∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)) → ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
1312reximdv 2892 . . . . . . 7 ((𝑎 + (i · 𝑏)) ≠ 0 → (∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)) → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
146, 9, 13syl6mpi 64 . . . . . 6 (1 ≠ 0 → (1 = (𝑎 + (i · 𝑏)) → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
1514reximdv 2892 . . . . 5 (1 ≠ 0 → (∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)) → ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
1615reximdv 2892 . . . 4 (1 ≠ 0 → (∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)) → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
174, 16mpi 20 . . 3 (1 ≠ 0 → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)))
18 ioran 504 . . . . . . . . 9 (¬ (𝑎𝑐𝑏𝑑) ↔ (¬ 𝑎𝑐 ∧ ¬ 𝑏𝑑))
19 df-ne 2677 . . . . . . . . . . 11 (𝑎𝑐 ↔ ¬ 𝑎 = 𝑐)
2019con2bii 341 . . . . . . . . . 10 (𝑎 = 𝑐 ↔ ¬ 𝑎𝑐)
21 df-ne 2677 . . . . . . . . . . 11 (𝑏𝑑 ↔ ¬ 𝑏 = 𝑑)
2221con2bii 341 . . . . . . . . . 10 (𝑏 = 𝑑 ↔ ¬ 𝑏𝑑)
2320, 22anbi12i 720 . . . . . . . . 9 ((𝑎 = 𝑐𝑏 = 𝑑) ↔ (¬ 𝑎𝑐 ∧ ¬ 𝑏𝑑))
2418, 23bitr4i 262 . . . . . . . 8 (¬ (𝑎𝑐𝑏𝑑) ↔ (𝑎 = 𝑐𝑏 = 𝑑))
25 id 22 . . . . . . . . 9 (𝑎 = 𝑐𝑎 = 𝑐)
26 oveq2 6371 . . . . . . . . 9 (𝑏 = 𝑑 → (i · 𝑏) = (i · 𝑑))
2725, 26oveqan12d 6382 . . . . . . . 8 ((𝑎 = 𝑐𝑏 = 𝑑) → (𝑎 + (i · 𝑏)) = (𝑐 + (i · 𝑑)))
2824, 27sylbi 202 . . . . . . 7 (¬ (𝑎𝑐𝑏𝑑) → (𝑎 + (i · 𝑏)) = (𝑐 + (i · 𝑑)))
2928necon1ai 2704 . . . . . 6 ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → (𝑎𝑐𝑏𝑑))
30 neeq1 2739 . . . . . . . . . 10 (𝑥 = 𝑎 → (𝑥𝑦𝑎𝑦))
31 neeq2 2740 . . . . . . . . . 10 (𝑦 = 𝑐 → (𝑎𝑦𝑎𝑐))
3230, 31rspc2ev 3184 . . . . . . . . 9 ((𝑎 ∈ ℝ ∧ 𝑐 ∈ ℝ ∧ 𝑎𝑐) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥𝑦)
33323expia 1249 . . . . . . . 8 ((𝑎 ∈ ℝ ∧ 𝑐 ∈ ℝ) → (𝑎𝑐 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥𝑦))
3433ad2ant2r 770 . . . . . . 7 (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → (𝑎𝑐 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥𝑦))
35 neeq1 2739 . . . . . . . . . 10 (𝑥 = 𝑏 → (𝑥𝑦𝑏𝑦))
36 neeq2 2740 . . . . . . . . . 10 (𝑦 = 𝑑 → (𝑏𝑦𝑏𝑑))
3735, 36rspc2ev 3184 . . . . . . . . 9 ((𝑏 ∈ ℝ ∧ 𝑑 ∈ ℝ ∧ 𝑏𝑑) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥𝑦)
38373expia 1249 . . . . . . . 8 ((𝑏 ∈ ℝ ∧ 𝑑 ∈ ℝ) → (𝑏𝑑 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥𝑦))
3938ad2ant2l 769 . . . . . . 7 (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → (𝑏𝑑 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥𝑦))
4034, 39jaod 389 . . . . . 6 (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → ((𝑎𝑐𝑏𝑑) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥𝑦))
4129, 40syl5 33 . . . . 5 (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥𝑦))
4241rexlimdvva 2913 . . . 4 ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥𝑦))
4342rexlimivv 2911 . . 3 (∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥𝑦)
441, 17, 43mp2b 10 . 2 𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥𝑦
45 eqtr3 2526 . . . . . . . . 9 ((𝑥 = 0 ∧ 𝑦 = 0) → 𝑥 = 𝑦)
4645ex 443 . . . . . . . 8 (𝑥 = 0 → (𝑦 = 0 → 𝑥 = 𝑦))
4746necon3d 2698 . . . . . . 7 (𝑥 = 0 → (𝑥𝑦𝑦 ≠ 0))
48 neeq1 2739 . . . . . . . . 9 (𝑧 = 𝑦 → (𝑧 ≠ 0 ↔ 𝑦 ≠ 0))
4948rspcev 3171 . . . . . . . 8 ((𝑦 ∈ ℝ ∧ 𝑦 ≠ 0) → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)
5049expcom 444 . . . . . . 7 (𝑦 ≠ 0 → (𝑦 ∈ ℝ → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
5147, 50syl6 34 . . . . . 6 (𝑥 = 0 → (𝑥𝑦 → (𝑦 ∈ ℝ → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
5251com23 82 . . . . 5 (𝑥 = 0 → (𝑦 ∈ ℝ → (𝑥𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
5352adantld 476 . . . 4 (𝑥 = 0 → ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
54 neeq1 2739 . . . . . . . 8 (𝑧 = 𝑥 → (𝑧 ≠ 0 ↔ 𝑥 ≠ 0))
5554rspcev 3171 . . . . . . 7 ((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)
5655expcom 444 . . . . . 6 (𝑥 ≠ 0 → (𝑥 ∈ ℝ → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
5756adantrd 477 . . . . 5 (𝑥 ≠ 0 → ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
5857a1dd 47 . . . 4 (𝑥 ≠ 0 → ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
5953, 58pm2.61ine 2760 . . 3 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
6059rexlimivv 2911 . 2 (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)
61 ax-rrecex 9696 . . . 4 ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → ∃𝑥 ∈ ℝ (𝑧 · 𝑥) = 1)
62 remulcl 9709 . . . . . . 7 ((𝑧 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (𝑧 · 𝑥) ∈ ℝ)
6362adantlr 738 . . . . . 6 (((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) ∧ 𝑥 ∈ ℝ) → (𝑧 · 𝑥) ∈ ℝ)
64 eleq1 2571 . . . . . 6 ((𝑧 · 𝑥) = 1 → ((𝑧 · 𝑥) ∈ ℝ ↔ 1 ∈ ℝ))
6563, 64syl5ibcom 230 . . . . 5 (((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) ∧ 𝑥 ∈ ℝ) → ((𝑧 · 𝑥) = 1 → 1 ∈ ℝ))
6665rexlimdva 2906 . . . 4 ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → (∃𝑥 ∈ ℝ (𝑧 · 𝑥) = 1 → 1 ∈ ℝ))
6761, 66mpd 15 . . 3 ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → 1 ∈ ℝ)
6867rexlimiva 2903 . 2 (∃𝑧 ∈ ℝ 𝑧 ≠ 0 → 1 ∈ ℝ)
6944, 60, 68mp2b 10 1 1 ∈ ℝ
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wo 377  wa 378   = wceq 1468  wcel 1937  wne 2675  wrex 2792  (class class class)co 6363  cc 9622  cr 9623  0cc0 9624  1c1 9625  ici 9626   + caddc 9627   · cmul 9629
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1698  ax-4 1711  ax-5 1789  ax-6 1836  ax-7 1883  ax-10 1965  ax-11 1970  ax-12 1983  ax-13 2137  ax-ext 2485  ax-1cn 9682  ax-icn 9683  ax-addcl 9684  ax-mulcl 9686  ax-mulrcl 9687  ax-i2m1 9692  ax-1ne0 9693  ax-rrecex 9696  ax-cnre 9697
This theorem depends on definitions:  df-bi 192  df-or 379  df-an 380  df-3an 1023  df-tru 1471  df-ex 1693  df-nf 1697  df-sb 1829  df-clab 2492  df-cleq 2498  df-clel 2501  df-nfc 2635  df-ne 2677  df-ral 2796  df-rex 2797  df-rab 2800  df-v 3068  df-dif 3429  df-un 3431  df-in 3433  df-ss 3440  df-nul 3758  df-if 3909  df-sn 3996  df-pr 3998  df-op 4002  df-uni 4229  df-br 4435  df-iota 5597  df-fv 5641  df-ov 6366
This theorem is referenced by:  0re  9728  1red  9743  dedekind  9882  peano2re  9891  mul02lem2  9895  addid1  9898  renegcl  10024  peano2rem  10028  0reALT  10058  0lt1  10224  0le1  10225  relin01  10226  1le1  10329  eqneg  10416  ltp1  10532  ltm1  10534  recgt0  10538  mulgt1  10553  ltmulgt11  10554  lemulge11  10556  reclt1  10590  recgt1  10591  recgt1i  10592  recp1lt1  10593  recreclt  10594  recgt0ii  10601  ledivp1i  10621  ltdivp1i  10622  inelr  10688  cju  10694  nnssre  10702  nnge1  10724  nngt1ne1  10725  nnle1eq1  10726  nngt0  10727  nnnlt1  10728  nnrecre  10735  nnrecgt0  10736  nnsub  10737  2re  10768  3re  10772  4re  10775  5re  10777  6re  10779  7re  10781  8re  10783  9re  10785  10re  10787  0le2  10789  2pos  10790  3pos  10792  4pos  10794  5pos  10796  6pos  10797  7pos  10798  8pos  10799  9pos  10800  10pos  10801  neg1rr  10803  neg1lt0  10805  1lt2  10866  1lt3  10868  1lt4  10871  1lt5  10875  1lt6  10880  1lt7  10886  1lt8  10893  1lt9  10901  1lt10  10910  1ne2  10912  1le2  10913  1le3  10916  halflt1  10921  addltmul  10938  nnunb  10956  elnnnn0c  11006  nn0ge2m1nn  11025  elnnz1  11054  znnnlt1  11055  zltp1le  11077  zleltp1  11078  nn0lt2  11090  recnz  11101  gtndiv  11103  eluzp1m1  11273  eluzp1p1  11275  eluz2b2  11322  zbtwnre  11353  rebtwnz  11354  1rp  11397  qbtwnxr  11586  xmulid1  11660  xmulid2  11661  xmulm1  11662  x2times  11680  xrub  11692  0elunit  11846  1elunit  11847  divelunit  11870  lincmb01cmp  11871  iccf1o  11872  xov1plusxeqvd  11874  unitssre  11875  0nelfz1  11914  fzpreddisj  11943  fznatpl1  11948  fztpval  11955  fraclt1  12146  fracle1  12147  flbi2  12160  ico01fl0  12161  fldiv  12195  modid  12229  1mod  12237  modm1p1mod0  12250  seqf1olem1  12366  reexpcl  12403  reexpclz  12406  expge0  12422  expge1  12423  expgt1  12424  bernneq  12512  bernneq2  12513  expnbnd  12515  expnlbnd  12516  expnlbnd2  12517  expmulnbnd  12518  discr1  12522  facwordi  12588  faclbnd3  12591  faclbnd4lem1  12592  faclbnd4lem4  12595  faclbnd6  12598  facavg  12600  hashv01gt1  12642  hashge1  12686  hashnn0n0nn  12688  hash1snb  12714  hashgt12el  12716  hashgt12el2  12717  hashfun  12729  hashge2el2dif  12760  brfi1indALT  12776  brfi1indALTOLD  12782  lsw0  12844  f1oun2prg  13150  sgn1  13315  cjexp  13373  re1  13377  im1  13378  rei  13379  imi  13380  sqrlem1  13466  sqrlem2  13467  sqrlem3  13468  sqrlem4  13469  sqrlem7  13472  resqrex  13474  sqrt1  13495  sqrt2gt1lt2  13498  sqrtm1  13499  abs1  13520  absrdbnd  13564  caubnd2  13580  mulcn2  13819  reccn2  13820  rlimno1  13877  o1fsum  14033  expcnv  14082  geolim  14086  geolim2  14087  georeclim  14088  geomulcvg  14092  geoisumr  14094  geoisum1c  14096  geoihalfsum  14098  fprodreclf  14173  fprodge0  14207  fprodge1  14209  rerisefaccl  14230  refallfaccl  14231  ere  14303  ege2le3  14304  efgt1  14330  resin4p  14352  recos4p  14353  tanhbnd  14375  sinbnd  14394  cosbnd  14395  sinbnd2  14396  cosbnd2  14397  ef01bndlem  14398  sin01bnd  14399  cos01bnd  14400  cos1bnd  14401  cos2bnd  14402  sinltx  14403  sin01gt0  14404  cos01gt0  14405  sin02gt0  14406  sincos1sgn  14407  ene1  14422  rpnnen2lem2  14428  rpnnen2lem3  14429  rpnnen2lem4  14430  rpnnen2lem9  14435  rpnnen2  14438  ruclem6  14447  ruclem11  14452  ruclem12  14453  n2dvds1  14514  3dvds  14531  sadcadd  14594  isprm3  14795  sqnprm  14808  coprm  14819  phibndlem  14880  pythagtriplem3  14930  pcmpt  14999  fldivp1  15004  pockthi  15013  infpn2  15019  resslem  15347  slotsbhcdif  15483  oppcbas  15789  rescbas  15900  rescabs  15904  odubas  16544  lt6abl  17690  srgbinomlem4  17936  abvneg  18222  abvtrivd  18228  isnzr2hash  18647  0ringnnzr  18652  xrsmcmn  19149  xrsnsgrp  19162  gzrngunitlem  19190  gzrngunit  19191  rge0srg  19196  psgnodpmr  19316  remulg  19333  resubdrg  19334  thlbas  19417  matbas  19596  leordtval2  20385  tuslem  21440  setsmsbas  21648  dscmet  21745  dscopn  21746  nrginvrcnlem  21851  nmoid  21921  idnghm  21922  tgioo  21972  blcvx  21974  metnrmlem1a  22033  metnrmlem1  22034  metnrmlem1aOLD  22048  metnrmlem1OLD  22049  iicmp  22076  iicon  22077  iirev  22115  iihalf1  22117  iihalf2  22119  iihalf2cn  22120  elii1  22121  elii2  22122  iimulcl  22123  icopnfcnv  22128  icopnfhmeo  22129  iccpnfcnv  22130  iccpnfhmeo  22131  xrhmeo  22132  xrhmph  22133  evth  22145  xlebnum  22154  lebnumii  22155  htpycc  22169  reparphti  22187  pcoval1  22203  pco1  22205  pcoval2  22206  pcocn  22207  pcohtpylem  22209  pcopt  22212  pcopt2  22213  pcoass  22214  pcorevlem  22216  nmhmcn  22293  ovolunlem1a  22608  vitalilem2  22728  vitalilem4  22730  vitalilem5  22731  vitali  22732  i1f1  22809  itg11  22810  itg2const  22859  itg2monolem1  22869  itg2monolem3  22871  dveflem  23092  dvlipcn  23107  dvcvx  23133  ply1remlem  23274  fta1blem  23280  vieta1lem2  23425  aalioulem3  23451  aalioulem5  23453  aaliou3lem2  23460  ulmbdd  23514  iblulm  23523  radcnvlem1  23529  dvradcnv  23537  abelthlem2  23548  abelthlem3  23549  abelthlem5  23551  abelthlem7  23554  abelth  23557  abelth2  23558  reeff1olem  23562  reeff1o  23563  sinhalfpilem  23579  tangtx  23621  sincos4thpi  23629  pige3  23633  coskpi  23636  recosf1o  23645  tanregt0  23649  efif1olem3  23654  efif1olem4  23655  loge  23697  logdivlti  23730  logcnlem4  23751  logf1o2  23756  dvlog2lem  23758  logtayl  23766  logccv  23769  recxpcl  23781  cxplea  23802  cxpcn3lem  23848  cxpaddlelem  23852  loglesqrt  23859  logblog  23890  ang180lem2  23900  angpined  23917  chordthmlem4  23922  acosrecl  23990  atancj  23997  atanlogaddlem  24000  atantan  24010  atans2  24018  ressatans  24021  leibpi  24029  log2le1  24037  birthdaylem3  24040  cxp2lim  24063  cxploglim  24064  cxploglim2  24065  divsqrtsumlem  24066  cvxcl  24071  scvxcvx  24072  jensenlem2  24074  amgmlem  24076  emcllem2  24083  emcllem4  24085  emcllem6  24087  emcllem7  24088  emre  24092  emgt0  24093  harmonicbnd3  24094  harmonicubnd  24096  harmonicbnd4  24097  zetacvg  24101  lgamgulmlem2  24116  ftalem1  24158  ftalem2  24159  ftalem5  24162  ftalem5OLD  24164  issqf  24224  cht1  24253  chp1  24255  ppiltx  24265  mumullem2  24268  ppiublem1  24291  ppiub  24293  chtublem  24300  chtub  24301  logfacbnd3  24312  logexprlim  24314  perfectlem2  24319  dchrinv  24350  dchr1re  24352  efexple  24370  bposlem1  24373  bposlem2  24374  bposlem5  24377  bposlem8  24380  lgsdir2lem1  24412  lgsdir2lem5  24416  lgsdir  24419  lgsne0  24422  lgsabs1  24423  lgsdinn0  24429  lgseisen  24442  m1lgs  24451  chebbnd1lem3  24470  chebbnd1  24471  chtppilimlem1  24472  chtppilimlem2  24473  chtppilim  24474  chpchtlim  24478  vmadivsumb  24482  rplogsumlem2  24484  rpvmasumlem  24486  dchrmusumlema  24492  dchrmusum2  24493  dchrvmasumlem2  24497  dchrvmasumiflem1  24500  dchrisum0flblem1  24507  dchrisum0flblem2  24508  dchrisum0fno1  24510  rpvmasum2  24511  dchrisum0re  24512  dchrisum0lema  24513  dchrisum0lem1b  24514  dchrisum0lem1  24515  dchrisum0lem2a  24516  dchrisum0lem2  24517  logdivsum  24532  mulog2sumlem2  24534  2vmadivsumlem  24539  log2sumbnd  24543  selbergb  24548  selberg2b  24551  chpdifbndlem1  24552  selberg3lem1  24556  selberg3lem2  24557  selberg4lem1  24559  pntrmax  24563  pntrsumo1  24564  selbergsb  24574  pntrlog2bndlem3  24578  pntrlog2bndlem5  24580  pntpbnd1a  24584  pntpbnd2  24586  pntibndlem1  24588  pntibndlem2  24590  pntibndlem3  24591  pntibnd  24592  pntlemd  24593  pntlemc  24594  pntlemb  24596  pntlemr  24601  pntlemf  24604  pntlemk  24605  pntlemo  24606  pntlem3  24608  pntleml  24610  pnt  24613  abvcxp  24614  ostth2lem1  24617  padicabvf  24630  padicabvcxp  24631  ostth1  24632  ostth2lem2  24633  ostth2lem3  24634  ostth2lem4  24635  ostth2  24636  ostth3  24637  ostth  24638  trgcgrg  24721  ttgcontlem1  25076  brbtwn2  25096  colinearalglem4  25100  ax5seglem1  25119  ax5seglem2  25120  ax5seglem3  25122  ax5seglem5  25124  ax5seglem6  25125  ax5seglem9  25128  ax5seg  25129  axbtwnid  25130  axpaschlem  25131  axpasch  25132  axlowdimlem6  25138  axlowdimlem10  25142  axlowdimlem16  25148  axlowdim1  25150  axlowdim2  25151  axlowdim  25152  axcontlem2  25156  axcontlem4  25158  axcontlem7  25161  usgraex1elv  25285  usgraexmpldifpr  25288  spthispth  25464  constr3lem4  25536  constr3pthlem1  25544  konigsberg  25875  frgrawopreglem2  25933  frgrareg  26005  ex-dif  26033  ex-in  26035  ex-pss  26038  ex-res  26051  ex-fl  26057  nv1  26468  smcnlem  26496  ipidsq  26512  nmlno0lem  26597  norm-ii-i  26953  bcs2  26998  norm1  27065  nmopub2tALT  27725  nmfnleub2  27742  nmlnop0iALT  27811  nmopun  27830  unopbd  27831  nmopadjlem  27905  nmopcoadji  27917  pjnmopi  27964  pjbdlni  27965  stge0  28040  stle1  28041  hstle1  28042  hstle  28046  hstles  28047  stge1i  28054  stlesi  28057  staddi  28062  stadd3i  28064  strlem1  28066  strlem3a  28068  strlem5  28071  jplem1  28084  cdj1i  28249  addltmulALT  28262  xlt2addrd  28494  xdivrec  28552  xrsmulgzz  28596  xrnarchi  28656  resvbas  28750  rearchi  28760  xrge0slmod  28762  submateqlem1  28788  elunitrn  28858  elunitge0  28860  unitssxrge0  28861  unitdivcld  28862  xrge0iifcnv  28894  xrge0iifcv  28895  xrge0iifiso  28896  xrge0iifhom  28898  zrhre  28978  indf  28992  indfval  28993  pr01ssre  28994  esumcst  29039  hasheuni  29061  cntnevol  29205  ddemeas  29213  omssubadd  29282  omssubaddOLD  29286  iwrdsplit  29374  prob01  29400  dstfrvclim1  29464  coinfliprv  29469  ballotlem2  29475  ballotlem4  29485  ballotlemi1  29489  ballotlemic  29493  ballotlemi1OLD  29527  ballotlemicOLD  29531  sgnclre  29564  sgnnbi  29570  sgnpbi  29571  sgnmulsgp  29575  plymulx0  29589  plymulx  29590  signswch  29603  signstf  29608  signsvfn  29624  subfacp1lem1  30054  subfacp1lem5  30059  rescon  30121  iiscon  30127  iillyscon  30128  snmlff  30204  problem2  30450  problem3  30451  sinccvglem  30468  fz0n  30516  dnibndlem12  31287  knoppcnlem4  31294  relowlpssretop  31988  sin2h  32168  cos2h  32169  tan2h  32170  poimirlem7  32185  poimirlem16  32194  poimirlem17  32195  poimirlem19  32197  poimirlem20  32198  poimirlem22  32200  poimirlem23  32201  poimirlem29  32207  poimirlem30  32208  poimirlem31  32209  poimirlem32  32210  broucube  32212  itg2addnclem3  32233  asindmre  32265  dvasin  32266  dvacos  32267  dvreasin  32268  dvreacos  32269  areacirclem1  32270  fdc  32311  geomcau  32325  cntotbnd  32365  heiborlem8  32387  bfplem2  32392  bfp  32393  rabren3dioph  35898  pellexlem5  35917  pellexlem6  35918  pell1qrgaplem  35959  pell14qrgap  35961  pellqrex  35966  pellfundre  35969  pellfundlb  35972  pellfund14gap  35975  rmspecsqrtnq  35994  jm2.17a  36050  acongeq  36073  jm2.23  36091  jm3.1lem2  36113  relexp01min  36544  imo72b2  36975  amgmw2d  37007  cvgdvgrat  37019  lhe4.4ex1a  37035  binomcxplemnotnn0  37062  isosctrlem1ALT  37679  supxrgelem  37936  xrlexaddrp  37951  infxr  37966  infleinflem2  37970  sumnnodd  38114  dvnprodlem3  38242  stoweidlem1  38297  stoweidlem18  38314  stoweidlem19  38315  stoweidlem26  38322  stoweidlem34  38331  stoweidlem40  38337  stoweidlem41  38338  stoweidlem59  38356  stoweid  38361  stirlinglem10  38381  stirlinglem11  38382  dirkercncflem1  38401  fourierdlem16  38421  fourierdlem21  38426  fourierdlem22  38427  fourierdlem42  38448  fourierdlem42OLD  38449  fourierdlem68  38474  fourierdlem83  38489  fourierdlem103  38509  sqwvfourb  38529  fouriersw  38531  etransclem23  38558  salexct2  38642  salgencntex  38646  ovn0lem  38850  m1mod0mod1  39243  perfectALTVlem2  39364  nnsum3primesprm  39405  nnsum4primesodd  39411  nnsum4primesoddALTV  39412  nnsum4primeseven  39415  nnsum4primesevenALTV  39416  tgblthelfgott  39428  tgoldbach  39431  zm1nn  39571  lfgrnloop  39750  lfuhgr1v0e  39880  1loopgrvd2  40118  vdegp1bi-av  40153  lfgrwlkprop  40296  pthdlem1  40372  pthdlem2  40374  upgr4cycl4dv4e  40752  konigsberglem2  40823  konigsberglem3  40824  konigsberglem5  40826  frgrwopreglem2  40882  av-frgrareg  40948  basendxnmulrndx  41144  divlt1lt  41499  expnegico01  41504  3halfnz  41506  regt1loggt0  41536  rege1logbrege0  41558  rege1logbzge0  41559  blennnelnn  41576  dignnld  41603  nn0sumshdiglemA  41619  nn0sumshdiglem1  41621
  Copyright terms: Public domain W3C validator