Theorem 1re 11347

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 11297, 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 11308	. . 3 ⊢ 1 ≠ 0
2		ax-1cn 11297	. . . . 5 ⊢ 1 ∈ ℂ
3		cnre 11344	. . . . 5 ⊢ (1 ∈ ℂ → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)))
4	2, 3	ax-mp 5	. . . 4 ⊢ ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏))
5		neeq1 3021	. . . . . . . 8 ⊢ (1 = (𝑎 + (i · 𝑏)) → (1 ≠ 0 ↔ (𝑎 + (i · 𝑏)) ≠ 0))
6	5	biimpcd 252	. . . . . . 7 ⊢ (1 ≠ 0 → (1 = (𝑎 + (i · 𝑏)) → (𝑎 + (i · 𝑏)) ≠ 0))
7		0cn 11337	. . . . . . . 8 ⊢ 0 ∈ ℂ
8		cnre 11344	. . . . . . . 8 ⊢ (0 ∈ ℂ → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)))
9	7, 8	ax-mp 5	. . . . . . 7 ⊢ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑))
10		neeq2 3022	. . . . . . . . . 10 ⊢ (0 = (𝑐 + (i · 𝑑)) → ((𝑎 + (i · 𝑏)) ≠ 0 ↔ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
11	10	biimpcd 252	. . . . . . . . 9 ⊢ ((𝑎 + (i · 𝑏)) ≠ 0 → (0 = (𝑐 + (i · 𝑑)) → (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
12	11	reximdv 3181	. . . . . . . 8 ⊢ ((𝑎 + (i · 𝑏)) ≠ 0 → (∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)) → ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
13	12	reximdv 3181	. . . . . . 7 ⊢ ((𝑎 + (i · 𝑏)) ≠ 0 → (∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)) → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
14	6, 9, 13	syl6mpi 68	. . . . . 6 ⊢ (1 ≠ 0 → (1 = (𝑎 + (i · 𝑏)) → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
15	14	reximdv 3181	. . . . 5 ⊢ (1 ≠ 0 → (∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)) → ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
16	15	reximdv 3181	. . . 4 ⊢ (1 ≠ 0 → (∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)) → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
17	4, 16	mpi 21	. . 3 ⊢ (1 ≠ 0 → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)))
18		id 23	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑐 → 𝑎 = 𝑐)
19		oveq2 7459	. . . . . . . . . . . 12 ⊢ (𝑏 = 𝑑 → (i · 𝑏) = (i · 𝑑))
20	18, 19	oveqan12d 7470	. . . . . . . . . . 11 ⊢ ((𝑎 = 𝑐 ∧ 𝑏 = 𝑑) → (𝑎 + (i · 𝑏)) = (𝑐 + (i · 𝑑)))
21	20	expcom 419	. . . . . . . . . 10 ⊢ (𝑏 = 𝑑 → (𝑎 = 𝑐 → (𝑎 + (i · 𝑏)) = (𝑐 + (i · 𝑑))))
22	21	necon3d 2980	. . . . . . . . 9 ⊢ (𝑏 = 𝑑 → ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → 𝑎 ≠ 𝑐))
23	22	com12 33	. . . . . . . 8 ⊢ ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → (𝑏 = 𝑑 → 𝑎 ≠ 𝑐))
24	23	necon3bd 2973	. . . . . . 7 ⊢ ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → (¬ 𝑎 ≠ 𝑐 → 𝑏 ≠ 𝑑))
25	24	orrd 877	. . . . . 6 ⊢ ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → (𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑))
26		neeq1 3021	. . . . . . . . . 10 ⊢ (𝑥 = 𝑎 → (𝑥 ≠ 𝑦 ↔ 𝑎 ≠ 𝑦))
27		neeq2 3022	. . . . . . . . . 10 ⊢ (𝑦 = 𝑐 → (𝑎 ≠ 𝑦 ↔ 𝑎 ≠ 𝑐))
28	26, 27	rspc2ev 3592	. . . . . . . . 9 ⊢ ((𝑎 ∈ ℝ ∧ 𝑐 ∈ ℝ ∧ 𝑎 ≠ 𝑐) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦)
29	28	3expia 1139	. . . . . . . 8 ⊢ ((𝑎 ∈ ℝ ∧ 𝑐 ∈ ℝ) → (𝑎 ≠ 𝑐 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
30	29	ad2ant2r 760	. . . . . . 7 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → (𝑎 ≠ 𝑐 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
31		neeq1 3021	. . . . . . . . . 10 ⊢ (𝑥 = 𝑏 → (𝑥 ≠ 𝑦 ↔ 𝑏 ≠ 𝑦))
32		neeq2 3022	. . . . . . . . . 10 ⊢ (𝑦 = 𝑑 → (𝑏 ≠ 𝑦 ↔ 𝑏 ≠ 𝑑))
33	31, 32	rspc2ev 3592	. . . . . . . . 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 3223	. . . 4 ⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
39	38	rexlimivv 3208	. . 3 ⊢ (∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦)
40	1, 17, 39	mp2b 10	. 2 ⊢ ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦
41		eqtr3 2785	. . . . . . . . 9 ⊢ ((𝑥 = 0 ∧ 𝑦 = 0) → 𝑥 = 𝑦)
42	41	ex 418	. . . . . . . 8 ⊢ (𝑥 = 0 → (𝑦 = 0 → 𝑥 = 𝑦))
43	42	necon3d 2980	. . . . . . 7 ⊢ (𝑥 = 0 → (𝑥 ≠ 𝑦 → 𝑦 ≠ 0))
44		neeq1 3021	. . . . . . . . 9 ⊢ (𝑧 = 𝑦 → (𝑧 ≠ 0 ↔ 𝑦 ≠ 0))
45	44	rspcev 3580	. . . . . . . 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 3021	. . . . . . . 8 ⊢ (𝑧 = 𝑥 → (𝑧 ≠ 0 ↔ 𝑥 ≠ 0))
51	50	rspcev 3580	. . . . . . 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 3042	. . 3 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
56	55	rexlimivv 3208	. 2 ⊢ (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)
57		ax-rrecex 11311	. . . 4 ⊢ ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → ∃𝑥 ∈ ℝ (𝑧 · 𝑥) = 1)
58		remulcl 11324	. . . . . . 7 ⊢ ((𝑧 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (𝑧 · 𝑥) ∈ ℝ)
59	58	adantlr 728	. . . . . 6 ⊢ (((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) ∧ 𝑥 ∈ ℝ) → (𝑧 · 𝑥) ∈ ℝ)
60		eleq1 2852	. . . . . 6 ⊢ ((𝑧 · 𝑥) = 1 → ((𝑧 · 𝑥) ∈ ℝ ↔ 1 ∈ ℝ))
61	59, 60	syl5ibcom 248	. . . . 5 ⊢ (((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) ∧ 𝑥 ∈ ℝ) → ((𝑧 · 𝑥) = 1 → 1 ∈ ℝ))
62	61	rexlimdva 3167	. . . 4 ⊢ ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → (∃𝑥 ∈ ℝ (𝑧 · 𝑥) = 1 → 1 ∈ ℝ))
63	57, 62	mpd 16	. . 3 ⊢ ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → 1 ∈ ℝ)
64	63	rexlimiva 3159	. 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 2147   ≠ wne 2959  ∃wrex 3090  (class class class)co 7451  ℂcc 11237  ℝcr 11238  0cc0 11239  1c1 11240  ici 11241   + caddc 11242   · cmul 11244

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-1cn 11297  ax-icn 11298  ax-addcl 11299  ax-mulcl 11301  ax-mulrcl 11302  ax-i2m1 11307  ax-1ne0 11308  ax-rrecex 11311  ax-cnre 11312

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-br 5109  df-iota 6520  df-fv 6574  df-ov 7454

This theorem is used by:  1red  11348  pr01ssre  11351  1xr  11407  dedekind  11512  peano2re  11522  mul02lem2  11526  addrid  11529  renegcl  11660  peano2rem  11664  0reALT  11694  0lt1  11878  0le1  11879  relin01  11880  1le1  11984  eqneg  12077  ltp1  12197  ltm1  12199  recgt0  12203  ltmulgt11  12216  lemulge11  12219  reclt1  12252  recgt1  12253  recgt1i  12254  recp1lt1  12255  recreclt  12256  recgt0ii  12263  ledivp1i  12282  ltdivp1i  12283  neg1rr  12346  neg1lt0  12348  cju  12356  indf  12366  indfval  12367  nnssre  12379  nnge1  12406  nngt1ne1  12407  nnle1eq1  12408  nngt0  12409  nnnlt1  12410  nnne0  12412  nnrecre  12420  nnrecgt0  12421  nnsub  12422  1t1e1ALT  12433  2re  12457  3re  12463  4re  12467  5re  12470  6re  12473  7re  12476  8re  12479  9re  12482  0le2OLD  12486  2posOLD  12488  1lt2  12555  1lt3  12558  1lt4  12561  1lt5  12565  1lt6  12570  1lt7  12576  1lt8  12583  1lt9  12591  1ne2  12593  1le2  12594  1le3  12597  halflt1  12603  addltmul  12622  nnunb  12642  elnnnn0c  12691  nn0ge2m1nn  12716  elnnz1  12762  znnnlt1  12763  zltp1le  12786  zleltp1  12787  nn0lt2  12802  recnz  12814  gtndiv  12816  3halfnz  12818  10re  12877  1lt10  12999  1lt10OLD  13000  eluzp1m1  13031  eluzp1p1  13033  eluz2b2  13088  zbtwnre  13113  rebtwnz  13114  1rp  13164  divlt1lt  13231  divle1le  13232  nnledivrp  13274  qbtwnxr  13370  xmulrid  13449  xmulm1  13451  x2times  13469  xrub  13482  elicc01  13637  1elunit  13641  divelunit  13665  lincmb01cmp  13666  unitssre  13670  0nelfz1  13716  fzpreddisj  13747  fznatpl1  13752  fztpval  13760  fraclt1  13982  fracle1  13983  flbi2  13997  fldiv4p1lem1div2  14015  fldiv4lem1div2  14017  fldiv  14040  modid  14076  1mod  14083  m1modnnsub1  14100  modm1p1mod0  14105  seqf1olem1  14224  reexpcl  14261  reexpclz  14265  expge0  14281  expge1  14282  expgt1  14283  bernneq  14414  bernneq2  14415  expnbnd  14417  expnlbnd  14418  expnlbnd2  14419  expmulnbnd  14420  discr1  14424  facwordi  14474  faclbnd3  14477  faclbnd4lem1  14478  faclbnd4lem4  14481  faclbnd6  14484  facavg  14486  hashv01gt1  14530  hashnn0n0nn  14576  hashunsnggt  14579  hash1snb  14605  hashgt12el  14608  hashgt12el2  14609  hashfun  14623  hashge2el2dif  14666  tpf1ofv2  14684  lsw0  14751  f1oun2prg  15111  sgnclre  15298  sgnnbi  15300  sgnpbi  15301  cjexp  15360  re1  15364  im1  15365  rei  15366  imi  15367  01sqrexlem1  15452  01sqrexlem2  15453  01sqrexlem3  15454  01sqrexlem4  15455  01sqrexlem7  15458  resqrex  15460  sqrt1  15481  sqrt2gt1lt2  15484  sqrtm1  15485  abs1  15507  absrdbnd  15553  caubnd2  15569  mulcn2  15807  reccn2  15808  rlimno1  15865  o1fsum  16024  expcnv  16077  geolim  16083  geolim2  16084  georeclim  16085  geomulcvg  16089  geoisumr  16091  geoisum1c  16093  fprodge0  16204  fprodge1  16206  rerisefaccl  16228  refallfaccl  16229  ere  16299  ege2le3  16300  efgt1  16328  resin4p  16350  recos4p  16351  tanhbnd  16373  sinbnd  16392  cosbnd  16393  sinbnd2  16394  cosbnd2  16395  ef01bndlem  16396  sin01bnd  16397  cos01bnd  16398  cos1bnd  16399  cos2bnd  16400  sinltx  16401  sin01gt0  16402  cos01gt0  16403  sin02gt0  16404  sincos1sgn  16405  ene1  16422  rpnnen2lem2  16427  rpnnen2lem3  16428  rpnnen2lem4  16429  rpnnen2lem9  16434  rpnnen2lem12  16437  ruclem6  16447  ruclem11  16452  ruclem12  16453  3dvds  16545  flodddiv4  16629  sadcadd  16672  isprm3  16902  sqnprm  16922  coprm  16931  phibndlem  16991  pythagtriplem3  17040  pcmpt  17114  fldivp1  17119  pockthi  17129  infpn2  17135  basendxnmulrndx  17513  starvndxnbasendx  17521  scandxnbasendx  17533  vscandxnbasendx  17538  ipndxnbasendx  17549  basendxnocndx  17600  slotsbhcdif  17636  lt6abl  20160  srgbinomlem4  20506  0ringnnzr  20827  abvneg  21134  abvtrivd  21140  prmidl0  21685  xrsmcmn  21753  xrsnsgrp  21766  gzrngunitlem  21792  gzrngunit  21793  rge0srg  21798  psgnodpmr  21951  remulg  21968  resubdrg  21969  psdmvr  22545  dscmet  24946  dscopn  24947  nrginvrcnlem  25065  idnghm  25117  tgioo  25170  blcvx  25172  iicmp  25262  iiconn  25263  iirev  25305  iihalf1  25307  iihalf2  25309  elii1  25311  elii2  25312  iimulcl  25313  icopnfcnv  25318  icopnfhmeo  25319  iccpnfhmeo  25321  xrhmeo  25322  xrhmph  25323  evth  25335  xlebnum  25341  htpycc  25356  reparphti  25373  pcoval1  25389  pco1  25391  pcoval2  25392  pcocn  25393  pcohtpylem  25395  pcopt  25398  pcopt2  25399  pcoass  25400  pcorevlem  25402  nmhmcn  25496  ncvs1  25533  ovolunlem1a  25872  vitalilem2  25985  vitalilem4  25987  vitalilem5  25988  vitali  25989  i1f1  26066  itg11  26067  itg2const  26116  dveflem  26354  dvlipcn  26369  dvcvx  26395  ply1remlem  26538  fta1blem  26544  plyn0mulidp  26657  plymulidp  26658  vieta1lem2  26689  aalioulem3  26718  aalioulem5  26720  aaliou3lem2  26727  ulmbdd  26782  iblulm  26791  radcnvlem1  26797  dvradcnv  26805  abelthlem2  26816  abelthlem3  26817  abelthlem5  26819  abelthlem7  26822  abelth  26825  abelth2  26826  reeff1olem  26830  reeff1o  26831  sinhalfpilem  26849  tangtx  26891  sincos4thpi  26899  pige3ALT  26905  coskpi  26908  recosf1o  26920  tanregt0  26924  efif1olem3  26929  efif1olem4  26930  loge  26971  logdivlti  27005  logcnlem4  27030  logf1o2  27035  logtayl  27045  logccv  27048  recxpcl  27060  cxplea  27081  cxpcn3lem  27132  cxpaddlelem  27136  loglesqrt  27146  ang180lem2  27195  angpined  27215  acosrecl  27288  atancj  27295  atanlogaddlem  27298  atantan  27308  atans2  27316  ressatans  27319  leibpi  27327  log2le1  27335  birthdaylem3  27338  cxp2lim  27361  cxploglim  27362  cxploglim2  27363  divsqrtsumlem  27364  cvxcl  27369  scvxcvx  27370  jensenlem2  27372  amgmlem  27374  emcllem2  27381  emcllem4  27383  emcllem6  27385  emcllem7  27386  emre  27390  emgt0  27391  harmonicbnd3  27392  harmonicubnd  27394  harmonicbnd4  27395  zetacvg  27399  ftalem1  27457  ftalem2  27458  ftalem5  27461  issqf  27520  cht1  27549  chp1  27551  ppiltx  27561  mumullem2  27564  ppiublem1  27586  ppiub  27588  chtublem  27595  chtub  27596  logfacbnd3  27607  logexprlim  27609  perfectlem2  27614  dchrinv  27645  dchr1re  27647  efexple  27665  bposlem1  27668  bposlem2  27669  bposlem5  27672  bposlem8  27675  lgsdir2lem1  27709  lgsdir2lem5  27713  lgsdir  27716  lgsne0  27719  lgsabs1  27720  lgsdinn0  27729  gausslemma2dlem0i  27748  lgseisen  27763  m1lgs  27772  2lgslem3  27788  addsq2nreurex  27828  2sqreultblem  27832  2sqreunnltblem  27835  chebbnd1lem3  27855  chebbnd1  27856  chtppilimlem1  27857  chtppilimlem2  27858  chtppilim  27859  chpchtlim  27863  vmadivsumb  27867  rplogsumlem2  27869  rpvmasumlem  27871  dchrmusumlema  27877  dchrmusum2  27878  dchrvmasumlem2  27882  dchrvmasumiflem1  27885  dchrisum0flblem1  27892  dchrisum0flblem2  27893  dchrisum0fno1  27895  rpvmasum2  27896  dchrisum0re  27897  dchrisum0lema  27898  dchrisum0lem1b  27899  dchrisum0lem1  27900  dchrisum0lem2a  27901  dchrisum0lem2  27902  logdivsum  27917  mulog2sumlem2  27919  2vmadivsumlem  27924  log2sumbnd  27928  selbergb  27933  selberg2b  27936  chpdifbndlem1  27937  selberg3lem1  27941  selberg3lem2  27942  selberg4lem1  27944  pntrmax  27948  pntrsumo1  27949  selbergsb  27959  pntrlog2bndlem3  27963  pntrlog2bndlem5  27965  pntpbnd1a  27969  pntpbnd2  27971  pntibndlem1  27973  pntibndlem3  27976  pntlemd  27978  pntlemc  27979  pntlemb  27981  pntlemr  27986  pntlemf  27989  pntlemk  27990  pntlemo  27991  pntlem3  27993  pntleml  27995  abvcxp  27999  ostth2lem1  28002  ostth1  28017  ostth2lem2  28018  ostth2lem3  28019  ostth2lem4  28020  ostth2  28021  ostth3  28022  ostth  28023  slotsinbpsd  28960  slotslnbpsd  28961  trgcgrg  29035  brbtwn2  29540  colinearalglem4  29544  ax5seglem2  29564  ax5seglem3  29566  axpaschlem  29575  axpasch  29576  axlowdimlem6  29582  axlowdimlem10  29586  axlowdimlem16  29592  axlowdim1  29594  axlowdim2  29595  axlowdim  29596  axcontlem2  29600  elntg2  29620  lfgrnloop  29760  lfuhgr1v0e  29892  usgrexmpldifpr  29896  usgrexmplef  29897  1loopgrvd2  30141  vdegp1bi  30175  lfgrwlkprop  30327  pthdlem1  30409  pthdlem2  30411  clwlkclwwlkf  30656  upgr4cycl4dv4e  30843  konigsberglem2  30911  konigsberglem3  30912  konigsberglem5  30914  frgrreg  31052  ex-dif  31081  ex-in  31083  ex-pss  31086  ex-res  31099  ex-fl  31105  nv1  31334  smcnlem  31356  ipidsq  31369  nmlno0lem  31452  norm-ii-i  31796  bcs2  31841  norm1  31908  nmopub2tALT  32568  nmfnleub2  32585  nmlnop0iALT  32654  unopbd  32674  nmopadjlem  32748  nmopcoadji  32760  pjnmopi  32807  pjbdlni  32808  hstle1  32885  hstle  32889  hstles  32890  stge1i  32897  stlesi  32900  staddi  32905  stadd3i  32907  strlem1  32909  strlem5  32914  jplem1  32927  cdj1i  33092  addltmulALT  33147  xlt2addrd  33447  sgnmulsgp  33519  dp2lt10  33546  dp2ltsuc  33548  dp2ltc  33549  dplti  33567  dpmul4  33576  cshw1s2  33617  xrsmulgzz  33669  rearchi  34011  xrge0slmod  34013  evl1deg3  34213  constrconj  34488  2sqr3minply  34523  submateqlem1  34550  xrge0iifcnv  34676  xrge0iifcv  34677  xrge0iifiso  34678  xrge0iifhom  34680  zrhre  34762  esumcst  34806  cntnevol  34972  iwrdsplit  35130  dstfrvclim1  35221  coinfliprv  35226  ballotlem2  35232  ballotlem4  35242  ballotlemi1  35246  ballotlemic  35250  signswch  35301  signstf  35306  signsvfn  35322  itgexpif  35346  hgt750lemd  35388  logdivsqrle  35390  hgt750lem  35391  hgt750lem2  35392  hgt750leme  35398  tgoldbachgnn  35399  subfacp1lem1  36152  subfacp1lem5  36157  resconn  36219  iisconn  36225  iillysconn  36226  problem2  36639  problem3  36640  sinccvglem  36645  fz0n  36711  dnibndlem12  37570  knoppcnlem4  37577  knoppndvlem13  37605  cnndvlem1  37618  irrdiff  38515  relowlpssretop  38555  sin2h  38801  cos2h  38802  tan2h  38803  poimirlem7  38813  poimirlem16  38822  poimirlem17  38823  poimirlem19  38825  poimirlem20  38826  poimirlem22  38828  poimirlem23  38829  poimirlem29  38835  poimirlem31  38837  itg2addnclem3  38859  asindmre  38889  dvasin  38890  dvacos  38891  dvreasin  38892  dvreacos  38893  fdc  38945  geomcau  38959  cntotbnd  38996  heiborlem8  39018  bfplem2  39023  bfp  39024  aks4d1p1p7  43390  ine1  43637  re1m1e0m0  43714  sn-00idlem1  43715  sn-00idlem2  43716  remul02  43722  sn-0ne2  43723  reixi  43740  rei4  43741  remullid  43751  ipiiie0  43755  sn-0tie0  43781  sn-nnne0  43790  mulgt0b1d  43802  sn-0lt1  43805  sn-ltp1  43806  reneg1lt0  43810  sn-inelr  43817  rabren3dioph  44088  pellexlem5  44106  pellexlem6  44107  pell1qrgaplem  44146  pell14qrgap  44148  pellqrex  44152  pellfundre  44154  pellfundlb  44157  pellfund14gap  44160  jm2.17a  44233  acongeq  44256  jm2.23  44269  jm3.1lem2  44291  sqrtcval  44902  sqrtcval2  44903  resqrtval  44904  imsqrtval  44905  relexp01min  44974  cvgdvgrat  45558  lhe4.4ex1a  45574  binomcxplemnotnn0  45601  isosctrlem1ALT  46176  supxrgelem  46622  xrlexaddrp  46637  infxr  46651  infleinflem2  46655  sumnnodd  46915  limsup10exlem  47055  limsup10ex  47056  dvnprodlem3  47231  stoweidlem1  47284  stoweidlem18  47301  stoweidlem19  47302  stoweidlem26  47309  stoweidlem34  47317  stoweidlem40  47323  stoweidlem41  47324  stoweidlem59  47342  stoweid  47346  stirlinglem10  47366  stirlinglem11  47367  dirkercncflem1  47386  fourierdlem16  47406  fourierdlem21  47411  fourierdlem22  47412  fourierdlem42  47432  fourierdlem68  47457  fourierdlem83  47472  fourierdlem103  47492  sqwvfourb  47512  fouriersw  47514  etransclem23  47540  salgencntex  47626  ovn0lem  47848  smfmullem3  48076  smfmullem4  48077  numtowerdt  48189  goldratval  48209  cjnpoly  48212  zm1nn  48645  ceilhalf1  48681  m1mod0mod1  48703  muldvdsfacgt  48729  fmtnosqrt  48897  nprmdvdsfacm1lem4  48981  perfectALTVlem2  49093  2exp340mod341  49104  8exp8mod9  49107  nfermltl8rev  49113  nnsum3primesprm  49161  nnsum4primesodd  49167  nnsum4primesoddALTV  49168  nnsum4primeseven  49171  nnsum4primesevenALTV  49172  tgblthelfgott  49186  tgoldbach  49188  usgrexmpl1lem  49392  usgrexmpl2lem  49397  usgrexmpl2nb1  49403  usgrexmpl2nb3  49405  usgrexmpl2nb4  49406  usgrexmpl2nb5  49407  usgrexmpl2trifr  49408  gpg3kgrtriexlem3  49456  pgnbgreunbgrlem2lem1  49485  pgnbgreunbgrlem2lem2  49486  rege1logbrege0  50001  rege1logbzge0  50002  blennnelnn  50019  dignnld  50046  nn0sumshdiglemA  50062  nn0sumshdiglem1  50064  rrxlines  50177  eenglngeehlnmlem1  50181  eenglngeehlnmlem2  50182  line2ylem  50194  line2  50195  line2xlem  50196  line2x  50197  icccldii  50364  io1ii  50366  sepfsepc  50373  1ne3  51369  veronesev1lem  51401  veronesev4lem  51404  veronesev5lem  51405  veronesev6lem  51406  veronesevrowd  51407  veronesematrowd  51409  veroquadgsumlem  51411  veroquadmodzerod  51412  veroquadnolindfd  51413