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

Theorem 1re 10077
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 10032, 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 10043 . . 3 1 ≠ 0
2 ax-1cn 10032 . . . . 5 1 ∈ ℂ
3 cnre 10074 . . . . 5 (1 ∈ ℂ → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)))
42, 3ax-mp 5 . . . 4 𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏))
5 neeq1 2885 . . . . . . . 8 (1 = (𝑎 + (i · 𝑏)) → (1 ≠ 0 ↔ (𝑎 + (i · 𝑏)) ≠ 0))
65biimpcd 239 . . . . . . 7 (1 ≠ 0 → (1 = (𝑎 + (i · 𝑏)) → (𝑎 + (i · 𝑏)) ≠ 0))
7 0cn 10070 . . . . . . . 8 0 ∈ ℂ
8 cnre 10074 . . . . . . . 8 (0 ∈ ℂ → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)))
97, 8ax-mp 5 . . . . . . 7 𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑))
10 neeq2 2886 . . . . . . . . . 10 (0 = (𝑐 + (i · 𝑑)) → ((𝑎 + (i · 𝑏)) ≠ 0 ↔ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
1110biimpcd 239 . . . . . . . . 9 ((𝑎 + (i · 𝑏)) ≠ 0 → (0 = (𝑐 + (i · 𝑑)) → (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
1211reximdv 3045 . . . . . . . 8 ((𝑎 + (i · 𝑏)) ≠ 0 → (∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)) → ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
1312reximdv 3045 . . . . . . 7 ((𝑎 + (i · 𝑏)) ≠ 0 → (∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)) → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
146, 9, 13syl6mpi 67 . . . . . 6 (1 ≠ 0 → (1 = (𝑎 + (i · 𝑏)) → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
1514reximdv 3045 . . . . 5 (1 ≠ 0 → (∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)) → ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
1615reximdv 3045 . . . 4 (1 ≠ 0 → (∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)) → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
174, 16mpi 20 . . 3 (1 ≠ 0 → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)))
18 ioran 510 . . . . . . . . 9 (¬ (𝑎𝑐𝑏𝑑) ↔ (¬ 𝑎𝑐 ∧ ¬ 𝑏𝑑))
19 df-ne 2824 . . . . . . . . . . 11 (𝑎𝑐 ↔ ¬ 𝑎 = 𝑐)
2019con2bii 346 . . . . . . . . . 10 (𝑎 = 𝑐 ↔ ¬ 𝑎𝑐)
21 df-ne 2824 . . . . . . . . . . 11 (𝑏𝑑 ↔ ¬ 𝑏 = 𝑑)
2221con2bii 346 . . . . . . . . . 10 (𝑏 = 𝑑 ↔ ¬ 𝑏𝑑)
2320, 22anbi12i 733 . . . . . . . . 9 ((𝑎 = 𝑐𝑏 = 𝑑) ↔ (¬ 𝑎𝑐 ∧ ¬ 𝑏𝑑))
2418, 23bitr4i 267 . . . . . . . 8 (¬ (𝑎𝑐𝑏𝑑) ↔ (𝑎 = 𝑐𝑏 = 𝑑))
25 id 22 . . . . . . . . 9 (𝑎 = 𝑐𝑎 = 𝑐)
26 oveq2 6698 . . . . . . . . 9 (𝑏 = 𝑑 → (i · 𝑏) = (i · 𝑑))
2725, 26oveqan12d 6709 . . . . . . . 8 ((𝑎 = 𝑐𝑏 = 𝑑) → (𝑎 + (i · 𝑏)) = (𝑐 + (i · 𝑑)))
2824, 27sylbi 207 . . . . . . 7 (¬ (𝑎𝑐𝑏𝑑) → (𝑎 + (i · 𝑏)) = (𝑐 + (i · 𝑑)))
2928necon1ai 2850 . . . . . 6 ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → (𝑎𝑐𝑏𝑑))
30 neeq1 2885 . . . . . . . . . 10 (𝑥 = 𝑎 → (𝑥𝑦𝑎𝑦))
31 neeq2 2886 . . . . . . . . . 10 (𝑦 = 𝑐 → (𝑎𝑦𝑎𝑐))
3230, 31rspc2ev 3355 . . . . . . . . 9 ((𝑎 ∈ ℝ ∧ 𝑐 ∈ ℝ ∧ 𝑎𝑐) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥𝑦)
33323expia 1286 . . . . . . . 8 ((𝑎 ∈ ℝ ∧ 𝑐 ∈ ℝ) → (𝑎𝑐 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥𝑦))
3433ad2ant2r 798 . . . . . . 7 (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → (𝑎𝑐 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥𝑦))
35 neeq1 2885 . . . . . . . . . 10 (𝑥 = 𝑏 → (𝑥𝑦𝑏𝑦))
36 neeq2 2886 . . . . . . . . . 10 (𝑦 = 𝑑 → (𝑏𝑦𝑏𝑑))
3735, 36rspc2ev 3355 . . . . . . . . 9 ((𝑏 ∈ ℝ ∧ 𝑑 ∈ ℝ ∧ 𝑏𝑑) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥𝑦)
38373expia 1286 . . . . . . . 8 ((𝑏 ∈ ℝ ∧ 𝑑 ∈ ℝ) → (𝑏𝑑 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥𝑦))
3938ad2ant2l 797 . . . . . . 7 (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → (𝑏𝑑 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥𝑦))
4034, 39jaod 394 . . . . . 6 (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → ((𝑎𝑐𝑏𝑑) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥𝑦))
4129, 40syl5 34 . . . . 5 (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥𝑦))
4241rexlimdvva 3067 . . . 4 ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥𝑦))
4342rexlimivv 3065 . . 3 (∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥𝑦)
441, 17, 43mp2b 10 . 2 𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥𝑦
45 eqtr3 2672 . . . . . . . . 9 ((𝑥 = 0 ∧ 𝑦 = 0) → 𝑥 = 𝑦)
4645ex 449 . . . . . . . 8 (𝑥 = 0 → (𝑦 = 0 → 𝑥 = 𝑦))
4746necon3d 2844 . . . . . . 7 (𝑥 = 0 → (𝑥𝑦𝑦 ≠ 0))
48 neeq1 2885 . . . . . . . . 9 (𝑧 = 𝑦 → (𝑧 ≠ 0 ↔ 𝑦 ≠ 0))
4948rspcev 3340 . . . . . . . 8 ((𝑦 ∈ ℝ ∧ 𝑦 ≠ 0) → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)
5049expcom 450 . . . . . . 7 (𝑦 ≠ 0 → (𝑦 ∈ ℝ → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
5147, 50syl6 35 . . . . . 6 (𝑥 = 0 → (𝑥𝑦 → (𝑦 ∈ ℝ → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
5251com23 86 . . . . 5 (𝑥 = 0 → (𝑦 ∈ ℝ → (𝑥𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
5352adantld 482 . . . 4 (𝑥 = 0 → ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
54 neeq1 2885 . . . . . . . 8 (𝑧 = 𝑥 → (𝑧 ≠ 0 ↔ 𝑥 ≠ 0))
5554rspcev 3340 . . . . . . 7 ((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)
5655expcom 450 . . . . . 6 (𝑥 ≠ 0 → (𝑥 ∈ ℝ → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
5756adantrd 483 . . . . 5 (𝑥 ≠ 0 → ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
5857a1dd 50 . . . 4 (𝑥 ≠ 0 → ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
5953, 58pm2.61ine 2906 . . 3 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
6059rexlimivv 3065 . 2 (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)
61 ax-rrecex 10046 . . . 4 ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → ∃𝑥 ∈ ℝ (𝑧 · 𝑥) = 1)
62 remulcl 10059 . . . . . . 7 ((𝑧 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (𝑧 · 𝑥) ∈ ℝ)
6362adantlr 751 . . . . . 6 (((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) ∧ 𝑥 ∈ ℝ) → (𝑧 · 𝑥) ∈ ℝ)
64 eleq1 2718 . . . . . 6 ((𝑧 · 𝑥) = 1 → ((𝑧 · 𝑥) ∈ ℝ ↔ 1 ∈ ℝ))
6563, 64syl5ibcom 235 . . . . 5 (((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) ∧ 𝑥 ∈ ℝ) → ((𝑧 · 𝑥) = 1 → 1 ∈ ℝ))
6665rexlimdva 3060 . . . 4 ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → (∃𝑥 ∈ ℝ (𝑧 · 𝑥) = 1 → 1 ∈ ℝ))
6761, 66mpd 15 . . 3 ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → 1 ∈ ℝ)
6867rexlimiva 3057 . 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 1523  wcel 2030  wne 2823  wrex 2942  (class class class)co 6690  cc 9972  cr 9973  0cc0 9974  1c1 9975  ici 9976   + caddc 9977   · cmul 9979
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-mulcl 10036  ax-mulrcl 10037  ax-i2m1 10042  ax-1ne0 10043  ax-rrecex 10046  ax-cnre 10047
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-br 4686  df-iota 5889  df-fv 5934  df-ov 6693
This theorem is referenced by:  0re  10078  1red  10093  dedekind  10238  peano2re  10247  mul02lem2  10251  addid1  10254  renegcl  10382  peano2rem  10386  0reALT  10416  0lt1  10588  0le1  10589  relin01  10590  1le1  10693  eqneg  10783  ltp1  10899  ltm1  10901  recgt0  10905  mulgt1  10920  ltmulgt11  10921  lemulge11  10923  reclt1  10956  recgt1  10957  recgt1i  10958  recp1lt1  10959  recreclt  10960  recgt0ii  10967  ledivp1i  10987  ltdivp1i  10988  inelr  11048  cju  11054  nnssre  11062  nnge1  11084  nngt1ne1  11085  nnle1eq1  11086  nngt0  11087  nnnlt1  11088  nnrecre  11095  nnrecgt0  11096  nnsub  11097  2re  11128  3re  11132  4re  11135  5re  11137  6re  11139  7re  11141  8re  11143  9re  11145  10reOLD  11147  0le2  11149  2pos  11150  3pos  11152  4pos  11154  5pos  11156  6pos  11157  7pos  11158  8pos  11159  9pos  11160  10posOLD  11161  neg1rr  11163  neg1lt0  11165  1lt2  11232  1lt3  11234  1lt4  11237  1lt5  11241  1lt6  11246  1lt7  11252  1lt8  11259  1lt9  11267  1lt10OLD  11276  1ne2  11278  1le2  11279  1le3  11282  halflt1  11288  addltmul  11306  nnunb  11326  elnnnn0c  11376  nn0ge2m1nn  11398  elnnz1  11441  znnnlt1  11442  zltp1le  11465  zleltp1  11466  nn0lt2  11478  recnz  11490  gtndiv  11492  3halfnz  11494  1lt10  11719  eluzp1m1  11749  eluzp1p1  11751  eluz2b2  11799  zbtwnre  11824  rebtwnz  11825  1rp  11874  divlt1lt  11937  divle1le  11938  nnledivrp  11978  qbtwnxr  12069  xmulid1  12147  xmulid2  12148  xmulm1  12149  x2times  12167  xrub  12180  0elunit  12328  1elunit  12329  divelunit  12352  lincmb01cmp  12353  iccf1o  12354  xov1plusxeqvd  12356  unitssre  12357  0nelfz1  12398  fzpreddisj  12428  fznatpl1  12433  fztpval  12440  fraclt1  12643  fracle1  12644  flbi2  12658  ico01fl0  12660  fldiv4p1lem1div2  12676  fldiv4lem1div2  12678  fldiv  12699  modid  12735  1mod  12742  m1modnnsub1  12756  modm1p1mod0  12761  seqf1olem1  12880  reexpcl  12917  reexpclz  12920  expge0  12936  expge1  12937  expgt1  12938  bernneq  13030  bernneq2  13031  expnbnd  13033  expnlbnd  13034  expnlbnd2  13035  expmulnbnd  13036  discr1  13040  facwordi  13116  faclbnd3  13119  faclbnd4lem1  13120  faclbnd4lem4  13123  faclbnd6  13126  facavg  13128  hashv01gt1  13173  hashge1  13216  hashnn0n0nn  13218  hash1snb  13245  hashgt12el  13248  hashgt12el2  13249  hashfun  13262  hashge2el2dif  13300  brfi1indALT  13320  lsw0  13385  f1oun2prg  13708  sgn1  13876  cjexp  13934  re1  13938  im1  13939  rei  13940  imi  13941  sqrlem1  14027  sqrlem2  14028  sqrlem3  14029  sqrlem4  14030  sqrlem7  14033  resqrex  14035  sqrt1  14056  sqrt2gt1lt2  14059  sqrtm1  14060  abs1  14081  absrdbnd  14125  caubnd2  14141  mulcn2  14370  reccn2  14371  rlimno1  14428  o1fsum  14589  expcnv  14640  geolim  14645  geolim2  14646  georeclim  14647  geomulcvg  14651  geoisumr  14653  geoisum1c  14655  geoihalfsum  14658  fprodreclf  14733  fprodge0  14768  fprodge1  14770  rerisefaccl  14792  refallfaccl  14793  ere  14863  ege2le3  14864  efgt1  14890  resin4p  14912  recos4p  14913  tanhbnd  14935  sinbnd  14954  cosbnd  14955  sinbnd2  14956  cosbnd2  14957  ef01bndlem  14958  sin01bnd  14959  cos01bnd  14960  cos1bnd  14961  cos2bnd  14962  sinltx  14963  sin01gt0  14964  cos01gt0  14965  sin02gt0  14966  sincos1sgn  14967  ene1  14982  rpnnen2lem2  14988  rpnnen2lem3  14989  rpnnen2lem4  14990  rpnnen2lem9  14995  rpnnen2lem12  14998  ruclem6  15008  ruclem11  15013  ruclem12  15014  3dvds  15099  3dvdsOLD  15100  halfleoddlt  15133  n2dvds1  15151  flodddiv4  15184  sadcadd  15227  isprm3  15443  sqnprm  15461  coprm  15470  phibndlem  15522  pythagtriplem3  15570  pcmpt  15643  fldivp1  15648  pockthi  15658  infpn2  15664  resslem  15980  basendxnmulrndx  16046  slotsbhcdif  16127  oppcbas  16425  rescbas  16536  rescabs  16540  odubas  17180  lt6abl  18342  srgbinomlem4  18589  abvneg  18882  abvtrivd  18888  rmodislmod  18979  isnzr2hash  19312  0ringnnzr  19317  cnfldfun  19806  xrsmcmn  19817  xrsnsgrp  19830  gzrngunitlem  19859  gzrngunit  19860  rge0srg  19865  psgnodpmr  19984  remulg  20001  resubdrg  20002  thlbas  20088  matbas  20267  leordtval2  21064  tuslem  22118  setsmsbas  22327  dscmet  22424  dscopn  22425  nrginvrcnlem  22542  nmoid  22593  idnghm  22594  tgioo  22646  blcvx  22648  metnrmlem1a  22708  metnrmlem1  22709  iicmp  22736  iiconn  22737  iirev  22775  iihalf1  22777  iihalf2  22779  iihalf2cn  22780  elii1  22781  elii2  22782  iimulcl  22783  icopnfcnv  22788  icopnfhmeo  22789  iccpnfcnv  22790  iccpnfhmeo  22791  xrhmeo  22792  xrhmph  22793  evth  22805  xlebnum  22811  lebnumii  22812  htpycc  22826  reparphti  22843  pcoval1  22859  pco1  22861  pcoval2  22862  pcocn  22863  pcohtpylem  22865  pcopt  22868  pcopt2  22869  pcoass  22870  pcorevlem  22872  nmhmcn  22966  ncvs1  23003  ovolunlem1a  23310  vitalilem2  23423  vitalilem4  23425  vitalilem5  23426  vitali  23427  i1f1  23502  itg11  23503  itg2const  23552  itg2monolem1  23562  itg2monolem3  23564  dveflem  23787  dvlipcn  23802  dvcvx  23828  ply1remlem  23967  fta1blem  23973  vieta1lem2  24111  aalioulem3  24134  aalioulem5  24136  aaliou3lem2  24143  ulmbdd  24197  iblulm  24206  radcnvlem1  24212  dvradcnv  24220  abelthlem2  24231  abelthlem3  24232  abelthlem5  24234  abelthlem7  24237  abelth  24240  abelth2  24241  reeff1olem  24245  reeff1o  24246  sinhalfpilem  24260  tangtx  24302  sincos4thpi  24310  pige3  24314  coskpi  24317  recosf1o  24326  tanregt0  24330  efif1olem3  24335  efif1olem4  24336  loge  24378  logdivlti  24411  logcnlem4  24436  logf1o2  24441  dvlog2lem  24443  logtayl  24451  logccv  24454  recxpcl  24466  cxplea  24487  cxpcn3lem  24533  cxpaddlelem  24537  loglesqrt  24544  logblog  24575  ang180lem2  24585  angpined  24602  chordthmlem4  24607  acosrecl  24675  atancj  24682  atanlogaddlem  24685  atantan  24695  atans2  24703  ressatans  24706  leibpi  24714  log2le1  24722  birthdaylem3  24725  cxp2lim  24748  cxploglim  24749  cxploglim2  24750  divsqrtsumlem  24751  cvxcl  24756  scvxcvx  24757  jensenlem2  24759  amgmlem  24761  emcllem2  24768  emcllem4  24770  emcllem6  24772  emcllem7  24773  emre  24777  emgt0  24778  harmonicbnd3  24779  harmonicubnd  24781  harmonicbnd4  24782  zetacvg  24786  lgamgulmlem2  24801  ftalem1  24844  ftalem2  24845  ftalem5  24848  issqf  24907  cht1  24936  chp1  24938  ppiltx  24948  mumullem2  24951  ppiublem1  24972  ppiub  24974  chtublem  24981  chtub  24982  logfacbnd3  24993  logexprlim  24995  perfectlem2  25000  dchrinv  25031  dchr1re  25033  efexple  25051  bposlem1  25054  bposlem2  25055  bposlem5  25058  bposlem8  25061  lgsdir2lem1  25095  lgsdir2lem5  25099  lgsdir  25102  lgsne0  25105  lgsabs1  25106  lgsdinn0  25115  gausslemma2dlem0i  25134  lgseisen  25149  m1lgs  25158  2lgslem3  25174  chebbnd1lem3  25205  chebbnd1  25206  chtppilimlem1  25207  chtppilimlem2  25208  chtppilim  25209  chpchtlim  25213  vmadivsumb  25217  rplogsumlem2  25219  rpvmasumlem  25221  dchrmusumlema  25227  dchrmusum2  25228  dchrvmasumlem2  25232  dchrvmasumiflem1  25235  dchrisum0flblem1  25242  dchrisum0flblem2  25243  dchrisum0fno1  25245  rpvmasum2  25246  dchrisum0re  25247  dchrisum0lema  25248  dchrisum0lem1b  25249  dchrisum0lem1  25250  dchrisum0lem2a  25251  dchrisum0lem2  25252  logdivsum  25267  mulog2sumlem2  25269  2vmadivsumlem  25274  log2sumbnd  25278  selbergb  25283  selberg2b  25286  chpdifbndlem1  25287  selberg3lem1  25291  selberg3lem2  25292  selberg4lem1  25294  pntrmax  25298  pntrsumo1  25299  selbergsb  25309  pntrlog2bndlem3  25313  pntrlog2bndlem5  25315  pntpbnd1a  25319  pntpbnd2  25321  pntibndlem1  25323  pntibndlem2  25325  pntibndlem3  25326  pntibnd  25327  pntlemd  25328  pntlemc  25329  pntlemb  25331  pntlemr  25336  pntlemf  25339  pntlemk  25340  pntlemo  25341  pntlem3  25343  pntleml  25345  pnt  25348  abvcxp  25349  ostth2lem1  25352  padicabvf  25365  padicabvcxp  25366  ostth1  25367  ostth2lem2  25368  ostth2lem3  25369  ostth2lem4  25370  ostth2  25371  ostth3  25372  ostth  25373  trgcgrg  25455  ttgcontlem1  25810  brbtwn2  25830  colinearalglem4  25834  ax5seglem1  25853  ax5seglem2  25854  ax5seglem3  25856  ax5seglem5  25858  ax5seglem6  25859  ax5seglem9  25862  ax5seg  25863  axbtwnid  25864  axpaschlem  25865  axpasch  25866  axlowdimlem6  25872  axlowdimlem10  25876  axlowdimlem16  25882  axlowdim1  25884  axlowdim2  25885  axlowdim  25886  axcontlem2  25890  axcontlem4  25892  axcontlem7  25895  lfgrnloop  26065  lfuhgr1v0e  26191  usgrexmpldifpr  26195  usgrexmplef  26196  1loopgrvd2  26455  vdegp1bi  26489  lfgrwlkprop  26640  pthdlem1  26718  pthdlem2  26720  upgr4cycl4dv4e  27163  konigsberglem2  27231  konigsberglem3  27232  konigsberglem5  27234  frgrreg  27381  ex-dif  27410  ex-in  27412  ex-pss  27415  ex-res  27428  ex-fl  27434  nv1  27658  smcnlem  27680  ipidsq  27693  nmlno0lem  27776  norm-ii-i  28122  bcs2  28167  norm1  28234  nmopub2tALT  28896  nmfnleub2  28913  nmlnop0iALT  28982  nmopun  29001  unopbd  29002  nmopadjlem  29076  nmopcoadji  29088  pjnmopi  29135  pjbdlni  29136  stge0  29211  stle1  29212  hstle1  29213  hstle  29217  hstles  29218  stge1i  29225  stlesi  29228  staddi  29233  stadd3i  29235  strlem1  29237  strlem3a  29239  strlem5  29242  jplem1  29255  cdj1i  29420  addltmulALT  29433  xlt2addrd  29651  pr01ssre  29698  dp2lt10  29719  dp2ltsuc  29721  dp2ltc  29722  dplti  29741  dpmul4  29750  xdivrec  29763  xrsmulgzz  29806  xrnarchi  29866  resvbas  29960  rearchi  29970  xrge0slmod  29972  submateqlem1  30001  elunitrn  30071  elunitge0  30073  unitssxrge0  30074  unitdivcld  30075  xrge0iifcnv  30107  xrge0iifcv  30108  xrge0iifiso  30109  xrge0iifhom  30111  zrhre  30191  indf  30205  indfval  30206  esumcst  30253  hasheuni  30275  cntnevol  30419  ddemeas  30427  omssubadd  30490  iwrdsplit  30577  prob01  30603  dstfrvclim1  30667  coinfliprv  30672  ballotlem2  30678  ballotlem4  30688  ballotlemi1  30692  ballotlemic  30696  sgnclre  30729  sgnnbi  30735  sgnpbi  30736  sgnmulsgp  30740  plymulx0  30752  plymulx  30753  signswch  30766  signstf  30771  signsvfn  30787  itgexpif  30812  hgt750lemd  30854  logdivsqrle  30856  hgt750lem  30857  hgt750lem2  30858  hgt750leme  30864  tgoldbachgnn  30865  subfacp1lem1  31287  subfacp1lem5  31292  resconn  31354  iisconn  31360  iillysconn  31361  snmlff  31437  problem2  31685  problem2OLD  31686  problem3  31687  sinccvglem  31692  fz0n  31742  dnizeq0  32590  dnibndlem12  32604  knoppcnlem4  32611  knoppndvlem13  32640  cnndvlem1  32653  relowlpssretop  33342  sin2h  33529  cos2h  33530  tan2h  33531  poimirlem7  33546  poimirlem16  33555  poimirlem17  33556  poimirlem19  33558  poimirlem20  33559  poimirlem22  33561  poimirlem23  33562  poimirlem29  33568  poimirlem30  33569  poimirlem31  33570  poimirlem32  33571  broucube  33573  itg2addnclem3  33593  asindmre  33625  dvasin  33626  dvacos  33627  dvreasin  33628  dvreacos  33629  areacirclem1  33630  fdc  33671  geomcau  33685  cntotbnd  33725  heiborlem8  33747  bfplem2  33752  bfp  33753  rabren3dioph  37696  pellexlem5  37714  pellexlem6  37715  pell1qrgaplem  37754  pell14qrgap  37756  pellqrex  37760  pellfundre  37762  pellfundlb  37765  pellfund14gap  37768  rmspecsqrtnqOLD  37788  jm2.17a  37844  acongeq  37867  jm2.23  37880  jm3.1lem2  37902  relexp01min  38322  imo72b2  38792  cvgdvgrat  38829  lhe4.4ex1a  38845  binomcxplemnotnn0  38872  isosctrlem1ALT  39484  supxrgelem  39866  xrlexaddrp  39881  infxr  39896  infleinflem2  39900  1xr  39999  sumnnodd  40180  limsup10exlem  40322  limsup10ex  40323  liminf10ex  40324  dvnprodlem3  40481  stoweidlem1  40536  stoweidlem18  40553  stoweidlem19  40554  stoweidlem26  40561  stoweidlem34  40569  stoweidlem40  40575  stoweidlem41  40576  stoweidlem59  40594  stoweid  40598  stirlinglem10  40618  stirlinglem11  40619  dirkercncflem1  40638  fourierdlem16  40658  fourierdlem21  40663  fourierdlem22  40664  fourierdlem42  40684  fourierdlem68  40709  fourierdlem83  40724  fourierdlem103  40744  sqwvfourb  40764  fouriersw  40766  etransclem23  40792  salexct2  40875  salgencntex  40879  ovn0lem  41100  smfmullem3  41321  smfmullem4  41322  zm1nn  41641  m1mod0mod1  41664  fmtnosqrt  41776  perfectALTVlem2  41956  nnsum3primesprm  42003  nnsum4primesodd  42009  nnsum4primesoddALTV  42010  nnsum4primeseven  42013  nnsum4primesevenALTV  42014  tgblthelfgott  42028  tgoldbach  42030  tgblthelfgottOLD  42034  tgoldbachOLD  42037  expnegico01  42633  regt1loggt0  42655  rege1logbrege0  42677  rege1logbzge0  42678  blennnelnn  42695  dignnld  42722  nn0sumshdiglemA  42738  nn0sumshdiglem1  42740
  Copyright terms: Public domain W3C validator