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

Theorem 1re 10634
Description: The number 1 is real. 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 10588, 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 10599 . . 3 1 ≠ 0
2 ax-1cn 10588 . . . . 5 1 ∈ ℂ
3 cnre 10631 . . . . 5 (1 ∈ ℂ → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)))
42, 3ax-mp 5 . . . 4 𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏))
5 neeq1 3052 . . . . . . . 8 (1 = (𝑎 + (i · 𝑏)) → (1 ≠ 0 ↔ (𝑎 + (i · 𝑏)) ≠ 0))
65biimpcd 252 . . . . . . 7 (1 ≠ 0 → (1 = (𝑎 + (i · 𝑏)) → (𝑎 + (i · 𝑏)) ≠ 0))
7 0cn 10626 . . . . . . . 8 0 ∈ ℂ
8 cnre 10631 . . . . . . . 8 (0 ∈ ℂ → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)))
97, 8ax-mp 5 . . . . . . 7 𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑))
10 neeq2 3053 . . . . . . . . . 10 (0 = (𝑐 + (i · 𝑑)) → ((𝑎 + (i · 𝑏)) ≠ 0 ↔ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
1110biimpcd 252 . . . . . . . . 9 ((𝑎 + (i · 𝑏)) ≠ 0 → (0 = (𝑐 + (i · 𝑑)) → (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
1211reximdv 3235 . . . . . . . 8 ((𝑎 + (i · 𝑏)) ≠ 0 → (∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)) → ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
1312reximdv 3235 . . . . . . 7 ((𝑎 + (i · 𝑏)) ≠ 0 → (∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)) → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
146, 9, 13syl6mpi 67 . . . . . 6 (1 ≠ 0 → (1 = (𝑎 + (i · 𝑏)) → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
1514reximdv 3235 . . . . 5 (1 ≠ 0 → (∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)) → ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
1615reximdv 3235 . . . 4 (1 ≠ 0 → (∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)) → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
174, 16mpi 20 . . 3 (1 ≠ 0 → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)))
18 ioran 981 . . . . . . . . 9 (¬ (𝑎𝑐𝑏𝑑) ↔ (¬ 𝑎𝑐 ∧ ¬ 𝑏𝑑))
19 df-ne 2991 . . . . . . . . . . 11 (𝑎𝑐 ↔ ¬ 𝑎 = 𝑐)
2019con2bii 361 . . . . . . . . . 10 (𝑎 = 𝑐 ↔ ¬ 𝑎𝑐)
21 df-ne 2991 . . . . . . . . . . 11 (𝑏𝑑 ↔ ¬ 𝑏 = 𝑑)
2221con2bii 361 . . . . . . . . . 10 (𝑏 = 𝑑 ↔ ¬ 𝑏𝑑)
2320, 22anbi12i 629 . . . . . . . . 9 ((𝑎 = 𝑐𝑏 = 𝑑) ↔ (¬ 𝑎𝑐 ∧ ¬ 𝑏𝑑))
2418, 23bitr4i 281 . . . . . . . 8 (¬ (𝑎𝑐𝑏𝑑) ↔ (𝑎 = 𝑐𝑏 = 𝑑))
25 id 22 . . . . . . . . 9 (𝑎 = 𝑐𝑎 = 𝑐)
26 oveq2 7147 . . . . . . . . 9 (𝑏 = 𝑑 → (i · 𝑏) = (i · 𝑑))
2725, 26oveqan12d 7158 . . . . . . . 8 ((𝑎 = 𝑐𝑏 = 𝑑) → (𝑎 + (i · 𝑏)) = (𝑐 + (i · 𝑑)))
2824, 27sylbi 220 . . . . . . 7 (¬ (𝑎𝑐𝑏𝑑) → (𝑎 + (i · 𝑏)) = (𝑐 + (i · 𝑑)))
2928necon1ai 3017 . . . . . 6 ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → (𝑎𝑐𝑏𝑑))
30 neeq1 3052 . . . . . . . . . 10 (𝑥 = 𝑎 → (𝑥𝑦𝑎𝑦))
31 neeq2 3053 . . . . . . . . . 10 (𝑦 = 𝑐 → (𝑎𝑦𝑎𝑐))
3230, 31rspc2ev 3586 . . . . . . . . 9 ((𝑎 ∈ ℝ ∧ 𝑐 ∈ ℝ ∧ 𝑎𝑐) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥𝑦)
33323expia 1118 . . . . . . . 8 ((𝑎 ∈ ℝ ∧ 𝑐 ∈ ℝ) → (𝑎𝑐 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥𝑦))
3433ad2ant2r 746 . . . . . . 7 (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → (𝑎𝑐 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥𝑦))
35 neeq1 3052 . . . . . . . . . 10 (𝑥 = 𝑏 → (𝑥𝑦𝑏𝑦))
36 neeq2 3053 . . . . . . . . . 10 (𝑦 = 𝑑 → (𝑏𝑦𝑏𝑑))
3735, 36rspc2ev 3586 . . . . . . . . 9 ((𝑏 ∈ ℝ ∧ 𝑑 ∈ ℝ ∧ 𝑏𝑑) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥𝑦)
38373expia 1118 . . . . . . . 8 ((𝑏 ∈ ℝ ∧ 𝑑 ∈ ℝ) → (𝑏𝑑 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥𝑦))
3938ad2ant2l 745 . . . . . . 7 (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → (𝑏𝑑 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥𝑦))
4034, 39jaod 856 . . . . . 6 (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → ((𝑎𝑐𝑏𝑑) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥𝑦))
4129, 40syl5 34 . . . . 5 (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥𝑦))
4241rexlimdvva 3256 . . . 4 ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥𝑦))
4342rexlimivv 3254 . . 3 (∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥𝑦)
441, 17, 43mp2b 10 . 2 𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥𝑦
45 eqtr3 2823 . . . . . . . . 9 ((𝑥 = 0 ∧ 𝑦 = 0) → 𝑥 = 𝑦)
4645ex 416 . . . . . . . 8 (𝑥 = 0 → (𝑦 = 0 → 𝑥 = 𝑦))
4746necon3d 3011 . . . . . . 7 (𝑥 = 0 → (𝑥𝑦𝑦 ≠ 0))
48 neeq1 3052 . . . . . . . . 9 (𝑧 = 𝑦 → (𝑧 ≠ 0 ↔ 𝑦 ≠ 0))
4948rspcev 3574 . . . . . . . 8 ((𝑦 ∈ ℝ ∧ 𝑦 ≠ 0) → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)
5049expcom 417 . . . . . . 7 (𝑦 ≠ 0 → (𝑦 ∈ ℝ → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
5147, 50syl6 35 . . . . . 6 (𝑥 = 0 → (𝑥𝑦 → (𝑦 ∈ ℝ → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
5251com23 86 . . . . 5 (𝑥 = 0 → (𝑦 ∈ ℝ → (𝑥𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
5352adantld 494 . . . 4 (𝑥 = 0 → ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
54 neeq1 3052 . . . . . . . 8 (𝑧 = 𝑥 → (𝑧 ≠ 0 ↔ 𝑥 ≠ 0))
5554rspcev 3574 . . . . . . 7 ((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)
5655expcom 417 . . . . . 6 (𝑥 ≠ 0 → (𝑥 ∈ ℝ → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
5756adantrd 495 . . . . 5 (𝑥 ≠ 0 → ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
5857a1dd 50 . . . 4 (𝑥 ≠ 0 → ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
5953, 58pm2.61ine 3073 . . 3 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
6059rexlimivv 3254 . 2 (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)
61 ax-rrecex 10602 . . . 4 ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → ∃𝑥 ∈ ℝ (𝑧 · 𝑥) = 1)
62 remulcl 10615 . . . . . . 7 ((𝑧 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (𝑧 · 𝑥) ∈ ℝ)
6362adantlr 714 . . . . . 6 (((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) ∧ 𝑥 ∈ ℝ) → (𝑧 · 𝑥) ∈ ℝ)
64 eleq1 2880 . . . . . 6 ((𝑧 · 𝑥) = 1 → ((𝑧 · 𝑥) ∈ ℝ ↔ 1 ∈ ℝ))
6563, 64syl5ibcom 248 . . . . 5 (((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) ∧ 𝑥 ∈ ℝ) → ((𝑧 · 𝑥) = 1 → 1 ∈ ℝ))
6665rexlimdva 3246 . . . 4 ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → (∃𝑥 ∈ ℝ (𝑧 · 𝑥) = 1 → 1 ∈ ℝ))
6761, 66mpd 15 . . 3 ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → 1 ∈ ℝ)
6867rexlimiva 3243 . 2 (∃𝑧 ∈ ℝ 𝑧 ≠ 0 → 1 ∈ ℝ)
6944, 60, 68mp2b 10 1 1 ∈ ℝ
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 399  wo 844   = wceq 1538  wcel 2112  wne 2990  wrex 3110  (class class class)co 7139  cc 10528  cr 10529  0cc0 10530  1c1 10531  ici 10532   + caddc 10533   · cmul 10535
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-ext 2773  ax-1cn 10588  ax-icn 10589  ax-addcl 10590  ax-mulcl 10592  ax-mulrcl 10593  ax-i2m1 10598  ax-1ne0 10599  ax-rrecex 10602  ax-cnre 10603
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-ex 1782  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-ne 2991  df-ral 3114  df-rex 3115  df-v 3446  df-un 3889  df-in 3891  df-ss 3901  df-sn 4529  df-pr 4531  df-op 4535  df-uni 4804  df-br 5034  df-iota 6287  df-fv 6336  df-ov 7142
This theorem is referenced by:  1red  10635  1xr  10693  dedekind  10796  peano2re  10806  mul02lem2  10810  addid1  10813  renegcl  10942  peano2rem  10946  0reALT  10976  0lt1  11155  0le1  11156  relin01  11157  1le1  11261  eqneg  11353  ltp1  11473  ltm1  11475  recgt0  11479  mulgt1  11492  ltmulgt11  11493  lemulge11  11495  reclt1  11528  recgt1  11529  recgt1i  11530  recp1lt1  11531  recreclt  11532  recgt0ii  11539  ledivp1i  11558  ltdivp1i  11559  inelr  11619  cju  11625  nnssre  11633  nnge1  11657  nngt1ne1  11658  nnle1eq1  11659  nngt0  11660  nnnlt1  11661  nnne0  11663  nnrecre  11671  nnrecgt0  11672  nnsub  11673  2re  11703  3re  11709  4re  11713  5re  11716  6re  11719  7re  11722  8re  11725  9re  11728  0le2  11731  2pos  11732  3pos  11734  4pos  11736  5pos  11738  6pos  11739  7pos  11740  8pos  11741  9pos  11742  neg1rr  11744  neg1lt0  11746  1lt2  11800  1lt3  11802  1lt4  11805  1lt5  11809  1lt6  11814  1lt7  11820  1lt8  11827  1lt9  11835  1ne2  11837  1le2  11838  1le3  11841  halflt1  11847  addltmul  11865  nnunb  11885  elnnnn0c  11934  nn0ge2m1nn  11956  elnnz1  12000  znnnlt1  12001  zltp1le  12024  zleltp1  12025  nn0lt2  12037  recnz  12049  gtndiv  12051  3halfnz  12053  10re  12109  1lt10  12229  eluzp1m1  12260  eluzp1p1  12262  eluz2b2  12313  zbtwnre  12338  rebtwnz  12339  1rp  12385  divlt1lt  12450  divle1le  12451  nnledivrp  12493  qbtwnxr  12585  xmulid1  12664  xmulm1  12666  x2times  12684  xrub  12697  elicc01  12848  1elunit  12852  divelunit  12876  lincmb01cmp  12877  unitssre  12881  0nelfz1  12925  fzpreddisj  12955  fznatpl1  12960  fztpval  12968  fraclt1  13171  fracle1  13172  flbi2  13186  fldiv4p1lem1div2  13204  fldiv4lem1div2  13206  fldiv  13227  modid  13263  1mod  13270  m1modnnsub1  13284  modm1p1mod0  13289  seqf1olem1  13409  reexpcl  13446  reexpclz  13449  expge0  13465  expge1  13466  expgt1  13467  bernneq  13590  bernneq2  13591  expnbnd  13593  expnlbnd  13594  expnlbnd2  13595  expmulnbnd  13596  discr1  13600  facwordi  13649  faclbnd3  13652  faclbnd4lem1  13653  faclbnd4lem4  13656  faclbnd6  13659  facavg  13661  hashv01gt1  13705  hashnn0n0nn  13752  hashunsnggt  13755  hash1snb  13780  hashgt12el  13783  hashgt12el2  13784  hashfun  13798  hashge2el2dif  13838  lsw0  13912  f1oun2prg  14274  cjexp  14504  re1  14508  im1  14509  rei  14510  imi  14511  sqrlem1  14597  sqrlem2  14598  sqrlem3  14599  sqrlem4  14600  sqrlem7  14603  resqrex  14605  sqrt1  14626  sqrt2gt1lt2  14629  sqrtm1  14630  abs1  14652  absrdbnd  14696  caubnd2  14712  mulcn2  14947  reccn2  14948  rlimno1  15005  o1fsum  15163  expcnv  15214  geolim  15221  geolim2  15222  georeclim  15223  geomulcvg  15227  geoisumr  15229  geoisum1c  15231  fprodge0  15342  fprodge1  15344  rerisefaccl  15366  refallfaccl  15367  ere  15437  ege2le3  15438  efgt1  15464  resin4p  15486  recos4p  15487  tanhbnd  15509  sinbnd  15528  cosbnd  15529  sinbnd2  15530  cosbnd2  15531  ef01bndlem  15532  sin01bnd  15533  cos01bnd  15534  cos1bnd  15535  cos2bnd  15536  sinltx  15537  sin01gt0  15538  cos01gt0  15539  sin02gt0  15540  sincos1sgn  15541  ene1  15558  rpnnen2lem2  15563  rpnnen2lem3  15564  rpnnen2lem4  15565  rpnnen2lem9  15570  rpnnen2lem12  15573  ruclem6  15583  ruclem11  15588  ruclem12  15589  3dvds  15675  flodddiv4  15757  sadcadd  15800  isprm3  16020  sqnprm  16039  coprm  16048  phibndlem  16100  pythagtriplem3  16148  pcmpt  16221  fldivp1  16226  pockthi  16236  infpn2  16242  resslem  16552  basendxnmulrndx  16613  slotsbhcdif  16688  oppcbas  16983  rescbas  17094  rescabs  17098  odubas  17738  symgvalstruct  18520  lt6abl  19011  srgbinomlem4  19289  abvneg  19601  abvtrivd  19607  rmodislmod  19698  0ringnnzr  20038  cnfldfun  20106  xrsmcmn  20117  xrsnsgrp  20130  gzrngunitlem  20159  gzrngunit  20160  rge0srg  20165  psgnodpmr  20282  remulg  20299  resubdrg  20300  thlbas  20388  tuslem  22876  setsmsbas  23085  dscmet  23182  dscopn  23183  nrginvrcnlem  23300  idnghm  23352  tgioo  23404  blcvx  23406  iicmp  23494  iiconn  23495  iirev  23537  iihalf1  23539  iihalf2  23541  iihalf2cn  23542  elii1  23543  elii2  23544  iimulcl  23545  icopnfcnv  23550  icopnfhmeo  23551  iccpnfhmeo  23553  xrhmeo  23554  xrhmph  23555  evth  23567  xlebnum  23573  htpycc  23588  reparphti  23605  pcoval1  23621  pco1  23623  pcoval2  23624  pcocn  23625  pcohtpylem  23627  pcopt  23630  pcopt2  23631  pcoass  23632  pcorevlem  23634  nmhmcn  23728  ncvs1  23765  ovolunlem1a  24103  vitalilem2  24216  vitalilem4  24218  vitalilem5  24219  vitali  24220  i1f1  24297  itg11  24298  itg2const  24347  dveflem  24585  dvlipcn  24600  dvcvx  24626  ply1remlem  24766  fta1blem  24772  vieta1lem2  24910  aalioulem3  24933  aalioulem5  24935  aaliou3lem2  24942  ulmbdd  24996  iblulm  25005  radcnvlem1  25011  dvradcnv  25019  abelthlem2  25030  abelthlem3  25031  abelthlem5  25033  abelthlem7  25036  abelth  25039  abelth2  25040  reeff1olem  25044  reeff1o  25045  sinhalfpilem  25059  tangtx  25101  sincos4thpi  25109  pige3ALT  25115  coskpi  25118  cos0pilt1  25127  recosf1o  25130  tanregt0  25134  efif1olem3  25139  efif1olem4  25140  loge  25181  logdivlti  25214  logcnlem4  25239  logf1o2  25244  logtayl  25254  logccv  25257  recxpcl  25269  cxplea  25290  cxpcn3lem  25339  cxpaddlelem  25343  loglesqrt  25350  ang180lem2  25399  angpined  25419  acosrecl  25492  atancj  25499  atanlogaddlem  25502  atantan  25512  atans2  25520  ressatans  25523  leibpi  25531  log2le1  25539  birthdaylem3  25542  cxp2lim  25565  cxploglim  25566  cxploglim2  25567  divsqrtsumlem  25568  cvxcl  25573  scvxcvx  25574  jensenlem2  25576  amgmlem  25578  emcllem2  25585  emcllem4  25587  emcllem6  25589  emcllem7  25590  emre  25594  emgt0  25595  harmonicbnd3  25596  harmonicubnd  25598  harmonicbnd4  25599  zetacvg  25603  ftalem1  25661  ftalem2  25662  ftalem5  25665  issqf  25724  cht1  25753  chp1  25755  ppiltx  25765  mumullem2  25768  ppiublem1  25789  ppiub  25791  chtublem  25798  chtub  25799  logfacbnd3  25810  logexprlim  25812  perfectlem2  25817  dchrinv  25848  dchr1re  25850  efexple  25868  bposlem1  25871  bposlem2  25872  bposlem5  25875  bposlem8  25878  lgsdir2lem1  25912  lgsdir2lem5  25916  lgsdir  25919  lgsne0  25922  lgsabs1  25923  lgsdinn0  25932  gausslemma2dlem0i  25951  lgseisen  25966  m1lgs  25975  2lgslem3  25991  addsq2nreurex  26031  2sqreultblem  26035  2sqreunnltblem  26038  chebbnd1lem3  26058  chebbnd1  26059  chtppilimlem1  26060  chtppilimlem2  26061  chtppilim  26062  chpchtlim  26066  vmadivsumb  26070  rplogsumlem2  26072  rpvmasumlem  26074  dchrmusumlema  26080  dchrmusum2  26081  dchrvmasumlem2  26085  dchrvmasumiflem1  26088  dchrisum0flblem1  26095  dchrisum0flblem2  26096  dchrisum0fno1  26098  rpvmasum2  26099  dchrisum0re  26100  dchrisum0lema  26101  dchrisum0lem1b  26102  dchrisum0lem1  26103  dchrisum0lem2a  26104  dchrisum0lem2  26105  logdivsum  26120  mulog2sumlem2  26122  2vmadivsumlem  26127  log2sumbnd  26131  selbergb  26136  selberg2b  26139  chpdifbndlem1  26140  selberg3lem1  26144  selberg3lem2  26145  selberg4lem1  26147  pntrmax  26151  pntrsumo1  26152  selbergsb  26162  pntrlog2bndlem3  26166  pntrlog2bndlem5  26168  pntpbnd1a  26172  pntpbnd2  26174  pntibndlem1  26176  pntibndlem3  26179  pntlemd  26181  pntlemc  26182  pntlemb  26184  pntlemr  26189  pntlemf  26192  pntlemk  26193  pntlemo  26194  pntlem3  26196  pntleml  26198  abvcxp  26202  ostth2lem1  26205  ostth1  26220  ostth2lem2  26221  ostth2lem3  26222  ostth2lem4  26223  ostth2  26224  ostth3  26225  ostth  26226  trgcgrg  26312  brbtwn2  26702  colinearalglem4  26706  ax5seglem2  26726  ax5seglem3  26728  axpaschlem  26737  axpasch  26738  axlowdimlem6  26744  axlowdimlem10  26748  axlowdimlem16  26754  axlowdim1  26756  axlowdim2  26757  axlowdim  26758  axcontlem2  26762  elntg2  26782  lfgrnloop  26921  lfuhgr1v0e  27047  usgrexmpldifpr  27051  usgrexmplef  27052  1loopgrvd2  27296  vdegp1bi  27330  lfgrwlkprop  27480  pthdlem1  27558  pthdlem2  27560  clwlkclwwlkf  27796  upgr4cycl4dv4e  27973  konigsberglem2  28041  konigsberglem3  28042  konigsberglem5  28044  frgrreg  28182  ex-dif  28211  ex-in  28213  ex-pss  28216  ex-res  28229  ex-fl  28235  nv1  28461  smcnlem  28483  ipidsq  28496  nmlno0lem  28579  norm-ii-i  28923  bcs2  28968  norm1  29035  nmopub2tALT  29695  nmfnleub2  29712  nmlnop0iALT  29781  unopbd  29801  nmopadjlem  29875  nmopcoadji  29887  pjnmopi  29934  pjbdlni  29935  hstle1  30012  hstle  30016  hstles  30017  stge1i  30024  stlesi  30027  staddi  30032  stadd3i  30034  strlem1  30036  strlem5  30041  jplem1  30054  cdj1i  30219  addltmulALT  30232  xlt2addrd  30511  pr01ssre  30569  dp2lt10  30589  dp2ltsuc  30591  dp2ltc  30592  dplti  30610  dpmul4  30619  cshw1s2  30663  xrsmulgzz  30715  resvbas  30959  rearchi  30969  xrge0slmod  30971  prmidl0  31034  submateqlem1  31160  xrge0iifcnv  31284  xrge0iifcv  31285  xrge0iifiso  31286  xrge0iifhom  31288  zrhre  31368  indf  31382  indfval  31383  esumcst  31430  cntnevol  31595  omssubadd  31666  iwrdsplit  31753  dstfrvclim1  31843  coinfliprv  31848  ballotlem2  31854  ballotlem4  31864  ballotlemi1  31868  ballotlemic  31872  sgnclre  31905  sgnnbi  31911  sgnpbi  31912  sgnmulsgp  31916  plymulx0  31925  plymulx  31926  signswch  31939  signstf  31944  signsvfn  31960  itgexpif  31985  hgt750lemd  32027  logdivsqrle  32029  hgt750lem  32030  hgt750lem2  32031  hgt750leme  32037  tgoldbachgnn  32038  subfacp1lem1  32534  subfacp1lem5  32539  resconn  32601  iisconn  32607  iillysconn  32608  problem2  33017  problem3  33018  sinccvglem  33023  fz0n  33070  dnibndlem12  33936  knoppcnlem4  33943  knoppndvlem13  33971  cnndvlem1  33984  irrdiff  34735  relowlpssretop  34776  sin2h  35040  cos2h  35041  tan2h  35042  poimirlem7  35057  poimirlem16  35066  poimirlem17  35067  poimirlem19  35069  poimirlem20  35070  poimirlem22  35072  poimirlem23  35073  poimirlem29  35079  poimirlem31  35081  itg2addnclem3  35103  asindmre  35133  dvasin  35134  dvacos  35135  dvreasin  35136  dvreacos  35137  fdc  35176  geomcau  35190  cntotbnd  35227  heiborlem8  35249  bfplem2  35254  bfp  35255  3lexlogpow5ineq2  39335  2xp3dxp2ge1d  39374  factwoffsmonot  39375  1t1e1ALT  39450  re1m1e0m0  39522  sn-00idlem1  39523  sn-00idlem2  39524  remul02  39530  sn-0ne2  39531  reixi  39546  rei4  39547  remulid2  39557  ipiiie0  39561  sn-0tie0  39563  mulgt0b2d  39572  sn-0lt1  39574  sn-ltp1  39575  reneg1lt0  39576  sn-inelr  39577  rabren3dioph  39743  pellexlem5  39761  pellexlem6  39762  pell1qrgaplem  39801  pell14qrgap  39803  pellqrex  39807  pellfundre  39809  pellfundlb  39812  pellfund14gap  39815  jm2.17a  39888  acongeq  39911  jm2.23  39924  jm3.1lem2  39946  sqrtcval  40328  sqrtcval2  40329  resqrtval  40330  imsqrtval  40331  relexp01min  40401  mnringbased  40910  cvgdvgrat  41004  lhe4.4ex1a  41020  binomcxplemnotnn0  41047  isosctrlem1ALT  41627  supxrgelem  41956  xrlexaddrp  41971  infxr  41986  infleinflem2  41990  sumnnodd  42259  limsup10exlem  42401  limsup10ex  42402  dvnprodlem3  42577  stoweidlem1  42630  stoweidlem18  42647  stoweidlem19  42648  stoweidlem26  42655  stoweidlem34  42663  stoweidlem40  42669  stoweidlem41  42670  stoweidlem59  42688  stoweid  42692  stirlinglem10  42712  stirlinglem11  42713  dirkercncflem1  42732  fourierdlem16  42752  fourierdlem21  42757  fourierdlem22  42758  fourierdlem42  42778  fourierdlem68  42803  fourierdlem83  42818  fourierdlem103  42838  sqwvfourb  42858  fouriersw  42860  etransclem23  42886  salgencntex  42970  ovn0lem  43191  smfmullem3  43412  smfmullem4  43413  zm1nn  43846  m1mod0mod1  43873  fmtnosqrt  44043  perfectALTVlem2  44227  2exp340mod341  44238  8exp8mod9  44241  nfermltl8rev  44247  nnsum3primesprm  44295  nnsum4primesodd  44301  nnsum4primesoddALTV  44302  nnsum4primeseven  44305  nnsum4primesevenALTV  44306  tgblthelfgott  44320  tgoldbach  44322  rege1logbrege0  44959  rege1logbzge0  44960  blennnelnn  44977  dignnld  45004  nn0sumshdiglemA  45020  nn0sumshdiglem1  45022  rrx2xpref1o  45119  rrxlines  45134  eenglngeehlnmlem1  45138  eenglngeehlnmlem2  45139  line2ylem  45152  line2x  45155
  Copyright terms: Public domain W3C validator