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

Theorem 1re 10202
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 10157, 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 10168 . . 3 1 ≠ 0
2 ax-1cn 10157 . . . . 5 1 ∈ ℂ
3 cnre 10199 . . . . 5 (1 ∈ ℂ → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)))
42, 3ax-mp 5 . . . 4 𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏))
5 neeq1 2982 . . . . . . . 8 (1 = (𝑎 + (i · 𝑏)) → (1 ≠ 0 ↔ (𝑎 + (i · 𝑏)) ≠ 0))
65biimpcd 239 . . . . . . 7 (1 ≠ 0 → (1 = (𝑎 + (i · 𝑏)) → (𝑎 + (i · 𝑏)) ≠ 0))
7 0cn 10195 . . . . . . . 8 0 ∈ ℂ
8 cnre 10199 . . . . . . . 8 (0 ∈ ℂ → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)))
97, 8ax-mp 5 . . . . . . 7 𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑))
10 neeq2 2983 . . . . . . . . . 10 (0 = (𝑐 + (i · 𝑑)) → ((𝑎 + (i · 𝑏)) ≠ 0 ↔ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
1110biimpcd 239 . . . . . . . . 9 ((𝑎 + (i · 𝑏)) ≠ 0 → (0 = (𝑐 + (i · 𝑑)) → (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
1211reximdv 3142 . . . . . . . 8 ((𝑎 + (i · 𝑏)) ≠ 0 → (∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)) → ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
1312reximdv 3142 . . . . . . 7 ((𝑎 + (i · 𝑏)) ≠ 0 → (∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)) → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
146, 9, 13syl6mpi 67 . . . . . 6 (1 ≠ 0 → (1 = (𝑎 + (i · 𝑏)) → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
1514reximdv 3142 . . . . 5 (1 ≠ 0 → (∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)) → ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
1615reximdv 3142 . . . 4 (1 ≠ 0 → (∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)) → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
174, 16mpi 20 . . 3 (1 ≠ 0 → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)))
18 ioran 512 . . . . . . . . 9 (¬ (𝑎𝑐𝑏𝑑) ↔ (¬ 𝑎𝑐 ∧ ¬ 𝑏𝑑))
19 df-ne 2921 . . . . . . . . . . 11 (𝑎𝑐 ↔ ¬ 𝑎 = 𝑐)
2019con2bii 346 . . . . . . . . . 10 (𝑎 = 𝑐 ↔ ¬ 𝑎𝑐)
21 df-ne 2921 . . . . . . . . . . 11 (𝑏𝑑 ↔ ¬ 𝑏 = 𝑑)
2221con2bii 346 . . . . . . . . . 10 (𝑏 = 𝑑 ↔ ¬ 𝑏𝑑)
2320, 22anbi12i 735 . . . . . . . . 9 ((𝑎 = 𝑐𝑏 = 𝑑) ↔ (¬ 𝑎𝑐 ∧ ¬ 𝑏𝑑))
2418, 23bitr4i 267 . . . . . . . 8 (¬ (𝑎𝑐𝑏𝑑) ↔ (𝑎 = 𝑐𝑏 = 𝑑))
25 id 22 . . . . . . . . 9 (𝑎 = 𝑐𝑎 = 𝑐)
26 oveq2 6809 . . . . . . . . 9 (𝑏 = 𝑑 → (i · 𝑏) = (i · 𝑑))
2725, 26oveqan12d 6820 . . . . . . . 8 ((𝑎 = 𝑐𝑏 = 𝑑) → (𝑎 + (i · 𝑏)) = (𝑐 + (i · 𝑑)))
2824, 27sylbi 207 . . . . . . 7 (¬ (𝑎𝑐𝑏𝑑) → (𝑎 + (i · 𝑏)) = (𝑐 + (i · 𝑑)))
2928necon1ai 2947 . . . . . 6 ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → (𝑎𝑐𝑏𝑑))
30 neeq1 2982 . . . . . . . . . 10 (𝑥 = 𝑎 → (𝑥𝑦𝑎𝑦))
31 neeq2 2983 . . . . . . . . . 10 (𝑦 = 𝑐 → (𝑎𝑦𝑎𝑐))
3230, 31rspc2ev 3451 . . . . . . . . 9 ((𝑎 ∈ ℝ ∧ 𝑐 ∈ ℝ ∧ 𝑎𝑐) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥𝑦)
33323expia 1114 . . . . . . . 8 ((𝑎 ∈ ℝ ∧ 𝑐 ∈ ℝ) → (𝑎𝑐 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥𝑦))
3433ad2ant2r 800 . . . . . . 7 (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → (𝑎𝑐 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥𝑦))
35 neeq1 2982 . . . . . . . . . 10 (𝑥 = 𝑏 → (𝑥𝑦𝑏𝑦))
36 neeq2 2983 . . . . . . . . . 10 (𝑦 = 𝑑 → (𝑏𝑦𝑏𝑑))
3735, 36rspc2ev 3451 . . . . . . . . 9 ((𝑏 ∈ ℝ ∧ 𝑑 ∈ ℝ ∧ 𝑏𝑑) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥𝑦)
38373expia 1114 . . . . . . . 8 ((𝑏 ∈ ℝ ∧ 𝑑 ∈ ℝ) → (𝑏𝑑 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥𝑦))
3938ad2ant2l 799 . . . . . . 7 (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → (𝑏𝑑 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥𝑦))
4034, 39jaod 394 . . . . . 6 (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → ((𝑎𝑐𝑏𝑑) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥𝑦))
4129, 40syl5 34 . . . . 5 (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥𝑦))
4241rexlimdvva 3164 . . . 4 ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥𝑦))
4342rexlimivv 3162 . . 3 (∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥𝑦)
441, 17, 43mp2b 10 . 2 𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥𝑦
45 eqtr3 2769 . . . . . . . . 9 ((𝑥 = 0 ∧ 𝑦 = 0) → 𝑥 = 𝑦)
4645ex 449 . . . . . . . 8 (𝑥 = 0 → (𝑦 = 0 → 𝑥 = 𝑦))
4746necon3d 2941 . . . . . . 7 (𝑥 = 0 → (𝑥𝑦𝑦 ≠ 0))
48 neeq1 2982 . . . . . . . . 9 (𝑧 = 𝑦 → (𝑧 ≠ 0 ↔ 𝑦 ≠ 0))
4948rspcev 3437 . . . . . . . 8 ((𝑦 ∈ ℝ ∧ 𝑦 ≠ 0) → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)
5049expcom 450 . . . . . . 7 (𝑦 ≠ 0 → (𝑦 ∈ ℝ → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
5147, 50syl6 35 . . . . . 6 (𝑥 = 0 → (𝑥𝑦 → (𝑦 ∈ ℝ → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
5251com23 86 . . . . 5 (𝑥 = 0 → (𝑦 ∈ ℝ → (𝑥𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
5352adantld 484 . . . 4 (𝑥 = 0 → ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
54 neeq1 2982 . . . . . . . 8 (𝑧 = 𝑥 → (𝑧 ≠ 0 ↔ 𝑥 ≠ 0))
5554rspcev 3437 . . . . . . 7 ((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)
5655expcom 450 . . . . . 6 (𝑥 ≠ 0 → (𝑥 ∈ ℝ → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
5756adantrd 485 . . . . 5 (𝑥 ≠ 0 → ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
5857a1dd 50 . . . 4 (𝑥 ≠ 0 → ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
5953, 58pm2.61ine 3003 . . 3 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
6059rexlimivv 3162 . 2 (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)
61 ax-rrecex 10171 . . . 4 ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → ∃𝑥 ∈ ℝ (𝑧 · 𝑥) = 1)
62 remulcl 10184 . . . . . . 7 ((𝑧 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (𝑧 · 𝑥) ∈ ℝ)
6362adantlr 753 . . . . . 6 (((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) ∧ 𝑥 ∈ ℝ) → (𝑧 · 𝑥) ∈ ℝ)
64 eleq1 2815 . . . . . 6 ((𝑧 · 𝑥) = 1 → ((𝑧 · 𝑥) ∈ ℝ ↔ 1 ∈ ℝ))
6563, 64syl5ibcom 235 . . . . 5 (((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) ∧ 𝑥 ∈ ℝ) → ((𝑧 · 𝑥) = 1 → 1 ∈ ℝ))
6665rexlimdva 3157 . . . 4 ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → (∃𝑥 ∈ ℝ (𝑧 · 𝑥) = 1 → 1 ∈ ℝ))
6761, 66mpd 15 . . 3 ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → 1 ∈ ℝ)
6867rexlimiva 3154 . 2 (∃𝑧 ∈ ℝ 𝑧 ≠ 0 → 1 ∈ ℝ)
6944, 60, 68mp2b 10 1 1 ∈ ℝ
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wo 382  wa 383   = wceq 1620  wcel 2127  wne 2920  wrex 3039  (class class class)co 6801  cc 10097  cr 10098  0cc0 10099  1c1 10100  ici 10101   + caddc 10102   · cmul 10104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1859  ax-4 1874  ax-5 1976  ax-6 2042  ax-7 2078  ax-9 2136  ax-10 2156  ax-11 2171  ax-12 2184  ax-13 2379  ax-ext 2728  ax-1cn 10157  ax-icn 10158  ax-addcl 10159  ax-mulcl 10161  ax-mulrcl 10162  ax-i2m1 10167  ax-1ne0 10168  ax-rrecex 10171  ax-cnre 10172
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1623  df-ex 1842  df-nf 1847  df-sb 2035  df-clab 2735  df-cleq 2741  df-clel 2744  df-nfc 2879  df-ne 2921  df-ral 3043  df-rex 3044  df-rab 3047  df-v 3330  df-dif 3706  df-un 3708  df-in 3710  df-ss 3717  df-nul 4047  df-if 4219  df-sn 4310  df-pr 4312  df-op 4316  df-uni 4577  df-br 4793  df-iota 6000  df-fv 6045  df-ov 6804
This theorem is referenced by:  0re  10203  1red  10218  dedekind  10363  peano2re  10372  mul02lem2  10376  addid1  10379  renegcl  10507  peano2rem  10511  0reALT  10541  0lt1  10713  0le1  10714  relin01  10715  1le1  10818  eqneg  10908  ltp1  11024  ltm1  11026  recgt0  11030  mulgt1  11045  ltmulgt11  11046  lemulge11  11048  reclt1  11081  recgt1  11082  recgt1i  11083  recp1lt1  11084  recreclt  11085  recgt0ii  11092  ledivp1i  11112  ltdivp1i  11113  inelr  11173  cju  11179  nnssre  11187  nnge1  11209  nngt1ne1  11210  nnle1eq1  11211  nngt0  11212  nnnlt1  11213  nnrecre  11220  nnrecgt0  11221  nnsub  11222  2re  11253  3re  11257  4re  11260  5re  11262  6re  11264  7re  11266  8re  11268  9re  11270  10reOLD  11272  0le2  11274  2pos  11275  3pos  11277  4pos  11279  5pos  11281  6pos  11282  7pos  11283  8pos  11284  9pos  11285  10posOLD  11286  neg1rr  11288  neg1lt0  11290  1lt2  11357  1lt3  11359  1lt4  11362  1lt5  11366  1lt6  11371  1lt7  11377  1lt8  11384  1lt9  11392  1lt10OLD  11401  1ne2  11403  1le2  11404  1le3  11407  halflt1  11413  addltmul  11431  nnunb  11451  elnnnn0c  11501  nn0ge2m1nn  11523  elnnz1  11566  znnnlt1  11567  zltp1le  11590  zleltp1  11591  nn0lt2  11603  recnz  11615  gtndiv  11617  3halfnz  11619  1lt10  11844  eluzp1m1  11874  eluzp1p1  11876  eluz2b2  11925  zbtwnre  11950  rebtwnz  11951  1rp  12000  divlt1lt  12063  divle1le  12064  nnledivrp  12104  qbtwnxr  12195  xmulid1  12273  xmulid2  12274  xmulm1  12275  x2times  12293  xrub  12306  0elunit  12454  1elunit  12455  divelunit  12478  lincmb01cmp  12479  iccf1o  12480  xov1plusxeqvd  12482  unitssre  12483  0nelfz1  12524  fzpreddisj  12554  fznatpl1  12559  fztpval  12566  fraclt1  12768  fracle1  12769  flbi2  12783  ico01fl0  12785  fldiv4p1lem1div2  12801  fldiv4lem1div2  12803  fldiv  12824  modid  12860  1mod  12867  m1modnnsub1  12881  modm1p1mod0  12886  seqf1olem1  13005  reexpcl  13042  reexpclz  13045  expge0  13061  expge1  13062  expgt1  13063  bernneq  13155  bernneq2  13156  expnbnd  13158  expnlbnd  13159  expnlbnd2  13160  expmulnbnd  13161  discr1  13165  facwordi  13241  faclbnd3  13244  faclbnd4lem1  13245  faclbnd4lem4  13248  faclbnd6  13251  facavg  13253  hashv01gt1  13298  hashge1  13341  hashnn0n0nn  13343  hash1snb  13370  hashgt12el  13373  hashgt12el2  13374  hashfun  13387  hashge2el2dif  13425  brfi1indALT  13445  lsw0  13510  f1oun2prg  13833  sgn1  14002  cjexp  14060  re1  14064  im1  14065  rei  14066  imi  14067  sqrlem1  14153  sqrlem2  14154  sqrlem3  14155  sqrlem4  14156  sqrlem7  14159  resqrex  14161  sqrt1  14182  sqrt2gt1lt2  14185  sqrtm1  14186  abs1  14207  absrdbnd  14251  caubnd2  14267  mulcn2  14496  reccn2  14497  rlimno1  14554  o1fsum  14715  expcnv  14766  geolim  14771  geolim2  14772  georeclim  14773  geomulcvg  14777  geoisumr  14779  geoisum1c  14781  geoihalfsum  14784  fprodreclf  14859  fprodge0  14894  fprodge1  14896  rerisefaccl  14918  refallfaccl  14919  ere  14989  ege2le3  14990  efgt1  15016  resin4p  15038  recos4p  15039  tanhbnd  15061  sinbnd  15080  cosbnd  15081  sinbnd2  15082  cosbnd2  15083  ef01bndlem  15084  sin01bnd  15085  cos01bnd  15086  cos1bnd  15087  cos2bnd  15088  sinltx  15089  sin01gt0  15090  cos01gt0  15091  sin02gt0  15092  sincos1sgn  15093  ene1  15108  rpnnen2lem2  15114  rpnnen2lem3  15115  rpnnen2lem4  15116  rpnnen2lem9  15121  rpnnen2lem12  15124  ruclem6  15134  ruclem11  15139  ruclem12  15140  3dvds  15225  3dvdsOLD  15226  halfleoddlt  15259  n2dvds1  15277  flodddiv4  15310  sadcadd  15353  isprm3  15569  sqnprm  15587  coprm  15596  phibndlem  15648  pythagtriplem3  15696  pcmpt  15769  fldivp1  15774  pockthi  15784  infpn2  15790  resslem  16106  basendxnmulrndx  16172  slotsbhcdif  16253  oppcbas  16550  rescbas  16661  rescabs  16665  odubas  17305  lt6abl  18467  srgbinomlem4  18714  abvneg  19007  abvtrivd  19013  rmodislmod  19104  isnzr2hash  19437  0ringnnzr  19442  cnfldfun  19931  xrsmcmn  19942  xrsnsgrp  19955  gzrngunitlem  19984  gzrngunit  19985  rge0srg  19990  psgnodpmr  20109  remulg  20126  resubdrg  20127  thlbas  20213  matbas  20392  leordtval2  21189  tuslem  22243  setsmsbas  22452  dscmet  22549  dscopn  22550  nrginvrcnlem  22667  nmoid  22718  idnghm  22719  tgioo  22771  blcvx  22773  metnrmlem1a  22833  metnrmlem1  22834  iicmp  22861  iiconn  22862  iirev  22900  iihalf1  22902  iihalf2  22904  iihalf2cn  22905  elii1  22906  elii2  22907  iimulcl  22908  icopnfcnv  22913  icopnfhmeo  22914  iccpnfcnv  22915  iccpnfhmeo  22916  xrhmeo  22917  xrhmph  22918  evth  22930  xlebnum  22936  lebnumii  22937  htpycc  22951  reparphti  22968  pcoval1  22984  pco1  22986  pcoval2  22987  pcocn  22988  pcohtpylem  22990  pcopt  22993  pcopt2  22994  pcoass  22995  pcorevlem  22997  nmhmcn  23091  ncvs1  23128  ovolunlem1a  23435  vitalilem2  23548  vitalilem4  23550  vitalilem5  23551  vitali  23552  i1f1  23627  itg11  23628  itg2const  23677  itg2monolem1  23687  itg2monolem3  23689  dveflem  23912  dvlipcn  23927  dvcvx  23953  ply1remlem  24092  fta1blem  24098  vieta1lem2  24236  aalioulem3  24259  aalioulem5  24261  aaliou3lem2  24268  ulmbdd  24322  iblulm  24331  radcnvlem1  24337  dvradcnv  24345  abelthlem2  24356  abelthlem3  24357  abelthlem5  24359  abelthlem7  24362  abelth  24365  abelth2  24366  reeff1olem  24370  reeff1o  24371  sinhalfpilem  24385  tangtx  24427  sincos4thpi  24435  pige3  24439  coskpi  24442  recosf1o  24451  tanregt0  24455  efif1olem3  24460  efif1olem4  24461  loge  24503  logdivlti  24536  logcnlem4  24561  logf1o2  24566  dvlog2lem  24568  logtayl  24576  logccv  24579  recxpcl  24591  cxplea  24612  cxpcn3lem  24658  cxpaddlelem  24662  loglesqrt  24669  logblog  24700  ang180lem2  24710  angpined  24727  chordthmlem4  24732  acosrecl  24800  atancj  24807  atanlogaddlem  24810  atantan  24820  atans2  24828  ressatans  24831  leibpi  24839  log2le1  24847  birthdaylem3  24850  cxp2lim  24873  cxploglim  24874  cxploglim2  24875  divsqrtsumlem  24876  cvxcl  24881  scvxcvx  24882  jensenlem2  24884  amgmlem  24886  emcllem2  24893  emcllem4  24895  emcllem6  24897  emcllem7  24898  emre  24902  emgt0  24903  harmonicbnd3  24904  harmonicubnd  24906  harmonicbnd4  24907  zetacvg  24911  lgamgulmlem2  24926  ftalem1  24969  ftalem2  24970  ftalem5  24973  issqf  25032  cht1  25061  chp1  25063  ppiltx  25073  mumullem2  25076  ppiublem1  25097  ppiub  25099  chtublem  25106  chtub  25107  logfacbnd3  25118  logexprlim  25120  perfectlem2  25125  dchrinv  25156  dchr1re  25158  efexple  25176  bposlem1  25179  bposlem2  25180  bposlem5  25183  bposlem8  25186  lgsdir2lem1  25220  lgsdir2lem5  25224  lgsdir  25227  lgsne0  25230  lgsabs1  25231  lgsdinn0  25240  gausslemma2dlem0i  25259  lgseisen  25274  m1lgs  25283  2lgslem3  25299  chebbnd1lem3  25330  chebbnd1  25331  chtppilimlem1  25332  chtppilimlem2  25333  chtppilim  25334  chpchtlim  25338  vmadivsumb  25342  rplogsumlem2  25344  rpvmasumlem  25346  dchrmusumlema  25352  dchrmusum2  25353  dchrvmasumlem2  25357  dchrvmasumiflem1  25360  dchrisum0flblem1  25367  dchrisum0flblem2  25368  dchrisum0fno1  25370  rpvmasum2  25371  dchrisum0re  25372  dchrisum0lema  25373  dchrisum0lem1b  25374  dchrisum0lem1  25375  dchrisum0lem2a  25376  dchrisum0lem2  25377  logdivsum  25392  mulog2sumlem2  25394  2vmadivsumlem  25399  log2sumbnd  25403  selbergb  25408  selberg2b  25411  chpdifbndlem1  25412  selberg3lem1  25416  selberg3lem2  25417  selberg4lem1  25419  pntrmax  25423  pntrsumo1  25424  selbergsb  25434  pntrlog2bndlem3  25438  pntrlog2bndlem5  25440  pntpbnd1a  25444  pntpbnd2  25446  pntibndlem1  25448  pntibndlem2  25450  pntibndlem3  25451  pntibnd  25452  pntlemd  25453  pntlemc  25454  pntlemb  25456  pntlemr  25461  pntlemf  25464  pntlemk  25465  pntlemo  25466  pntlem3  25468  pntleml  25470  pnt  25473  abvcxp  25474  ostth2lem1  25477  padicabvf  25490  padicabvcxp  25491  ostth1  25492  ostth2lem2  25493  ostth2lem3  25494  ostth2lem4  25495  ostth2  25496  ostth3  25497  ostth  25498  trgcgrg  25580  ttgcontlem1  25935  brbtwn2  25955  colinearalglem4  25959  ax5seglem1  25978  ax5seglem2  25979  ax5seglem3  25981  ax5seglem5  25983  ax5seglem6  25984  ax5seglem9  25987  ax5seg  25988  axbtwnid  25989  axpaschlem  25990  axpasch  25991  axlowdimlem6  25997  axlowdimlem10  26001  axlowdimlem16  26007  axlowdim1  26009  axlowdim2  26010  axlowdim  26011  axcontlem2  26015  axcontlem4  26017  axcontlem7  26020  lfgrnloop  26190  lfuhgr1v0e  26316  usgrexmpldifpr  26320  usgrexmplef  26321  1loopgrvd2  26580  vdegp1bi  26614  lfgrwlkprop  26765  pthdlem1  26843  pthdlem2  26845  clwlkclwwlkf  27102  upgr4cycl4dv4e  27308  konigsberglem2  27376  konigsberglem3  27377  konigsberglem5  27379  frgrreg  27533  ex-dif  27562  ex-in  27564  ex-pss  27567  ex-res  27580  ex-fl  27586  nv1  27810  smcnlem  27832  ipidsq  27845  nmlno0lem  27928  norm-ii-i  28274  bcs2  28319  norm1  28386  nmopub2tALT  29048  nmfnleub2  29065  nmlnop0iALT  29134  nmopun  29153  unopbd  29154  nmopadjlem  29228  nmopcoadji  29240  pjnmopi  29287  pjbdlni  29288  stge0  29363  stle1  29364  hstle1  29365  hstle  29369  hstles  29370  stge1i  29377  stlesi  29380  staddi  29385  stadd3i  29387  strlem1  29389  strlem3a  29391  strlem5  29394  jplem1  29407  cdj1i  29572  addltmulALT  29585  xlt2addrd  29803  pr01ssre  29850  dp2lt10  29871  dp2ltsuc  29873  dp2ltc  29874  dplti  29893  dpmul4  29902  xdivrec  29915  xrsmulgzz  29958  xrnarchi  30018  resvbas  30112  rearchi  30122  xrge0slmod  30124  submateqlem1  30153  elunitrn  30223  elunitge0  30225  unitssxrge0  30226  unitdivcld  30227  xrge0iifcnv  30259  xrge0iifcv  30260  xrge0iifiso  30261  xrge0iifhom  30263  zrhre  30343  indf  30357  indfval  30358  esumcst  30405  hasheuni  30427  cntnevol  30571  ddemeas  30579  omssubadd  30642  iwrdsplit  30729  prob01  30755  dstfrvclim1  30819  coinfliprv  30824  ballotlem2  30830  ballotlem4  30840  ballotlemi1  30844  ballotlemic  30848  sgnclre  30881  sgnnbi  30887  sgnpbi  30888  sgnmulsgp  30892  plymulx0  30904  plymulx  30905  signswch  30918  signstf  30923  signsvfn  30939  itgexpif  30964  hgt750lemd  31006  logdivsqrle  31008  hgt750lem  31009  hgt750lem2  31010  hgt750leme  31016  tgoldbachgnn  31017  subfacp1lem1  31439  subfacp1lem5  31444  resconn  31506  iisconn  31512  iillysconn  31513  snmlff  31589  problem2  31837  problem2OLD  31838  problem3  31839  sinccvglem  31844  fz0n  31894  dnizeq0  32742  dnibndlem12  32756  knoppcnlem4  32763  knoppndvlem13  32792  cnndvlem1  32805  relowlpssretop  33494  sin2h  33681  cos2h  33682  tan2h  33683  poimirlem7  33698  poimirlem16  33707  poimirlem17  33708  poimirlem19  33710  poimirlem20  33711  poimirlem22  33713  poimirlem23  33714  poimirlem29  33720  poimirlem30  33721  poimirlem31  33722  poimirlem32  33723  broucube  33725  itg2addnclem3  33745  asindmre  33777  dvasin  33778  dvacos  33779  dvreasin  33780  dvreacos  33781  areacirclem1  33782  fdc  33823  geomcau  33837  cntotbnd  33877  heiborlem8  33899  bfplem2  33904  bfp  33905  rabren3dioph  37850  pellexlem5  37868  pellexlem6  37869  pell1qrgaplem  37908  pell14qrgap  37910  pellqrex  37914  pellfundre  37916  pellfundlb  37919  pellfund14gap  37922  rmspecsqrtnqOLD  37942  jm2.17a  37998  acongeq  38021  jm2.23  38034  jm3.1lem2  38056  relexp01min  38476  imo72b2  38946  cvgdvgrat  38983  lhe4.4ex1a  38999  binomcxplemnotnn0  39026  isosctrlem1ALT  39638  supxrgelem  40020  xrlexaddrp  40035  infxr  40050  infleinflem2  40054  1xr  40153  sumnnodd  40334  limsup10exlem  40476  limsup10ex  40477  liminf10ex  40478  dvnprodlem3  40635  stoweidlem1  40690  stoweidlem18  40707  stoweidlem19  40708  stoweidlem26  40715  stoweidlem34  40723  stoweidlem40  40729  stoweidlem41  40730  stoweidlem59  40748  stoweid  40752  stirlinglem10  40772  stirlinglem11  40773  dirkercncflem1  40792  fourierdlem16  40812  fourierdlem21  40817  fourierdlem22  40818  fourierdlem42  40838  fourierdlem68  40863  fourierdlem83  40878  fourierdlem103  40898  sqwvfourb  40918  fouriersw  40920  etransclem23  40946  salexct2  41029  salgencntex  41033  ovn0lem  41254  smfmullem3  41475  smfmullem4  41476  zm1nn  41795  m1mod0mod1  41818  fmtnosqrt  41930  perfectALTVlem2  42110  nnsum3primesprm  42157  nnsum4primesodd  42163  nnsum4primesoddALTV  42164  nnsum4primeseven  42167  nnsum4primesevenALTV  42168  tgblthelfgott  42182  tgoldbach  42184  tgblthelfgottOLD  42188  tgoldbachOLD  42191  expnegico01  42787  regt1loggt0  42809  rege1logbrege0  42831  rege1logbzge0  42832  blennnelnn  42849  dignnld  42876  nn0sumshdiglemA  42892  nn0sumshdiglem1  42894
  Copyright terms: Public domain W3C validator