Theorem 1re 11112

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 11064, 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 11075	. . 3 ⊢ 1 ≠ 0
2		ax-1cn 11064	. . . . 5 ⊢ 1 ∈ ℂ
3		cnre 11109	. . . . 5 ⊢ (1 ∈ ℂ → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)))
4	2, 3	ax-mp 5	. . . 4 ⊢ ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏))
5		neeq1 2990	. . . . . . . 8 ⊢ (1 = (𝑎 + (i · 𝑏)) → (1 ≠ 0 ↔ (𝑎 + (i · 𝑏)) ≠ 0))
6	5	biimpcd 249	. . . . . . 7 ⊢ (1 ≠ 0 → (1 = (𝑎 + (i · 𝑏)) → (𝑎 + (i · 𝑏)) ≠ 0))
7		0cn 11104	. . . . . . . 8 ⊢ 0 ∈ ℂ
8		cnre 11109	. . . . . . . 8 ⊢ (0 ∈ ℂ → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)))
9	7, 8	ax-mp 5	. . . . . . 7 ⊢ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑))
10		neeq2 2991	. . . . . . . . . 10 ⊢ (0 = (𝑐 + (i · 𝑑)) → ((𝑎 + (i · 𝑏)) ≠ 0 ↔ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
11	10	biimpcd 249	. . . . . . . . 9 ⊢ ((𝑎 + (i · 𝑏)) ≠ 0 → (0 = (𝑐 + (i · 𝑑)) → (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
12	11	reximdv 3147	. . . . . . . 8 ⊢ ((𝑎 + (i · 𝑏)) ≠ 0 → (∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)) → ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
13	12	reximdv 3147	. . . . . . 7 ⊢ ((𝑎 + (i · 𝑏)) ≠ 0 → (∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)) → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
14	6, 9, 13	syl6mpi 67	. . . . . 6 ⊢ (1 ≠ 0 → (1 = (𝑎 + (i · 𝑏)) → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
15	14	reximdv 3147	. . . . 5 ⊢ (1 ≠ 0 → (∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)) → ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
16	15	reximdv 3147	. . . 4 ⊢ (1 ≠ 0 → (∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)) → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
17	4, 16	mpi 20	. . 3 ⊢ (1 ≠ 0 → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)))
18		id 22	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑐 → 𝑎 = 𝑐)
19		oveq2 7354	. . . . . . . . . . . 12 ⊢ (𝑏 = 𝑑 → (i · 𝑏) = (i · 𝑑))
20	18, 19	oveqan12d 7365	. . . . . . . . . . 11 ⊢ ((𝑎 = 𝑐 ∧ 𝑏 = 𝑑) → (𝑎 + (i · 𝑏)) = (𝑐 + (i · 𝑑)))
21	20	expcom 413	. . . . . . . . . 10 ⊢ (𝑏 = 𝑑 → (𝑎 = 𝑐 → (𝑎 + (i · 𝑏)) = (𝑐 + (i · 𝑑))))
22	21	necon3d 2949	. . . . . . . . 9 ⊢ (𝑏 = 𝑑 → ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → 𝑎 ≠ 𝑐))
23	22	com12 32	. . . . . . . 8 ⊢ ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → (𝑏 = 𝑑 → 𝑎 ≠ 𝑐))
24	23	necon3bd 2942	. . . . . . 7 ⊢ ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → (¬ 𝑎 ≠ 𝑐 → 𝑏 ≠ 𝑑))
25	24	orrd 863	. . . . . 6 ⊢ ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → (𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑))
26		neeq1 2990	. . . . . . . . . 10 ⊢ (𝑥 = 𝑎 → (𝑥 ≠ 𝑦 ↔ 𝑎 ≠ 𝑦))
27		neeq2 2991	. . . . . . . . . 10 ⊢ (𝑦 = 𝑐 → (𝑎 ≠ 𝑦 ↔ 𝑎 ≠ 𝑐))
28	26, 27	rspc2ev 3585	. . . . . . . . 9 ⊢ ((𝑎 ∈ ℝ ∧ 𝑐 ∈ ℝ ∧ 𝑎 ≠ 𝑐) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦)
29	28	3expia 1121	. . . . . . . 8 ⊢ ((𝑎 ∈ ℝ ∧ 𝑐 ∈ ℝ) → (𝑎 ≠ 𝑐 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
30	29	ad2ant2r 747	. . . . . . 7 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → (𝑎 ≠ 𝑐 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
31		neeq1 2990	. . . . . . . . . 10 ⊢ (𝑥 = 𝑏 → (𝑥 ≠ 𝑦 ↔ 𝑏 ≠ 𝑦))
32		neeq2 2991	. . . . . . . . . 10 ⊢ (𝑦 = 𝑑 → (𝑏 ≠ 𝑦 ↔ 𝑏 ≠ 𝑑))
33	31, 32	rspc2ev 3585	. . . . . . . . 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 3189	. . . 4 ⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
39	38	rexlimivv 3174	. . 3 ⊢ (∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦)
40	1, 17, 39	mp2b 10	. 2 ⊢ ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦
41		eqtr3 2753	. . . . . . . . 9 ⊢ ((𝑥 = 0 ∧ 𝑦 = 0) → 𝑥 = 𝑦)
42	41	ex 412	. . . . . . . 8 ⊢ (𝑥 = 0 → (𝑦 = 0 → 𝑥 = 𝑦))
43	42	necon3d 2949	. . . . . . 7 ⊢ (𝑥 = 0 → (𝑥 ≠ 𝑦 → 𝑦 ≠ 0))
44		neeq1 2990	. . . . . . . . 9 ⊢ (𝑧 = 𝑦 → (𝑧 ≠ 0 ↔ 𝑦 ≠ 0))
45	44	rspcev 3572	. . . . . . . 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 2990	. . . . . . . 8 ⊢ (𝑧 = 𝑥 → (𝑧 ≠ 0 ↔ 𝑥 ≠ 0))
51	50	rspcev 3572	. . . . . . 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 3011	. . 3 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
56	55	rexlimivv 3174	. 2 ⊢ (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)
57		ax-rrecex 11078	. . . 4 ⊢ ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → ∃𝑥 ∈ ℝ (𝑧 · 𝑥) = 1)
58		remulcl 11091	. . . . . . 7 ⊢ ((𝑧 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (𝑧 · 𝑥) ∈ ℝ)
59	58	adantlr 715	. . . . . 6 ⊢ (((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) ∧ 𝑥 ∈ ℝ) → (𝑧 · 𝑥) ∈ ℝ)
60		eleq1 2819	. . . . . 6 ⊢ ((𝑧 · 𝑥) = 1 → ((𝑧 · 𝑥) ∈ ℝ ↔ 1 ∈ ℝ))
61	59, 60	syl5ibcom 245	. . . . 5 ⊢ (((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) ∧ 𝑥 ∈ ℝ) → ((𝑧 · 𝑥) = 1 → 1 ∈ ℝ))
62	61	rexlimdva 3133	. . . 4 ⊢ ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → (∃𝑥 ∈ ℝ (𝑧 · 𝑥) = 1 → 1 ∈ ℝ))
63	57, 62	mpd 15	. . 3 ⊢ ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → 1 ∈ ℝ)
64	63	rexlimiva 3125	. 2 ⊢ (∃𝑧 ∈ ℝ 𝑧 ≠ 0 → 1 ∈ ℝ)
65	40, 56, 64	mp2b 10	1 ⊢ 1 ∈ ℝ

Syntax hints:   → wi 4   ∧ wa 395   ∨ wo 847   = wceq 1541   ∈ wcel 2111   ≠ wne 2928  ∃wrex 3056  (class class class)co 7346  ℂcc 11004  ℝcr 11005  0cc0 11006  1c1 11007  ici 11008   + caddc 11009   · cmul 11011

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-1cn 11064  ax-icn 11065  ax-addcl 11066  ax-mulcl 11068  ax-mulrcl 11069  ax-i2m1 11074  ax-1ne0 11075  ax-rrecex 11078  ax-cnre 11079

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ne 2929  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4281  df-if 4473  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-br 5090  df-iota 6437  df-fv 6489  df-ov 7349

This theorem is referenced by:  1red  11113  1xr  11171  dedekind  11276  peano2re  11286  mul02lem2  11290  addrid  11293  renegcl  11424  peano2rem  11428  0reALT  11458  0lt1  11639  0le1  11640  relin01  11641  1le1  11745  eqneg  11841  ltp1  11961  ltm1  11963  recgt0  11967  mulgt1OLD  11980  ltmulgt11  11981  lemulge11  11984  reclt1  12017  recgt1  12018  recgt1i  12019  recp1lt1  12020  recreclt  12021  recgt0ii  12028  ledivp1i  12047  ltdivp1i  12048  neg1rr  12111  neg1lt0  12113  cju  12121  nnssre  12129  nnge1  12153  nngt1ne1  12154  nnle1eq1  12155  nngt0  12156  nnnlt1  12157  nnne0  12159  nnrecre  12167  nnrecgt0  12168  nnsub  12169  2re  12199  3re  12205  4re  12209  5re  12212  6re  12215  7re  12218  8re  12221  9re  12224  0le2  12227  2pos  12228  3pos  12230  4pos  12232  5pos  12234  6pos  12235  7pos  12236  8pos  12237  9pos  12238  1lt2  12291  1lt3  12293  1lt4  12296  1lt5  12300  1lt6  12305  1lt7  12311  1lt8  12318  1lt9  12326  1ne2  12328  1le2  12329  1le3  12332  halflt1  12338  addltmul  12357  nnunb  12377  elnnnn0c  12426  nn0ge2m1nn  12451  elnnz1  12498  znnnlt1  12499  zltp1le  12522  zleltp1  12523  nn0lt2  12536  recnz  12548  gtndiv  12550  3halfnz  12552  10re  12607  1lt10  12727  eluzp1m1  12758  eluzp1p1  12760  eluz2b2  12819  zbtwnre  12844  rebtwnz  12845  1rp  12894  divlt1lt  12961  divle1le  12962  nnledivrp  13004  qbtwnxr  13099  xmulrid  13178  xmulm1  13180  x2times  13198  xrub  13211  elicc01  13366  1elunit  13370  divelunit  13394  lincmb01cmp  13395  unitssre  13399  0nelfz1  13443  fzpreddisj  13473  fznatpl1  13478  fztpval  13486  fraclt1  13706  fracle1  13707  flbi2  13721  fldiv4p1lem1div2  13739  fldiv4lem1div2  13741  fldiv  13764  modid  13800  1mod  13807  m1modnnsub1  13824  modm1p1mod0  13829  seqf1olem1  13948  reexpcl  13985  reexpclz  13989  expge0  14005  expge1  14006  expgt1  14007  bernneq  14136  bernneq2  14137  expnbnd  14139  expnlbnd  14140  expnlbnd2  14141  expmulnbnd  14142  discr1  14146  facwordi  14196  faclbnd3  14199  faclbnd4lem1  14200  faclbnd4lem4  14203  faclbnd6  14206  facavg  14208  hashv01gt1  14252  hashnn0n0nn  14298  hashunsnggt  14301  hash1snb  14326  hashgt12el  14329  hashgt12el2  14330  hashfun  14344  hashge2el2dif  14387  tpf1ofv2  14405  lsw0  14472  f1oun2prg  14824  cjexp  15057  re1  15061  im1  15062  rei  15063  imi  15064  01sqrexlem1  15149  01sqrexlem2  15150  01sqrexlem3  15151  01sqrexlem4  15152  01sqrexlem7  15155  resqrex  15157  sqrt1  15178  sqrt2gt1lt2  15181  sqrtm1  15182  abs1  15204  absrdbnd  15249  caubnd2  15265  mulcn2  15503  reccn2  15504  rlimno1  15561  o1fsum  15720  expcnv  15771  geolim  15777  geolim2  15778  georeclim  15779  geomulcvg  15783  geoisumr  15785  geoisum1c  15787  fprodge0  15900  fprodge1  15902  rerisefaccl  15924  refallfaccl  15925  ere  15996  ege2le3  15997  efgt1  16025  resin4p  16047  recos4p  16048  tanhbnd  16070  sinbnd  16089  cosbnd  16090  sinbnd2  16091  cosbnd2  16092  ef01bndlem  16093  sin01bnd  16094  cos01bnd  16095  cos1bnd  16096  cos2bnd  16097  sinltx  16098  sin01gt0  16099  cos01gt0  16100  sin02gt0  16101  sincos1sgn  16102  ene1  16119  rpnnen2lem2  16124  rpnnen2lem3  16125  rpnnen2lem4  16126  rpnnen2lem9  16131  rpnnen2lem12  16134  ruclem6  16144  ruclem11  16149  ruclem12  16150  3dvds  16242  flodddiv4  16326  sadcadd  16369  isprm3  16594  sqnprm  16613  coprm  16622  phibndlem  16681  pythagtriplem3  16730  pcmpt  16804  fldivp1  16809  pockthi  16819  infpn2  16825  basendxnmulrndx  17200  starvndxnbasendx  17208  scandxnbasendx  17220  vscandxnbasendx  17225  ipndxnbasendx  17236  basendxnocndx  17287  slotsbhcdif  17319  lt6abl  19807  srgbinomlem4  20147  0ringnnzr  20440  abvneg  20741  abvtrivd  20747  xrsmcmn  21328  xrsnsgrp  21344  gzrngunitlem  21369  gzrngunit  21370  rge0srg  21375  psgnodpmr  21527  remulg  21544  resubdrg  21545  psdmvr  22084  dscmet  24487  dscopn  24488  nrginvrcnlem  24606  idnghm  24658  tgioo  24711  blcvx  24713  iicmp  24806  iiconn  24807  iirev  24850  iihalf1  24852  iihalf2  24855  iihalf2cnOLD  24857  elii1  24858  elii2  24859  iimulcl  24860  icopnfcnv  24867  icopnfhmeo  24868  iccpnfhmeo  24870  xrhmeo  24871  xrhmph  24872  evth  24885  xlebnum  24891  htpycc  24906  reparphti  24923  reparphtiOLD  24924  pcoval1  24940  pco1  24942  pcoval2  24943  pcocn  24944  pcohtpylem  24946  pcopt  24949  pcopt2  24950  pcoass  24951  pcorevlem  24953  nmhmcn  25047  ncvs1  25084  ovolunlem1a  25424  vitalilem2  25537  vitalilem4  25539  vitalilem5  25540  vitali  25541  i1f1  25618  itg11  25619  itg2const  25668  dveflem  25910  dvlipcn  25926  dvcvx  25952  ply1remlem  26097  fta1blem  26103  vieta1lem2  26246  aalioulem3  26269  aalioulem5  26271  aaliou3lem2  26278  ulmbdd  26334  iblulm  26343  radcnvlem1  26349  dvradcnv  26357  abelthlem2  26369  abelthlem3  26370  abelthlem5  26372  abelthlem7  26375  abelth  26378  abelth2  26379  reeff1olem  26383  reeff1o  26384  sinhalfpilem  26399  tangtx  26441  sincos4thpi  26449  pige3ALT  26456  coskpi  26459  cos0pilt1  26468  recosf1o  26471  tanregt0  26475  efif1olem3  26480  efif1olem4  26481  loge  26522  logdivlti  26556  logcnlem4  26581  logf1o2  26586  logtayl  26596  logccv  26599  recxpcl  26611  cxplea  26632  cxpcn3lem  26684  cxpaddlelem  26688  loglesqrt  26698  ang180lem2  26747  angpined  26767  acosrecl  26840  atancj  26847  atanlogaddlem  26850  atantan  26860  atans2  26868  ressatans  26871  leibpi  26879  log2le1  26887  birthdaylem3  26890  cxp2lim  26914  cxploglim  26915  cxploglim2  26916  divsqrtsumlem  26917  cvxcl  26922  scvxcvx  26923  jensenlem2  26925  amgmlem  26927  emcllem2  26934  emcllem4  26936  emcllem6  26938  emcllem7  26939  emre  26943  emgt0  26944  harmonicbnd3  26945  harmonicubnd  26947  harmonicbnd4  26948  zetacvg  26952  ftalem1  27010  ftalem2  27011  ftalem5  27014  issqf  27073  cht1  27102  chp1  27104  ppiltx  27114  mumullem2  27117  ppiublem1  27140  ppiub  27142  chtublem  27149  chtub  27150  logfacbnd3  27161  logexprlim  27163  perfectlem2  27168  dchrinv  27199  dchr1re  27201  efexple  27219  bposlem1  27222  bposlem2  27223  bposlem5  27226  bposlem8  27229  lgsdir2lem1  27263  lgsdir2lem5  27267  lgsdir  27270  lgsne0  27273  lgsabs1  27274  lgsdinn0  27283  gausslemma2dlem0i  27302  lgseisen  27317  m1lgs  27326  2lgslem3  27342  addsq2nreurex  27382  2sqreultblem  27386  2sqreunnltblem  27389  chebbnd1lem3  27409  chebbnd1  27410  chtppilimlem1  27411  chtppilimlem2  27412  chtppilim  27413  chpchtlim  27417  vmadivsumb  27421  rplogsumlem2  27423  rpvmasumlem  27425  dchrmusumlema  27431  dchrmusum2  27432  dchrvmasumlem2  27436  dchrvmasumiflem1  27439  dchrisum0flblem1  27446  dchrisum0flblem2  27447  dchrisum0fno1  27449  rpvmasum2  27450  dchrisum0re  27451  dchrisum0lema  27452  dchrisum0lem1b  27453  dchrisum0lem1  27454  dchrisum0lem2a  27455  dchrisum0lem2  27456  logdivsum  27471  mulog2sumlem2  27473  2vmadivsumlem  27478  log2sumbnd  27482  selbergb  27487  selberg2b  27490  chpdifbndlem1  27491  selberg3lem1  27495  selberg3lem2  27496  selberg4lem1  27498  pntrmax  27502  pntrsumo1  27503  selbergsb  27513  pntrlog2bndlem3  27517  pntrlog2bndlem5  27519  pntpbnd1a  27523  pntpbnd2  27525  pntibndlem1  27527  pntibndlem3  27530  pntlemd  27532  pntlemc  27533  pntlemb  27535  pntlemr  27540  pntlemf  27543  pntlemk  27544  pntlemo  27545  pntlem3  27547  pntleml  27549  abvcxp  27553  ostth2lem1  27556  ostth1  27571  ostth2lem2  27572  ostth2lem3  27573  ostth2lem4  27574  ostth2  27575  ostth3  27576  ostth  27577  slotsinbpsd  28419  slotslnbpsd  28420  trgcgrg  28493  brbtwn2  28883  colinearalglem4  28887  ax5seglem2  28907  ax5seglem3  28909  axpaschlem  28918  axpasch  28919  axlowdimlem6  28925  axlowdimlem10  28929  axlowdimlem16  28935  axlowdim1  28937  axlowdim2  28938  axlowdim  28939  axcontlem2  28943  elntg2  28963  lfgrnloop  29103  lfuhgr1v0e  29232  usgrexmpldifpr  29236  usgrexmplef  29237  1loopgrvd2  29482  vdegp1bi  29516  lfgrwlkprop  29664  pthdlem1  29744  pthdlem2  29746  clwlkclwwlkf  29988  upgr4cycl4dv4e  30165  konigsberglem2  30233  konigsberglem3  30234  konigsberglem5  30236  frgrreg  30374  ex-dif  30403  ex-in  30405  ex-pss  30408  ex-res  30421  ex-fl  30427  nv1  30655  smcnlem  30677  ipidsq  30690  nmlno0lem  30773  norm-ii-i  31117  bcs2  31162  norm1  31229  nmopub2tALT  31889  nmfnleub2  31906  nmlnop0iALT  31975  unopbd  31995  nmopadjlem  32069  nmopcoadji  32081  pjnmopi  32128  pjbdlni  32129  hstle1  32206  hstle  32210  hstles  32211  stge1i  32218  stlesi  32221  staddi  32226  stadd3i  32228  strlem1  32230  strlem5  32235  jplem1  32248  cdj1i  32413  addltmulALT  32426  xlt2addrd  32742  pr01ssre  32807  sgnclre  32815  sgnnbi  32821  sgnpbi  32822  sgnmulsgp  32826  indf  32836  indfval  32837  dp2lt10  32864  dp2ltsuc  32866  dp2ltc  32867  dplti  32885  dpmul4  32894  cshw1s2  32941  xrsmulgzz  32990  rearchi  33311  xrge0slmod  33313  prmidl0  33415  evl1deg3  33541  constrconj  33758  2sqr3minply  33793  submateqlem1  33820  xrge0iifcnv  33946  xrge0iifcv  33947  xrge0iifiso  33948  xrge0iifhom  33950  zrhre  34032  esumcst  34076  cntnevol  34241  omssubadd  34313  iwrdsplit  34400  dstfrvclim1  34491  coinfliprv  34496  ballotlem2  34502  ballotlem4  34512  ballotlemi1  34516  ballotlemic  34520  plymulx0  34560  plymulx  34561  signswch  34574  signstf  34579  signsvfn  34595  itgexpif  34619  hgt750lemd  34661  logdivsqrle  34663  hgt750lem  34664  hgt750lem2  34665  hgt750leme  34671  tgoldbachgnn  34672  subfacp1lem1  35223  subfacp1lem5  35228  resconn  35290  iisconn  35296  iillysconn  35297  problem2  35710  problem3  35711  sinccvglem  35716  fz0n  35775  dnibndlem12  36531  knoppcnlem4  36538  knoppndvlem13  36566  cnndvlem1  36579  irrdiff  37368  relowlpssretop  37406  sin2h  37658  cos2h  37659  tan2h  37660  poimirlem7  37675  poimirlem16  37684  poimirlem17  37685  poimirlem19  37687  poimirlem20  37688  poimirlem22  37690  poimirlem23  37691  poimirlem29  37697  poimirlem31  37699  itg2addnclem3  37721  asindmre  37751  dvasin  37752  dvacos  37753  dvreasin  37754  dvreacos  37755  fdc  37793  geomcau  37807  cntotbnd  37844  heiborlem8  37866  bfplem2  37871  bfp  37872  aks4d1p1p7  42115  1t1e1ALT  42296  ine1  42355  re1m1e0m0  42438  sn-00idlem1  42439  sn-00idlem2  42440  remul02  42446  sn-0ne2  42447  reixi  42464  rei4  42465  remullid  42475  ipiiie0  42479  sn-0tie0  42492  sn-nnne0  42501  mulgt0b1d  42513  sn-0lt1  42516  sn-ltp1  42517  reneg1lt0  42521  sn-inelr  42528  rabren3dioph  42856  pellexlem5  42874  pellexlem6  42875  pell1qrgaplem  42914  pell14qrgap  42916  pellqrex  42920  pellfundre  42922  pellfundlb  42925  pellfund14gap  42928  jm2.17a  43001  acongeq  43024  jm2.23  43037  jm3.1lem2  43059  sqrtcval  43682  sqrtcval2  43683  resqrtval  43684  imsqrtval  43685  relexp01min  43754  cvgdvgrat  44354  lhe4.4ex1a  44370  binomcxplemnotnn0  44397  isosctrlem1ALT  44974  supxrgelem  45384  xrlexaddrp  45399  infxr  45413  infleinflem2  45417  sumnnodd  45678  limsup10exlem  45818  limsup10ex  45819  dvnprodlem3  45994  stoweidlem1  46047  stoweidlem18  46064  stoweidlem19  46065  stoweidlem26  46072  stoweidlem34  46080  stoweidlem40  46086  stoweidlem41  46087  stoweidlem59  46105  stoweid  46109  stirlinglem10  46129  stirlinglem11  46130  dirkercncflem1  46149  fourierdlem16  46169  fourierdlem21  46174  fourierdlem22  46175  fourierdlem42  46195  fourierdlem68  46220  fourierdlem83  46235  fourierdlem103  46255  sqwvfourb  46275  fouriersw  46277  etransclem23  46303  salgencntex  46389  ovn0lem  46611  smfmullem3  46839  smfmullem4  46840  cjnpoly  46928  zm1nn  47341  ceilhalf1  47373  m1mod0mod1  47393  fmtnosqrt  47578  perfectALTVlem2  47761  2exp340mod341  47772  8exp8mod9  47775  nfermltl8rev  47781  nnsum3primesprm  47829  nnsum4primesodd  47835  nnsum4primesoddALTV  47836  nnsum4primeseven  47839  nnsum4primesevenALTV  47840  tgblthelfgott  47854  tgoldbach  47856  usgrexmpl1lem  48060  usgrexmpl2lem  48065  usgrexmpl2nb1  48071  usgrexmpl2nb3  48073  usgrexmpl2nb4  48074  usgrexmpl2nb5  48075  usgrexmpl2trifr  48076  gpg3kgrtriexlem3  48124  pgnbgreunbgrlem2lem1  48153  pgnbgreunbgrlem2lem2  48154  rege1logbrege0  48598  rege1logbzge0  48599  blennnelnn  48616  dignnld  48643  nn0sumshdiglemA  48659  nn0sumshdiglem1  48661  rrx2xpref1o  48758  rrxlines  48773  eenglngeehlnmlem1  48777  eenglngeehlnmlem2  48778  line2ylem  48791  line2x  48794  icccldii  48958  io1ii  48960  sepfsepc  48967