Theorem 1re 11261

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 11213, 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 11224	. . 3 ⊢ 1 ≠ 0
2		ax-1cn 11213	. . . . 5 ⊢ 1 ∈ ℂ
3		cnre 11258	. . . . 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 249	. . . . . . 7 ⊢ (1 ≠ 0 → (1 = (𝑎 + (i · 𝑏)) → (𝑎 + (i · 𝑏)) ≠ 0))
7		0cn 11253	. . . . . . . 8 ⊢ 0 ∈ ℂ
8		cnre 11258	. . . . . . . 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 249	. . . . . . . . 9 ⊢ ((𝑎 + (i · 𝑏)) ≠ 0 → (0 = (𝑐 + (i · 𝑑)) → (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
12	11	reximdv 3170	. . . . . . . 8 ⊢ ((𝑎 + (i · 𝑏)) ≠ 0 → (∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)) → ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
13	12	reximdv 3170	. . . . . . 7 ⊢ ((𝑎 + (i · 𝑏)) ≠ 0 → (∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)) → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
14	6, 9, 13	syl6mpi 67	. . . . . 6 ⊢ (1 ≠ 0 → (1 = (𝑎 + (i · 𝑏)) → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
15	14	reximdv 3170	. . . . 5 ⊢ (1 ≠ 0 → (∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)) → ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
16	15	reximdv 3170	. . . 4 ⊢ (1 ≠ 0 → (∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)) → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
17	4, 16	mpi 20	. . 3 ⊢ (1 ≠ 0 → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)))
18		ioran 986	. . . . . . . . 9 ⊢ (¬ (𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑) ↔ (¬ 𝑎 ≠ 𝑐 ∧ ¬ 𝑏 ≠ 𝑑))
19		df-ne 2941	. . . . . . . . . . 11 ⊢ (𝑎 ≠ 𝑐 ↔ ¬ 𝑎 = 𝑐)
20	19	con2bii 357	. . . . . . . . . 10 ⊢ (𝑎 = 𝑐 ↔ ¬ 𝑎 ≠ 𝑐)
21		df-ne 2941	. . . . . . . . . . 11 ⊢ (𝑏 ≠ 𝑑 ↔ ¬ 𝑏 = 𝑑)
22	21	con2bii 357	. . . . . . . . . 10 ⊢ (𝑏 = 𝑑 ↔ ¬ 𝑏 ≠ 𝑑)
23	20, 22	anbi12i 628	. . . . . . . . 9 ⊢ ((𝑎 = 𝑐 ∧ 𝑏 = 𝑑) ↔ (¬ 𝑎 ≠ 𝑐 ∧ ¬ 𝑏 ≠ 𝑑))
24	18, 23	bitr4i 278	. . . . . . . 8 ⊢ (¬ (𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑) ↔ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑))
25		id 22	. . . . . . . . 9 ⊢ (𝑎 = 𝑐 → 𝑎 = 𝑐)
26		oveq2 7439	. . . . . . . . 9 ⊢ (𝑏 = 𝑑 → (i · 𝑏) = (i · 𝑑))
27	25, 26	oveqan12d 7450	. . . . . . . 8 ⊢ ((𝑎 = 𝑐 ∧ 𝑏 = 𝑑) → (𝑎 + (i · 𝑏)) = (𝑐 + (i · 𝑑)))
28	24, 27	sylbi 217	. . . . . . 7 ⊢ (¬ (𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑) → (𝑎 + (i · 𝑏)) = (𝑐 + (i · 𝑑)))
29	28	necon1ai 2968	. . . . . 6 ⊢ ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → (𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑))
30		neeq1 3003	. . . . . . . . . 10 ⊢ (𝑥 = 𝑎 → (𝑥 ≠ 𝑦 ↔ 𝑎 ≠ 𝑦))
31		neeq2 3004	. . . . . . . . . 10 ⊢ (𝑦 = 𝑐 → (𝑎 ≠ 𝑦 ↔ 𝑎 ≠ 𝑐))
32	30, 31	rspc2ev 3635	. . . . . . . . 9 ⊢ ((𝑎 ∈ ℝ ∧ 𝑐 ∈ ℝ ∧ 𝑎 ≠ 𝑐) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦)
33	32	3expia 1122	. . . . . . . 8 ⊢ ((𝑎 ∈ ℝ ∧ 𝑐 ∈ ℝ) → (𝑎 ≠ 𝑐 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
34	33	ad2ant2r 747	. . . . . . 7 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → (𝑎 ≠ 𝑐 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
35		neeq1 3003	. . . . . . . . . 10 ⊢ (𝑥 = 𝑏 → (𝑥 ≠ 𝑦 ↔ 𝑏 ≠ 𝑦))
36		neeq2 3004	. . . . . . . . . 10 ⊢ (𝑦 = 𝑑 → (𝑏 ≠ 𝑦 ↔ 𝑏 ≠ 𝑑))
37	35, 36	rspc2ev 3635	. . . . . . . . 9 ⊢ ((𝑏 ∈ ℝ ∧ 𝑑 ∈ ℝ ∧ 𝑏 ≠ 𝑑) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦)
38	37	3expia 1122	. . . . . . . 8 ⊢ ((𝑏 ∈ ℝ ∧ 𝑑 ∈ ℝ) → (𝑏 ≠ 𝑑 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
39	38	ad2ant2l 746	. . . . . . 7 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → (𝑏 ≠ 𝑑 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
40	34, 39	jaod 860	. . . . . 6 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → ((𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
41	29, 40	syl5 34	. . . . 5 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
42	41	rexlimdvva 3213	. . . 4 ⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
43	42	rexlimivv 3201	. . 3 ⊢ (∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦)
44	1, 17, 43	mp2b 10	. 2 ⊢ ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦
45		eqtr3 2763	. . . . . . . . 9 ⊢ ((𝑥 = 0 ∧ 𝑦 = 0) → 𝑥 = 𝑦)
46	45	ex 412	. . . . . . . 8 ⊢ (𝑥 = 0 → (𝑦 = 0 → 𝑥 = 𝑦))
47	46	necon3d 2961	. . . . . . 7 ⊢ (𝑥 = 0 → (𝑥 ≠ 𝑦 → 𝑦 ≠ 0))
48		neeq1 3003	. . . . . . . . 9 ⊢ (𝑧 = 𝑦 → (𝑧 ≠ 0 ↔ 𝑦 ≠ 0))
49	48	rspcev 3622	. . . . . . . 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 3003	. . . . . . . 8 ⊢ (𝑧 = 𝑥 → (𝑧 ≠ 0 ↔ 𝑥 ≠ 0))
55	54	rspcev 3622	. . . . . . 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 3025	. . 3 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
60	59	rexlimivv 3201	. 2 ⊢ (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)
61		ax-rrecex 11227	. . . 4 ⊢ ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → ∃𝑥 ∈ ℝ (𝑧 · 𝑥) = 1)
62		remulcl 11240	. . . . . . 7 ⊢ ((𝑧 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (𝑧 · 𝑥) ∈ ℝ)
63	62	adantlr 715	. . . . . 6 ⊢ (((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) ∧ 𝑥 ∈ ℝ) → (𝑧 · 𝑥) ∈ ℝ)
64		eleq1 2829	. . . . . 6 ⊢ ((𝑧 · 𝑥) = 1 → ((𝑧 · 𝑥) ∈ ℝ ↔ 1 ∈ ℝ))
65	63, 64	syl5ibcom 245	. . . . 5 ⊢ (((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) ∧ 𝑥 ∈ ℝ) → ((𝑧 · 𝑥) = 1 → 1 ∈ ℝ))
66	65	rexlimdva 3155	. . . 4 ⊢ ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → (∃𝑥 ∈ ℝ (𝑧 · 𝑥) = 1 → 1 ∈ ℝ))
67	61, 66	mpd 15	. . 3 ⊢ ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → 1 ∈ ℝ)
68	67	rexlimiva 3147	. 2 ⊢ (∃𝑧 ∈ ℝ 𝑧 ≠ 0 → 1 ∈ ℝ)
69	44, 60, 68	mp2b 10	1 ⊢ 1 ∈ ℝ

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∨ wo 848   = wceq 1540   ∈ wcel 2108   ≠ wne 2940  ∃wrex 3070  (class class class)co 7431  ℂcc 11153  ℝcr 11154  0cc0 11155  1c1 11156  ici 11157   + caddc 11158   · cmul 11160

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 2708  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-mulcl 11217  ax-mulrcl 11218  ax-i2m1 11223  ax-1ne0 11224  ax-rrecex 11227  ax-cnre 11228

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-iota 6514  df-fv 6569  df-ov 7434

This theorem is referenced by:  1red  11262  1xr  11320  dedekind  11424  peano2re  11434  mul02lem2  11438  addrid  11441  renegcl  11572  peano2rem  11576  0reALT  11606  0lt1  11785  0le1  11786  relin01  11787  1le1  11891  eqneg  11987  ltp1  12107  ltm1  12109  recgt0  12113  mulgt1OLD  12126  ltmulgt11  12127  lemulge11  12130  reclt1  12163  recgt1  12164  recgt1i  12165  recp1lt1  12166  recreclt  12167  recgt0ii  12174  ledivp1i  12193  ltdivp1i  12194  inelr  12256  cju  12262  nnssre  12270  nnge1  12294  nngt1ne1  12295  nnle1eq1  12296  nngt0  12297  nnnlt1  12298  nnne0  12300  nnrecre  12308  nnrecgt0  12309  nnsub  12310  2re  12340  3re  12346  4re  12350  5re  12353  6re  12356  7re  12359  8re  12362  9re  12365  0le2  12368  2pos  12369  3pos  12371  4pos  12373  5pos  12375  6pos  12376  7pos  12377  8pos  12378  9pos  12379  neg1rr  12381  neg1lt0  12383  1lt2  12437  1lt3  12439  1lt4  12442  1lt5  12446  1lt6  12451  1lt7  12457  1lt8  12464  1lt9  12472  1ne2  12474  1le2  12475  1le3  12478  halflt1  12484  addltmul  12502  nnunb  12522  elnnnn0c  12571  nn0ge2m1nn  12596  elnnz1  12643  znnnlt1  12644  zltp1le  12667  zleltp1  12668  nn0lt2  12681  recnz  12693  gtndiv  12695  3halfnz  12697  10re  12752  1lt10  12872  eluzp1m1  12904  eluzp1p1  12906  eluz2b2  12963  zbtwnre  12988  rebtwnz  12989  1rp  13038  divlt1lt  13104  divle1le  13105  nnledivrp  13147  qbtwnxr  13242  xmulrid  13321  xmulm1  13323  x2times  13341  xrub  13354  elicc01  13506  1elunit  13510  divelunit  13534  lincmb01cmp  13535  unitssre  13539  0nelfz1  13583  fzpreddisj  13613  fznatpl1  13618  fztpval  13626  fraclt1  13842  fracle1  13843  flbi2  13857  fldiv4p1lem1div2  13875  fldiv4lem1div2  13877  fldiv  13900  modid  13936  1mod  13943  m1modnnsub1  13958  modm1p1mod0  13963  seqf1olem1  14082  reexpcl  14119  reexpclz  14123  expge0  14139  expge1  14140  expgt1  14141  bernneq  14268  bernneq2  14269  expnbnd  14271  expnlbnd  14272  expnlbnd2  14273  expmulnbnd  14274  discr1  14278  facwordi  14328  faclbnd3  14331  faclbnd4lem1  14332  faclbnd4lem4  14335  faclbnd6  14338  facavg  14340  hashv01gt1  14384  hashnn0n0nn  14430  hashunsnggt  14433  hash1snb  14458  hashgt12el  14461  hashgt12el2  14462  hashfun  14476  hashge2el2dif  14519  tpf1ofv2  14537  lsw0  14603  f1oun2prg  14956  cjexp  15189  re1  15193  im1  15194  rei  15195  imi  15196  01sqrexlem1  15281  01sqrexlem2  15282  01sqrexlem3  15283  01sqrexlem4  15284  01sqrexlem7  15287  resqrex  15289  sqrt1  15310  sqrt2gt1lt2  15313  sqrtm1  15314  abs1  15336  absrdbnd  15380  caubnd2  15396  mulcn2  15632  reccn2  15633  rlimno1  15690  o1fsum  15849  expcnv  15900  geolim  15906  geolim2  15907  georeclim  15908  geomulcvg  15912  geoisumr  15914  geoisum1c  15916  fprodge0  16029  fprodge1  16031  rerisefaccl  16053  refallfaccl  16054  ere  16125  ege2le3  16126  efgt1  16152  resin4p  16174  recos4p  16175  tanhbnd  16197  sinbnd  16216  cosbnd  16217  sinbnd2  16218  cosbnd2  16219  ef01bndlem  16220  sin01bnd  16221  cos01bnd  16222  cos1bnd  16223  cos2bnd  16224  sinltx  16225  sin01gt0  16226  cos01gt0  16227  sin02gt0  16228  sincos1sgn  16229  ene1  16246  rpnnen2lem2  16251  rpnnen2lem3  16252  rpnnen2lem4  16253  rpnnen2lem9  16258  rpnnen2lem12  16261  ruclem6  16271  ruclem11  16276  ruclem12  16277  3dvds  16368  flodddiv4  16452  sadcadd  16495  isprm3  16720  sqnprm  16739  coprm  16748  phibndlem  16807  pythagtriplem3  16856  pcmpt  16930  fldivp1  16935  pockthi  16945  infpn2  16951  resslemOLD  17288  basendxnmulrndx  17339  basendxnmulrndxOLD  17340  starvndxnbasendx  17348  scandxnbasendx  17360  vscandxnbasendx  17365  ipndxnbasendx  17376  basendxnocndx  17427  slotsbhcdif  17459  slotsbhcdifOLD  17460  rescabsOLD  17878  odubasOLD  18337  symgvalstructOLD  19415  lt6abl  19913  srgbinomlem4  20226  0ringnnzr  20525  abvneg  20827  abvtrivd  20833  cnfldfunALTOLDOLD  21393  xrsmcmn  21404  xrsnsgrp  21420  gzrngunitlem  21450  gzrngunit  21451  rge0srg  21456  psgnodpmr  21608  remulg  21625  resubdrg  21626  thlbasOLD  21715  psdmvr  22173  tuslemOLD  24276  setsmsbasOLD  24486  dscmet  24585  dscopn  24586  nrginvrcnlem  24712  idnghm  24764  tgioo  24817  blcvx  24819  iicmp  24912  iiconn  24913  iirev  24956  iihalf1  24958  iihalf2  24961  iihalf2cnOLD  24963  elii1  24964  elii2  24965  iimulcl  24966  icopnfcnv  24973  icopnfhmeo  24974  iccpnfhmeo  24976  xrhmeo  24977  xrhmph  24978  evth  24991  xlebnum  24997  htpycc  25012  reparphti  25029  reparphtiOLD  25030  pcoval1  25046  pco1  25048  pcoval2  25049  pcocn  25050  pcohtpylem  25052  pcopt  25055  pcopt2  25056  pcoass  25057  pcorevlem  25059  nmhmcn  25153  ncvs1  25191  ovolunlem1a  25531  vitalilem2  25644  vitalilem4  25646  vitalilem5  25647  vitali  25648  i1f1  25725  itg11  25726  itg2const  25775  dveflem  26017  dvlipcn  26033  dvcvx  26059  ply1remlem  26204  fta1blem  26210  vieta1lem2  26353  aalioulem3  26376  aalioulem5  26378  aaliou3lem2  26385  ulmbdd  26441  iblulm  26450  radcnvlem1  26456  dvradcnv  26464  abelthlem2  26476  abelthlem3  26477  abelthlem5  26479  abelthlem7  26482  abelth  26485  abelth2  26486  reeff1olem  26490  reeff1o  26491  sinhalfpilem  26505  tangtx  26547  sincos4thpi  26555  pige3ALT  26562  coskpi  26565  cos0pilt1  26574  recosf1o  26577  tanregt0  26581  efif1olem3  26586  efif1olem4  26587  loge  26628  logdivlti  26662  logcnlem4  26687  logf1o2  26692  logtayl  26702  logccv  26705  recxpcl  26717  cxplea  26738  cxpcn3lem  26790  cxpaddlelem  26794  loglesqrt  26804  ang180lem2  26853  angpined  26873  acosrecl  26946  atancj  26953  atanlogaddlem  26956  atantan  26966  atans2  26974  ressatans  26977  leibpi  26985  log2le1  26993  birthdaylem3  26996  cxp2lim  27020  cxploglim  27021  cxploglim2  27022  divsqrtsumlem  27023  cvxcl  27028  scvxcvx  27029  jensenlem2  27031  amgmlem  27033  emcllem2  27040  emcllem4  27042  emcllem6  27044  emcllem7  27045  emre  27049  emgt0  27050  harmonicbnd3  27051  harmonicubnd  27053  harmonicbnd4  27054  zetacvg  27058  ftalem1  27116  ftalem2  27117  ftalem5  27120  issqf  27179  cht1  27208  chp1  27210  ppiltx  27220  mumullem2  27223  ppiublem1  27246  ppiub  27248  chtublem  27255  chtub  27256  logfacbnd3  27267  logexprlim  27269  perfectlem2  27274  dchrinv  27305  dchr1re  27307  efexple  27325  bposlem1  27328  bposlem2  27329  bposlem5  27332  bposlem8  27335  lgsdir2lem1  27369  lgsdir2lem5  27373  lgsdir  27376  lgsne0  27379  lgsabs1  27380  lgsdinn0  27389  gausslemma2dlem0i  27408  lgseisen  27423  m1lgs  27432  2lgslem3  27448  addsq2nreurex  27488  2sqreultblem  27492  2sqreunnltblem  27495  chebbnd1lem3  27515  chebbnd1  27516  chtppilimlem1  27517  chtppilimlem2  27518  chtppilim  27519  chpchtlim  27523  vmadivsumb  27527  rplogsumlem2  27529  rpvmasumlem  27531  dchrmusumlema  27537  dchrmusum2  27538  dchrvmasumlem2  27542  dchrvmasumiflem1  27545  dchrisum0flblem1  27552  dchrisum0flblem2  27553  dchrisum0fno1  27555  rpvmasum2  27556  dchrisum0re  27557  dchrisum0lema  27558  dchrisum0lem1b  27559  dchrisum0lem1  27560  dchrisum0lem2a  27561  dchrisum0lem2  27562  logdivsum  27577  mulog2sumlem2  27579  2vmadivsumlem  27584  log2sumbnd  27588  selbergb  27593  selberg2b  27596  chpdifbndlem1  27597  selberg3lem1  27601  selberg3lem2  27602  selberg4lem1  27604  pntrmax  27608  pntrsumo1  27609  selbergsb  27619  pntrlog2bndlem3  27623  pntrlog2bndlem5  27625  pntpbnd1a  27629  pntpbnd2  27631  pntibndlem1  27633  pntibndlem3  27636  pntlemd  27638  pntlemc  27639  pntlemb  27641  pntlemr  27646  pntlemf  27649  pntlemk  27650  pntlemo  27651  pntlem3  27653  pntleml  27655  abvcxp  27659  ostth2lem1  27662  ostth1  27677  ostth2lem2  27678  ostth2lem3  27679  ostth2lem4  27680  ostth2  27681  ostth3  27682  ostth  27683  slotsinbpsd  28449  slotslnbpsd  28450  trgcgrg  28523  brbtwn2  28920  colinearalglem4  28924  ax5seglem2  28944  ax5seglem3  28946  axpaschlem  28955  axpasch  28956  axlowdimlem6  28962  axlowdimlem10  28966  axlowdimlem16  28972  axlowdim1  28974  axlowdim2  28975  axlowdim  28976  axcontlem2  28980  elntg2  29000  lfgrnloop  29142  lfuhgr1v0e  29271  usgrexmpldifpr  29275  usgrexmplef  29276  1loopgrvd2  29521  vdegp1bi  29555  lfgrwlkprop  29705  pthdlem1  29786  pthdlem2  29788  clwlkclwwlkf  30027  upgr4cycl4dv4e  30204  konigsberglem2  30272  konigsberglem3  30273  konigsberglem5  30275  frgrreg  30413  ex-dif  30442  ex-in  30444  ex-pss  30447  ex-res  30460  ex-fl  30466  nv1  30694  smcnlem  30716  ipidsq  30729  nmlno0lem  30812  norm-ii-i  31156  bcs2  31201  norm1  31268  nmopub2tALT  31928  nmfnleub2  31945  nmlnop0iALT  32014  unopbd  32034  nmopadjlem  32108  nmopcoadji  32120  pjnmopi  32167  pjbdlni  32168  hstle1  32245  hstle  32249  hstles  32250  stge1i  32257  stlesi  32260  staddi  32265  stadd3i  32267  strlem1  32269  strlem5  32274  jplem1  32287  cdj1i  32452  addltmulALT  32465  xlt2addrd  32762  pr01ssre  32826  indf  32840  indfval  32841  dp2lt10  32866  dp2ltsuc  32868  dp2ltc  32869  dplti  32887  dpmul4  32896  cshw1s2  32945  xrsmulgzz  33011  resvbasOLD  33360  rearchi  33374  xrge0slmod  33376  prmidl0  33478  evl1deg3  33603  constrconj  33786  2sqr3minply  33791  submateqlem1  33806  xrge0iifcnv  33932  xrge0iifcv  33933  xrge0iifiso  33934  xrge0iifhom  33936  zrhre  34020  esumcst  34064  cntnevol  34229  omssubadd  34302  iwrdsplit  34389  dstfrvclim1  34480  coinfliprv  34485  ballotlem2  34491  ballotlem4  34501  ballotlemi1  34505  ballotlemic  34509  sgnclre  34542  sgnnbi  34548  sgnpbi  34549  sgnmulsgp  34553  plymulx0  34562  plymulx  34563  signswch  34576  signstf  34581  signsvfn  34597  itgexpif  34621  hgt750lemd  34663  logdivsqrle  34665  hgt750lem  34666  hgt750lem2  34667  hgt750leme  34673  tgoldbachgnn  34674  subfacp1lem1  35184  subfacp1lem5  35189  resconn  35251  iisconn  35257  iillysconn  35258  problem2  35671  problem3  35672  sinccvglem  35677  fz0n  35731  dnibndlem12  36490  knoppcnlem4  36497  knoppndvlem13  36525  cnndvlem1  36538  irrdiff  37327  relowlpssretop  37365  sin2h  37617  cos2h  37618  tan2h  37619  poimirlem7  37634  poimirlem16  37643  poimirlem17  37644  poimirlem19  37646  poimirlem20  37647  poimirlem22  37649  poimirlem23  37650  poimirlem29  37656  poimirlem31  37658  itg2addnclem3  37680  asindmre  37710  dvasin  37711  dvacos  37712  dvreasin  37713  dvreacos  37714  fdc  37752  geomcau  37766  cntotbnd  37803  heiborlem8  37825  bfplem2  37830  bfp  37831  aks4d1p1p7  42075  2xp3dxp2ge1d  42242  factwoffsmonot  42243  1t1e1ALT  42296  ine1  42349  re1m1e0m0  42427  sn-00idlem1  42428  sn-00idlem2  42429  remul02  42435  sn-0ne2  42436  reixi  42452  rei4  42453  remullid  42463  ipiiie0  42467  sn-0tie0  42469  sn-nnne0  42478  mulgt0b2d  42490  sn-0lt1  42493  sn-ltp1  42494  reneg1lt0  42496  sn-inelr  42497  rabren3dioph  42826  pellexlem5  42844  pellexlem6  42845  pell1qrgaplem  42884  pell14qrgap  42886  pellqrex  42890  pellfundre  42892  pellfundlb  42895  pellfund14gap  42898  jm2.17a  42972  acongeq  42995  jm2.23  43008  jm3.1lem2  43030  sqrtcval  43654  sqrtcval2  43655  resqrtval  43656  imsqrtval  43657  relexp01min  43726  mnringbasedOLD  44231  cvgdvgrat  44332  lhe4.4ex1a  44348  binomcxplemnotnn0  44375  isosctrlem1ALT  44954  supxrgelem  45348  xrlexaddrp  45363  infxr  45378  infleinflem2  45382  sumnnodd  45645  limsup10exlem  45787  limsup10ex  45788  dvnprodlem3  45963  stoweidlem1  46016  stoweidlem18  46033  stoweidlem19  46034  stoweidlem26  46041  stoweidlem34  46049  stoweidlem40  46055  stoweidlem41  46056  stoweidlem59  46074  stoweid  46078  stirlinglem10  46098  stirlinglem11  46099  dirkercncflem1  46118  fourierdlem16  46138  fourierdlem21  46143  fourierdlem22  46144  fourierdlem42  46164  fourierdlem68  46189  fourierdlem83  46204  fourierdlem103  46224  sqwvfourb  46244  fouriersw  46246  etransclem23  46272  salgencntex  46358  ovn0lem  46580  smfmullem3  46808  smfmullem4  46809  zm1nn  47314  m1mod0mod1  47356  fmtnosqrt  47526  perfectALTVlem2  47709  2exp340mod341  47720  8exp8mod9  47723  nfermltl8rev  47729  nnsum3primesprm  47777  nnsum4primesodd  47783  nnsum4primesoddALTV  47784  nnsum4primeseven  47787  nnsum4primesevenALTV  47788  tgblthelfgott  47802  tgoldbach  47804  usgrexmpl1lem  47980  usgrexmpl2lem  47985  usgrexmpl2nb1  47991  usgrexmpl2nb3  47993  usgrexmpl2nb4  47994  usgrexmpl2nb5  47995  usgrexmpl2trifr  47996  gpg3kgrtriexlem3  48041  rege1logbrege0  48479  rege1logbzge0  48480  blennnelnn  48497  dignnld  48524  nn0sumshdiglemA  48540  nn0sumshdiglem1  48542  rrx2xpref1o  48639  rrxlines  48654  eenglngeehlnmlem1  48658  eenglngeehlnmlem2  48659  line2ylem  48672  line2x  48675  icccldii  48816  io1ii  48818  sepfsepc  48825