Theorem 1re 11115

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 11067, 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 11078	. . 3 ⊢ 1 ≠ 0
2		ax-1cn 11067	. . . . 5 ⊢ 1 ∈ ℂ
3		cnre 11112	. . . . 5 ⊢ (1 ∈ ℂ → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)))
4	2, 3	ax-mp 5	. . . 4 ⊢ ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏))
5		neeq1 2987	. . . . . . . 8 ⊢ (1 = (𝑎 + (i · 𝑏)) → (1 ≠ 0 ↔ (𝑎 + (i · 𝑏)) ≠ 0))
6	5	biimpcd 249	. . . . . . 7 ⊢ (1 ≠ 0 → (1 = (𝑎 + (i · 𝑏)) → (𝑎 + (i · 𝑏)) ≠ 0))
7		0cn 11107	. . . . . . . 8 ⊢ 0 ∈ ℂ
8		cnre 11112	. . . . . . . 8 ⊢ (0 ∈ ℂ → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)))
9	7, 8	ax-mp 5	. . . . . . 7 ⊢ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑))
10		neeq2 2988	. . . . . . . . . 10 ⊢ (0 = (𝑐 + (i · 𝑑)) → ((𝑎 + (i · 𝑏)) ≠ 0 ↔ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
11	10	biimpcd 249	. . . . . . . . 9 ⊢ ((𝑎 + (i · 𝑏)) ≠ 0 → (0 = (𝑐 + (i · 𝑑)) → (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
12	11	reximdv 3144	. . . . . . . 8 ⊢ ((𝑎 + (i · 𝑏)) ≠ 0 → (∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)) → ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
13	12	reximdv 3144	. . . . . . 7 ⊢ ((𝑎 + (i · 𝑏)) ≠ 0 → (∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)) → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
14	6, 9, 13	syl6mpi 67	. . . . . 6 ⊢ (1 ≠ 0 → (1 = (𝑎 + (i · 𝑏)) → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
15	14	reximdv 3144	. . . . 5 ⊢ (1 ≠ 0 → (∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)) → ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
16	15	reximdv 3144	. . . 4 ⊢ (1 ≠ 0 → (∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)) → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
17	4, 16	mpi 20	. . 3 ⊢ (1 ≠ 0 → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)))
18		id 22	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑐 → 𝑎 = 𝑐)
19		oveq2 7357	. . . . . . . . . . . 12 ⊢ (𝑏 = 𝑑 → (i · 𝑏) = (i · 𝑑))
20	18, 19	oveqan12d 7368	. . . . . . . . . . 11 ⊢ ((𝑎 = 𝑐 ∧ 𝑏 = 𝑑) → (𝑎 + (i · 𝑏)) = (𝑐 + (i · 𝑑)))
21	20	expcom 413	. . . . . . . . . 10 ⊢ (𝑏 = 𝑑 → (𝑎 = 𝑐 → (𝑎 + (i · 𝑏)) = (𝑐 + (i · 𝑑))))
22	21	necon3d 2946	. . . . . . . . 9 ⊢ (𝑏 = 𝑑 → ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → 𝑎 ≠ 𝑐))
23	22	com12 32	. . . . . . . 8 ⊢ ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → (𝑏 = 𝑑 → 𝑎 ≠ 𝑐))
24	23	necon3bd 2939	. . . . . . 7 ⊢ ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → (¬ 𝑎 ≠ 𝑐 → 𝑏 ≠ 𝑑))
25	24	orrd 863	. . . . . 6 ⊢ ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → (𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑))
26		neeq1 2987	. . . . . . . . . 10 ⊢ (𝑥 = 𝑎 → (𝑥 ≠ 𝑦 ↔ 𝑎 ≠ 𝑦))
27		neeq2 2988	. . . . . . . . . 10 ⊢ (𝑦 = 𝑐 → (𝑎 ≠ 𝑦 ↔ 𝑎 ≠ 𝑐))
28	26, 27	rspc2ev 3590	. . . . . . . . 9 ⊢ ((𝑎 ∈ ℝ ∧ 𝑐 ∈ ℝ ∧ 𝑎 ≠ 𝑐) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦)
29	28	3expia 1121	. . . . . . . 8 ⊢ ((𝑎 ∈ ℝ ∧ 𝑐 ∈ ℝ) → (𝑎 ≠ 𝑐 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
30	29	ad2ant2r 747	. . . . . . 7 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → (𝑎 ≠ 𝑐 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
31		neeq1 2987	. . . . . . . . . 10 ⊢ (𝑥 = 𝑏 → (𝑥 ≠ 𝑦 ↔ 𝑏 ≠ 𝑦))
32		neeq2 2988	. . . . . . . . . 10 ⊢ (𝑦 = 𝑑 → (𝑏 ≠ 𝑦 ↔ 𝑏 ≠ 𝑑))
33	31, 32	rspc2ev 3590	. . . . . . . . 9 ⊢ ((𝑏 ∈ ℝ ∧ 𝑑 ∈ ℝ ∧ 𝑏 ≠ 𝑑) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦)
34	33	3expia 1121	. . . . . . . 8 ⊢ ((𝑏 ∈ ℝ ∧ 𝑑 ∈ ℝ) → (𝑏 ≠ 𝑑 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
35	34	ad2ant2l 746	. . . . . . 7 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → (𝑏 ≠ 𝑑 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
36	30, 35	jaod 859	. . . . . 6 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → ((𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
37	25, 36	syl5 34	. . . . 5 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
38	37	rexlimdvva 3186	. . . 4 ⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
39	38	rexlimivv 3171	. . 3 ⊢ (∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦)
40	1, 17, 39	mp2b 10	. 2 ⊢ ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦
41		eqtr3 2751	. . . . . . . . 9 ⊢ ((𝑥 = 0 ∧ 𝑦 = 0) → 𝑥 = 𝑦)
42	41	ex 412	. . . . . . . 8 ⊢ (𝑥 = 0 → (𝑦 = 0 → 𝑥 = 𝑦))
43	42	necon3d 2946	. . . . . . 7 ⊢ (𝑥 = 0 → (𝑥 ≠ 𝑦 → 𝑦 ≠ 0))
44		neeq1 2987	. . . . . . . . 9 ⊢ (𝑧 = 𝑦 → (𝑧 ≠ 0 ↔ 𝑦 ≠ 0))
45	44	rspcev 3577	. . . . . . . 8 ⊢ ((𝑦 ∈ ℝ ∧ 𝑦 ≠ 0) → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)
46	45	expcom 413	. . . . . . 7 ⊢ (𝑦 ≠ 0 → (𝑦 ∈ ℝ → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
47	43, 46	syl6 35	. . . . . 6 ⊢ (𝑥 = 0 → (𝑥 ≠ 𝑦 → (𝑦 ∈ ℝ → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
48	47	com23 86	. . . . 5 ⊢ (𝑥 = 0 → (𝑦 ∈ ℝ → (𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
49	48	adantld 490	. . . 4 ⊢ (𝑥 = 0 → ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
50		neeq1 2987	. . . . . . . 8 ⊢ (𝑧 = 𝑥 → (𝑧 ≠ 0 ↔ 𝑥 ≠ 0))
51	50	rspcev 3577	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)
52	51	expcom 413	. . . . . 6 ⊢ (𝑥 ≠ 0 → (𝑥 ∈ ℝ → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
53	52	adantrd 491	. . . . 5 ⊢ (𝑥 ≠ 0 → ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
54	53	a1dd 50	. . . 4 ⊢ (𝑥 ≠ 0 → ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
55	49, 54	pm2.61ine 3008	. . 3 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
56	55	rexlimivv 3171	. 2 ⊢ (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)
57		ax-rrecex 11081	. . . 4 ⊢ ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → ∃𝑥 ∈ ℝ (𝑧 · 𝑥) = 1)
58		remulcl 11094	. . . . . . 7 ⊢ ((𝑧 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (𝑧 · 𝑥) ∈ ℝ)
59	58	adantlr 715	. . . . . 6 ⊢ (((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) ∧ 𝑥 ∈ ℝ) → (𝑧 · 𝑥) ∈ ℝ)
60		eleq1 2816	. . . . . 6 ⊢ ((𝑧 · 𝑥) = 1 → ((𝑧 · 𝑥) ∈ ℝ ↔ 1 ∈ ℝ))
61	59, 60	syl5ibcom 245	. . . . 5 ⊢ (((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) ∧ 𝑥 ∈ ℝ) → ((𝑧 · 𝑥) = 1 → 1 ∈ ℝ))
62	61	rexlimdva 3130	. . . 4 ⊢ ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → (∃𝑥 ∈ ℝ (𝑧 · 𝑥) = 1 → 1 ∈ ℝ))
63	57, 62	mpd 15	. . 3 ⊢ ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → 1 ∈ ℝ)
64	63	rexlimiva 3122	. 2 ⊢ (∃𝑧 ∈ ℝ 𝑧 ≠ 0 → 1 ∈ ℝ)
65	40, 56, 64	mp2b 10	1 ⊢ 1 ∈ ℝ

Syntax hints:   → wi 4   ∧ wa 395   ∨ wo 847   = wceq 1540   ∈ wcel 2109   ≠ wne 2925  ∃wrex 3053  (class class class)co 7349  ℂcc 11007  ℝcr 11008  0cc0 11009  1c1 11010  ici 11011   + caddc 11012   · cmul 11014

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-1cn 11067  ax-icn 11068  ax-addcl 11069  ax-mulcl 11071  ax-mulrcl 11072  ax-i2m1 11077  ax-1ne0 11078  ax-rrecex 11081  ax-cnre 11082

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-iota 6438  df-fv 6490  df-ov 7352

This theorem is referenced by:  1red  11116  1xr  11174  dedekind  11279  peano2re  11289  mul02lem2  11293  addrid  11296  renegcl  11427  peano2rem  11431  0reALT  11461  0lt1  11642  0le1  11643  relin01  11644  1le1  11748  eqneg  11844  ltp1  11964  ltm1  11966  recgt0  11970  mulgt1OLD  11983  ltmulgt11  11984  lemulge11  11987  reclt1  12020  recgt1  12021  recgt1i  12022  recp1lt1  12023  recreclt  12024  recgt0ii  12031  ledivp1i  12050  ltdivp1i  12051  neg1rr  12114  neg1lt0  12116  cju  12124  nnssre  12132  nnge1  12156  nngt1ne1  12157  nnle1eq1  12158  nngt0  12159  nnnlt1  12160  nnne0  12162  nnrecre  12170  nnrecgt0  12171  nnsub  12172  2re  12202  3re  12208  4re  12212  5re  12215  6re  12218  7re  12221  8re  12224  9re  12227  0le2  12230  2pos  12231  3pos  12233  4pos  12235  5pos  12237  6pos  12238  7pos  12239  8pos  12240  9pos  12241  1lt2  12294  1lt3  12296  1lt4  12299  1lt5  12303  1lt6  12308  1lt7  12314  1lt8  12321  1lt9  12329  1ne2  12331  1le2  12332  1le3  12335  halflt1  12341  addltmul  12360  nnunb  12380  elnnnn0c  12429  nn0ge2m1nn  12454  elnnz1  12501  znnnlt1  12502  zltp1le  12525  zleltp1  12526  nn0lt2  12539  recnz  12551  gtndiv  12553  3halfnz  12555  10re  12610  1lt10  12730  eluzp1m1  12761  eluzp1p1  12763  eluz2b2  12822  zbtwnre  12847  rebtwnz  12848  1rp  12897  divlt1lt  12964  divle1le  12965  nnledivrp  13007  qbtwnxr  13102  xmulrid  13181  xmulm1  13183  x2times  13201  xrub  13214  elicc01  13369  1elunit  13373  divelunit  13397  lincmb01cmp  13398  unitssre  13402  0nelfz1  13446  fzpreddisj  13476  fznatpl1  13481  fztpval  13489  fraclt1  13706  fracle1  13707  flbi2  13721  fldiv4p1lem1div2  13739  fldiv4lem1div2  13741  fldiv  13764  modid  13800  1mod  13807  m1modnnsub1  13824  modm1p1mod0  13829  seqf1olem1  13948  reexpcl  13985  reexpclz  13989  expge0  14005  expge1  14006  expgt1  14007  bernneq  14136  bernneq2  14137  expnbnd  14139  expnlbnd  14140  expnlbnd2  14141  expmulnbnd  14142  discr1  14146  facwordi  14196  faclbnd3  14199  faclbnd4lem1  14200  faclbnd4lem4  14203  faclbnd6  14206  facavg  14208  hashv01gt1  14252  hashnn0n0nn  14298  hashunsnggt  14301  hash1snb  14326  hashgt12el  14329  hashgt12el2  14330  hashfun  14344  hashge2el2dif  14387  tpf1ofv2  14405  lsw0  14472  f1oun2prg  14824  cjexp  15057  re1  15061  im1  15062  rei  15063  imi  15064  01sqrexlem1  15149  01sqrexlem2  15150  01sqrexlem3  15151  01sqrexlem4  15152  01sqrexlem7  15155  resqrex  15157  sqrt1  15178  sqrt2gt1lt2  15181  sqrtm1  15182  abs1  15204  absrdbnd  15249  caubnd2  15265  mulcn2  15503  reccn2  15504  rlimno1  15561  o1fsum  15720  expcnv  15771  geolim  15777  geolim2  15778  georeclim  15779  geomulcvg  15783  geoisumr  15785  geoisum1c  15787  fprodge0  15900  fprodge1  15902  rerisefaccl  15924  refallfaccl  15925  ere  15996  ege2le3  15997  efgt1  16025  resin4p  16047  recos4p  16048  tanhbnd  16070  sinbnd  16089  cosbnd  16090  sinbnd2  16091  cosbnd2  16092  ef01bndlem  16093  sin01bnd  16094  cos01bnd  16095  cos1bnd  16096  cos2bnd  16097  sinltx  16098  sin01gt0  16099  cos01gt0  16100  sin02gt0  16101  sincos1sgn  16102  ene1  16119  rpnnen2lem2  16124  rpnnen2lem3  16125  rpnnen2lem4  16126  rpnnen2lem9  16131  rpnnen2lem12  16134  ruclem6  16144  ruclem11  16149  ruclem12  16150  3dvds  16242  flodddiv4  16326  sadcadd  16369  isprm3  16594  sqnprm  16613  coprm  16622  phibndlem  16681  pythagtriplem3  16730  pcmpt  16804  fldivp1  16809  pockthi  16819  infpn2  16825  basendxnmulrndx  17200  starvndxnbasendx  17208  scandxnbasendx  17220  vscandxnbasendx  17225  ipndxnbasendx  17236  basendxnocndx  17287  slotsbhcdif  17319  lt6abl  19774  srgbinomlem4  20114  0ringnnzr  20410  abvneg  20711  abvtrivd  20717  xrsmcmn  21298  xrsnsgrp  21314  gzrngunitlem  21339  gzrngunit  21340  rge0srg  21345  psgnodpmr  21497  remulg  21514  resubdrg  21515  psdmvr  22054  dscmet  24458  dscopn  24459  nrginvrcnlem  24577  idnghm  24629  tgioo  24682  blcvx  24684  iicmp  24777  iiconn  24778  iirev  24821  iihalf1  24823  iihalf2  24826  iihalf2cnOLD  24828  elii1  24829  elii2  24830  iimulcl  24831  icopnfcnv  24838  icopnfhmeo  24839  iccpnfhmeo  24841  xrhmeo  24842  xrhmph  24843  evth  24856  xlebnum  24862  htpycc  24877  reparphti  24894  reparphtiOLD  24895  pcoval1  24911  pco1  24913  pcoval2  24914  pcocn  24915  pcohtpylem  24917  pcopt  24920  pcopt2  24921  pcoass  24922  pcorevlem  24924  nmhmcn  25018  ncvs1  25055  ovolunlem1a  25395  vitalilem2  25508  vitalilem4  25510  vitalilem5  25511  vitali  25512  i1f1  25589  itg11  25590  itg2const  25639  dveflem  25881  dvlipcn  25897  dvcvx  25923  ply1remlem  26068  fta1blem  26074  vieta1lem2  26217  aalioulem3  26240  aalioulem5  26242  aaliou3lem2  26249  ulmbdd  26305  iblulm  26314  radcnvlem1  26320  dvradcnv  26328  abelthlem2  26340  abelthlem3  26341  abelthlem5  26343  abelthlem7  26346  abelth  26349  abelth2  26350  reeff1olem  26354  reeff1o  26355  sinhalfpilem  26370  tangtx  26412  sincos4thpi  26420  pige3ALT  26427  coskpi  26430  cos0pilt1  26439  recosf1o  26442  tanregt0  26446  efif1olem3  26451  efif1olem4  26452  loge  26493  logdivlti  26527  logcnlem4  26552  logf1o2  26557  logtayl  26567  logccv  26570  recxpcl  26582  cxplea  26603  cxpcn3lem  26655  cxpaddlelem  26659  loglesqrt  26669  ang180lem2  26718  angpined  26738  acosrecl  26811  atancj  26818  atanlogaddlem  26821  atantan  26831  atans2  26839  ressatans  26842  leibpi  26850  log2le1  26858  birthdaylem3  26861  cxp2lim  26885  cxploglim  26886  cxploglim2  26887  divsqrtsumlem  26888  cvxcl  26893  scvxcvx  26894  jensenlem2  26896  amgmlem  26898  emcllem2  26905  emcllem4  26907  emcllem6  26909  emcllem7  26910  emre  26914  emgt0  26915  harmonicbnd3  26916  harmonicubnd  26918  harmonicbnd4  26919  zetacvg  26923  ftalem1  26981  ftalem2  26982  ftalem5  26985  issqf  27044  cht1  27073  chp1  27075  ppiltx  27085  mumullem2  27088  ppiublem1  27111  ppiub  27113  chtublem  27120  chtub  27121  logfacbnd3  27132  logexprlim  27134  perfectlem2  27139  dchrinv  27170  dchr1re  27172  efexple  27190  bposlem1  27193  bposlem2  27194  bposlem5  27197  bposlem8  27200  lgsdir2lem1  27234  lgsdir2lem5  27238  lgsdir  27241  lgsne0  27244  lgsabs1  27245  lgsdinn0  27254  gausslemma2dlem0i  27273  lgseisen  27288  m1lgs  27297  2lgslem3  27313  addsq2nreurex  27353  2sqreultblem  27357  2sqreunnltblem  27360  chebbnd1lem3  27380  chebbnd1  27381  chtppilimlem1  27382  chtppilimlem2  27383  chtppilim  27384  chpchtlim  27388  vmadivsumb  27392  rplogsumlem2  27394  rpvmasumlem  27396  dchrmusumlema  27402  dchrmusum2  27403  dchrvmasumlem2  27407  dchrvmasumiflem1  27410  dchrisum0flblem1  27417  dchrisum0flblem2  27418  dchrisum0fno1  27420  rpvmasum2  27421  dchrisum0re  27422  dchrisum0lema  27423  dchrisum0lem1b  27424  dchrisum0lem1  27425  dchrisum0lem2a  27426  dchrisum0lem2  27427  logdivsum  27442  mulog2sumlem2  27444  2vmadivsumlem  27449  log2sumbnd  27453  selbergb  27458  selberg2b  27461  chpdifbndlem1  27462  selberg3lem1  27466  selberg3lem2  27467  selberg4lem1  27469  pntrmax  27473  pntrsumo1  27474  selbergsb  27484  pntrlog2bndlem3  27488  pntrlog2bndlem5  27490  pntpbnd1a  27494  pntpbnd2  27496  pntibndlem1  27498  pntibndlem3  27501  pntlemd  27503  pntlemc  27504  pntlemb  27506  pntlemr  27511  pntlemf  27514  pntlemk  27515  pntlemo  27516  pntlem3  27518  pntleml  27520  abvcxp  27524  ostth2lem1  27527  ostth1  27542  ostth2lem2  27543  ostth2lem3  27544  ostth2lem4  27545  ostth2  27546  ostth3  27547  ostth  27548  slotsinbpsd  28386  slotslnbpsd  28387  trgcgrg  28460  brbtwn2  28850  colinearalglem4  28854  ax5seglem2  28874  ax5seglem3  28876  axpaschlem  28885  axpasch  28886  axlowdimlem6  28892  axlowdimlem10  28896  axlowdimlem16  28902  axlowdim1  28904  axlowdim2  28905  axlowdim  28906  axcontlem2  28910  elntg2  28930  lfgrnloop  29070  lfuhgr1v0e  29199  usgrexmpldifpr  29203  usgrexmplef  29204  1loopgrvd2  29449  vdegp1bi  29483  lfgrwlkprop  29631  pthdlem1  29711  pthdlem2  29713  clwlkclwwlkf  29952  upgr4cycl4dv4e  30129  konigsberglem2  30197  konigsberglem3  30198  konigsberglem5  30200  frgrreg  30338  ex-dif  30367  ex-in  30369  ex-pss  30372  ex-res  30385  ex-fl  30391  nv1  30619  smcnlem  30641  ipidsq  30654  nmlno0lem  30737  norm-ii-i  31081  bcs2  31126  norm1  31193  nmopub2tALT  31853  nmfnleub2  31870  nmlnop0iALT  31939  unopbd  31959  nmopadjlem  32033  nmopcoadji  32045  pjnmopi  32092  pjbdlni  32093  hstle1  32170  hstle  32174  hstles  32175  stge1i  32182  stlesi  32185  staddi  32190  stadd3i  32192  strlem1  32194  strlem5  32199  jplem1  32212  cdj1i  32377  addltmulALT  32390  xlt2addrd  32702  pr01ssre  32769  sgnclre  32777  sgnnbi  32783  sgnpbi  32784  sgnmulsgp  32788  indf  32798  indfval  32799  dp2lt10  32824  dp2ltsuc  32826  dp2ltc  32827  dplti  32845  dpmul4  32854  cshw1s2  32902  xrsmulgzz  32963  rearchi  33283  xrge0slmod  33285  prmidl0  33387  evl1deg3  33513  constrconj  33712  2sqr3minply  33747  submateqlem1  33774  xrge0iifcnv  33900  xrge0iifcv  33901  xrge0iifiso  33902  xrge0iifhom  33904  zrhre  33986  esumcst  34030  cntnevol  34195  omssubadd  34268  iwrdsplit  34355  dstfrvclim1  34446  coinfliprv  34451  ballotlem2  34457  ballotlem4  34467  ballotlemi1  34471  ballotlemic  34475  plymulx0  34515  plymulx  34516  signswch  34529  signstf  34534  signsvfn  34550  itgexpif  34574  hgt750lemd  34616  logdivsqrle  34618  hgt750lem  34619  hgt750lem2  34620  hgt750leme  34626  tgoldbachgnn  34627  subfacp1lem1  35152  subfacp1lem5  35157  resconn  35219  iisconn  35225  iillysconn  35226  problem2  35639  problem3  35640  sinccvglem  35645  fz0n  35704  dnibndlem12  36463  knoppcnlem4  36470  knoppndvlem13  36498  cnndvlem1  36511  irrdiff  37300  relowlpssretop  37338  sin2h  37590  cos2h  37591  tan2h  37592  poimirlem7  37607  poimirlem16  37616  poimirlem17  37617  poimirlem19  37619  poimirlem20  37620  poimirlem22  37622  poimirlem23  37623  poimirlem29  37629  poimirlem31  37631  itg2addnclem3  37653  asindmre  37683  dvasin  37684  dvacos  37685  dvreasin  37686  dvreacos  37687  fdc  37725  geomcau  37739  cntotbnd  37776  heiborlem8  37798  bfplem2  37803  bfp  37804  aks4d1p1p7  42047  1t1e1ALT  42228  ine1  42287  re1m1e0m0  42370  sn-00idlem1  42371  sn-00idlem2  42372  remul02  42378  sn-0ne2  42379  reixi  42396  rei4  42397  remullid  42407  ipiiie0  42411  sn-0tie0  42424  sn-nnne0  42433  mulgt0b1d  42445  sn-0lt1  42448  sn-ltp1  42449  reneg1lt0  42453  sn-inelr  42460  rabren3dioph  42788  pellexlem5  42806  pellexlem6  42807  pell1qrgaplem  42846  pell14qrgap  42848  pellqrex  42852  pellfundre  42854  pellfundlb  42857  pellfund14gap  42860  jm2.17a  42933  acongeq  42956  jm2.23  42969  jm3.1lem2  42991  sqrtcval  43614  sqrtcval2  43615  resqrtval  43616  imsqrtval  43617  relexp01min  43686  cvgdvgrat  44286  lhe4.4ex1a  44302  binomcxplemnotnn0  44329  isosctrlem1ALT  44907  supxrgelem  45317  xrlexaddrp  45332  infxr  45346  infleinflem2  45350  sumnnodd  45611  limsup10exlem  45753  limsup10ex  45754  dvnprodlem3  45929  stoweidlem1  45982  stoweidlem18  45999  stoweidlem19  46000  stoweidlem26  46007  stoweidlem34  46015  stoweidlem40  46021  stoweidlem41  46022  stoweidlem59  46040  stoweid  46044  stirlinglem10  46064  stirlinglem11  46065  dirkercncflem1  46084  fourierdlem16  46104  fourierdlem21  46109  fourierdlem22  46110  fourierdlem42  46130  fourierdlem68  46155  fourierdlem83  46170  fourierdlem103  46190  sqwvfourb  46210  fouriersw  46212  etransclem23  46238  salgencntex  46324  ovn0lem  46546  smfmullem3  46774  smfmullem4  46775  cjnpoly  46873  zm1nn  47286  ceilhalf1  47318  m1mod0mod1  47338  fmtnosqrt  47523  perfectALTVlem2  47706  2exp340mod341  47717  8exp8mod9  47720  nfermltl8rev  47726  nnsum3primesprm  47774  nnsum4primesodd  47780  nnsum4primesoddALTV  47781  nnsum4primeseven  47784  nnsum4primesevenALTV  47785  tgblthelfgott  47799  tgoldbach  47801  usgrexmpl1lem  48005  usgrexmpl2lem  48010  usgrexmpl2nb1  48016  usgrexmpl2nb3  48018  usgrexmpl2nb4  48019  usgrexmpl2nb5  48020  usgrexmpl2trifr  48021  gpg3kgrtriexlem3  48069  pgnbgreunbgrlem2lem1  48098  pgnbgreunbgrlem2lem2  48099  rege1logbrege0  48543  rege1logbzge0  48544  blennnelnn  48561  dignnld  48588  nn0sumshdiglemA  48604  nn0sumshdiglem1  48606  rrx2xpref1o  48703  rrxlines  48718  eenglngeehlnmlem1  48722  eenglngeehlnmlem2  48723  line2ylem  48736  line2x  48739  icccldii  48903  io1ii  48905  sepfsepc  48912