Theorem 1re 11155

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 11109, 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 11120	. . 3 ⊢ 1 ≠ 0
2		ax-1cn 11109	. . . . 5 ⊢ 1 ∈ ℂ
3		cnre 11152	. . . . 5 ⊢ (1 ∈ ℂ → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)))
4	2, 3	ax-mp 5	. . . 4 ⊢ ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏))
5		neeq1 3006	. . . . . . . 8 ⊢ (1 = (𝑎 + (i · 𝑏)) → (1 ≠ 0 ↔ (𝑎 + (i · 𝑏)) ≠ 0))
6	5	biimpcd 248	. . . . . . 7 ⊢ (1 ≠ 0 → (1 = (𝑎 + (i · 𝑏)) → (𝑎 + (i · 𝑏)) ≠ 0))
7		0cn 11147	. . . . . . . 8 ⊢ 0 ∈ ℂ
8		cnre 11152	. . . . . . . 8 ⊢ (0 ∈ ℂ → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)))
9	7, 8	ax-mp 5	. . . . . . 7 ⊢ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑))
10		neeq2 3007	. . . . . . . . . 10 ⊢ (0 = (𝑐 + (i · 𝑑)) → ((𝑎 + (i · 𝑏)) ≠ 0 ↔ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
11	10	biimpcd 248	. . . . . . . . 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 982	. . . . . . . . 9 ⊢ (¬ (𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑) ↔ (¬ 𝑎 ≠ 𝑐 ∧ ¬ 𝑏 ≠ 𝑑))
19		df-ne 2944	. . . . . . . . . . 11 ⊢ (𝑎 ≠ 𝑐 ↔ ¬ 𝑎 = 𝑐)
20	19	con2bii 357	. . . . . . . . . 10 ⊢ (𝑎 = 𝑐 ↔ ¬ 𝑎 ≠ 𝑐)
21		df-ne 2944	. . . . . . . . . . 11 ⊢ (𝑏 ≠ 𝑑 ↔ ¬ 𝑏 = 𝑑)
22	21	con2bii 357	. . . . . . . . . 10 ⊢ (𝑏 = 𝑑 ↔ ¬ 𝑏 ≠ 𝑑)
23	20, 22	anbi12i 627	. . . . . . . . 9 ⊢ ((𝑎 = 𝑐 ∧ 𝑏 = 𝑑) ↔ (¬ 𝑎 ≠ 𝑐 ∧ ¬ 𝑏 ≠ 𝑑))
24	18, 23	bitr4i 277	. . . . . . . 8 ⊢ (¬ (𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑) ↔ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑))
25		id 22	. . . . . . . . 9 ⊢ (𝑎 = 𝑐 → 𝑎 = 𝑐)
26		oveq2 7365	. . . . . . . . 9 ⊢ (𝑏 = 𝑑 → (i · 𝑏) = (i · 𝑑))
27	25, 26	oveqan12d 7376	. . . . . . . 8 ⊢ ((𝑎 = 𝑐 ∧ 𝑏 = 𝑑) → (𝑎 + (i · 𝑏)) = (𝑐 + (i · 𝑑)))
28	24, 27	sylbi 216	. . . . . . 7 ⊢ (¬ (𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑) → (𝑎 + (i · 𝑏)) = (𝑐 + (i · 𝑑)))
29	28	necon1ai 2971	. . . . . 6 ⊢ ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → (𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑))
30		neeq1 3006	. . . . . . . . . 10 ⊢ (𝑥 = 𝑎 → (𝑥 ≠ 𝑦 ↔ 𝑎 ≠ 𝑦))
31		neeq2 3007	. . . . . . . . . 10 ⊢ (𝑦 = 𝑐 → (𝑎 ≠ 𝑦 ↔ 𝑎 ≠ 𝑐))
32	30, 31	rspc2ev 3592	. . . . . . . . 9 ⊢ ((𝑎 ∈ ℝ ∧ 𝑐 ∈ ℝ ∧ 𝑎 ≠ 𝑐) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦)
33	32	3expia 1121	. . . . . . . 8 ⊢ ((𝑎 ∈ ℝ ∧ 𝑐 ∈ ℝ) → (𝑎 ≠ 𝑐 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
34	33	ad2ant2r 745	. . . . . . 7 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → (𝑎 ≠ 𝑐 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
35		neeq1 3006	. . . . . . . . . 10 ⊢ (𝑥 = 𝑏 → (𝑥 ≠ 𝑦 ↔ 𝑏 ≠ 𝑦))
36		neeq2 3007	. . . . . . . . . 10 ⊢ (𝑦 = 𝑑 → (𝑏 ≠ 𝑦 ↔ 𝑏 ≠ 𝑑))
37	35, 36	rspc2ev 3592	. . . . . . . . 9 ⊢ ((𝑏 ∈ ℝ ∧ 𝑑 ∈ ℝ ∧ 𝑏 ≠ 𝑑) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦)
38	37	3expia 1121	. . . . . . . 8 ⊢ ((𝑏 ∈ ℝ ∧ 𝑑 ∈ ℝ) → (𝑏 ≠ 𝑑 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
39	38	ad2ant2l 744	. . . . . . 7 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → (𝑏 ≠ 𝑑 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
40	34, 39	jaod 857	. . . . . 6 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → ((𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
41	29, 40	syl5 34	. . . . 5 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
42	41	rexlimdvva 3205	. . . 4 ⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
43	42	rexlimivv 3196	. . 3 ⊢ (∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦)
44	1, 17, 43	mp2b 10	. 2 ⊢ ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦
45		eqtr3 2762	. . . . . . . . 9 ⊢ ((𝑥 = 0 ∧ 𝑦 = 0) → 𝑥 = 𝑦)
46	45	ex 413	. . . . . . . 8 ⊢ (𝑥 = 0 → (𝑦 = 0 → 𝑥 = 𝑦))
47	46	necon3d 2964	. . . . . . 7 ⊢ (𝑥 = 0 → (𝑥 ≠ 𝑦 → 𝑦 ≠ 0))
48		neeq1 3006	. . . . . . . . 9 ⊢ (𝑧 = 𝑦 → (𝑧 ≠ 0 ↔ 𝑦 ≠ 0))
49	48	rspcev 3581	. . . . . . . 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 3006	. . . . . . . 8 ⊢ (𝑧 = 𝑥 → (𝑧 ≠ 0 ↔ 𝑥 ≠ 0))
55	54	rspcev 3581	. . . . . . 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 3028	. . 3 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
60	59	rexlimivv 3196	. 2 ⊢ (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)
61		ax-rrecex 11123	. . . 4 ⊢ ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → ∃𝑥 ∈ ℝ (𝑧 · 𝑥) = 1)
62		remulcl 11136	. . . . . . 7 ⊢ ((𝑧 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (𝑧 · 𝑥) ∈ ℝ)
63	62	adantlr 713	. . . . . 6 ⊢ (((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) ∧ 𝑥 ∈ ℝ) → (𝑧 · 𝑥) ∈ ℝ)
64		eleq1 2825	. . . . . 6 ⊢ ((𝑧 · 𝑥) = 1 → ((𝑧 · 𝑥) ∈ ℝ ↔ 1 ∈ ℝ))
65	63, 64	syl5ibcom 244	. . . . 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 396   ∨ wo 845   = wceq 1541   ∈ wcel 2106   ≠ wne 2943  ∃wrex 3073  (class class class)co 7357  ℂcc 11049  ℝcr 11050  0cc0 11051  1c1 11052  ici 11053   + caddc 11054   · cmul 11056

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2707  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-mulcl 11113  ax-mulrcl 11114  ax-i2m1 11119  ax-1ne0 11120  ax-rrecex 11123  ax-cnre 11124

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  df-ne 2944  df-ral 3065  df-rex 3074  df-rab 3408  df-v 3447  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-br 5106  df-iota 6448  df-fv 6504  df-ov 7360

This theorem is referenced by:  1red  11156  1xr  11214  dedekind  11318  peano2re  11328  mul02lem2  11332  addid1  11335  renegcl  11464  peano2rem  11468  0reALT  11498  0lt1  11677  0le1  11678  relin01  11679  1le1  11783  eqneg  11875  ltp1  11995  ltm1  11997  recgt0  12001  mulgt1  12014  ltmulgt11  12015  lemulge11  12017  reclt1  12050  recgt1  12051  recgt1i  12052  recp1lt1  12053  recreclt  12054  recgt0ii  12061  ledivp1i  12080  ltdivp1i  12081  inelr  12143  cju  12149  nnssre  12157  nnge1  12181  nngt1ne1  12182  nnle1eq1  12183  nngt0  12184  nnnlt1  12185  nnne0  12187  nnrecre  12195  nnrecgt0  12196  nnsub  12197  2re  12227  3re  12233  4re  12237  5re  12240  6re  12243  7re  12246  8re  12249  9re  12252  0le2  12255  2pos  12256  3pos  12258  4pos  12260  5pos  12262  6pos  12263  7pos  12264  8pos  12265  9pos  12266  neg1rr  12268  neg1lt0  12270  1lt2  12324  1lt3  12326  1lt4  12329  1lt5  12333  1lt6  12338  1lt7  12344  1lt8  12351  1lt9  12359  1ne2  12361  1le2  12362  1le3  12365  halflt1  12371  addltmul  12389  nnunb  12409  elnnnn0c  12458  nn0ge2m1nn  12482  elnnz1  12529  znnnlt1  12530  zltp1le  12553  zleltp1  12554  nn0lt2  12566  recnz  12578  gtndiv  12580  3halfnz  12582  10re  12637  1lt10  12757  eluzp1m1  12789  eluzp1p1  12791  eluz2b2  12846  zbtwnre  12871  rebtwnz  12872  1rp  12919  divlt1lt  12984  divle1le  12985  nnledivrp  13027  qbtwnxr  13119  xmulid1  13198  xmulm1  13200  x2times  13218  xrub  13231  elicc01  13383  1elunit  13387  divelunit  13411  lincmb01cmp  13412  unitssre  13416  0nelfz1  13460  fzpreddisj  13490  fznatpl1  13495  fztpval  13503  fraclt1  13707  fracle1  13708  flbi2  13722  fldiv4p1lem1div2  13740  fldiv4lem1div2  13742  fldiv  13765  modid  13801  1mod  13808  m1modnnsub1  13822  modm1p1mod0  13827  seqf1olem1  13947  reexpcl  13984  reexpclz  13988  expge0  14004  expge1  14005  expgt1  14006  bernneq  14132  bernneq2  14133  expnbnd  14135  expnlbnd  14136  expnlbnd2  14137  expmulnbnd  14138  discr1  14142  facwordi  14189  faclbnd3  14192  faclbnd4lem1  14193  faclbnd4lem4  14196  faclbnd6  14199  facavg  14201  hashv01gt1  14245  hashnn0n0nn  14291  hashunsnggt  14294  hash1snb  14319  hashgt12el  14322  hashgt12el2  14323  hashfun  14337  hashge2el2dif  14379  lsw0  14453  f1oun2prg  14806  cjexp  15035  re1  15039  im1  15040  rei  15041  imi  15042  01sqrexlem1  15127  01sqrexlem2  15128  01sqrexlem3  15129  01sqrexlem4  15130  01sqrexlem7  15133  resqrex  15135  sqrt1  15156  sqrt2gt1lt2  15159  sqrtm1  15160  abs1  15182  absrdbnd  15226  caubnd2  15242  mulcn2  15478  reccn2  15479  rlimno1  15538  o1fsum  15698  expcnv  15749  geolim  15755  geolim2  15756  georeclim  15757  geomulcvg  15761  geoisumr  15763  geoisum1c  15765  fprodge0  15876  fprodge1  15878  rerisefaccl  15900  refallfaccl  15901  ere  15971  ege2le3  15972  efgt1  15998  resin4p  16020  recos4p  16021  tanhbnd  16043  sinbnd  16062  cosbnd  16063  sinbnd2  16064  cosbnd2  16065  ef01bndlem  16066  sin01bnd  16067  cos01bnd  16068  cos1bnd  16069  cos2bnd  16070  sinltx  16071  sin01gt0  16072  cos01gt0  16073  sin02gt0  16074  sincos1sgn  16075  ene1  16092  rpnnen2lem2  16097  rpnnen2lem3  16098  rpnnen2lem4  16099  rpnnen2lem9  16104  rpnnen2lem12  16107  ruclem6  16117  ruclem11  16122  ruclem12  16123  3dvds  16213  flodddiv4  16295  sadcadd  16338  isprm3  16559  sqnprm  16578  coprm  16587  phibndlem  16642  pythagtriplem3  16690  pcmpt  16764  fldivp1  16769  pockthi  16779  infpn2  16785  resslemOLD  17123  basendxnmulrndx  17176  basendxnmulrndxOLD  17177  starvndxnbasendx  17185  scandxnbasendx  17197  vscandxnbasendx  17202  ipndxnbasendx  17213  basendxnocndx  17264  slotsbhcdif  17296  slotsbhcdifOLD  17297  oppcbasOLD  17600  rescbasOLD  17713  rescabsOLD  17719  odubasOLD  18181  symgvalstructOLD  19179  lt6abl  19672  srgbinomlem4  19960  abvneg  20293  abvtrivd  20299  rmodislmodOLD  20391  0ringnnzr  20739  cnfldfunALTOLD  20810  xrsmcmn  20820  xrsnsgrp  20833  gzrngunitlem  20862  gzrngunit  20863  rge0srg  20868  psgnodpmr  20994  remulg  21011  resubdrg  21012  thlbasOLD  21101  tuslemOLD  23619  setsmsbasOLD  23829  dscmet  23928  dscopn  23929  nrginvrcnlem  24055  idnghm  24107  tgioo  24159  blcvx  24161  iicmp  24249  iiconn  24250  iirev  24292  iihalf1  24294  iihalf2  24296  iihalf2cn  24297  elii1  24298  elii2  24299  iimulcl  24300  icopnfcnv  24305  icopnfhmeo  24306  iccpnfhmeo  24308  xrhmeo  24309  xrhmph  24310  evth  24322  xlebnum  24328  htpycc  24343  reparphti  24360  pcoval1  24376  pco1  24378  pcoval2  24379  pcocn  24380  pcohtpylem  24382  pcopt  24385  pcopt2  24386  pcoass  24387  pcorevlem  24389  nmhmcn  24483  ncvs1  24521  ovolunlem1a  24860  vitalilem2  24973  vitalilem4  24975  vitalilem5  24976  vitali  24977  i1f1  25054  itg11  25055  itg2const  25105  dveflem  25343  dvlipcn  25358  dvcvx  25384  ply1remlem  25527  fta1blem  25533  vieta1lem2  25671  aalioulem3  25694  aalioulem5  25696  aaliou3lem2  25703  ulmbdd  25757  iblulm  25766  radcnvlem1  25772  dvradcnv  25780  abelthlem2  25791  abelthlem3  25792  abelthlem5  25794  abelthlem7  25797  abelth  25800  abelth2  25801  reeff1olem  25805  reeff1o  25806  sinhalfpilem  25820  tangtx  25862  sincos4thpi  25870  pige3ALT  25876  coskpi  25879  cos0pilt1  25888  recosf1o  25891  tanregt0  25895  efif1olem3  25900  efif1olem4  25901  loge  25942  logdivlti  25975  logcnlem4  26000  logf1o2  26005  logtayl  26015  logccv  26018  recxpcl  26030  cxplea  26051  cxpcn3lem  26100  cxpaddlelem  26104  loglesqrt  26111  ang180lem2  26160  angpined  26180  acosrecl  26253  atancj  26260  atanlogaddlem  26263  atantan  26273  atans2  26281  ressatans  26284  leibpi  26292  log2le1  26300  birthdaylem3  26303  cxp2lim  26326  cxploglim  26327  cxploglim2  26328  divsqrtsumlem  26329  cvxcl  26334  scvxcvx  26335  jensenlem2  26337  amgmlem  26339  emcllem2  26346  emcllem4  26348  emcllem6  26350  emcllem7  26351  emre  26355  emgt0  26356  harmonicbnd3  26357  harmonicubnd  26359  harmonicbnd4  26360  zetacvg  26364  ftalem1  26422  ftalem2  26423  ftalem5  26426  issqf  26485  cht1  26514  chp1  26516  ppiltx  26526  mumullem2  26529  ppiublem1  26550  ppiub  26552  chtublem  26559  chtub  26560  logfacbnd3  26571  logexprlim  26573  perfectlem2  26578  dchrinv  26609  dchr1re  26611  efexple  26629  bposlem1  26632  bposlem2  26633  bposlem5  26636  bposlem8  26639  lgsdir2lem1  26673  lgsdir2lem5  26677  lgsdir  26680  lgsne0  26683  lgsabs1  26684  lgsdinn0  26693  gausslemma2dlem0i  26712  lgseisen  26727  m1lgs  26736  2lgslem3  26752  addsq2nreurex  26792  2sqreultblem  26796  2sqreunnltblem  26799  chebbnd1lem3  26819  chebbnd1  26820  chtppilimlem1  26821  chtppilimlem2  26822  chtppilim  26823  chpchtlim  26827  vmadivsumb  26831  rplogsumlem2  26833  rpvmasumlem  26835  dchrmusumlema  26841  dchrmusum2  26842  dchrvmasumlem2  26846  dchrvmasumiflem1  26849  dchrisum0flblem1  26856  dchrisum0flblem2  26857  dchrisum0fno1  26859  rpvmasum2  26860  dchrisum0re  26861  dchrisum0lema  26862  dchrisum0lem1b  26863  dchrisum0lem1  26864  dchrisum0lem2a  26865  dchrisum0lem2  26866  logdivsum  26881  mulog2sumlem2  26883  2vmadivsumlem  26888  log2sumbnd  26892  selbergb  26897  selberg2b  26900  chpdifbndlem1  26901  selberg3lem1  26905  selberg3lem2  26906  selberg4lem1  26908  pntrmax  26912  pntrsumo1  26913  selbergsb  26923  pntrlog2bndlem3  26927  pntrlog2bndlem5  26929  pntpbnd1a  26933  pntpbnd2  26935  pntibndlem1  26937  pntibndlem3  26940  pntlemd  26942  pntlemc  26943  pntlemb  26945  pntlemr  26950  pntlemf  26953  pntlemk  26954  pntlemo  26955  pntlem3  26957  pntleml  26959  abvcxp  26963  ostth2lem1  26966  ostth1  26981  ostth2lem2  26982  ostth2lem3  26983  ostth2lem4  26984  ostth2  26985  ostth3  26986  ostth  26987  slotsinbpsd  27383  slotslnbpsd  27384  trgcgrg  27457  brbtwn2  27854  colinearalglem4  27858  ax5seglem2  27878  ax5seglem3  27880  axpaschlem  27889  axpasch  27890  axlowdimlem6  27896  axlowdimlem10  27900  axlowdimlem16  27906  axlowdim1  27908  axlowdim2  27909  axlowdim  27910  axcontlem2  27914  elntg2  27934  lfgrnloop  28076  lfuhgr1v0e  28202  usgrexmpldifpr  28206  usgrexmplef  28207  1loopgrvd2  28451  vdegp1bi  28485  lfgrwlkprop  28635  pthdlem1  28714  pthdlem2  28716  clwlkclwwlkf  28952  upgr4cycl4dv4e  29129  konigsberglem2  29197  konigsberglem3  29198  konigsberglem5  29200  frgrreg  29338  ex-dif  29367  ex-in  29369  ex-pss  29372  ex-res  29385  ex-fl  29391  nv1  29617  smcnlem  29639  ipidsq  29652  nmlno0lem  29735  norm-ii-i  30079  bcs2  30124  norm1  30191  nmopub2tALT  30851  nmfnleub2  30868  nmlnop0iALT  30937  unopbd  30957  nmopadjlem  31031  nmopcoadji  31043  pjnmopi  31090  pjbdlni  31091  hstle1  31168  hstle  31172  hstles  31173  stge1i  31180  stlesi  31183  staddi  31188  stadd3i  31190  strlem1  31192  strlem5  31197  jplem1  31210  cdj1i  31375  addltmulALT  31388  xlt2addrd  31663  pr01ssre  31720  dp2lt10  31740  dp2ltsuc  31742  dp2ltc  31743  dplti  31761  dpmul4  31770  cshw1s2  31814  xrsmulgzz  31869  resvbasOLD  32125  rearchi  32138  xrge0slmod  32140  prmidl0  32223  submateqlem1  32388  xrge0iifcnv  32514  xrge0iifcv  32515  xrge0iifiso  32516  xrge0iifhom  32518  zrhre  32600  indf  32614  indfval  32615  esumcst  32662  cntnevol  32827  omssubadd  32900  iwrdsplit  32987  dstfrvclim1  33077  coinfliprv  33082  ballotlem2  33088  ballotlem4  33098  ballotlemi1  33102  ballotlemic  33106  sgnclre  33139  sgnnbi  33145  sgnpbi  33146  sgnmulsgp  33150  plymulx0  33159  plymulx  33160  signswch  33173  signstf  33178  signsvfn  33194  itgexpif  33219  hgt750lemd  33261  logdivsqrle  33263  hgt750lem  33264  hgt750lem2  33265  hgt750leme  33271  tgoldbachgnn  33272  subfacp1lem1  33773  subfacp1lem5  33778  resconn  33840  iisconn  33846  iillysconn  33847  problem2  34254  problem3  34255  sinccvglem  34260  fz0n  34303  dnibndlem12  34952  knoppcnlem4  34959  knoppndvlem13  34987  cnndvlem1  35000  irrdiff  35797  relowlpssretop  35835  sin2h  36068  cos2h  36069  tan2h  36070  poimirlem7  36085  poimirlem16  36094  poimirlem17  36095  poimirlem19  36097  poimirlem20  36098  poimirlem22  36100  poimirlem23  36101  poimirlem29  36107  poimirlem31  36109  itg2addnclem3  36131  asindmre  36161  dvasin  36162  dvacos  36163  dvreasin  36164  dvreacos  36165  fdc  36204  geomcau  36218  cntotbnd  36255  heiborlem8  36277  bfplem2  36282  bfp  36283  aks4d1p1p7  40531  2xp3dxp2ge1d  40614  factwoffsmonot  40615  1t1e1ALT  40764  re1m1e0m0  40852  sn-00idlem1  40853  sn-00idlem2  40854  remul02  40860  sn-0ne2  40861  reixi  40877  rei4  40878  remulid2  40888  ipiiie0  40892  sn-0tie0  40894  sn-nnne0  40903  mulgt0b2d  40915  sn-0lt1  40917  sn-ltp1  40918  reneg1lt0  40919  sn-inelr  40920  rabren3dioph  41124  pellexlem5  41142  pellexlem6  41143  pell1qrgaplem  41182  pell14qrgap  41184  pellqrex  41188  pellfundre  41190  pellfundlb  41193  pellfund14gap  41196  jm2.17a  41270  acongeq  41293  jm2.23  41306  jm3.1lem2  41328  sqrtcval  41903  sqrtcval2  41904  resqrtval  41905  imsqrtval  41906  relexp01min  41975  mnringbasedOLD  42482  cvgdvgrat  42583  lhe4.4ex1a  42599  binomcxplemnotnn0  42626  isosctrlem1ALT  43206  supxrgelem  43561  xrlexaddrp  43576  infxr  43591  infleinflem2  43595  sumnnodd  43861  limsup10exlem  44003  limsup10ex  44004  dvnprodlem3  44179  stoweidlem1  44232  stoweidlem18  44249  stoweidlem19  44250  stoweidlem26  44257  stoweidlem34  44265  stoweidlem40  44271  stoweidlem41  44272  stoweidlem59  44290  stoweid  44294  stirlinglem10  44314  stirlinglem11  44315  dirkercncflem1  44334  fourierdlem16  44354  fourierdlem21  44359  fourierdlem22  44360  fourierdlem42  44380  fourierdlem68  44405  fourierdlem83  44420  fourierdlem103  44440  sqwvfourb  44460  fouriersw  44462  etransclem23  44488  salgencntex  44574  ovn0lem  44796  smfmullem3  45024  smfmullem4  45025  zm1nn  45524  m1mod0mod1  45551  fmtnosqrt  45721  perfectALTVlem2  45904  2exp340mod341  45915  8exp8mod9  45918  nfermltl8rev  45924  nnsum3primesprm  45972  nnsum4primesodd  45978  nnsum4primesoddALTV  45979  nnsum4primeseven  45982  nnsum4primesevenALTV  45983  tgblthelfgott  45997  tgoldbach  45999  rege1logbrege0  46634  rege1logbzge0  46635  blennnelnn  46652  dignnld  46679  nn0sumshdiglemA  46695  nn0sumshdiglem1  46697  rrx2xpref1o  46794  rrxlines  46809  eenglngeehlnmlem1  46813  eenglngeehlnmlem2  46814  line2ylem  46827  line2x  46830  icccldii  46941  io1ii  46943  sepfsepc  46950