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

Theorem 1re 10242
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 10197, 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 10208 . . 3 1 ≠ 0
2 ax-1cn 10197 . . . . 5 1 ∈ ℂ
3 cnre 10239 . . . . 5 (1 ∈ ℂ → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)))
42, 3ax-mp 5 . . . 4 𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏))
5 neeq1 3005 . . . . . . . 8 (1 = (𝑎 + (i · 𝑏)) → (1 ≠ 0 ↔ (𝑎 + (i · 𝑏)) ≠ 0))
65biimpcd 239 . . . . . . 7 (1 ≠ 0 → (1 = (𝑎 + (i · 𝑏)) → (𝑎 + (i · 𝑏)) ≠ 0))
7 0cn 10235 . . . . . . . 8 0 ∈ ℂ
8 cnre 10239 . . . . . . . 8 (0 ∈ ℂ → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)))
97, 8ax-mp 5 . . . . . . 7 𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑))
10 neeq2 3006 . . . . . . . . . 10 (0 = (𝑐 + (i · 𝑑)) → ((𝑎 + (i · 𝑏)) ≠ 0 ↔ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
1110biimpcd 239 . . . . . . . . 9 ((𝑎 + (i · 𝑏)) ≠ 0 → (0 = (𝑐 + (i · 𝑑)) → (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
1211reximdv 3164 . . . . . . . 8 ((𝑎 + (i · 𝑏)) ≠ 0 → (∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)) → ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
1312reximdv 3164 . . . . . . 7 ((𝑎 + (i · 𝑏)) ≠ 0 → (∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)) → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
146, 9, 13syl6mpi 67 . . . . . 6 (1 ≠ 0 → (1 = (𝑎 + (i · 𝑏)) → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
1514reximdv 3164 . . . . 5 (1 ≠ 0 → (∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)) → ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
1615reximdv 3164 . . . 4 (1 ≠ 0 → (∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)) → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
174, 16mpi 20 . . 3 (1 ≠ 0 → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)))
18 ioran 958 . . . . . . . . 9 (¬ (𝑎𝑐𝑏𝑑) ↔ (¬ 𝑎𝑐 ∧ ¬ 𝑏𝑑))
19 df-ne 2944 . . . . . . . . . . 11 (𝑎𝑐 ↔ ¬ 𝑎 = 𝑐)
2019con2bii 346 . . . . . . . . . 10 (𝑎 = 𝑐 ↔ ¬ 𝑎𝑐)
21 df-ne 2944 . . . . . . . . . . 11 (𝑏𝑑 ↔ ¬ 𝑏 = 𝑑)
2221con2bii 346 . . . . . . . . . 10 (𝑏 = 𝑑 ↔ ¬ 𝑏𝑑)
2320, 22anbi12i 606 . . . . . . . . 9 ((𝑎 = 𝑐𝑏 = 𝑑) ↔ (¬ 𝑎𝑐 ∧ ¬ 𝑏𝑑))
2418, 23bitr4i 267 . . . . . . . 8 (¬ (𝑎𝑐𝑏𝑑) ↔ (𝑎 = 𝑐𝑏 = 𝑑))
25 id 22 . . . . . . . . 9 (𝑎 = 𝑐𝑎 = 𝑐)
26 oveq2 6802 . . . . . . . . 9 (𝑏 = 𝑑 → (i · 𝑏) = (i · 𝑑))
2725, 26oveqan12d 6813 . . . . . . . 8 ((𝑎 = 𝑐𝑏 = 𝑑) → (𝑎 + (i · 𝑏)) = (𝑐 + (i · 𝑑)))
2824, 27sylbi 207 . . . . . . 7 (¬ (𝑎𝑐𝑏𝑑) → (𝑎 + (i · 𝑏)) = (𝑐 + (i · 𝑑)))
2928necon1ai 2970 . . . . . 6 ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → (𝑎𝑐𝑏𝑑))
30 neeq1 3005 . . . . . . . . . 10 (𝑥 = 𝑎 → (𝑥𝑦𝑎𝑦))
31 neeq2 3006 . . . . . . . . . 10 (𝑦 = 𝑐 → (𝑎𝑦𝑎𝑐))
3230, 31rspc2ev 3475 . . . . . . . . 9 ((𝑎 ∈ ℝ ∧ 𝑐 ∈ ℝ ∧ 𝑎𝑐) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥𝑦)
33323expia 1114 . . . . . . . 8 ((𝑎 ∈ ℝ ∧ 𝑐 ∈ ℝ) → (𝑎𝑐 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥𝑦))
3433ad2ant2r 735 . . . . . . 7 (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → (𝑎𝑐 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥𝑦))
35 neeq1 3005 . . . . . . . . . 10 (𝑥 = 𝑏 → (𝑥𝑦𝑏𝑦))
36 neeq2 3006 . . . . . . . . . 10 (𝑦 = 𝑑 → (𝑏𝑦𝑏𝑑))
3735, 36rspc2ev 3475 . . . . . . . . 9 ((𝑏 ∈ ℝ ∧ 𝑑 ∈ ℝ ∧ 𝑏𝑑) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥𝑦)
38373expia 1114 . . . . . . . 8 ((𝑏 ∈ ℝ ∧ 𝑑 ∈ ℝ) → (𝑏𝑑 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥𝑦))
3938ad2ant2l 734 . . . . . . 7 (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → (𝑏𝑑 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥𝑦))
4034, 39jaod 840 . . . . . 6 (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → ((𝑎𝑐𝑏𝑑) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥𝑦))
4129, 40syl5 34 . . . . 5 (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥𝑦))
4241rexlimdvva 3186 . . . 4 ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥𝑦))
4342rexlimivv 3184 . . 3 (∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥𝑦)
441, 17, 43mp2b 10 . 2 𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥𝑦
45 eqtr3 2792 . . . . . . . . 9 ((𝑥 = 0 ∧ 𝑦 = 0) → 𝑥 = 𝑦)
4645ex 397 . . . . . . . 8 (𝑥 = 0 → (𝑦 = 0 → 𝑥 = 𝑦))
4746necon3d 2964 . . . . . . 7 (𝑥 = 0 → (𝑥𝑦𝑦 ≠ 0))
48 neeq1 3005 . . . . . . . . 9 (𝑧 = 𝑦 → (𝑧 ≠ 0 ↔ 𝑦 ≠ 0))
4948rspcev 3461 . . . . . . . 8 ((𝑦 ∈ ℝ ∧ 𝑦 ≠ 0) → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)
5049expcom 398 . . . . . . 7 (𝑦 ≠ 0 → (𝑦 ∈ ℝ → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
5147, 50syl6 35 . . . . . 6 (𝑥 = 0 → (𝑥𝑦 → (𝑦 ∈ ℝ → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
5251com23 86 . . . . 5 (𝑥 = 0 → (𝑦 ∈ ℝ → (𝑥𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
5352adantld 474 . . . 4 (𝑥 = 0 → ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
54 neeq1 3005 . . . . . . . 8 (𝑧 = 𝑥 → (𝑧 ≠ 0 ↔ 𝑥 ≠ 0))
5554rspcev 3461 . . . . . . 7 ((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)
5655expcom 398 . . . . . 6 (𝑥 ≠ 0 → (𝑥 ∈ ℝ → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
5756adantrd 475 . . . . 5 (𝑥 ≠ 0 → ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
5857a1dd 50 . . . 4 (𝑥 ≠ 0 → ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
5953, 58pm2.61ine 3026 . . 3 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
6059rexlimivv 3184 . 2 (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)
61 ax-rrecex 10211 . . . 4 ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → ∃𝑥 ∈ ℝ (𝑧 · 𝑥) = 1)
62 remulcl 10224 . . . . . . 7 ((𝑧 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (𝑧 · 𝑥) ∈ ℝ)
6362adantlr 688 . . . . . 6 (((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) ∧ 𝑥 ∈ ℝ) → (𝑧 · 𝑥) ∈ ℝ)
64 eleq1 2838 . . . . . 6 ((𝑧 · 𝑥) = 1 → ((𝑧 · 𝑥) ∈ ℝ ↔ 1 ∈ ℝ))
6563, 64syl5ibcom 235 . . . . 5 (((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) ∧ 𝑥 ∈ ℝ) → ((𝑧 · 𝑥) = 1 → 1 ∈ ℝ))
6665rexlimdva 3179 . . . 4 ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → (∃𝑥 ∈ ℝ (𝑧 · 𝑥) = 1 → 1 ∈ ℝ))
6761, 66mpd 15 . . 3 ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → 1 ∈ ℝ)
6867rexlimiva 3176 . 2 (∃𝑧 ∈ ℝ 𝑧 ≠ 0 → 1 ∈ ℝ)
6944, 60, 68mp2b 10 1 1 ∈ ℝ
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 382  wo 828   = wceq 1631  wcel 2145  wne 2943  wrex 3062  (class class class)co 6794  cc 10137  cr 10138  0cc0 10139  1c1 10140  ici 10141   + caddc 10142   · cmul 10144
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-1cn 10197  ax-icn 10198  ax-addcl 10199  ax-mulcl 10201  ax-mulrcl 10202  ax-i2m1 10207  ax-1ne0 10208  ax-rrecex 10211  ax-cnre 10212
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 829  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3353  df-dif 3727  df-un 3729  df-in 3731  df-ss 3738  df-nul 4065  df-if 4227  df-sn 4318  df-pr 4320  df-op 4324  df-uni 4576  df-br 4788  df-iota 5995  df-fv 6040  df-ov 6797
This theorem is referenced by:  0re  10243  1red  10258  dedekind  10403  peano2re  10412  mul02lem2  10416  addid1  10419  renegcl  10547  peano2rem  10551  0reALT  10581  0lt1  10753  0le1  10754  relin01  10755  1le1  10858  eqneg  10948  ltp1  11064  ltm1  11066  recgt0  11070  mulgt1  11085  ltmulgt11  11086  lemulge11  11088  reclt1  11121  recgt1  11122  recgt1i  11123  recp1lt1  11124  recreclt  11125  recgt0ii  11132  ledivp1i  11152  ltdivp1i  11153  inelr  11213  cju  11219  nnssre  11227  nnge1  11249  nngt1ne1  11250  nnle1eq1  11251  nngt0  11252  nnnlt1  11253  nnrecre  11260  nnrecgt0  11261  nnsub  11262  2re  11293  3re  11297  4re  11300  5re  11302  6re  11304  7re  11306  8re  11308  9re  11310  10reOLD  11312  0le2  11314  2pos  11315  3pos  11317  4pos  11319  5pos  11321  6pos  11322  7pos  11323  8pos  11324  9pos  11325  10posOLD  11326  neg1rr  11328  neg1lt0  11330  1lt2  11397  1lt3  11399  1lt4  11402  1lt5  11406  1lt6  11411  1lt7  11417  1lt8  11424  1lt9  11432  1lt10OLD  11441  1ne2  11443  1le2  11444  1le3  11447  halflt1  11453  addltmul  11471  nnunb  11491  elnnnn0c  11541  nn0ge2m1nn  11563  elnnz1  11606  znnnlt1  11607  zltp1le  11630  zleltp1  11631  nn0lt2  11643  recnz  11655  gtndiv  11657  3halfnz  11659  1lt10  11883  eluzp1m1  11913  eluzp1p1  11915  eluz2b2  11965  zbtwnre  11990  rebtwnz  11991  1rp  12040  divlt1lt  12103  divle1le  12104  nnledivrp  12146  qbtwnxr  12237  xmulid1  12315  xmulid2  12316  xmulm1  12317  x2times  12335  xrub  12348  0elunit  12498  1elunit  12499  divelunit  12522  lincmb01cmp  12523  iccf1o  12524  xov1plusxeqvd  12526  unitssre  12527  0nelfz1  12568  fzpreddisj  12598  fznatpl1  12603  fztpval  12610  fraclt1  12812  fracle1  12813  flbi2  12827  ico01fl0  12829  fldiv4p1lem1div2  12845  fldiv4lem1div2  12847  fldiv  12868  modid  12904  1mod  12911  m1modnnsub1  12925  modm1p1mod0  12930  seqf1olem1  13048  reexpcl  13085  reexpclz  13088  expge0  13104  expge1  13105  expgt1  13106  bernneq  13198  bernneq2  13199  expnbnd  13201  expnlbnd  13202  expnlbnd2  13203  expmulnbnd  13204  discr1  13208  facwordi  13281  faclbnd3  13284  faclbnd4lem1  13285  faclbnd4lem4  13288  faclbnd6  13291  facavg  13293  hashv01gt1  13338  hashge1  13381  hashnn0n0nn  13383  hash1snb  13410  hashgt12el  13413  hashgt12el2  13414  hashfun  13427  hashge2el2dif  13465  brfi1indALT  13485  lsw0  13550  f1oun2prg  13872  sgn1  14041  cjexp  14099  re1  14103  im1  14104  rei  14105  imi  14106  sqrlem1  14192  sqrlem2  14193  sqrlem3  14194  sqrlem4  14195  sqrlem7  14198  resqrex  14200  sqrt1  14221  sqrt2gt1lt2  14224  sqrtm1  14225  abs1  14246  absrdbnd  14290  caubnd2  14306  mulcn2  14535  reccn2  14536  rlimno1  14593  o1fsum  14753  expcnv  14804  geolim  14809  geolim2  14810  georeclim  14811  geomulcvg  14815  geoisumr  14817  geoisum1c  14819  fprodreclf  14897  fprodge0  14931  fprodge1  14933  rerisefaccl  14955  refallfaccl  14956  ere  15026  ege2le3  15027  efgt1  15053  resin4p  15075  recos4p  15076  tanhbnd  15098  sinbnd  15117  cosbnd  15118  sinbnd2  15119  cosbnd2  15120  ef01bndlem  15121  sin01bnd  15122  cos01bnd  15123  cos1bnd  15124  cos2bnd  15125  sinltx  15126  sin01gt0  15127  cos01gt0  15128  sin02gt0  15129  sincos1sgn  15130  ene1  15145  rpnnen2lem2  15151  rpnnen2lem3  15152  rpnnen2lem4  15153  rpnnen2lem9  15158  rpnnen2lem12  15161  ruclem6  15171  ruclem11  15176  ruclem12  15177  3dvds  15262  3dvdsOLD  15263  halfleoddlt  15295  n2dvds1  15313  flodddiv4  15346  sadcadd  15389  isprm3  15604  sqnprm  15622  coprm  15631  phibndlem  15683  pythagtriplem3  15731  pcmpt  15804  fldivp1  15809  pockthi  15819  infpn2  15825  resslem  16141  basendxnmulrndx  16208  slotsbhcdif  16289  oppcbas  16586  rescbas  16697  rescabs  16701  odubas  17342  lt6abl  18504  srgbinomlem4  18752  abvneg  19045  abvtrivd  19051  rmodislmod  19142  isnzr2hash  19480  0ringnnzr  19485  cnfldfun  19974  xrsmcmn  19985  xrsnsgrp  19998  gzrngunitlem  20027  gzrngunit  20028  rge0srg  20033  psgnodpmr  20152  remulg  20171  resubdrg  20172  thlbas  20258  matbas  20437  leordtval2  21238  tuslem  22292  setsmsbas  22501  dscmet  22598  dscopn  22599  nrginvrcnlem  22716  nmoid  22767  idnghm  22768  tgioo  22820  blcvx  22822  metnrmlem1a  22882  metnrmlem1  22883  iicmp  22910  iiconn  22911  iirev  22949  iihalf1  22951  iihalf2  22953  iihalf2cn  22954  elii1  22955  elii2  22956  iimulcl  22957  icopnfcnv  22962  icopnfhmeo  22963  iccpnfcnv  22964  iccpnfhmeo  22965  xrhmeo  22966  xrhmph  22967  evth  22979  xlebnum  22985  lebnumii  22986  htpycc  23000  reparphti  23017  pcoval1  23033  pco1  23035  pcoval2  23036  pcocn  23037  pcohtpylem  23039  pcopt  23042  pcopt2  23043  pcoass  23044  pcorevlem  23046  nmhmcn  23140  ncvs1  23177  ovolunlem1a  23485  vitalilem2  23598  vitalilem4  23600  vitalilem5  23601  vitali  23602  i1f1  23678  itg11  23679  itg2const  23728  itg2monolem1  23738  itg2monolem3  23740  dveflem  23963  dvlipcn  23978  dvcvx  24004  ply1remlem  24143  fta1blem  24149  vieta1lem2  24287  aalioulem3  24310  aalioulem5  24312  aaliou3lem2  24319  ulmbdd  24373  iblulm  24382  radcnvlem1  24388  dvradcnv  24396  abelthlem2  24407  abelthlem3  24408  abelthlem5  24410  abelthlem7  24413  abelth  24416  abelth2  24417  reeff1olem  24421  reeff1o  24422  sinhalfpilem  24437  tangtx  24479  sincos4thpi  24487  pige3  24491  coskpi  24494  recosf1o  24503  tanregt0  24507  efif1olem3  24512  efif1olem4  24513  loge  24555  logdivlti  24588  logcnlem4  24613  logf1o2  24618  dvlog2lem  24620  logtayl  24628  logccv  24631  recxpcl  24643  cxplea  24664  cxpcn3lem  24710  cxpaddlelem  24714  loglesqrt  24721  logblog  24752  ang180lem2  24762  angpined  24779  chordthmlem4  24784  acosrecl  24852  atancj  24859  atanlogaddlem  24862  atantan  24872  atans2  24880  ressatans  24883  leibpi  24891  log2le1  24899  birthdaylem3  24902  cxp2lim  24925  cxploglim  24926  cxploglim2  24927  divsqrtsumlem  24928  cvxcl  24933  scvxcvx  24934  jensenlem2  24936  amgmlem  24938  emcllem2  24945  emcllem4  24947  emcllem6  24949  emcllem7  24950  emre  24954  emgt0  24955  harmonicbnd3  24956  harmonicubnd  24958  harmonicbnd4  24959  zetacvg  24963  lgamgulmlem2  24978  ftalem1  25021  ftalem2  25022  ftalem5  25025  issqf  25084  cht1  25113  chp1  25115  ppiltx  25125  mumullem2  25128  ppiublem1  25149  ppiub  25151  chtublem  25158  chtub  25159  logfacbnd3  25170  logexprlim  25172  perfectlem2  25177  dchrinv  25208  dchr1re  25210  efexple  25228  bposlem1  25231  bposlem2  25232  bposlem5  25235  bposlem8  25238  lgsdir2lem1  25272  lgsdir2lem5  25276  lgsdir  25279  lgsne0  25282  lgsabs1  25283  lgsdinn0  25292  gausslemma2dlem0i  25311  lgseisen  25326  m1lgs  25335  2lgslem3  25351  chebbnd1lem3  25382  chebbnd1  25383  chtppilimlem1  25384  chtppilimlem2  25385  chtppilim  25386  chpchtlim  25390  vmadivsumb  25394  rplogsumlem2  25396  rpvmasumlem  25398  dchrmusumlema  25404  dchrmusum2  25405  dchrvmasumlem2  25409  dchrvmasumiflem1  25412  dchrisum0flblem1  25419  dchrisum0flblem2  25420  dchrisum0fno1  25422  rpvmasum2  25423  dchrisum0re  25424  dchrisum0lema  25425  dchrisum0lem1b  25426  dchrisum0lem1  25427  dchrisum0lem2a  25428  dchrisum0lem2  25429  logdivsum  25444  mulog2sumlem2  25446  2vmadivsumlem  25451  log2sumbnd  25455  selbergb  25460  selberg2b  25463  chpdifbndlem1  25464  selberg3lem1  25468  selberg3lem2  25469  selberg4lem1  25471  pntrmax  25475  pntrsumo1  25476  selbergsb  25486  pntrlog2bndlem3  25490  pntrlog2bndlem5  25492  pntpbnd1a  25496  pntpbnd2  25498  pntibndlem1  25500  pntibndlem2  25502  pntibndlem3  25503  pntibnd  25504  pntlemd  25505  pntlemc  25506  pntlemb  25508  pntlemr  25513  pntlemf  25516  pntlemk  25517  pntlemo  25518  pntlem3  25520  pntleml  25522  pnt  25525  abvcxp  25526  ostth2lem1  25529  padicabvf  25542  padicabvcxp  25543  ostth1  25544  ostth2lem2  25545  ostth2lem3  25546  ostth2lem4  25547  ostth2  25548  ostth3  25549  ostth  25550  trgcgrg  25632  ttgcontlem1  25987  brbtwn2  26007  colinearalglem4  26011  ax5seglem1  26030  ax5seglem2  26031  ax5seglem3  26033  ax5seglem5  26035  ax5seglem6  26036  ax5seglem9  26039  ax5seg  26040  axbtwnid  26041  axpaschlem  26042  axpasch  26043  axlowdimlem6  26049  axlowdimlem10  26053  axlowdimlem16  26059  axlowdim1  26061  axlowdim2  26062  axlowdim  26063  axcontlem2  26067  axcontlem4  26069  axcontlem7  26072  lfgrnloop  26242  lfuhgr1v0e  26370  usgrexmpldifpr  26374  usgrexmplef  26375  1loopgrvd2  26635  vdegp1bi  26669  lfgrwlkprop  26820  pthdlem1  26898  pthdlem2  26900  clwlkclwwlkf  27159  upgr4cycl4dv4e  27366  konigsberglem2  27434  konigsberglem3  27435  konigsberglem5  27437  frgrreg  27594  ex-dif  27623  ex-in  27625  ex-pss  27628  ex-res  27641  ex-fl  27647  nv1  27871  smcnlem  27893  ipidsq  27906  nmlno0lem  27989  norm-ii-i  28335  bcs2  28380  norm1  28447  nmopub2tALT  29109  nmfnleub2  29126  nmlnop0iALT  29195  nmopun  29214  unopbd  29215  nmopadjlem  29289  nmopcoadji  29301  pjnmopi  29348  pjbdlni  29349  stge0  29424  stle1  29425  hstle1  29426  hstle  29430  hstles  29431  stge1i  29438  stlesi  29441  staddi  29446  stadd3i  29448  strlem1  29450  strlem3a  29452  strlem5  29455  jplem1  29468  cdj1i  29633  addltmulALT  29646  xlt2addrd  29864  pr01ssre  29911  dp2lt10  29932  dp2ltsuc  29934  dp2ltc  29935  dplti  29954  dpmul4  29963  xdivrec  29976  xrsmulgzz  30019  xrnarchi  30079  resvbas  30173  rearchi  30183  xrge0slmod  30185  submateqlem1  30214  elunitrn  30284  elunitge0  30286  unitssxrge0  30287  unitdivcld  30288  xrge0iifcnv  30320  xrge0iifcv  30321  xrge0iifiso  30322  xrge0iifhom  30324  zrhre  30404  indf  30418  indfval  30419  esumcst  30466  hasheuni  30488  cntnevol  30632  ddemeas  30640  omssubadd  30703  iwrdsplit  30790  prob01  30816  dstfrvclim1  30880  coinfliprv  30885  ballotlem2  30891  ballotlem4  30901  ballotlemi1  30905  ballotlemic  30909  sgnclre  30942  sgnnbi  30948  sgnpbi  30949  sgnmulsgp  30953  plymulx0  30965  plymulx  30966  signswch  30979  signstf  30984  signsvfn  31000  itgexpif  31025  hgt750lemd  31067  logdivsqrle  31069  hgt750lem  31070  hgt750lem2  31071  hgt750leme  31077  tgoldbachgnn  31078  subfacp1lem1  31500  subfacp1lem5  31505  resconn  31567  iisconn  31573  iillysconn  31574  snmlff  31650  problem2  31898  problem2OLD  31899  problem3  31900  sinccvglem  31905  fz0n  31955  dnizeq0  32803  dnibndlem12  32817  knoppcnlem4  32824  knoppndvlem13  32853  cnndvlem1  32866  relowlpssretop  33550  sin2h  33733  cos2h  33734  tan2h  33735  poimirlem7  33750  poimirlem16  33759  poimirlem17  33760  poimirlem19  33762  poimirlem20  33763  poimirlem22  33765  poimirlem23  33766  poimirlem29  33772  poimirlem30  33773  poimirlem31  33774  poimirlem32  33775  broucube  33777  itg2addnclem3  33796  asindmre  33828  dvasin  33829  dvacos  33830  dvreasin  33831  dvreacos  33832  areacirclem1  33833  fdc  33874  geomcau  33888  cntotbnd  33928  heiborlem8  33950  bfplem2  33955  bfp  33956  rabren3dioph  37906  pellexlem5  37924  pellexlem6  37925  pell1qrgaplem  37964  pell14qrgap  37966  pellqrex  37970  pellfundre  37972  pellfundlb  37975  pellfund14gap  37978  rmspecsqrtnqOLD  37998  jm2.17a  38054  acongeq  38077  jm2.23  38090  jm3.1lem2  38112  relexp01min  38532  imo72b2  39002  cvgdvgrat  39039  lhe4.4ex1a  39055  binomcxplemnotnn0  39082  isosctrlem1ALT  39693  supxrgelem  40070  xrlexaddrp  40085  infxr  40100  infleinflem2  40104  1xr  40203  sumnnodd  40381  limsup10exlem  40523  limsup10ex  40524  liminf10ex  40525  dvnprodlem3  40682  stoweidlem1  40736  stoweidlem18  40753  stoweidlem19  40754  stoweidlem26  40761  stoweidlem34  40769  stoweidlem40  40775  stoweidlem41  40776  stoweidlem59  40794  stoweid  40798  stirlinglem10  40818  stirlinglem11  40819  dirkercncflem1  40838  fourierdlem16  40858  fourierdlem21  40863  fourierdlem22  40864  fourierdlem42  40884  fourierdlem68  40909  fourierdlem83  40924  fourierdlem103  40944  sqwvfourb  40964  fouriersw  40966  etransclem23  40992  salexct2  41075  salgencntex  41079  ovn0lem  41300  smfmullem3  41521  smfmullem4  41522  zm1nn  41845  m1mod0mod1  41868  fmtnosqrt  41980  perfectALTVlem2  42160  nnsum3primesprm  42207  nnsum4primesodd  42213  nnsum4primesoddALTV  42214  nnsum4primeseven  42217  nnsum4primesevenALTV  42218  tgblthelfgott  42232  tgoldbach  42234  tgblthelfgottOLD  42238  tgoldbachOLD  42241  expnegico01  42837  regt1loggt0  42859  rege1logbrege0  42881  rege1logbzge0  42882  blennnelnn  42899  dignnld  42926  nn0sumshdiglemA  42942  nn0sumshdiglem1  42944
  Copyright terms: Public domain W3C validator