Theorem 1re 11181

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 11131, 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 11142	. . 3 ⊢ 1 ≠ 0
2		ax-1cn 11131	. . . . 5 ⊢ 1 ∈ ℂ
3		cnre 11178	. . . . 5 ⊢ (1 ∈ ℂ → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)))
4	2, 3	ax-mp 5	. . . 4 ⊢ ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏))
5		neeq1 3019	. . . . . . . 8 ⊢ (1 = (𝑎 + (i · 𝑏)) → (1 ≠ 0 ↔ (𝑎 + (i · 𝑏)) ≠ 0))
6	5	biimpcd 251	. . . . . . 7 ⊢ (1 ≠ 0 → (1 = (𝑎 + (i · 𝑏)) → (𝑎 + (i · 𝑏)) ≠ 0))
7		0cn 11171	. . . . . . . 8 ⊢ 0 ∈ ℂ
8		cnre 11178	. . . . . . . 8 ⊢ (0 ∈ ℂ → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)))
9	7, 8	ax-mp 5	. . . . . . 7 ⊢ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑))
10		neeq2 3020	. . . . . . . . . 10 ⊢ (0 = (𝑐 + (i · 𝑑)) → ((𝑎 + (i · 𝑏)) ≠ 0 ↔ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
11	10	biimpcd 251	. . . . . . . . 9 ⊢ ((𝑎 + (i · 𝑏)) ≠ 0 → (0 = (𝑐 + (i · 𝑑)) → (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
12	11	reximdv 3177	. . . . . . . 8 ⊢ ((𝑎 + (i · 𝑏)) ≠ 0 → (∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)) → ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
13	12	reximdv 3177	. . . . . . 7 ⊢ ((𝑎 + (i · 𝑏)) ≠ 0 → (∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)) → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
14	6, 9, 13	syl6mpi 67	. . . . . 6 ⊢ (1 ≠ 0 → (1 = (𝑎 + (i · 𝑏)) → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
15	14	reximdv 3177	. . . . 5 ⊢ (1 ≠ 0 → (∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)) → ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
16	15	reximdv 3177	. . . 4 ⊢ (1 ≠ 0 → (∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)) → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
17	4, 16	mpi 20	. . 3 ⊢ (1 ≠ 0 → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)))
18		id 22	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑐 → 𝑎 = 𝑐)
19		oveq2 7404	. . . . . . . . . . . 12 ⊢ (𝑏 = 𝑑 → (i · 𝑏) = (i · 𝑑))
20	18, 19	oveqan12d 7415	. . . . . . . . . . 11 ⊢ ((𝑎 = 𝑐 ∧ 𝑏 = 𝑑) → (𝑎 + (i · 𝑏)) = (𝑐 + (i · 𝑑)))
21	20	expcom 417	. . . . . . . . . 10 ⊢ (𝑏 = 𝑑 → (𝑎 = 𝑐 → (𝑎 + (i · 𝑏)) = (𝑐 + (i · 𝑑))))
22	21	necon3d 2978	. . . . . . . . 9 ⊢ (𝑏 = 𝑑 → ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → 𝑎 ≠ 𝑐))
23	22	com12 32	. . . . . . . 8 ⊢ ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → (𝑏 = 𝑑 → 𝑎 ≠ 𝑐))
24	23	necon3bd 2971	. . . . . . 7 ⊢ ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → (¬ 𝑎 ≠ 𝑐 → 𝑏 ≠ 𝑑))
25	24	orrd 874	. . . . . 6 ⊢ ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → (𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑))
26		neeq1 3019	. . . . . . . . . 10 ⊢ (𝑥 = 𝑎 → (𝑥 ≠ 𝑦 ↔ 𝑎 ≠ 𝑦))
27		neeq2 3020	. . . . . . . . . 10 ⊢ (𝑦 = 𝑐 → (𝑎 ≠ 𝑦 ↔ 𝑎 ≠ 𝑐))
28	26, 27	rspc2ev 3594	. . . . . . . . 9 ⊢ ((𝑎 ∈ ℝ ∧ 𝑐 ∈ ℝ ∧ 𝑎 ≠ 𝑐) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦)
29	28	3expia 1134	. . . . . . . 8 ⊢ ((𝑎 ∈ ℝ ∧ 𝑐 ∈ ℝ) → (𝑎 ≠ 𝑐 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
30	29	ad2ant2r 757	. . . . . . 7 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → (𝑎 ≠ 𝑐 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
31		neeq1 3019	. . . . . . . . . 10 ⊢ (𝑥 = 𝑏 → (𝑥 ≠ 𝑦 ↔ 𝑏 ≠ 𝑦))
32		neeq2 3020	. . . . . . . . . 10 ⊢ (𝑦 = 𝑑 → (𝑏 ≠ 𝑦 ↔ 𝑏 ≠ 𝑑))
33	31, 32	rspc2ev 3594	. . . . . . . . 9 ⊢ ((𝑏 ∈ ℝ ∧ 𝑑 ∈ ℝ ∧ 𝑏 ≠ 𝑑) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦)
34	33	3expia 1134	. . . . . . . 8 ⊢ ((𝑏 ∈ ℝ ∧ 𝑑 ∈ ℝ) → (𝑏 ≠ 𝑑 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
35	34	ad2ant2l 756	. . . . . . 7 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → (𝑏 ≠ 𝑑 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
36	30, 35	jaod 870	. . . . . 6 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → ((𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
37	25, 36	syl5 34	. . . . 5 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
38	37	rexlimdvva 3219	. . . 4 ⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
39	38	rexlimivv 3204	. . 3 ⊢ (∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦)
40	1, 17, 39	mp2b 10	. 2 ⊢ ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦
41		eqtr3 2784	. . . . . . . . 9 ⊢ ((𝑥 = 0 ∧ 𝑦 = 0) → 𝑥 = 𝑦)
42	41	ex 416	. . . . . . . 8 ⊢ (𝑥 = 0 → (𝑦 = 0 → 𝑥 = 𝑦))
43	42	necon3d 2978	. . . . . . 7 ⊢ (𝑥 = 0 → (𝑥 ≠ 𝑦 → 𝑦 ≠ 0))
44		neeq1 3019	. . . . . . . . 9 ⊢ (𝑧 = 𝑦 → (𝑧 ≠ 0 ↔ 𝑦 ≠ 0))
45	44	rspcev 3581	. . . . . . . 8 ⊢ ((𝑦 ∈ ℝ ∧ 𝑦 ≠ 0) → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)
46	45	expcom 417	. . . . . . 7 ⊢ (𝑦 ≠ 0 → (𝑦 ∈ ℝ → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
47	43, 46	syl6 35	. . . . . 6 ⊢ (𝑥 = 0 → (𝑥 ≠ 𝑦 → (𝑦 ∈ ℝ → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
48	47	com23 86	. . . . 5 ⊢ (𝑥 = 0 → (𝑦 ∈ ℝ → (𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
49	48	adantld 494	. . . 4 ⊢ (𝑥 = 0 → ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
50		neeq1 3019	. . . . . . . 8 ⊢ (𝑧 = 𝑥 → (𝑧 ≠ 0 ↔ 𝑥 ≠ 0))
51	50	rspcev 3581	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)
52	51	expcom 417	. . . . . 6 ⊢ (𝑥 ≠ 0 → (𝑥 ∈ ℝ → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
53	52	adantrd 495	. . . . 5 ⊢ (𝑥 ≠ 0 → ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
54	53	a1dd 50	. . . 4 ⊢ (𝑥 ≠ 0 → ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
55	49, 54	pm2.61ine 3040	. . 3 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
56	55	rexlimivv 3204	. 2 ⊢ (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)
57		ax-rrecex 11145	. . . 4 ⊢ ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → ∃𝑥 ∈ ℝ (𝑧 · 𝑥) = 1)
58		remulcl 11158	. . . . . . 7 ⊢ ((𝑧 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (𝑧 · 𝑥) ∈ ℝ)
59	58	adantlr 725	. . . . . 6 ⊢ (((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) ∧ 𝑥 ∈ ℝ) → (𝑧 · 𝑥) ∈ ℝ)
60		eleq1 2850	. . . . . 6 ⊢ ((𝑧 · 𝑥) = 1 → ((𝑧 · 𝑥) ∈ ℝ ↔ 1 ∈ ℝ))
61	59, 60	syl5ibcom 247	. . . . 5 ⊢ (((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) ∧ 𝑥 ∈ ℝ) → ((𝑧 · 𝑥) = 1 → 1 ∈ ℝ))
62	61	rexlimdva 3163	. . . 4 ⊢ ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → (∃𝑥 ∈ ℝ (𝑧 · 𝑥) = 1 → 1 ∈ ℝ))
63	57, 62	mpd 15	. . 3 ⊢ ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → 1 ∈ ℝ)
64	63	rexlimiva 3155	. 2 ⊢ (∃𝑧 ∈ ℝ 𝑧 ≠ 0 → 1 ∈ ℝ)
65	40, 56, 64	mp2b 10	1 ⊢ 1 ∈ ℝ

Syntax hints:   → wi 4   ∧ wa 399   ∨ wo 858   = wceq 1560   ∈ wcel 2142   ≠ wne 2957  ∃wrex 3086  (class class class)co 7396  ℂcc 11071  ℝcr 11072  0cc0 11073  1c1 11074  ici 11075   + caddc 11076   · cmul 11078

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734  ax-1cn 11131  ax-icn 11132  ax-addcl 11133  ax-mulcl 11135  ax-mulrcl 11136  ax-i2m1 11141  ax-1ne0 11142  ax-rrecex 11145  ax-cnre 11146

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-ral 3077  df-rex 3087  df-rab 3415  df-v 3456  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4481  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-iota 6477  df-fv 6529  df-ov 7399

This theorem is referenced by:  1red  11182  pr01ssre  11185  1xr  11241  dedekind  11346  peano2re  11356  mul02lem2  11360  addrid  11363  renegcl  11494  peano2rem  11498  0reALT  11528  0lt1  11709  0le1  11710  relin01  11711  1le1  11815  eqneg  11911  ltp1  12031  ltm1  12033  recgt0  12037  mulgt1OLD  12050  ltmulgt11  12051  lemulge11  12054  reclt1  12087  recgt1  12088  recgt1i  12089  recp1lt1  12090  recreclt  12091  recgt0ii  12098  ledivp1i  12117  ltdivp1i  12118  neg1rr  12181  neg1lt0  12183  cju  12191  indf  12201  indfval  12202  nnssre  12214  nnge1  12241  nngt1ne1  12242  nnle1eq1  12243  nngt0  12244  nnnlt1  12245  nnne0  12247  nnrecre  12255  nnrecgt0  12256  nnsub  12257  1t1e1ALT  12268  2re  12292  3re  12298  4re  12302  5re  12305  6re  12308  7re  12311  8re  12314  9re  12317  0le2OLD  12321  2posOLD  12323  1lt2  12390  1lt3  12393  1lt4  12396  1lt5  12400  1lt6  12405  1lt7  12411  1lt8  12418  1lt9  12426  1ne2  12428  1le2  12429  1le3  12432  halflt1  12438  addltmul  12457  nnunb  12477  elnnnn0c  12526  nn0ge2m1nn  12551  elnnz1  12597  znnnlt1  12598  zltp1le  12621  zleltp1  12622  nn0lt2  12636  recnz  12648  gtndiv  12650  3halfnz  12652  10re  12711  1lt10  12833  1lt10OLD  12834  eluzp1m1  12865  eluzp1p1  12867  eluz2b2  12922  zbtwnre  12947  rebtwnz  12948  1rp  12997  divlt1lt  13064  divle1le  13065  nnledivrp  13107  qbtwnxr  13203  xmulrid  13282  xmulm1  13284  x2times  13302  xrub  13315  elicc01  13470  1elunit  13474  divelunit  13498  lincmb01cmp  13499  unitssre  13503  0nelfz1  13548  fzpreddisj  13578  fznatpl1  13583  fztpval  13591  fraclt1  13812  fracle1  13813  flbi2  13827  fldiv4p1lem1div2  13845  fldiv4lem1div2  13847  fldiv  13870  modid  13906  1mod  13913  m1modnnsub1  13930  modm1p1mod0  13935  seqf1olem1  14054  reexpcl  14091  reexpclz  14095  expge0  14111  expge1  14112  expgt1  14113  bernneq  14242  bernneq2  14243  expnbnd  14245  expnlbnd  14246  expnlbnd2  14247  expmulnbnd  14248  discr1  14252  facwordi  14302  faclbnd3  14305  faclbnd4lem1  14306  faclbnd4lem4  14309  faclbnd6  14312  facavg  14314  hashv01gt1  14358  hashnn0n0nn  14404  hashunsnggt  14407  hash1snb  14432  hashgt12el  14435  hashgt12el2  14436  hashfun  14450  hashge2el2dif  14493  tpf1ofv2  14511  lsw0  14578  f1oun2prg  14930  sgnclre  15115  sgnnbi  15117  sgnpbi  15118  cjexp  15177  re1  15181  im1  15182  rei  15183  imi  15184  01sqrexlem1  15269  01sqrexlem2  15270  01sqrexlem3  15271  01sqrexlem4  15272  01sqrexlem7  15275  resqrex  15277  sqrt1  15298  sqrt2gt1lt2  15301  sqrtm1  15302  abs1  15324  absrdbnd  15369  caubnd2  15385  mulcn2  15623  reccn2  15624  rlimno1  15681  o1fsum  15841  expcnv  15894  geolim  15900  geolim2  15901  georeclim  15902  geomulcvg  15906  geoisumr  15908  geoisum1c  15910  fprodge0  16023  fprodge1  16025  rerisefaccl  16047  refallfaccl  16048  ere  16119  ege2le3  16120  efgt1  16148  resin4p  16170  recos4p  16171  tanhbnd  16193  sinbnd  16212  cosbnd  16213  sinbnd2  16214  cosbnd2  16215  ef01bndlem  16216  sin01bnd  16217  cos01bnd  16218  cos1bnd  16219  cos2bnd  16220  sinltx  16221  sin01gt0  16222  cos01gt0  16223  sin02gt0  16224  sincos1sgn  16225  ene1  16242  rpnnen2lem2  16247  rpnnen2lem3  16248  rpnnen2lem4  16249  rpnnen2lem9  16254  rpnnen2lem12  16257  ruclem6  16267  ruclem11  16272  ruclem12  16273  3dvds  16365  flodddiv4  16449  sadcadd  16492  isprm3  16717  sqnprm  16737  coprm  16746  phibndlem  16805  pythagtriplem3  16854  pcmpt  16928  fldivp1  16933  pockthi  16943  infpn2  16949  basendxnmulrndx  17325  starvndxnbasendx  17333  scandxnbasendx  17345  vscandxnbasendx  17350  ipndxnbasendx  17361  basendxnocndx  17412  slotsbhcdif  17444  lt6abl  19935  srgbinomlem4  20279  0ringnnzr  20575  abvneg  20875  abvtrivd  20881  xrsmcmn  21447  xrsnsgrp  21460  gzrngunitlem  21484  gzrngunit  21485  rge0srg  21490  psgnodpmr  21642  remulg  21659  resubdrg  21660  psdmvr  22234  dscmet  24632  dscopn  24633  nrginvrcnlem  24751  idnghm  24803  tgioo  24856  blcvx  24858  iicmp  24948  iiconn  24949  iirev  24991  iihalf1  24993  iihalf2  24995  elii1  24997  elii2  24998  iimulcl  24999  icopnfcnv  25004  icopnfhmeo  25005  iccpnfhmeo  25007  xrhmeo  25008  xrhmph  25009  evth  25021  xlebnum  25027  htpycc  25042  reparphti  25059  pcoval1  25075  pco1  25077  pcoval2  25078  pcocn  25079  pcohtpylem  25081  pcopt  25084  pcopt2  25085  pcoass  25086  pcorevlem  25088  nmhmcn  25182  ncvs1  25219  ovolunlem1a  25558  vitalilem2  25671  vitalilem4  25673  vitalilem5  25674  vitali  25675  i1f1  25752  itg11  25753  itg2const  25802  dveflem  26041  dvlipcn  26056  dvcvx  26082  ply1remlem  26225  fta1blem  26231  plyn0mulidp  26345  plymulidp  26346  vieta1lem2  26375  aalioulem3  26398  aalioulem5  26400  aaliou3lem2  26407  ulmbdd  26461  iblulm  26470  radcnvlem1  26476  dvradcnv  26484  abelthlem2  26495  abelthlem3  26496  abelthlem5  26498  abelthlem7  26501  abelth  26504  abelth2  26505  reeff1olem  26509  reeff1o  26510  sinhalfpilem  26528  tangtx  26570  sincos4thpi  26578  pige3ALT  26585  coskpi  26588  cos0pilt1  26597  recosf1o  26600  tanregt0  26604  efif1olem3  26609  efif1olem4  26610  loge  26651  logdivlti  26685  logcnlem4  26710  logf1o2  26715  logtayl  26725  logccv  26728  recxpcl  26740  cxplea  26761  cxpcn3lem  26812  cxpaddlelem  26816  loglesqrt  26826  ang180lem2  26875  angpined  26895  acosrecl  26968  atancj  26975  atanlogaddlem  26978  atantan  26988  atans2  26996  ressatans  26999  leibpi  27007  log2le1  27015  birthdaylem3  27018  cxp2lim  27041  cxploglim  27042  cxploglim2  27043  divsqrtsumlem  27044  cvxcl  27049  scvxcvx  27050  jensenlem2  27052  amgmlem  27054  emcllem2  27061  emcllem4  27063  emcllem6  27065  emcllem7  27066  emre  27070  emgt0  27071  harmonicbnd3  27072  harmonicubnd  27074  harmonicbnd4  27075  zetacvg  27079  ftalem1  27137  ftalem2  27138  ftalem5  27141  issqf  27200  cht1  27229  chp1  27231  ppiltx  27241  mumullem2  27244  ppiublem1  27266  ppiub  27268  chtublem  27275  chtub  27276  logfacbnd3  27287  logexprlim  27289  perfectlem2  27294  dchrinv  27325  dchr1re  27327  efexple  27345  bposlem1  27348  bposlem2  27349  bposlem5  27352  bposlem8  27355  lgsdir2lem1  27389  lgsdir2lem5  27393  lgsdir  27396  lgsne0  27399  lgsabs1  27400  lgsdinn0  27409  gausslemma2dlem0i  27428  lgseisen  27443  m1lgs  27452  2lgslem3  27468  addsq2nreurex  27508  2sqreultblem  27512  2sqreunnltblem  27515  chebbnd1lem3  27535  chebbnd1  27536  chtppilimlem1  27537  chtppilimlem2  27538  chtppilim  27539  chpchtlim  27543  vmadivsumb  27547  rplogsumlem2  27549  rpvmasumlem  27551  dchrmusumlema  27557  dchrmusum2  27558  dchrvmasumlem2  27562  dchrvmasumiflem1  27565  dchrisum0flblem1  27572  dchrisum0flblem2  27573  dchrisum0fno1  27575  rpvmasum2  27576  dchrisum0re  27577  dchrisum0lema  27578  dchrisum0lem1b  27579  dchrisum0lem1  27580  dchrisum0lem2a  27581  dchrisum0lem2  27582  logdivsum  27597  mulog2sumlem2  27599  2vmadivsumlem  27604  log2sumbnd  27608  selbergb  27613  selberg2b  27616  chpdifbndlem1  27617  selberg3lem1  27621  selberg3lem2  27622  selberg4lem1  27624  pntrmax  27628  pntrsumo1  27629  selbergsb  27639  pntrlog2bndlem3  27643  pntrlog2bndlem5  27645  pntpbnd1a  27649  pntpbnd2  27651  pntibndlem1  27653  pntibndlem3  27656  pntlemd  27658  pntlemc  27659  pntlemb  27661  pntlemr  27666  pntlemf  27669  pntlemk  27670  pntlemo  27671  pntlem3  27673  pntleml  27675  abvcxp  27679  ostth2lem1  27682  ostth1  27697  ostth2lem2  27698  ostth2lem3  27699  ostth2lem4  27700  ostth2  27701  ostth3  27702  ostth  27703  slotsinbpsd  28610  slotslnbpsd  28611  trgcgrg  28684  brbtwn2  29106  colinearalglem4  29110  ax5seglem2  29130  ax5seglem3  29132  axpaschlem  29141  axpasch  29142  axlowdimlem6  29148  axlowdimlem10  29152  axlowdimlem16  29158  axlowdim1  29160  axlowdim2  29161  axlowdim  29162  axcontlem2  29166  elntg2  29186  lfgrnloop  29326  lfuhgr1v0e  29455  usgrexmpldifpr  29459  usgrexmplef  29460  1loopgrvd2  29704  vdegp1bi  29738  lfgrwlkprop  29886  pthdlem1  29966  pthdlem2  29968  clwlkclwwlkf  30210  upgr4cycl4dv4e  30387  konigsberglem2  30455  konigsberglem3  30456  konigsberglem5  30458  frgrreg  30596  ex-dif  30625  ex-in  30627  ex-pss  30630  ex-res  30643  ex-fl  30649  nv1  30878  smcnlem  30900  ipidsq  30913  nmlno0lem  30996  norm-ii-i  31340  bcs2  31385  norm1  31452  nmopub2tALT  32112  nmfnleub2  32129  nmlnop0iALT  32198  unopbd  32218  nmopadjlem  32292  nmopcoadji  32304  pjnmopi  32351  pjbdlni  32352  hstle1  32429  hstle  32433  hstles  32434  stge1i  32441  stlesi  32444  staddi  32449  stadd3i  32451  strlem1  32453  strlem5  32458  jplem1  32471  cdj1i  32636  addltmulALT  32649  xlt2addrd  32961  sgnmulsgp  33034  dp2lt10  33061  dp2ltsuc  33063  dp2ltc  33064  dplti  33082  dpmul4  33091  cshw1s2  33138  xrsmulgzz  33187  rearchi  33532  xrge0slmod  33534  prmidl0  33637  evl1deg3  33774  constrconj  34042  2sqr3minply  34077  submateqlem1  34104  xrge0iifcnv  34230  xrge0iifcv  34231  xrge0iifiso  34232  xrge0iifhom  34234  zrhre  34316  esumcst  34360  cntnevol  34525  omssubadd  34597  iwrdsplit  34684  dstfrvclim1  34775  coinfliprv  34780  ballotlem2  34786  ballotlem4  34796  ballotlemi1  34800  ballotlemic  34804  signswch  34855  signstf  34860  signsvfn  34876  itgexpif  34900  hgt750lemd  34942  logdivsqrle  34944  hgt750lem  34945  hgt750lem2  34946  hgt750leme  34952  tgoldbachgnn  34953  subfacp1lem1  35529  subfacp1lem5  35534  resconn  35596  iisconn  35602  iillysconn  35603  problem2  36016  problem3  36017  sinccvglem  36022  fz0n  36081  dnibndlem12  36927  knoppcnlem4  36934  knoppndvlem13  36962  cnndvlem1  36975  irrdiff  37818  relowlpssretop  37858  sin2h  38109  cos2h  38110  tan2h  38111  poimirlem7  38126  poimirlem16  38135  poimirlem17  38136  poimirlem19  38138  poimirlem20  38139  poimirlem22  38141  poimirlem23  38142  poimirlem29  38148  poimirlem31  38150  itg2addnclem3  38172  asindmre  38202  dvasin  38203  dvacos  38204  dvreasin  38205  dvreacos  38206  fdc  38244  geomcau  38258  cntotbnd  38295  heiborlem8  38317  bfplem2  38322  bfp  38323  aks4d1p1p7  42691  ine1  42923  re1m1e0m0  43006  sn-00idlem1  43007  sn-00idlem2  43008  remul02  43014  sn-0ne2  43015  reixi  43032  rei4  43033  remullid  43043  ipiiie0  43047  sn-0tie0  43073  sn-nnne0  43082  mulgt0b1d  43094  sn-0lt1  43097  sn-ltp1  43098  reneg1lt0  43102  sn-inelr  43109  rabren3dioph  43392  pellexlem5  43410  pellexlem6  43411  pell1qrgaplem  43450  pell14qrgap  43452  pellqrex  43456  pellfundre  43458  pellfundlb  43461  pellfund14gap  43464  jm2.17a  43537  acongeq  43560  jm2.23  43573  jm3.1lem2  43595  sqrtcval  44217  sqrtcval2  44218  resqrtval  44219  imsqrtval  44220  relexp01min  44289  cvgdvgrat  44889  lhe4.4ex1a  44905  binomcxplemnotnn0  44932  isosctrlem1ALT  45509  supxrgelem  45913  xrlexaddrp  45928  infxr  45942  infleinflem2  45946  sumnnodd  46206  limsup10exlem  46346  limsup10ex  46347  dvnprodlem3  46522  stoweidlem1  46575  stoweidlem18  46592  stoweidlem19  46593  stoweidlem26  46600  stoweidlem34  46608  stoweidlem40  46614  stoweidlem41  46615  stoweidlem59  46633  stoweid  46637  stirlinglem10  46657  stirlinglem11  46658  dirkercncflem1  46677  fourierdlem16  46697  fourierdlem21  46702  fourierdlem22  46703  fourierdlem42  46723  fourierdlem68  46748  fourierdlem83  46763  fourierdlem103  46783  sqwvfourb  46803  fouriersw  46805  etransclem23  46831  salgencntex  46917  ovn0lem  47139  smfmullem3  47367  smfmullem4  47368  nthrucw  47462  cjnpoly  47483  zm1nn  47896  ceilhalf1  47932  m1mod0mod1  47954  muldvdsfacgt  47980  fmtnosqrt  48148  nprmdvdsfacm1lem4  48232  perfectALTVlem2  48344  2exp340mod341  48355  8exp8mod9  48358  nfermltl8rev  48364  nnsum3primesprm  48412  nnsum4primesodd  48418  nnsum4primesoddALTV  48419  nnsum4primeseven  48422  nnsum4primesevenALTV  48423  tgblthelfgott  48437  tgoldbach  48439  usgrexmpl1lem  48643  usgrexmpl2lem  48648  usgrexmpl2nb1  48654  usgrexmpl2nb3  48656  usgrexmpl2nb4  48657  usgrexmpl2nb5  48658  usgrexmpl2trifr  48659  gpg3kgrtriexlem3  48707  pgnbgreunbgrlem2lem1  48736  pgnbgreunbgrlem2lem2  48737  rege1logbrege0  49180  rege1logbzge0  49181  blennnelnn  49198  dignnld  49225  nn0sumshdiglemA  49241  nn0sumshdiglem1  49243  rrx2xpref1o  49340  rrxlines  49355  eenglngeehlnmlem1  49359  eenglngeehlnmlem2  49360  line2ylem  49373  line2x  49376  icccldii  49540  io1ii  49542  sepfsepc  49549