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

Theorem 1re 9793
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 9748, 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 9759 . . 3 1 ≠ 0
2 ax-1cn 9748 . . . . 5 1 ∈ ℂ
3 cnre 9790 . . . . 5 (1 ∈ ℂ → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)))
42, 3ax-mp 5 . . . 4 𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏))
5 neeq1 2748 . . . . . . . 8 (1 = (𝑎 + (i · 𝑏)) → (1 ≠ 0 ↔ (𝑎 + (i · 𝑏)) ≠ 0))
65biimpcd 237 . . . . . . 7 (1 ≠ 0 → (1 = (𝑎 + (i · 𝑏)) → (𝑎 + (i · 𝑏)) ≠ 0))
7 0cn 9786 . . . . . . . 8 0 ∈ ℂ
8 cnre 9790 . . . . . . . 8 (0 ∈ ℂ → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)))
97, 8ax-mp 5 . . . . . . 7 𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑))
10 neeq2 2749 . . . . . . . . . 10 (0 = (𝑐 + (i · 𝑑)) → ((𝑎 + (i · 𝑏)) ≠ 0 ↔ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
1110biimpcd 237 . . . . . . . . 9 ((𝑎 + (i · 𝑏)) ≠ 0 → (0 = (𝑐 + (i · 𝑑)) → (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
1211reximdv 2903 . . . . . . . 8 ((𝑎 + (i · 𝑏)) ≠ 0 → (∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)) → ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
1312reximdv 2903 . . . . . . 7 ((𝑎 + (i · 𝑏)) ≠ 0 → (∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)) → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
146, 9, 13syl6mpi 64 . . . . . 6 (1 ≠ 0 → (1 = (𝑎 + (i · 𝑏)) → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
1514reximdv 2903 . . . . 5 (1 ≠ 0 → (∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)) → ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
1615reximdv 2903 . . . 4 (1 ≠ 0 → (∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)) → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
174, 16mpi 20 . . 3 (1 ≠ 0 → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)))
18 ioran 509 . . . . . . . . 9 (¬ (𝑎𝑐𝑏𝑑) ↔ (¬ 𝑎𝑐 ∧ ¬ 𝑏𝑑))
19 df-ne 2686 . . . . . . . . . . 11 (𝑎𝑐 ↔ ¬ 𝑎 = 𝑐)
2019con2bii 345 . . . . . . . . . 10 (𝑎 = 𝑐 ↔ ¬ 𝑎𝑐)
21 df-ne 2686 . . . . . . . . . . 11 (𝑏𝑑 ↔ ¬ 𝑏 = 𝑑)
2221con2bii 345 . . . . . . . . . 10 (𝑏 = 𝑑 ↔ ¬ 𝑏𝑑)
2320, 22anbi12i 728 . . . . . . . . 9 ((𝑎 = 𝑐𝑏 = 𝑑) ↔ (¬ 𝑎𝑐 ∧ ¬ 𝑏𝑑))
2418, 23bitr4i 265 . . . . . . . 8 (¬ (𝑎𝑐𝑏𝑑) ↔ (𝑎 = 𝑐𝑏 = 𝑑))
25 id 22 . . . . . . . . 9 (𝑎 = 𝑐𝑎 = 𝑐)
26 oveq2 6433 . . . . . . . . 9 (𝑏 = 𝑑 → (i · 𝑏) = (i · 𝑑))
2725, 26oveqan12d 6444 . . . . . . . 8 ((𝑎 = 𝑐𝑏 = 𝑑) → (𝑎 + (i · 𝑏)) = (𝑐 + (i · 𝑑)))
2824, 27sylbi 205 . . . . . . 7 (¬ (𝑎𝑐𝑏𝑑) → (𝑎 + (i · 𝑏)) = (𝑐 + (i · 𝑑)))
2928necon1ai 2713 . . . . . 6 ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → (𝑎𝑐𝑏𝑑))
30 neeq1 2748 . . . . . . . . . 10 (𝑥 = 𝑎 → (𝑥𝑦𝑎𝑦))
31 neeq2 2749 . . . . . . . . . 10 (𝑦 = 𝑐 → (𝑎𝑦𝑎𝑐))
3230, 31rspc2ev 3199 . . . . . . . . 9 ((𝑎 ∈ ℝ ∧ 𝑐 ∈ ℝ ∧ 𝑎𝑐) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥𝑦)
33323expia 1258 . . . . . . . 8 ((𝑎 ∈ ℝ ∧ 𝑐 ∈ ℝ) → (𝑎𝑐 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥𝑦))
3433ad2ant2r 778 . . . . . . 7 (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → (𝑎𝑐 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥𝑦))
35 neeq1 2748 . . . . . . . . . 10 (𝑥 = 𝑏 → (𝑥𝑦𝑏𝑦))
36 neeq2 2749 . . . . . . . . . 10 (𝑦 = 𝑑 → (𝑏𝑦𝑏𝑑))
3735, 36rspc2ev 3199 . . . . . . . . 9 ((𝑏 ∈ ℝ ∧ 𝑑 ∈ ℝ ∧ 𝑏𝑑) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥𝑦)
38373expia 1258 . . . . . . . 8 ((𝑏 ∈ ℝ ∧ 𝑑 ∈ ℝ) → (𝑏𝑑 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥𝑦))
3938ad2ant2l 777 . . . . . . 7 (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → (𝑏𝑑 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥𝑦))
4034, 39jaod 393 . . . . . 6 (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → ((𝑎𝑐𝑏𝑑) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥𝑦))
4129, 40syl5 33 . . . . 5 (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥𝑦))
4241rexlimdvva 2924 . . . 4 ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥𝑦))
4342rexlimivv 2922 . . 3 (∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥𝑦)
441, 17, 43mp2b 10 . 2 𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥𝑦
45 eqtr3 2535 . . . . . . . . 9 ((𝑥 = 0 ∧ 𝑦 = 0) → 𝑥 = 𝑦)
4645ex 448 . . . . . . . 8 (𝑥 = 0 → (𝑦 = 0 → 𝑥 = 𝑦))
4746necon3d 2707 . . . . . . 7 (𝑥 = 0 → (𝑥𝑦𝑦 ≠ 0))
48 neeq1 2748 . . . . . . . . 9 (𝑧 = 𝑦 → (𝑧 ≠ 0 ↔ 𝑦 ≠ 0))
4948rspcev 3186 . . . . . . . 8 ((𝑦 ∈ ℝ ∧ 𝑦 ≠ 0) → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)
5049expcom 449 . . . . . . 7 (𝑦 ≠ 0 → (𝑦 ∈ ℝ → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
5147, 50syl6 34 . . . . . 6 (𝑥 = 0 → (𝑥𝑦 → (𝑦 ∈ ℝ → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
5251com23 83 . . . . 5 (𝑥 = 0 → (𝑦 ∈ ℝ → (𝑥𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
5352adantld 481 . . . 4 (𝑥 = 0 → ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
54 neeq1 2748 . . . . . . . 8 (𝑧 = 𝑥 → (𝑧 ≠ 0 ↔ 𝑥 ≠ 0))
5554rspcev 3186 . . . . . . 7 ((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)
5655expcom 449 . . . . . 6 (𝑥 ≠ 0 → (𝑥 ∈ ℝ → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
5756adantrd 482 . . . . 5 (𝑥 ≠ 0 → ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
5857a1dd 47 . . . 4 (𝑥 ≠ 0 → ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
5953, 58pm2.61ine 2769 . . 3 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
6059rexlimivv 2922 . 2 (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)
61 ax-rrecex 9762 . . . 4 ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → ∃𝑥 ∈ ℝ (𝑧 · 𝑥) = 1)
62 remulcl 9775 . . . . . . 7 ((𝑧 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (𝑧 · 𝑥) ∈ ℝ)
6362adantlr 746 . . . . . 6 (((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) ∧ 𝑥 ∈ ℝ) → (𝑧 · 𝑥) ∈ ℝ)
64 eleq1 2580 . . . . . 6 ((𝑧 · 𝑥) = 1 → ((𝑧 · 𝑥) ∈ ℝ ↔ 1 ∈ ℝ))
6563, 64syl5ibcom 233 . . . . 5 (((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) ∧ 𝑥 ∈ ℝ) → ((𝑧 · 𝑥) = 1 → 1 ∈ ℝ))
6665rexlimdva 2917 . . . 4 ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → (∃𝑥 ∈ ℝ (𝑧 · 𝑥) = 1 → 1 ∈ ℝ))
6761, 66mpd 15 . . 3 ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → 1 ∈ ℝ)
6867rexlimiva 2914 . 2 (∃𝑧 ∈ ℝ 𝑧 ≠ 0 → 1 ∈ ℝ)
6944, 60, 68mp2b 10 1 1 ∈ ℝ
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wo 381  wa 382   = wceq 1474  wcel 1938  wne 2684  wrex 2801  (class class class)co 6425  cc 9688  cr 9689  0cc0 9690  1c1 9691  ici 9692   + caddc 9693   · cmul 9695
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1700  ax-4 1713  ax-5 1793  ax-6 1838  ax-7 1885  ax-10 1966  ax-11 1971  ax-12 1983  ax-13 2137  ax-ext 2494  ax-1cn 9748  ax-icn 9749  ax-addcl 9750  ax-mulcl 9752  ax-mulrcl 9753  ax-i2m1 9758  ax-1ne0 9759  ax-rrecex 9762  ax-cnre 9763
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1699  df-sb 1831  df-clab 2501  df-cleq 2507  df-clel 2510  df-nfc 2644  df-ne 2686  df-ral 2805  df-rex 2806  df-rab 2809  df-v 3079  df-dif 3447  df-un 3449  df-in 3451  df-ss 3458  df-nul 3778  df-if 3940  df-sn 4029  df-pr 4031  df-op 4035  df-uni 4271  df-br 4482  df-iota 5653  df-fv 5697  df-ov 6428
This theorem is referenced by:  0re  9794  1red  9809  dedekind  9950  peano2re  9959  mul02lem2  9963  addid1  9966  renegcl  10094  peano2rem  10098  0reALT  10128  0lt1  10298  0le1  10299  relin01  10300  1le1  10403  eqneg  10493  ltp1  10609  ltm1  10611  recgt0  10615  mulgt1  10630  ltmulgt11  10631  lemulge11  10633  reclt1  10667  recgt1  10668  recgt1i  10669  recp1lt1  10670  recreclt  10671  recgt0ii  10678  ledivp1i  10698  ltdivp1i  10699  inelr  10764  cju  10770  nnssre  10778  nnge1  10800  nngt1ne1  10801  nnle1eq1  10802  nngt0  10803  nnnlt1  10804  nnrecre  10811  nnrecgt0  10812  nnsub  10813  2re  10844  3re  10848  4re  10851  5re  10853  6re  10855  7re  10857  8re  10859  9re  10861  10reOLD  10863  0le2  10865  2pos  10866  3pos  10868  4pos  10870  5pos  10872  6pos  10873  7pos  10874  8pos  10875  9pos  10876  10posOLD  10877  neg1rr  10879  neg1lt0  10881  1lt2  10948  1lt3  10950  1lt4  10953  1lt5  10957  1lt6  10962  1lt7  10968  1lt8  10975  1lt9  10983  1lt10OLD  10992  1ne2  10994  1le2  10995  1le3  10998  halflt1  11004  addltmul  11022  nnunb  11042  elnnnn0c  11092  nn0ge2m1nn  11114  elnnz1  11143  znnnlt1  11144  zltp1le  11167  zleltp1  11168  nn0lt2  11180  recnz  11191  gtndiv  11193  3halfnz  11195  1lt10  11420  eluzp1m1  11450  eluzp1p1  11452  eluz2b2  11500  zbtwnre  11527  rebtwnz  11528  1rp  11577  divlt1lt  11640  divle1le  11641  nnledivrp  11681  qbtwnxr  11773  xmulid1  11847  xmulid2  11848  xmulm1  11849  x2times  11867  xrub  11879  0elunit  12029  1elunit  12030  divelunit  12053  lincmb01cmp  12054  iccf1o  12055  xov1plusxeqvd  12057  unitssre  12058  0nelfz1  12098  fzpreddisj  12127  fznatpl1  12132  fztpval  12139  fraclt1  12332  fracle1  12333  flbi2  12347  ico01fl0  12349  fldiv4p1lem1div2  12365  fldiv4lem1div2  12367  fldiv  12388  modid  12424  1mod  12431  m1modnnsub1  12445  modm1p1mod0  12450  seqf1olem1  12569  reexpcl  12606  reexpclz  12609  expge0  12625  expge1  12626  expgt1  12627  bernneq  12719  bernneq2  12720  expnbnd  12722  expnlbnd  12723  expnlbnd2  12724  expmulnbnd  12725  discr1  12729  facwordi  12805  faclbnd3  12808  faclbnd4lem1  12809  faclbnd4lem4  12812  faclbnd6  12815  facavg  12817  hashv01gt1  12859  hashge1  12903  hashnn0n0nn  12905  hash1snb  12931  hashgt12el  12933  hashgt12el2  12934  hashfun  12947  hashge2el2dif  12978  brfi1indALT  12994  brfi1indALTOLD  13000  lsw0  13062  f1oun2prg  13369  sgn1  13537  cjexp  13595  re1  13599  im1  13600  rei  13601  imi  13602  sqrlem1  13688  sqrlem2  13689  sqrlem3  13690  sqrlem4  13691  sqrlem7  13694  resqrex  13696  sqrt1  13717  sqrt2gt1lt2  13720  sqrtm1  13721  abs1  13742  absrdbnd  13786  caubnd2  13802  mulcn2  14038  reccn2  14039  rlimno1  14096  o1fsum  14253  expcnv  14302  geolim  14307  geolim2  14308  georeclim  14309  geomulcvg  14313  geoisumr  14315  geoisum1c  14317  geoihalfsum  14320  fprodreclf  14395  fprodge0  14430  fprodge1  14432  rerisefaccl  14454  refallfaccl  14455  ere  14525  ege2le3  14526  efgt1  14552  resin4p  14574  recos4p  14575  tanhbnd  14597  sinbnd  14616  cosbnd  14617  sinbnd2  14618  cosbnd2  14619  ef01bndlem  14620  sin01bnd  14621  cos01bnd  14622  cos1bnd  14623  cos2bnd  14624  sinltx  14625  sin01gt0  14626  cos01gt0  14627  sin02gt0  14628  sincos1sgn  14629  ene1  14644  rpnnen2lem2  14650  rpnnen2lem3  14651  rpnnen2lem4  14652  rpnnen2lem9  14657  rpnnen2lem12  14660  ruclem6  14670  ruclem11  14675  ruclem12  14676  3dvds  14757  3dvdsOLD  14758  halfleoddlt  14791  n2dvds1  14809  flodddiv4  14845  sadcadd  14889  isprm3  15108  sqnprm  15126  coprm  15135  phibndlem  15189  pythagtriplem3  15243  pcmpt  15316  fldivp1  15321  pockthi  15331  infpn2  15337  resslem  15642  slotsbhcdif  15785  oppcbas  16091  rescbas  16202  rescabs  16206  odubas  16846  lt6abl  18024  srgbinomlem4  18271  abvneg  18562  abvtrivd  18568  isnzr2hash  18987  0ringnnzr  18992  xrsmcmn  19490  xrsnsgrp  19503  gzrngunitlem  19532  gzrngunit  19533  rge0srg  19538  psgnodpmr  19659  remulg  19676  resubdrg  19677  thlbas  19760  matbas  19939  leordtval2  20727  tuslem  21782  setsmsbas  21990  dscmet  22087  dscopn  22088  nrginvrcnlem  22193  nmoid  22263  idnghm  22264  tgioo  22314  blcvx  22316  metnrmlem1a  22375  metnrmlem1  22376  metnrmlem1aOLD  22390  metnrmlem1OLD  22391  iicmp  22418  iicon  22419  iirev  22457  iihalf1  22459  iihalf2  22461  iihalf2cn  22462  elii1  22463  elii2  22464  iimulcl  22465  icopnfcnv  22470  icopnfhmeo  22471  iccpnfcnv  22472  iccpnfhmeo  22473  xrhmeo  22474  xrhmph  22475  evth  22487  xlebnum  22496  lebnumii  22497  htpycc  22511  reparphti  22529  pcoval1  22545  pco1  22547  pcoval2  22548  pcocn  22549  pcohtpylem  22551  pcopt  22554  pcopt2  22555  pcoass  22556  pcorevlem  22558  nmhmcn  22635  ovolunlem1a  22947  vitalilem2  23060  vitalilem4  23062  vitalilem5  23063  vitali  23064  i1f1  23139  itg11  23140  itg2const  23189  itg2monolem1  23199  itg2monolem3  23201  dveflem  23422  dvlipcn  23437  dvcvx  23463  ply1remlem  23604  fta1blem  23610  vieta1lem2  23755  aalioulem3  23781  aalioulem5  23783  aaliou3lem2  23790  ulmbdd  23844  iblulm  23853  radcnvlem1  23859  dvradcnv  23867  abelthlem2  23878  abelthlem3  23879  abelthlem5  23881  abelthlem7  23884  abelth  23887  abelth2  23888  reeff1olem  23892  reeff1o  23893  sinhalfpilem  23907  tangtx  23949  sincos4thpi  23957  pige3  23961  coskpi  23964  recosf1o  23973  tanregt0  23977  efif1olem3  23982  efif1olem4  23983  loge  24025  logdivlti  24058  logcnlem4  24079  logf1o2  24084  dvlog2lem  24086  logtayl  24094  logccv  24097  recxpcl  24109  cxplea  24130  cxpcn3lem  24176  cxpaddlelem  24180  loglesqrt  24187  logblog  24218  ang180lem2  24228  angpined  24245  chordthmlem4  24250  acosrecl  24318  atancj  24325  atanlogaddlem  24328  atantan  24338  atans2  24346  ressatans  24349  leibpi  24357  log2le1  24365  birthdaylem3  24368  cxp2lim  24391  cxploglim  24392  cxploglim2  24393  divsqrtsumlem  24394  cvxcl  24399  scvxcvx  24400  jensenlem2  24402  amgmlem  24404  emcllem2  24411  emcllem4  24413  emcllem6  24415  emcllem7  24416  emre  24420  emgt0  24421  harmonicbnd3  24422  harmonicubnd  24424  harmonicbnd4  24425  zetacvg  24429  lgamgulmlem2  24444  ftalem1  24487  ftalem2  24488  ftalem5  24491  ftalem5OLD  24493  issqf  24552  cht1  24581  chp1  24583  ppiltx  24593  mumullem2  24596  ppiublem1  24617  ppiub  24619  chtublem  24626  chtub  24627  logfacbnd3  24638  logexprlim  24640  perfectlem2  24645  dchrinv  24676  dchr1re  24678  efexple  24696  bposlem1  24699  bposlem2  24700  bposlem5  24703  bposlem8  24706  lgsdir2lem1  24740  lgsdir2lem5  24744  lgsdir  24747  lgsne0  24750  lgsabs1  24751  lgsdinn0  24760  gausslemma2dlem0i  24779  lgseisen  24794  m1lgs  24803  2lgslem3  24819  chebbnd1lem3  24850  chebbnd1  24851  chtppilimlem1  24852  chtppilimlem2  24853  chtppilim  24854  chpchtlim  24858  vmadivsumb  24862  rplogsumlem2  24864  rpvmasumlem  24866  dchrmusumlema  24872  dchrmusum2  24873  dchrvmasumlem2  24877  dchrvmasumiflem1  24880  dchrisum0flblem1  24887  dchrisum0flblem2  24888  dchrisum0fno1  24890  rpvmasum2  24891  dchrisum0re  24892  dchrisum0lema  24893  dchrisum0lem1b  24894  dchrisum0lem1  24895  dchrisum0lem2a  24896  dchrisum0lem2  24897  logdivsum  24912  mulog2sumlem2  24914  2vmadivsumlem  24919  log2sumbnd  24923  selbergb  24928  selberg2b  24931  chpdifbndlem1  24932  selberg3lem1  24936  selberg3lem2  24937  selberg4lem1  24939  pntrmax  24943  pntrsumo1  24944  selbergsb  24954  pntrlog2bndlem3  24958  pntrlog2bndlem5  24960  pntpbnd1a  24964  pntpbnd2  24966  pntibndlem1  24968  pntibndlem2  24970  pntibndlem3  24971  pntibnd  24972  pntlemd  24973  pntlemc  24974  pntlemb  24976  pntlemr  24981  pntlemf  24984  pntlemk  24985  pntlemo  24986  pntlem3  24988  pntleml  24990  pnt  24993  abvcxp  24994  ostth2lem1  24997  padicabvf  25010  padicabvcxp  25011  ostth1  25012  ostth2lem2  25013  ostth2lem3  25014  ostth2lem4  25015  ostth2  25016  ostth3  25017  ostth  25018  trgcgrg  25101  ttgcontlem1  25456  brbtwn2  25476  colinearalglem4  25480  ax5seglem1  25499  ax5seglem2  25500  ax5seglem3  25502  ax5seglem5  25504  ax5seglem6  25505  ax5seglem9  25508  ax5seg  25509  axbtwnid  25510  axpaschlem  25511  axpasch  25512  axlowdimlem6  25518  axlowdimlem10  25522  axlowdimlem16  25528  axlowdim1  25530  axlowdim2  25531  axlowdim  25532  axcontlem2  25536  axcontlem4  25538  axcontlem7  25541  usgraex1elv  25664  usgraexmpldifpr  25667  spthispth  25842  constr3lem4  25914  constr3pthlem1  25922  konigsberg  26253  frgrawopreglem2  26311  frgrareg  26383  ex-dif  26411  ex-in  26413  ex-pss  26416  ex-res  26429  ex-fl  26435  nv1  26682  smcnlem  26710  ipidsq  26726  nmlno0lem  26811  norm-ii-i  27167  bcs2  27212  norm1  27279  nmopub2tALT  27941  nmfnleub2  27958  nmlnop0iALT  28027  nmopun  28046  unopbd  28047  nmopadjlem  28121  nmopcoadji  28133  pjnmopi  28180  pjbdlni  28181  stge0  28256  stle1  28257  hstle1  28258  hstle  28262  hstles  28263  stge1i  28270  stlesi  28273  staddi  28278  stadd3i  28280  strlem1  28282  strlem3a  28284  strlem5  28287  jplem1  28300  cdj1i  28465  addltmulALT  28478  xlt2addrd  28704  xdivrec  28762  xrsmulgzz  28806  xrnarchi  28866  resvbas  28960  rearchi  28970  xrge0slmod  28972  submateqlem1  28998  elunitrn  29068  elunitge0  29070  unitssxrge0  29071  unitdivcld  29072  xrge0iifcnv  29104  xrge0iifcv  29105  xrge0iifiso  29106  xrge0iifhom  29108  zrhre  29188  indf  29202  indfval  29203  pr01ssre  29204  esumcst  29249  hasheuni  29271  cntnevol  29415  ddemeas  29423  omssubadd  29492  omssubaddOLD  29496  iwrdsplit  29584  prob01  29610  dstfrvclim1  29674  coinfliprv  29679  ballotlem2  29685  ballotlem4  29695  ballotlemi1  29699  ballotlemic  29703  ballotlemi1OLD  29737  ballotlemicOLD  29741  sgnclre  29774  sgnnbi  29780  sgnpbi  29781  sgnmulsgp  29785  plymulx0  29796  plymulx  29797  signswch  29810  signstf  29815  signsvfn  29831  subfacp1lem1  30261  subfacp1lem5  30266  rescon  30328  iiscon  30334  iillyscon  30335  snmlff  30411  problem2  30657  problem2OLD  30658  problem3  30659  sinccvglem  30664  fz0n  30712  dnizeq0  31470  dnibndlem12  31484  knoppcnlem4  31491  knoppndvlem13  31520  cnndvlem1  31533  relowlpssretop  32220  sin2h  32444  cos2h  32445  tan2h  32446  poimirlem7  32461  poimirlem16  32470  poimirlem17  32471  poimirlem19  32473  poimirlem20  32474  poimirlem22  32476  poimirlem23  32477  poimirlem29  32483  poimirlem30  32484  poimirlem31  32485  poimirlem32  32486  broucube  32488  itg2addnclem3  32508  asindmre  32540  dvasin  32541  dvacos  32542  dvreasin  32543  dvreacos  32544  areacirclem1  32545  fdc  32586  geomcau  32600  cntotbnd  32640  heiborlem8  32662  bfplem2  32667  bfp  32668  rabren3dioph  36272  pellexlem5  36290  pellexlem6  36291  pell1qrgaplem  36330  pell14qrgap  36332  pellqrex  36336  pellfundre  36338  pellfundlb  36341  pellfund14gap  36344  rmspecsqrtnqOLD  36364  jm2.17a  36420  acongeq  36443  jm2.23  36456  jm3.1lem2  36478  relexp01min  36906  imo72b2  37379  cvgdvgrat  37416  lhe4.4ex1a  37432  binomcxplemnotnn0  37459  isosctrlem1ALT  38074  supxrgelem  38380  xrlexaddrp  38395  infxr  38410  infleinflem2  38414  sumnnodd  38583  dvnprodlem3  38728  stoweidlem1  38784  stoweidlem18  38801  stoweidlem19  38802  stoweidlem26  38809  stoweidlem34  38817  stoweidlem40  38823  stoweidlem41  38824  stoweidlem59  38842  stoweid  38846  stirlinglem10  38866  stirlinglem11  38867  dirkercncflem1  38886  fourierdlem16  38906  fourierdlem21  38911  fourierdlem22  38912  fourierdlem42  38933  fourierdlem42OLD  38934  fourierdlem68  38959  fourierdlem83  38974  fourierdlem103  38994  sqwvfourb  39014  fouriersw  39016  etransclem23  39043  salexct2  39127  salgencntex  39131  ovn0lem  39349  smfmullem3  39572  smfmullem4  39573  m1mod0mod1  39844  fmtnosqrt  39884  perfectALTVlem2  40060  nnsum3primesprm  40101  nnsum4primesodd  40107  nnsum4primesoddALTV  40108  nnsum4primeseven  40111  nnsum4primesevenALTV  40112  tgblthelfgott  40124  tgoldbach  40127  tgblthelfgottOLD  40131  tgoldbachOLD  40134  zm1nn  40265  lfgrnloop  40442  lfuhgr1v0e  40572  1loopgrvd2  40810  vdegp1bi-av  40845  lfgrwlkprop  40988  pthdlem1  41064  pthdlem2  41066  upgr4cycl4dv4e  41444  konigsberglem2  41515  konigsberglem3  41516  konigsberglem5  41518  frgrwopreglem2  41574  av-frgrareg  41640  basendxnmulrndx  41836  expnegico01  42194  regt1loggt0  42220  rege1logbrege0  42242  rege1logbzge0  42243  blennnelnn  42260  dignnld  42287  nn0sumshdiglemA  42303  nn0sumshdiglem1  42305
  Copyright terms: Public domain W3C validator