Theorem 1re 10376

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 10330, 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 10341	. . 3 ⊢ 1 ≠ 0
2		ax-1cn 10330	. . . . 5 ⊢ 1 ∈ ℂ
3		cnre 10373	. . . . 5 ⊢ (1 ∈ ℂ → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)))
4	2, 3	ax-mp 5	. . . 4 ⊢ ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏))
5		neeq1 3031	. . . . . . . 8 ⊢ (1 = (𝑎 + (i · 𝑏)) → (1 ≠ 0 ↔ (𝑎 + (i · 𝑏)) ≠ 0))
6	5	biimpcd 241	. . . . . . 7 ⊢ (1 ≠ 0 → (1 = (𝑎 + (i · 𝑏)) → (𝑎 + (i · 𝑏)) ≠ 0))
7		0cn 10368	. . . . . . . 8 ⊢ 0 ∈ ℂ
8		cnre 10373	. . . . . . . 8 ⊢ (0 ∈ ℂ → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)))
9	7, 8	ax-mp 5	. . . . . . 7 ⊢ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑))
10		neeq2 3032	. . . . . . . . . 10 ⊢ (0 = (𝑐 + (i · 𝑑)) → ((𝑎 + (i · 𝑏)) ≠ 0 ↔ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
11	10	biimpcd 241	. . . . . . . . 9 ⊢ ((𝑎 + (i · 𝑏)) ≠ 0 → (0 = (𝑐 + (i · 𝑑)) → (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
12	11	reximdv 3197	. . . . . . . 8 ⊢ ((𝑎 + (i · 𝑏)) ≠ 0 → (∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)) → ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
13	12	reximdv 3197	. . . . . . 7 ⊢ ((𝑎 + (i · 𝑏)) ≠ 0 → (∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)) → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
14	6, 9, 13	syl6mpi 67	. . . . . 6 ⊢ (1 ≠ 0 → (1 = (𝑎 + (i · 𝑏)) → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
15	14	reximdv 3197	. . . . 5 ⊢ (1 ≠ 0 → (∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)) → ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
16	15	reximdv 3197	. . . 4 ⊢ (1 ≠ 0 → (∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)) → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
17	4, 16	mpi 20	. . 3 ⊢ (1 ≠ 0 → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)))
18		ioran 969	. . . . . . . . 9 ⊢ (¬ (𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑) ↔ (¬ 𝑎 ≠ 𝑐 ∧ ¬ 𝑏 ≠ 𝑑))
19		df-ne 2970	. . . . . . . . . . 11 ⊢ (𝑎 ≠ 𝑐 ↔ ¬ 𝑎 = 𝑐)
20	19	con2bii 349	. . . . . . . . . 10 ⊢ (𝑎 = 𝑐 ↔ ¬ 𝑎 ≠ 𝑐)
21		df-ne 2970	. . . . . . . . . . 11 ⊢ (𝑏 ≠ 𝑑 ↔ ¬ 𝑏 = 𝑑)
22	21	con2bii 349	. . . . . . . . . 10 ⊢ (𝑏 = 𝑑 ↔ ¬ 𝑏 ≠ 𝑑)
23	20, 22	anbi12i 620	. . . . . . . . 9 ⊢ ((𝑎 = 𝑐 ∧ 𝑏 = 𝑑) ↔ (¬ 𝑎 ≠ 𝑐 ∧ ¬ 𝑏 ≠ 𝑑))
24	18, 23	bitr4i 270	. . . . . . . 8 ⊢ (¬ (𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑) ↔ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑))
25		id 22	. . . . . . . . 9 ⊢ (𝑎 = 𝑐 → 𝑎 = 𝑐)
26		oveq2 6930	. . . . . . . . 9 ⊢ (𝑏 = 𝑑 → (i · 𝑏) = (i · 𝑑))
27	25, 26	oveqan12d 6941	. . . . . . . 8 ⊢ ((𝑎 = 𝑐 ∧ 𝑏 = 𝑑) → (𝑎 + (i · 𝑏)) = (𝑐 + (i · 𝑑)))
28	24, 27	sylbi 209	. . . . . . 7 ⊢ (¬ (𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑) → (𝑎 + (i · 𝑏)) = (𝑐 + (i · 𝑑)))
29	28	necon1ai 2996	. . . . . 6 ⊢ ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → (𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑))
30		neeq1 3031	. . . . . . . . . 10 ⊢ (𝑥 = 𝑎 → (𝑥 ≠ 𝑦 ↔ 𝑎 ≠ 𝑦))
31		neeq2 3032	. . . . . . . . . 10 ⊢ (𝑦 = 𝑐 → (𝑎 ≠ 𝑦 ↔ 𝑎 ≠ 𝑐))
32	30, 31	rspc2ev 3526	. . . . . . . . 9 ⊢ ((𝑎 ∈ ℝ ∧ 𝑐 ∈ ℝ ∧ 𝑎 ≠ 𝑐) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦)
33	32	3expia 1111	. . . . . . . 8 ⊢ ((𝑎 ∈ ℝ ∧ 𝑐 ∈ ℝ) → (𝑎 ≠ 𝑐 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
34	33	ad2ant2r 737	. . . . . . 7 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → (𝑎 ≠ 𝑐 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
35		neeq1 3031	. . . . . . . . . 10 ⊢ (𝑥 = 𝑏 → (𝑥 ≠ 𝑦 ↔ 𝑏 ≠ 𝑦))
36		neeq2 3032	. . . . . . . . . 10 ⊢ (𝑦 = 𝑑 → (𝑏 ≠ 𝑦 ↔ 𝑏 ≠ 𝑑))
37	35, 36	rspc2ev 3526	. . . . . . . . 9 ⊢ ((𝑏 ∈ ℝ ∧ 𝑑 ∈ ℝ ∧ 𝑏 ≠ 𝑑) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦)
38	37	3expia 1111	. . . . . . . 8 ⊢ ((𝑏 ∈ ℝ ∧ 𝑑 ∈ ℝ) → (𝑏 ≠ 𝑑 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
39	38	ad2ant2l 736	. . . . . . 7 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → (𝑏 ≠ 𝑑 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
40	34, 39	jaod 848	. . . . . 6 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → ((𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
41	29, 40	syl5 34	. . . . 5 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
42	41	rexlimdvva 3221	. . . 4 ⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
43	42	rexlimivv 3219	. . 3 ⊢ (∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦)
44	1, 17, 43	mp2b 10	. 2 ⊢ ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦
45		eqtr3 2801	. . . . . . . . 9 ⊢ ((𝑥 = 0 ∧ 𝑦 = 0) → 𝑥 = 𝑦)
46	45	ex 403	. . . . . . . 8 ⊢ (𝑥 = 0 → (𝑦 = 0 → 𝑥 = 𝑦))
47	46	necon3d 2990	. . . . . . 7 ⊢ (𝑥 = 0 → (𝑥 ≠ 𝑦 → 𝑦 ≠ 0))
48		neeq1 3031	. . . . . . . . 9 ⊢ (𝑧 = 𝑦 → (𝑧 ≠ 0 ↔ 𝑦 ≠ 0))
49	48	rspcev 3511	. . . . . . . 8 ⊢ ((𝑦 ∈ ℝ ∧ 𝑦 ≠ 0) → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)
50	49	expcom 404	. . . . . . 7 ⊢ (𝑦 ≠ 0 → (𝑦 ∈ ℝ → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
51	47, 50	syl6 35	. . . . . 6 ⊢ (𝑥 = 0 → (𝑥 ≠ 𝑦 → (𝑦 ∈ ℝ → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
52	51	com23 86	. . . . 5 ⊢ (𝑥 = 0 → (𝑦 ∈ ℝ → (𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
53	52	adantld 486	. . . 4 ⊢ (𝑥 = 0 → ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
54		neeq1 3031	. . . . . . . 8 ⊢ (𝑧 = 𝑥 → (𝑧 ≠ 0 ↔ 𝑥 ≠ 0))
55	54	rspcev 3511	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)
56	55	expcom 404	. . . . . 6 ⊢ (𝑥 ≠ 0 → (𝑥 ∈ ℝ → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
57	56	adantrd 487	. . . . 5 ⊢ (𝑥 ≠ 0 → ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
58	57	a1dd 50	. . . 4 ⊢ (𝑥 ≠ 0 → ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
59	53, 58	pm2.61ine 3053	. . 3 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
60	59	rexlimivv 3219	. 2 ⊢ (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)
61		ax-rrecex 10344	. . . 4 ⊢ ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → ∃𝑥 ∈ ℝ (𝑧 · 𝑥) = 1)
62		remulcl 10357	. . . . . . 7 ⊢ ((𝑧 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (𝑧 · 𝑥) ∈ ℝ)
63	62	adantlr 705	. . . . . 6 ⊢ (((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) ∧ 𝑥 ∈ ℝ) → (𝑧 · 𝑥) ∈ ℝ)
64		eleq1 2847	. . . . . 6 ⊢ ((𝑧 · 𝑥) = 1 → ((𝑧 · 𝑥) ∈ ℝ ↔ 1 ∈ ℝ))
65	63, 64	syl5ibcom 237	. . . . 5 ⊢ (((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) ∧ 𝑥 ∈ ℝ) → ((𝑧 · 𝑥) = 1 → 1 ∈ ℝ))
66	65	rexlimdva 3213	. . . 4 ⊢ ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → (∃𝑥 ∈ ℝ (𝑧 · 𝑥) = 1 → 1 ∈ ℝ))
67	61, 66	mpd 15	. . 3 ⊢ ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → 1 ∈ ℝ)
68	67	rexlimiva 3210	. 2 ⊢ (∃𝑧 ∈ ℝ 𝑧 ≠ 0 → 1 ∈ ℝ)
69	44, 60, 68	mp2b 10	1 ⊢ 1 ∈ ℝ

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 386   ∨ wo 836   = wceq 1601   ∈ wcel 2107   ≠ wne 2969  ∃wrex 3091  (class class class)co 6922  ℂcc 10270  ℝcr 10271  0cc0 10272  1c1 10273  ici 10274   + caddc 10275   · cmul 10277

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-1cn 10330  ax-icn 10331  ax-addcl 10332  ax-mulcl 10334  ax-mulrcl 10335  ax-i2m1 10340  ax-1ne0 10341  ax-rrecex 10344  ax-cnre 10345

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ne 2970  df-ral 3095  df-rex 3096  df-rab 3099  df-v 3400  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-nul 4142  df-if 4308  df-sn 4399  df-pr 4401  df-op 4405  df-uni 4672  df-br 4887  df-iota 6099  df-fv 6143  df-ov 6925

This theorem is referenced by:  1red  10377  0reOLD  10379  1xr  10436  dedekind  10539  peano2re  10549  mul02lem2  10553  addid1  10556  renegcl  10686  peano2rem  10690  0reALT  10720  0lt1  10897  0le1  10898  relin01  10899  1le1  11003  eqneg  11095  ltp1  11215  ltm1  11217  recgt0  11221  mulgt1  11236  ltmulgt11  11237  lemulge11  11239  reclt1  11272  recgt1  11273  recgt1i  11274  recp1lt1  11275  recreclt  11276  recgt0ii  11283  ledivp1i  11303  ltdivp1i  11304  inelr  11364  cju  11370  nnssre  11378  nnge1  11404  nngt1ne1  11405  nnle1eq1  11406  nngt0  11407  nnnlt1  11408  nnne0  11410  nnrecre  11417  nnrecgt0  11418  nnsub  11419  2re  11449  3re  11455  4re  11460  5re  11464  6re  11468  7re  11472  8re  11476  9re  11480  0le2  11484  2pos  11485  3pos  11487  4pos  11489  5pos  11491  6pos  11492  7pos  11493  8pos  11494  9pos  11495  neg1rr  11497  neg1lt0  11499  1lt2  11553  1lt3  11555  1lt4  11558  1lt5  11562  1lt6  11567  1lt7  11573  1lt8  11580  1lt9  11588  1ne2  11590  1le2  11591  1le3  11594  halflt1  11600  addltmul  11618  nnunb  11638  elnnnn0c  11689  nn0ge2m1nn  11711  elnnz1  11755  znnnlt1  11756  zltp1le  11779  zleltp1  11780  nn0lt2  11792  recnz  11804  gtndiv  11806  3halfnz  11808  10re  11864  1lt10  11986  eluzp1m1  12016  eluzp1p1  12018  eluz2b2  12068  zbtwnre  12093  rebtwnz  12094  1rp  12141  divlt1lt  12208  divle1le  12209  nnledivrp  12251  qbtwnxr  12343  xmulid1  12421  xmulm1  12423  x2times  12441  xrub  12454  elicc01  12604  1elunit  12606  divelunit  12631  lincmb01cmp  12632  unitssre  12636  0nelfz1  12677  fzpreddisj  12707  fznatpl1  12712  fztpval  12720  fraclt1  12922  fracle1  12923  flbi2  12937  fldiv4p1lem1div2  12955  fldiv4lem1div2  12957  fldiv  12978  modid  13014  1mod  13021  m1modnnsub1  13035  modm1p1mod0  13040  seqf1olem1  13158  reexpcl  13195  reexpclz  13198  expge0  13214  expge1  13215  expgt1  13216  bernneq  13309  bernneq2  13310  expnbnd  13312  expnlbnd  13313  expnlbnd2  13314  expmulnbnd  13315  discr1  13319  facwordi  13394  faclbnd3  13397  faclbnd4lem1  13398  faclbnd4lem4  13401  faclbnd6  13404  facavg  13406  hashv01gt1  13450  hashnn0n0nn  13495  hash1snb  13521  hashgt12el  13524  hashgt12el2  13525  hashfun  13538  hashge2el2dif  13576  brfi1indALT  13596  lsw0  13655  f1oun2prg  14068  cjexp  14297  re1  14301  im1  14302  rei  14303  imi  14304  sqrlem1  14390  sqrlem2  14391  sqrlem3  14392  sqrlem4  14393  sqrlem7  14396  resqrex  14398  sqrt1  14419  sqrt2gt1lt2  14422  sqrtm1  14423  abs1  14444  absrdbnd  14488  caubnd2  14504  mulcn2  14734  reccn2  14735  rlimno1  14792  o1fsum  14949  expcnv  15000  geolim  15005  geolim2  15006  georeclim  15007  geomulcvg  15011  geoisumr  15013  geoisum1c  15015  fprodge0  15126  fprodge1  15128  rerisefaccl  15150  refallfaccl  15151  ere  15221  ege2le3  15222  efgt1  15248  resin4p  15270  recos4p  15271  tanhbnd  15293  sinbnd  15312  cosbnd  15313  sinbnd2  15314  cosbnd2  15315  ef01bndlem  15316  sin01bnd  15317  cos01bnd  15318  cos1bnd  15319  cos2bnd  15320  sinltx  15321  sin01gt0  15322  cos01gt0  15323  sin02gt0  15324  sincos1sgn  15325  ene1  15342  rpnnen2lem2  15348  rpnnen2lem3  15349  rpnnen2lem4  15350  rpnnen2lem9  15355  rpnnen2lem12  15358  ruclem6  15368  ruclem11  15373  ruclem12  15374  3dvds  15459  n2dvds1OLD  15497  flodddiv4  15543  sadcadd  15586  isprm3  15801  sqnprm  15818  coprm  15827  phibndlem  15879  pythagtriplem3  15927  pcmpt  16000  fldivp1  16005  pockthi  16015  infpn2  16021  resslem  16329  basendxnmulrndx  16391  slotsbhcdif  16466  oppcbas  16763  rescbas  16874  rescabs  16878  odubas  17519  lt6abl  18682  srgbinomlem4  18930  abvneg  19226  abvtrivd  19232  rmodislmod  19323  0ringnnzr  19666  cnfldfun  20154  xrsmcmn  20165  xrsnsgrp  20178  gzrngunitlem  20207  gzrngunit  20208  rge0srg  20213  psgnodpmr  20331  remulg  20350  resubdrg  20351  thlbas  20439  matbas  20623  tuslem  22479  setsmsbas  22688  dscmet  22785  dscopn  22786  nrginvrcnlem  22903  idnghm  22955  tgioo  23007  blcvx  23009  iicmp  23097  iiconn  23098  iirev  23136  iihalf1  23138  iihalf2  23140  iihalf2cn  23141  elii1  23142  elii2  23143  iimulcl  23144  icopnfcnv  23149  icopnfhmeo  23150  iccpnfhmeo  23152  xrhmeo  23153  xrhmph  23154  evth  23166  xlebnum  23172  lebnumii  23173  htpycc  23187  reparphti  23204  pcoval1  23220  pco1  23222  pcoval2  23223  pcocn  23224  pcohtpylem  23226  pcopt  23229  pcopt2  23230  pcoass  23231  pcorevlem  23233  nmhmcn  23327  ncvs1  23364  ovolunlem1a  23700  vitalilem2  23813  vitalilem4  23815  vitalilem5  23816  vitali  23817  i1f1  23894  itg11  23895  itg2const  23944  dveflem  24179  dvlipcn  24194  dvcvx  24220  ply1remlem  24359  fta1blem  24365  vieta1lem2  24503  aalioulem3  24526  aalioulem5  24528  aaliou3lem2  24535  ulmbdd  24589  iblulm  24598  radcnvlem1  24604  dvradcnv  24612  abelthlem2  24623  abelthlem3  24624  abelthlem5  24626  abelthlem7  24629  abelth  24632  abelth2  24633  reeff1olem  24637  reeff1o  24638  sinhalfpilem  24653  tangtx  24695  sincos4thpi  24703  pige3  24707  coskpi  24710  recosf1o  24719  tanregt0  24723  efif1olem3  24728  efif1olem4  24729  loge  24770  logdivlti  24803  logcnlem4  24828  logf1o2  24833  dvlog2lem  24835  logtayl  24843  logccv  24846  recxpcl  24858  cxplea  24879  cxpcn3lem  24928  cxpaddlelem  24932  loglesqrt  24939  logblog  24970  ang180lem2  24988  angpined  25008  chordthmlem4  25013  acosrecl  25081  atancj  25088  atanlogaddlem  25091  atantan  25101  atans2  25109  ressatans  25112  leibpi  25121  log2le1  25129  birthdaylem3  25132  cxp2lim  25155  cxploglim  25156  cxploglim2  25157  divsqrtsumlem  25158  cvxcl  25163  scvxcvx  25164  jensenlem2  25166  amgmlem  25168  emcllem2  25175  emcllem4  25177  emcllem6  25179  emcllem7  25180  emre  25184  emgt0  25185  harmonicbnd3  25186  harmonicubnd  25188  harmonicbnd4  25189  zetacvg  25193  ftalem1  25251  ftalem2  25252  ftalem5  25255  issqf  25314  cht1  25343  chp1  25345  ppiltx  25355  mumullem2  25358  ppiublem1  25379  ppiub  25381  chtublem  25388  chtub  25389  logfacbnd3  25400  logexprlim  25402  perfectlem2  25407  dchrinv  25438  dchr1re  25440  efexple  25458  bposlem1  25461  bposlem2  25462  bposlem5  25465  bposlem8  25468  lgsdir2lem1  25502  lgsdir2lem5  25506  lgsdir  25509  lgsne0  25512  lgsabs1  25513  lgsdinn0  25522  gausslemma2dlem0i  25541  lgseisen  25556  m1lgs  25565  2lgslem3  25581  chebbnd1lem3  25612  chebbnd1  25613  chtppilimlem1  25614  chtppilimlem2  25615  chtppilim  25616  chpchtlim  25620  vmadivsumb  25624  rplogsumlem2  25626  rpvmasumlem  25628  dchrmusumlema  25634  dchrmusum2  25635  dchrvmasumlem2  25639  dchrvmasumiflem1  25642  dchrisum0flblem1  25649  dchrisum0flblem2  25650  dchrisum0fno1  25652  rpvmasum2  25653  dchrisum0re  25654  dchrisum0lema  25655  dchrisum0lem1b  25656  dchrisum0lem1  25657  dchrisum0lem2a  25658  dchrisum0lem2  25659  logdivsum  25674  mulog2sumlem2  25676  2vmadivsumlem  25681  log2sumbnd  25685  selbergb  25690  selberg2b  25693  chpdifbndlem1  25694  selberg3lem1  25698  selberg3lem2  25699  selberg4lem1  25701  pntrmax  25705  pntrsumo1  25706  selbergsb  25716  pntrlog2bndlem3  25720  pntrlog2bndlem5  25722  pntpbnd1a  25726  pntpbnd2  25728  pntibndlem1  25730  pntibndlem3  25733  pntlemd  25735  pntlemc  25736  pntlemb  25738  pntlemr  25743  pntlemf  25746  pntlemk  25747  pntlemo  25748  pntlem3  25750  pntleml  25752  pnt  25755  abvcxp  25756  ostth2lem1  25759  ostth1  25774  ostth2lem2  25775  ostth2lem3  25776  ostth2lem4  25777  ostth2  25778  ostth3  25779  ostth  25780  trgcgrg  25866  brbtwn2  26254  colinearalglem4  26258  ax5seglem2  26278  ax5seglem3  26280  axpaschlem  26289  axpasch  26290  axlowdimlem6  26296  axlowdimlem10  26300  axlowdimlem16  26306  axlowdim1  26308  axlowdim2  26309  axlowdim  26310  axcontlem2  26314  elntg2  26334  lfgrnloop  26473  lfuhgr1v0e  26601  usgrexmpldifpr  26605  usgrexmplef  26606  1loopgrvd2  26851  vdegp1bi  26885  lfgrwlkprop  27038  pthdlem1  27118  pthdlem2  27120  clwlkclwwlkfOLD  27392  clwlkclwwlkf  27396  upgr4cycl4dv4e  27588  konigsberglem2  27659  konigsberglem3  27660  konigsberglem5  27662  frgrreg  27826  ex-dif  27855  ex-in  27857  ex-pss  27860  ex-res  27873  ex-fl  27879  nv1  28102  smcnlem  28124  ipidsq  28137  nmlno0lem  28220  norm-ii-i  28566  bcs2  28611  norm1  28678  nmopub2tALT  29340  nmfnleub2  29357  nmlnop0iALT  29426  unopbd  29446  nmopadjlem  29520  nmopcoadji  29532  pjnmopi  29579  pjbdlni  29580  hstle1  29657  hstle  29661  hstles  29662  stge1i  29669  stlesi  29672  staddi  29677  stadd3i  29679  strlem1  29681  strlem5  29686  jplem1  29699  cdj1i  29864  addltmulALT  29877  xlt2addrd  30088  pr01ssre  30134  dp2lt10  30154  dp2ltsuc  30156  dp2ltc  30157  dplti  30175  dpmul4  30184  xrsmulgzz  30240  resvbas  30394  rearchi  30404  xrge0slmod  30406  submateqlem1  30471  xrge0iifcnv  30577  xrge0iifcv  30578  xrge0iifiso  30579  xrge0iifhom  30581  zrhre  30661  indf  30675  indfval  30676  esumcst  30723  cntnevol  30889  omssubadd  30960  iwrdsplit  31047  iwrdsplitOLD  31048  dstfrvclim1  31138  coinfliprv  31143  ballotlem2  31149  ballotlem4  31159  ballotlemi1  31163  ballotlemic  31167  sgnclre  31200  sgnnbi  31206  sgnpbi  31207  sgnmulsgp  31211  plymulx0  31224  plymulx  31225  signswch  31238  signstf  31243  signsvfn  31261  itgexpif  31286  hgt750lemd  31328  logdivsqrle  31330  hgt750lem  31331  hgt750lem2  31332  hgt750leme  31338  tgoldbachgnn  31339  subfacp1lem1  31760  subfacp1lem5  31765  resconn  31827  iisconn  31833  iillysconn  31834  problem2  32157  problem3  32158  sinccvglem  32163  fz0n  32210  dnibndlem12  33062  knoppcnlem4  33069  knoppndvlem13  33097  cnndvlem1  33110  relowlpssretop  33807  sin2h  34024  cos2h  34025  tan2h  34026  poimirlem7  34042  poimirlem16  34051  poimirlem17  34052  poimirlem19  34054  poimirlem20  34055  poimirlem22  34057  poimirlem23  34058  poimirlem29  34064  poimirlem31  34066  itg2addnclem3  34088  asindmre  34120  dvasin  34121  dvacos  34122  dvreasin  34123  dvreacos  34124  fdc  34165  geomcau  34179  cntotbnd  34219  heiborlem8  34241  bfplem2  34246  bfp  34247  1t1e1ALT  38142  rabren3dioph  38339  pellexlem5  38357  pellexlem6  38358  pell1qrgaplem  38397  pell14qrgap  38399  pellqrex  38403  pellfundre  38405  pellfundlb  38408  pellfund14gap  38411  jm2.17a  38486  acongeq  38509  jm2.23  38522  jm3.1lem2  38544  relexp01min  38962  cvgdvgrat  39468  lhe4.4ex1a  39484  binomcxplemnotnn0  39511  isosctrlem1ALT  40103  supxrgelem  40461  xrlexaddrp  40476  infxr  40491  infleinflem2  40495  sumnnodd  40770  limsup10exlem  40912  limsup10ex  40913  dvnprodlem3  41091  stoweidlem1  41145  stoweidlem18  41162  stoweidlem19  41163  stoweidlem26  41170  stoweidlem34  41178  stoweidlem40  41184  stoweidlem41  41185  stoweidlem59  41203  stoweid  41207  stirlinglem10  41227  stirlinglem11  41228  dirkercncflem1  41247  fourierdlem16  41267  fourierdlem21  41272  fourierdlem22  41273  fourierdlem42  41293  fourierdlem68  41318  fourierdlem83  41333  fourierdlem103  41353  sqwvfourb  41373  fouriersw  41375  etransclem23  41401  salgencntex  41485  ovn0lem  41706  smfmullem3  41927  smfmullem4  41928  zm1nn  42344  m1mod0mod1  42371  fmtnosqrt  42472  perfectALTVlem2  42656  nnsum3primesprm  42703  nnsum4primesodd  42709  nnsum4primesoddALTV  42710  nnsum4primeseven  42713  nnsum4primesevenALTV  42714  tgblthelfgott  42728  tgoldbach  42730  rege1logbrege0  43367  rege1logbzge0  43368  blennnelnn  43385  dignnld  43412  nn0sumshdiglemA  43428  nn0sumshdiglem1  43430  rrx2xpref1o  43454  rrxlines  43469  eenglngeehlnmlem1  43473  eenglngeehlnmlem2  43474  line2ylem  43487  line2x  43490