Theorem 1re 11308

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 11258, 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 11269	. . 3 ⊢ 1 ≠ 0
2		ax-1cn 11258	. . . . 5 ⊢ 1 ∈ ℂ
3		cnre 11305	. . . . 5 ⊢ (1 ∈ ℂ → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)))
4	2, 3	ax-mp 5	. . . 4 ⊢ ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏))
5		neeq1 3018	. . . . . . . 8 ⊢ (1 = (𝑎 + (i · 𝑏)) → (1 ≠ 0 ↔ (𝑎 + (i · 𝑏)) ≠ 0))
6	5	biimpcd 252	. . . . . . 7 ⊢ (1 ≠ 0 → (1 = (𝑎 + (i · 𝑏)) → (𝑎 + (i · 𝑏)) ≠ 0))
7		0cn 11298	. . . . . . . 8 ⊢ 0 ∈ ℂ
8		cnre 11305	. . . . . . . 8 ⊢ (0 ∈ ℂ → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)))
9	7, 8	ax-mp 5	. . . . . . 7 ⊢ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑))
10		neeq2 3019	. . . . . . . . . 10 ⊢ (0 = (𝑐 + (i · 𝑑)) → ((𝑎 + (i · 𝑏)) ≠ 0 ↔ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
11	10	biimpcd 252	. . . . . . . . 9 ⊢ ((𝑎 + (i · 𝑏)) ≠ 0 → (0 = (𝑐 + (i · 𝑑)) → (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
12	11	reximdv 3178	. . . . . . . 8 ⊢ ((𝑎 + (i · 𝑏)) ≠ 0 → (∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)) → ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
13	12	reximdv 3178	. . . . . . 7 ⊢ ((𝑎 + (i · 𝑏)) ≠ 0 → (∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)) → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
14	6, 9, 13	syl6mpi 68	. . . . . 6 ⊢ (1 ≠ 0 → (1 = (𝑎 + (i · 𝑏)) → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
15	14	reximdv 3178	. . . . 5 ⊢ (1 ≠ 0 → (∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)) → ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
16	15	reximdv 3178	. . . 4 ⊢ (1 ≠ 0 → (∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)) → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
17	4, 16	mpi 21	. . 3 ⊢ (1 ≠ 0 → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)))
18		id 23	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑐 → 𝑎 = 𝑐)
19		oveq2 7428	. . . . . . . . . . . 12 ⊢ (𝑏 = 𝑑 → (i · 𝑏) = (i · 𝑑))
20	18, 19	oveqan12d 7439	. . . . . . . . . . 11 ⊢ ((𝑎 = 𝑐 ∧ 𝑏 = 𝑑) → (𝑎 + (i · 𝑏)) = (𝑐 + (i · 𝑑)))
21	20	expcom 419	. . . . . . . . . 10 ⊢ (𝑏 = 𝑑 → (𝑎 = 𝑐 → (𝑎 + (i · 𝑏)) = (𝑐 + (i · 𝑑))))
22	21	necon3d 2977	. . . . . . . . 9 ⊢ (𝑏 = 𝑑 → ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → 𝑎 ≠ 𝑐))
23	22	com12 33	. . . . . . . 8 ⊢ ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → (𝑏 = 𝑑 → 𝑎 ≠ 𝑐))
24	23	necon3bd 2970	. . . . . . 7 ⊢ ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → (¬ 𝑎 ≠ 𝑐 → 𝑏 ≠ 𝑑))
25	24	orrd 877	. . . . . 6 ⊢ ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → (𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑))
26		neeq1 3018	. . . . . . . . . 10 ⊢ (𝑥 = 𝑎 → (𝑥 ≠ 𝑦 ↔ 𝑎 ≠ 𝑦))
27		neeq2 3019	. . . . . . . . . 10 ⊢ (𝑦 = 𝑐 → (𝑎 ≠ 𝑦 ↔ 𝑎 ≠ 𝑐))
28	26, 27	rspc2ev 3589	. . . . . . . . 9 ⊢ ((𝑎 ∈ ℝ ∧ 𝑐 ∈ ℝ ∧ 𝑎 ≠ 𝑐) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦)
29	28	3expia 1139	. . . . . . . 8 ⊢ ((𝑎 ∈ ℝ ∧ 𝑐 ∈ ℝ) → (𝑎 ≠ 𝑐 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
30	29	ad2ant2r 760	. . . . . . 7 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → (𝑎 ≠ 𝑐 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
31		neeq1 3018	. . . . . . . . . 10 ⊢ (𝑥 = 𝑏 → (𝑥 ≠ 𝑦 ↔ 𝑏 ≠ 𝑦))
32		neeq2 3019	. . . . . . . . . 10 ⊢ (𝑦 = 𝑑 → (𝑏 ≠ 𝑦 ↔ 𝑏 ≠ 𝑑))
33	31, 32	rspc2ev 3589	. . . . . . . . 9 ⊢ ((𝑏 ∈ ℝ ∧ 𝑑 ∈ ℝ ∧ 𝑏 ≠ 𝑑) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦)
34	33	3expia 1139	. . . . . . . 8 ⊢ ((𝑏 ∈ ℝ ∧ 𝑑 ∈ ℝ) → (𝑏 ≠ 𝑑 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
35	34	ad2ant2l 759	. . . . . . 7 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → (𝑏 ≠ 𝑑 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
36	30, 35	jaod 873	. . . . . 6 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → ((𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
37	25, 36	syl5 35	. . . . 5 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
38	37	rexlimdvva 3220	. . . 4 ⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
39	38	rexlimivv 3205	. . 3 ⊢ (∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦)
40	1, 17, 39	mp2b 10	. 2 ⊢ ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦
41		eqtr3 2783	. . . . . . . . 9 ⊢ ((𝑥 = 0 ∧ 𝑦 = 0) → 𝑥 = 𝑦)
42	41	ex 418	. . . . . . . 8 ⊢ (𝑥 = 0 → (𝑦 = 0 → 𝑥 = 𝑦))
43	42	necon3d 2977	. . . . . . 7 ⊢ (𝑥 = 0 → (𝑥 ≠ 𝑦 → 𝑦 ≠ 0))
44		neeq1 3018	. . . . . . . . 9 ⊢ (𝑧 = 𝑦 → (𝑧 ≠ 0 ↔ 𝑦 ≠ 0))
45	44	rspcev 3577	. . . . . . . 8 ⊢ ((𝑦 ∈ ℝ ∧ 𝑦 ≠ 0) → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)
46	45	expcom 419	. . . . . . 7 ⊢ (𝑦 ≠ 0 → (𝑦 ∈ ℝ → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
47	43, 46	syl6 36	. . . . . 6 ⊢ (𝑥 = 0 → (𝑥 ≠ 𝑦 → (𝑦 ∈ ℝ → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
48	47	com23 87	. . . . 5 ⊢ (𝑥 = 0 → (𝑦 ∈ ℝ → (𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
49	48	adantld 496	. . . 4 ⊢ (𝑥 = 0 → ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
50		neeq1 3018	. . . . . . . 8 ⊢ (𝑧 = 𝑥 → (𝑧 ≠ 0 ↔ 𝑥 ≠ 0))
51	50	rspcev 3577	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)
52	51	expcom 419	. . . . . 6 ⊢ (𝑥 ≠ 0 → (𝑥 ∈ ℝ → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
53	52	adantrd 497	. . . . 5 ⊢ (𝑥 ≠ 0 → ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
54	53	a1dd 51	. . . 4 ⊢ (𝑥 ≠ 0 → ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
55	49, 54	pm2.61ine 3039	. . 3 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
56	55	rexlimivv 3205	. 2 ⊢ (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)
57		ax-rrecex 11272	. . . 4 ⊢ ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → ∃𝑥 ∈ ℝ (𝑧 · 𝑥) = 1)
58		remulcl 11285	. . . . . . 7 ⊢ ((𝑧 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (𝑧 · 𝑥) ∈ ℝ)
59	58	adantlr 728	. . . . . 6 ⊢ (((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) ∧ 𝑥 ∈ ℝ) → (𝑧 · 𝑥) ∈ ℝ)
60		eleq1 2849	. . . . . 6 ⊢ ((𝑧 · 𝑥) = 1 → ((𝑧 · 𝑥) ∈ ℝ ↔ 1 ∈ ℝ))
61	59, 60	syl5ibcom 248	. . . . 5 ⊢ (((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) ∧ 𝑥 ∈ ℝ) → ((𝑧 · 𝑥) = 1 → 1 ∈ ℝ))
62	61	rexlimdva 3164	. . . 4 ⊢ ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → (∃𝑥 ∈ ℝ (𝑧 · 𝑥) = 1 → 1 ∈ ℝ))
63	57, 62	mpd 16	. . 3 ⊢ ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → 1 ∈ ℝ)
64	63	rexlimiva 3156	. 2 ⊢ (∃𝑧 ∈ ℝ 𝑧 ≠ 0 → 1 ∈ ℝ)
65	40, 56, 64	mp2b 10	1 ⊢ 1 ∈ ℝ

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∨ wo 861   = wceq 1570   ∈ wcel 2145   ≠ wne 2956  ∃wrex 3087  (class class class)co 7420  ℂcc 11198  ℝcr 11199  0cc0 11200  1c1 11201  ici 11202   + caddc 11203   · cmul 11205

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-1cn 11258  ax-icn 11259  ax-addcl 11260  ax-mulcl 11262  ax-mulrcl 11263  ax-i2m1 11268  ax-1ne0 11269  ax-rrecex 11272  ax-cnre 11273

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6494  df-fv 6546  df-ov 7423

This theorem is used by:  1red  11309  pr01ssre  11312  1xr  11368  dedekind  11473  peano2re  11483  mul02lem2  11487  addrid  11490  renegcl  11621  peano2rem  11625  0reALT  11655  0lt1  11838  0le1  11839  relin01  11840  1le1  11944  eqneg  12037  ltp1  12157  ltm1  12159  recgt0  12163  ltmulgt11  12176  lemulge11  12179  reclt1  12212  recgt1  12213  recgt1i  12214  recp1lt1  12215  recreclt  12216  recgt0ii  12223  ledivp1i  12242  ltdivp1i  12243  neg1rr  12306  neg1lt0  12308  cju  12316  indf  12326  indfval  12327  nnssre  12339  nnge1  12366  nngt1ne1  12367  nnle1eq1  12368  nngt0  12369  nnnlt1  12370  nnne0  12372  nnrecre  12380  nnrecgt0  12381  nnsub  12382  1t1e1ALT  12393  2re  12417  3re  12423  4re  12427  5re  12430  6re  12433  7re  12436  8re  12439  9re  12442  0le2OLD  12446  2posOLD  12448  1lt2  12515  1lt3  12518  1lt4  12521  1lt5  12525  1lt6  12530  1lt7  12536  1lt8  12543  1lt9  12551  1ne2  12553  1le2  12554  1le3  12557  halflt1  12563  addltmul  12582  nnunb  12602  elnnnn0c  12651  nn0ge2m1nn  12676  elnnz1  12722  znnnlt1  12723  zltp1le  12746  zleltp1  12747  nn0lt2  12762  recnz  12774  gtndiv  12776  3halfnz  12778  10re  12837  1lt10  12959  1lt10OLD  12960  eluzp1m1  12991  eluzp1p1  12993  eluz2b2  13048  zbtwnre  13073  rebtwnz  13074  1rp  13124  divlt1lt  13191  divle1le  13192  nnledivrp  13234  qbtwnxr  13330  xmulrid  13409  xmulm1  13411  x2times  13429  xrub  13442  elicc01  13597  1elunit  13601  divelunit  13625  lincmb01cmp  13626  unitssre  13630  0nelfz1  13676  fzpreddisj  13707  fznatpl1  13712  fztpval  13720  fraclt1  13942  fracle1  13943  flbi2  13957  fldiv4p1lem1div2  13975  fldiv4lem1div2  13977  fldiv  14000  modid  14036  1mod  14043  m1modnnsub1  14060  modm1p1mod0  14065  seqf1olem1  14184  reexpcl  14221  reexpclz  14225  expge0  14241  expge1  14242  expgt1  14243  bernneq  14373  bernneq2  14374  expnbnd  14376  expnlbnd  14377  expnlbnd2  14378  expmulnbnd  14379  discr1  14383  facwordi  14433  faclbnd3  14436  faclbnd4lem1  14437  faclbnd4lem4  14440  faclbnd6  14443  facavg  14445  hashv01gt1  14489  hashnn0n0nn  14535  hashunsnggt  14538  hash1snb  14564  hashgt12el  14567  hashgt12el2  14568  hashfun  14582  hashge2el2dif  14625  tpf1ofv2  14643  lsw0  14710  f1oun2prg  15068  sgnclre  15255  sgnnbi  15257  sgnpbi  15258  cjexp  15317  re1  15321  im1  15322  rei  15323  imi  15324  01sqrexlem1  15409  01sqrexlem2  15410  01sqrexlem3  15411  01sqrexlem4  15412  01sqrexlem7  15415  resqrex  15417  sqrt1  15438  sqrt2gt1lt2  15441  sqrtm1  15442  abs1  15464  absrdbnd  15509  caubnd2  15525  mulcn2  15763  reccn2  15764  rlimno1  15821  o1fsum  15980  expcnv  16033  geolim  16039  geolim2  16040  georeclim  16041  geomulcvg  16045  geoisumr  16047  geoisum1c  16049  fprodge0  16160  fprodge1  16162  rerisefaccl  16184  refallfaccl  16185  ere  16255  ege2le3  16256  efgt1  16284  resin4p  16306  recos4p  16307  tanhbnd  16329  sinbnd  16348  cosbnd  16349  sinbnd2  16350  cosbnd2  16351  ef01bndlem  16352  sin01bnd  16353  cos01bnd  16354  cos1bnd  16355  cos2bnd  16356  sinltx  16357  sin01gt0  16358  cos01gt0  16359  sin02gt0  16360  sincos1sgn  16361  ene1  16378  rpnnen2lem2  16383  rpnnen2lem3  16384  rpnnen2lem4  16385  rpnnen2lem9  16390  rpnnen2lem12  16393  ruclem6  16403  ruclem11  16408  ruclem12  16409  3dvds  16501  flodddiv4  16585  sadcadd  16628  isprm3  16858  sqnprm  16878  coprm  16887  phibndlem  16947  pythagtriplem3  16996  pcmpt  17070  fldivp1  17075  pockthi  17085  infpn2  17091  basendxnmulrndx  17467  starvndxnbasendx  17475  scandxnbasendx  17487  vscandxnbasendx  17492  ipndxnbasendx  17503  basendxnocndx  17554  slotsbhcdif  17586  lt6abl  20109  srgbinomlem4  20455  0ringnnzr  20776  abvneg  21083  abvtrivd  21089  prmidl0  21634  xrsmcmn  21701  xrsnsgrp  21714  gzrngunitlem  21738  gzrngunit  21739  rge0srg  21744  psgnodpmr  21896  remulg  21913  resubdrg  21914  psdmvr  22490  dscmet  24891  dscopn  24892  nrginvrcnlem  25010  idnghm  25062  tgioo  25115  blcvx  25117  iicmp  25207  iiconn  25208  iirev  25250  iihalf1  25252  iihalf2  25254  elii1  25256  elii2  25257  iimulcl  25258  icopnfcnv  25263  icopnfhmeo  25264  iccpnfhmeo  25266  xrhmeo  25267  xrhmph  25268  evth  25280  xlebnum  25286  htpycc  25301  reparphti  25318  pcoval1  25334  pco1  25336  pcoval2  25337  pcocn  25338  pcohtpylem  25340  pcopt  25343  pcopt2  25344  pcoass  25345  pcorevlem  25347  nmhmcn  25441  ncvs1  25478  ovolunlem1a  25817  vitalilem2  25930  vitalilem4  25932  vitalilem5  25933  vitali  25934  i1f1  26011  itg11  26012  itg2const  26061  dveflem  26299  dvlipcn  26314  dvcvx  26340  ply1remlem  26483  fta1blem  26489  plyn0mulidp  26602  plymulidp  26603  vieta1lem2  26634  aalioulem3  26661  aalioulem5  26663  aaliou3lem2  26670  ulmbdd  26725  iblulm  26734  radcnvlem1  26740  dvradcnv  26748  abelthlem2  26759  abelthlem3  26760  abelthlem5  26762  abelthlem7  26765  abelth  26768  abelth2  26769  reeff1olem  26773  reeff1o  26774  sinhalfpilem  26792  tangtx  26834  sincos4thpi  26842  pige3ALT  26848  coskpi  26851  cos0pilt1  26860  recosf1o  26863  tanregt0  26867  efif1olem3  26872  efif1olem4  26873  loge  26914  logdivlti  26948  logcnlem4  26973  logf1o2  26978  logtayl  26988  logccv  26991  recxpcl  27003  cxplea  27024  cxpcn3lem  27075  cxpaddlelem  27079  loglesqrt  27089  ang180lem2  27138  angpined  27158  acosrecl  27231  atancj  27238  atanlogaddlem  27241  atantan  27251  atans2  27259  ressatans  27262  leibpi  27270  log2le1  27278  birthdaylem3  27281  cxp2lim  27304  cxploglim  27305  cxploglim2  27306  divsqrtsumlem  27307  cvxcl  27312  scvxcvx  27313  jensenlem2  27315  amgmlem  27317  emcllem2  27324  emcllem4  27326  emcllem6  27328  emcllem7  27329  emre  27333  emgt0  27334  harmonicbnd3  27335  harmonicubnd  27337  harmonicbnd4  27338  zetacvg  27342  ftalem1  27400  ftalem2  27401  ftalem5  27404  issqf  27463  cht1  27492  chp1  27494  ppiltx  27504  mumullem2  27507  ppiublem1  27529  ppiub  27531  chtublem  27538  chtub  27539  logfacbnd3  27550  logexprlim  27552  perfectlem2  27557  dchrinv  27588  dchr1re  27590  efexple  27608  bposlem1  27611  bposlem2  27612  bposlem5  27615  bposlem8  27618  lgsdir2lem1  27652  lgsdir2lem5  27656  lgsdir  27659  lgsne0  27662  lgsabs1  27663  lgsdinn0  27672  gausslemma2dlem0i  27691  lgseisen  27706  m1lgs  27715  2lgslem3  27731  addsq2nreurex  27771  2sqreultblem  27775  2sqreunnltblem  27778  chebbnd1lem3  27798  chebbnd1  27799  chtppilimlem1  27800  chtppilimlem2  27801  chtppilim  27802  chpchtlim  27806  vmadivsumb  27810  rplogsumlem2  27812  rpvmasumlem  27814  dchrmusumlema  27820  dchrmusum2  27821  dchrvmasumlem2  27825  dchrvmasumiflem1  27828  dchrisum0flblem1  27835  dchrisum0flblem2  27836  dchrisum0fno1  27838  rpvmasum2  27839  dchrisum0re  27840  dchrisum0lema  27841  dchrisum0lem1b  27842  dchrisum0lem1  27843  dchrisum0lem2a  27844  dchrisum0lem2  27845  logdivsum  27860  mulog2sumlem2  27862  2vmadivsumlem  27867  log2sumbnd  27871  selbergb  27876  selberg2b  27879  chpdifbndlem1  27880  selberg3lem1  27884  selberg3lem2  27885  selberg4lem1  27887  pntrmax  27891  pntrsumo1  27892  selbergsb  27902  pntrlog2bndlem3  27906  pntrlog2bndlem5  27908  pntpbnd1a  27912  pntpbnd2  27914  pntibndlem1  27916  pntibndlem3  27919  pntlemd  27921  pntlemc  27922  pntlemb  27924  pntlemr  27929  pntlemf  27932  pntlemk  27933  pntlemo  27934  pntlem3  27936  pntleml  27938  abvcxp  27942  ostth2lem1  27945  ostth1  27960  ostth2lem2  27961  ostth2lem3  27962  ostth2lem4  27963  ostth2  27964  ostth3  27965  ostth  27966  slotsinbpsd  28903  slotslnbpsd  28904  trgcgrg  28978  brbtwn2  29483  colinearalglem4  29487  ax5seglem2  29507  ax5seglem3  29509  axpaschlem  29518  axpasch  29519  axlowdimlem6  29525  axlowdimlem10  29529  axlowdimlem16  29535  axlowdim1  29537  axlowdim2  29538  axlowdim  29539  axcontlem2  29543  elntg2  29563  lfgrnloop  29703  lfuhgr1v0e  29835  usgrexmpldifpr  29839  usgrexmplef  29840  1loopgrvd2  30084  vdegp1bi  30118  lfgrwlkprop  30270  pthdlem1  30352  pthdlem2  30354  clwlkclwwlkf  30599  upgr4cycl4dv4e  30786  konigsberglem2  30854  konigsberglem3  30855  konigsberglem5  30857  frgrreg  30995  ex-dif  31024  ex-in  31026  ex-pss  31029  ex-res  31042  ex-fl  31048  nv1  31277  smcnlem  31299  ipidsq  31312  nmlno0lem  31395  norm-ii-i  31739  bcs2  31784  norm1  31851  nmopub2tALT  32511  nmfnleub2  32528  nmlnop0iALT  32597  unopbd  32617  nmopadjlem  32691  nmopcoadji  32703  pjnmopi  32750  pjbdlni  32751  hstle1  32828  hstle  32832  hstles  32833  stge1i  32840  stlesi  32843  staddi  32848  stadd3i  32850  strlem1  32852  strlem5  32857  jplem1  32870  cdj1i  33035  addltmulALT  33048  xlt2addrd  33351  sgnmulsgp  33423  dp2lt10  33450  dp2ltsuc  33452  dp2ltc  33453  dplti  33471  dpmul4  33480  cshw1s2  33521  xrsmulgzz  33570  rearchi  33907  xrge0slmod  33909  evl1deg3  34110  constrconj  34377  2sqr3minply  34412  submateqlem1  34439  xrge0iifcnv  34565  xrge0iifcv  34566  xrge0iifiso  34567  xrge0iifhom  34569  zrhre  34651  esumcst  34695  cntnevol  34861  omssubadd  34932  iwrdsplit  35019  dstfrvclim1  35110  coinfliprv  35115  ballotlem2  35121  ballotlem4  35131  ballotlemi1  35135  ballotlemic  35139  signswch  35190  signstf  35195  signsvfn  35211  itgexpif  35235  hgt750lemd  35277  logdivsqrle  35279  hgt750lem  35280  hgt750lem2  35281  hgt750leme  35287  tgoldbachgnn  35288  subfacp1lem1  35944  subfacp1lem5  35949  resconn  36011  iisconn  36017  iillysconn  36018  problem2  36431  problem3  36432  sinccvglem  36437  fz0n  36496  dnibndlem12  37355  knoppcnlem4  37362  knoppndvlem13  37390  cnndvlem1  37403  irrdiff  38247  relowlpssretop  38287  sin2h  38533  cos2h  38534  tan2h  38535  poimirlem7  38545  poimirlem16  38554  poimirlem17  38555  poimirlem19  38557  poimirlem20  38558  poimirlem22  38560  poimirlem23  38561  poimirlem29  38567  poimirlem31  38569  itg2addnclem3  38591  asindmre  38621  dvasin  38622  dvacos  38623  dvreasin  38624  dvreacos  38625  fdc  38679  geomcau  38693  cntotbnd  38730  heiborlem8  38752  bfplem2  38757  bfp  38758  aks4d1p1p7  43124  ine1  43371  re1m1e0m0  43448  sn-00idlem1  43449  sn-00idlem2  43450  remul02  43456  sn-0ne2  43457  reixi  43474  rei4  43475  remullid  43485  ipiiie0  43489  sn-0tie0  43515  sn-nnne0  43524  mulgt0b1d  43536  sn-0lt1  43539  sn-ltp1  43540  reneg1lt0  43544  sn-inelr  43551  rabren3dioph  43821  pellexlem5  43839  pellexlem6  43840  pell1qrgaplem  43879  pell14qrgap  43881  pellqrex  43885  pellfundre  43887  pellfundlb  43890  pellfund14gap  43893  jm2.17a  43966  acongeq  43989  jm2.23  44002  jm3.1lem2  44024  sqrtcval  44640  sqrtcval2  44641  resqrtval  44642  imsqrtval  44643  relexp01min  44712  cvgdvgrat  45296  lhe4.4ex1a  45312  binomcxplemnotnn0  45339  isosctrlem1ALT  45915  supxrgelem  46348  xrlexaddrp  46363  infxr  46377  infleinflem2  46381  sumnnodd  46641  limsup10exlem  46781  limsup10ex  46782  dvnprodlem3  46957  stoweidlem1  47010  stoweidlem18  47027  stoweidlem19  47028  stoweidlem26  47035  stoweidlem34  47043  stoweidlem40  47049  stoweidlem41  47050  stoweidlem59  47068  stoweid  47072  stirlinglem10  47092  stirlinglem11  47093  dirkercncflem1  47112  fourierdlem16  47132  fourierdlem21  47137  fourierdlem22  47138  fourierdlem42  47158  fourierdlem68  47183  fourierdlem83  47198  fourierdlem103  47218  sqwvfourb  47238  fouriersw  47240  etransclem23  47266  salgencntex  47352  ovn0lem  47574  smfmullem3  47802  smfmullem4  47803  numtowerdt  47915  goldratval  47935  cjnpoly  47938  zm1nn  48371  ceilhalf1  48407  m1mod0mod1  48429  muldvdsfacgt  48455  fmtnosqrt  48623  nprmdvdsfacm1lem4  48707  perfectALTVlem2  48819  2exp340mod341  48830  8exp8mod9  48833  nfermltl8rev  48839  nnsum3primesprm  48887  nnsum4primesodd  48893  nnsum4primesoddALTV  48894  nnsum4primeseven  48897  nnsum4primesevenALTV  48898  tgblthelfgott  48912  tgoldbach  48914  usgrexmpl1lem  49118  usgrexmpl2lem  49123  usgrexmpl2nb1  49129  usgrexmpl2nb3  49131  usgrexmpl2nb4  49132  usgrexmpl2nb5  49133  usgrexmpl2trifr  49134  gpg3kgrtriexlem3  49182  pgnbgreunbgrlem2lem1  49211  pgnbgreunbgrlem2lem2  49212  rege1logbrege0  49669  rege1logbzge0  49670  blennnelnn  49687  dignnld  49714  nn0sumshdiglemA  49730  nn0sumshdiglem1  49732  rrx2xpref1o  49829  rrxlines  49844  eenglngeehlnmlem1  49848  eenglngeehlnmlem2  49849  line2ylem  49862  line2x  49865  icccldii  50026  io1ii  50028  sepfsepc  50035  1ne3  50940  veronesev1lem  50972  veronesev4lem  50975  veronesev5lem  50976  veronesev6lem  50977  veronesevrowd  50978  veronesematrowd  50980  veroquadgsumlem  50982  veroquadmodzerod  50983  veroquadnolindfd  50984