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

Theorem 1re 9895
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 9850, 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 9861 . . 3 1 ≠ 0
2 ax-1cn 9850 . . . . 5 1 ∈ ℂ
3 cnre 9892 . . . . 5 (1 ∈ ℂ → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)))
42, 3ax-mp 5 . . . 4 𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏))
5 neeq1 2843 . . . . . . . 8 (1 = (𝑎 + (i · 𝑏)) → (1 ≠ 0 ↔ (𝑎 + (i · 𝑏)) ≠ 0))
65biimpcd 237 . . . . . . 7 (1 ≠ 0 → (1 = (𝑎 + (i · 𝑏)) → (𝑎 + (i · 𝑏)) ≠ 0))
7 0cn 9888 . . . . . . . 8 0 ∈ ℂ
8 cnre 9892 . . . . . . . 8 (0 ∈ ℂ → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)))
97, 8ax-mp 5 . . . . . . 7 𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑))
10 neeq2 2844 . . . . . . . . . 10 (0 = (𝑐 + (i · 𝑑)) → ((𝑎 + (i · 𝑏)) ≠ 0 ↔ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
1110biimpcd 237 . . . . . . . . 9 ((𝑎 + (i · 𝑏)) ≠ 0 → (0 = (𝑐 + (i · 𝑑)) → (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
1211reximdv 2998 . . . . . . . 8 ((𝑎 + (i · 𝑏)) ≠ 0 → (∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)) → ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
1312reximdv 2998 . . . . . . 7 ((𝑎 + (i · 𝑏)) ≠ 0 → (∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)) → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
146, 9, 13syl6mpi 64 . . . . . 6 (1 ≠ 0 → (1 = (𝑎 + (i · 𝑏)) → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
1514reximdv 2998 . . . . 5 (1 ≠ 0 → (∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)) → ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
1615reximdv 2998 . . . 4 (1 ≠ 0 → (∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)) → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
174, 16mpi 20 . . 3 (1 ≠ 0 → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)))
18 ioran 509 . . . . . . . . 9 (¬ (𝑎𝑐𝑏𝑑) ↔ (¬ 𝑎𝑐 ∧ ¬ 𝑏𝑑))
19 df-ne 2781 . . . . . . . . . . 11 (𝑎𝑐 ↔ ¬ 𝑎 = 𝑐)
2019con2bii 345 . . . . . . . . . 10 (𝑎 = 𝑐 ↔ ¬ 𝑎𝑐)
21 df-ne 2781 . . . . . . . . . . 11 (𝑏𝑑 ↔ ¬ 𝑏 = 𝑑)
2221con2bii 345 . . . . . . . . . 10 (𝑏 = 𝑑 ↔ ¬ 𝑏𝑑)
2320, 22anbi12i 728 . . . . . . . . 9 ((𝑎 = 𝑐𝑏 = 𝑑) ↔ (¬ 𝑎𝑐 ∧ ¬ 𝑏𝑑))
2418, 23bitr4i 265 . . . . . . . 8 (¬ (𝑎𝑐𝑏𝑑) ↔ (𝑎 = 𝑐𝑏 = 𝑑))
25 id 22 . . . . . . . . 9 (𝑎 = 𝑐𝑎 = 𝑐)
26 oveq2 6535 . . . . . . . . 9 (𝑏 = 𝑑 → (i · 𝑏) = (i · 𝑑))
2725, 26oveqan12d 6546 . . . . . . . 8 ((𝑎 = 𝑐𝑏 = 𝑑) → (𝑎 + (i · 𝑏)) = (𝑐 + (i · 𝑑)))
2824, 27sylbi 205 . . . . . . 7 (¬ (𝑎𝑐𝑏𝑑) → (𝑎 + (i · 𝑏)) = (𝑐 + (i · 𝑑)))
2928necon1ai 2808 . . . . . 6 ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → (𝑎𝑐𝑏𝑑))
30 neeq1 2843 . . . . . . . . . 10 (𝑥 = 𝑎 → (𝑥𝑦𝑎𝑦))
31 neeq2 2844 . . . . . . . . . 10 (𝑦 = 𝑐 → (𝑎𝑦𝑎𝑐))
3230, 31rspc2ev 3294 . . . . . . . . 9 ((𝑎 ∈ ℝ ∧ 𝑐 ∈ ℝ ∧ 𝑎𝑐) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥𝑦)
33323expia 1258 . . . . . . . 8 ((𝑎 ∈ ℝ ∧ 𝑐 ∈ ℝ) → (𝑎𝑐 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥𝑦))
3433ad2ant2r 778 . . . . . . 7 (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → (𝑎𝑐 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥𝑦))
35 neeq1 2843 . . . . . . . . . 10 (𝑥 = 𝑏 → (𝑥𝑦𝑏𝑦))
36 neeq2 2844 . . . . . . . . . 10 (𝑦 = 𝑑 → (𝑏𝑦𝑏𝑑))
3735, 36rspc2ev 3294 . . . . . . . . 9 ((𝑏 ∈ ℝ ∧ 𝑑 ∈ ℝ ∧ 𝑏𝑑) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥𝑦)
38373expia 1258 . . . . . . . 8 ((𝑏 ∈ ℝ ∧ 𝑑 ∈ ℝ) → (𝑏𝑑 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥𝑦))
3938ad2ant2l 777 . . . . . . 7 (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → (𝑏𝑑 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥𝑦))
4034, 39jaod 393 . . . . . 6 (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → ((𝑎𝑐𝑏𝑑) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥𝑦))
4129, 40syl5 33 . . . . 5 (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥𝑦))
4241rexlimdvva 3019 . . . 4 ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥𝑦))
4342rexlimivv 3017 . . 3 (∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥𝑦)
441, 17, 43mp2b 10 . 2 𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥𝑦
45 eqtr3 2630 . . . . . . . . 9 ((𝑥 = 0 ∧ 𝑦 = 0) → 𝑥 = 𝑦)
4645ex 448 . . . . . . . 8 (𝑥 = 0 → (𝑦 = 0 → 𝑥 = 𝑦))
4746necon3d 2802 . . . . . . 7 (𝑥 = 0 → (𝑥𝑦𝑦 ≠ 0))
48 neeq1 2843 . . . . . . . . 9 (𝑧 = 𝑦 → (𝑧 ≠ 0 ↔ 𝑦 ≠ 0))
4948rspcev 3281 . . . . . . . 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 2843 . . . . . . . 8 (𝑧 = 𝑥 → (𝑧 ≠ 0 ↔ 𝑥 ≠ 0))
5554rspcev 3281 . . . . . . 7 ((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)
5655expcom 449 . . . . . 6 (𝑥 ≠ 0 → (𝑥 ∈ ℝ → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
5756adantrd 482 . . . . 5 (𝑥 ≠ 0 → ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
5857a1dd 47 . . . 4 (𝑥 ≠ 0 → ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
5953, 58pm2.61ine 2864 . . 3 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
6059rexlimivv 3017 . 2 (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)
61 ax-rrecex 9864 . . . 4 ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → ∃𝑥 ∈ ℝ (𝑧 · 𝑥) = 1)
62 remulcl 9877 . . . . . . 7 ((𝑧 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (𝑧 · 𝑥) ∈ ℝ)
6362adantlr 746 . . . . . 6 (((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) ∧ 𝑥 ∈ ℝ) → (𝑧 · 𝑥) ∈ ℝ)
64 eleq1 2675 . . . . . 6 ((𝑧 · 𝑥) = 1 → ((𝑧 · 𝑥) ∈ ℝ ↔ 1 ∈ ℝ))
6563, 64syl5ibcom 233 . . . . 5 (((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) ∧ 𝑥 ∈ ℝ) → ((𝑧 · 𝑥) = 1 → 1 ∈ ℝ))
6665rexlimdva 3012 . . . 4 ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → (∃𝑥 ∈ ℝ (𝑧 · 𝑥) = 1 → 1 ∈ ℝ))
6761, 66mpd 15 . . 3 ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → 1 ∈ ℝ)
6867rexlimiva 3009 . 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 1976  wne 2779  wrex 2896  (class class class)co 6527  cc 9790  cr 9791  0cc0 9792  1c1 9793  ici 9794   + caddc 9795   · cmul 9797
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-1cn 9850  ax-icn 9851  ax-addcl 9852  ax-mulcl 9854  ax-mulrcl 9855  ax-i2m1 9860  ax-1ne0 9861  ax-rrecex 9864  ax-cnre 9865
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 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-ral 2900  df-rex 2901  df-rab 2904  df-v 3174  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-sn 4125  df-pr 4127  df-op 4131  df-uni 4367  df-br 4578  df-iota 5754  df-fv 5798  df-ov 6530
This theorem is referenced by:  0re  9896  1red  9911  dedekind  10051  peano2re  10060  mul02lem2  10064  addid1  10067  renegcl  10195  peano2rem  10199  0reALT  10229  0lt1  10399  0le1  10400  relin01  10401  1le1  10504  eqneg  10594  ltp1  10710  ltm1  10712  recgt0  10716  mulgt1  10731  ltmulgt11  10732  lemulge11  10734  reclt1  10767  recgt1  10768  recgt1i  10769  recp1lt1  10770  recreclt  10771  recgt0ii  10778  ledivp1i  10798  ltdivp1i  10799  inelr  10857  cju  10863  nnssre  10871  nnge1  10893  nngt1ne1  10894  nnle1eq1  10895  nngt0  10896  nnnlt1  10897  nnrecre  10904  nnrecgt0  10905  nnsub  10906  2re  10937  3re  10941  4re  10944  5re  10946  6re  10948  7re  10950  8re  10952  9re  10954  10reOLD  10956  0le2  10958  2pos  10959  3pos  10961  4pos  10963  5pos  10965  6pos  10966  7pos  10967  8pos  10968  9pos  10969  10posOLD  10970  neg1rr  10972  neg1lt0  10974  1lt2  11041  1lt3  11043  1lt4  11046  1lt5  11050  1lt6  11055  1lt7  11061  1lt8  11068  1lt9  11076  1lt10OLD  11085  1ne2  11087  1le2  11088  1le3  11091  halflt1  11097  addltmul  11115  nnunb  11135  elnnnn0c  11185  nn0ge2m1nn  11207  elnnz1  11236  znnnlt1  11237  zltp1le  11260  zleltp1  11261  nn0lt2  11273  recnz  11284  gtndiv  11286  3halfnz  11288  1lt10  11513  eluzp1m1  11543  eluzp1p1  11545  eluz2b2  11593  zbtwnre  11618  rebtwnz  11619  1rp  11668  divlt1lt  11731  divle1le  11732  nnledivrp  11772  qbtwnxr  11864  xmulid1  11938  xmulid2  11939  xmulm1  11940  x2times  11958  xrub  11970  0elunit  12117  1elunit  12118  divelunit  12141  lincmb01cmp  12142  iccf1o  12143  xov1plusxeqvd  12145  unitssre  12146  0nelfz1  12186  fzpreddisj  12215  fznatpl1  12220  fztpval  12227  fraclt1  12420  fracle1  12421  flbi2  12435  ico01fl0  12437  fldiv4p1lem1div2  12453  fldiv4lem1div2  12455  fldiv  12476  modid  12512  1mod  12519  m1modnnsub1  12533  modm1p1mod0  12538  seqf1olem1  12657  reexpcl  12694  reexpclz  12697  expge0  12713  expge1  12714  expgt1  12715  bernneq  12807  bernneq2  12808  expnbnd  12810  expnlbnd  12811  expnlbnd2  12812  expmulnbnd  12813  discr1  12817  facwordi  12893  faclbnd3  12896  faclbnd4lem1  12897  faclbnd4lem4  12900  faclbnd6  12903  facavg  12905  hashv01gt1  12947  hashge1  12991  hashnn0n0nn  12993  hash1snb  13020  hashgt12el  13022  hashgt12el2  13023  hashfun  13036  hashge2el2dif  13067  brfi1indALT  13083  brfi1indALTOLD  13089  lsw0  13151  f1oun2prg  13458  sgn1  13626  cjexp  13684  re1  13688  im1  13689  rei  13690  imi  13691  sqrlem1  13777  sqrlem2  13778  sqrlem3  13779  sqrlem4  13780  sqrlem7  13783  resqrex  13785  sqrt1  13806  sqrt2gt1lt2  13809  sqrtm1  13810  abs1  13831  absrdbnd  13875  caubnd2  13891  mulcn2  14120  reccn2  14121  rlimno1  14178  o1fsum  14332  expcnv  14381  geolim  14386  geolim2  14387  georeclim  14388  geomulcvg  14392  geoisumr  14394  geoisum1c  14396  geoihalfsum  14399  fprodreclf  14474  fprodge0  14509  fprodge1  14511  rerisefaccl  14533  refallfaccl  14534  ere  14604  ege2le3  14605  efgt1  14631  resin4p  14653  recos4p  14654  tanhbnd  14676  sinbnd  14695  cosbnd  14696  sinbnd2  14697  cosbnd2  14698  ef01bndlem  14699  sin01bnd  14700  cos01bnd  14701  cos1bnd  14702  cos2bnd  14703  sinltx  14704  sin01gt0  14705  cos01gt0  14706  sin02gt0  14707  sincos1sgn  14708  ene1  14723  rpnnen2lem2  14729  rpnnen2lem3  14730  rpnnen2lem4  14731  rpnnen2lem9  14736  rpnnen2lem12  14739  ruclem6  14749  ruclem11  14754  ruclem12  14755  3dvds  14836  3dvdsOLD  14837  halfleoddlt  14870  n2dvds1  14888  flodddiv4  14921  sadcadd  14964  isprm3  15180  sqnprm  15198  coprm  15207  phibndlem  15259  pythagtriplem3  15307  pcmpt  15380  fldivp1  15385  pockthi  15395  infpn2  15401  resslem  15706  slotsbhcdif  15849  oppcbas  16147  rescbas  16258  rescabs  16262  odubas  16902  lt6abl  18065  srgbinomlem4  18312  abvneg  18603  abvtrivd  18609  isnzr2hash  19031  0ringnnzr  19036  xrsmcmn  19534  xrsnsgrp  19547  gzrngunitlem  19576  gzrngunit  19577  rge0srg  19582  psgnodpmr  19700  remulg  19717  resubdrg  19718  thlbas  19801  matbas  19980  leordtval2  20768  tuslem  21823  setsmsbas  22031  dscmet  22128  dscopn  22129  nrginvrcnlem  22238  nmoid  22288  idnghm  22289  tgioo  22339  blcvx  22341  metnrmlem1a  22400  metnrmlem1  22401  iicmp  22428  iicon  22429  iirev  22467  iihalf1  22469  iihalf2  22471  iihalf2cn  22472  elii1  22473  elii2  22474  iimulcl  22475  icopnfcnv  22480  icopnfhmeo  22481  iccpnfcnv  22482  iccpnfhmeo  22483  xrhmeo  22484  xrhmph  22485  evth  22497  xlebnum  22503  lebnumii  22504  htpycc  22518  reparphti  22536  pcoval1  22552  pco1  22554  pcoval2  22555  pcocn  22556  pcohtpylem  22558  pcopt  22561  pcopt2  22562  pcoass  22563  pcorevlem  22565  nmhmcn  22659  ncvs1  22691  ovolunlem1a  22988  vitalilem2  23101  vitalilem4  23103  vitalilem5  23104  vitali  23105  i1f1  23180  itg11  23181  itg2const  23230  itg2monolem1  23240  itg2monolem3  23242  dveflem  23463  dvlipcn  23478  dvcvx  23504  ply1remlem  23643  fta1blem  23649  vieta1lem2  23787  aalioulem3  23810  aalioulem5  23812  aaliou3lem2  23819  ulmbdd  23873  iblulm  23882  radcnvlem1  23888  dvradcnv  23896  abelthlem2  23907  abelthlem3  23908  abelthlem5  23910  abelthlem7  23913  abelth  23916  abelth2  23917  reeff1olem  23921  reeff1o  23922  sinhalfpilem  23936  tangtx  23978  sincos4thpi  23986  pige3  23990  coskpi  23993  recosf1o  24002  tanregt0  24006  efif1olem3  24011  efif1olem4  24012  loge  24054  logdivlti  24087  logcnlem4  24108  logf1o2  24113  dvlog2lem  24115  logtayl  24123  logccv  24126  recxpcl  24138  cxplea  24159  cxpcn3lem  24205  cxpaddlelem  24209  loglesqrt  24216  logblog  24247  ang180lem2  24257  angpined  24274  chordthmlem4  24279  acosrecl  24347  atancj  24354  atanlogaddlem  24357  atantan  24367  atans2  24375  ressatans  24378  leibpi  24386  log2le1  24394  birthdaylem3  24397  cxp2lim  24420  cxploglim  24421  cxploglim2  24422  divsqrtsumlem  24423  cvxcl  24428  scvxcvx  24429  jensenlem2  24431  amgmlem  24433  emcllem2  24440  emcllem4  24442  emcllem6  24444  emcllem7  24445  emre  24449  emgt0  24450  harmonicbnd3  24451  harmonicubnd  24453  harmonicbnd4  24454  zetacvg  24458  lgamgulmlem2  24473  ftalem1  24516  ftalem2  24517  ftalem5  24520  issqf  24579  cht1  24608  chp1  24610  ppiltx  24620  mumullem2  24623  ppiublem1  24644  ppiub  24646  chtublem  24653  chtub  24654  logfacbnd3  24665  logexprlim  24667  perfectlem2  24672  dchrinv  24703  dchr1re  24705  efexple  24723  bposlem1  24726  bposlem2  24727  bposlem5  24730  bposlem8  24733  lgsdir2lem1  24767  lgsdir2lem5  24771  lgsdir  24774  lgsne0  24777  lgsabs1  24778  lgsdinn0  24787  gausslemma2dlem0i  24806  lgseisen  24821  m1lgs  24830  2lgslem3  24846  chebbnd1lem3  24877  chebbnd1  24878  chtppilimlem1  24879  chtppilimlem2  24880  chtppilim  24881  chpchtlim  24885  vmadivsumb  24889  rplogsumlem2  24891  rpvmasumlem  24893  dchrmusumlema  24899  dchrmusum2  24900  dchrvmasumlem2  24904  dchrvmasumiflem1  24907  dchrisum0flblem1  24914  dchrisum0flblem2  24915  dchrisum0fno1  24917  rpvmasum2  24918  dchrisum0re  24919  dchrisum0lema  24920  dchrisum0lem1b  24921  dchrisum0lem1  24922  dchrisum0lem2a  24923  dchrisum0lem2  24924  logdivsum  24939  mulog2sumlem2  24941  2vmadivsumlem  24946  log2sumbnd  24950  selbergb  24955  selberg2b  24958  chpdifbndlem1  24959  selberg3lem1  24963  selberg3lem2  24964  selberg4lem1  24966  pntrmax  24970  pntrsumo1  24971  selbergsb  24981  pntrlog2bndlem3  24985  pntrlog2bndlem5  24987  pntpbnd1a  24991  pntpbnd2  24993  pntibndlem1  24995  pntibndlem2  24997  pntibndlem3  24998  pntibnd  24999  pntlemd  25000  pntlemc  25001  pntlemb  25003  pntlemr  25008  pntlemf  25011  pntlemk  25012  pntlemo  25013  pntlem3  25015  pntleml  25017  pnt  25020  abvcxp  25021  ostth2lem1  25024  padicabvf  25037  padicabvcxp  25038  ostth1  25039  ostth2lem2  25040  ostth2lem3  25041  ostth2lem4  25042  ostth2  25043  ostth3  25044  ostth  25045  trgcgrg  25128  ttgcontlem1  25483  brbtwn2  25503  colinearalglem4  25507  ax5seglem1  25526  ax5seglem2  25527  ax5seglem3  25529  ax5seglem5  25531  ax5seglem6  25532  ax5seglem9  25535  ax5seg  25536  axbtwnid  25537  axpaschlem  25538  axpasch  25539  axlowdimlem6  25545  axlowdimlem10  25549  axlowdimlem16  25555  axlowdim1  25557  axlowdim2  25558  axlowdim  25559  axcontlem2  25563  axcontlem4  25565  axcontlem7  25568  usgraex1elv  25691  usgraexmpldifpr  25694  spthispth  25869  constr3lem4  25941  constr3pthlem1  25949  konigsberg  26280  frgrawopreglem2  26338  frgrareg  26410  ex-dif  26438  ex-in  26440  ex-pss  26443  ex-res  26456  ex-fl  26462  nv1  26709  smcnlem  26737  ipidsq  26753  nmlno0lem  26838  norm-ii-i  27184  bcs2  27229  norm1  27296  nmopub2tALT  27958  nmfnleub2  27975  nmlnop0iALT  28044  nmopun  28063  unopbd  28064  nmopadjlem  28138  nmopcoadji  28150  pjnmopi  28197  pjbdlni  28198  stge0  28273  stle1  28274  hstle1  28275  hstle  28279  hstles  28280  stge1i  28287  stlesi  28290  staddi  28295  stadd3i  28297  strlem1  28299  strlem3a  28301  strlem5  28304  jplem1  28317  cdj1i  28482  addltmulALT  28495  xlt2addrd  28719  xdivrec  28772  xrsmulgzz  28815  xrnarchi  28875  resvbas  28969  rearchi  28979  xrge0slmod  28981  submateqlem1  29007  elunitrn  29077  elunitge0  29079  unitssxrge0  29080  unitdivcld  29081  xrge0iifcnv  29113  xrge0iifcv  29114  xrge0iifiso  29115  xrge0iifhom  29117  zrhre  29197  indf  29211  indfval  29212  pr01ssre  29213  esumcst  29258  hasheuni  29280  cntnevol  29424  ddemeas  29432  omssubadd  29495  iwrdsplit  29582  prob01  29608  dstfrvclim1  29672  coinfliprv  29677  ballotlem2  29683  ballotlem4  29693  ballotlemi1  29697  ballotlemic  29701  sgnclre  29734  sgnnbi  29740  sgnpbi  29741  sgnmulsgp  29745  plymulx0  29756  plymulx  29757  signswch  29770  signstf  29775  signsvfn  29791  subfacp1lem1  30221  subfacp1lem5  30226  rescon  30288  iiscon  30294  iillyscon  30295  snmlff  30371  problem2  30619  problem2OLD  30620  problem3  30621  sinccvglem  30626  fz0n  30675  dnizeq0  31441  dnibndlem12  31455  knoppcnlem4  31462  knoppndvlem13  31491  cnndvlem1  31504  relowlpssretop  32184  sin2h  32365  cos2h  32366  tan2h  32367  poimirlem7  32382  poimirlem16  32391  poimirlem17  32392  poimirlem19  32394  poimirlem20  32395  poimirlem22  32397  poimirlem23  32398  poimirlem29  32404  poimirlem30  32405  poimirlem31  32406  poimirlem32  32407  broucube  32409  itg2addnclem3  32429  asindmre  32461  dvasin  32462  dvacos  32463  dvreasin  32464  dvreacos  32465  areacirclem1  32466  fdc  32507  geomcau  32521  cntotbnd  32561  heiborlem8  32583  bfplem2  32588  bfp  32589  rabren3dioph  36193  pellexlem5  36211  pellexlem6  36212  pell1qrgaplem  36251  pell14qrgap  36253  pellqrex  36257  pellfundre  36259  pellfundlb  36262  pellfund14gap  36265  rmspecsqrtnqOLD  36285  jm2.17a  36341  acongeq  36364  jm2.23  36377  jm3.1lem2  36399  relexp01min  36820  imo72b2  37293  cvgdvgrat  37330  lhe4.4ex1a  37346  binomcxplemnotnn0  37373  isosctrlem1ALT  37988  supxrgelem  38291  xrlexaddrp  38306  infxr  38321  infleinflem2  38325  sumnnodd  38494  dvnprodlem3  38635  stoweidlem1  38691  stoweidlem18  38708  stoweidlem19  38709  stoweidlem26  38716  stoweidlem34  38724  stoweidlem40  38730  stoweidlem41  38731  stoweidlem59  38749  stoweid  38753  stirlinglem10  38773  stirlinglem11  38774  dirkercncflem1  38793  fourierdlem16  38813  fourierdlem21  38818  fourierdlem22  38819  fourierdlem42  38839  fourierdlem68  38864  fourierdlem83  38879  fourierdlem103  38899  sqwvfourb  38919  fouriersw  38921  etransclem23  38947  salexct2  39030  salgencntex  39034  ovn0lem  39252  smfmullem3  39475  smfmullem4  39476  m1mod0mod1  39747  fmtnosqrt  39787  perfectALTVlem2  39963  nnsum3primesprm  40004  nnsum4primesodd  40010  nnsum4primesoddALTV  40011  nnsum4primeseven  40014  nnsum4primesevenALTV  40015  tgblthelfgott  40027  tgoldbach  40030  tgblthelfgottOLD  40034  tgoldbachOLD  40037  zm1nn  40168  lfgrnloop  40345  lfuhgr1v0e  40475  1loopgrvd2  40713  vdegp1bi-av  40748  lfgrwlkprop  40891  pthdlem1  40967  pthdlem2  40969  upgr4cycl4dv4e  41347  konigsberglem2  41418  konigsberglem3  41419  konigsberglem5  41421  frgrwopreglem2  41477  av-frgrareg  41543  basendxnmulrndx  41739  expnegico01  42097  regt1loggt0  42123  rege1logbrege0  42145  rege1logbzge0  42146  blennnelnn  42163  dignnld  42190  nn0sumshdiglemA  42206  nn0sumshdiglem1  42208
  Copyright terms: Public domain W3C validator