Theorem 1re 11214

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 11168, 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 11179	. . 3 ⊢ 1 ≠ 0
2		ax-1cn 11168	. . . . 5 ⊢ 1 ∈ ℂ
3		cnre 11211	. . . . 5 ⊢ (1 ∈ ℂ → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)))
4	2, 3	ax-mp 5	. . . 4 ⊢ ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏))
5		neeq1 3004	. . . . . . . 8 ⊢ (1 = (𝑎 + (i · 𝑏)) → (1 ≠ 0 ↔ (𝑎 + (i · 𝑏)) ≠ 0))
6	5	biimpcd 248	. . . . . . 7 ⊢ (1 ≠ 0 → (1 = (𝑎 + (i · 𝑏)) → (𝑎 + (i · 𝑏)) ≠ 0))
7		0cn 11206	. . . . . . . 8 ⊢ 0 ∈ ℂ
8		cnre 11211	. . . . . . . 8 ⊢ (0 ∈ ℂ → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)))
9	7, 8	ax-mp 5	. . . . . . 7 ⊢ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑))
10		neeq2 3005	. . . . . . . . . 10 ⊢ (0 = (𝑐 + (i · 𝑑)) → ((𝑎 + (i · 𝑏)) ≠ 0 ↔ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
11	10	biimpcd 248	. . . . . . . . 9 ⊢ ((𝑎 + (i · 𝑏)) ≠ 0 → (0 = (𝑐 + (i · 𝑑)) → (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
12	11	reximdv 3171	. . . . . . . 8 ⊢ ((𝑎 + (i · 𝑏)) ≠ 0 → (∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)) → ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
13	12	reximdv 3171	. . . . . . 7 ⊢ ((𝑎 + (i · 𝑏)) ≠ 0 → (∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)) → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
14	6, 9, 13	syl6mpi 67	. . . . . 6 ⊢ (1 ≠ 0 → (1 = (𝑎 + (i · 𝑏)) → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
15	14	reximdv 3171	. . . . 5 ⊢ (1 ≠ 0 → (∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)) → ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
16	15	reximdv 3171	. . . 4 ⊢ (1 ≠ 0 → (∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)) → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
17	4, 16	mpi 20	. . 3 ⊢ (1 ≠ 0 → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)))
18		ioran 983	. . . . . . . . 9 ⊢ (¬ (𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑) ↔ (¬ 𝑎 ≠ 𝑐 ∧ ¬ 𝑏 ≠ 𝑑))
19		df-ne 2942	. . . . . . . . . . 11 ⊢ (𝑎 ≠ 𝑐 ↔ ¬ 𝑎 = 𝑐)
20	19	con2bii 358	. . . . . . . . . 10 ⊢ (𝑎 = 𝑐 ↔ ¬ 𝑎 ≠ 𝑐)
21		df-ne 2942	. . . . . . . . . . 11 ⊢ (𝑏 ≠ 𝑑 ↔ ¬ 𝑏 = 𝑑)
22	21	con2bii 358	. . . . . . . . . 10 ⊢ (𝑏 = 𝑑 ↔ ¬ 𝑏 ≠ 𝑑)
23	20, 22	anbi12i 628	. . . . . . . . 9 ⊢ ((𝑎 = 𝑐 ∧ 𝑏 = 𝑑) ↔ (¬ 𝑎 ≠ 𝑐 ∧ ¬ 𝑏 ≠ 𝑑))
24	18, 23	bitr4i 278	. . . . . . . 8 ⊢ (¬ (𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑) ↔ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑))
25		id 22	. . . . . . . . 9 ⊢ (𝑎 = 𝑐 → 𝑎 = 𝑐)
26		oveq2 7417	. . . . . . . . 9 ⊢ (𝑏 = 𝑑 → (i · 𝑏) = (i · 𝑑))
27	25, 26	oveqan12d 7428	. . . . . . . 8 ⊢ ((𝑎 = 𝑐 ∧ 𝑏 = 𝑑) → (𝑎 + (i · 𝑏)) = (𝑐 + (i · 𝑑)))
28	24, 27	sylbi 216	. . . . . . 7 ⊢ (¬ (𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑) → (𝑎 + (i · 𝑏)) = (𝑐 + (i · 𝑑)))
29	28	necon1ai 2969	. . . . . 6 ⊢ ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → (𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑))
30		neeq1 3004	. . . . . . . . . 10 ⊢ (𝑥 = 𝑎 → (𝑥 ≠ 𝑦 ↔ 𝑎 ≠ 𝑦))
31		neeq2 3005	. . . . . . . . . 10 ⊢ (𝑦 = 𝑐 → (𝑎 ≠ 𝑦 ↔ 𝑎 ≠ 𝑐))
32	30, 31	rspc2ev 3625	. . . . . . . . 9 ⊢ ((𝑎 ∈ ℝ ∧ 𝑐 ∈ ℝ ∧ 𝑎 ≠ 𝑐) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦)
33	32	3expia 1122	. . . . . . . 8 ⊢ ((𝑎 ∈ ℝ ∧ 𝑐 ∈ ℝ) → (𝑎 ≠ 𝑐 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
34	33	ad2ant2r 746	. . . . . . 7 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → (𝑎 ≠ 𝑐 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
35		neeq1 3004	. . . . . . . . . 10 ⊢ (𝑥 = 𝑏 → (𝑥 ≠ 𝑦 ↔ 𝑏 ≠ 𝑦))
36		neeq2 3005	. . . . . . . . . 10 ⊢ (𝑦 = 𝑑 → (𝑏 ≠ 𝑦 ↔ 𝑏 ≠ 𝑑))
37	35, 36	rspc2ev 3625	. . . . . . . . 9 ⊢ ((𝑏 ∈ ℝ ∧ 𝑑 ∈ ℝ ∧ 𝑏 ≠ 𝑑) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦)
38	37	3expia 1122	. . . . . . . 8 ⊢ ((𝑏 ∈ ℝ ∧ 𝑑 ∈ ℝ) → (𝑏 ≠ 𝑑 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
39	38	ad2ant2l 745	. . . . . . 7 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → (𝑏 ≠ 𝑑 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
40	34, 39	jaod 858	. . . . . 6 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → ((𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
41	29, 40	syl5 34	. . . . 5 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
42	41	rexlimdvva 3212	. . . 4 ⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
43	42	rexlimivv 3200	. . 3 ⊢ (∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦)
44	1, 17, 43	mp2b 10	. 2 ⊢ ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦
45		eqtr3 2759	. . . . . . . . 9 ⊢ ((𝑥 = 0 ∧ 𝑦 = 0) → 𝑥 = 𝑦)
46	45	ex 414	. . . . . . . 8 ⊢ (𝑥 = 0 → (𝑦 = 0 → 𝑥 = 𝑦))
47	46	necon3d 2962	. . . . . . 7 ⊢ (𝑥 = 0 → (𝑥 ≠ 𝑦 → 𝑦 ≠ 0))
48		neeq1 3004	. . . . . . . . 9 ⊢ (𝑧 = 𝑦 → (𝑧 ≠ 0 ↔ 𝑦 ≠ 0))
49	48	rspcev 3613	. . . . . . . 8 ⊢ ((𝑦 ∈ ℝ ∧ 𝑦 ≠ 0) → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)
50	49	expcom 415	. . . . . . 7 ⊢ (𝑦 ≠ 0 → (𝑦 ∈ ℝ → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
51	47, 50	syl6 35	. . . . . 6 ⊢ (𝑥 = 0 → (𝑥 ≠ 𝑦 → (𝑦 ∈ ℝ → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
52	51	com23 86	. . . . 5 ⊢ (𝑥 = 0 → (𝑦 ∈ ℝ → (𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
53	52	adantld 492	. . . 4 ⊢ (𝑥 = 0 → ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
54		neeq1 3004	. . . . . . . 8 ⊢ (𝑧 = 𝑥 → (𝑧 ≠ 0 ↔ 𝑥 ≠ 0))
55	54	rspcev 3613	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)
56	55	expcom 415	. . . . . 6 ⊢ (𝑥 ≠ 0 → (𝑥 ∈ ℝ → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
57	56	adantrd 493	. . . . 5 ⊢ (𝑥 ≠ 0 → ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
58	57	a1dd 50	. . . 4 ⊢ (𝑥 ≠ 0 → ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
59	53, 58	pm2.61ine 3026	. . 3 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
60	59	rexlimivv 3200	. 2 ⊢ (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)
61		ax-rrecex 11182	. . . 4 ⊢ ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → ∃𝑥 ∈ ℝ (𝑧 · 𝑥) = 1)
62		remulcl 11195	. . . . . . 7 ⊢ ((𝑧 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (𝑧 · 𝑥) ∈ ℝ)
63	62	adantlr 714	. . . . . 6 ⊢ (((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) ∧ 𝑥 ∈ ℝ) → (𝑧 · 𝑥) ∈ ℝ)
64		eleq1 2822	. . . . . 6 ⊢ ((𝑧 · 𝑥) = 1 → ((𝑧 · 𝑥) ∈ ℝ ↔ 1 ∈ ℝ))
65	63, 64	syl5ibcom 244	. . . . 5 ⊢ (((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) ∧ 𝑥 ∈ ℝ) → ((𝑧 · 𝑥) = 1 → 1 ∈ ℝ))
66	65	rexlimdva 3156	. . . 4 ⊢ ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → (∃𝑥 ∈ ℝ (𝑧 · 𝑥) = 1 → 1 ∈ ℝ))
67	61, 66	mpd 15	. . 3 ⊢ ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → 1 ∈ ℝ)
68	67	rexlimiva 3148	. 2 ⊢ (∃𝑧 ∈ ℝ 𝑧 ≠ 0 → 1 ∈ ℝ)
69	44, 60, 68	mp2b 10	1 ⊢ 1 ∈ ℝ

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 397   ∨ wo 846   = wceq 1542   ∈ wcel 2107   ≠ wne 2941  ∃wrex 3071  (class class class)co 7409  ℂcc 11108  ℝcr 11109  0cc0 11110  1c1 11111  ici 11112   + caddc 11113   · cmul 11115

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-1cn 11168  ax-icn 11169  ax-addcl 11170  ax-mulcl 11172  ax-mulrcl 11173  ax-i2m1 11178  ax-1ne0 11179  ax-rrecex 11182  ax-cnre 11183

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  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 7412

This theorem is referenced by:  1red  11215  1xr  11273  dedekind  11377  peano2re  11387  mul02lem2  11391  addrid  11394  renegcl  11523  peano2rem  11527  0reALT  11557  0lt1  11736  0le1  11737  relin01  11738  1le1  11842  eqneg  11934  ltp1  12054  ltm1  12056  recgt0  12060  mulgt1  12073  ltmulgt11  12074  lemulge11  12076  reclt1  12109  recgt1  12110  recgt1i  12111  recp1lt1  12112  recreclt  12113  recgt0ii  12120  ledivp1i  12139  ltdivp1i  12140  inelr  12202  cju  12208  nnssre  12216  nnge1  12240  nngt1ne1  12241  nnle1eq1  12242  nngt0  12243  nnnlt1  12244  nnne0  12246  nnrecre  12254  nnrecgt0  12255  nnsub  12256  2re  12286  3re  12292  4re  12296  5re  12299  6re  12302  7re  12305  8re  12308  9re  12311  0le2  12314  2pos  12315  3pos  12317  4pos  12319  5pos  12321  6pos  12322  7pos  12323  8pos  12324  9pos  12325  neg1rr  12327  neg1lt0  12329  1lt2  12383  1lt3  12385  1lt4  12388  1lt5  12392  1lt6  12397  1lt7  12403  1lt8  12410  1lt9  12418  1ne2  12420  1le2  12421  1le3  12424  halflt1  12430  addltmul  12448  nnunb  12468  elnnnn0c  12517  nn0ge2m1nn  12541  elnnz1  12588  znnnlt1  12589  zltp1le  12612  zleltp1  12613  nn0lt2  12625  recnz  12637  gtndiv  12639  3halfnz  12641  10re  12696  1lt10  12816  eluzp1m1  12848  eluzp1p1  12850  eluz2b2  12905  zbtwnre  12930  rebtwnz  12931  1rp  12978  divlt1lt  13043  divle1le  13044  nnledivrp  13086  qbtwnxr  13179  xmulrid  13258  xmulm1  13260  x2times  13278  xrub  13291  elicc01  13443  1elunit  13447  divelunit  13471  lincmb01cmp  13472  unitssre  13476  0nelfz1  13520  fzpreddisj  13550  fznatpl1  13555  fztpval  13563  fraclt1  13767  fracle1  13768  flbi2  13782  fldiv4p1lem1div2  13800  fldiv4lem1div2  13802  fldiv  13825  modid  13861  1mod  13868  m1modnnsub1  13882  modm1p1mod0  13887  seqf1olem1  14007  reexpcl  14044  reexpclz  14048  expge0  14064  expge1  14065  expgt1  14066  bernneq  14192  bernneq2  14193  expnbnd  14195  expnlbnd  14196  expnlbnd2  14197  expmulnbnd  14198  discr1  14202  facwordi  14249  faclbnd3  14252  faclbnd4lem1  14253  faclbnd4lem4  14256  faclbnd6  14259  facavg  14261  hashv01gt1  14305  hashnn0n0nn  14351  hashunsnggt  14354  hash1snb  14379  hashgt12el  14382  hashgt12el2  14383  hashfun  14397  hashge2el2dif  14441  lsw0  14515  f1oun2prg  14868  cjexp  15097  re1  15101  im1  15102  rei  15103  imi  15104  01sqrexlem1  15189  01sqrexlem2  15190  01sqrexlem3  15191  01sqrexlem4  15192  01sqrexlem7  15195  resqrex  15197  sqrt1  15218  sqrt2gt1lt2  15221  sqrtm1  15222  abs1  15244  absrdbnd  15288  caubnd2  15304  mulcn2  15540  reccn2  15541  rlimno1  15600  o1fsum  15759  expcnv  15810  geolim  15816  geolim2  15817  georeclim  15818  geomulcvg  15822  geoisumr  15824  geoisum1c  15826  fprodge0  15937  fprodge1  15939  rerisefaccl  15961  refallfaccl  15962  ere  16032  ege2le3  16033  efgt1  16059  resin4p  16081  recos4p  16082  tanhbnd  16104  sinbnd  16123  cosbnd  16124  sinbnd2  16125  cosbnd2  16126  ef01bndlem  16127  sin01bnd  16128  cos01bnd  16129  cos1bnd  16130  cos2bnd  16131  sinltx  16132  sin01gt0  16133  cos01gt0  16134  sin02gt0  16135  sincos1sgn  16136  ene1  16153  rpnnen2lem2  16158  rpnnen2lem3  16159  rpnnen2lem4  16160  rpnnen2lem9  16165  rpnnen2lem12  16168  ruclem6  16178  ruclem11  16183  ruclem12  16184  3dvds  16274  flodddiv4  16356  sadcadd  16399  isprm3  16620  sqnprm  16639  coprm  16648  phibndlem  16703  pythagtriplem3  16751  pcmpt  16825  fldivp1  16830  pockthi  16840  infpn2  16846  resslemOLD  17187  basendxnmulrndx  17240  basendxnmulrndxOLD  17241  starvndxnbasendx  17249  scandxnbasendx  17261  vscandxnbasendx  17266  ipndxnbasendx  17277  basendxnocndx  17328  slotsbhcdif  17360  slotsbhcdifOLD  17361  oppcbasOLD  17664  rescbasOLD  17777  rescabsOLD  17783  odubasOLD  18245  symgvalstructOLD  19265  lt6abl  19763  srgbinomlem4  20052  0ringnnzr  20302  abvneg  20442  abvtrivd  20448  rmodislmodOLD  20541  cnfldfunALTOLD  20958  xrsmcmn  20968  xrsnsgrp  20981  gzrngunitlem  21010  gzrngunit  21011  rge0srg  21016  psgnodpmr  21143  remulg  21160  resubdrg  21161  thlbasOLD  21250  tuslemOLD  23772  setsmsbasOLD  23982  dscmet  24081  dscopn  24082  nrginvrcnlem  24208  idnghm  24260  tgioo  24312  blcvx  24314  iicmp  24402  iiconn  24403  iirev  24445  iihalf1  24447  iihalf2  24449  iihalf2cn  24450  elii1  24451  elii2  24452  iimulcl  24453  icopnfcnv  24458  icopnfhmeo  24459  iccpnfhmeo  24461  xrhmeo  24462  xrhmph  24463  evth  24475  xlebnum  24481  htpycc  24496  reparphti  24513  pcoval1  24529  pco1  24531  pcoval2  24532  pcocn  24533  pcohtpylem  24535  pcopt  24538  pcopt2  24539  pcoass  24540  pcorevlem  24542  nmhmcn  24636  ncvs1  24674  ovolunlem1a  25013  vitalilem2  25126  vitalilem4  25128  vitalilem5  25129  vitali  25130  i1f1  25207  itg11  25208  itg2const  25258  dveflem  25496  dvlipcn  25511  dvcvx  25537  ply1remlem  25680  fta1blem  25686  vieta1lem2  25824  aalioulem3  25847  aalioulem5  25849  aaliou3lem2  25856  ulmbdd  25910  iblulm  25919  radcnvlem1  25925  dvradcnv  25933  abelthlem2  25944  abelthlem3  25945  abelthlem5  25947  abelthlem7  25950  abelth  25953  abelth2  25954  reeff1olem  25958  reeff1o  25959  sinhalfpilem  25973  tangtx  26015  sincos4thpi  26023  pige3ALT  26029  coskpi  26032  cos0pilt1  26041  recosf1o  26044  tanregt0  26048  efif1olem3  26053  efif1olem4  26054  loge  26095  logdivlti  26128  logcnlem4  26153  logf1o2  26158  logtayl  26168  logccv  26171  recxpcl  26183  cxplea  26204  cxpcn3lem  26255  cxpaddlelem  26259  loglesqrt  26266  ang180lem2  26315  angpined  26335  acosrecl  26408  atancj  26415  atanlogaddlem  26418  atantan  26428  atans2  26436  ressatans  26439  leibpi  26447  log2le1  26455  birthdaylem3  26458  cxp2lim  26481  cxploglim  26482  cxploglim2  26483  divsqrtsumlem  26484  cvxcl  26489  scvxcvx  26490  jensenlem2  26492  amgmlem  26494  emcllem2  26501  emcllem4  26503  emcllem6  26505  emcllem7  26506  emre  26510  emgt0  26511  harmonicbnd3  26512  harmonicubnd  26514  harmonicbnd4  26515  zetacvg  26519  ftalem1  26577  ftalem2  26578  ftalem5  26581  issqf  26640  cht1  26669  chp1  26671  ppiltx  26681  mumullem2  26684  ppiublem1  26705  ppiub  26707  chtublem  26714  chtub  26715  logfacbnd3  26726  logexprlim  26728  perfectlem2  26733  dchrinv  26764  dchr1re  26766  efexple  26784  bposlem1  26787  bposlem2  26788  bposlem5  26791  bposlem8  26794  lgsdir2lem1  26828  lgsdir2lem5  26832  lgsdir  26835  lgsne0  26838  lgsabs1  26839  lgsdinn0  26848  gausslemma2dlem0i  26867  lgseisen  26882  m1lgs  26891  2lgslem3  26907  addsq2nreurex  26947  2sqreultblem  26951  2sqreunnltblem  26954  chebbnd1lem3  26974  chebbnd1  26975  chtppilimlem1  26976  chtppilimlem2  26977  chtppilim  26978  chpchtlim  26982  vmadivsumb  26986  rplogsumlem2  26988  rpvmasumlem  26990  dchrmusumlema  26996  dchrmusum2  26997  dchrvmasumlem2  27001  dchrvmasumiflem1  27004  dchrisum0flblem1  27011  dchrisum0flblem2  27012  dchrisum0fno1  27014  rpvmasum2  27015  dchrisum0re  27016  dchrisum0lema  27017  dchrisum0lem1b  27018  dchrisum0lem1  27019  dchrisum0lem2a  27020  dchrisum0lem2  27021  logdivsum  27036  mulog2sumlem2  27038  2vmadivsumlem  27043  log2sumbnd  27047  selbergb  27052  selberg2b  27055  chpdifbndlem1  27056  selberg3lem1  27060  selberg3lem2  27061  selberg4lem1  27063  pntrmax  27067  pntrsumo1  27068  selbergsb  27078  pntrlog2bndlem3  27082  pntrlog2bndlem5  27084  pntpbnd1a  27088  pntpbnd2  27090  pntibndlem1  27092  pntibndlem3  27095  pntlemd  27097  pntlemc  27098  pntlemb  27100  pntlemr  27105  pntlemf  27108  pntlemk  27109  pntlemo  27110  pntlem3  27112  pntleml  27114  abvcxp  27118  ostth2lem1  27121  ostth1  27136  ostth2lem2  27137  ostth2lem3  27138  ostth2lem4  27139  ostth2  27140  ostth3  27141  ostth  27142  slotsinbpsd  27692  slotslnbpsd  27693  trgcgrg  27766  brbtwn2  28163  colinearalglem4  28167  ax5seglem2  28187  ax5seglem3  28189  axpaschlem  28198  axpasch  28199  axlowdimlem6  28205  axlowdimlem10  28209  axlowdimlem16  28215  axlowdim1  28217  axlowdim2  28218  axlowdim  28219  axcontlem2  28223  elntg2  28243  lfgrnloop  28385  lfuhgr1v0e  28511  usgrexmpldifpr  28515  usgrexmplef  28516  1loopgrvd2  28760  vdegp1bi  28794  lfgrwlkprop  28944  pthdlem1  29023  pthdlem2  29025  clwlkclwwlkf  29261  upgr4cycl4dv4e  29438  konigsberglem2  29506  konigsberglem3  29507  konigsberglem5  29509  frgrreg  29647  ex-dif  29676  ex-in  29678  ex-pss  29681  ex-res  29694  ex-fl  29700  nv1  29928  smcnlem  29950  ipidsq  29963  nmlno0lem  30046  norm-ii-i  30390  bcs2  30435  norm1  30502  nmopub2tALT  31162  nmfnleub2  31179  nmlnop0iALT  31248  unopbd  31268  nmopadjlem  31342  nmopcoadji  31354  pjnmopi  31401  pjbdlni  31402  hstle1  31479  hstle  31483  hstles  31484  stge1i  31491  stlesi  31494  staddi  31499  stadd3i  31501  strlem1  31503  strlem5  31508  jplem1  31521  cdj1i  31686  addltmulALT  31699  xlt2addrd  31971  pr01ssre  32030  dp2lt10  32050  dp2ltsuc  32052  dp2ltc  32053  dplti  32071  dpmul4  32080  cshw1s2  32124  xrsmulgzz  32179  resvbasOLD  32448  rearchi  32461  xrge0slmod  32463  prmidl0  32569  submateqlem1  32787  xrge0iifcnv  32913  xrge0iifcv  32914  xrge0iifiso  32915  xrge0iifhom  32917  zrhre  32999  indf  33013  indfval  33014  esumcst  33061  cntnevol  33226  omssubadd  33299  iwrdsplit  33386  dstfrvclim1  33476  coinfliprv  33481  ballotlem2  33487  ballotlem4  33497  ballotlemi1  33501  ballotlemic  33505  sgnclre  33538  sgnnbi  33544  sgnpbi  33545  sgnmulsgp  33549  plymulx0  33558  plymulx  33559  signswch  33572  signstf  33577  signsvfn  33593  itgexpif  33618  hgt750lemd  33660  logdivsqrle  33662  hgt750lem  33663  hgt750lem2  33664  hgt750leme  33670  tgoldbachgnn  33671  subfacp1lem1  34170  subfacp1lem5  34175  resconn  34237  iisconn  34243  iillysconn  34244  problem2  34651  problem3  34652  sinccvglem  34657  fz0n  34700  gg-iihalf2cn  35168  gg-reparphti  35172  dnibndlem12  35365  knoppcnlem4  35372  knoppndvlem13  35400  cnndvlem1  35413  irrdiff  36207  relowlpssretop  36245  sin2h  36478  cos2h  36479  tan2h  36480  poimirlem7  36495  poimirlem16  36504  poimirlem17  36505  poimirlem19  36507  poimirlem20  36508  poimirlem22  36510  poimirlem23  36511  poimirlem29  36517  poimirlem31  36519  itg2addnclem3  36541  asindmre  36571  dvasin  36572  dvacos  36573  dvreasin  36574  dvreacos  36575  fdc  36613  geomcau  36627  cntotbnd  36664  heiborlem8  36686  bfplem2  36691  bfp  36692  aks4d1p1p7  40939  2xp3dxp2ge1d  41022  factwoffsmonot  41023  1t1e1ALT  41176  re1m1e0m0  41270  sn-00idlem1  41271  sn-00idlem2  41272  remul02  41278  sn-0ne2  41279  reixi  41295  rei4  41296  remullid  41306  ipiiie0  41310  sn-0tie0  41312  sn-nnne0  41321  mulgt0b2d  41333  sn-0lt1  41335  sn-ltp1  41336  reneg1lt0  41337  sn-inelr  41338  rabren3dioph  41553  pellexlem5  41571  pellexlem6  41572  pell1qrgaplem  41611  pell14qrgap  41613  pellqrex  41617  pellfundre  41619  pellfundlb  41622  pellfund14gap  41625  jm2.17a  41699  acongeq  41722  jm2.23  41735  jm3.1lem2  41757  sqrtcval  42392  sqrtcval2  42393  resqrtval  42394  imsqrtval  42395  relexp01min  42464  mnringbasedOLD  42971  cvgdvgrat  43072  lhe4.4ex1a  43088  binomcxplemnotnn0  43115  isosctrlem1ALT  43695  supxrgelem  44047  xrlexaddrp  44062  infxr  44077  infleinflem2  44081  sumnnodd  44346  limsup10exlem  44488  limsup10ex  44489  dvnprodlem3  44664  stoweidlem1  44717  stoweidlem18  44734  stoweidlem19  44735  stoweidlem26  44742  stoweidlem34  44750  stoweidlem40  44756  stoweidlem41  44757  stoweidlem59  44775  stoweid  44779  stirlinglem10  44799  stirlinglem11  44800  dirkercncflem1  44819  fourierdlem16  44839  fourierdlem21  44844  fourierdlem22  44845  fourierdlem42  44865  fourierdlem68  44890  fourierdlem83  44905  fourierdlem103  44925  sqwvfourb  44945  fouriersw  44947  etransclem23  44973  salgencntex  45059  ovn0lem  45281  smfmullem3  45509  smfmullem4  45510  zm1nn  46010  m1mod0mod1  46037  fmtnosqrt  46207  perfectALTVlem2  46390  2exp340mod341  46401  8exp8mod9  46404  nfermltl8rev  46410  nnsum3primesprm  46458  nnsum4primesodd  46464  nnsum4primesoddALTV  46465  nnsum4primeseven  46468  nnsum4primesevenALTV  46469  tgblthelfgott  46483  tgoldbach  46485  rege1logbrege0  47244  rege1logbzge0  47245  blennnelnn  47262  dignnld  47289  nn0sumshdiglemA  47305  nn0sumshdiglem1  47307  rrx2xpref1o  47404  rrxlines  47419  eenglngeehlnmlem1  47423  eenglngeehlnmlem2  47424  line2ylem  47437  line2x  47440  icccldii  47551  io1ii  47553  sepfsepc  47560