Theorem 1re 11271

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 11223, 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 11234	. . 3 ⊢ 1 ≠ 0
2		ax-1cn 11223	. . . . 5 ⊢ 1 ∈ ℂ
3		cnre 11268	. . . . 5 ⊢ (1 ∈ ℂ → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)))
4	2, 3	ax-mp 5	. . . 4 ⊢ ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏))
5		neeq1 2996	. . . . . . . 8 ⊢ (1 = (𝑎 + (i · 𝑏)) → (1 ≠ 0 ↔ (𝑎 + (i · 𝑏)) ≠ 0))
6	5	biimpcd 248	. . . . . . 7 ⊢ (1 ≠ 0 → (1 = (𝑎 + (i · 𝑏)) → (𝑎 + (i · 𝑏)) ≠ 0))
7		0cn 11263	. . . . . . . 8 ⊢ 0 ∈ ℂ
8		cnre 11268	. . . . . . . 8 ⊢ (0 ∈ ℂ → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)))
9	7, 8	ax-mp 5	. . . . . . 7 ⊢ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑))
10		neeq2 2997	. . . . . . . . . 10 ⊢ (0 = (𝑐 + (i · 𝑑)) → ((𝑎 + (i · 𝑏)) ≠ 0 ↔ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
11	10	biimpcd 248	. . . . . . . . 9 ⊢ ((𝑎 + (i · 𝑏)) ≠ 0 → (0 = (𝑐 + (i · 𝑑)) → (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
12	11	reximdv 3163	. . . . . . . 8 ⊢ ((𝑎 + (i · 𝑏)) ≠ 0 → (∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)) → ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
13	12	reximdv 3163	. . . . . . 7 ⊢ ((𝑎 + (i · 𝑏)) ≠ 0 → (∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)) → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
14	6, 9, 13	syl6mpi 67	. . . . . 6 ⊢ (1 ≠ 0 → (1 = (𝑎 + (i · 𝑏)) → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
15	14	reximdv 3163	. . . . 5 ⊢ (1 ≠ 0 → (∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)) → ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
16	15	reximdv 3163	. . . 4 ⊢ (1 ≠ 0 → (∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)) → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
17	4, 16	mpi 20	. . 3 ⊢ (1 ≠ 0 → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)))
18		ioran 981	. . . . . . . . 9 ⊢ (¬ (𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑) ↔ (¬ 𝑎 ≠ 𝑐 ∧ ¬ 𝑏 ≠ 𝑑))
19		df-ne 2934	. . . . . . . . . . 11 ⊢ (𝑎 ≠ 𝑐 ↔ ¬ 𝑎 = 𝑐)
20	19	con2bii 356	. . . . . . . . . 10 ⊢ (𝑎 = 𝑐 ↔ ¬ 𝑎 ≠ 𝑐)
21		df-ne 2934	. . . . . . . . . . 11 ⊢ (𝑏 ≠ 𝑑 ↔ ¬ 𝑏 = 𝑑)
22	21	con2bii 356	. . . . . . . . . 10 ⊢ (𝑏 = 𝑑 ↔ ¬ 𝑏 ≠ 𝑑)
23	20, 22	anbi12i 626	. . . . . . . . 9 ⊢ ((𝑎 = 𝑐 ∧ 𝑏 = 𝑑) ↔ (¬ 𝑎 ≠ 𝑐 ∧ ¬ 𝑏 ≠ 𝑑))
24	18, 23	bitr4i 277	. . . . . . . 8 ⊢ (¬ (𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑) ↔ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑))
25		id 22	. . . . . . . . 9 ⊢ (𝑎 = 𝑐 → 𝑎 = 𝑐)
26		oveq2 7438	. . . . . . . . 9 ⊢ (𝑏 = 𝑑 → (i · 𝑏) = (i · 𝑑))
27	25, 26	oveqan12d 7449	. . . . . . . 8 ⊢ ((𝑎 = 𝑐 ∧ 𝑏 = 𝑑) → (𝑎 + (i · 𝑏)) = (𝑐 + (i · 𝑑)))
28	24, 27	sylbi 216	. . . . . . 7 ⊢ (¬ (𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑) → (𝑎 + (i · 𝑏)) = (𝑐 + (i · 𝑑)))
29	28	necon1ai 2961	. . . . . 6 ⊢ ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → (𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑))
30		neeq1 2996	. . . . . . . . . 10 ⊢ (𝑥 = 𝑎 → (𝑥 ≠ 𝑦 ↔ 𝑎 ≠ 𝑦))
31		neeq2 2997	. . . . . . . . . 10 ⊢ (𝑦 = 𝑐 → (𝑎 ≠ 𝑦 ↔ 𝑎 ≠ 𝑐))
32	30, 31	rspc2ev 3633	. . . . . . . . 9 ⊢ ((𝑎 ∈ ℝ ∧ 𝑐 ∈ ℝ ∧ 𝑎 ≠ 𝑐) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦)
33	32	3expia 1118	. . . . . . . 8 ⊢ ((𝑎 ∈ ℝ ∧ 𝑐 ∈ ℝ) → (𝑎 ≠ 𝑐 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
34	33	ad2ant2r 745	. . . . . . 7 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → (𝑎 ≠ 𝑐 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
35		neeq1 2996	. . . . . . . . . 10 ⊢ (𝑥 = 𝑏 → (𝑥 ≠ 𝑦 ↔ 𝑏 ≠ 𝑦))
36		neeq2 2997	. . . . . . . . . 10 ⊢ (𝑦 = 𝑑 → (𝑏 ≠ 𝑦 ↔ 𝑏 ≠ 𝑑))
37	35, 36	rspc2ev 3633	. . . . . . . . 9 ⊢ ((𝑏 ∈ ℝ ∧ 𝑑 ∈ ℝ ∧ 𝑏 ≠ 𝑑) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦)
38	37	3expia 1118	. . . . . . . 8 ⊢ ((𝑏 ∈ ℝ ∧ 𝑑 ∈ ℝ) → (𝑏 ≠ 𝑑 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
39	38	ad2ant2l 744	. . . . . . 7 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → (𝑏 ≠ 𝑑 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
40	34, 39	jaod 857	. . . . . 6 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → ((𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
41	29, 40	syl5 34	. . . . 5 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
42	41	rexlimdvva 3206	. . . 4 ⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
43	42	rexlimivv 3194	. . 3 ⊢ (∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦)
44	1, 17, 43	mp2b 10	. 2 ⊢ ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦
45		eqtr3 2755	. . . . . . . . 9 ⊢ ((𝑥 = 0 ∧ 𝑦 = 0) → 𝑥 = 𝑦)
46	45	ex 411	. . . . . . . 8 ⊢ (𝑥 = 0 → (𝑦 = 0 → 𝑥 = 𝑦))
47	46	necon3d 2954	. . . . . . 7 ⊢ (𝑥 = 0 → (𝑥 ≠ 𝑦 → 𝑦 ≠ 0))
48		neeq1 2996	. . . . . . . . 9 ⊢ (𝑧 = 𝑦 → (𝑧 ≠ 0 ↔ 𝑦 ≠ 0))
49	48	rspcev 3620	. . . . . . . 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 2996	. . . . . . . 8 ⊢ (𝑧 = 𝑥 → (𝑧 ≠ 0 ↔ 𝑥 ≠ 0))
55	54	rspcev 3620	. . . . . . 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 3018	. . 3 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
60	59	rexlimivv 3194	. 2 ⊢ (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)
61		ax-rrecex 11237	. . . 4 ⊢ ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → ∃𝑥 ∈ ℝ (𝑧 · 𝑥) = 1)
62		remulcl 11250	. . . . . . 7 ⊢ ((𝑧 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (𝑧 · 𝑥) ∈ ℝ)
63	62	adantlr 713	. . . . . 6 ⊢ (((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) ∧ 𝑥 ∈ ℝ) → (𝑧 · 𝑥) ∈ ℝ)
64		eleq1 2817	. . . . . 6 ⊢ ((𝑧 · 𝑥) = 1 → ((𝑧 · 𝑥) ∈ ℝ ↔ 1 ∈ ℝ))
65	63, 64	syl5ibcom 244	. . . . 5 ⊢ (((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) ∧ 𝑥 ∈ ℝ) → ((𝑧 · 𝑥) = 1 → 1 ∈ ℝ))
66	65	rexlimdva 3148	. . . 4 ⊢ ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → (∃𝑥 ∈ ℝ (𝑧 · 𝑥) = 1 → 1 ∈ ℝ))
67	61, 66	mpd 15	. . 3 ⊢ ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → 1 ∈ ℝ)
68	67	rexlimiva 3140	. 2 ⊢ (∃𝑧 ∈ ℝ 𝑧 ≠ 0 → 1 ∈ ℝ)
69	44, 60, 68	mp2b 10	1 ⊢ 1 ∈ ℝ

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 394   ∨ wo 845   = wceq 1534   ∈ wcel 2100   ≠ wne 2933  ∃wrex 3063  (class class class)co 7430  ℂcc 11163  ℝcr 11164  0cc0 11165  1c1 11166  ici 11167   + caddc 11168   · cmul 11170

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2102  ax-9 2110  ax-ext 2700  ax-1cn 11223  ax-icn 11224  ax-addcl 11225  ax-mulcl 11227  ax-mulrcl 11228  ax-i2m1 11233  ax-1ne0 11234  ax-rrecex 11237  ax-cnre 11238

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2062  df-clab 2707  df-cleq 2721  df-clel 2806  df-ne 2934  df-ral 3055  df-rex 3064  df-rab 3429  df-v 3474  df-dif 3962  df-un 3964  df-ss 3976  df-nul 4336  df-if 4537  df-sn 4637  df-pr 4639  df-op 4643  df-uni 4919  df-br 5157  df-iota 6510  df-fv 6566  df-ov 7433

This theorem is referenced by:  1red  11272  1xr  11330  dedekind  11434  peano2re  11444  mul02lem2  11448  addrid  11451  renegcl  11580  peano2rem  11584  0reALT  11614  0lt1  11793  0le1  11794  relin01  11795  1le1  11899  eqneg  11995  ltp1  12115  ltm1  12117  recgt0  12121  mulgt1OLD  12134  ltmulgt11  12135  lemulge11  12138  reclt1  12171  recgt1  12172  recgt1i  12173  recp1lt1  12174  recreclt  12175  recgt0ii  12182  ledivp1i  12201  ltdivp1i  12202  inelr  12264  cju  12270  nnssre  12278  nnge1  12302  nngt1ne1  12303  nnle1eq1  12304  nngt0  12305  nnnlt1  12306  nnne0  12308  nnrecre  12316  nnrecgt0  12317  nnsub  12318  2re  12348  3re  12354  4re  12358  5re  12361  6re  12364  7re  12367  8re  12370  9re  12373  0le2  12376  2pos  12377  3pos  12379  4pos  12381  5pos  12383  6pos  12384  7pos  12385  8pos  12386  9pos  12387  neg1rr  12389  neg1lt0  12391  1lt2  12445  1lt3  12447  1lt4  12450  1lt5  12454  1lt6  12459  1lt7  12465  1lt8  12472  1lt9  12480  1ne2  12482  1le2  12483  1le3  12486  halflt1  12492  addltmul  12510  nnunb  12530  elnnnn0c  12579  nn0ge2m1nn  12603  elnnz1  12650  znnnlt1  12651  zltp1le  12674  zleltp1  12675  nn0lt2  12687  recnz  12699  gtndiv  12701  3halfnz  12703  10re  12758  1lt10  12878  eluzp1m1  12910  eluzp1p1  12912  eluz2b2  12967  zbtwnre  12992  rebtwnz  12993  1rp  13042  divlt1lt  13107  divle1le  13108  nnledivrp  13150  qbtwnxr  13243  xmulrid  13322  xmulm1  13324  x2times  13342  xrub  13355  elicc01  13507  1elunit  13511  divelunit  13535  lincmb01cmp  13536  unitssre  13540  0nelfz1  13584  fzpreddisj  13614  fznatpl1  13619  fztpval  13627  fraclt1  13833  fracle1  13834  flbi2  13848  fldiv4p1lem1div2  13866  fldiv4lem1div2  13868  fldiv  13891  modid  13927  1mod  13934  m1modnnsub1  13948  modm1p1mod0  13953  seqf1olem1  14072  reexpcl  14109  reexpclz  14113  expge0  14129  expge1  14130  expgt1  14131  bernneq  14258  bernneq2  14259  expnbnd  14261  expnlbnd  14262  expnlbnd2  14263  expmulnbnd  14264  discr1  14268  facwordi  14318  faclbnd3  14321  faclbnd4lem1  14322  faclbnd4lem4  14325  faclbnd6  14328  facavg  14330  hashv01gt1  14374  hashnn0n0nn  14420  hashunsnggt  14423  hash1snb  14448  hashgt12el  14451  hashgt12el2  14452  hashfun  14466  hashge2el2dif  14511  tpf1ofv2  14528  lsw0  14594  f1oun2prg  14947  cjexp  15176  re1  15180  im1  15181  rei  15182  imi  15183  01sqrexlem1  15268  01sqrexlem2  15269  01sqrexlem3  15270  01sqrexlem4  15271  01sqrexlem7  15274  resqrex  15276  sqrt1  15297  sqrt2gt1lt2  15300  sqrtm1  15301  abs1  15323  absrdbnd  15367  caubnd2  15383  mulcn2  15619  reccn2  15620  rlimno1  15679  o1fsum  15838  expcnv  15889  geolim  15895  geolim2  15896  georeclim  15897  geomulcvg  15901  geoisumr  15903  geoisum1c  15905  fprodge0  16016  fprodge1  16018  rerisefaccl  16040  refallfaccl  16041  ere  16112  ege2le3  16113  efgt1  16139  resin4p  16161  recos4p  16162  tanhbnd  16184  sinbnd  16203  cosbnd  16204  sinbnd2  16205  cosbnd2  16206  ef01bndlem  16207  sin01bnd  16208  cos01bnd  16209  cos1bnd  16210  cos2bnd  16211  sinltx  16212  sin01gt0  16213  cos01gt0  16214  sin02gt0  16215  sincos1sgn  16216  ene1  16233  rpnnen2lem2  16238  rpnnen2lem3  16239  rpnnen2lem4  16240  rpnnen2lem9  16245  rpnnen2lem12  16248  ruclem6  16258  ruclem11  16263  ruclem12  16264  3dvds  16354  flodddiv4  16436  sadcadd  16479  isprm3  16705  sqnprm  16724  coprm  16733  phibndlem  16793  pythagtriplem3  16841  pcmpt  16915  fldivp1  16920  pockthi  16930  infpn2  16936  resslemOLD  17277  basendxnmulrndx  17330  basendxnmulrndxOLD  17331  starvndxnbasendx  17339  scandxnbasendx  17351  vscandxnbasendx  17356  ipndxnbasendx  17367  basendxnocndx  17418  slotsbhcdif  17450  slotsbhcdifOLD  17451  oppcbasOLD  17754  rescbasOLD  17867  rescabsOLD  17873  odubasOLD  18338  symgvalstructOLD  19417  lt6abl  19915  srgbinomlem4  20234  0ringnnzr  20529  abvneg  20827  abvtrivd  20833  rmodislmodOLD  20929  cnfldfunALTOLDOLD  21394  xrsmcmn  21405  xrsnsgrp  21421  gzrngunitlem  21451  gzrngunit  21452  rge0srg  21457  psgnodpmr  21608  remulg  21625  resubdrg  21626  thlbasOLD  21715  tuslemOLD  24286  setsmsbasOLD  24496  dscmet  24595  dscopn  24596  nrginvrcnlem  24722  idnghm  24774  tgioo  24826  blcvx  24828  iicmp  24920  iiconn  24921  iirev  24964  iihalf1  24966  iihalf2  24969  iihalf2cnOLD  24971  elii1  24972  elii2  24973  iimulcl  24974  icopnfcnv  24981  icopnfhmeo  24982  iccpnfhmeo  24984  xrhmeo  24985  xrhmph  24986  evth  24999  xlebnum  25005  htpycc  25020  reparphti  25037  reparphtiOLD  25038  pcoval1  25054  pco1  25056  pcoval2  25057  pcocn  25058  pcohtpylem  25060  pcopt  25063  pcopt2  25064  pcoass  25065  pcorevlem  25067  nmhmcn  25161  ncvs1  25199  ovolunlem1a  25539  vitalilem2  25652  vitalilem4  25654  vitalilem5  25655  vitali  25656  i1f1  25733  itg11  25734  itg2const  25784  dveflem  26025  dvlipcn  26041  dvcvx  26067  ply1remlem  26215  fta1blem  26221  vieta1lem2  26362  aalioulem3  26385  aalioulem5  26387  aaliou3lem2  26394  ulmbdd  26450  iblulm  26459  radcnvlem1  26465  dvradcnv  26473  abelthlem2  26485  abelthlem3  26486  abelthlem5  26488  abelthlem7  26491  abelth  26494  abelth2  26495  reeff1olem  26499  reeff1o  26500  sinhalfpilem  26514  tangtx  26556  sincos4thpi  26564  pige3ALT  26570  coskpi  26573  cos0pilt1  26582  recosf1o  26585  tanregt0  26589  efif1olem3  26594  efif1olem4  26595  loge  26636  logdivlti  26670  logcnlem4  26695  logf1o2  26700  logtayl  26710  logccv  26713  recxpcl  26725  cxplea  26746  cxpcn3lem  26798  cxpaddlelem  26802  loglesqrt  26812  ang180lem2  26861  angpined  26881  acosrecl  26954  atancj  26961  atanlogaddlem  26964  atantan  26974  atans2  26982  ressatans  26985  leibpi  26993  log2le1  27001  birthdaylem3  27004  cxp2lim  27028  cxploglim  27029  cxploglim2  27030  divsqrtsumlem  27031  cvxcl  27036  scvxcvx  27037  jensenlem2  27039  amgmlem  27041  emcllem2  27048  emcllem4  27050  emcllem6  27052  emcllem7  27053  emre  27057  emgt0  27058  harmonicbnd3  27059  harmonicubnd  27061  harmonicbnd4  27062  zetacvg  27066  ftalem1  27124  ftalem2  27125  ftalem5  27128  issqf  27187  cht1  27216  chp1  27218  ppiltx  27228  mumullem2  27231  ppiublem1  27254  ppiub  27256  chtublem  27263  chtub  27264  logfacbnd3  27275  logexprlim  27277  perfectlem2  27282  dchrinv  27313  dchr1re  27315  efexple  27333  bposlem1  27336  bposlem2  27337  bposlem5  27340  bposlem8  27343  lgsdir2lem1  27377  lgsdir2lem5  27381  lgsdir  27384  lgsne0  27387  lgsabs1  27388  lgsdinn0  27397  gausslemma2dlem0i  27416  lgseisen  27431  m1lgs  27440  2lgslem3  27456  addsq2nreurex  27496  2sqreultblem  27500  2sqreunnltblem  27503  chebbnd1lem3  27523  chebbnd1  27524  chtppilimlem1  27525  chtppilimlem2  27526  chtppilim  27527  chpchtlim  27531  vmadivsumb  27535  rplogsumlem2  27537  rpvmasumlem  27539  dchrmusumlema  27545  dchrmusum2  27546  dchrvmasumlem2  27550  dchrvmasumiflem1  27553  dchrisum0flblem1  27560  dchrisum0flblem2  27561  dchrisum0fno1  27563  rpvmasum2  27564  dchrisum0re  27565  dchrisum0lema  27566  dchrisum0lem1b  27567  dchrisum0lem1  27568  dchrisum0lem2a  27569  dchrisum0lem2  27570  logdivsum  27585  mulog2sumlem2  27587  2vmadivsumlem  27592  log2sumbnd  27596  selbergb  27601  selberg2b  27604  chpdifbndlem1  27605  selberg3lem1  27609  selberg3lem2  27610  selberg4lem1  27612  pntrmax  27616  pntrsumo1  27617  selbergsb  27627  pntrlog2bndlem3  27631  pntrlog2bndlem5  27633  pntpbnd1a  27637  pntpbnd2  27639  pntibndlem1  27641  pntibndlem3  27644  pntlemd  27646  pntlemc  27647  pntlemb  27649  pntlemr  27654  pntlemf  27657  pntlemk  27658  pntlemo  27659  pntlem3  27661  pntleml  27663  abvcxp  27667  ostth2lem1  27670  ostth1  27685  ostth2lem2  27686  ostth2lem3  27687  ostth2lem4  27688  ostth2  27689  ostth3  27690  ostth  27691  slotsinbpsd  28391  slotslnbpsd  28392  trgcgrg  28465  brbtwn2  28862  colinearalglem4  28866  ax5seglem2  28886  ax5seglem3  28888  axpaschlem  28897  axpasch  28898  axlowdimlem6  28904  axlowdimlem10  28908  axlowdimlem16  28914  axlowdim1  28916  axlowdim2  28917  axlowdim  28918  axcontlem2  28922  elntg2  28942  lfgrnloop  29084  lfuhgr1v0e  29213  usgrexmpldifpr  29217  usgrexmplef  29218  1loopgrvd2  29463  vdegp1bi  29497  lfgrwlkprop  29647  pthdlem1  29726  pthdlem2  29728  clwlkclwwlkf  29964  upgr4cycl4dv4e  30141  konigsberglem2  30209  konigsberglem3  30210  konigsberglem5  30212  frgrreg  30350  ex-dif  30379  ex-in  30381  ex-pss  30384  ex-res  30397  ex-fl  30403  nv1  30631  smcnlem  30653  ipidsq  30666  nmlno0lem  30749  norm-ii-i  31093  bcs2  31138  norm1  31205  nmopub2tALT  31865  nmfnleub2  31882  nmlnop0iALT  31951  unopbd  31971  nmopadjlem  32045  nmopcoadji  32057  pjnmopi  32104  pjbdlni  32105  hstle1  32182  hstle  32186  hstles  32187  stge1i  32194  stlesi  32197  staddi  32202  stadd3i  32204  strlem1  32206  strlem5  32211  jplem1  32224  cdj1i  32389  addltmulALT  32402  xlt2addrd  32691  pr01ssre  32754  dp2lt10  32774  dp2ltsuc  32776  dp2ltc  32777  dplti  32795  dpmul4  32804  cshw1s2  32853  xrsmulgzz  32918  resvbasOLD  33252  rearchi  33266  xrge0slmod  33268  prmidl0  33370  evl1deg3  33495  constrconj  33662  2sqr3minply  33665  submateqlem1  33680  xrge0iifcnv  33806  xrge0iifcv  33807  xrge0iifiso  33808  xrge0iifhom  33810  zrhre  33892  indf  33906  indfval  33907  esumcst  33954  cntnevol  34119  omssubadd  34192  iwrdsplit  34279  dstfrvclim1  34369  coinfliprv  34374  ballotlem2  34380  ballotlem4  34390  ballotlemi1  34394  ballotlemic  34398  sgnclre  34431  sgnnbi  34437  sgnpbi  34438  sgnmulsgp  34442  plymulx0  34451  plymulx  34452  signswch  34465  signstf  34470  signsvfn  34486  itgexpif  34510  hgt750lemd  34552  logdivsqrle  34554  hgt750lem  34555  hgt750lem2  34556  hgt750leme  34562  tgoldbachgnn  34563  subfacp1lem1  35074  subfacp1lem5  35079  resconn  35141  iisconn  35147  iillysconn  35148  problem2  35561  problem3  35562  sinccvglem  35567  fz0n  35620  dnibndlem12  36260  knoppcnlem4  36267  knoppndvlem13  36295  cnndvlem1  36308  irrdiff  37100  relowlpssretop  37138  sin2h  37378  cos2h  37379  tan2h  37380  poimirlem7  37395  poimirlem16  37404  poimirlem17  37405  poimirlem19  37407  poimirlem20  37408  poimirlem22  37410  poimirlem23  37411  poimirlem29  37417  poimirlem31  37419  itg2addnclem3  37441  asindmre  37471  dvasin  37472  dvacos  37473  dvreasin  37474  dvreacos  37475  fdc  37513  geomcau  37527  cntotbnd  37564  heiborlem8  37586  bfplem2  37591  bfp  37592  aks4d1p1p7  41840  2xp3dxp2ge1d  42003  factwoffsmonot  42004  1t1e1ALT  42055  ine1  42096  re1m1e0m0  42162  sn-00idlem1  42163  sn-00idlem2  42164  remul02  42170  sn-0ne2  42171  reixi  42187  rei4  42188  remullid  42198  ipiiie0  42202  sn-0tie0  42204  sn-nnne0  42213  mulgt0b2d  42225  sn-0lt1  42228  sn-ltp1  42229  reneg1lt0  42231  sn-inelr  42232  rabren3dioph  42563  pellexlem5  42581  pellexlem6  42582  pell1qrgaplem  42621  pell14qrgap  42623  pellqrex  42627  pellfundre  42629  pellfundlb  42632  pellfund14gap  42635  jm2.17a  42709  acongeq  42732  jm2.23  42745  jm3.1lem2  42767  sqrtcval  43399  sqrtcval2  43400  resqrtval  43401  imsqrtval  43402  relexp01min  43471  mnringbasedOLD  43977  cvgdvgrat  44078  lhe4.4ex1a  44094  binomcxplemnotnn0  44121  isosctrlem1ALT  44701  supxrgelem  45042  xrlexaddrp  45057  infxr  45072  infleinflem2  45076  sumnnodd  45341  limsup10exlem  45483  limsup10ex  45484  dvnprodlem3  45659  stoweidlem1  45712  stoweidlem18  45729  stoweidlem19  45730  stoweidlem26  45737  stoweidlem34  45745  stoweidlem40  45751  stoweidlem41  45752  stoweidlem59  45770  stoweid  45774  stirlinglem10  45794  stirlinglem11  45795  dirkercncflem1  45814  fourierdlem16  45834  fourierdlem21  45839  fourierdlem22  45840  fourierdlem42  45860  fourierdlem68  45885  fourierdlem83  45900  fourierdlem103  45920  sqwvfourb  45940  fouriersw  45942  etransclem23  45968  salgencntex  46054  ovn0lem  46276  smfmullem3  46504  smfmullem4  46505  zm1nn  47005  m1mod0mod1  47031  fmtnosqrt  47201  perfectALTVlem2  47384  2exp340mod341  47395  8exp8mod9  47398  nfermltl8rev  47404  nnsum3primesprm  47452  nnsum4primesodd  47458  nnsum4primesoddALTV  47459  nnsum4primeseven  47462  nnsum4primesevenALTV  47463  tgblthelfgott  47477  tgoldbach  47479  rege1logbrege0  48047  rege1logbzge0  48048  blennnelnn  48065  dignnld  48092  nn0sumshdiglemA  48108  nn0sumshdiglem1  48110  rrx2xpref1o  48207  rrxlines  48222  eenglngeehlnmlem1  48226  eenglngeehlnmlem2  48227  line2ylem  48240  line2x  48243  icccldii  48353  io1ii  48355  sepfsepc  48362