Theorem 1re 10982

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 10936, 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 10947	. . 3 ⊢ 1 ≠ 0
2		ax-1cn 10936	. . . . 5 ⊢ 1 ∈ ℂ
3		cnre 10979	. . . . 5 ⊢ (1 ∈ ℂ → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)))
4	2, 3	ax-mp 5	. . . 4 ⊢ ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏))
5		neeq1 3003	. . . . . . . 8 ⊢ (1 = (𝑎 + (i · 𝑏)) → (1 ≠ 0 ↔ (𝑎 + (i · 𝑏)) ≠ 0))
6	5	biimpcd 248	. . . . . . 7 ⊢ (1 ≠ 0 → (1 = (𝑎 + (i · 𝑏)) → (𝑎 + (i · 𝑏)) ≠ 0))
7		0cn 10974	. . . . . . . 8 ⊢ 0 ∈ ℂ
8		cnre 10979	. . . . . . . 8 ⊢ (0 ∈ ℂ → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)))
9	7, 8	ax-mp 5	. . . . . . 7 ⊢ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑))
10		neeq2 3004	. . . . . . . . . 10 ⊢ (0 = (𝑐 + (i · 𝑑)) → ((𝑎 + (i · 𝑏)) ≠ 0 ↔ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
11	10	biimpcd 248	. . . . . . . . 9 ⊢ ((𝑎 + (i · 𝑏)) ≠ 0 → (0 = (𝑐 + (i · 𝑑)) → (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
12	11	reximdv 3212	. . . . . . . 8 ⊢ ((𝑎 + (i · 𝑏)) ≠ 0 → (∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)) → ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
13	12	reximdv 3212	. . . . . . 7 ⊢ ((𝑎 + (i · 𝑏)) ≠ 0 → (∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)) → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
14	6, 9, 13	syl6mpi 67	. . . . . 6 ⊢ (1 ≠ 0 → (1 = (𝑎 + (i · 𝑏)) → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
15	14	reximdv 3212	. . . . 5 ⊢ (1 ≠ 0 → (∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)) → ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
16	15	reximdv 3212	. . . 4 ⊢ (1 ≠ 0 → (∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)) → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
17	4, 16	mpi 20	. . 3 ⊢ (1 ≠ 0 → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)))
18		ioran 981	. . . . . . . . 9 ⊢ (¬ (𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑) ↔ (¬ 𝑎 ≠ 𝑐 ∧ ¬ 𝑏 ≠ 𝑑))
19		df-ne 2941	. . . . . . . . . . 11 ⊢ (𝑎 ≠ 𝑐 ↔ ¬ 𝑎 = 𝑐)
20	19	con2bii 358	. . . . . . . . . 10 ⊢ (𝑎 = 𝑐 ↔ ¬ 𝑎 ≠ 𝑐)
21		df-ne 2941	. . . . . . . . . . 11 ⊢ (𝑏 ≠ 𝑑 ↔ ¬ 𝑏 = 𝑑)
22	21	con2bii 358	. . . . . . . . . 10 ⊢ (𝑏 = 𝑑 ↔ ¬ 𝑏 ≠ 𝑑)
23	20, 22	anbi12i 627	. . . . . . . . 9 ⊢ ((𝑎 = 𝑐 ∧ 𝑏 = 𝑑) ↔ (¬ 𝑎 ≠ 𝑐 ∧ ¬ 𝑏 ≠ 𝑑))
24	18, 23	bitr4i 277	. . . . . . . 8 ⊢ (¬ (𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑) ↔ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑))
25		id 22	. . . . . . . . 9 ⊢ (𝑎 = 𝑐 → 𝑎 = 𝑐)
26		oveq2 7290	. . . . . . . . 9 ⊢ (𝑏 = 𝑑 → (i · 𝑏) = (i · 𝑑))
27	25, 26	oveqan12d 7301	. . . . . . . 8 ⊢ ((𝑎 = 𝑐 ∧ 𝑏 = 𝑑) → (𝑎 + (i · 𝑏)) = (𝑐 + (i · 𝑑)))
28	24, 27	sylbi 216	. . . . . . 7 ⊢ (¬ (𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑) → (𝑎 + (i · 𝑏)) = (𝑐 + (i · 𝑑)))
29	28	necon1ai 2968	. . . . . 6 ⊢ ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → (𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑))
30		neeq1 3003	. . . . . . . . . 10 ⊢ (𝑥 = 𝑎 → (𝑥 ≠ 𝑦 ↔ 𝑎 ≠ 𝑦))
31		neeq2 3004	. . . . . . . . . 10 ⊢ (𝑦 = 𝑐 → (𝑎 ≠ 𝑦 ↔ 𝑎 ≠ 𝑐))
32	30, 31	rspc2ev 3571	. . . . . . . . 9 ⊢ ((𝑎 ∈ ℝ ∧ 𝑐 ∈ ℝ ∧ 𝑎 ≠ 𝑐) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦)
33	32	3expia 1120	. . . . . . . 8 ⊢ ((𝑎 ∈ ℝ ∧ 𝑐 ∈ ℝ) → (𝑎 ≠ 𝑐 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
34	33	ad2ant2r 744	. . . . . . 7 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → (𝑎 ≠ 𝑐 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
35		neeq1 3003	. . . . . . . . . 10 ⊢ (𝑥 = 𝑏 → (𝑥 ≠ 𝑦 ↔ 𝑏 ≠ 𝑦))
36		neeq2 3004	. . . . . . . . . 10 ⊢ (𝑦 = 𝑑 → (𝑏 ≠ 𝑦 ↔ 𝑏 ≠ 𝑑))
37	35, 36	rspc2ev 3571	. . . . . . . . 9 ⊢ ((𝑏 ∈ ℝ ∧ 𝑑 ∈ ℝ ∧ 𝑏 ≠ 𝑑) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦)
38	37	3expia 1120	. . . . . . . 8 ⊢ ((𝑏 ∈ ℝ ∧ 𝑑 ∈ ℝ) → (𝑏 ≠ 𝑑 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
39	38	ad2ant2l 743	. . . . . . 7 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → (𝑏 ≠ 𝑑 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
40	34, 39	jaod 856	. . . . . 6 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → ((𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
41	29, 40	syl5 34	. . . . 5 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
42	41	rexlimdvva 3233	. . . 4 ⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
43	42	rexlimivv 3231	. . 3 ⊢ (∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦)
44	1, 17, 43	mp2b 10	. 2 ⊢ ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦
45		eqtr3 2761	. . . . . . . . 9 ⊢ ((𝑥 = 0 ∧ 𝑦 = 0) → 𝑥 = 𝑦)
46	45	ex 413	. . . . . . . 8 ⊢ (𝑥 = 0 → (𝑦 = 0 → 𝑥 = 𝑦))
47	46	necon3d 2961	. . . . . . 7 ⊢ (𝑥 = 0 → (𝑥 ≠ 𝑦 → 𝑦 ≠ 0))
48		neeq1 3003	. . . . . . . . 9 ⊢ (𝑧 = 𝑦 → (𝑧 ≠ 0 ↔ 𝑦 ≠ 0))
49	48	rspcev 3560	. . . . . . . 8 ⊢ ((𝑦 ∈ ℝ ∧ 𝑦 ≠ 0) → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)
50	49	expcom 414	. . . . . . 7 ⊢ (𝑦 ≠ 0 → (𝑦 ∈ ℝ → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
51	47, 50	syl6 35	. . . . . 6 ⊢ (𝑥 = 0 → (𝑥 ≠ 𝑦 → (𝑦 ∈ ℝ → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
52	51	com23 86	. . . . 5 ⊢ (𝑥 = 0 → (𝑦 ∈ ℝ → (𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
53	52	adantld 491	. . . 4 ⊢ (𝑥 = 0 → ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
54		neeq1 3003	. . . . . . . 8 ⊢ (𝑧 = 𝑥 → (𝑧 ≠ 0 ↔ 𝑥 ≠ 0))
55	54	rspcev 3560	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)
56	55	expcom 414	. . . . . 6 ⊢ (𝑥 ≠ 0 → (𝑥 ∈ ℝ → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
57	56	adantrd 492	. . . . 5 ⊢ (𝑥 ≠ 0 → ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
58	57	a1dd 50	. . . 4 ⊢ (𝑥 ≠ 0 → ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
59	53, 58	pm2.61ine 3025	. . 3 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
60	59	rexlimivv 3231	. 2 ⊢ (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)
61		ax-rrecex 10950	. . . 4 ⊢ ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → ∃𝑥 ∈ ℝ (𝑧 · 𝑥) = 1)
62		remulcl 10963	. . . . . . 7 ⊢ ((𝑧 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (𝑧 · 𝑥) ∈ ℝ)
63	62	adantlr 712	. . . . . 6 ⊢ (((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) ∧ 𝑥 ∈ ℝ) → (𝑧 · 𝑥) ∈ ℝ)
64		eleq1 2823	. . . . . 6 ⊢ ((𝑧 · 𝑥) = 1 → ((𝑧 · 𝑥) ∈ ℝ ↔ 1 ∈ ℝ))
65	63, 64	syl5ibcom 244	. . . . 5 ⊢ (((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) ∧ 𝑥 ∈ ℝ) → ((𝑧 · 𝑥) = 1 → 1 ∈ ℝ))
66	65	rexlimdva 3223	. . . 4 ⊢ ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → (∃𝑥 ∈ ℝ (𝑧 · 𝑥) = 1 → 1 ∈ ℝ))
67	61, 66	mpd 15	. . 3 ⊢ ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → 1 ∈ ℝ)
68	67	rexlimiva 3220	. 2 ⊢ (∃𝑧 ∈ ℝ 𝑧 ≠ 0 → 1 ∈ ℝ)
69	44, 60, 68	mp2b 10	1 ⊢ 1 ∈ ℝ

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 396   ∨ wo 844   = wceq 1538   ∈ wcel 2103   ≠ wne 2940  ∃wrex 3070  (class class class)co 7282  ℂcc 10876  ℝcr 10877  0cc0 10878  1c1 10879  ici 10880   + caddc 10881   · cmul 10883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1910  ax-6 1968  ax-7 2008  ax-8 2105  ax-9 2113  ax-ext 2706  ax-1cn 10936  ax-icn 10937  ax-addcl 10938  ax-mulcl 10940  ax-mulrcl 10941  ax-i2m1 10946  ax-1ne0 10947  ax-rrecex 10950  ax-cnre 10951

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1541  df-fal 1551  df-ex 1779  df-sb 2065  df-clab 2713  df-cleq 2727  df-clel 2813  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3139  df-v 3433  df-dif 3889  df-un 3891  df-in 3893  df-ss 3903  df-nul 4256  df-if 4459  df-sn 4561  df-pr 4563  df-op 4567  df-uni 4839  df-br 5074  df-iota 6393  df-fv 6443  df-ov 7285

This theorem is referenced by:  1red  10983  1xr  11041  dedekind  11145  peano2re  11155  mul02lem2  11159  addid1  11162  renegcl  11291  peano2rem  11295  0reALT  11325  0lt1  11504  0le1  11505  relin01  11506  1le1  11610  eqneg  11702  ltp1  11822  ltm1  11824  recgt0  11828  mulgt1  11841  ltmulgt11  11842  lemulge11  11844  reclt1  11877  recgt1  11878  recgt1i  11879  recp1lt1  11880  recreclt  11881  recgt0ii  11888  ledivp1i  11907  ltdivp1i  11908  inelr  11970  cju  11976  nnssre  11984  nnge1  12008  nngt1ne1  12009  nnle1eq1  12010  nngt0  12011  nnnlt1  12012  nnne0  12014  nnrecre  12022  nnrecgt0  12023  nnsub  12024  2re  12054  3re  12060  4re  12064  5re  12067  6re  12070  7re  12073  8re  12076  9re  12079  0le2  12082  2pos  12083  3pos  12085  4pos  12087  5pos  12089  6pos  12090  7pos  12091  8pos  12092  9pos  12093  neg1rr  12095  neg1lt0  12097  1lt2  12151  1lt3  12153  1lt4  12156  1lt5  12160  1lt6  12165  1lt7  12171  1lt8  12178  1lt9  12186  1ne2  12188  1le2  12189  1le3  12192  halflt1  12198  addltmul  12216  nnunb  12236  elnnnn0c  12285  nn0ge2m1nn  12309  elnnz1  12353  znnnlt1  12354  zltp1le  12377  zleltp1  12378  nn0lt2  12390  recnz  12402  gtndiv  12404  3halfnz  12406  10re  12463  1lt10  12583  eluzp1m1  12615  eluzp1p1  12617  eluz2b2  12668  zbtwnre  12693  rebtwnz  12694  1rp  12741  divlt1lt  12806  divle1le  12807  nnledivrp  12849  qbtwnxr  12941  xmulid1  13020  xmulm1  13022  x2times  13040  xrub  13053  elicc01  13205  1elunit  13209  divelunit  13233  lincmb01cmp  13234  unitssre  13238  0nelfz1  13282  fzpreddisj  13312  fznatpl1  13317  fztpval  13325  fraclt1  13529  fracle1  13530  flbi2  13544  fldiv4p1lem1div2  13562  fldiv4lem1div2  13564  fldiv  13587  modid  13623  1mod  13630  m1modnnsub1  13644  modm1p1mod0  13649  seqf1olem1  13769  reexpcl  13806  reexpclz  13809  expge0  13826  expge1  13827  expgt1  13828  bernneq  13951  bernneq2  13952  expnbnd  13954  expnlbnd  13955  expnlbnd2  13956  expmulnbnd  13957  discr1  13961  facwordi  14010  faclbnd3  14013  faclbnd4lem1  14014  faclbnd4lem4  14017  faclbnd6  14020  facavg  14022  hashv01gt1  14066  hashnn0n0nn  14113  hashunsnggt  14116  hash1snb  14141  hashgt12el  14144  hashgt12el2  14145  hashfun  14159  hashge2el2dif  14201  lsw0  14275  f1oun2prg  14637  cjexp  14868  re1  14872  im1  14873  rei  14874  imi  14875  sqrlem1  14961  sqrlem2  14962  sqrlem3  14963  sqrlem4  14964  sqrlem7  14967  resqrex  14969  sqrt1  14990  sqrt2gt1lt2  14993  sqrtm1  14994  abs1  15016  absrdbnd  15060  caubnd2  15076  mulcn2  15312  reccn2  15313  rlimno1  15372  o1fsum  15532  expcnv  15583  geolim  15589  geolim2  15590  georeclim  15591  geomulcvg  15595  geoisumr  15597  geoisum1c  15599  fprodge0  15710  fprodge1  15712  rerisefaccl  15734  refallfaccl  15735  ere  15805  ege2le3  15806  efgt1  15832  resin4p  15854  recos4p  15855  tanhbnd  15877  sinbnd  15896  cosbnd  15897  sinbnd2  15898  cosbnd2  15899  ef01bndlem  15900  sin01bnd  15901  cos01bnd  15902  cos1bnd  15903  cos2bnd  15904  sinltx  15905  sin01gt0  15906  cos01gt0  15907  sin02gt0  15908  sincos1sgn  15909  ene1  15926  rpnnen2lem2  15931  rpnnen2lem3  15932  rpnnen2lem4  15933  rpnnen2lem9  15938  rpnnen2lem12  15941  ruclem6  15951  ruclem11  15956  ruclem12  15957  3dvds  16047  flodddiv4  16129  sadcadd  16172  isprm3  16395  sqnprm  16414  coprm  16423  phibndlem  16478  pythagtriplem3  16526  pcmpt  16600  fldivp1  16605  pockthi  16615  infpn2  16621  resslemOLD  16959  basendxnmulrndx  17012  basendxnmulrndxOLD  17013  starvndxnbasendx  17021  scandxnbasendx  17033  vscandxnbasendx  17038  ipndxnbasendx  17049  basendxnocndx  17100  slotsbhcdif  17132  slotsbhcdifOLD  17133  oppcbasOLD  17436  rescbasOLD  17549  rescabsOLD  17555  odubasOLD  18017  symgvalstructOLD  19012  lt6abl  19503  srgbinomlem4  19786  abvneg  20101  abvtrivd  20107  rmodislmodOLD  20199  0ringnnzr  20547  cnfldfunALTOLD  20618  xrsmcmn  20628  xrsnsgrp  20641  gzrngunitlem  20670  gzrngunit  20671  rge0srg  20676  psgnodpmr  20802  remulg  20819  resubdrg  20820  thlbasOLD  20909  tuslemOLD  23426  setsmsbasOLD  23636  dscmet  23735  dscopn  23736  nrginvrcnlem  23862  idnghm  23914  tgioo  23966  blcvx  23968  iicmp  24056  iiconn  24057  iirev  24099  iihalf1  24101  iihalf2  24103  iihalf2cn  24104  elii1  24105  elii2  24106  iimulcl  24107  icopnfcnv  24112  icopnfhmeo  24113  iccpnfhmeo  24115  xrhmeo  24116  xrhmph  24117  evth  24129  xlebnum  24135  htpycc  24150  reparphti  24167  pcoval1  24183  pco1  24185  pcoval2  24186  pcocn  24187  pcohtpylem  24189  pcopt  24192  pcopt2  24193  pcoass  24194  pcorevlem  24196  nmhmcn  24290  ncvs1  24328  ovolunlem1a  24667  vitalilem2  24780  vitalilem4  24782  vitalilem5  24783  vitali  24784  i1f1  24861  itg11  24862  itg2const  24912  dveflem  25150  dvlipcn  25165  dvcvx  25191  ply1remlem  25334  fta1blem  25340  vieta1lem2  25478  aalioulem3  25501  aalioulem5  25503  aaliou3lem2  25510  ulmbdd  25564  iblulm  25573  radcnvlem1  25579  dvradcnv  25587  abelthlem2  25598  abelthlem3  25599  abelthlem5  25601  abelthlem7  25604  abelth  25607  abelth2  25608  reeff1olem  25612  reeff1o  25613  sinhalfpilem  25627  tangtx  25669  sincos4thpi  25677  pige3ALT  25683  coskpi  25686  cos0pilt1  25695  recosf1o  25698  tanregt0  25702  efif1olem3  25707  efif1olem4  25708  loge  25749  logdivlti  25782  logcnlem4  25807  logf1o2  25812  logtayl  25822  logccv  25825  recxpcl  25837  cxplea  25858  cxpcn3lem  25907  cxpaddlelem  25911  loglesqrt  25918  ang180lem2  25967  angpined  25987  acosrecl  26060  atancj  26067  atanlogaddlem  26070  atantan  26080  atans2  26088  ressatans  26091  leibpi  26099  log2le1  26107  birthdaylem3  26110  cxp2lim  26133  cxploglim  26134  cxploglim2  26135  divsqrtsumlem  26136  cvxcl  26141  scvxcvx  26142  jensenlem2  26144  amgmlem  26146  emcllem2  26153  emcllem4  26155  emcllem6  26157  emcllem7  26158  emre  26162  emgt0  26163  harmonicbnd3  26164  harmonicubnd  26166  harmonicbnd4  26167  zetacvg  26171  ftalem1  26229  ftalem2  26230  ftalem5  26233  issqf  26292  cht1  26321  chp1  26323  ppiltx  26333  mumullem2  26336  ppiublem1  26357  ppiub  26359  chtublem  26366  chtub  26367  logfacbnd3  26378  logexprlim  26380  perfectlem2  26385  dchrinv  26416  dchr1re  26418  efexple  26436  bposlem1  26439  bposlem2  26440  bposlem5  26443  bposlem8  26446  lgsdir2lem1  26480  lgsdir2lem5  26484  lgsdir  26487  lgsne0  26490  lgsabs1  26491  lgsdinn0  26500  gausslemma2dlem0i  26519  lgseisen  26534  m1lgs  26543  2lgslem3  26559  addsq2nreurex  26599  2sqreultblem  26603  2sqreunnltblem  26606  chebbnd1lem3  26626  chebbnd1  26627  chtppilimlem1  26628  chtppilimlem2  26629  chtppilim  26630  chpchtlim  26634  vmadivsumb  26638  rplogsumlem2  26640  rpvmasumlem  26642  dchrmusumlema  26648  dchrmusum2  26649  dchrvmasumlem2  26653  dchrvmasumiflem1  26656  dchrisum0flblem1  26663  dchrisum0flblem2  26664  dchrisum0fno1  26666  rpvmasum2  26667  dchrisum0re  26668  dchrisum0lema  26669  dchrisum0lem1b  26670  dchrisum0lem1  26671  dchrisum0lem2a  26672  dchrisum0lem2  26673  logdivsum  26688  mulog2sumlem2  26690  2vmadivsumlem  26695  log2sumbnd  26699  selbergb  26704  selberg2b  26707  chpdifbndlem1  26708  selberg3lem1  26712  selberg3lem2  26713  selberg4lem1  26715  pntrmax  26719  pntrsumo1  26720  selbergsb  26730  pntrlog2bndlem3  26734  pntrlog2bndlem5  26736  pntpbnd1a  26740  pntpbnd2  26742  pntibndlem1  26744  pntibndlem3  26747  pntlemd  26749  pntlemc  26750  pntlemb  26752  pntlemr  26757  pntlemf  26760  pntlemk  26761  pntlemo  26762  pntlem3  26764  pntleml  26766  abvcxp  26770  ostth2lem1  26773  ostth1  26788  ostth2lem2  26789  ostth2lem3  26790  ostth2lem4  26791  ostth2  26792  ostth3  26793  ostth  26794  slotsinbpsd  26809  slotslnbpsd  26810  trgcgrg  26883  brbtwn2  27280  colinearalglem4  27284  ax5seglem2  27304  ax5seglem3  27306  axpaschlem  27315  axpasch  27316  axlowdimlem6  27322  axlowdimlem10  27326  axlowdimlem16  27332  axlowdim1  27334  axlowdim2  27335  axlowdim  27336  axcontlem2  27340  elntg2  27360  lfgrnloop  27502  lfuhgr1v0e  27628  usgrexmpldifpr  27632  usgrexmplef  27633  1loopgrvd2  27877  vdegp1bi  27911  lfgrwlkprop  28062  pthdlem1  28141  pthdlem2  28143  clwlkclwwlkf  28379  upgr4cycl4dv4e  28556  konigsberglem2  28624  konigsberglem3  28625  konigsberglem5  28627  frgrreg  28765  ex-dif  28794  ex-in  28796  ex-pss  28799  ex-res  28812  ex-fl  28818  nv1  29044  smcnlem  29066  ipidsq  29079  nmlno0lem  29162  norm-ii-i  29506  bcs2  29551  norm1  29618  nmopub2tALT  30278  nmfnleub2  30295  nmlnop0iALT  30364  unopbd  30384  nmopadjlem  30458  nmopcoadji  30470  pjnmopi  30517  pjbdlni  30518  hstle1  30595  hstle  30599  hstles  30600  stge1i  30607  stlesi  30610  staddi  30615  stadd3i  30617  strlem1  30619  strlem5  30624  jplem1  30637  cdj1i  30802  addltmulALT  30815  xlt2addrd  31088  pr01ssre  31145  dp2lt10  31165  dp2ltsuc  31167  dp2ltc  31168  dplti  31186  dpmul4  31195  cshw1s2  31239  xrsmulgzz  31294  resvbasOLD  31540  rearchi  31553  xrge0slmod  31555  prmidl0  31633  submateqlem1  31764  xrge0iifcnv  31890  xrge0iifcv  31891  xrge0iifiso  31892  xrge0iifhom  31894  zrhre  31976  indf  31990  indfval  31991  esumcst  32038  cntnevol  32203  omssubadd  32274  iwrdsplit  32361  dstfrvclim1  32451  coinfliprv  32456  ballotlem2  32462  ballotlem4  32472  ballotlemi1  32476  ballotlemic  32480  sgnclre  32513  sgnnbi  32519  sgnpbi  32520  sgnmulsgp  32524  plymulx0  32533  plymulx  32534  signswch  32547  signstf  32552  signsvfn  32568  itgexpif  32593  hgt750lemd  32635  logdivsqrle  32637  hgt750lem  32638  hgt750lem2  32639  hgt750leme  32645  tgoldbachgnn  32646  subfacp1lem1  33148  subfacp1lem5  33153  resconn  33215  iisconn  33221  iillysconn  33222  problem2  33631  problem3  33632  sinccvglem  33637  fz0n  33703  dnibndlem12  34676  knoppcnlem4  34683  knoppndvlem13  34711  cnndvlem1  34724  irrdiff  35504  relowlpssretop  35542  sin2h  35774  cos2h  35775  tan2h  35776  poimirlem7  35791  poimirlem16  35800  poimirlem17  35801  poimirlem19  35803  poimirlem20  35804  poimirlem22  35806  poimirlem23  35807  poimirlem29  35813  poimirlem31  35815  itg2addnclem3  35837  asindmre  35867  dvasin  35868  dvacos  35869  dvreasin  35870  dvreacos  35871  fdc  35910  geomcau  35924  cntotbnd  35961  heiborlem8  35983  bfplem2  35988  bfp  35989  aks4d1p1p7  40087  2xp3dxp2ge1d  40167  factwoffsmonot  40168  1t1e1ALT  40297  re1m1e0m0  40385  sn-00idlem1  40386  sn-00idlem2  40387  remul02  40393  sn-0ne2  40394  reixi  40409  rei4  40410  remulid2  40420  ipiiie0  40424  sn-0tie0  40426  mulgt0b2d  40435  sn-0lt1  40437  sn-ltp1  40438  reneg1lt0  40439  sn-inelr  40440  rabren3dioph  40642  pellexlem5  40660  pellexlem6  40661  pell1qrgaplem  40700  pell14qrgap  40702  pellqrex  40706  pellfundre  40708  pellfundlb  40711  pellfund14gap  40714  jm2.17a  40787  acongeq  40810  jm2.23  40823  jm3.1lem2  40845  sqrtcval  41254  sqrtcval2  41255  resqrtval  41256  imsqrtval  41257  relexp01min  41326  mnringbasedOLD  41835  cvgdvgrat  41936  lhe4.4ex1a  41952  binomcxplemnotnn0  41979  isosctrlem1ALT  42559  supxrgelem  42891  xrlexaddrp  42906  infxr  42921  infleinflem2  42925  sumnnodd  43187  limsup10exlem  43329  limsup10ex  43330  dvnprodlem3  43505  stoweidlem1  43558  stoweidlem18  43575  stoweidlem19  43576  stoweidlem26  43583  stoweidlem34  43591  stoweidlem40  43597  stoweidlem41  43598  stoweidlem59  43616  stoweid  43620  stirlinglem10  43640  stirlinglem11  43641  dirkercncflem1  43660  fourierdlem16  43680  fourierdlem21  43685  fourierdlem22  43686  fourierdlem42  43706  fourierdlem68  43731  fourierdlem83  43746  fourierdlem103  43766  sqwvfourb  43786  fouriersw  43788  etransclem23  43814  salgencntex  43898  ovn0lem  44120  smfmullem3  44348  smfmullem4  44349  zm1nn  44815  m1mod0mod1  44842  fmtnosqrt  45012  perfectALTVlem2  45195  2exp340mod341  45206  8exp8mod9  45209  nfermltl8rev  45215  nnsum3primesprm  45263  nnsum4primesodd  45269  nnsum4primesoddALTV  45270  nnsum4primeseven  45273  nnsum4primesevenALTV  45274  tgblthelfgott  45288  tgoldbach  45290  rege1logbrege0  45925  rege1logbzge0  45926  blennnelnn  45943  dignnld  45970  nn0sumshdiglemA  45986  nn0sumshdiglem1  45988  rrx2xpref1o  46085  rrxlines  46100  eenglngeehlnmlem1  46104  eenglngeehlnmlem2  46105  line2ylem  46118  line2x  46121  icccldii  46233  io1ii  46235  sepfsepc  46242