Theorem 1re 11132

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 11084, 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 11095	. . 3 ⊢ 1 ≠ 0
2		ax-1cn 11084	. . . . 5 ⊢ 1 ∈ ℂ
3		cnre 11129	. . . . 5 ⊢ (1 ∈ ℂ → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)))
4	2, 3	ax-mp 5	. . . 4 ⊢ ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏))
5		neeq1 2994	. . . . . . . 8 ⊢ (1 = (𝑎 + (i · 𝑏)) → (1 ≠ 0 ↔ (𝑎 + (i · 𝑏)) ≠ 0))
6	5	biimpcd 249	. . . . . . 7 ⊢ (1 ≠ 0 → (1 = (𝑎 + (i · 𝑏)) → (𝑎 + (i · 𝑏)) ≠ 0))
7		0cn 11124	. . . . . . . 8 ⊢ 0 ∈ ℂ
8		cnre 11129	. . . . . . . 8 ⊢ (0 ∈ ℂ → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)))
9	7, 8	ax-mp 5	. . . . . . 7 ⊢ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑))
10		neeq2 2995	. . . . . . . . . 10 ⊢ (0 = (𝑐 + (i · 𝑑)) → ((𝑎 + (i · 𝑏)) ≠ 0 ↔ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
11	10	biimpcd 249	. . . . . . . . 9 ⊢ ((𝑎 + (i · 𝑏)) ≠ 0 → (0 = (𝑐 + (i · 𝑑)) → (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
12	11	reximdv 3151	. . . . . . . 8 ⊢ ((𝑎 + (i · 𝑏)) ≠ 0 → (∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)) → ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
13	12	reximdv 3151	. . . . . . 7 ⊢ ((𝑎 + (i · 𝑏)) ≠ 0 → (∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)) → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
14	6, 9, 13	syl6mpi 67	. . . . . 6 ⊢ (1 ≠ 0 → (1 = (𝑎 + (i · 𝑏)) → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
15	14	reximdv 3151	. . . . 5 ⊢ (1 ≠ 0 → (∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)) → ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
16	15	reximdv 3151	. . . 4 ⊢ (1 ≠ 0 → (∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)) → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
17	4, 16	mpi 20	. . 3 ⊢ (1 ≠ 0 → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)))
18		id 22	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑐 → 𝑎 = 𝑐)
19		oveq2 7366	. . . . . . . . . . . 12 ⊢ (𝑏 = 𝑑 → (i · 𝑏) = (i · 𝑑))
20	18, 19	oveqan12d 7377	. . . . . . . . . . 11 ⊢ ((𝑎 = 𝑐 ∧ 𝑏 = 𝑑) → (𝑎 + (i · 𝑏)) = (𝑐 + (i · 𝑑)))
21	20	expcom 413	. . . . . . . . . 10 ⊢ (𝑏 = 𝑑 → (𝑎 = 𝑐 → (𝑎 + (i · 𝑏)) = (𝑐 + (i · 𝑑))))
22	21	necon3d 2953	. . . . . . . . 9 ⊢ (𝑏 = 𝑑 → ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → 𝑎 ≠ 𝑐))
23	22	com12 32	. . . . . . . 8 ⊢ ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → (𝑏 = 𝑑 → 𝑎 ≠ 𝑐))
24	23	necon3bd 2946	. . . . . . 7 ⊢ ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → (¬ 𝑎 ≠ 𝑐 → 𝑏 ≠ 𝑑))
25	24	orrd 863	. . . . . 6 ⊢ ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → (𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑))
26		neeq1 2994	. . . . . . . . . 10 ⊢ (𝑥 = 𝑎 → (𝑥 ≠ 𝑦 ↔ 𝑎 ≠ 𝑦))
27		neeq2 2995	. . . . . . . . . 10 ⊢ (𝑦 = 𝑐 → (𝑎 ≠ 𝑦 ↔ 𝑎 ≠ 𝑐))
28	26, 27	rspc2ev 3589	. . . . . . . . 9 ⊢ ((𝑎 ∈ ℝ ∧ 𝑐 ∈ ℝ ∧ 𝑎 ≠ 𝑐) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦)
29	28	3expia 1121	. . . . . . . 8 ⊢ ((𝑎 ∈ ℝ ∧ 𝑐 ∈ ℝ) → (𝑎 ≠ 𝑐 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
30	29	ad2ant2r 747	. . . . . . 7 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → (𝑎 ≠ 𝑐 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
31		neeq1 2994	. . . . . . . . . 10 ⊢ (𝑥 = 𝑏 → (𝑥 ≠ 𝑦 ↔ 𝑏 ≠ 𝑦))
32		neeq2 2995	. . . . . . . . . 10 ⊢ (𝑦 = 𝑑 → (𝑏 ≠ 𝑦 ↔ 𝑏 ≠ 𝑑))
33	31, 32	rspc2ev 3589	. . . . . . . . 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 3193	. . . 4 ⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
39	38	rexlimivv 3178	. . 3 ⊢ (∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦)
40	1, 17, 39	mp2b 10	. 2 ⊢ ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦
41		eqtr3 2758	. . . . . . . . 9 ⊢ ((𝑥 = 0 ∧ 𝑦 = 0) → 𝑥 = 𝑦)
42	41	ex 412	. . . . . . . 8 ⊢ (𝑥 = 0 → (𝑦 = 0 → 𝑥 = 𝑦))
43	42	necon3d 2953	. . . . . . 7 ⊢ (𝑥 = 0 → (𝑥 ≠ 𝑦 → 𝑦 ≠ 0))
44		neeq1 2994	. . . . . . . . 9 ⊢ (𝑧 = 𝑦 → (𝑧 ≠ 0 ↔ 𝑦 ≠ 0))
45	44	rspcev 3576	. . . . . . . 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 2994	. . . . . . . 8 ⊢ (𝑧 = 𝑥 → (𝑧 ≠ 0 ↔ 𝑥 ≠ 0))
51	50	rspcev 3576	. . . . . . 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 3015	. . 3 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
56	55	rexlimivv 3178	. 2 ⊢ (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)
57		ax-rrecex 11098	. . . 4 ⊢ ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → ∃𝑥 ∈ ℝ (𝑧 · 𝑥) = 1)
58		remulcl 11111	. . . . . . 7 ⊢ ((𝑧 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (𝑧 · 𝑥) ∈ ℝ)
59	58	adantlr 715	. . . . . 6 ⊢ (((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) ∧ 𝑥 ∈ ℝ) → (𝑧 · 𝑥) ∈ ℝ)
60		eleq1 2824	. . . . . 6 ⊢ ((𝑧 · 𝑥) = 1 → ((𝑧 · 𝑥) ∈ ℝ ↔ 1 ∈ ℝ))
61	59, 60	syl5ibcom 245	. . . . 5 ⊢ (((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) ∧ 𝑥 ∈ ℝ) → ((𝑧 · 𝑥) = 1 → 1 ∈ ℝ))
62	61	rexlimdva 3137	. . . 4 ⊢ ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → (∃𝑥 ∈ ℝ (𝑧 · 𝑥) = 1 → 1 ∈ ℝ))
63	57, 62	mpd 15	. . 3 ⊢ ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → 1 ∈ ℝ)
64	63	rexlimiva 3129	. 2 ⊢ (∃𝑧 ∈ ℝ 𝑧 ≠ 0 → 1 ∈ ℝ)
65	40, 56, 64	mp2b 10	1 ⊢ 1 ∈ ℝ

Syntax hints:   → wi 4   ∧ wa 395   ∨ wo 847   = wceq 1541   ∈ wcel 2113   ≠ wne 2932  ∃wrex 3060  (class class class)co 7358  ℂcc 11024  ℝcr 11025  0cc0 11026  1c1 11027  ici 11028   + caddc 11029   · cmul 11031

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-1cn 11084  ax-icn 11085  ax-addcl 11086  ax-mulcl 11088  ax-mulrcl 11089  ax-i2m1 11094  ax-1ne0 11095  ax-rrecex 11098  ax-cnre 11099

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-iota 6448  df-fv 6500  df-ov 7361

This theorem is referenced by:  1red  11133  1xr  11191  dedekind  11296  peano2re  11306  mul02lem2  11310  addrid  11313  renegcl  11444  peano2rem  11448  0reALT  11478  0lt1  11659  0le1  11660  relin01  11661  1le1  11765  eqneg  11861  ltp1  11981  ltm1  11983  recgt0  11987  mulgt1OLD  12000  ltmulgt11  12001  lemulge11  12004  reclt1  12037  recgt1  12038  recgt1i  12039  recp1lt1  12040  recreclt  12041  recgt0ii  12048  ledivp1i  12067  ltdivp1i  12068  neg1rr  12131  neg1lt0  12133  cju  12141  nnssre  12149  nnge1  12173  nngt1ne1  12174  nnle1eq1  12175  nngt0  12176  nnnlt1  12177  nnne0  12179  nnrecre  12187  nnrecgt0  12188  nnsub  12189  2re  12219  3re  12225  4re  12229  5re  12232  6re  12235  7re  12238  8re  12241  9re  12244  0le2  12247  2pos  12248  3pos  12250  4pos  12252  5pos  12254  6pos  12255  7pos  12256  8pos  12257  9pos  12258  1lt2  12311  1lt3  12313  1lt4  12316  1lt5  12320  1lt6  12325  1lt7  12331  1lt8  12338  1lt9  12346  1ne2  12348  1le2  12349  1le3  12352  halflt1  12358  addltmul  12377  nnunb  12397  elnnnn0c  12446  nn0ge2m1nn  12471  elnnz1  12517  znnnlt1  12518  zltp1le  12541  zleltp1  12542  nn0lt2  12555  recnz  12567  gtndiv  12569  3halfnz  12571  10re  12626  1lt10  12746  eluzp1m1  12777  eluzp1p1  12779  eluz2b2  12834  zbtwnre  12859  rebtwnz  12860  1rp  12909  divlt1lt  12976  divle1le  12977  nnledivrp  13019  qbtwnxr  13115  xmulrid  13194  xmulm1  13196  x2times  13214  xrub  13227  elicc01  13382  1elunit  13386  divelunit  13410  lincmb01cmp  13411  unitssre  13415  0nelfz1  13459  fzpreddisj  13489  fznatpl1  13494  fztpval  13502  fraclt1  13722  fracle1  13723  flbi2  13737  fldiv4p1lem1div2  13755  fldiv4lem1div2  13757  fldiv  13780  modid  13816  1mod  13823  m1modnnsub1  13840  modm1p1mod0  13845  seqf1olem1  13964  reexpcl  14001  reexpclz  14005  expge0  14021  expge1  14022  expgt1  14023  bernneq  14152  bernneq2  14153  expnbnd  14155  expnlbnd  14156  expnlbnd2  14157  expmulnbnd  14158  discr1  14162  facwordi  14212  faclbnd3  14215  faclbnd4lem1  14216  faclbnd4lem4  14219  faclbnd6  14222  facavg  14224  hashv01gt1  14268  hashnn0n0nn  14314  hashunsnggt  14317  hash1snb  14342  hashgt12el  14345  hashgt12el2  14346  hashfun  14360  hashge2el2dif  14403  tpf1ofv2  14421  lsw0  14488  f1oun2prg  14840  cjexp  15073  re1  15077  im1  15078  rei  15079  imi  15080  01sqrexlem1  15165  01sqrexlem2  15166  01sqrexlem3  15167  01sqrexlem4  15168  01sqrexlem7  15171  resqrex  15173  sqrt1  15194  sqrt2gt1lt2  15197  sqrtm1  15198  abs1  15220  absrdbnd  15265  caubnd2  15281  mulcn2  15519  reccn2  15520  rlimno1  15577  o1fsum  15736  expcnv  15787  geolim  15793  geolim2  15794  georeclim  15795  geomulcvg  15799  geoisumr  15801  geoisum1c  15803  fprodge0  15916  fprodge1  15918  rerisefaccl  15940  refallfaccl  15941  ere  16012  ege2le3  16013  efgt1  16041  resin4p  16063  recos4p  16064  tanhbnd  16086  sinbnd  16105  cosbnd  16106  sinbnd2  16107  cosbnd2  16108  ef01bndlem  16109  sin01bnd  16110  cos01bnd  16111  cos1bnd  16112  cos2bnd  16113  sinltx  16114  sin01gt0  16115  cos01gt0  16116  sin02gt0  16117  sincos1sgn  16118  ene1  16135  rpnnen2lem2  16140  rpnnen2lem3  16141  rpnnen2lem4  16142  rpnnen2lem9  16147  rpnnen2lem12  16150  ruclem6  16160  ruclem11  16165  ruclem12  16166  3dvds  16258  flodddiv4  16342  sadcadd  16385  isprm3  16610  sqnprm  16629  coprm  16638  phibndlem  16697  pythagtriplem3  16746  pcmpt  16820  fldivp1  16825  pockthi  16835  infpn2  16841  basendxnmulrndx  17216  starvndxnbasendx  17224  scandxnbasendx  17236  vscandxnbasendx  17241  ipndxnbasendx  17252  basendxnocndx  17303  slotsbhcdif  17335  lt6abl  19824  srgbinomlem4  20164  0ringnnzr  20458  abvneg  20759  abvtrivd  20765  xrsmcmn  21346  xrsnsgrp  21362  gzrngunitlem  21387  gzrngunit  21388  rge0srg  21393  psgnodpmr  21545  remulg  21562  resubdrg  21563  psdmvr  22112  dscmet  24516  dscopn  24517  nrginvrcnlem  24635  idnghm  24687  tgioo  24740  blcvx  24742  iicmp  24835  iiconn  24836  iirev  24879  iihalf1  24881  iihalf2  24884  iihalf2cnOLD  24886  elii1  24887  elii2  24888  iimulcl  24889  icopnfcnv  24896  icopnfhmeo  24897  iccpnfhmeo  24899  xrhmeo  24900  xrhmph  24901  evth  24914  xlebnum  24920  htpycc  24935  reparphti  24952  reparphtiOLD  24953  pcoval1  24969  pco1  24971  pcoval2  24972  pcocn  24973  pcohtpylem  24975  pcopt  24978  pcopt2  24979  pcoass  24980  pcorevlem  24982  nmhmcn  25076  ncvs1  25113  ovolunlem1a  25453  vitalilem2  25566  vitalilem4  25568  vitalilem5  25569  vitali  25570  i1f1  25647  itg11  25648  itg2const  25697  dveflem  25939  dvlipcn  25955  dvcvx  25981  ply1remlem  26126  fta1blem  26132  vieta1lem2  26275  aalioulem3  26298  aalioulem5  26300  aaliou3lem2  26307  ulmbdd  26363  iblulm  26372  radcnvlem1  26378  dvradcnv  26386  abelthlem2  26398  abelthlem3  26399  abelthlem5  26401  abelthlem7  26404  abelth  26407  abelth2  26408  reeff1olem  26412  reeff1o  26413  sinhalfpilem  26428  tangtx  26470  sincos4thpi  26478  pige3ALT  26485  coskpi  26488  cos0pilt1  26497  recosf1o  26500  tanregt0  26504  efif1olem3  26509  efif1olem4  26510  loge  26551  logdivlti  26585  logcnlem4  26610  logf1o2  26615  logtayl  26625  logccv  26628  recxpcl  26640  cxplea  26661  cxpcn3lem  26713  cxpaddlelem  26717  loglesqrt  26727  ang180lem2  26776  angpined  26796  acosrecl  26869  atancj  26876  atanlogaddlem  26879  atantan  26889  atans2  26897  ressatans  26900  leibpi  26908  log2le1  26916  birthdaylem3  26919  cxp2lim  26943  cxploglim  26944  cxploglim2  26945  divsqrtsumlem  26946  cvxcl  26951  scvxcvx  26952  jensenlem2  26954  amgmlem  26956  emcllem2  26963  emcllem4  26965  emcllem6  26967  emcllem7  26968  emre  26972  emgt0  26973  harmonicbnd3  26974  harmonicubnd  26976  harmonicbnd4  26977  zetacvg  26981  ftalem1  27039  ftalem2  27040  ftalem5  27043  issqf  27102  cht1  27131  chp1  27133  ppiltx  27143  mumullem2  27146  ppiublem1  27169  ppiub  27171  chtublem  27178  chtub  27179  logfacbnd3  27190  logexprlim  27192  perfectlem2  27197  dchrinv  27228  dchr1re  27230  efexple  27248  bposlem1  27251  bposlem2  27252  bposlem5  27255  bposlem8  27258  lgsdir2lem1  27292  lgsdir2lem5  27296  lgsdir  27299  lgsne0  27302  lgsabs1  27303  lgsdinn0  27312  gausslemma2dlem0i  27331  lgseisen  27346  m1lgs  27355  2lgslem3  27371  addsq2nreurex  27411  2sqreultblem  27415  2sqreunnltblem  27418  chebbnd1lem3  27438  chebbnd1  27439  chtppilimlem1  27440  chtppilimlem2  27441  chtppilim  27442  chpchtlim  27446  vmadivsumb  27450  rplogsumlem2  27452  rpvmasumlem  27454  dchrmusumlema  27460  dchrmusum2  27461  dchrvmasumlem2  27465  dchrvmasumiflem1  27468  dchrisum0flblem1  27475  dchrisum0flblem2  27476  dchrisum0fno1  27478  rpvmasum2  27479  dchrisum0re  27480  dchrisum0lema  27481  dchrisum0lem1b  27482  dchrisum0lem1  27483  dchrisum0lem2a  27484  dchrisum0lem2  27485  logdivsum  27500  mulog2sumlem2  27502  2vmadivsumlem  27507  log2sumbnd  27511  selbergb  27516  selberg2b  27519  chpdifbndlem1  27520  selberg3lem1  27524  selberg3lem2  27525  selberg4lem1  27527  pntrmax  27531  pntrsumo1  27532  selbergsb  27542  pntrlog2bndlem3  27546  pntrlog2bndlem5  27548  pntpbnd1a  27552  pntpbnd2  27554  pntibndlem1  27556  pntibndlem3  27559  pntlemd  27561  pntlemc  27562  pntlemb  27564  pntlemr  27569  pntlemf  27572  pntlemk  27573  pntlemo  27574  pntlem3  27576  pntleml  27578  abvcxp  27582  ostth2lem1  27585  ostth1  27600  ostth2lem2  27601  ostth2lem3  27602  ostth2lem4  27603  ostth2  27604  ostth3  27605  ostth  27606  slotsinbpsd  28513  slotslnbpsd  28514  trgcgrg  28587  brbtwn2  28978  colinearalglem4  28982  ax5seglem2  29002  ax5seglem3  29004  axpaschlem  29013  axpasch  29014  axlowdimlem6  29020  axlowdimlem10  29024  axlowdimlem16  29030  axlowdim1  29032  axlowdim2  29033  axlowdim  29034  axcontlem2  29038  elntg2  29058  lfgrnloop  29198  lfuhgr1v0e  29327  usgrexmpldifpr  29331  usgrexmplef  29332  1loopgrvd2  29577  vdegp1bi  29611  lfgrwlkprop  29759  pthdlem1  29839  pthdlem2  29841  clwlkclwwlkf  30083  upgr4cycl4dv4e  30260  konigsberglem2  30328  konigsberglem3  30329  konigsberglem5  30331  frgrreg  30469  ex-dif  30498  ex-in  30500  ex-pss  30503  ex-res  30516  ex-fl  30522  nv1  30750  smcnlem  30772  ipidsq  30785  nmlno0lem  30868  norm-ii-i  31212  bcs2  31257  norm1  31324  nmopub2tALT  31984  nmfnleub2  32001  nmlnop0iALT  32070  unopbd  32090  nmopadjlem  32164  nmopcoadji  32176  pjnmopi  32223  pjbdlni  32224  hstle1  32301  hstle  32305  hstles  32306  stge1i  32313  stlesi  32316  staddi  32321  stadd3i  32323  strlem1  32325  strlem5  32330  jplem1  32343  cdj1i  32508  addltmulALT  32521  xlt2addrd  32839  pr01ssre  32905  sgnclre  32913  sgnnbi  32919  sgnpbi  32920  sgnmulsgp  32924  indf  32934  indfval  32935  dp2lt10  32965  dp2ltsuc  32967  dp2ltc  32968  dplti  32986  dpmul4  32995  cshw1s2  33042  xrsmulgzz  33091  rearchi  33427  xrge0slmod  33429  prmidl0  33531  evl1deg3  33659  constrconj  33902  2sqr3minply  33937  submateqlem1  33964  xrge0iifcnv  34090  xrge0iifcv  34091  xrge0iifiso  34092  xrge0iifhom  34094  zrhre  34176  esumcst  34220  cntnevol  34385  omssubadd  34457  iwrdsplit  34544  dstfrvclim1  34635  coinfliprv  34640  ballotlem2  34646  ballotlem4  34656  ballotlemi1  34660  ballotlemic  34664  plymulx0  34704  plymulx  34705  signswch  34718  signstf  34723  signsvfn  34739  itgexpif  34763  hgt750lemd  34805  logdivsqrle  34807  hgt750lem  34808  hgt750lem2  34809  hgt750leme  34815  tgoldbachgnn  34816  subfacp1lem1  35373  subfacp1lem5  35378  resconn  35440  iisconn  35446  iillysconn  35447  problem2  35860  problem3  35861  sinccvglem  35866  fz0n  35925  dnibndlem12  36689  knoppcnlem4  36696  knoppndvlem13  36724  cnndvlem1  36737  irrdiff  37531  relowlpssretop  37569  sin2h  37811  cos2h  37812  tan2h  37813  poimirlem7  37828  poimirlem16  37837  poimirlem17  37838  poimirlem19  37840  poimirlem20  37841  poimirlem22  37843  poimirlem23  37844  poimirlem29  37850  poimirlem31  37852  itg2addnclem3  37874  asindmre  37904  dvasin  37905  dvacos  37906  dvreasin  37907  dvreacos  37908  fdc  37946  geomcau  37960  cntotbnd  37997  heiborlem8  38019  bfplem2  38024  bfp  38025  aks4d1p1p7  42328  1t1e1ALT  42510  ine1  42569  re1m1e0m0  42652  sn-00idlem1  42653  sn-00idlem2  42654  remul02  42660  sn-0ne2  42661  reixi  42678  rei4  42679  remullid  42689  ipiiie0  42693  sn-0tie0  42706  sn-nnne0  42715  mulgt0b1d  42727  sn-0lt1  42730  sn-ltp1  42731  reneg1lt0  42735  sn-inelr  42742  rabren3dioph  43057  pellexlem5  43075  pellexlem6  43076  pell1qrgaplem  43115  pell14qrgap  43117  pellqrex  43121  pellfundre  43123  pellfundlb  43126  pellfund14gap  43129  jm2.17a  43202  acongeq  43225  jm2.23  43238  jm3.1lem2  43260  sqrtcval  43882  sqrtcval2  43883  resqrtval  43884  imsqrtval  43885  relexp01min  43954  cvgdvgrat  44554  lhe4.4ex1a  44570  binomcxplemnotnn0  44597  isosctrlem1ALT  45174  supxrgelem  45582  xrlexaddrp  45597  infxr  45611  infleinflem2  45615  sumnnodd  45876  limsup10exlem  46016  limsup10ex  46017  dvnprodlem3  46192  stoweidlem1  46245  stoweidlem18  46262  stoweidlem19  46263  stoweidlem26  46270  stoweidlem34  46278  stoweidlem40  46284  stoweidlem41  46285  stoweidlem59  46303  stoweid  46307  stirlinglem10  46327  stirlinglem11  46328  dirkercncflem1  46347  fourierdlem16  46367  fourierdlem21  46372  fourierdlem22  46373  fourierdlem42  46393  fourierdlem68  46418  fourierdlem83  46433  fourierdlem103  46453  sqwvfourb  46473  fouriersw  46475  etransclem23  46501  salgencntex  46587  ovn0lem  46809  smfmullem3  47037  smfmullem4  47038  nthrucw  47130  cjnpoly  47135  zm1nn  47548  ceilhalf1  47580  m1mod0mod1  47600  fmtnosqrt  47785  perfectALTVlem2  47968  2exp340mod341  47979  8exp8mod9  47982  nfermltl8rev  47988  nnsum3primesprm  48036  nnsum4primesodd  48042  nnsum4primesoddALTV  48043  nnsum4primeseven  48046  nnsum4primesevenALTV  48047  tgblthelfgott  48061  tgoldbach  48063  usgrexmpl1lem  48267  usgrexmpl2lem  48272  usgrexmpl2nb1  48278  usgrexmpl2nb3  48280  usgrexmpl2nb4  48281  usgrexmpl2nb5  48282  usgrexmpl2trifr  48283  gpg3kgrtriexlem3  48331  pgnbgreunbgrlem2lem1  48360  pgnbgreunbgrlem2lem2  48361  rege1logbrege0  48804  rege1logbzge0  48805  blennnelnn  48822  dignnld  48849  nn0sumshdiglemA  48865  nn0sumshdiglem1  48867  rrx2xpref1o  48964  rrxlines  48979  eenglngeehlnmlem1  48983  eenglngeehlnmlem2  48984  line2ylem  48997  line2x  49000  icccldii  49164  io1ii  49166  sepfsepc  49173