Theorem 1re 11134

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 11086, 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.

Step	Hyp	Ref	Expression
1		ax-1ne0 11097	. . 3 ⊢ 1 ≠ 0
2		ax-1cn 11086	. . . . 5 ⊢ 1 ∈ ℂ
3		cnre 11131	. . . . 5 ⊢ (1 ∈ ℂ → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)))
4	2, 3	ax-mp 5	. . . 4 ⊢ ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏))
5		neeq1 2987	. . . . . . . 8 ⊢ (1 = (𝑎 + (i · 𝑏)) → (1 ≠ 0 ↔ (𝑎 + (i · 𝑏)) ≠ 0))
6	5	biimpcd 249	. . . . . . 7 ⊢ (1 ≠ 0 → (1 = (𝑎 + (i · 𝑏)) → (𝑎 + (i · 𝑏)) ≠ 0))
7		0cn 11126	. . . . . . . 8 ⊢ 0 ∈ ℂ
8		cnre 11131	. . . . . . . 8 ⊢ (0 ∈ ℂ → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)))
9	7, 8	ax-mp 5	. . . . . . 7 ⊢ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑))
10		neeq2 2988	. . . . . . . . . 10 ⊢ (0 = (𝑐 + (i · 𝑑)) → ((𝑎 + (i · 𝑏)) ≠ 0 ↔ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
11	10	biimpcd 249	. . . . . . . . 9 ⊢ ((𝑎 + (i · 𝑏)) ≠ 0 → (0 = (𝑐 + (i · 𝑑)) → (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
12	11	reximdv 3144	. . . . . . . 8 ⊢ ((𝑎 + (i · 𝑏)) ≠ 0 → (∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)) → ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
13	12	reximdv 3144	. . . . . . 7 ⊢ ((𝑎 + (i · 𝑏)) ≠ 0 → (∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)) → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
14	6, 9, 13	syl6mpi 67	. . . . . 6 ⊢ (1 ≠ 0 → (1 = (𝑎 + (i · 𝑏)) → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
15	14	reximdv 3144	. . . . 5 ⊢ (1 ≠ 0 → (∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)) → ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
16	15	reximdv 3144	. . . 4 ⊢ (1 ≠ 0 → (∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)) → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
17	4, 16	mpi 20	. . 3 ⊢ (1 ≠ 0 → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)))
18		id 22	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑐 → 𝑎 = 𝑐)
19		oveq2 7361	. . . . . . . . . . . 12 ⊢ (𝑏 = 𝑑 → (i · 𝑏) = (i · 𝑑))
20	18, 19	oveqan12d 7372	. . . . . . . . . . 11 ⊢ ((𝑎 = 𝑐 ∧ 𝑏 = 𝑑) → (𝑎 + (i · 𝑏)) = (𝑐 + (i · 𝑑)))
21	20	expcom 413	. . . . . . . . . 10 ⊢ (𝑏 = 𝑑 → (𝑎 = 𝑐 → (𝑎 + (i · 𝑏)) = (𝑐 + (i · 𝑑))))
22	21	necon3d 2946	. . . . . . . . 9 ⊢ (𝑏 = 𝑑 → ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → 𝑎 ≠ 𝑐))
23	22	com12 32	. . . . . . . 8 ⊢ ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → (𝑏 = 𝑑 → 𝑎 ≠ 𝑐))
24	23	necon3bd 2939	. . . . . . 7 ⊢ ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → (¬ 𝑎 ≠ 𝑐 → 𝑏 ≠ 𝑑))
25	24	orrd 863	. . . . . 6 ⊢ ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → (𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑))
26		neeq1 2987	. . . . . . . . . 10 ⊢ (𝑥 = 𝑎 → (𝑥 ≠ 𝑦 ↔ 𝑎 ≠ 𝑦))
27		neeq2 2988	. . . . . . . . . 10 ⊢ (𝑦 = 𝑐 → (𝑎 ≠ 𝑦 ↔ 𝑎 ≠ 𝑐))
28	26, 27	rspc2ev 3592	. . . . . . . . 9 ⊢ ((𝑎 ∈ ℝ ∧ 𝑐 ∈ ℝ ∧ 𝑎 ≠ 𝑐) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦)
29	28	3expia 1121	. . . . . . . 8 ⊢ ((𝑎 ∈ ℝ ∧ 𝑐 ∈ ℝ) → (𝑎 ≠ 𝑐 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
30	29	ad2ant2r 747	. . . . . . 7 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → (𝑎 ≠ 𝑐 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
31		neeq1 2987	. . . . . . . . . 10 ⊢ (𝑥 = 𝑏 → (𝑥 ≠ 𝑦 ↔ 𝑏 ≠ 𝑦))
32		neeq2 2988	. . . . . . . . . 10 ⊢ (𝑦 = 𝑑 → (𝑏 ≠ 𝑦 ↔ 𝑏 ≠ 𝑑))
33	31, 32	rspc2ev 3592	. . . . . . . . 9 ⊢ ((𝑏 ∈ ℝ ∧ 𝑑 ∈ ℝ ∧ 𝑏 ≠ 𝑑) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦)
34	33	3expia 1121	. . . . . . . 8 ⊢ ((𝑏 ∈ ℝ ∧ 𝑑 ∈ ℝ) → (𝑏 ≠ 𝑑 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
35	34	ad2ant2l 746	. . . . . . 7 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → (𝑏 ≠ 𝑑 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
36	30, 35	jaod 859	. . . . . 6 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → ((𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
37	25, 36	syl5 34	. . . . 5 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
38	37	rexlimdvva 3186	. . . 4 ⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
39	38	rexlimivv 3171	. . 3 ⊢ (∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦)
40	1, 17, 39	mp2b 10	. 2 ⊢ ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦
41		eqtr3 2751	. . . . . . . . 9 ⊢ ((𝑥 = 0 ∧ 𝑦 = 0) → 𝑥 = 𝑦)
42	41	ex 412	. . . . . . . 8 ⊢ (𝑥 = 0 → (𝑦 = 0 → 𝑥 = 𝑦))
43	42	necon3d 2946	. . . . . . 7 ⊢ (𝑥 = 0 → (𝑥 ≠ 𝑦 → 𝑦 ≠ 0))
44		neeq1 2987	. . . . . . . . 9 ⊢ (𝑧 = 𝑦 → (𝑧 ≠ 0 ↔ 𝑦 ≠ 0))
45	44	rspcev 3579	. . . . . . . 8 ⊢ ((𝑦 ∈ ℝ ∧ 𝑦 ≠ 0) → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)
46	45	expcom 413	. . . . . . 7 ⊢ (𝑦 ≠ 0 → (𝑦 ∈ ℝ → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
47	43, 46	syl6 35	. . . . . 6 ⊢ (𝑥 = 0 → (𝑥 ≠ 𝑦 → (𝑦 ∈ ℝ → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
48	47	com23 86	. . . . 5 ⊢ (𝑥 = 0 → (𝑦 ∈ ℝ → (𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
49	48	adantld 490	. . . 4 ⊢ (𝑥 = 0 → ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
50		neeq1 2987	. . . . . . . 8 ⊢ (𝑧 = 𝑥 → (𝑧 ≠ 0 ↔ 𝑥 ≠ 0))
51	50	rspcev 3579	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)
52	51	expcom 413	. . . . . 6 ⊢ (𝑥 ≠ 0 → (𝑥 ∈ ℝ → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
53	52	adantrd 491	. . . . 5 ⊢ (𝑥 ≠ 0 → ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
54	53	a1dd 50	. . . 4 ⊢ (𝑥 ≠ 0 → ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
55	49, 54	pm2.61ine 3008	. . 3 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
56	55	rexlimivv 3171	. 2 ⊢ (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)
57		ax-rrecex 11100	. . . 4 ⊢ ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → ∃𝑥 ∈ ℝ (𝑧 · 𝑥) = 1)
58		remulcl 11113	. . . . . . 7 ⊢ ((𝑧 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (𝑧 · 𝑥) ∈ ℝ)
59	58	adantlr 715	. . . . . 6 ⊢ (((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) ∧ 𝑥 ∈ ℝ) → (𝑧 · 𝑥) ∈ ℝ)
60		eleq1 2816	. . . . . 6 ⊢ ((𝑧 · 𝑥) = 1 → ((𝑧 · 𝑥) ∈ ℝ ↔ 1 ∈ ℝ))
61	59, 60	syl5ibcom 245	. . . . 5 ⊢ (((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) ∧ 𝑥 ∈ ℝ) → ((𝑧 · 𝑥) = 1 → 1 ∈ ℝ))
62	61	rexlimdva 3130	. . . 4 ⊢ ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → (∃𝑥 ∈ ℝ (𝑧 · 𝑥) = 1 → 1 ∈ ℝ))
63	57, 62	mpd 15	. . 3 ⊢ ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → 1 ∈ ℝ)
64	63	rexlimiva 3122	. 2 ⊢ (∃𝑧 ∈ ℝ 𝑧 ≠ 0 → 1 ∈ ℝ)
65	40, 56, 64	mp2b 10	1 ⊢ 1 ∈ ℝ

Syntax hints:   → wi 4   ∧ wa 395   ∨ wo 847   = wceq 1540   ∈ wcel 2109   ≠ wne 2925  ∃wrex 3053  (class class class)co 7353  ℂcc 11026  ℝcr 11027  0cc0 11028  1c1 11029  ici 11030   + caddc 11031   · cmul 11033

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-1cn 11086  ax-icn 11087  ax-addcl 11088  ax-mulcl 11090  ax-mulrcl 11091  ax-i2m1 11096  ax-1ne0 11097  ax-rrecex 11100  ax-cnre 11101

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-iota 6442  df-fv 6494  df-ov 7356

This theorem is referenced by:  1red  11135  1xr  11193  dedekind  11298  peano2re  11308  mul02lem2  11312  addrid  11315  renegcl  11446  peano2rem  11450  0reALT  11480  0lt1  11661  0le1  11662  relin01  11663  1le1  11767  eqneg  11863  ltp1  11983  ltm1  11985  recgt0  11989  mulgt1OLD  12002  ltmulgt11  12003  lemulge11  12006  reclt1  12039  recgt1  12040  recgt1i  12041  recp1lt1  12042  recreclt  12043  recgt0ii  12050  ledivp1i  12069  ltdivp1i  12070  neg1rr  12133  neg1lt0  12135  cju  12143  nnssre  12151  nnge1  12175  nngt1ne1  12176  nnle1eq1  12177  nngt0  12178  nnnlt1  12179  nnne0  12181  nnrecre  12189  nnrecgt0  12190  nnsub  12191  2re  12221  3re  12227  4re  12231  5re  12234  6re  12237  7re  12240  8re  12243  9re  12246  0le2  12249  2pos  12250  3pos  12252  4pos  12254  5pos  12256  6pos  12257  7pos  12258  8pos  12259  9pos  12260  1lt2  12313  1lt3  12315  1lt4  12318  1lt5  12322  1lt6  12327  1lt7  12333  1lt8  12340  1lt9  12348  1ne2  12350  1le2  12351  1le3  12354  halflt1  12360  addltmul  12379  nnunb  12399  elnnnn0c  12448  nn0ge2m1nn  12473  elnnz1  12520  znnnlt1  12521  zltp1le  12544  zleltp1  12545  nn0lt2  12558  recnz  12570  gtndiv  12572  3halfnz  12574  10re  12629  1lt10  12749  eluzp1m1  12780  eluzp1p1  12782  eluz2b2  12841  zbtwnre  12866  rebtwnz  12867  1rp  12916  divlt1lt  12983  divle1le  12984  nnledivrp  13026  qbtwnxr  13121  xmulrid  13200  xmulm1  13202  x2times  13220  xrub  13233  elicc01  13388  1elunit  13392  divelunit  13416  lincmb01cmp  13417  unitssre  13421  0nelfz1  13465  fzpreddisj  13495  fznatpl1  13500  fztpval  13508  fraclt1  13725  fracle1  13726  flbi2  13740  fldiv4p1lem1div2  13758  fldiv4lem1div2  13760  fldiv  13783  modid  13819  1mod  13826  m1modnnsub1  13843  modm1p1mod0  13848  seqf1olem1  13967  reexpcl  14004  reexpclz  14008  expge0  14024  expge1  14025  expgt1  14026  bernneq  14155  bernneq2  14156  expnbnd  14158  expnlbnd  14159  expnlbnd2  14160  expmulnbnd  14161  discr1  14165  facwordi  14215  faclbnd3  14218  faclbnd4lem1  14219  faclbnd4lem4  14222  faclbnd6  14225  facavg  14227  hashv01gt1  14271  hashnn0n0nn  14317  hashunsnggt  14320  hash1snb  14345  hashgt12el  14348  hashgt12el2  14349  hashfun  14363  hashge2el2dif  14406  tpf1ofv2  14424  lsw0  14491  f1oun2prg  14843  cjexp  15076  re1  15080  im1  15081  rei  15082  imi  15083  01sqrexlem1  15168  01sqrexlem2  15169  01sqrexlem3  15170  01sqrexlem4  15171  01sqrexlem7  15174  resqrex  15176  sqrt1  15197  sqrt2gt1lt2  15200  sqrtm1  15201  abs1  15223  absrdbnd  15268  caubnd2  15284  mulcn2  15522  reccn2  15523  rlimno1  15580  o1fsum  15739  expcnv  15790  geolim  15796  geolim2  15797  georeclim  15798  geomulcvg  15802  geoisumr  15804  geoisum1c  15806  fprodge0  15919  fprodge1  15921  rerisefaccl  15943  refallfaccl  15944  ere  16015  ege2le3  16016  efgt1  16044  resin4p  16066  recos4p  16067  tanhbnd  16089  sinbnd  16108  cosbnd  16109  sinbnd2  16110  cosbnd2  16111  ef01bndlem  16112  sin01bnd  16113  cos01bnd  16114  cos1bnd  16115  cos2bnd  16116  sinltx  16117  sin01gt0  16118  cos01gt0  16119  sin02gt0  16120  sincos1sgn  16121  ene1  16138  rpnnen2lem2  16143  rpnnen2lem3  16144  rpnnen2lem4  16145  rpnnen2lem9  16150  rpnnen2lem12  16153  ruclem6  16163  ruclem11  16168  ruclem12  16169  3dvds  16261  flodddiv4  16345  sadcadd  16388  isprm3  16613  sqnprm  16632  coprm  16641  phibndlem  16700  pythagtriplem3  16749  pcmpt  16823  fldivp1  16828  pockthi  16838  infpn2  16844  basendxnmulrndx  17219  starvndxnbasendx  17227  scandxnbasendx  17239  vscandxnbasendx  17244  ipndxnbasendx  17255  basendxnocndx  17306  slotsbhcdif  17338  lt6abl  19793  srgbinomlem4  20133  0ringnnzr  20429  abvneg  20730  abvtrivd  20736  xrsmcmn  21317  xrsnsgrp  21333  gzrngunitlem  21358  gzrngunit  21359  rge0srg  21364  psgnodpmr  21516  remulg  21533  resubdrg  21534  psdmvr  22073  dscmet  24477  dscopn  24478  nrginvrcnlem  24596  idnghm  24648  tgioo  24701  blcvx  24703  iicmp  24796  iiconn  24797  iirev  24840  iihalf1  24842  iihalf2  24845  iihalf2cnOLD  24847  elii1  24848  elii2  24849  iimulcl  24850  icopnfcnv  24857  icopnfhmeo  24858  iccpnfhmeo  24860  xrhmeo  24861  xrhmph  24862  evth  24875  xlebnum  24881  htpycc  24896  reparphti  24913  reparphtiOLD  24914  pcoval1  24930  pco1  24932  pcoval2  24933  pcocn  24934  pcohtpylem  24936  pcopt  24939  pcopt2  24940  pcoass  24941  pcorevlem  24943  nmhmcn  25037  ncvs1  25074  ovolunlem1a  25414  vitalilem2  25527  vitalilem4  25529  vitalilem5  25530  vitali  25531  i1f1  25608  itg11  25609  itg2const  25658  dveflem  25900  dvlipcn  25916  dvcvx  25942  ply1remlem  26087  fta1blem  26093  vieta1lem2  26236  aalioulem3  26259  aalioulem5  26261  aaliou3lem2  26268  ulmbdd  26324  iblulm  26333  radcnvlem1  26339  dvradcnv  26347  abelthlem2  26359  abelthlem3  26360  abelthlem5  26362  abelthlem7  26365  abelth  26368  abelth2  26369  reeff1olem  26373  reeff1o  26374  sinhalfpilem  26389  tangtx  26431  sincos4thpi  26439  pige3ALT  26446  coskpi  26449  cos0pilt1  26458  recosf1o  26461  tanregt0  26465  efif1olem3  26470  efif1olem4  26471  loge  26512  logdivlti  26546  logcnlem4  26571  logf1o2  26576  logtayl  26586  logccv  26589  recxpcl  26601  cxplea  26622  cxpcn3lem  26674  cxpaddlelem  26678  loglesqrt  26688  ang180lem2  26737  angpined  26757  acosrecl  26830  atancj  26837  atanlogaddlem  26840  atantan  26850  atans2  26858  ressatans  26861  leibpi  26869  log2le1  26877  birthdaylem3  26880  cxp2lim  26904  cxploglim  26905  cxploglim2  26906  divsqrtsumlem  26907  cvxcl  26912  scvxcvx  26913  jensenlem2  26915  amgmlem  26917  emcllem2  26924  emcllem4  26926  emcllem6  26928  emcllem7  26929  emre  26933  emgt0  26934  harmonicbnd3  26935  harmonicubnd  26937  harmonicbnd4  26938  zetacvg  26942  ftalem1  27000  ftalem2  27001  ftalem5  27004  issqf  27063  cht1  27092  chp1  27094  ppiltx  27104  mumullem2  27107  ppiublem1  27130  ppiub  27132  chtublem  27139  chtub  27140  logfacbnd3  27151  logexprlim  27153  perfectlem2  27158  dchrinv  27189  dchr1re  27191  efexple  27209  bposlem1  27212  bposlem2  27213  bposlem5  27216  bposlem8  27219  lgsdir2lem1  27253  lgsdir2lem5  27257  lgsdir  27260  lgsne0  27263  lgsabs1  27264  lgsdinn0  27273  gausslemma2dlem0i  27292  lgseisen  27307  m1lgs  27316  2lgslem3  27332  addsq2nreurex  27372  2sqreultblem  27376  2sqreunnltblem  27379  chebbnd1lem3  27399  chebbnd1  27400  chtppilimlem1  27401  chtppilimlem2  27402  chtppilim  27403  chpchtlim  27407  vmadivsumb  27411  rplogsumlem2  27413  rpvmasumlem  27415  dchrmusumlema  27421  dchrmusum2  27422  dchrvmasumlem2  27426  dchrvmasumiflem1  27429  dchrisum0flblem1  27436  dchrisum0flblem2  27437  dchrisum0fno1  27439  rpvmasum2  27440  dchrisum0re  27441  dchrisum0lema  27442  dchrisum0lem1b  27443  dchrisum0lem1  27444  dchrisum0lem2a  27445  dchrisum0lem2  27446  logdivsum  27461  mulog2sumlem2  27463  2vmadivsumlem  27468  log2sumbnd  27472  selbergb  27477  selberg2b  27480  chpdifbndlem1  27481  selberg3lem1  27485  selberg3lem2  27486  selberg4lem1  27488  pntrmax  27492  pntrsumo1  27493  selbergsb  27503  pntrlog2bndlem3  27507  pntrlog2bndlem5  27509  pntpbnd1a  27513  pntpbnd2  27515  pntibndlem1  27517  pntibndlem3  27520  pntlemd  27522  pntlemc  27523  pntlemb  27525  pntlemr  27530  pntlemf  27533  pntlemk  27534  pntlemo  27535  pntlem3  27537  pntleml  27539  abvcxp  27543  ostth2lem1  27546  ostth1  27561  ostth2lem2  27562  ostth2lem3  27563  ostth2lem4  27564  ostth2  27565  ostth3  27566  ostth  27567  slotsinbpsd  28405  slotslnbpsd  28406  trgcgrg  28479  brbtwn2  28869  colinearalglem4  28873  ax5seglem2  28893  ax5seglem3  28895  axpaschlem  28904  axpasch  28905  axlowdimlem6  28911  axlowdimlem10  28915  axlowdimlem16  28921  axlowdim1  28923  axlowdim2  28924  axlowdim  28925  axcontlem2  28929  elntg2  28949  lfgrnloop  29089  lfuhgr1v0e  29218  usgrexmpldifpr  29222  usgrexmplef  29223  1loopgrvd2  29468  vdegp1bi  29502  lfgrwlkprop  29650  pthdlem1  29730  pthdlem2  29732  clwlkclwwlkf  29971  upgr4cycl4dv4e  30148  konigsberglem2  30216  konigsberglem3  30217  konigsberglem5  30219  frgrreg  30357  ex-dif  30386  ex-in  30388  ex-pss  30391  ex-res  30404  ex-fl  30410  nv1  30638  smcnlem  30660  ipidsq  30673  nmlno0lem  30756  norm-ii-i  31100  bcs2  31145  norm1  31212  nmopub2tALT  31872  nmfnleub2  31889  nmlnop0iALT  31958  unopbd  31978  nmopadjlem  32052  nmopcoadji  32064  pjnmopi  32111  pjbdlni  32112  hstle1  32189  hstle  32193  hstles  32194  stge1i  32201  stlesi  32204  staddi  32209  stadd3i  32211  strlem1  32213  strlem5  32218  jplem1  32231  cdj1i  32396  addltmulALT  32409  xlt2addrd  32721  pr01ssre  32788  sgnclre  32796  sgnnbi  32802  sgnpbi  32803  sgnmulsgp  32807  indf  32817  indfval  32818  dp2lt10  32843  dp2ltsuc  32845  dp2ltc  32846  dplti  32864  dpmul4  32873  cshw1s2  32921  xrsmulgzz  32982  rearchi  33302  xrge0slmod  33304  prmidl0  33406  evl1deg3  33532  constrconj  33731  2sqr3minply  33766  submateqlem1  33793  xrge0iifcnv  33919  xrge0iifcv  33920  xrge0iifiso  33921  xrge0iifhom  33923  zrhre  34005  esumcst  34049  cntnevol  34214  omssubadd  34287  iwrdsplit  34374  dstfrvclim1  34465  coinfliprv  34470  ballotlem2  34476  ballotlem4  34486  ballotlemi1  34490  ballotlemic  34494  plymulx0  34534  plymulx  34535  signswch  34548  signstf  34553  signsvfn  34569  itgexpif  34593  hgt750lemd  34635  logdivsqrle  34637  hgt750lem  34638  hgt750lem2  34639  hgt750leme  34645  tgoldbachgnn  34646  subfacp1lem1  35171  subfacp1lem5  35176  resconn  35238  iisconn  35244  iillysconn  35245  problem2  35658  problem3  35659  sinccvglem  35664  fz0n  35723  dnibndlem12  36482  knoppcnlem4  36489  knoppndvlem13  36517  cnndvlem1  36530  irrdiff  37319  relowlpssretop  37357  sin2h  37609  cos2h  37610  tan2h  37611  poimirlem7  37626  poimirlem16  37635  poimirlem17  37636  poimirlem19  37638  poimirlem20  37639  poimirlem22  37641  poimirlem23  37642  poimirlem29  37648  poimirlem31  37650  itg2addnclem3  37672  asindmre  37702  dvasin  37703  dvacos  37704  dvreasin  37705  dvreacos  37706  fdc  37744  geomcau  37758  cntotbnd  37795  heiborlem8  37817  bfplem2  37822  bfp  37823  aks4d1p1p7  42067  1t1e1ALT  42248  ine1  42307  re1m1e0m0  42390  sn-00idlem1  42391  sn-00idlem2  42392  remul02  42398  sn-0ne2  42399  reixi  42416  rei4  42417  remullid  42427  ipiiie0  42431  sn-0tie0  42444  sn-nnne0  42453  mulgt0b1d  42465  sn-0lt1  42468  sn-ltp1  42469  reneg1lt0  42473  sn-inelr  42480  rabren3dioph  42808  pellexlem5  42826  pellexlem6  42827  pell1qrgaplem  42866  pell14qrgap  42868  pellqrex  42872  pellfundre  42874  pellfundlb  42877  pellfund14gap  42880  jm2.17a  42953  acongeq  42976  jm2.23  42989  jm3.1lem2  43011  sqrtcval  43634  sqrtcval2  43635  resqrtval  43636  imsqrtval  43637  relexp01min  43706  cvgdvgrat  44306  lhe4.4ex1a  44322  binomcxplemnotnn0  44349  isosctrlem1ALT  44927  supxrgelem  45337  xrlexaddrp  45352  infxr  45366  infleinflem2  45370  sumnnodd  45631  limsup10exlem  45773  limsup10ex  45774  dvnprodlem3  45949  stoweidlem1  46002  stoweidlem18  46019  stoweidlem19  46020  stoweidlem26  46027  stoweidlem34  46035  stoweidlem40  46041  stoweidlem41  46042  stoweidlem59  46060  stoweid  46064  stirlinglem10  46084  stirlinglem11  46085  dirkercncflem1  46104  fourierdlem16  46124  fourierdlem21  46129  fourierdlem22  46130  fourierdlem42  46150  fourierdlem68  46175  fourierdlem83  46190  fourierdlem103  46210  sqwvfourb  46230  fouriersw  46232  etransclem23  46258  salgencntex  46344  ovn0lem  46566  smfmullem3  46794  smfmullem4  46795  cjnpoly  46893  zm1nn  47306  ceilhalf1  47338  m1mod0mod1  47358  fmtnosqrt  47543  perfectALTVlem2  47726  2exp340mod341  47737  8exp8mod9  47740  nfermltl8rev  47746  nnsum3primesprm  47794  nnsum4primesodd  47800  nnsum4primesoddALTV  47801  nnsum4primeseven  47804  nnsum4primesevenALTV  47805  tgblthelfgott  47819  tgoldbach  47821  usgrexmpl1lem  48025  usgrexmpl2lem  48030  usgrexmpl2nb1  48036  usgrexmpl2nb3  48038  usgrexmpl2nb4  48039  usgrexmpl2nb5  48040  usgrexmpl2trifr  48041  gpg3kgrtriexlem3  48089  pgnbgreunbgrlem2lem1  48118  pgnbgreunbgrlem2lem2  48119  rege1logbrege0  48563  rege1logbzge0  48564  blennnelnn  48581  dignnld  48608  nn0sumshdiglemA  48624  nn0sumshdiglem1  48626  rrx2xpref1o  48723  rrxlines  48738  eenglngeehlnmlem1  48742  eenglngeehlnmlem2  48743  line2ylem  48756  line2x  48759  icccldii  48923  io1ii  48925  sepfsepc  48932