Theorem 1re 11233

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 11185, 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 11196	. . 3 ⊢ 1 ≠ 0
2		ax-1cn 11185	. . . . 5 ⊢ 1 ∈ ℂ
3		cnre 11230	. . . . 5 ⊢ (1 ∈ ℂ → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)))
4	2, 3	ax-mp 5	. . . 4 ⊢ ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏))
5		neeq1 2994	. . . . . . . 8 ⊢ (1 = (𝑎 + (i · 𝑏)) → (1 ≠ 0 ↔ (𝑎 + (i · 𝑏)) ≠ 0))
6	5	biimpcd 249	. . . . . . 7 ⊢ (1 ≠ 0 → (1 = (𝑎 + (i · 𝑏)) → (𝑎 + (i · 𝑏)) ≠ 0))
7		0cn 11225	. . . . . . . 8 ⊢ 0 ∈ ℂ
8		cnre 11230	. . . . . . . 8 ⊢ (0 ∈ ℂ → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)))
9	7, 8	ax-mp 5	. . . . . . 7 ⊢ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑))
10		neeq2 2995	. . . . . . . . . 10 ⊢ (0 = (𝑐 + (i · 𝑑)) → ((𝑎 + (i · 𝑏)) ≠ 0 ↔ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
11	10	biimpcd 249	. . . . . . . . 9 ⊢ ((𝑎 + (i · 𝑏)) ≠ 0 → (0 = (𝑐 + (i · 𝑑)) → (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
12	11	reximdv 3155	. . . . . . . 8 ⊢ ((𝑎 + (i · 𝑏)) ≠ 0 → (∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)) → ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
13	12	reximdv 3155	. . . . . . 7 ⊢ ((𝑎 + (i · 𝑏)) ≠ 0 → (∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)) → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
14	6, 9, 13	syl6mpi 67	. . . . . 6 ⊢ (1 ≠ 0 → (1 = (𝑎 + (i · 𝑏)) → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
15	14	reximdv 3155	. . . . 5 ⊢ (1 ≠ 0 → (∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)) → ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
16	15	reximdv 3155	. . . 4 ⊢ (1 ≠ 0 → (∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)) → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
17	4, 16	mpi 20	. . 3 ⊢ (1 ≠ 0 → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)))
18		ioran 985	. . . . . . . . 9 ⊢ (¬ (𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑) ↔ (¬ 𝑎 ≠ 𝑐 ∧ ¬ 𝑏 ≠ 𝑑))
19		df-ne 2933	. . . . . . . . . . 11 ⊢ (𝑎 ≠ 𝑐 ↔ ¬ 𝑎 = 𝑐)
20	19	con2bii 357	. . . . . . . . . 10 ⊢ (𝑎 = 𝑐 ↔ ¬ 𝑎 ≠ 𝑐)
21		df-ne 2933	. . . . . . . . . . 11 ⊢ (𝑏 ≠ 𝑑 ↔ ¬ 𝑏 = 𝑑)
22	21	con2bii 357	. . . . . . . . . 10 ⊢ (𝑏 = 𝑑 ↔ ¬ 𝑏 ≠ 𝑑)
23	20, 22	anbi12i 628	. . . . . . . . 9 ⊢ ((𝑎 = 𝑐 ∧ 𝑏 = 𝑑) ↔ (¬ 𝑎 ≠ 𝑐 ∧ ¬ 𝑏 ≠ 𝑑))
24	18, 23	bitr4i 278	. . . . . . . 8 ⊢ (¬ (𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑) ↔ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑))
25		id 22	. . . . . . . . 9 ⊢ (𝑎 = 𝑐 → 𝑎 = 𝑐)
26		oveq2 7411	. . . . . . . . 9 ⊢ (𝑏 = 𝑑 → (i · 𝑏) = (i · 𝑑))
27	25, 26	oveqan12d 7422	. . . . . . . 8 ⊢ ((𝑎 = 𝑐 ∧ 𝑏 = 𝑑) → (𝑎 + (i · 𝑏)) = (𝑐 + (i · 𝑑)))
28	24, 27	sylbi 217	. . . . . . 7 ⊢ (¬ (𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑) → (𝑎 + (i · 𝑏)) = (𝑐 + (i · 𝑑)))
29	28	necon1ai 2959	. . . . . 6 ⊢ ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → (𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑))
30		neeq1 2994	. . . . . . . . . 10 ⊢ (𝑥 = 𝑎 → (𝑥 ≠ 𝑦 ↔ 𝑎 ≠ 𝑦))
31		neeq2 2995	. . . . . . . . . 10 ⊢ (𝑦 = 𝑐 → (𝑎 ≠ 𝑦 ↔ 𝑎 ≠ 𝑐))
32	30, 31	rspc2ev 3614	. . . . . . . . 9 ⊢ ((𝑎 ∈ ℝ ∧ 𝑐 ∈ ℝ ∧ 𝑎 ≠ 𝑐) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦)
33	32	3expia 1121	. . . . . . . 8 ⊢ ((𝑎 ∈ ℝ ∧ 𝑐 ∈ ℝ) → (𝑎 ≠ 𝑐 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
34	33	ad2ant2r 747	. . . . . . 7 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → (𝑎 ≠ 𝑐 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
35		neeq1 2994	. . . . . . . . . 10 ⊢ (𝑥 = 𝑏 → (𝑥 ≠ 𝑦 ↔ 𝑏 ≠ 𝑦))
36		neeq2 2995	. . . . . . . . . 10 ⊢ (𝑦 = 𝑑 → (𝑏 ≠ 𝑦 ↔ 𝑏 ≠ 𝑑))
37	35, 36	rspc2ev 3614	. . . . . . . . 9 ⊢ ((𝑏 ∈ ℝ ∧ 𝑑 ∈ ℝ ∧ 𝑏 ≠ 𝑑) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦)
38	37	3expia 1121	. . . . . . . 8 ⊢ ((𝑏 ∈ ℝ ∧ 𝑑 ∈ ℝ) → (𝑏 ≠ 𝑑 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
39	38	ad2ant2l 746	. . . . . . 7 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → (𝑏 ≠ 𝑑 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
40	34, 39	jaod 859	. . . . . 6 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → ((𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
41	29, 40	syl5 34	. . . . 5 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
42	41	rexlimdvva 3198	. . . 4 ⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
43	42	rexlimivv 3186	. . 3 ⊢ (∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦)
44	1, 17, 43	mp2b 10	. 2 ⊢ ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦
45		eqtr3 2757	. . . . . . . . 9 ⊢ ((𝑥 = 0 ∧ 𝑦 = 0) → 𝑥 = 𝑦)
46	45	ex 412	. . . . . . . 8 ⊢ (𝑥 = 0 → (𝑦 = 0 → 𝑥 = 𝑦))
47	46	necon3d 2953	. . . . . . 7 ⊢ (𝑥 = 0 → (𝑥 ≠ 𝑦 → 𝑦 ≠ 0))
48		neeq1 2994	. . . . . . . . 9 ⊢ (𝑧 = 𝑦 → (𝑧 ≠ 0 ↔ 𝑦 ≠ 0))
49	48	rspcev 3601	. . . . . . . 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 2994	. . . . . . . 8 ⊢ (𝑧 = 𝑥 → (𝑧 ≠ 0 ↔ 𝑥 ≠ 0))
55	54	rspcev 3601	. . . . . . 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 3015	. . 3 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
60	59	rexlimivv 3186	. 2 ⊢ (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)
61		ax-rrecex 11199	. . . 4 ⊢ ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → ∃𝑥 ∈ ℝ (𝑧 · 𝑥) = 1)
62		remulcl 11212	. . . . . . 7 ⊢ ((𝑧 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (𝑧 · 𝑥) ∈ ℝ)
63	62	adantlr 715	. . . . . 6 ⊢ (((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) ∧ 𝑥 ∈ ℝ) → (𝑧 · 𝑥) ∈ ℝ)
64		eleq1 2822	. . . . . 6 ⊢ ((𝑧 · 𝑥) = 1 → ((𝑧 · 𝑥) ∈ ℝ ↔ 1 ∈ ℝ))
65	63, 64	syl5ibcom 245	. . . . 5 ⊢ (((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) ∧ 𝑥 ∈ ℝ) → ((𝑧 · 𝑥) = 1 → 1 ∈ ℝ))
66	65	rexlimdva 3141	. . . 4 ⊢ ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → (∃𝑥 ∈ ℝ (𝑧 · 𝑥) = 1 → 1 ∈ ℝ))
67	61, 66	mpd 15	. . 3 ⊢ ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → 1 ∈ ℝ)
68	67	rexlimiva 3133	. 2 ⊢ (∃𝑧 ∈ ℝ 𝑧 ≠ 0 → 1 ∈ ℝ)
69	44, 60, 68	mp2b 10	1 ⊢ 1 ∈ ℝ

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∨ wo 847   = wceq 1540   ∈ wcel 2108   ≠ wne 2932  ∃wrex 3060  (class class class)co 7403  ℂcc 11125  ℝcr 11126  0cc0 11127  1c1 11128  ici 11129   + caddc 11130   · cmul 11132

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-1cn 11185  ax-icn 11186  ax-addcl 11187  ax-mulcl 11189  ax-mulrcl 11190  ax-i2m1 11195  ax-1ne0 11196  ax-rrecex 11199  ax-cnre 11200

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 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-iota 6483  df-fv 6538  df-ov 7406

This theorem is referenced by:  1red  11234  1xr  11292  dedekind  11396  peano2re  11406  mul02lem2  11410  addrid  11413  renegcl  11544  peano2rem  11548  0reALT  11578  0lt1  11757  0le1  11758  relin01  11759  1le1  11863  eqneg  11959  ltp1  12079  ltm1  12081  recgt0  12085  mulgt1OLD  12098  ltmulgt11  12099  lemulge11  12102  reclt1  12135  recgt1  12136  recgt1i  12137  recp1lt1  12138  recreclt  12139  recgt0ii  12146  ledivp1i  12165  ltdivp1i  12166  inelr  12228  cju  12234  nnssre  12242  nnge1  12266  nngt1ne1  12267  nnle1eq1  12268  nngt0  12269  nnnlt1  12270  nnne0  12272  nnrecre  12280  nnrecgt0  12281  nnsub  12282  2re  12312  3re  12318  4re  12322  5re  12325  6re  12328  7re  12331  8re  12334  9re  12337  0le2  12340  2pos  12341  3pos  12343  4pos  12345  5pos  12347  6pos  12348  7pos  12349  8pos  12350  9pos  12351  neg1rr  12353  neg1lt0  12355  1lt2  12409  1lt3  12411  1lt4  12414  1lt5  12418  1lt6  12423  1lt7  12429  1lt8  12436  1lt9  12444  1ne2  12446  1le2  12447  1le3  12450  halflt1  12456  addltmul  12475  nnunb  12495  elnnnn0c  12544  nn0ge2m1nn  12569  elnnz1  12616  znnnlt1  12617  zltp1le  12640  zleltp1  12641  nn0lt2  12654  recnz  12666  gtndiv  12668  3halfnz  12670  10re  12725  1lt10  12845  eluzp1m1  12876  eluzp1p1  12878  eluz2b2  12935  zbtwnre  12960  rebtwnz  12961  1rp  13010  divlt1lt  13076  divle1le  13077  nnledivrp  13119  qbtwnxr  13214  xmulrid  13293  xmulm1  13295  x2times  13313  xrub  13326  elicc01  13481  1elunit  13485  divelunit  13509  lincmb01cmp  13510  unitssre  13514  0nelfz1  13558  fzpreddisj  13588  fznatpl1  13593  fztpval  13601  fraclt1  13817  fracle1  13818  flbi2  13832  fldiv4p1lem1div2  13850  fldiv4lem1div2  13852  fldiv  13875  modid  13911  1mod  13918  m1modnnsub1  13933  modm1p1mod0  13938  seqf1olem1  14057  reexpcl  14094  reexpclz  14098  expge0  14114  expge1  14115  expgt1  14116  bernneq  14245  bernneq2  14246  expnbnd  14248  expnlbnd  14249  expnlbnd2  14250  expmulnbnd  14251  discr1  14255  facwordi  14305  faclbnd3  14308  faclbnd4lem1  14309  faclbnd4lem4  14312  faclbnd6  14315  facavg  14317  hashv01gt1  14361  hashnn0n0nn  14407  hashunsnggt  14410  hash1snb  14435  hashgt12el  14438  hashgt12el2  14439  hashfun  14453  hashge2el2dif  14496  tpf1ofv2  14514  lsw0  14581  f1oun2prg  14934  cjexp  15167  re1  15171  im1  15172  rei  15173  imi  15174  01sqrexlem1  15259  01sqrexlem2  15260  01sqrexlem3  15261  01sqrexlem4  15262  01sqrexlem7  15265  resqrex  15267  sqrt1  15288  sqrt2gt1lt2  15291  sqrtm1  15292  abs1  15314  absrdbnd  15358  caubnd2  15374  mulcn2  15610  reccn2  15611  rlimno1  15668  o1fsum  15827  expcnv  15878  geolim  15884  geolim2  15885  georeclim  15886  geomulcvg  15890  geoisumr  15892  geoisum1c  15894  fprodge0  16007  fprodge1  16009  rerisefaccl  16031  refallfaccl  16032  ere  16103  ege2le3  16104  efgt1  16132  resin4p  16154  recos4p  16155  tanhbnd  16177  sinbnd  16196  cosbnd  16197  sinbnd2  16198  cosbnd2  16199  ef01bndlem  16200  sin01bnd  16201  cos01bnd  16202  cos1bnd  16203  cos2bnd  16204  sinltx  16205  sin01gt0  16206  cos01gt0  16207  sin02gt0  16208  sincos1sgn  16209  ene1  16226  rpnnen2lem2  16231  rpnnen2lem3  16232  rpnnen2lem4  16233  rpnnen2lem9  16238  rpnnen2lem12  16241  ruclem6  16251  ruclem11  16256  ruclem12  16257  3dvds  16348  flodddiv4  16432  sadcadd  16475  isprm3  16700  sqnprm  16719  coprm  16728  phibndlem  16787  pythagtriplem3  16836  pcmpt  16910  fldivp1  16915  pockthi  16925  infpn2  16931  basendxnmulrndx  17308  starvndxnbasendx  17316  scandxnbasendx  17328  vscandxnbasendx  17333  ipndxnbasendx  17344  basendxnocndx  17395  slotsbhcdif  17427  lt6abl  19874  srgbinomlem4  20187  0ringnnzr  20483  abvneg  20784  abvtrivd  20790  xrsmcmn  21352  xrsnsgrp  21368  gzrngunitlem  21398  gzrngunit  21399  rge0srg  21404  psgnodpmr  21548  remulg  21565  resubdrg  21566  psdmvr  22105  dscmet  24509  dscopn  24510  nrginvrcnlem  24628  idnghm  24680  tgioo  24733  blcvx  24735  iicmp  24828  iiconn  24829  iirev  24872  iihalf1  24874  iihalf2  24877  iihalf2cnOLD  24879  elii1  24880  elii2  24881  iimulcl  24882  icopnfcnv  24889  icopnfhmeo  24890  iccpnfhmeo  24892  xrhmeo  24893  xrhmph  24894  evth  24907  xlebnum  24913  htpycc  24928  reparphti  24945  reparphtiOLD  24946  pcoval1  24962  pco1  24964  pcoval2  24965  pcocn  24966  pcohtpylem  24968  pcopt  24971  pcopt2  24972  pcoass  24973  pcorevlem  24975  nmhmcn  25069  ncvs1  25107  ovolunlem1a  25447  vitalilem2  25560  vitalilem4  25562  vitalilem5  25563  vitali  25564  i1f1  25641  itg11  25642  itg2const  25691  dveflem  25933  dvlipcn  25949  dvcvx  25975  ply1remlem  26120  fta1blem  26126  vieta1lem2  26269  aalioulem3  26292  aalioulem5  26294  aaliou3lem2  26301  ulmbdd  26357  iblulm  26366  radcnvlem1  26372  dvradcnv  26380  abelthlem2  26392  abelthlem3  26393  abelthlem5  26395  abelthlem7  26398  abelth  26401  abelth2  26402  reeff1olem  26406  reeff1o  26407  sinhalfpilem  26422  tangtx  26464  sincos4thpi  26472  pige3ALT  26479  coskpi  26482  cos0pilt1  26491  recosf1o  26494  tanregt0  26498  efif1olem3  26503  efif1olem4  26504  loge  26545  logdivlti  26579  logcnlem4  26604  logf1o2  26609  logtayl  26619  logccv  26622  recxpcl  26634  cxplea  26655  cxpcn3lem  26707  cxpaddlelem  26711  loglesqrt  26721  ang180lem2  26770  angpined  26790  acosrecl  26863  atancj  26870  atanlogaddlem  26873  atantan  26883  atans2  26891  ressatans  26894  leibpi  26902  log2le1  26910  birthdaylem3  26913  cxp2lim  26937  cxploglim  26938  cxploglim2  26939  divsqrtsumlem  26940  cvxcl  26945  scvxcvx  26946  jensenlem2  26948  amgmlem  26950  emcllem2  26957  emcllem4  26959  emcllem6  26961  emcllem7  26962  emre  26966  emgt0  26967  harmonicbnd3  26968  harmonicubnd  26970  harmonicbnd4  26971  zetacvg  26975  ftalem1  27033  ftalem2  27034  ftalem5  27037  issqf  27096  cht1  27125  chp1  27127  ppiltx  27137  mumullem2  27140  ppiublem1  27163  ppiub  27165  chtublem  27172  chtub  27173  logfacbnd3  27184  logexprlim  27186  perfectlem2  27191  dchrinv  27222  dchr1re  27224  efexple  27242  bposlem1  27245  bposlem2  27246  bposlem5  27249  bposlem8  27252  lgsdir2lem1  27286  lgsdir2lem5  27290  lgsdir  27293  lgsne0  27296  lgsabs1  27297  lgsdinn0  27306  gausslemma2dlem0i  27325  lgseisen  27340  m1lgs  27349  2lgslem3  27365  addsq2nreurex  27405  2sqreultblem  27409  2sqreunnltblem  27412  chebbnd1lem3  27432  chebbnd1  27433  chtppilimlem1  27434  chtppilimlem2  27435  chtppilim  27436  chpchtlim  27440  vmadivsumb  27444  rplogsumlem2  27446  rpvmasumlem  27448  dchrmusumlema  27454  dchrmusum2  27455  dchrvmasumlem2  27459  dchrvmasumiflem1  27462  dchrisum0flblem1  27469  dchrisum0flblem2  27470  dchrisum0fno1  27472  rpvmasum2  27473  dchrisum0re  27474  dchrisum0lema  27475  dchrisum0lem1b  27476  dchrisum0lem1  27477  dchrisum0lem2a  27478  dchrisum0lem2  27479  logdivsum  27494  mulog2sumlem2  27496  2vmadivsumlem  27501  log2sumbnd  27505  selbergb  27510  selberg2b  27513  chpdifbndlem1  27514  selberg3lem1  27518  selberg3lem2  27519  selberg4lem1  27521  pntrmax  27525  pntrsumo1  27526  selbergsb  27536  pntrlog2bndlem3  27540  pntrlog2bndlem5  27542  pntpbnd1a  27546  pntpbnd2  27548  pntibndlem1  27550  pntibndlem3  27553  pntlemd  27555  pntlemc  27556  pntlemb  27558  pntlemr  27563  pntlemf  27566  pntlemk  27567  pntlemo  27568  pntlem3  27570  pntleml  27572  abvcxp  27576  ostth2lem1  27579  ostth1  27594  ostth2lem2  27595  ostth2lem3  27596  ostth2lem4  27597  ostth2  27598  ostth3  27599  ostth  27600  slotsinbpsd  28366  slotslnbpsd  28367  trgcgrg  28440  brbtwn2  28830  colinearalglem4  28834  ax5seglem2  28854  ax5seglem3  28856  axpaschlem  28865  axpasch  28866  axlowdimlem6  28872  axlowdimlem10  28876  axlowdimlem16  28882  axlowdim1  28884  axlowdim2  28885  axlowdim  28886  axcontlem2  28890  elntg2  28910  lfgrnloop  29050  lfuhgr1v0e  29179  usgrexmpldifpr  29183  usgrexmplef  29184  1loopgrvd2  29429  vdegp1bi  29463  lfgrwlkprop  29613  pthdlem1  29694  pthdlem2  29696  clwlkclwwlkf  29935  upgr4cycl4dv4e  30112  konigsberglem2  30180  konigsberglem3  30181  konigsberglem5  30183  frgrreg  30321  ex-dif  30350  ex-in  30352  ex-pss  30355  ex-res  30368  ex-fl  30374  nv1  30602  smcnlem  30624  ipidsq  30637  nmlno0lem  30720  norm-ii-i  31064  bcs2  31109  norm1  31176  nmopub2tALT  31836  nmfnleub2  31853  nmlnop0iALT  31922  unopbd  31942  nmopadjlem  32016  nmopcoadji  32028  pjnmopi  32075  pjbdlni  32076  hstle1  32153  hstle  32157  hstles  32158  stge1i  32165  stlesi  32168  staddi  32173  stadd3i  32175  strlem1  32177  strlem5  32182  jplem1  32195  cdj1i  32360  addltmulALT  32373  xlt2addrd  32682  pr01ssre  32749  sgnclre  32757  sgnnbi  32763  sgnpbi  32764  sgnmulsgp  32768  indf  32778  indfval  32779  dp2lt10  32804  dp2ltsuc  32806  dp2ltc  32807  dplti  32825  dpmul4  32834  cshw1s2  32882  xrsmulgzz  32947  rearchi  33307  xrge0slmod  33309  prmidl0  33411  evl1deg3  33537  constrconj  33725  2sqr3minply  33760  submateqlem1  33784  xrge0iifcnv  33910  xrge0iifcv  33911  xrge0iifiso  33912  xrge0iifhom  33914  zrhre  33996  esumcst  34040  cntnevol  34205  omssubadd  34278  iwrdsplit  34365  dstfrvclim1  34456  coinfliprv  34461  ballotlem2  34467  ballotlem4  34477  ballotlemi1  34481  ballotlemic  34485  plymulx0  34525  plymulx  34526  signswch  34539  signstf  34544  signsvfn  34560  itgexpif  34584  hgt750lemd  34626  logdivsqrle  34628  hgt750lem  34629  hgt750lem2  34630  hgt750leme  34636  tgoldbachgnn  34637  subfacp1lem1  35147  subfacp1lem5  35152  resconn  35214  iisconn  35220  iillysconn  35221  problem2  35634  problem3  35635  sinccvglem  35640  fz0n  35694  dnibndlem12  36453  knoppcnlem4  36460  knoppndvlem13  36488  cnndvlem1  36501  irrdiff  37290  relowlpssretop  37328  sin2h  37580  cos2h  37581  tan2h  37582  poimirlem7  37597  poimirlem16  37606  poimirlem17  37607  poimirlem19  37609  poimirlem20  37610  poimirlem22  37612  poimirlem23  37613  poimirlem29  37619  poimirlem31  37621  itg2addnclem3  37643  asindmre  37673  dvasin  37674  dvacos  37675  dvreasin  37676  dvreacos  37677  fdc  37715  geomcau  37729  cntotbnd  37766  heiborlem8  37788  bfplem2  37793  bfp  37794  aks4d1p1p7  42033  2xp3dxp2ge1d  42200  factwoffsmonot  42201  1t1e1ALT  42253  ine1  42310  re1m1e0m0  42387  sn-00idlem1  42388  sn-00idlem2  42389  remul02  42395  sn-0ne2  42396  reixi  42412  rei4  42413  remullid  42423  ipiiie0  42427  sn-0tie0  42429  sn-nnne0  42438  mulgt0b2d  42450  sn-0lt1  42453  sn-ltp1  42454  reneg1lt0  42456  sn-inelr  42457  rabren3dioph  42785  pellexlem5  42803  pellexlem6  42804  pell1qrgaplem  42843  pell14qrgap  42845  pellqrex  42849  pellfundre  42851  pellfundlb  42854  pellfund14gap  42857  jm2.17a  42931  acongeq  42954  jm2.23  42967  jm3.1lem2  42989  sqrtcval  43612  sqrtcval2  43613  resqrtval  43614  imsqrtval  43615  relexp01min  43684  cvgdvgrat  44285  lhe4.4ex1a  44301  binomcxplemnotnn0  44328  isosctrlem1ALT  44906  supxrgelem  45312  xrlexaddrp  45327  infxr  45342  infleinflem2  45346  sumnnodd  45607  limsup10exlem  45749  limsup10ex  45750  dvnprodlem3  45925  stoweidlem1  45978  stoweidlem18  45995  stoweidlem19  45996  stoweidlem26  46003  stoweidlem34  46011  stoweidlem40  46017  stoweidlem41  46018  stoweidlem59  46036  stoweid  46040  stirlinglem10  46060  stirlinglem11  46061  dirkercncflem1  46080  fourierdlem16  46100  fourierdlem21  46105  fourierdlem22  46106  fourierdlem42  46126  fourierdlem68  46151  fourierdlem83  46166  fourierdlem103  46186  sqwvfourb  46206  fouriersw  46208  etransclem23  46234  salgencntex  46320  ovn0lem  46542  smfmullem3  46770  smfmullem4  46771  zm1nn  47279  ceilhalf1  47311  m1mod0mod1  47331  fmtnosqrt  47501  perfectALTVlem2  47684  2exp340mod341  47695  8exp8mod9  47698  nfermltl8rev  47704  nnsum3primesprm  47752  nnsum4primesodd  47758  nnsum4primesoddALTV  47759  nnsum4primeseven  47762  nnsum4primesevenALTV  47763  tgblthelfgott  47777  tgoldbach  47779  usgrexmpl1lem  47973  usgrexmpl2lem  47978  usgrexmpl2nb1  47984  usgrexmpl2nb3  47986  usgrexmpl2nb4  47987  usgrexmpl2nb5  47988  usgrexmpl2trifr  47989  gpg3kgrtriexlem3  48035  rege1logbrege0  48486  rege1logbzge0  48487  blennnelnn  48504  dignnld  48531  nn0sumshdiglemA  48547  nn0sumshdiglem1  48549  rrx2xpref1o  48646  rrxlines  48661  eenglngeehlnmlem1  48665  eenglngeehlnmlem2  48666  line2ylem  48679  line2x  48682  icccldii  48841  io1ii  48843  sepfsepc  48850