Theorem 1re 11258

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 11210, 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 11221	. . 3 ⊢ 1 ≠ 0
2		ax-1cn 11210	. . . . 5 ⊢ 1 ∈ ℂ
3		cnre 11255	. . . . 5 ⊢ (1 ∈ ℂ → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)))
4	2, 3	ax-mp 5	. . . 4 ⊢ ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏))
5		neeq1 3000	. . . . . . . 8 ⊢ (1 = (𝑎 + (i · 𝑏)) → (1 ≠ 0 ↔ (𝑎 + (i · 𝑏)) ≠ 0))
6	5	biimpcd 249	. . . . . . 7 ⊢ (1 ≠ 0 → (1 = (𝑎 + (i · 𝑏)) → (𝑎 + (i · 𝑏)) ≠ 0))
7		0cn 11250	. . . . . . . 8 ⊢ 0 ∈ ℂ
8		cnre 11255	. . . . . . . 8 ⊢ (0 ∈ ℂ → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)))
9	7, 8	ax-mp 5	. . . . . . 7 ⊢ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑))
10		neeq2 3001	. . . . . . . . . 10 ⊢ (0 = (𝑐 + (i · 𝑑)) → ((𝑎 + (i · 𝑏)) ≠ 0 ↔ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
11	10	biimpcd 249	. . . . . . . . 9 ⊢ ((𝑎 + (i · 𝑏)) ≠ 0 → (0 = (𝑐 + (i · 𝑑)) → (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
12	11	reximdv 3167	. . . . . . . 8 ⊢ ((𝑎 + (i · 𝑏)) ≠ 0 → (∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)) → ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
13	12	reximdv 3167	. . . . . . 7 ⊢ ((𝑎 + (i · 𝑏)) ≠ 0 → (∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)) → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
14	6, 9, 13	syl6mpi 67	. . . . . 6 ⊢ (1 ≠ 0 → (1 = (𝑎 + (i · 𝑏)) → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
15	14	reximdv 3167	. . . . 5 ⊢ (1 ≠ 0 → (∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)) → ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
16	15	reximdv 3167	. . . 4 ⊢ (1 ≠ 0 → (∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)) → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
17	4, 16	mpi 20	. . 3 ⊢ (1 ≠ 0 → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)))
18		ioran 985	. . . . . . . . 9 ⊢ (¬ (𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑) ↔ (¬ 𝑎 ≠ 𝑐 ∧ ¬ 𝑏 ≠ 𝑑))
19		df-ne 2938	. . . . . . . . . . 11 ⊢ (𝑎 ≠ 𝑐 ↔ ¬ 𝑎 = 𝑐)
20	19	con2bii 357	. . . . . . . . . 10 ⊢ (𝑎 = 𝑐 ↔ ¬ 𝑎 ≠ 𝑐)
21		df-ne 2938	. . . . . . . . . . 11 ⊢ (𝑏 ≠ 𝑑 ↔ ¬ 𝑏 = 𝑑)
22	21	con2bii 357	. . . . . . . . . 10 ⊢ (𝑏 = 𝑑 ↔ ¬ 𝑏 ≠ 𝑑)
23	20, 22	anbi12i 628	. . . . . . . . 9 ⊢ ((𝑎 = 𝑐 ∧ 𝑏 = 𝑑) ↔ (¬ 𝑎 ≠ 𝑐 ∧ ¬ 𝑏 ≠ 𝑑))
24	18, 23	bitr4i 278	. . . . . . . 8 ⊢ (¬ (𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑) ↔ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑))
25		id 22	. . . . . . . . 9 ⊢ (𝑎 = 𝑐 → 𝑎 = 𝑐)
26		oveq2 7438	. . . . . . . . 9 ⊢ (𝑏 = 𝑑 → (i · 𝑏) = (i · 𝑑))
27	25, 26	oveqan12d 7449	. . . . . . . 8 ⊢ ((𝑎 = 𝑐 ∧ 𝑏 = 𝑑) → (𝑎 + (i · 𝑏)) = (𝑐 + (i · 𝑑)))
28	24, 27	sylbi 217	. . . . . . 7 ⊢ (¬ (𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑) → (𝑎 + (i · 𝑏)) = (𝑐 + (i · 𝑑)))
29	28	necon1ai 2965	. . . . . 6 ⊢ ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → (𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑))
30		neeq1 3000	. . . . . . . . . 10 ⊢ (𝑥 = 𝑎 → (𝑥 ≠ 𝑦 ↔ 𝑎 ≠ 𝑦))
31		neeq2 3001	. . . . . . . . . 10 ⊢ (𝑦 = 𝑐 → (𝑎 ≠ 𝑦 ↔ 𝑎 ≠ 𝑐))
32	30, 31	rspc2ev 3634	. . . . . . . . 9 ⊢ ((𝑎 ∈ ℝ ∧ 𝑐 ∈ ℝ ∧ 𝑎 ≠ 𝑐) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦)
33	32	3expia 1120	. . . . . . . 8 ⊢ ((𝑎 ∈ ℝ ∧ 𝑐 ∈ ℝ) → (𝑎 ≠ 𝑐 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
34	33	ad2ant2r 747	. . . . . . 7 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → (𝑎 ≠ 𝑐 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
35		neeq1 3000	. . . . . . . . . 10 ⊢ (𝑥 = 𝑏 → (𝑥 ≠ 𝑦 ↔ 𝑏 ≠ 𝑦))
36		neeq2 3001	. . . . . . . . . 10 ⊢ (𝑦 = 𝑑 → (𝑏 ≠ 𝑦 ↔ 𝑏 ≠ 𝑑))
37	35, 36	rspc2ev 3634	. . . . . . . . 9 ⊢ ((𝑏 ∈ ℝ ∧ 𝑑 ∈ ℝ ∧ 𝑏 ≠ 𝑑) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦)
38	37	3expia 1120	. . . . . . . 8 ⊢ ((𝑏 ∈ ℝ ∧ 𝑑 ∈ ℝ) → (𝑏 ≠ 𝑑 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
39	38	ad2ant2l 746	. . . . . . 7 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → (𝑏 ≠ 𝑑 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
40	34, 39	jaod 859	. . . . . 6 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → ((𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
41	29, 40	syl5 34	. . . . 5 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
42	41	rexlimdvva 3210	. . . 4 ⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
43	42	rexlimivv 3198	. . 3 ⊢ (∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦)
44	1, 17, 43	mp2b 10	. 2 ⊢ ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦
45		eqtr3 2760	. . . . . . . . 9 ⊢ ((𝑥 = 0 ∧ 𝑦 = 0) → 𝑥 = 𝑦)
46	45	ex 412	. . . . . . . 8 ⊢ (𝑥 = 0 → (𝑦 = 0 → 𝑥 = 𝑦))
47	46	necon3d 2958	. . . . . . 7 ⊢ (𝑥 = 0 → (𝑥 ≠ 𝑦 → 𝑦 ≠ 0))
48		neeq1 3000	. . . . . . . . 9 ⊢ (𝑧 = 𝑦 → (𝑧 ≠ 0 ↔ 𝑦 ≠ 0))
49	48	rspcev 3621	. . . . . . . 8 ⊢ ((𝑦 ∈ ℝ ∧ 𝑦 ≠ 0) → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)
50	49	expcom 413	. . . . . . 7 ⊢ (𝑦 ≠ 0 → (𝑦 ∈ ℝ → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
51	47, 50	syl6 35	. . . . . 6 ⊢ (𝑥 = 0 → (𝑥 ≠ 𝑦 → (𝑦 ∈ ℝ → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
52	51	com23 86	. . . . 5 ⊢ (𝑥 = 0 → (𝑦 ∈ ℝ → (𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
53	52	adantld 490	. . . 4 ⊢ (𝑥 = 0 → ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
54		neeq1 3000	. . . . . . . 8 ⊢ (𝑧 = 𝑥 → (𝑧 ≠ 0 ↔ 𝑥 ≠ 0))
55	54	rspcev 3621	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)
56	55	expcom 413	. . . . . 6 ⊢ (𝑥 ≠ 0 → (𝑥 ∈ ℝ → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
57	56	adantrd 491	. . . . 5 ⊢ (𝑥 ≠ 0 → ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
58	57	a1dd 50	. . . 4 ⊢ (𝑥 ≠ 0 → ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
59	53, 58	pm2.61ine 3022	. . 3 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
60	59	rexlimivv 3198	. 2 ⊢ (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)
61		ax-rrecex 11224	. . . 4 ⊢ ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → ∃𝑥 ∈ ℝ (𝑧 · 𝑥) = 1)
62		remulcl 11237	. . . . . . 7 ⊢ ((𝑧 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (𝑧 · 𝑥) ∈ ℝ)
63	62	adantlr 715	. . . . . 6 ⊢ (((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) ∧ 𝑥 ∈ ℝ) → (𝑧 · 𝑥) ∈ ℝ)
64		eleq1 2826	. . . . . 6 ⊢ ((𝑧 · 𝑥) = 1 → ((𝑧 · 𝑥) ∈ ℝ ↔ 1 ∈ ℝ))
65	63, 64	syl5ibcom 245	. . . . 5 ⊢ (((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) ∧ 𝑥 ∈ ℝ) → ((𝑧 · 𝑥) = 1 → 1 ∈ ℝ))
66	65	rexlimdva 3152	. . . 4 ⊢ ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → (∃𝑥 ∈ ℝ (𝑧 · 𝑥) = 1 → 1 ∈ ℝ))
67	61, 66	mpd 15	. . 3 ⊢ ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → 1 ∈ ℝ)
68	67	rexlimiva 3144	. 2 ⊢ (∃𝑧 ∈ ℝ 𝑧 ≠ 0 → 1 ∈ ℝ)
69	44, 60, 68	mp2b 10	1 ⊢ 1 ∈ ℝ

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∨ wo 847   = wceq 1536   ∈ wcel 2105   ≠ wne 2937  ∃wrex 3067  (class class class)co 7430  ℂcc 11150  ℝcr 11151  0cc0 11152  1c1 11153  ici 11154   + caddc 11155   · cmul 11157

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-mulcl 11214  ax-mulrcl 11215  ax-i2m1 11220  ax-1ne0 11221  ax-rrecex 11224  ax-cnre 11225

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ne 2938  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-iota 6515  df-fv 6570  df-ov 7433

This theorem is referenced by:  1red  11259  1xr  11317  dedekind  11421  peano2re  11431  mul02lem2  11435  addrid  11438  renegcl  11569  peano2rem  11573  0reALT  11603  0lt1  11782  0le1  11783  relin01  11784  1le1  11888  eqneg  11984  ltp1  12104  ltm1  12106  recgt0  12110  mulgt1OLD  12123  ltmulgt11  12124  lemulge11  12127  reclt1  12160  recgt1  12161  recgt1i  12162  recp1lt1  12163  recreclt  12164  recgt0ii  12171  ledivp1i  12190  ltdivp1i  12191  inelr  12253  cju  12259  nnssre  12267  nnge1  12291  nngt1ne1  12292  nnle1eq1  12293  nngt0  12294  nnnlt1  12295  nnne0  12297  nnrecre  12305  nnrecgt0  12306  nnsub  12307  2re  12337  3re  12343  4re  12347  5re  12350  6re  12353  7re  12356  8re  12359  9re  12362  0le2  12365  2pos  12366  3pos  12368  4pos  12370  5pos  12372  6pos  12373  7pos  12374  8pos  12375  9pos  12376  neg1rr  12378  neg1lt0  12380  1lt2  12434  1lt3  12436  1lt4  12439  1lt5  12443  1lt6  12448  1lt7  12454  1lt8  12461  1lt9  12469  1ne2  12471  1le2  12472  1le3  12475  halflt1  12481  addltmul  12499  nnunb  12519  elnnnn0c  12568  nn0ge2m1nn  12593  elnnz1  12640  znnnlt1  12641  zltp1le  12664  zleltp1  12665  nn0lt2  12678  recnz  12690  gtndiv  12692  3halfnz  12694  10re  12749  1lt10  12869  eluzp1m1  12901  eluzp1p1  12903  eluz2b2  12960  zbtwnre  12985  rebtwnz  12986  1rp  13035  divlt1lt  13101  divle1le  13102  nnledivrp  13144  qbtwnxr  13238  xmulrid  13317  xmulm1  13319  x2times  13337  xrub  13350  elicc01  13502  1elunit  13506  divelunit  13530  lincmb01cmp  13531  unitssre  13535  0nelfz1  13579  fzpreddisj  13609  fznatpl1  13614  fztpval  13622  fraclt1  13838  fracle1  13839  flbi2  13853  fldiv4p1lem1div2  13871  fldiv4lem1div2  13873  fldiv  13896  modid  13932  1mod  13939  m1modnnsub1  13954  modm1p1mod0  13959  seqf1olem1  14078  reexpcl  14115  reexpclz  14119  expge0  14135  expge1  14136  expgt1  14137  bernneq  14264  bernneq2  14265  expnbnd  14267  expnlbnd  14268  expnlbnd2  14269  expmulnbnd  14270  discr1  14274  facwordi  14324  faclbnd3  14327  faclbnd4lem1  14328  faclbnd4lem4  14331  faclbnd6  14334  facavg  14336  hashv01gt1  14380  hashnn0n0nn  14426  hashunsnggt  14429  hash1snb  14454  hashgt12el  14457  hashgt12el2  14458  hashfun  14472  hashge2el2dif  14515  tpf1ofv2  14533  lsw0  14599  f1oun2prg  14952  cjexp  15185  re1  15189  im1  15190  rei  15191  imi  15192  01sqrexlem1  15277  01sqrexlem2  15278  01sqrexlem3  15279  01sqrexlem4  15280  01sqrexlem7  15283  resqrex  15285  sqrt1  15306  sqrt2gt1lt2  15309  sqrtm1  15310  abs1  15332  absrdbnd  15376  caubnd2  15392  mulcn2  15628  reccn2  15629  rlimno1  15686  o1fsum  15845  expcnv  15896  geolim  15902  geolim2  15903  georeclim  15904  geomulcvg  15908  geoisumr  15910  geoisum1c  15912  fprodge0  16025  fprodge1  16027  rerisefaccl  16049  refallfaccl  16050  ere  16121  ege2le3  16122  efgt1  16148  resin4p  16170  recos4p  16171  tanhbnd  16193  sinbnd  16212  cosbnd  16213  sinbnd2  16214  cosbnd2  16215  ef01bndlem  16216  sin01bnd  16217  cos01bnd  16218  cos1bnd  16219  cos2bnd  16220  sinltx  16221  sin01gt0  16222  cos01gt0  16223  sin02gt0  16224  sincos1sgn  16225  ene1  16242  rpnnen2lem2  16247  rpnnen2lem3  16248  rpnnen2lem4  16249  rpnnen2lem9  16254  rpnnen2lem12  16257  ruclem6  16267  ruclem11  16272  ruclem12  16273  3dvds  16364  flodddiv4  16448  sadcadd  16491  isprm3  16716  sqnprm  16735  coprm  16744  phibndlem  16803  pythagtriplem3  16851  pcmpt  16925  fldivp1  16930  pockthi  16940  infpn2  16946  resslemOLD  17287  basendxnmulrndx  17340  basendxnmulrndxOLD  17341  starvndxnbasendx  17349  scandxnbasendx  17361  vscandxnbasendx  17366  ipndxnbasendx  17377  basendxnocndx  17428  slotsbhcdif  17460  slotsbhcdifOLD  17461  oppcbasOLD  17764  rescbasOLD  17877  rescabsOLD  17883  odubasOLD  18348  symgvalstructOLD  19429  lt6abl  19927  srgbinomlem4  20246  0ringnnzr  20541  abvneg  20843  abvtrivd  20849  rmodislmodOLD  20945  cnfldfunALTOLDOLD  21410  xrsmcmn  21421  xrsnsgrp  21437  gzrngunitlem  21467  gzrngunit  21468  rge0srg  21473  psgnodpmr  21625  remulg  21642  resubdrg  21643  thlbasOLD  21732  tuslemOLD  24291  setsmsbasOLD  24501  dscmet  24600  dscopn  24601  nrginvrcnlem  24727  idnghm  24779  tgioo  24831  blcvx  24833  iicmp  24925  iiconn  24926  iirev  24969  iihalf1  24971  iihalf2  24974  iihalf2cnOLD  24976  elii1  24977  elii2  24978  iimulcl  24979  icopnfcnv  24986  icopnfhmeo  24987  iccpnfhmeo  24989  xrhmeo  24990  xrhmph  24991  evth  25004  xlebnum  25010  htpycc  25025  reparphti  25042  reparphtiOLD  25043  pcoval1  25059  pco1  25061  pcoval2  25062  pcocn  25063  pcohtpylem  25065  pcopt  25068  pcopt2  25069  pcoass  25070  pcorevlem  25072  nmhmcn  25166  ncvs1  25204  ovolunlem1a  25544  vitalilem2  25657  vitalilem4  25659  vitalilem5  25660  vitali  25661  i1f1  25738  itg11  25739  itg2const  25789  dveflem  26031  dvlipcn  26047  dvcvx  26073  ply1remlem  26218  fta1blem  26224  vieta1lem2  26367  aalioulem3  26390  aalioulem5  26392  aaliou3lem2  26399  ulmbdd  26455  iblulm  26464  radcnvlem1  26470  dvradcnv  26478  abelthlem2  26490  abelthlem3  26491  abelthlem5  26493  abelthlem7  26496  abelth  26499  abelth2  26500  reeff1olem  26504  reeff1o  26505  sinhalfpilem  26519  tangtx  26561  sincos4thpi  26569  pige3ALT  26576  coskpi  26579  cos0pilt1  26588  recosf1o  26591  tanregt0  26595  efif1olem3  26600  efif1olem4  26601  loge  26642  logdivlti  26676  logcnlem4  26701  logf1o2  26706  logtayl  26716  logccv  26719  recxpcl  26731  cxplea  26752  cxpcn3lem  26804  cxpaddlelem  26808  loglesqrt  26818  ang180lem2  26867  angpined  26887  acosrecl  26960  atancj  26967  atanlogaddlem  26970  atantan  26980  atans2  26988  ressatans  26991  leibpi  26999  log2le1  27007  birthdaylem3  27010  cxp2lim  27034  cxploglim  27035  cxploglim2  27036  divsqrtsumlem  27037  cvxcl  27042  scvxcvx  27043  jensenlem2  27045  amgmlem  27047  emcllem2  27054  emcllem4  27056  emcllem6  27058  emcllem7  27059  emre  27063  emgt0  27064  harmonicbnd3  27065  harmonicubnd  27067  harmonicbnd4  27068  zetacvg  27072  ftalem1  27130  ftalem2  27131  ftalem5  27134  issqf  27193  cht1  27222  chp1  27224  ppiltx  27234  mumullem2  27237  ppiublem1  27260  ppiub  27262  chtublem  27269  chtub  27270  logfacbnd3  27281  logexprlim  27283  perfectlem2  27288  dchrinv  27319  dchr1re  27321  efexple  27339  bposlem1  27342  bposlem2  27343  bposlem5  27346  bposlem8  27349  lgsdir2lem1  27383  lgsdir2lem5  27387  lgsdir  27390  lgsne0  27393  lgsabs1  27394  lgsdinn0  27403  gausslemma2dlem0i  27422  lgseisen  27437  m1lgs  27446  2lgslem3  27462  addsq2nreurex  27502  2sqreultblem  27506  2sqreunnltblem  27509  chebbnd1lem3  27529  chebbnd1  27530  chtppilimlem1  27531  chtppilimlem2  27532  chtppilim  27533  chpchtlim  27537  vmadivsumb  27541  rplogsumlem2  27543  rpvmasumlem  27545  dchrmusumlema  27551  dchrmusum2  27552  dchrvmasumlem2  27556  dchrvmasumiflem1  27559  dchrisum0flblem1  27566  dchrisum0flblem2  27567  dchrisum0fno1  27569  rpvmasum2  27570  dchrisum0re  27571  dchrisum0lema  27572  dchrisum0lem1b  27573  dchrisum0lem1  27574  dchrisum0lem2a  27575  dchrisum0lem2  27576  logdivsum  27591  mulog2sumlem2  27593  2vmadivsumlem  27598  log2sumbnd  27602  selbergb  27607  selberg2b  27610  chpdifbndlem1  27611  selberg3lem1  27615  selberg3lem2  27616  selberg4lem1  27618  pntrmax  27622  pntrsumo1  27623  selbergsb  27633  pntrlog2bndlem3  27637  pntrlog2bndlem5  27639  pntpbnd1a  27643  pntpbnd2  27645  pntibndlem1  27647  pntibndlem3  27650  pntlemd  27652  pntlemc  27653  pntlemb  27655  pntlemr  27660  pntlemf  27663  pntlemk  27664  pntlemo  27665  pntlem3  27667  pntleml  27669  abvcxp  27673  ostth2lem1  27676  ostth1  27691  ostth2lem2  27692  ostth2lem3  27693  ostth2lem4  27694  ostth2  27695  ostth3  27696  ostth  27697  slotsinbpsd  28463  slotslnbpsd  28464  trgcgrg  28537  brbtwn2  28934  colinearalglem4  28938  ax5seglem2  28958  ax5seglem3  28960  axpaschlem  28969  axpasch  28970  axlowdimlem6  28976  axlowdimlem10  28980  axlowdimlem16  28986  axlowdim1  28988  axlowdim2  28989  axlowdim  28990  axcontlem2  28994  elntg2  29014  lfgrnloop  29156  lfuhgr1v0e  29285  usgrexmpldifpr  29289  usgrexmplef  29290  1loopgrvd2  29535  vdegp1bi  29569  lfgrwlkprop  29719  pthdlem1  29798  pthdlem2  29800  clwlkclwwlkf  30036  upgr4cycl4dv4e  30213  konigsberglem2  30281  konigsberglem3  30282  konigsberglem5  30284  frgrreg  30422  ex-dif  30451  ex-in  30453  ex-pss  30456  ex-res  30469  ex-fl  30475  nv1  30703  smcnlem  30725  ipidsq  30738  nmlno0lem  30821  norm-ii-i  31165  bcs2  31210  norm1  31277  nmopub2tALT  31937  nmfnleub2  31954  nmlnop0iALT  32023  unopbd  32043  nmopadjlem  32117  nmopcoadji  32129  pjnmopi  32176  pjbdlni  32177  hstle1  32254  hstle  32258  hstles  32259  stge1i  32266  stlesi  32269  staddi  32274  stadd3i  32276  strlem1  32278  strlem5  32283  jplem1  32296  cdj1i  32461  addltmulALT  32474  xlt2addrd  32768  pr01ssre  32830  dp2lt10  32850  dp2ltsuc  32852  dp2ltc  32853  dplti  32871  dpmul4  32880  cshw1s2  32929  xrsmulgzz  32993  resvbasOLD  33339  rearchi  33353  xrge0slmod  33355  prmidl0  33457  evl1deg3  33582  constrconj  33749  2sqr3minply  33752  submateqlem1  33767  xrge0iifcnv  33893  xrge0iifcv  33894  xrge0iifiso  33895  xrge0iifhom  33897  zrhre  33981  indf  33995  indfval  33996  esumcst  34043  cntnevol  34208  omssubadd  34281  iwrdsplit  34368  dstfrvclim1  34458  coinfliprv  34463  ballotlem2  34469  ballotlem4  34479  ballotlemi1  34483  ballotlemic  34487  sgnclre  34520  sgnnbi  34526  sgnpbi  34527  sgnmulsgp  34531  plymulx0  34540  plymulx  34541  signswch  34554  signstf  34559  signsvfn  34575  itgexpif  34599  hgt750lemd  34641  logdivsqrle  34643  hgt750lem  34644  hgt750lem2  34645  hgt750leme  34651  tgoldbachgnn  34652  subfacp1lem1  35163  subfacp1lem5  35168  resconn  35230  iisconn  35236  iillysconn  35237  problem2  35650  problem3  35651  sinccvglem  35656  fz0n  35710  dnibndlem12  36471  knoppcnlem4  36478  knoppndvlem13  36506  cnndvlem1  36519  irrdiff  37308  relowlpssretop  37346  sin2h  37596  cos2h  37597  tan2h  37598  poimirlem7  37613  poimirlem16  37622  poimirlem17  37623  poimirlem19  37625  poimirlem20  37626  poimirlem22  37628  poimirlem23  37629  poimirlem29  37635  poimirlem31  37637  itg2addnclem3  37659  asindmre  37689  dvasin  37690  dvacos  37691  dvreasin  37692  dvreacos  37693  fdc  37731  geomcau  37745  cntotbnd  37782  heiborlem8  37804  bfplem2  37809  bfp  37810  aks4d1p1p7  42055  2xp3dxp2ge1d  42222  factwoffsmonot  42223  1t1e1ALT  42274  ine1  42327  re1m1e0m0  42403  sn-00idlem1  42404  sn-00idlem2  42405  remul02  42411  sn-0ne2  42412  reixi  42428  rei4  42429  remullid  42439  ipiiie0  42443  sn-0tie0  42445  sn-nnne0  42454  mulgt0b2d  42466  sn-0lt1  42469  sn-ltp1  42470  reneg1lt0  42472  sn-inelr  42473  rabren3dioph  42802  pellexlem5  42820  pellexlem6  42821  pell1qrgaplem  42860  pell14qrgap  42862  pellqrex  42866  pellfundre  42868  pellfundlb  42871  pellfund14gap  42874  jm2.17a  42948  acongeq  42971  jm2.23  42984  jm3.1lem2  43006  sqrtcval  43630  sqrtcval2  43631  resqrtval  43632  imsqrtval  43633  relexp01min  43702  mnringbasedOLD  44207  cvgdvgrat  44308  lhe4.4ex1a  44324  binomcxplemnotnn0  44351  isosctrlem1ALT  44931  supxrgelem  45286  xrlexaddrp  45301  infxr  45316  infleinflem2  45320  sumnnodd  45585  limsup10exlem  45727  limsup10ex  45728  dvnprodlem3  45903  stoweidlem1  45956  stoweidlem18  45973  stoweidlem19  45974  stoweidlem26  45981  stoweidlem34  45989  stoweidlem40  45995  stoweidlem41  45996  stoweidlem59  46014  stoweid  46018  stirlinglem10  46038  stirlinglem11  46039  dirkercncflem1  46058  fourierdlem16  46078  fourierdlem21  46083  fourierdlem22  46084  fourierdlem42  46104  fourierdlem68  46129  fourierdlem83  46144  fourierdlem103  46164  sqwvfourb  46184  fouriersw  46186  etransclem23  46212  salgencntex  46298  ovn0lem  46520  smfmullem3  46748  smfmullem4  46749  zm1nn  47251  m1mod0mod1  47293  fmtnosqrt  47463  perfectALTVlem2  47646  2exp340mod341  47657  8exp8mod9  47660  nfermltl8rev  47666  nnsum3primesprm  47714  nnsum4primesodd  47720  nnsum4primesoddALTV  47721  nnsum4primeseven  47724  nnsum4primesevenALTV  47725  tgblthelfgott  47739  tgoldbach  47741  usgrexmpl1lem  47915  usgrexmpl2lem  47920  usgrexmpl2nb1  47926  usgrexmpl2nb3  47928  usgrexmpl2nb4  47929  usgrexmpl2nb5  47930  usgrexmpl2trifr  47931  rege1logbrege0  48407  rege1logbzge0  48408  blennnelnn  48425  dignnld  48452  nn0sumshdiglemA  48468  nn0sumshdiglem1  48470  rrx2xpref1o  48567  rrxlines  48582  eenglngeehlnmlem1  48586  eenglngeehlnmlem2  48587  line2ylem  48600  line2x  48603  icccldii  48714  io1ii  48716  sepfsepc  48723