Theorem 1re 11225

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 11175, 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 11186	. . 3 ⊢ 1 ≠ 0
2		ax-1cn 11175	. . . . 5 ⊢ 1 ∈ ℂ
3		cnre 11222	. . . . 5 ⊢ (1 ∈ ℂ → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)))
4	2, 3	ax-mp 5	. . . 4 ⊢ ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏))
5		neeq1 3022	. . . . . . . 8 ⊢ (1 = (𝑎 + (i · 𝑏)) → (1 ≠ 0 ↔ (𝑎 + (i · 𝑏)) ≠ 0))
6	5	biimpcd 252	. . . . . . 7 ⊢ (1 ≠ 0 → (1 = (𝑎 + (i · 𝑏)) → (𝑎 + (i · 𝑏)) ≠ 0))
7		0cn 11215	. . . . . . . 8 ⊢ 0 ∈ ℂ
8		cnre 11222	. . . . . . . 8 ⊢ (0 ∈ ℂ → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)))
9	7, 8	ax-mp 5	. . . . . . 7 ⊢ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑))
10		neeq2 3023	. . . . . . . . . 10 ⊢ (0 = (𝑐 + (i · 𝑑)) → ((𝑎 + (i · 𝑏)) ≠ 0 ↔ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
11	10	biimpcd 252	. . . . . . . . 9 ⊢ ((𝑎 + (i · 𝑏)) ≠ 0 → (0 = (𝑐 + (i · 𝑑)) → (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
12	11	reximdv 3182	. . . . . . . 8 ⊢ ((𝑎 + (i · 𝑏)) ≠ 0 → (∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)) → ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
13	12	reximdv 3182	. . . . . . 7 ⊢ ((𝑎 + (i · 𝑏)) ≠ 0 → (∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)) → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
14	6, 9, 13	syl6mpi 68	. . . . . 6 ⊢ (1 ≠ 0 → (1 = (𝑎 + (i · 𝑏)) → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
15	14	reximdv 3182	. . . . 5 ⊢ (1 ≠ 0 → (∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)) → ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
16	15	reximdv 3182	. . . 4 ⊢ (1 ≠ 0 → (∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)) → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
17	4, 16	mpi 21	. . 3 ⊢ (1 ≠ 0 → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)))
18		id 23	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑐 → 𝑎 = 𝑐)
19		oveq2 7427	. . . . . . . . . . . 12 ⊢ (𝑏 = 𝑑 → (i · 𝑏) = (i · 𝑑))
20	18, 19	oveqan12d 7438	. . . . . . . . . . 11 ⊢ ((𝑎 = 𝑐 ∧ 𝑏 = 𝑑) → (𝑎 + (i · 𝑏)) = (𝑐 + (i · 𝑑)))
21	20	expcom 419	. . . . . . . . . 10 ⊢ (𝑏 = 𝑑 → (𝑎 = 𝑐 → (𝑎 + (i · 𝑏)) = (𝑐 + (i · 𝑑))))
22	21	necon3d 2981	. . . . . . . . 9 ⊢ (𝑏 = 𝑑 → ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → 𝑎 ≠ 𝑐))
23	22	com12 33	. . . . . . . 8 ⊢ ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → (𝑏 = 𝑑 → 𝑎 ≠ 𝑐))
24	23	necon3bd 2974	. . . . . . 7 ⊢ ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → (¬ 𝑎 ≠ 𝑐 → 𝑏 ≠ 𝑑))
25	24	orrd 877	. . . . . 6 ⊢ ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → (𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑))
26		neeq1 3022	. . . . . . . . . 10 ⊢ (𝑥 = 𝑎 → (𝑥 ≠ 𝑦 ↔ 𝑎 ≠ 𝑦))
27		neeq2 3023	. . . . . . . . . 10 ⊢ (𝑦 = 𝑐 → (𝑎 ≠ 𝑦 ↔ 𝑎 ≠ 𝑐))
28	26, 27	rspc2ev 3596	. . . . . . . . 9 ⊢ ((𝑎 ∈ ℝ ∧ 𝑐 ∈ ℝ ∧ 𝑎 ≠ 𝑐) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦)
29	28	3expia 1139	. . . . . . . 8 ⊢ ((𝑎 ∈ ℝ ∧ 𝑐 ∈ ℝ) → (𝑎 ≠ 𝑐 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
30	29	ad2ant2r 760	. . . . . . 7 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → (𝑎 ≠ 𝑐 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
31		neeq1 3022	. . . . . . . . . 10 ⊢ (𝑥 = 𝑏 → (𝑥 ≠ 𝑦 ↔ 𝑏 ≠ 𝑦))
32		neeq2 3023	. . . . . . . . . 10 ⊢ (𝑦 = 𝑑 → (𝑏 ≠ 𝑦 ↔ 𝑏 ≠ 𝑑))
33	31, 32	rspc2ev 3596	. . . . . . . . 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 3224	. . . 4 ⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
39	38	rexlimivv 3209	. . 3 ⊢ (∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦)
40	1, 17, 39	mp2b 10	. 2 ⊢ ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦
41		eqtr3 2787	. . . . . . . . 9 ⊢ ((𝑥 = 0 ∧ 𝑦 = 0) → 𝑥 = 𝑦)
42	41	ex 418	. . . . . . . 8 ⊢ (𝑥 = 0 → (𝑦 = 0 → 𝑥 = 𝑦))
43	42	necon3d 2981	. . . . . . 7 ⊢ (𝑥 = 0 → (𝑥 ≠ 𝑦 → 𝑦 ≠ 0))
44		neeq1 3022	. . . . . . . . 9 ⊢ (𝑧 = 𝑦 → (𝑧 ≠ 0 ↔ 𝑦 ≠ 0))
45	44	rspcev 3583	. . . . . . . 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 3022	. . . . . . . 8 ⊢ (𝑧 = 𝑥 → (𝑧 ≠ 0 ↔ 𝑥 ≠ 0))
51	50	rspcev 3583	. . . . . . 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 3043	. . 3 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
56	55	rexlimivv 3209	. 2 ⊢ (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)
57		ax-rrecex 11189	. . . 4 ⊢ ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → ∃𝑥 ∈ ℝ (𝑧 · 𝑥) = 1)
58		remulcl 11202	. . . . . . 7 ⊢ ((𝑧 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (𝑧 · 𝑥) ∈ ℝ)
59	58	adantlr 728	. . . . . 6 ⊢ (((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) ∧ 𝑥 ∈ ℝ) → (𝑧 · 𝑥) ∈ ℝ)
60		eleq1 2853	. . . . . 6 ⊢ ((𝑧 · 𝑥) = 1 → ((𝑧 · 𝑥) ∈ ℝ ↔ 1 ∈ ℝ))
61	59, 60	syl5ibcom 248	. . . . 5 ⊢ (((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) ∧ 𝑥 ∈ ℝ) → ((𝑧 · 𝑥) = 1 → 1 ∈ ℝ))
62	61	rexlimdva 3168	. . . 4 ⊢ ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → (∃𝑥 ∈ ℝ (𝑧 · 𝑥) = 1 → 1 ∈ ℝ))
63	57, 62	mpd 16	. . 3 ⊢ ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → 1 ∈ ℝ)
64	63	rexlimiva 3160	. 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 2146   ≠ wne 2960  ∃wrex 3091  (class class class)co 7419  ℂcc 11115  ℝcr 11116  0cc0 11117  1c1 11118  ici 11119   + caddc 11120   · cmul 11122

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 2148  ax-9 2156  ax-ext 2737  ax-1cn 11175  ax-icn 11176  ax-addcl 11177  ax-mulcl 11179  ax-mulrcl 11180  ax-i2m1 11185  ax-1ne0 11186  ax-rrecex 11189  ax-cnre 11190

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 2744  df-cleq 2757  df-clel 2840  df-ne 2961  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-iota 6496  df-fv 6548  df-ov 7422

This theorem is used by:  1red  11226  pr01ssre  11229  1xr  11285  dedekind  11390  peano2re  11400  mul02lem2  11404  addrid  11407  renegcl  11538  peano2rem  11542  0reALT  11572  0lt1  11753  0le1  11754  relin01  11755  1le1  11859  eqneg  11952  ltp1  12072  ltm1  12074  recgt0  12078  ltmulgt11  12091  lemulge11  12094  reclt1  12127  recgt1  12128  recgt1i  12129  recp1lt1  12130  recreclt  12131  recgt0ii  12138  ledivp1i  12157  ltdivp1i  12158  neg1rr  12221  neg1lt0  12223  cju  12231  indf  12241  indfval  12242  nnssre  12254  nnge1  12281  nngt1ne1  12282  nnle1eq1  12283  nngt0  12284  nnnlt1  12285  nnne0  12287  nnrecre  12295  nnrecgt0  12296  nnsub  12297  1t1e1ALT  12308  2re  12332  3re  12338  4re  12342  5re  12345  6re  12348  7re  12351  8re  12354  9re  12357  0le2OLD  12361  2posOLD  12363  1lt2  12430  1lt3  12433  1lt4  12436  1lt5  12440  1lt6  12445  1lt7  12451  1lt8  12458  1lt9  12466  1ne2  12468  1le2  12469  1le3  12472  halflt1  12478  addltmul  12497  nnunb  12517  elnnnn0c  12566  nn0ge2m1nn  12591  elnnz1  12637  znnnlt1  12638  zltp1le  12661  zleltp1  12662  nn0lt2  12677  recnz  12689  gtndiv  12691  3halfnz  12693  10re  12752  1lt10  12874  1lt10OLD  12875  eluzp1m1  12906  eluzp1p1  12908  eluz2b2  12963  zbtwnre  12988  rebtwnz  12989  1rp  13038  divlt1lt  13105  divle1le  13106  nnledivrp  13148  qbtwnxr  13244  xmulrid  13323  xmulm1  13325  x2times  13343  xrub  13356  elicc01  13511  1elunit  13515  divelunit  13539  lincmb01cmp  13540  unitssre  13544  0nelfz1  13589  fzpreddisj  13620  fznatpl1  13625  fztpval  13633  fraclt1  13855  fracle1  13856  flbi2  13870  fldiv4p1lem1div2  13888  fldiv4lem1div2  13890  fldiv  13913  modid  13949  1mod  13956  m1modnnsub1  13973  modm1p1mod0  13978  seqf1olem1  14097  reexpcl  14134  reexpclz  14138  expge0  14154  expge1  14155  expgt1  14156  bernneq  14285  bernneq2  14286  expnbnd  14288  expnlbnd  14289  expnlbnd2  14290  expmulnbnd  14291  discr1  14295  facwordi  14345  faclbnd3  14348  faclbnd4lem1  14349  faclbnd4lem4  14352  faclbnd6  14355  facavg  14357  hashv01gt1  14401  hashnn0n0nn  14447  hashunsnggt  14450  hash1snb  14476  hashgt12el  14479  hashgt12el2  14480  hashfun  14494  hashge2el2dif  14537  tpf1ofv2  14555  lsw0  14622  f1oun2prg  14980  sgnclre  15165  sgnnbi  15167  sgnpbi  15168  cjexp  15227  re1  15231  im1  15232  rei  15233  imi  15234  01sqrexlem1  15319  01sqrexlem2  15320  01sqrexlem3  15321  01sqrexlem4  15322  01sqrexlem7  15325  resqrex  15327  sqrt1  15348  sqrt2gt1lt2  15351  sqrtm1  15352  abs1  15374  absrdbnd  15419  caubnd2  15435  mulcn2  15673  reccn2  15674  rlimno1  15731  o1fsum  15890  expcnv  15943  geolim  15949  geolim2  15950  georeclim  15951  geomulcvg  15955  geoisumr  15957  geoisum1c  15959  fprodge0  16072  fprodge1  16074  rerisefaccl  16096  refallfaccl  16097  ere  16167  ege2le3  16168  efgt1  16196  resin4p  16218  recos4p  16219  tanhbnd  16241  sinbnd  16260  cosbnd  16261  sinbnd2  16262  cosbnd2  16263  ef01bndlem  16264  sin01bnd  16265  cos01bnd  16266  cos1bnd  16267  cos2bnd  16268  sinltx  16269  sin01gt0  16270  cos01gt0  16271  sin02gt0  16272  sincos1sgn  16273  ene1  16290  rpnnen2lem2  16295  rpnnen2lem3  16296  rpnnen2lem4  16297  rpnnen2lem9  16302  rpnnen2lem12  16305  ruclem6  16315  ruclem11  16320  ruclem12  16321  3dvds  16413  flodddiv4  16497  sadcadd  16540  isprm3  16765  sqnprm  16785  coprm  16794  phibndlem  16853  pythagtriplem3  16902  pcmpt  16976  fldivp1  16981  pockthi  16991  infpn2  16997  basendxnmulrndx  17373  starvndxnbasendx  17381  scandxnbasendx  17393  vscandxnbasendx  17398  ipndxnbasendx  17409  basendxnocndx  17460  slotsbhcdif  17492  lt6abl  20011  srgbinomlem4  20357  0ringnnzr  20675  abvneg  20981  abvtrivd  20987  prmidl0  21530  xrsmcmn  21597  xrsnsgrp  21610  gzrngunitlem  21634  gzrngunit  21635  rge0srg  21640  psgnodpmr  21792  remulg  21809  resubdrg  21810  psdmvr  22384  dscmet  24782  dscopn  24783  nrginvrcnlem  24901  idnghm  24953  tgioo  25006  blcvx  25008  iicmp  25098  iiconn  25099  iirev  25141  iihalf1  25143  iihalf2  25145  elii1  25147  elii2  25148  iimulcl  25149  icopnfcnv  25154  icopnfhmeo  25155  iccpnfhmeo  25157  xrhmeo  25158  xrhmph  25159  evth  25171  xlebnum  25177  htpycc  25192  reparphti  25209  pcoval1  25225  pco1  25227  pcoval2  25228  pcocn  25229  pcohtpylem  25231  pcopt  25234  pcopt2  25235  pcoass  25236  pcorevlem  25238  nmhmcn  25332  ncvs1  25369  ovolunlem1a  25708  vitalilem2  25821  vitalilem4  25823  vitalilem5  25824  vitali  25825  i1f1  25902  itg11  25903  itg2const  25952  dveflem  26191  dvlipcn  26206  dvcvx  26232  ply1remlem  26375  fta1blem  26381  plyn0mulidp  26495  plymulidp  26496  vieta1lem2  26525  aalioulem3  26550  aalioulem5  26552  aaliou3lem2  26559  ulmbdd  26614  iblulm  26623  radcnvlem1  26629  dvradcnv  26637  abelthlem2  26648  abelthlem3  26649  abelthlem5  26651  abelthlem7  26654  abelth  26657  abelth2  26658  reeff1olem  26662  reeff1o  26663  sinhalfpilem  26681  tangtx  26723  sincos4thpi  26731  pige3ALT  26738  coskpi  26741  cos0pilt1  26750  recosf1o  26753  tanregt0  26757  efif1olem3  26762  efif1olem4  26763  loge  26804  logdivlti  26838  logcnlem4  26863  logf1o2  26868  logtayl  26878  logccv  26881  recxpcl  26893  cxplea  26914  cxpcn3lem  26965  cxpaddlelem  26969  loglesqrt  26979  ang180lem2  27028  angpined  27048  acosrecl  27121  atancj  27128  atanlogaddlem  27131  atantan  27141  atans2  27149  ressatans  27152  leibpi  27160  log2le1  27168  birthdaylem3  27171  cxp2lim  27194  cxploglim  27195  cxploglim2  27196  divsqrtsumlem  27197  cvxcl  27202  scvxcvx  27203  jensenlem2  27205  amgmlem  27207  emcllem2  27214  emcllem4  27216  emcllem6  27218  emcllem7  27219  emre  27223  emgt0  27224  harmonicbnd3  27225  harmonicubnd  27227  harmonicbnd4  27228  zetacvg  27232  ftalem1  27290  ftalem2  27291  ftalem5  27294  issqf  27353  cht1  27382  chp1  27384  ppiltx  27394  mumullem2  27397  ppiublem1  27419  ppiub  27421  chtublem  27428  chtub  27429  logfacbnd3  27440  logexprlim  27442  perfectlem2  27447  dchrinv  27478  dchr1re  27480  efexple  27498  bposlem1  27501  bposlem2  27502  bposlem5  27505  bposlem8  27508  lgsdir2lem1  27542  lgsdir2lem5  27546  lgsdir  27549  lgsne0  27552  lgsabs1  27553  lgsdinn0  27562  gausslemma2dlem0i  27581  lgseisen  27596  m1lgs  27605  2lgslem3  27621  addsq2nreurex  27661  2sqreultblem  27665  2sqreunnltblem  27668  chebbnd1lem3  27688  chebbnd1  27689  chtppilimlem1  27690  chtppilimlem2  27691  chtppilim  27692  chpchtlim  27696  vmadivsumb  27700  rplogsumlem2  27702  rpvmasumlem  27704  dchrmusumlema  27710  dchrmusum2  27711  dchrvmasumlem2  27715  dchrvmasumiflem1  27718  dchrisum0flblem1  27725  dchrisum0flblem2  27726  dchrisum0fno1  27728  rpvmasum2  27729  dchrisum0re  27730  dchrisum0lema  27731  dchrisum0lem1b  27732  dchrisum0lem1  27733  dchrisum0lem2a  27734  dchrisum0lem2  27735  logdivsum  27750  mulog2sumlem2  27752  2vmadivsumlem  27757  log2sumbnd  27761  selbergb  27766  selberg2b  27769  chpdifbndlem1  27770  selberg3lem1  27774  selberg3lem2  27775  selberg4lem1  27777  pntrmax  27781  pntrsumo1  27782  selbergsb  27792  pntrlog2bndlem3  27796  pntrlog2bndlem5  27798  pntpbnd1a  27802  pntpbnd2  27804  pntibndlem1  27806  pntibndlem3  27809  pntlemd  27811  pntlemc  27812  pntlemb  27814  pntlemr  27819  pntlemf  27822  pntlemk  27823  pntlemo  27824  pntlem3  27826  pntleml  27828  abvcxp  27832  ostth2lem1  27835  ostth1  27850  ostth2lem2  27851  ostth2lem3  27852  ostth2lem4  27853  ostth2  27854  ostth3  27855  ostth  27856  slotsinbpsd  28763  slotslnbpsd  28764  trgcgrg  28837  brbtwn2  29312  colinearalglem4  29316  ax5seglem2  29336  ax5seglem3  29338  axpaschlem  29347  axpasch  29348  axlowdimlem6  29354  axlowdimlem10  29358  axlowdimlem16  29364  axlowdim1  29366  axlowdim2  29367  axlowdim  29368  axcontlem2  29372  elntg2  29392  lfgrnloop  29532  lfuhgr1v0e  29664  usgrexmpldifpr  29668  usgrexmplef  29669  1loopgrvd2  29913  vdegp1bi  29947  lfgrwlkprop  30099  pthdlem1  30181  pthdlem2  30183  clwlkclwwlkf  30428  upgr4cycl4dv4e  30609  konigsberglem2  30677  konigsberglem3  30678  konigsberglem5  30680  frgrreg  30818  ex-dif  30847  ex-in  30849  ex-pss  30852  ex-res  30865  ex-fl  30871  nv1  31100  smcnlem  31122  ipidsq  31135  nmlno0lem  31218  norm-ii-i  31562  bcs2  31607  norm1  31674  nmopub2tALT  32334  nmfnleub2  32351  nmlnop0iALT  32420  unopbd  32440  nmopadjlem  32514  nmopcoadji  32526  pjnmopi  32573  pjbdlni  32574  hstle1  32651  hstle  32655  hstles  32656  stge1i  32663  stlesi  32666  staddi  32671  stadd3i  32673  strlem1  32675  strlem5  32680  jplem1  32693  cdj1i  32858  addltmulALT  32871  xlt2addrd  33176  sgnmulsgp  33248  dp2lt10  33275  dp2ltsuc  33277  dp2ltc  33278  dplti  33296  dpmul4  33305  cshw1s2  33346  xrsmulgzz  33395  rearchi  33732  xrge0slmod  33734  evl1deg3  33934  constrconj  34201  2sqr3minply  34236  submateqlem1  34263  xrge0iifcnv  34389  xrge0iifcv  34390  xrge0iifiso  34391  xrge0iifhom  34393  zrhre  34475  esumcst  34519  cntnevol  34685  omssubadd  34757  iwrdsplit  34844  dstfrvclim1  34935  coinfliprv  34940  ballotlem2  34946  ballotlem4  34956  ballotlemi1  34960  ballotlemic  34964  signswch  35015  signstf  35020  signsvfn  35036  itgexpif  35060  hgt750lemd  35102  logdivsqrle  35104  hgt750lem  35105  hgt750lem2  35106  hgt750leme  35112  tgoldbachgnn  35113  subfacp1lem1  35710  subfacp1lem5  35715  resconn  35777  iisconn  35783  iillysconn  35784  problem2  36197  problem3  36198  sinccvglem  36203  fz0n  36262  dnibndlem12  37137  knoppcnlem4  37144  knoppndvlem13  37172  cnndvlem1  37185  irrdiff  38029  relowlpssretop  38069  sin2h  38320  cos2h  38321  tan2h  38322  poimirlem7  38337  poimirlem16  38346  poimirlem17  38347  poimirlem19  38349  poimirlem20  38350  poimirlem22  38352  poimirlem23  38353  poimirlem29  38359  poimirlem31  38361  itg2addnclem3  38383  asindmre  38413  dvasin  38414  dvacos  38415  dvreasin  38416  dvreacos  38417  fdc  38456  geomcau  38470  cntotbnd  38507  heiborlem8  38529  bfplem2  38534  bfp  38535  aks4d1p1p7  42901  ine1  43135  re1m1e0m0  43218  sn-00idlem1  43219  sn-00idlem2  43220  remul02  43226  sn-0ne2  43227  reixi  43244  rei4  43245  remullid  43255  ipiiie0  43259  sn-0tie0  43285  sn-nnne0  43294  mulgt0b1d  43306  sn-0lt1  43309  sn-ltp1  43310  reneg1lt0  43314  sn-inelr  43321  rabren3dioph  43602  pellexlem5  43620  pellexlem6  43621  pell1qrgaplem  43660  pell14qrgap  43662  pellqrex  43666  pellfundre  43668  pellfundlb  43671  pellfund14gap  43674  jm2.17a  43747  acongeq  43770  jm2.23  43783  jm3.1lem2  43805  sqrtcval  44427  sqrtcval2  44428  resqrtval  44429  imsqrtval  44430  relexp01min  44499  cvgdvgrat  45083  lhe4.4ex1a  45099  binomcxplemnotnn0  45126  isosctrlem1ALT  45702  supxrgelem  46113  xrlexaddrp  46128  infxr  46142  infleinflem2  46146  sumnnodd  46406  limsup10exlem  46546  limsup10ex  46547  dvnprodlem3  46722  stoweidlem1  46775  stoweidlem18  46792  stoweidlem19  46793  stoweidlem26  46800  stoweidlem34  46808  stoweidlem40  46814  stoweidlem41  46815  stoweidlem59  46833  stoweid  46837  stirlinglem10  46857  stirlinglem11  46858  dirkercncflem1  46877  fourierdlem16  46897  fourierdlem21  46902  fourierdlem22  46903  fourierdlem42  46923  fourierdlem68  46948  fourierdlem83  46963  fourierdlem103  46983  sqwvfourb  47003  fouriersw  47005  etransclem23  47031  salgencntex  47117  ovn0lem  47339  smfmullem3  47567  smfmullem4  47568  nthrucw  47667  cjnpoly  47686  zm1nn  48099  ceilhalf1  48135  m1mod0mod1  48157  muldvdsfacgt  48183  fmtnosqrt  48351  nprmdvdsfacm1lem4  48435  perfectALTVlem2  48547  2exp340mod341  48558  8exp8mod9  48561  nfermltl8rev  48567  nnsum3primesprm  48615  nnsum4primesodd  48621  nnsum4primesoddALTV  48622  nnsum4primeseven  48625  nnsum4primesevenALTV  48626  tgblthelfgott  48640  tgoldbach  48642  usgrexmpl1lem  48846  usgrexmpl2lem  48851  usgrexmpl2nb1  48857  usgrexmpl2nb3  48859  usgrexmpl2nb4  48860  usgrexmpl2nb5  48861  usgrexmpl2trifr  48862  gpg3kgrtriexlem3  48910  pgnbgreunbgrlem2lem1  48939  pgnbgreunbgrlem2lem2  48940  rege1logbrege0  49397  rege1logbzge0  49398  blennnelnn  49415  dignnld  49442  nn0sumshdiglemA  49458  nn0sumshdiglem1  49460  rrx2xpref1o  49557  rrxlines  49572  eenglngeehlnmlem1  49576  eenglngeehlnmlem2  49577  line2ylem  49590  line2x  49593  icccldii  49756  io1ii  49758  sepfsepc  49765  1ne3  50682