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

Theorem 1re 9983
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 9938, 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 9949 . . 3 1 ≠ 0
2 ax-1cn 9938 . . . . 5 1 ∈ ℂ
3 cnre 9980 . . . . 5 (1 ∈ ℂ → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)))
42, 3ax-mp 5 . . . 4 𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏))
5 neeq1 2852 . . . . . . . 8 (1 = (𝑎 + (i · 𝑏)) → (1 ≠ 0 ↔ (𝑎 + (i · 𝑏)) ≠ 0))
65biimpcd 239 . . . . . . 7 (1 ≠ 0 → (1 = (𝑎 + (i · 𝑏)) → (𝑎 + (i · 𝑏)) ≠ 0))
7 0cn 9976 . . . . . . . 8 0 ∈ ℂ
8 cnre 9980 . . . . . . . 8 (0 ∈ ℂ → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)))
97, 8ax-mp 5 . . . . . . 7 𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑))
10 neeq2 2853 . . . . . . . . . 10 (0 = (𝑐 + (i · 𝑑)) → ((𝑎 + (i · 𝑏)) ≠ 0 ↔ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
1110biimpcd 239 . . . . . . . . 9 ((𝑎 + (i · 𝑏)) ≠ 0 → (0 = (𝑐 + (i · 𝑑)) → (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
1211reximdv 3010 . . . . . . . 8 ((𝑎 + (i · 𝑏)) ≠ 0 → (∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)) → ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
1312reximdv 3010 . . . . . . 7 ((𝑎 + (i · 𝑏)) ≠ 0 → (∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)) → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
146, 9, 13syl6mpi 67 . . . . . 6 (1 ≠ 0 → (1 = (𝑎 + (i · 𝑏)) → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
1514reximdv 3010 . . . . 5 (1 ≠ 0 → (∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)) → ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
1615reximdv 3010 . . . 4 (1 ≠ 0 → (∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)) → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
174, 16mpi 20 . . 3 (1 ≠ 0 → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)))
18 ioran 511 . . . . . . . . 9 (¬ (𝑎𝑐𝑏𝑑) ↔ (¬ 𝑎𝑐 ∧ ¬ 𝑏𝑑))
19 df-ne 2791 . . . . . . . . . . 11 (𝑎𝑐 ↔ ¬ 𝑎 = 𝑐)
2019con2bii 347 . . . . . . . . . 10 (𝑎 = 𝑐 ↔ ¬ 𝑎𝑐)
21 df-ne 2791 . . . . . . . . . . 11 (𝑏𝑑 ↔ ¬ 𝑏 = 𝑑)
2221con2bii 347 . . . . . . . . . 10 (𝑏 = 𝑑 ↔ ¬ 𝑏𝑑)
2320, 22anbi12i 732 . . . . . . . . 9 ((𝑎 = 𝑐𝑏 = 𝑑) ↔ (¬ 𝑎𝑐 ∧ ¬ 𝑏𝑑))
2418, 23bitr4i 267 . . . . . . . 8 (¬ (𝑎𝑐𝑏𝑑) ↔ (𝑎 = 𝑐𝑏 = 𝑑))
25 id 22 . . . . . . . . 9 (𝑎 = 𝑐𝑎 = 𝑐)
26 oveq2 6612 . . . . . . . . 9 (𝑏 = 𝑑 → (i · 𝑏) = (i · 𝑑))
2725, 26oveqan12d 6623 . . . . . . . 8 ((𝑎 = 𝑐𝑏 = 𝑑) → (𝑎 + (i · 𝑏)) = (𝑐 + (i · 𝑑)))
2824, 27sylbi 207 . . . . . . 7 (¬ (𝑎𝑐𝑏𝑑) → (𝑎 + (i · 𝑏)) = (𝑐 + (i · 𝑑)))
2928necon1ai 2817 . . . . . 6 ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → (𝑎𝑐𝑏𝑑))
30 neeq1 2852 . . . . . . . . . 10 (𝑥 = 𝑎 → (𝑥𝑦𝑎𝑦))
31 neeq2 2853 . . . . . . . . . 10 (𝑦 = 𝑐 → (𝑎𝑦𝑎𝑐))
3230, 31rspc2ev 3308 . . . . . . . . 9 ((𝑎 ∈ ℝ ∧ 𝑐 ∈ ℝ ∧ 𝑎𝑐) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥𝑦)
33323expia 1264 . . . . . . . 8 ((𝑎 ∈ ℝ ∧ 𝑐 ∈ ℝ) → (𝑎𝑐 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥𝑦))
3433ad2ant2r 782 . . . . . . 7 (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → (𝑎𝑐 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥𝑦))
35 neeq1 2852 . . . . . . . . . 10 (𝑥 = 𝑏 → (𝑥𝑦𝑏𝑦))
36 neeq2 2853 . . . . . . . . . 10 (𝑦 = 𝑑 → (𝑏𝑦𝑏𝑑))
3735, 36rspc2ev 3308 . . . . . . . . 9 ((𝑏 ∈ ℝ ∧ 𝑑 ∈ ℝ ∧ 𝑏𝑑) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥𝑦)
38373expia 1264 . . . . . . . 8 ((𝑏 ∈ ℝ ∧ 𝑑 ∈ ℝ) → (𝑏𝑑 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥𝑦))
3938ad2ant2l 781 . . . . . . 7 (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → (𝑏𝑑 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥𝑦))
4034, 39jaod 395 . . . . . 6 (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → ((𝑎𝑐𝑏𝑑) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥𝑦))
4129, 40syl5 34 . . . . 5 (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥𝑦))
4241rexlimdvva 3031 . . . 4 ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥𝑦))
4342rexlimivv 3029 . . 3 (∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥𝑦)
441, 17, 43mp2b 10 . 2 𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥𝑦
45 eqtr3 2642 . . . . . . . . 9 ((𝑥 = 0 ∧ 𝑦 = 0) → 𝑥 = 𝑦)
4645ex 450 . . . . . . . 8 (𝑥 = 0 → (𝑦 = 0 → 𝑥 = 𝑦))
4746necon3d 2811 . . . . . . 7 (𝑥 = 0 → (𝑥𝑦𝑦 ≠ 0))
48 neeq1 2852 . . . . . . . . 9 (𝑧 = 𝑦 → (𝑧 ≠ 0 ↔ 𝑦 ≠ 0))
4948rspcev 3295 . . . . . . . 8 ((𝑦 ∈ ℝ ∧ 𝑦 ≠ 0) → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)
5049expcom 451 . . . . . . 7 (𝑦 ≠ 0 → (𝑦 ∈ ℝ → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
5147, 50syl6 35 . . . . . 6 (𝑥 = 0 → (𝑥𝑦 → (𝑦 ∈ ℝ → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
5251com23 86 . . . . 5 (𝑥 = 0 → (𝑦 ∈ ℝ → (𝑥𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
5352adantld 483 . . . 4 (𝑥 = 0 → ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
54 neeq1 2852 . . . . . . . 8 (𝑧 = 𝑥 → (𝑧 ≠ 0 ↔ 𝑥 ≠ 0))
5554rspcev 3295 . . . . . . 7 ((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)
5655expcom 451 . . . . . 6 (𝑥 ≠ 0 → (𝑥 ∈ ℝ → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
5756adantrd 484 . . . . 5 (𝑥 ≠ 0 → ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
5857a1dd 50 . . . 4 (𝑥 ≠ 0 → ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
5953, 58pm2.61ine 2873 . . 3 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
6059rexlimivv 3029 . 2 (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)
61 ax-rrecex 9952 . . . 4 ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → ∃𝑥 ∈ ℝ (𝑧 · 𝑥) = 1)
62 remulcl 9965 . . . . . . 7 ((𝑧 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (𝑧 · 𝑥) ∈ ℝ)
6362adantlr 750 . . . . . 6 (((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) ∧ 𝑥 ∈ ℝ) → (𝑧 · 𝑥) ∈ ℝ)
64 eleq1 2686 . . . . . 6 ((𝑧 · 𝑥) = 1 → ((𝑧 · 𝑥) ∈ ℝ ↔ 1 ∈ ℝ))
6563, 64syl5ibcom 235 . . . . 5 (((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) ∧ 𝑥 ∈ ℝ) → ((𝑧 · 𝑥) = 1 → 1 ∈ ℝ))
6665rexlimdva 3024 . . . 4 ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → (∃𝑥 ∈ ℝ (𝑧 · 𝑥) = 1 → 1 ∈ ℝ))
6761, 66mpd 15 . . 3 ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → 1 ∈ ℝ)
6867rexlimiva 3021 . 2 (∃𝑧 ∈ ℝ 𝑧 ≠ 0 → 1 ∈ ℝ)
6944, 60, 68mp2b 10 1 1 ∈ ℝ
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wo 383  wa 384   = wceq 1480  wcel 1987  wne 2790  wrex 2908  (class class class)co 6604  cc 9878  cr 9879  0cc0 9880  1c1 9881  ici 9882   + caddc 9883   · cmul 9885
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-1cn 9938  ax-icn 9939  ax-addcl 9940  ax-mulcl 9942  ax-mulrcl 9943  ax-i2m1 9948  ax-1ne0 9949  ax-rrecex 9952  ax-cnre 9953
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-rab 2916  df-v 3188  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-nul 3892  df-if 4059  df-sn 4149  df-pr 4151  df-op 4155  df-uni 4403  df-br 4614  df-iota 5810  df-fv 5855  df-ov 6607
This theorem is referenced by:  0re  9984  1red  9999  dedekind  10144  peano2re  10153  mul02lem2  10157  addid1  10160  renegcl  10288  peano2rem  10292  0reALT  10322  0lt1  10494  0le1  10495  relin01  10496  1le1  10599  eqneg  10689  ltp1  10805  ltm1  10807  recgt0  10811  mulgt1  10826  ltmulgt11  10827  lemulge11  10829  reclt1  10862  recgt1  10863  recgt1i  10864  recp1lt1  10865  recreclt  10866  recgt0ii  10873  ledivp1i  10893  ltdivp1i  10894  inelr  10954  cju  10960  nnssre  10968  nnge1  10990  nngt1ne1  10991  nnle1eq1  10992  nngt0  10993  nnnlt1  10994  nnrecre  11001  nnrecgt0  11002  nnsub  11003  2re  11034  3re  11038  4re  11041  5re  11043  6re  11045  7re  11047  8re  11049  9re  11051  10reOLD  11053  0le2  11055  2pos  11056  3pos  11058  4pos  11060  5pos  11062  6pos  11063  7pos  11064  8pos  11065  9pos  11066  10posOLD  11067  neg1rr  11069  neg1lt0  11071  1lt2  11138  1lt3  11140  1lt4  11143  1lt5  11147  1lt6  11152  1lt7  11158  1lt8  11165  1lt9  11173  1lt10OLD  11182  1ne2  11184  1le2  11185  1le3  11188  halflt1  11194  addltmul  11212  nnunb  11232  elnnnn0c  11282  nn0ge2m1nn  11304  elnnz1  11347  znnnlt1  11348  zltp1le  11371  zleltp1  11372  nn0lt2  11384  recnz  11396  gtndiv  11398  3halfnz  11400  1lt10  11625  eluzp1m1  11655  eluzp1p1  11657  eluz2b2  11705  zbtwnre  11730  rebtwnz  11731  1rp  11780  divlt1lt  11843  divle1le  11844  nnledivrp  11884  qbtwnxr  11974  xmulid1  12052  xmulid2  12053  xmulm1  12054  x2times  12072  xrub  12085  0elunit  12232  1elunit  12233  divelunit  12256  lincmb01cmp  12257  iccf1o  12258  xov1plusxeqvd  12260  unitssre  12261  0nelfz1  12302  fzpreddisj  12332  fznatpl1  12337  fztpval  12344  fraclt1  12543  fracle1  12544  flbi2  12558  ico01fl0  12560  fldiv4p1lem1div2  12576  fldiv4lem1div2  12578  fldiv  12599  modid  12635  1mod  12642  m1modnnsub1  12656  modm1p1mod0  12661  seqf1olem1  12780  reexpcl  12817  reexpclz  12820  expge0  12836  expge1  12837  expgt1  12838  bernneq  12930  bernneq2  12931  expnbnd  12933  expnlbnd  12934  expnlbnd2  12935  expmulnbnd  12936  discr1  12940  facwordi  13016  faclbnd3  13019  faclbnd4lem1  13020  faclbnd4lem4  13023  faclbnd6  13026  facavg  13028  hashv01gt1  13073  hashge1  13118  hashnn0n0nn  13120  hash1snb  13147  hashgt12el  13150  hashgt12el2  13151  hashfun  13164  hashge2el2dif  13200  brfi1indALT  13221  brfi1indALTOLD  13227  lsw0  13291  f1oun2prg  13598  sgn1  13766  cjexp  13824  re1  13828  im1  13829  rei  13830  imi  13831  sqrlem1  13917  sqrlem2  13918  sqrlem3  13919  sqrlem4  13920  sqrlem7  13923  resqrex  13925  sqrt1  13946  sqrt2gt1lt2  13949  sqrtm1  13950  abs1  13971  absrdbnd  14015  caubnd2  14031  mulcn2  14260  reccn2  14261  rlimno1  14318  o1fsum  14472  expcnv  14521  geolim  14526  geolim2  14527  georeclim  14528  geomulcvg  14532  geoisumr  14534  geoisum1c  14536  geoihalfsum  14539  fprodreclf  14614  fprodge0  14649  fprodge1  14651  rerisefaccl  14673  refallfaccl  14674  ere  14744  ege2le3  14745  efgt1  14771  resin4p  14793  recos4p  14794  tanhbnd  14816  sinbnd  14835  cosbnd  14836  sinbnd2  14837  cosbnd2  14838  ef01bndlem  14839  sin01bnd  14840  cos01bnd  14841  cos1bnd  14842  cos2bnd  14843  sinltx  14844  sin01gt0  14845  cos01gt0  14846  sin02gt0  14847  sincos1sgn  14848  ene1  14863  rpnnen2lem2  14869  rpnnen2lem3  14870  rpnnen2lem4  14871  rpnnen2lem9  14876  rpnnen2lem12  14879  ruclem6  14889  ruclem11  14894  ruclem12  14895  3dvds  14976  3dvdsOLD  14977  halfleoddlt  15010  n2dvds1  15028  flodddiv4  15061  sadcadd  15104  isprm3  15320  sqnprm  15338  coprm  15347  phibndlem  15399  pythagtriplem3  15447  pcmpt  15520  fldivp1  15525  pockthi  15535  infpn2  15541  resslem  15854  basendxnmulrndx  15920  slotsbhcdif  16001  oppcbas  16299  rescbas  16410  rescabs  16414  odubas  17054  lt6abl  18217  srgbinomlem4  18464  abvneg  18755  abvtrivd  18761  isnzr2hash  19183  0ringnnzr  19188  cnfldfun  19677  xrsmcmn  19688  xrsnsgrp  19701  gzrngunitlem  19730  gzrngunit  19731  rge0srg  19736  psgnodpmr  19855  remulg  19872  resubdrg  19873  thlbas  19959  matbas  20138  leordtval2  20926  tuslem  21981  setsmsbas  22190  dscmet  22287  dscopn  22288  nrginvrcnlem  22405  nmoid  22456  idnghm  22457  tgioo  22507  blcvx  22509  metnrmlem1a  22569  metnrmlem1  22570  iicmp  22597  iiconn  22598  iirev  22636  iihalf1  22638  iihalf2  22640  iihalf2cn  22641  elii1  22642  elii2  22643  iimulcl  22644  icopnfcnv  22649  icopnfhmeo  22650  iccpnfcnv  22651  iccpnfhmeo  22652  xrhmeo  22653  xrhmph  22654  evth  22666  xlebnum  22672  lebnumii  22673  htpycc  22687  reparphti  22705  pcoval1  22721  pco1  22723  pcoval2  22724  pcocn  22725  pcohtpylem  22727  pcopt  22730  pcopt2  22731  pcoass  22732  pcorevlem  22734  nmhmcn  22828  ncvs1  22865  ovolunlem1a  23171  vitalilem2  23284  vitalilem4  23286  vitalilem5  23287  vitali  23288  i1f1  23363  itg11  23364  itg2const  23413  itg2monolem1  23423  itg2monolem3  23425  dveflem  23646  dvlipcn  23661  dvcvx  23687  ply1remlem  23826  fta1blem  23832  vieta1lem2  23970  aalioulem3  23993  aalioulem5  23995  aaliou3lem2  24002  ulmbdd  24056  iblulm  24065  radcnvlem1  24071  dvradcnv  24079  abelthlem2  24090  abelthlem3  24091  abelthlem5  24093  abelthlem7  24096  abelth  24099  abelth2  24100  reeff1olem  24104  reeff1o  24105  sinhalfpilem  24119  tangtx  24161  sincos4thpi  24169  pige3  24173  coskpi  24176  recosf1o  24185  tanregt0  24189  efif1olem3  24194  efif1olem4  24195  loge  24237  logdivlti  24270  logcnlem4  24291  logf1o2  24296  dvlog2lem  24298  logtayl  24306  logccv  24309  recxpcl  24321  cxplea  24342  cxpcn3lem  24388  cxpaddlelem  24392  loglesqrt  24399  logblog  24430  ang180lem2  24440  angpined  24457  chordthmlem4  24462  acosrecl  24530  atancj  24537  atanlogaddlem  24540  atantan  24550  atans2  24558  ressatans  24561  leibpi  24569  log2le1  24577  birthdaylem3  24580  cxp2lim  24603  cxploglim  24604  cxploglim2  24605  divsqrtsumlem  24606  cvxcl  24611  scvxcvx  24612  jensenlem2  24614  amgmlem  24616  emcllem2  24623  emcllem4  24625  emcllem6  24627  emcllem7  24628  emre  24632  emgt0  24633  harmonicbnd3  24634  harmonicubnd  24636  harmonicbnd4  24637  zetacvg  24641  lgamgulmlem2  24656  ftalem1  24699  ftalem2  24700  ftalem5  24703  issqf  24762  cht1  24791  chp1  24793  ppiltx  24803  mumullem2  24806  ppiublem1  24827  ppiub  24829  chtublem  24836  chtub  24837  logfacbnd3  24848  logexprlim  24850  perfectlem2  24855  dchrinv  24886  dchr1re  24888  efexple  24906  bposlem1  24909  bposlem2  24910  bposlem5  24913  bposlem8  24916  lgsdir2lem1  24950  lgsdir2lem5  24954  lgsdir  24957  lgsne0  24960  lgsabs1  24961  lgsdinn0  24970  gausslemma2dlem0i  24989  lgseisen  25004  m1lgs  25013  2lgslem3  25029  chebbnd1lem3  25060  chebbnd1  25061  chtppilimlem1  25062  chtppilimlem2  25063  chtppilim  25064  chpchtlim  25068  vmadivsumb  25072  rplogsumlem2  25074  rpvmasumlem  25076  dchrmusumlema  25082  dchrmusum2  25083  dchrvmasumlem2  25087  dchrvmasumiflem1  25090  dchrisum0flblem1  25097  dchrisum0flblem2  25098  dchrisum0fno1  25100  rpvmasum2  25101  dchrisum0re  25102  dchrisum0lema  25103  dchrisum0lem1b  25104  dchrisum0lem1  25105  dchrisum0lem2a  25106  dchrisum0lem2  25107  logdivsum  25122  mulog2sumlem2  25124  2vmadivsumlem  25129  log2sumbnd  25133  selbergb  25138  selberg2b  25141  chpdifbndlem1  25142  selberg3lem1  25146  selberg3lem2  25147  selberg4lem1  25149  pntrmax  25153  pntrsumo1  25154  selbergsb  25164  pntrlog2bndlem3  25168  pntrlog2bndlem5  25170  pntpbnd1a  25174  pntpbnd2  25176  pntibndlem1  25178  pntibndlem2  25180  pntibndlem3  25181  pntibnd  25182  pntlemd  25183  pntlemc  25184  pntlemb  25186  pntlemr  25191  pntlemf  25194  pntlemk  25195  pntlemo  25196  pntlem3  25198  pntleml  25200  pnt  25203  abvcxp  25204  ostth2lem1  25207  padicabvf  25220  padicabvcxp  25221  ostth1  25222  ostth2lem2  25223  ostth2lem3  25224  ostth2lem4  25225  ostth2  25226  ostth3  25227  ostth  25228  trgcgrg  25310  ttgcontlem1  25665  brbtwn2  25685  colinearalglem4  25689  ax5seglem1  25708  ax5seglem2  25709  ax5seglem3  25711  ax5seglem5  25713  ax5seglem6  25714  ax5seglem9  25717  ax5seg  25718  axbtwnid  25719  axpaschlem  25720  axpasch  25721  axlowdimlem6  25727  axlowdimlem10  25731  axlowdimlem16  25737  axlowdim1  25739  axlowdim2  25740  axlowdim  25741  axcontlem2  25745  axcontlem4  25747  axcontlem7  25750  lfgrnloop  25915  lfuhgr1v0e  26039  usgrexmpldifpr  26043  usgrexmplef  26044  1loopgrvd2  26285  vdegp1bi  26319  lfgrwlkprop  26453  pthdlem1  26531  pthdlem2  26533  upgr4cycl4dv4e  26911  konigsberglem2  26981  konigsberglem3  26982  konigsberglem5  26984  frgrwopreglem2  27040  frgrreg  27106  ex-dif  27134  ex-in  27136  ex-pss  27139  ex-res  27152  ex-fl  27158  nv1  27376  smcnlem  27398  ipidsq  27411  nmlno0lem  27494  norm-ii-i  27840  bcs2  27885  norm1  27952  nmopub2tALT  28614  nmfnleub2  28631  nmlnop0iALT  28700  nmopun  28719  unopbd  28720  nmopadjlem  28794  nmopcoadji  28806  pjnmopi  28853  pjbdlni  28854  stge0  28929  stle1  28930  hstle1  28931  hstle  28935  hstles  28936  stge1i  28943  stlesi  28946  staddi  28951  stadd3i  28953  strlem1  28955  strlem3a  28957  strlem5  28960  jplem1  28973  cdj1i  29138  addltmulALT  29151  xlt2addrd  29364  xdivrec  29417  xrsmulgzz  29460  xrnarchi  29520  resvbas  29614  rearchi  29624  xrge0slmod  29626  submateqlem1  29652  elunitrn  29722  elunitge0  29724  unitssxrge0  29725  unitdivcld  29726  xrge0iifcnv  29758  xrge0iifcv  29759  xrge0iifiso  29760  xrge0iifhom  29762  zrhre  29842  indf  29856  indfval  29857  pr01ssre  29858  esumcst  29903  hasheuni  29925  cntnevol  30069  ddemeas  30077  omssubadd  30140  iwrdsplit  30227  prob01  30253  dstfrvclim1  30317  coinfliprv  30322  ballotlem2  30328  ballotlem4  30338  ballotlemi1  30342  ballotlemic  30346  sgnclre  30379  sgnnbi  30385  sgnpbi  30386  sgnmulsgp  30390  plymulx0  30401  plymulx  30402  signswch  30415  signstf  30420  signsvfn  30436  subfacp1lem1  30866  subfacp1lem5  30871  resconn  30933  iisconn  30939  iillysconn  30940  snmlff  31016  problem2  31264  problem2OLD  31265  problem3  31266  sinccvglem  31271  fz0n  31321  dnizeq0  32104  dnibndlem12  32118  knoppcnlem4  32125  knoppndvlem13  32154  cnndvlem1  32167  relowlpssretop  32841  sin2h  33028  cos2h  33029  tan2h  33030  poimirlem7  33045  poimirlem16  33054  poimirlem17  33055  poimirlem19  33057  poimirlem20  33058  poimirlem22  33060  poimirlem23  33061  poimirlem29  33067  poimirlem30  33068  poimirlem31  33069  poimirlem32  33070  broucube  33072  itg2addnclem3  33092  asindmre  33124  dvasin  33125  dvacos  33126  dvreasin  33127  dvreacos  33128  areacirclem1  33129  fdc  33170  geomcau  33184  cntotbnd  33224  heiborlem8  33246  bfplem2  33251  bfp  33252  rabren3dioph  36856  pellexlem5  36874  pellexlem6  36875  pell1qrgaplem  36914  pell14qrgap  36916  pellqrex  36920  pellfundre  36922  pellfundlb  36925  pellfund14gap  36928  rmspecsqrtnqOLD  36948  jm2.17a  37004  acongeq  37027  jm2.23  37040  jm3.1lem2  37062  relexp01min  37483  imo72b2  37954  cvgdvgrat  37991  lhe4.4ex1a  38007  binomcxplemnotnn0  38034  isosctrlem1ALT  38650  supxrgelem  39014  xrlexaddrp  39029  infxr  39044  infleinflem2  39048  sumnnodd  39263  dvnprodlem3  39466  stoweidlem1  39522  stoweidlem18  39539  stoweidlem19  39540  stoweidlem26  39547  stoweidlem34  39555  stoweidlem40  39561  stoweidlem41  39562  stoweidlem59  39580  stoweid  39584  stirlinglem10  39604  stirlinglem11  39605  dirkercncflem1  39624  fourierdlem16  39644  fourierdlem21  39649  fourierdlem22  39650  fourierdlem42  39670  fourierdlem68  39695  fourierdlem83  39710  fourierdlem103  39730  sqwvfourb  39750  fouriersw  39752  etransclem23  39778  salexct2  39861  salgencntex  39865  ovn0lem  40083  smfmullem3  40304  smfmullem4  40305  zm1nn  40610  m1mod0mod1  40634  fmtnosqrt  40747  perfectALTVlem2  40923  nnsum3primesprm  40964  nnsum4primesodd  40970  nnsum4primesoddALTV  40971  nnsum4primeseven  40974  nnsum4primesevenALTV  40975  tgblthelfgott  40987  tgoldbach  40990  tgblthelfgottOLD  40994  tgoldbachOLD  40997  expnegico01  41593  regt1loggt0  41619  rege1logbrege0  41641  rege1logbzge0  41642  blennnelnn  41659  dignnld  41686  nn0sumshdiglemA  41702  nn0sumshdiglem1  41704
  Copyright terms: Public domain W3C validator