Theorem 1re 10906

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 10860, 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 10871	. . 3 ⊢ 1 ≠ 0
2		ax-1cn 10860	. . . . 5 ⊢ 1 ∈ ℂ
3		cnre 10903	. . . . 5 ⊢ (1 ∈ ℂ → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)))
4	2, 3	ax-mp 5	. . . 4 ⊢ ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏))
5		neeq1 3005	. . . . . . . 8 ⊢ (1 = (𝑎 + (i · 𝑏)) → (1 ≠ 0 ↔ (𝑎 + (i · 𝑏)) ≠ 0))
6	5	biimpcd 248	. . . . . . 7 ⊢ (1 ≠ 0 → (1 = (𝑎 + (i · 𝑏)) → (𝑎 + (i · 𝑏)) ≠ 0))
7		0cn 10898	. . . . . . . 8 ⊢ 0 ∈ ℂ
8		cnre 10903	. . . . . . . 8 ⊢ (0 ∈ ℂ → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)))
9	7, 8	ax-mp 5	. . . . . . 7 ⊢ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑))
10		neeq2 3006	. . . . . . . . . 10 ⊢ (0 = (𝑐 + (i · 𝑑)) → ((𝑎 + (i · 𝑏)) ≠ 0 ↔ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
11	10	biimpcd 248	. . . . . . . . 9 ⊢ ((𝑎 + (i · 𝑏)) ≠ 0 → (0 = (𝑐 + (i · 𝑑)) → (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
12	11	reximdv 3201	. . . . . . . 8 ⊢ ((𝑎 + (i · 𝑏)) ≠ 0 → (∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)) → ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
13	12	reximdv 3201	. . . . . . 7 ⊢ ((𝑎 + (i · 𝑏)) ≠ 0 → (∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)) → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
14	6, 9, 13	syl6mpi 67	. . . . . 6 ⊢ (1 ≠ 0 → (1 = (𝑎 + (i · 𝑏)) → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
15	14	reximdv 3201	. . . . 5 ⊢ (1 ≠ 0 → (∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)) → ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
16	15	reximdv 3201	. . . 4 ⊢ (1 ≠ 0 → (∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)) → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
17	4, 16	mpi 20	. . 3 ⊢ (1 ≠ 0 → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)))
18		ioran 980	. . . . . . . . 9 ⊢ (¬ (𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑) ↔ (¬ 𝑎 ≠ 𝑐 ∧ ¬ 𝑏 ≠ 𝑑))
19		df-ne 2943	. . . . . . . . . . 11 ⊢ (𝑎 ≠ 𝑐 ↔ ¬ 𝑎 = 𝑐)
20	19	con2bii 357	. . . . . . . . . 10 ⊢ (𝑎 = 𝑐 ↔ ¬ 𝑎 ≠ 𝑐)
21		df-ne 2943	. . . . . . . . . . 11 ⊢ (𝑏 ≠ 𝑑 ↔ ¬ 𝑏 = 𝑑)
22	21	con2bii 357	. . . . . . . . . 10 ⊢ (𝑏 = 𝑑 ↔ ¬ 𝑏 ≠ 𝑑)
23	20, 22	anbi12i 626	. . . . . . . . 9 ⊢ ((𝑎 = 𝑐 ∧ 𝑏 = 𝑑) ↔ (¬ 𝑎 ≠ 𝑐 ∧ ¬ 𝑏 ≠ 𝑑))
24	18, 23	bitr4i 277	. . . . . . . 8 ⊢ (¬ (𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑) ↔ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑))
25		id 22	. . . . . . . . 9 ⊢ (𝑎 = 𝑐 → 𝑎 = 𝑐)
26		oveq2 7263	. . . . . . . . 9 ⊢ (𝑏 = 𝑑 → (i · 𝑏) = (i · 𝑑))
27	25, 26	oveqan12d 7274	. . . . . . . 8 ⊢ ((𝑎 = 𝑐 ∧ 𝑏 = 𝑑) → (𝑎 + (i · 𝑏)) = (𝑐 + (i · 𝑑)))
28	24, 27	sylbi 216	. . . . . . 7 ⊢ (¬ (𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑) → (𝑎 + (i · 𝑏)) = (𝑐 + (i · 𝑑)))
29	28	necon1ai 2970	. . . . . 6 ⊢ ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → (𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑))
30		neeq1 3005	. . . . . . . . . 10 ⊢ (𝑥 = 𝑎 → (𝑥 ≠ 𝑦 ↔ 𝑎 ≠ 𝑦))
31		neeq2 3006	. . . . . . . . . 10 ⊢ (𝑦 = 𝑐 → (𝑎 ≠ 𝑦 ↔ 𝑎 ≠ 𝑐))
32	30, 31	rspc2ev 3564	. . . . . . . . 9 ⊢ ((𝑎 ∈ ℝ ∧ 𝑐 ∈ ℝ ∧ 𝑎 ≠ 𝑐) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦)
33	32	3expia 1119	. . . . . . . 8 ⊢ ((𝑎 ∈ ℝ ∧ 𝑐 ∈ ℝ) → (𝑎 ≠ 𝑐 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
34	33	ad2ant2r 743	. . . . . . 7 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → (𝑎 ≠ 𝑐 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
35		neeq1 3005	. . . . . . . . . 10 ⊢ (𝑥 = 𝑏 → (𝑥 ≠ 𝑦 ↔ 𝑏 ≠ 𝑦))
36		neeq2 3006	. . . . . . . . . 10 ⊢ (𝑦 = 𝑑 → (𝑏 ≠ 𝑦 ↔ 𝑏 ≠ 𝑑))
37	35, 36	rspc2ev 3564	. . . . . . . . 9 ⊢ ((𝑏 ∈ ℝ ∧ 𝑑 ∈ ℝ ∧ 𝑏 ≠ 𝑑) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦)
38	37	3expia 1119	. . . . . . . 8 ⊢ ((𝑏 ∈ ℝ ∧ 𝑑 ∈ ℝ) → (𝑏 ≠ 𝑑 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
39	38	ad2ant2l 742	. . . . . . 7 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → (𝑏 ≠ 𝑑 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
40	34, 39	jaod 855	. . . . . 6 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → ((𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
41	29, 40	syl5 34	. . . . 5 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
42	41	rexlimdvva 3222	. . . 4 ⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
43	42	rexlimivv 3220	. . 3 ⊢ (∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦)
44	1, 17, 43	mp2b 10	. 2 ⊢ ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦
45		eqtr3 2764	. . . . . . . . 9 ⊢ ((𝑥 = 0 ∧ 𝑦 = 0) → 𝑥 = 𝑦)
46	45	ex 412	. . . . . . . 8 ⊢ (𝑥 = 0 → (𝑦 = 0 → 𝑥 = 𝑦))
47	46	necon3d 2963	. . . . . . 7 ⊢ (𝑥 = 0 → (𝑥 ≠ 𝑦 → 𝑦 ≠ 0))
48		neeq1 3005	. . . . . . . . 9 ⊢ (𝑧 = 𝑦 → (𝑧 ≠ 0 ↔ 𝑦 ≠ 0))
49	48	rspcev 3552	. . . . . . . 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 3005	. . . . . . . 8 ⊢ (𝑧 = 𝑥 → (𝑧 ≠ 0 ↔ 𝑥 ≠ 0))
55	54	rspcev 3552	. . . . . . 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 3027	. . 3 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
60	59	rexlimivv 3220	. 2 ⊢ (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)
61		ax-rrecex 10874	. . . 4 ⊢ ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → ∃𝑥 ∈ ℝ (𝑧 · 𝑥) = 1)
62		remulcl 10887	. . . . . . 7 ⊢ ((𝑧 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (𝑧 · 𝑥) ∈ ℝ)
63	62	adantlr 711	. . . . . 6 ⊢ (((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) ∧ 𝑥 ∈ ℝ) → (𝑧 · 𝑥) ∈ ℝ)
64		eleq1 2826	. . . . . 6 ⊢ ((𝑧 · 𝑥) = 1 → ((𝑧 · 𝑥) ∈ ℝ ↔ 1 ∈ ℝ))
65	63, 64	syl5ibcom 244	. . . . 5 ⊢ (((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) ∧ 𝑥 ∈ ℝ) → ((𝑧 · 𝑥) = 1 → 1 ∈ ℝ))
66	65	rexlimdva 3212	. . . 4 ⊢ ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → (∃𝑥 ∈ ℝ (𝑧 · 𝑥) = 1 → 1 ∈ ℝ))
67	61, 66	mpd 15	. . 3 ⊢ ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → 1 ∈ ℝ)
68	67	rexlimiva 3209	. 2 ⊢ (∃𝑧 ∈ ℝ 𝑧 ≠ 0 → 1 ∈ ℝ)
69	44, 60, 68	mp2b 10	1 ⊢ 1 ∈ ℝ

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∨ wo 843   = wceq 1539   ∈ wcel 2108   ≠ wne 2942  ∃wrex 3064  (class class class)co 7255  ℂcc 10800  ℝcr 10801  0cc0 10802  1c1 10803  ici 10804   + caddc 10805   · cmul 10807

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-1cn 10860  ax-icn 10861  ax-addcl 10862  ax-mulcl 10864  ax-mulrcl 10865  ax-i2m1 10870  ax-1ne0 10871  ax-rrecex 10874  ax-cnre 10875

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ne 2943  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-iota 6376  df-fv 6426  df-ov 7258

This theorem is referenced by:  1red  10907  1xr  10965  dedekind  11068  peano2re  11078  mul02lem2  11082  addid1  11085  renegcl  11214  peano2rem  11218  0reALT  11248  0lt1  11427  0le1  11428  relin01  11429  1le1  11533  eqneg  11625  ltp1  11745  ltm1  11747  recgt0  11751  mulgt1  11764  ltmulgt11  11765  lemulge11  11767  reclt1  11800  recgt1  11801  recgt1i  11802  recp1lt1  11803  recreclt  11804  recgt0ii  11811  ledivp1i  11830  ltdivp1i  11831  inelr  11893  cju  11899  nnssre  11907  nnge1  11931  nngt1ne1  11932  nnle1eq1  11933  nngt0  11934  nnnlt1  11935  nnne0  11937  nnrecre  11945  nnrecgt0  11946  nnsub  11947  2re  11977  3re  11983  4re  11987  5re  11990  6re  11993  7re  11996  8re  11999  9re  12002  0le2  12005  2pos  12006  3pos  12008  4pos  12010  5pos  12012  6pos  12013  7pos  12014  8pos  12015  9pos  12016  neg1rr  12018  neg1lt0  12020  1lt2  12074  1lt3  12076  1lt4  12079  1lt5  12083  1lt6  12088  1lt7  12094  1lt8  12101  1lt9  12109  1ne2  12111  1le2  12112  1le3  12115  halflt1  12121  addltmul  12139  nnunb  12159  elnnnn0c  12208  nn0ge2m1nn  12232  elnnz1  12276  znnnlt1  12277  zltp1le  12300  zleltp1  12301  nn0lt2  12313  recnz  12325  gtndiv  12327  3halfnz  12329  10re  12385  1lt10  12505  eluzp1m1  12537  eluzp1p1  12539  eluz2b2  12590  zbtwnre  12615  rebtwnz  12616  1rp  12663  divlt1lt  12728  divle1le  12729  nnledivrp  12771  qbtwnxr  12863  xmulid1  12942  xmulm1  12944  x2times  12962  xrub  12975  elicc01  13127  1elunit  13131  divelunit  13155  lincmb01cmp  13156  unitssre  13160  0nelfz1  13204  fzpreddisj  13234  fznatpl1  13239  fztpval  13247  fraclt1  13450  fracle1  13451  flbi2  13465  fldiv4p1lem1div2  13483  fldiv4lem1div2  13485  fldiv  13508  modid  13544  1mod  13551  m1modnnsub1  13565  modm1p1mod0  13570  seqf1olem1  13690  reexpcl  13727  reexpclz  13730  expge0  13747  expge1  13748  expgt1  13749  bernneq  13872  bernneq2  13873  expnbnd  13875  expnlbnd  13876  expnlbnd2  13877  expmulnbnd  13878  discr1  13882  facwordi  13931  faclbnd3  13934  faclbnd4lem1  13935  faclbnd4lem4  13938  faclbnd6  13941  facavg  13943  hashv01gt1  13987  hashnn0n0nn  14034  hashunsnggt  14037  hash1snb  14062  hashgt12el  14065  hashgt12el2  14066  hashfun  14080  hashge2el2dif  14122  lsw0  14196  f1oun2prg  14558  cjexp  14789  re1  14793  im1  14794  rei  14795  imi  14796  sqrlem1  14882  sqrlem2  14883  sqrlem3  14884  sqrlem4  14885  sqrlem7  14888  resqrex  14890  sqrt1  14911  sqrt2gt1lt2  14914  sqrtm1  14915  abs1  14937  absrdbnd  14981  caubnd2  14997  mulcn2  15233  reccn2  15234  rlimno1  15293  o1fsum  15453  expcnv  15504  geolim  15510  geolim2  15511  georeclim  15512  geomulcvg  15516  geoisumr  15518  geoisum1c  15520  fprodge0  15631  fprodge1  15633  rerisefaccl  15655  refallfaccl  15656  ere  15726  ege2le3  15727  efgt1  15753  resin4p  15775  recos4p  15776  tanhbnd  15798  sinbnd  15817  cosbnd  15818  sinbnd2  15819  cosbnd2  15820  ef01bndlem  15821  sin01bnd  15822  cos01bnd  15823  cos1bnd  15824  cos2bnd  15825  sinltx  15826  sin01gt0  15827  cos01gt0  15828  sin02gt0  15829  sincos1sgn  15830  ene1  15847  rpnnen2lem2  15852  rpnnen2lem3  15853  rpnnen2lem4  15854  rpnnen2lem9  15859  rpnnen2lem12  15862  ruclem6  15872  ruclem11  15877  ruclem12  15878  3dvds  15968  flodddiv4  16050  sadcadd  16093  isprm3  16316  sqnprm  16335  coprm  16344  phibndlem  16399  pythagtriplem3  16447  pcmpt  16521  fldivp1  16526  pockthi  16536  infpn2  16542  resslemOLD  16878  basendxnmulrndx  16931  basendxnmulrndxOLD  16932  starvndxnbasendx  16940  scandxnbasendx  16952  vscandxnbasendx  16957  ipndxnbasendx  16968  slotsbhcdif  17044  slotsbhcdifOLD  17045  oppcbasOLD  17346  rescbasOLD  17459  rescabs  17464  odubas  17925  symgvalstructOLD  18920  lt6abl  19411  srgbinomlem4  19694  abvneg  20009  abvtrivd  20015  rmodislmodOLD  20107  0ringnnzr  20453  cnfldfun  20522  xrsmcmn  20533  xrsnsgrp  20546  gzrngunitlem  20575  gzrngunit  20576  rge0srg  20581  psgnodpmr  20707  remulg  20724  resubdrg  20725  thlbas  20813  tuslemOLD  23327  setsmsbas  23536  dscmet  23634  dscopn  23635  nrginvrcnlem  23761  idnghm  23813  tgioo  23865  blcvx  23867  iicmp  23955  iiconn  23956  iirev  23998  iihalf1  24000  iihalf2  24002  iihalf2cn  24003  elii1  24004  elii2  24005  iimulcl  24006  icopnfcnv  24011  icopnfhmeo  24012  iccpnfhmeo  24014  xrhmeo  24015  xrhmph  24016  evth  24028  xlebnum  24034  htpycc  24049  reparphti  24066  pcoval1  24082  pco1  24084  pcoval2  24085  pcocn  24086  pcohtpylem  24088  pcopt  24091  pcopt2  24092  pcoass  24093  pcorevlem  24095  nmhmcn  24189  ncvs1  24226  ovolunlem1a  24565  vitalilem2  24678  vitalilem4  24680  vitalilem5  24681  vitali  24682  i1f1  24759  itg11  24760  itg2const  24810  dveflem  25048  dvlipcn  25063  dvcvx  25089  ply1remlem  25232  fta1blem  25238  vieta1lem2  25376  aalioulem3  25399  aalioulem5  25401  aaliou3lem2  25408  ulmbdd  25462  iblulm  25471  radcnvlem1  25477  dvradcnv  25485  abelthlem2  25496  abelthlem3  25497  abelthlem5  25499  abelthlem7  25502  abelth  25505  abelth2  25506  reeff1olem  25510  reeff1o  25511  sinhalfpilem  25525  tangtx  25567  sincos4thpi  25575  pige3ALT  25581  coskpi  25584  cos0pilt1  25593  recosf1o  25596  tanregt0  25600  efif1olem3  25605  efif1olem4  25606  loge  25647  logdivlti  25680  logcnlem4  25705  logf1o2  25710  logtayl  25720  logccv  25723  recxpcl  25735  cxplea  25756  cxpcn3lem  25805  cxpaddlelem  25809  loglesqrt  25816  ang180lem2  25865  angpined  25885  acosrecl  25958  atancj  25965  atanlogaddlem  25968  atantan  25978  atans2  25986  ressatans  25989  leibpi  25997  log2le1  26005  birthdaylem3  26008  cxp2lim  26031  cxploglim  26032  cxploglim2  26033  divsqrtsumlem  26034  cvxcl  26039  scvxcvx  26040  jensenlem2  26042  amgmlem  26044  emcllem2  26051  emcllem4  26053  emcllem6  26055  emcllem7  26056  emre  26060  emgt0  26061  harmonicbnd3  26062  harmonicubnd  26064  harmonicbnd4  26065  zetacvg  26069  ftalem1  26127  ftalem2  26128  ftalem5  26131  issqf  26190  cht1  26219  chp1  26221  ppiltx  26231  mumullem2  26234  ppiublem1  26255  ppiub  26257  chtublem  26264  chtub  26265  logfacbnd3  26276  logexprlim  26278  perfectlem2  26283  dchrinv  26314  dchr1re  26316  efexple  26334  bposlem1  26337  bposlem2  26338  bposlem5  26341  bposlem8  26344  lgsdir2lem1  26378  lgsdir2lem5  26382  lgsdir  26385  lgsne0  26388  lgsabs1  26389  lgsdinn0  26398  gausslemma2dlem0i  26417  lgseisen  26432  m1lgs  26441  2lgslem3  26457  addsq2nreurex  26497  2sqreultblem  26501  2sqreunnltblem  26504  chebbnd1lem3  26524  chebbnd1  26525  chtppilimlem1  26526  chtppilimlem2  26527  chtppilim  26528  chpchtlim  26532  vmadivsumb  26536  rplogsumlem2  26538  rpvmasumlem  26540  dchrmusumlema  26546  dchrmusum2  26547  dchrvmasumlem2  26551  dchrvmasumiflem1  26554  dchrisum0flblem1  26561  dchrisum0flblem2  26562  dchrisum0fno1  26564  rpvmasum2  26565  dchrisum0re  26566  dchrisum0lema  26567  dchrisum0lem1b  26568  dchrisum0lem1  26569  dchrisum0lem2a  26570  dchrisum0lem2  26571  logdivsum  26586  mulog2sumlem2  26588  2vmadivsumlem  26593  log2sumbnd  26597  selbergb  26602  selberg2b  26605  chpdifbndlem1  26606  selberg3lem1  26610  selberg3lem2  26611  selberg4lem1  26613  pntrmax  26617  pntrsumo1  26618  selbergsb  26628  pntrlog2bndlem3  26632  pntrlog2bndlem5  26634  pntpbnd1a  26638  pntpbnd2  26640  pntibndlem1  26642  pntibndlem3  26645  pntlemd  26647  pntlemc  26648  pntlemb  26650  pntlemr  26655  pntlemf  26658  pntlemk  26659  pntlemo  26660  pntlem3  26662  pntleml  26664  abvcxp  26668  ostth2lem1  26671  ostth1  26686  ostth2lem2  26687  ostth2lem3  26688  ostth2lem4  26689  ostth2  26690  ostth3  26691  ostth  26692  slotsinbpsd  26707  slotslnbpsd  26708  trgcgrg  26780  brbtwn2  27176  colinearalglem4  27180  ax5seglem2  27200  ax5seglem3  27202  axpaschlem  27211  axpasch  27212  axlowdimlem6  27218  axlowdimlem10  27222  axlowdimlem16  27228  axlowdim1  27230  axlowdim2  27231  axlowdim  27232  axcontlem2  27236  elntg2  27256  lfgrnloop  27398  lfuhgr1v0e  27524  usgrexmpldifpr  27528  usgrexmplef  27529  1loopgrvd2  27773  vdegp1bi  27807  lfgrwlkprop  27957  pthdlem1  28035  pthdlem2  28037  clwlkclwwlkf  28273  upgr4cycl4dv4e  28450  konigsberglem2  28518  konigsberglem3  28519  konigsberglem5  28521  frgrreg  28659  ex-dif  28688  ex-in  28690  ex-pss  28693  ex-res  28706  ex-fl  28712  nv1  28938  smcnlem  28960  ipidsq  28973  nmlno0lem  29056  norm-ii-i  29400  bcs2  29445  norm1  29512  nmopub2tALT  30172  nmfnleub2  30189  nmlnop0iALT  30258  unopbd  30278  nmopadjlem  30352  nmopcoadji  30364  pjnmopi  30411  pjbdlni  30412  hstle1  30489  hstle  30493  hstles  30494  stge1i  30501  stlesi  30504  staddi  30509  stadd3i  30511  strlem1  30513  strlem5  30518  jplem1  30531  cdj1i  30696  addltmulALT  30709  xlt2addrd  30983  pr01ssre  31040  dp2lt10  31060  dp2ltsuc  31062  dp2ltc  31063  dplti  31081  dpmul4  31090  cshw1s2  31134  xrsmulgzz  31189  resvbasOLD  31435  rearchi  31448  xrge0slmod  31450  prmidl0  31528  submateqlem1  31659  xrge0iifcnv  31785  xrge0iifcv  31786  xrge0iifiso  31787  xrge0iifhom  31789  zrhre  31869  indf  31883  indfval  31884  esumcst  31931  cntnevol  32096  omssubadd  32167  iwrdsplit  32254  dstfrvclim1  32344  coinfliprv  32349  ballotlem2  32355  ballotlem4  32365  ballotlemi1  32369  ballotlemic  32373  sgnclre  32406  sgnnbi  32412  sgnpbi  32413  sgnmulsgp  32417  plymulx0  32426  plymulx  32427  signswch  32440  signstf  32445  signsvfn  32461  itgexpif  32486  hgt750lemd  32528  logdivsqrle  32530  hgt750lem  32531  hgt750lem2  32532  hgt750leme  32538  tgoldbachgnn  32539  subfacp1lem1  33041  subfacp1lem5  33046  resconn  33108  iisconn  33114  iillysconn  33115  problem2  33524  problem3  33525  sinccvglem  33530  fz0n  33602  dnibndlem12  34596  knoppcnlem4  34603  knoppndvlem13  34631  cnndvlem1  34644  irrdiff  35424  relowlpssretop  35462  sin2h  35694  cos2h  35695  tan2h  35696  poimirlem7  35711  poimirlem16  35720  poimirlem17  35721  poimirlem19  35723  poimirlem20  35724  poimirlem22  35726  poimirlem23  35727  poimirlem29  35733  poimirlem31  35735  itg2addnclem3  35757  asindmre  35787  dvasin  35788  dvacos  35789  dvreasin  35790  dvreacos  35791  fdc  35830  geomcau  35844  cntotbnd  35881  heiborlem8  35903  bfplem2  35908  bfp  35909  aks4d1p1p7  40010  2xp3dxp2ge1d  40090  factwoffsmonot  40091  1t1e1ALT  40213  re1m1e0m0  40301  sn-00idlem1  40302  sn-00idlem2  40303  remul02  40309  sn-0ne2  40310  reixi  40325  rei4  40326  remulid2  40336  ipiiie0  40340  sn-0tie0  40342  mulgt0b2d  40351  sn-0lt1  40353  sn-ltp1  40354  reneg1lt0  40355  sn-inelr  40356  rabren3dioph  40553  pellexlem5  40571  pellexlem6  40572  pell1qrgaplem  40611  pell14qrgap  40613  pellqrex  40617  pellfundre  40619  pellfundlb  40622  pellfund14gap  40625  jm2.17a  40698  acongeq  40721  jm2.23  40734  jm3.1lem2  40756  sqrtcval  41138  sqrtcval2  41139  resqrtval  41140  imsqrtval  41141  relexp01min  41210  mnringbasedOLD  41719  cvgdvgrat  41820  lhe4.4ex1a  41836  binomcxplemnotnn0  41863  isosctrlem1ALT  42443  supxrgelem  42766  xrlexaddrp  42781  infxr  42796  infleinflem2  42800  sumnnodd  43061  limsup10exlem  43203  limsup10ex  43204  dvnprodlem3  43379  stoweidlem1  43432  stoweidlem18  43449  stoweidlem19  43450  stoweidlem26  43457  stoweidlem34  43465  stoweidlem40  43471  stoweidlem41  43472  stoweidlem59  43490  stoweid  43494  stirlinglem10  43514  stirlinglem11  43515  dirkercncflem1  43534  fourierdlem16  43554  fourierdlem21  43559  fourierdlem22  43560  fourierdlem42  43580  fourierdlem68  43605  fourierdlem83  43620  fourierdlem103  43640  sqwvfourb  43660  fouriersw  43662  etransclem23  43688  salgencntex  43772  ovn0lem  43993  smfmullem3  44214  smfmullem4  44215  zm1nn  44682  m1mod0mod1  44709  fmtnosqrt  44879  perfectALTVlem2  45062  2exp340mod341  45073  8exp8mod9  45076  nfermltl8rev  45082  nnsum3primesprm  45130  nnsum4primesodd  45136  nnsum4primesoddALTV  45137  nnsum4primeseven  45140  nnsum4primesevenALTV  45141  tgblthelfgott  45155  tgoldbach  45157  rege1logbrege0  45792  rege1logbzge0  45793  blennnelnn  45810  dignnld  45837  nn0sumshdiglemA  45853  nn0sumshdiglem1  45855  rrx2xpref1o  45952  rrxlines  45967  eenglngeehlnmlem1  45971  eenglngeehlnmlem2  45972  line2ylem  45985  line2x  45988  icccldii  46100  io1ii  46102  sepfsepc  46109