Theorem 1re 11220

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 11172, 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 11183	. . 3 ⊢ 1 ≠ 0
2		ax-1cn 11172	. . . . 5 ⊢ 1 ∈ ℂ
3		cnre 11217	. . . . 5 ⊢ (1 ∈ ℂ → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)))
4	2, 3	ax-mp 5	. . . 4 ⊢ ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏))
5		neeq1 3001	. . . . . . . 8 ⊢ (1 = (𝑎 + (i · 𝑏)) → (1 ≠ 0 ↔ (𝑎 + (i · 𝑏)) ≠ 0))
6	5	biimpcd 248	. . . . . . 7 ⊢ (1 ≠ 0 → (1 = (𝑎 + (i · 𝑏)) → (𝑎 + (i · 𝑏)) ≠ 0))
7		0cn 11212	. . . . . . . 8 ⊢ 0 ∈ ℂ
8		cnre 11217	. . . . . . . 8 ⊢ (0 ∈ ℂ → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)))
9	7, 8	ax-mp 5	. . . . . . 7 ⊢ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑))
10		neeq2 3002	. . . . . . . . . 10 ⊢ (0 = (𝑐 + (i · 𝑑)) → ((𝑎 + (i · 𝑏)) ≠ 0 ↔ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
11	10	biimpcd 248	. . . . . . . . 9 ⊢ ((𝑎 + (i · 𝑏)) ≠ 0 → (0 = (𝑐 + (i · 𝑑)) → (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
12	11	reximdv 3168	. . . . . . . 8 ⊢ ((𝑎 + (i · 𝑏)) ≠ 0 → (∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)) → ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
13	12	reximdv 3168	. . . . . . 7 ⊢ ((𝑎 + (i · 𝑏)) ≠ 0 → (∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)) → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
14	6, 9, 13	syl6mpi 67	. . . . . 6 ⊢ (1 ≠ 0 → (1 = (𝑎 + (i · 𝑏)) → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
15	14	reximdv 3168	. . . . 5 ⊢ (1 ≠ 0 → (∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)) → ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
16	15	reximdv 3168	. . . 4 ⊢ (1 ≠ 0 → (∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)) → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
17	4, 16	mpi 20	. . 3 ⊢ (1 ≠ 0 → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)))
18		ioran 980	. . . . . . . . 9 ⊢ (¬ (𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑) ↔ (¬ 𝑎 ≠ 𝑐 ∧ ¬ 𝑏 ≠ 𝑑))
19		df-ne 2939	. . . . . . . . . . 11 ⊢ (𝑎 ≠ 𝑐 ↔ ¬ 𝑎 = 𝑐)
20	19	con2bii 356	. . . . . . . . . 10 ⊢ (𝑎 = 𝑐 ↔ ¬ 𝑎 ≠ 𝑐)
21		df-ne 2939	. . . . . . . . . . 11 ⊢ (𝑏 ≠ 𝑑 ↔ ¬ 𝑏 = 𝑑)
22	21	con2bii 356	. . . . . . . . . 10 ⊢ (𝑏 = 𝑑 ↔ ¬ 𝑏 ≠ 𝑑)
23	20, 22	anbi12i 625	. . . . . . . . 9 ⊢ ((𝑎 = 𝑐 ∧ 𝑏 = 𝑑) ↔ (¬ 𝑎 ≠ 𝑐 ∧ ¬ 𝑏 ≠ 𝑑))
24	18, 23	bitr4i 277	. . . . . . . 8 ⊢ (¬ (𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑) ↔ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑))
25		id 22	. . . . . . . . 9 ⊢ (𝑎 = 𝑐 → 𝑎 = 𝑐)
26		oveq2 7421	. . . . . . . . 9 ⊢ (𝑏 = 𝑑 → (i · 𝑏) = (i · 𝑑))
27	25, 26	oveqan12d 7432	. . . . . . . 8 ⊢ ((𝑎 = 𝑐 ∧ 𝑏 = 𝑑) → (𝑎 + (i · 𝑏)) = (𝑐 + (i · 𝑑)))
28	24, 27	sylbi 216	. . . . . . 7 ⊢ (¬ (𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑) → (𝑎 + (i · 𝑏)) = (𝑐 + (i · 𝑑)))
29	28	necon1ai 2966	. . . . . 6 ⊢ ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → (𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑))
30		neeq1 3001	. . . . . . . . . 10 ⊢ (𝑥 = 𝑎 → (𝑥 ≠ 𝑦 ↔ 𝑎 ≠ 𝑦))
31		neeq2 3002	. . . . . . . . . 10 ⊢ (𝑦 = 𝑐 → (𝑎 ≠ 𝑦 ↔ 𝑎 ≠ 𝑐))
32	30, 31	rspc2ev 3625	. . . . . . . . 9 ⊢ ((𝑎 ∈ ℝ ∧ 𝑐 ∈ ℝ ∧ 𝑎 ≠ 𝑐) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦)
33	32	3expia 1119	. . . . . . . 8 ⊢ ((𝑎 ∈ ℝ ∧ 𝑐 ∈ ℝ) → (𝑎 ≠ 𝑐 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
34	33	ad2ant2r 743	. . . . . . 7 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → (𝑎 ≠ 𝑐 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
35		neeq1 3001	. . . . . . . . . 10 ⊢ (𝑥 = 𝑏 → (𝑥 ≠ 𝑦 ↔ 𝑏 ≠ 𝑦))
36		neeq2 3002	. . . . . . . . . 10 ⊢ (𝑦 = 𝑑 → (𝑏 ≠ 𝑦 ↔ 𝑏 ≠ 𝑑))
37	35, 36	rspc2ev 3625	. . . . . . . . 9 ⊢ ((𝑏 ∈ ℝ ∧ 𝑑 ∈ ℝ ∧ 𝑏 ≠ 𝑑) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦)
38	37	3expia 1119	. . . . . . . 8 ⊢ ((𝑏 ∈ ℝ ∧ 𝑑 ∈ ℝ) → (𝑏 ≠ 𝑑 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
39	38	ad2ant2l 742	. . . . . . 7 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → (𝑏 ≠ 𝑑 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
40	34, 39	jaod 855	. . . . . 6 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → ((𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
41	29, 40	syl5 34	. . . . 5 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
42	41	rexlimdvva 3209	. . . 4 ⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
43	42	rexlimivv 3197	. . 3 ⊢ (∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦)
44	1, 17, 43	mp2b 10	. 2 ⊢ ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦
45		eqtr3 2756	. . . . . . . . 9 ⊢ ((𝑥 = 0 ∧ 𝑦 = 0) → 𝑥 = 𝑦)
46	45	ex 411	. . . . . . . 8 ⊢ (𝑥 = 0 → (𝑦 = 0 → 𝑥 = 𝑦))
47	46	necon3d 2959	. . . . . . 7 ⊢ (𝑥 = 0 → (𝑥 ≠ 𝑦 → 𝑦 ≠ 0))
48		neeq1 3001	. . . . . . . . 9 ⊢ (𝑧 = 𝑦 → (𝑧 ≠ 0 ↔ 𝑦 ≠ 0))
49	48	rspcev 3613	. . . . . . . 8 ⊢ ((𝑦 ∈ ℝ ∧ 𝑦 ≠ 0) → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)
50	49	expcom 412	. . . . . . 7 ⊢ (𝑦 ≠ 0 → (𝑦 ∈ ℝ → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
51	47, 50	syl6 35	. . . . . 6 ⊢ (𝑥 = 0 → (𝑥 ≠ 𝑦 → (𝑦 ∈ ℝ → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
52	51	com23 86	. . . . 5 ⊢ (𝑥 = 0 → (𝑦 ∈ ℝ → (𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
53	52	adantld 489	. . . 4 ⊢ (𝑥 = 0 → ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
54		neeq1 3001	. . . . . . . 8 ⊢ (𝑧 = 𝑥 → (𝑧 ≠ 0 ↔ 𝑥 ≠ 0))
55	54	rspcev 3613	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)
56	55	expcom 412	. . . . . 6 ⊢ (𝑥 ≠ 0 → (𝑥 ∈ ℝ → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
57	56	adantrd 490	. . . . 5 ⊢ (𝑥 ≠ 0 → ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
58	57	a1dd 50	. . . 4 ⊢ (𝑥 ≠ 0 → ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
59	53, 58	pm2.61ine 3023	. . 3 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
60	59	rexlimivv 3197	. 2 ⊢ (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)
61		ax-rrecex 11186	. . . 4 ⊢ ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → ∃𝑥 ∈ ℝ (𝑧 · 𝑥) = 1)
62		remulcl 11199	. . . . . . 7 ⊢ ((𝑧 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (𝑧 · 𝑥) ∈ ℝ)
63	62	adantlr 711	. . . . . 6 ⊢ (((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) ∧ 𝑥 ∈ ℝ) → (𝑧 · 𝑥) ∈ ℝ)
64		eleq1 2819	. . . . . 6 ⊢ ((𝑧 · 𝑥) = 1 → ((𝑧 · 𝑥) ∈ ℝ ↔ 1 ∈ ℝ))
65	63, 64	syl5ibcom 244	. . . . 5 ⊢ (((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) ∧ 𝑥 ∈ ℝ) → ((𝑧 · 𝑥) = 1 → 1 ∈ ℝ))
66	65	rexlimdva 3153	. . . 4 ⊢ ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → (∃𝑥 ∈ ℝ (𝑧 · 𝑥) = 1 → 1 ∈ ℝ))
67	61, 66	mpd 15	. . 3 ⊢ ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → 1 ∈ ℝ)
68	67	rexlimiva 3145	. 2 ⊢ (∃𝑧 ∈ ℝ 𝑧 ≠ 0 → 1 ∈ ℝ)
69	44, 60, 68	mp2b 10	1 ⊢ 1 ∈ ℝ

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 394   ∨ wo 843   = wceq 1539   ∈ wcel 2104   ≠ wne 2938  ∃wrex 3068  (class class class)co 7413  ℂcc 11112  ℝcr 11113  0cc0 11114  1c1 11115  ici 11116   + caddc 11117   · cmul 11119

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701  ax-1cn 11172  ax-icn 11173  ax-addcl 11174  ax-mulcl 11176  ax-mulrcl 11177  ax-i2m1 11182  ax-1ne0 11183  ax-rrecex 11186  ax-cnre 11187

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3431  df-v 3474  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-iota 6496  df-fv 6552  df-ov 7416

This theorem is referenced by:  1red  11221  1xr  11279  dedekind  11383  peano2re  11393  mul02lem2  11397  addrid  11400  renegcl  11529  peano2rem  11533  0reALT  11563  0lt1  11742  0le1  11743  relin01  11744  1le1  11848  eqneg  11940  ltp1  12060  ltm1  12062  recgt0  12066  mulgt1  12079  ltmulgt11  12080  lemulge11  12082  reclt1  12115  recgt1  12116  recgt1i  12117  recp1lt1  12118  recreclt  12119  recgt0ii  12126  ledivp1i  12145  ltdivp1i  12146  inelr  12208  cju  12214  nnssre  12222  nnge1  12246  nngt1ne1  12247  nnle1eq1  12248  nngt0  12249  nnnlt1  12250  nnne0  12252  nnrecre  12260  nnrecgt0  12261  nnsub  12262  2re  12292  3re  12298  4re  12302  5re  12305  6re  12308  7re  12311  8re  12314  9re  12317  0le2  12320  2pos  12321  3pos  12323  4pos  12325  5pos  12327  6pos  12328  7pos  12329  8pos  12330  9pos  12331  neg1rr  12333  neg1lt0  12335  1lt2  12389  1lt3  12391  1lt4  12394  1lt5  12398  1lt6  12403  1lt7  12409  1lt8  12416  1lt9  12424  1ne2  12426  1le2  12427  1le3  12430  halflt1  12436  addltmul  12454  nnunb  12474  elnnnn0c  12523  nn0ge2m1nn  12547  elnnz1  12594  znnnlt1  12595  zltp1le  12618  zleltp1  12619  nn0lt2  12631  recnz  12643  gtndiv  12645  3halfnz  12647  10re  12702  1lt10  12822  eluzp1m1  12854  eluzp1p1  12856  eluz2b2  12911  zbtwnre  12936  rebtwnz  12937  1rp  12984  divlt1lt  13049  divle1le  13050  nnledivrp  13092  qbtwnxr  13185  xmulrid  13264  xmulm1  13266  x2times  13284  xrub  13297  elicc01  13449  1elunit  13453  divelunit  13477  lincmb01cmp  13478  unitssre  13482  0nelfz1  13526  fzpreddisj  13556  fznatpl1  13561  fztpval  13569  fraclt1  13773  fracle1  13774  flbi2  13788  fldiv4p1lem1div2  13806  fldiv4lem1div2  13808  fldiv  13831  modid  13867  1mod  13874  m1modnnsub1  13888  modm1p1mod0  13893  seqf1olem1  14013  reexpcl  14050  reexpclz  14054  expge0  14070  expge1  14071  expgt1  14072  bernneq  14198  bernneq2  14199  expnbnd  14201  expnlbnd  14202  expnlbnd2  14203  expmulnbnd  14204  discr1  14208  facwordi  14255  faclbnd3  14258  faclbnd4lem1  14259  faclbnd4lem4  14262  faclbnd6  14265  facavg  14267  hashv01gt1  14311  hashnn0n0nn  14357  hashunsnggt  14360  hash1snb  14385  hashgt12el  14388  hashgt12el2  14389  hashfun  14403  hashge2el2dif  14447  lsw0  14521  f1oun2prg  14874  cjexp  15103  re1  15107  im1  15108  rei  15109  imi  15110  01sqrexlem1  15195  01sqrexlem2  15196  01sqrexlem3  15197  01sqrexlem4  15198  01sqrexlem7  15201  resqrex  15203  sqrt1  15224  sqrt2gt1lt2  15227  sqrtm1  15228  abs1  15250  absrdbnd  15294  caubnd2  15310  mulcn2  15546  reccn2  15547  rlimno1  15606  o1fsum  15765  expcnv  15816  geolim  15822  geolim2  15823  georeclim  15824  geomulcvg  15828  geoisumr  15830  geoisum1c  15832  fprodge0  15943  fprodge1  15945  rerisefaccl  15967  refallfaccl  15968  ere  16038  ege2le3  16039  efgt1  16065  resin4p  16087  recos4p  16088  tanhbnd  16110  sinbnd  16129  cosbnd  16130  sinbnd2  16131  cosbnd2  16132  ef01bndlem  16133  sin01bnd  16134  cos01bnd  16135  cos1bnd  16136  cos2bnd  16137  sinltx  16138  sin01gt0  16139  cos01gt0  16140  sin02gt0  16141  sincos1sgn  16142  ene1  16159  rpnnen2lem2  16164  rpnnen2lem3  16165  rpnnen2lem4  16166  rpnnen2lem9  16171  rpnnen2lem12  16174  ruclem6  16184  ruclem11  16189  ruclem12  16190  3dvds  16280  flodddiv4  16362  sadcadd  16405  isprm3  16626  sqnprm  16645  coprm  16654  phibndlem  16709  pythagtriplem3  16757  pcmpt  16831  fldivp1  16836  pockthi  16846  infpn2  16852  resslemOLD  17193  basendxnmulrndx  17246  basendxnmulrndxOLD  17247  starvndxnbasendx  17255  scandxnbasendx  17267  vscandxnbasendx  17272  ipndxnbasendx  17283  basendxnocndx  17334  slotsbhcdif  17366  slotsbhcdifOLD  17367  oppcbasOLD  17670  rescbasOLD  17783  rescabsOLD  17789  odubasOLD  18251  symgvalstructOLD  19308  lt6abl  19806  srgbinomlem4  20125  0ringnnzr  20416  abvneg  20587  abvtrivd  20593  rmodislmodOLD  20687  cnfldfunALTOLD  21160  xrsmcmn  21170  xrsnsgrp  21183  gzrngunitlem  21212  gzrngunit  21213  rge0srg  21218  psgnodpmr  21364  remulg  21381  resubdrg  21382  thlbasOLD  21471  tuslemOLD  23994  setsmsbasOLD  24204  dscmet  24303  dscopn  24304  nrginvrcnlem  24430  idnghm  24482  tgioo  24534  blcvx  24536  iicmp  24628  iiconn  24629  iirev  24672  iihalf1  24674  iihalf2  24677  iihalf2cnOLD  24679  elii1  24680  elii2  24681  iimulcl  24682  icopnfcnv  24689  icopnfhmeo  24690  iccpnfhmeo  24692  xrhmeo  24693  xrhmph  24694  evth  24707  xlebnum  24713  htpycc  24728  reparphti  24745  reparphtiOLD  24746  pcoval1  24762  pco1  24764  pcoval2  24765  pcocn  24766  pcohtpylem  24768  pcopt  24771  pcopt2  24772  pcoass  24773  pcorevlem  24775  nmhmcn  24869  ncvs1  24907  ovolunlem1a  25247  vitalilem2  25360  vitalilem4  25362  vitalilem5  25363  vitali  25364  i1f1  25441  itg11  25442  itg2const  25492  dveflem  25730  dvlipcn  25745  dvcvx  25771  ply1remlem  25914  fta1blem  25920  vieta1lem2  26058  aalioulem3  26081  aalioulem5  26083  aaliou3lem2  26090  ulmbdd  26144  iblulm  26153  radcnvlem1  26159  dvradcnv  26167  abelthlem2  26178  abelthlem3  26179  abelthlem5  26181  abelthlem7  26184  abelth  26187  abelth2  26188  reeff1olem  26192  reeff1o  26193  sinhalfpilem  26207  tangtx  26249  sincos4thpi  26257  pige3ALT  26263  coskpi  26266  cos0pilt1  26275  recosf1o  26278  tanregt0  26282  efif1olem3  26287  efif1olem4  26288  loge  26329  logdivlti  26362  logcnlem4  26387  logf1o2  26392  logtayl  26402  logccv  26405  recxpcl  26417  cxplea  26438  cxpcn3lem  26489  cxpaddlelem  26493  loglesqrt  26500  ang180lem2  26549  angpined  26569  acosrecl  26642  atancj  26649  atanlogaddlem  26652  atantan  26662  atans2  26670  ressatans  26673  leibpi  26681  log2le1  26689  birthdaylem3  26692  cxp2lim  26715  cxploglim  26716  cxploglim2  26717  divsqrtsumlem  26718  cvxcl  26723  scvxcvx  26724  jensenlem2  26726  amgmlem  26728  emcllem2  26735  emcllem4  26737  emcllem6  26739  emcllem7  26740  emre  26744  emgt0  26745  harmonicbnd3  26746  harmonicubnd  26748  harmonicbnd4  26749  zetacvg  26753  ftalem1  26811  ftalem2  26812  ftalem5  26815  issqf  26874  cht1  26903  chp1  26905  ppiltx  26915  mumullem2  26918  ppiublem1  26939  ppiub  26941  chtublem  26948  chtub  26949  logfacbnd3  26960  logexprlim  26962  perfectlem2  26967  dchrinv  26998  dchr1re  27000  efexple  27018  bposlem1  27021  bposlem2  27022  bposlem5  27025  bposlem8  27028  lgsdir2lem1  27062  lgsdir2lem5  27066  lgsdir  27069  lgsne0  27072  lgsabs1  27073  lgsdinn0  27082  gausslemma2dlem0i  27101  lgseisen  27116  m1lgs  27125  2lgslem3  27141  addsq2nreurex  27181  2sqreultblem  27185  2sqreunnltblem  27188  chebbnd1lem3  27208  chebbnd1  27209  chtppilimlem1  27210  chtppilimlem2  27211  chtppilim  27212  chpchtlim  27216  vmadivsumb  27220  rplogsumlem2  27222  rpvmasumlem  27224  dchrmusumlema  27230  dchrmusum2  27231  dchrvmasumlem2  27235  dchrvmasumiflem1  27238  dchrisum0flblem1  27245  dchrisum0flblem2  27246  dchrisum0fno1  27248  rpvmasum2  27249  dchrisum0re  27250  dchrisum0lema  27251  dchrisum0lem1b  27252  dchrisum0lem1  27253  dchrisum0lem2a  27254  dchrisum0lem2  27255  logdivsum  27270  mulog2sumlem2  27272  2vmadivsumlem  27277  log2sumbnd  27281  selbergb  27286  selberg2b  27289  chpdifbndlem1  27290  selberg3lem1  27294  selberg3lem2  27295  selberg4lem1  27297  pntrmax  27301  pntrsumo1  27302  selbergsb  27312  pntrlog2bndlem3  27316  pntrlog2bndlem5  27318  pntpbnd1a  27322  pntpbnd2  27324  pntibndlem1  27326  pntibndlem3  27329  pntlemd  27331  pntlemc  27332  pntlemb  27334  pntlemr  27339  pntlemf  27342  pntlemk  27343  pntlemo  27344  pntlem3  27346  pntleml  27348  abvcxp  27352  ostth2lem1  27355  ostth1  27370  ostth2lem2  27371  ostth2lem3  27372  ostth2lem4  27373  ostth2  27374  ostth3  27375  ostth  27376  slotsinbpsd  27957  slotslnbpsd  27958  trgcgrg  28031  brbtwn2  28428  colinearalglem4  28432  ax5seglem2  28452  ax5seglem3  28454  axpaschlem  28463  axpasch  28464  axlowdimlem6  28470  axlowdimlem10  28474  axlowdimlem16  28480  axlowdim1  28482  axlowdim2  28483  axlowdim  28484  axcontlem2  28488  elntg2  28508  lfgrnloop  28650  lfuhgr1v0e  28776  usgrexmpldifpr  28780  usgrexmplef  28781  1loopgrvd2  29025  vdegp1bi  29059  lfgrwlkprop  29209  pthdlem1  29288  pthdlem2  29290  clwlkclwwlkf  29526  upgr4cycl4dv4e  29703  konigsberglem2  29771  konigsberglem3  29772  konigsberglem5  29774  frgrreg  29912  ex-dif  29941  ex-in  29943  ex-pss  29946  ex-res  29959  ex-fl  29965  nv1  30193  smcnlem  30215  ipidsq  30228  nmlno0lem  30311  norm-ii-i  30655  bcs2  30700  norm1  30767  nmopub2tALT  31427  nmfnleub2  31444  nmlnop0iALT  31513  unopbd  31533  nmopadjlem  31607  nmopcoadji  31619  pjnmopi  31666  pjbdlni  31667  hstle1  31744  hstle  31748  hstles  31749  stge1i  31756  stlesi  31759  staddi  31764  stadd3i  31766  strlem1  31768  strlem5  31773  jplem1  31786  cdj1i  31951  addltmulALT  31964  xlt2addrd  32236  pr01ssre  32295  dp2lt10  32315  dp2ltsuc  32317  dp2ltc  32318  dplti  32336  dpmul4  32345  cshw1s2  32389  xrsmulgzz  32444  resvbasOLD  32716  rearchi  32729  xrge0slmod  32731  prmidl0  32841  submateqlem1  33083  xrge0iifcnv  33209  xrge0iifcv  33210  xrge0iifiso  33211  xrge0iifhom  33213  zrhre  33295  indf  33309  indfval  33310  esumcst  33357  cntnevol  33522  omssubadd  33595  iwrdsplit  33682  dstfrvclim1  33772  coinfliprv  33777  ballotlem2  33783  ballotlem4  33793  ballotlemi1  33797  ballotlemic  33801  sgnclre  33834  sgnnbi  33840  sgnpbi  33841  sgnmulsgp  33845  plymulx0  33854  plymulx  33855  signswch  33868  signstf  33873  signsvfn  33889  itgexpif  33914  hgt750lemd  33956  logdivsqrle  33958  hgt750lem  33959  hgt750lem2  33960  hgt750leme  33966  tgoldbachgnn  33967  subfacp1lem1  34466  subfacp1lem5  34471  resconn  34533  iisconn  34539  iillysconn  34540  problem2  34947  problem3  34948  sinccvglem  34953  fz0n  35002  dnibndlem12  35670  knoppcnlem4  35677  knoppndvlem13  35705  cnndvlem1  35718  irrdiff  36512  relowlpssretop  36550  sin2h  36783  cos2h  36784  tan2h  36785  poimirlem7  36800  poimirlem16  36809  poimirlem17  36810  poimirlem19  36812  poimirlem20  36813  poimirlem22  36815  poimirlem23  36816  poimirlem29  36822  poimirlem31  36824  itg2addnclem3  36846  asindmre  36876  dvasin  36877  dvacos  36878  dvreasin  36879  dvreacos  36880  fdc  36918  geomcau  36932  cntotbnd  36969  heiborlem8  36991  bfplem2  36996  bfp  36997  aks4d1p1p7  41247  2xp3dxp2ge1d  41330  factwoffsmonot  41331  1t1e1ALT  41480  re1m1e0m0  41574  sn-00idlem1  41575  sn-00idlem2  41576  remul02  41582  sn-0ne2  41583  reixi  41599  rei4  41600  remullid  41610  ipiiie0  41614  sn-0tie0  41616  sn-nnne0  41625  mulgt0b2d  41637  sn-0lt1  41639  sn-ltp1  41640  reneg1lt0  41641  sn-inelr  41642  rabren3dioph  41857  pellexlem5  41875  pellexlem6  41876  pell1qrgaplem  41915  pell14qrgap  41917  pellqrex  41921  pellfundre  41923  pellfundlb  41926  pellfund14gap  41929  jm2.17a  42003  acongeq  42026  jm2.23  42039  jm3.1lem2  42061  sqrtcval  42696  sqrtcval2  42697  resqrtval  42698  imsqrtval  42699  relexp01min  42768  mnringbasedOLD  43275  cvgdvgrat  43376  lhe4.4ex1a  43392  binomcxplemnotnn0  43419  isosctrlem1ALT  43999  supxrgelem  44347  xrlexaddrp  44362  infxr  44377  infleinflem2  44381  sumnnodd  44646  limsup10exlem  44788  limsup10ex  44789  dvnprodlem3  44964  stoweidlem1  45017  stoweidlem18  45034  stoweidlem19  45035  stoweidlem26  45042  stoweidlem34  45050  stoweidlem40  45056  stoweidlem41  45057  stoweidlem59  45075  stoweid  45079  stirlinglem10  45099  stirlinglem11  45100  dirkercncflem1  45119  fourierdlem16  45139  fourierdlem21  45144  fourierdlem22  45145  fourierdlem42  45165  fourierdlem68  45190  fourierdlem83  45205  fourierdlem103  45225  sqwvfourb  45245  fouriersw  45247  etransclem23  45273  salgencntex  45359  ovn0lem  45581  smfmullem3  45809  smfmullem4  45810  zm1nn  46310  m1mod0mod1  46337  fmtnosqrt  46507  perfectALTVlem2  46690  2exp340mod341  46701  8exp8mod9  46704  nfermltl8rev  46710  nnsum3primesprm  46758  nnsum4primesodd  46764  nnsum4primesoddALTV  46765  nnsum4primeseven  46768  nnsum4primesevenALTV  46769  tgblthelfgott  46783  tgoldbach  46785  rege1logbrege0  47333  rege1logbzge0  47334  blennnelnn  47351  dignnld  47378  nn0sumshdiglemA  47394  nn0sumshdiglem1  47396  rrx2xpref1o  47493  rrxlines  47508  eenglngeehlnmlem1  47512  eenglngeehlnmlem2  47513  line2ylem  47526  line2x  47529  icccldii  47640  io1ii  47642  sepfsepc  47649