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 11133, 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 11144	. . 3 ⊢ 1 ≠ 0
2		ax-1cn 11133	. . . . 5 ⊢ 1 ∈ ℂ
3		cnre 11178	. . . . 5 ⊢ (1 ∈ ℂ → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)))
4	2, 3	ax-mp 5	. . . 4 ⊢ ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏))
5		neeq1 2988	. . . . . . . 8 ⊢ (1 = (𝑎 + (i · 𝑏)) → (1 ≠ 0 ↔ (𝑎 + (i · 𝑏)) ≠ 0))
6	5	biimpcd 249	. . . . . . 7 ⊢ (1 ≠ 0 → (1 = (𝑎 + (i · 𝑏)) → (𝑎 + (i · 𝑏)) ≠ 0))
7		0cn 11173	. . . . . . . 8 ⊢ 0 ∈ ℂ
8		cnre 11178	. . . . . . . 8 ⊢ (0 ∈ ℂ → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)))
9	7, 8	ax-mp 5	. . . . . . 7 ⊢ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑))
10		neeq2 2989	. . . . . . . . . 10 ⊢ (0 = (𝑐 + (i · 𝑑)) → ((𝑎 + (i · 𝑏)) ≠ 0 ↔ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
11	10	biimpcd 249	. . . . . . . . 9 ⊢ ((𝑎 + (i · 𝑏)) ≠ 0 → (0 = (𝑐 + (i · 𝑑)) → (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
12	11	reximdv 3149	. . . . . . . 8 ⊢ ((𝑎 + (i · 𝑏)) ≠ 0 → (∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)) → ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
13	12	reximdv 3149	. . . . . . 7 ⊢ ((𝑎 + (i · 𝑏)) ≠ 0 → (∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)) → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
14	6, 9, 13	syl6mpi 67	. . . . . 6 ⊢ (1 ≠ 0 → (1 = (𝑎 + (i · 𝑏)) → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
15	14	reximdv 3149	. . . . 5 ⊢ (1 ≠ 0 → (∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)) → ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
16	15	reximdv 3149	. . . 4 ⊢ (1 ≠ 0 → (∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)) → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
17	4, 16	mpi 20	. . 3 ⊢ (1 ≠ 0 → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)))
18		id 22	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑐 → 𝑎 = 𝑐)
19		oveq2 7398	. . . . . . . . . . . 12 ⊢ (𝑏 = 𝑑 → (i · 𝑏) = (i · 𝑑))
20	18, 19	oveqan12d 7409	. . . . . . . . . . 11 ⊢ ((𝑎 = 𝑐 ∧ 𝑏 = 𝑑) → (𝑎 + (i · 𝑏)) = (𝑐 + (i · 𝑑)))
21	20	expcom 413	. . . . . . . . . 10 ⊢ (𝑏 = 𝑑 → (𝑎 = 𝑐 → (𝑎 + (i · 𝑏)) = (𝑐 + (i · 𝑑))))
22	21	necon3d 2947	. . . . . . . . 9 ⊢ (𝑏 = 𝑑 → ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → 𝑎 ≠ 𝑐))
23	22	com12 32	. . . . . . . 8 ⊢ ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → (𝑏 = 𝑑 → 𝑎 ≠ 𝑐))
24	23	necon3bd 2940	. . . . . . 7 ⊢ ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → (¬ 𝑎 ≠ 𝑐 → 𝑏 ≠ 𝑑))
25	24	orrd 863	. . . . . 6 ⊢ ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → (𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑))
26		neeq1 2988	. . . . . . . . . 10 ⊢ (𝑥 = 𝑎 → (𝑥 ≠ 𝑦 ↔ 𝑎 ≠ 𝑦))
27		neeq2 2989	. . . . . . . . . 10 ⊢ (𝑦 = 𝑐 → (𝑎 ≠ 𝑦 ↔ 𝑎 ≠ 𝑐))
28	26, 27	rspc2ev 3604	. . . . . . . . 9 ⊢ ((𝑎 ∈ ℝ ∧ 𝑐 ∈ ℝ ∧ 𝑎 ≠ 𝑐) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦)
29	28	3expia 1121	. . . . . . . 8 ⊢ ((𝑎 ∈ ℝ ∧ 𝑐 ∈ ℝ) → (𝑎 ≠ 𝑐 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
30	29	ad2ant2r 747	. . . . . . 7 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → (𝑎 ≠ 𝑐 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
31		neeq1 2988	. . . . . . . . . 10 ⊢ (𝑥 = 𝑏 → (𝑥 ≠ 𝑦 ↔ 𝑏 ≠ 𝑦))
32		neeq2 2989	. . . . . . . . . 10 ⊢ (𝑦 = 𝑑 → (𝑏 ≠ 𝑦 ↔ 𝑏 ≠ 𝑑))
33	31, 32	rspc2ev 3604	. . . . . . . . 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 3195	. . . 4 ⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
39	38	rexlimivv 3180	. . 3 ⊢ (∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦)
40	1, 17, 39	mp2b 10	. 2 ⊢ ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦
41		eqtr3 2752	. . . . . . . . 9 ⊢ ((𝑥 = 0 ∧ 𝑦 = 0) → 𝑥 = 𝑦)
42	41	ex 412	. . . . . . . 8 ⊢ (𝑥 = 0 → (𝑦 = 0 → 𝑥 = 𝑦))
43	42	necon3d 2947	. . . . . . 7 ⊢ (𝑥 = 0 → (𝑥 ≠ 𝑦 → 𝑦 ≠ 0))
44		neeq1 2988	. . . . . . . . 9 ⊢ (𝑧 = 𝑦 → (𝑧 ≠ 0 ↔ 𝑦 ≠ 0))
45	44	rspcev 3591	. . . . . . . 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 2988	. . . . . . . 8 ⊢ (𝑧 = 𝑥 → (𝑧 ≠ 0 ↔ 𝑥 ≠ 0))
51	50	rspcev 3591	. . . . . . 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 3009	. . 3 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
56	55	rexlimivv 3180	. 2 ⊢ (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)
57		ax-rrecex 11147	. . . 4 ⊢ ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → ∃𝑥 ∈ ℝ (𝑧 · 𝑥) = 1)
58		remulcl 11160	. . . . . . 7 ⊢ ((𝑧 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (𝑧 · 𝑥) ∈ ℝ)
59	58	adantlr 715	. . . . . 6 ⊢ (((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) ∧ 𝑥 ∈ ℝ) → (𝑧 · 𝑥) ∈ ℝ)
60		eleq1 2817	. . . . . 6 ⊢ ((𝑧 · 𝑥) = 1 → ((𝑧 · 𝑥) ∈ ℝ ↔ 1 ∈ ℝ))
61	59, 60	syl5ibcom 245	. . . . 5 ⊢ (((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) ∧ 𝑥 ∈ ℝ) → ((𝑧 · 𝑥) = 1 → 1 ∈ ℝ))
62	61	rexlimdva 3135	. . . 4 ⊢ ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → (∃𝑥 ∈ ℝ (𝑧 · 𝑥) = 1 → 1 ∈ ℝ))
63	57, 62	mpd 15	. . 3 ⊢ ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → 1 ∈ ℝ)
64	63	rexlimiva 3127	. 2 ⊢ (∃𝑧 ∈ ℝ 𝑧 ≠ 0 → 1 ∈ ℝ)
65	40, 56, 64	mp2b 10	1 ⊢ 1 ∈ ℝ

Syntax hints:   → wi 4   ∧ wa 395   ∨ wo 847   = wceq 1540   ∈ wcel 2109   ≠ wne 2926  ∃wrex 3054  (class class class)co 7390  ℂcc 11073  ℝcr 11074  0cc0 11075  1c1 11076  ici 11077   + caddc 11078   · cmul 11080

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 2702  ax-1cn 11133  ax-icn 11134  ax-addcl 11135  ax-mulcl 11137  ax-mulrcl 11138  ax-i2m1 11143  ax-1ne0 11144  ax-rrecex 11147  ax-cnre 11148

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 2709  df-cleq 2722  df-clel 2804  df-ne 2927  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-iota 6467  df-fv 6522  df-ov 7393

This theorem is referenced by:  1red  11182  1xr  11240  dedekind  11344  peano2re  11354  mul02lem2  11358  addrid  11361  renegcl  11492  peano2rem  11496  0reALT  11526  0lt1  11707  0le1  11708  relin01  11709  1le1  11813  eqneg  11909  ltp1  12029  ltm1  12031  recgt0  12035  mulgt1OLD  12048  ltmulgt11  12049  lemulge11  12052  reclt1  12085  recgt1  12086  recgt1i  12087  recp1lt1  12088  recreclt  12089  recgt0ii  12096  ledivp1i  12115  ltdivp1i  12116  neg1rr  12179  neg1lt0  12181  cju  12189  nnssre  12197  nnge1  12221  nngt1ne1  12222  nnle1eq1  12223  nngt0  12224  nnnlt1  12225  nnne0  12227  nnrecre  12235  nnrecgt0  12236  nnsub  12237  2re  12267  3re  12273  4re  12277  5re  12280  6re  12283  7re  12286  8re  12289  9re  12292  0le2  12295  2pos  12296  3pos  12298  4pos  12300  5pos  12302  6pos  12303  7pos  12304  8pos  12305  9pos  12306  1lt2  12359  1lt3  12361  1lt4  12364  1lt5  12368  1lt6  12373  1lt7  12379  1lt8  12386  1lt9  12394  1ne2  12396  1le2  12397  1le3  12400  halflt1  12406  addltmul  12425  nnunb  12445  elnnnn0c  12494  nn0ge2m1nn  12519  elnnz1  12566  znnnlt1  12567  zltp1le  12590  zleltp1  12591  nn0lt2  12604  recnz  12616  gtndiv  12618  3halfnz  12620  10re  12675  1lt10  12795  eluzp1m1  12826  eluzp1p1  12828  eluz2b2  12887  zbtwnre  12912  rebtwnz  12913  1rp  12962  divlt1lt  13029  divle1le  13030  nnledivrp  13072  qbtwnxr  13167  xmulrid  13246  xmulm1  13248  x2times  13266  xrub  13279  elicc01  13434  1elunit  13438  divelunit  13462  lincmb01cmp  13463  unitssre  13467  0nelfz1  13511  fzpreddisj  13541  fznatpl1  13546  fztpval  13554  fraclt1  13771  fracle1  13772  flbi2  13786  fldiv4p1lem1div2  13804  fldiv4lem1div2  13806  fldiv  13829  modid  13865  1mod  13872  m1modnnsub1  13889  modm1p1mod0  13894  seqf1olem1  14013  reexpcl  14050  reexpclz  14054  expge0  14070  expge1  14071  expgt1  14072  bernneq  14201  bernneq2  14202  expnbnd  14204  expnlbnd  14205  expnlbnd2  14206  expmulnbnd  14207  discr1  14211  facwordi  14261  faclbnd3  14264  faclbnd4lem1  14265  faclbnd4lem4  14268  faclbnd6  14271  facavg  14273  hashv01gt1  14317  hashnn0n0nn  14363  hashunsnggt  14366  hash1snb  14391  hashgt12el  14394  hashgt12el2  14395  hashfun  14409  hashge2el2dif  14452  tpf1ofv2  14470  lsw0  14537  f1oun2prg  14890  cjexp  15123  re1  15127  im1  15128  rei  15129  imi  15130  01sqrexlem1  15215  01sqrexlem2  15216  01sqrexlem3  15217  01sqrexlem4  15218  01sqrexlem7  15221  resqrex  15223  sqrt1  15244  sqrt2gt1lt2  15247  sqrtm1  15248  abs1  15270  absrdbnd  15315  caubnd2  15331  mulcn2  15569  reccn2  15570  rlimno1  15627  o1fsum  15786  expcnv  15837  geolim  15843  geolim2  15844  georeclim  15845  geomulcvg  15849  geoisumr  15851  geoisum1c  15853  fprodge0  15966  fprodge1  15968  rerisefaccl  15990  refallfaccl  15991  ere  16062  ege2le3  16063  efgt1  16091  resin4p  16113  recos4p  16114  tanhbnd  16136  sinbnd  16155  cosbnd  16156  sinbnd2  16157  cosbnd2  16158  ef01bndlem  16159  sin01bnd  16160  cos01bnd  16161  cos1bnd  16162  cos2bnd  16163  sinltx  16164  sin01gt0  16165  cos01gt0  16166  sin02gt0  16167  sincos1sgn  16168  ene1  16185  rpnnen2lem2  16190  rpnnen2lem3  16191  rpnnen2lem4  16192  rpnnen2lem9  16197  rpnnen2lem12  16200  ruclem6  16210  ruclem11  16215  ruclem12  16216  3dvds  16308  flodddiv4  16392  sadcadd  16435  isprm3  16660  sqnprm  16679  coprm  16688  phibndlem  16747  pythagtriplem3  16796  pcmpt  16870  fldivp1  16875  pockthi  16885  infpn2  16891  basendxnmulrndx  17266  starvndxnbasendx  17274  scandxnbasendx  17286  vscandxnbasendx  17291  ipndxnbasendx  17302  basendxnocndx  17353  slotsbhcdif  17385  lt6abl  19832  srgbinomlem4  20145  0ringnnzr  20441  abvneg  20742  abvtrivd  20748  xrsmcmn  21310  xrsnsgrp  21326  gzrngunitlem  21356  gzrngunit  21357  rge0srg  21362  psgnodpmr  21506  remulg  21523  resubdrg  21524  psdmvr  22063  dscmet  24467  dscopn  24468  nrginvrcnlem  24586  idnghm  24638  tgioo  24691  blcvx  24693  iicmp  24786  iiconn  24787  iirev  24830  iihalf1  24832  iihalf2  24835  iihalf2cnOLD  24837  elii1  24838  elii2  24839  iimulcl  24840  icopnfcnv  24847  icopnfhmeo  24848  iccpnfhmeo  24850  xrhmeo  24851  xrhmph  24852  evth  24865  xlebnum  24871  htpycc  24886  reparphti  24903  reparphtiOLD  24904  pcoval1  24920  pco1  24922  pcoval2  24923  pcocn  24924  pcohtpylem  24926  pcopt  24929  pcopt2  24930  pcoass  24931  pcorevlem  24933  nmhmcn  25027  ncvs1  25064  ovolunlem1a  25404  vitalilem2  25517  vitalilem4  25519  vitalilem5  25520  vitali  25521  i1f1  25598  itg11  25599  itg2const  25648  dveflem  25890  dvlipcn  25906  dvcvx  25932  ply1remlem  26077  fta1blem  26083  vieta1lem2  26226  aalioulem3  26249  aalioulem5  26251  aaliou3lem2  26258  ulmbdd  26314  iblulm  26323  radcnvlem1  26329  dvradcnv  26337  abelthlem2  26349  abelthlem3  26350  abelthlem5  26352  abelthlem7  26355  abelth  26358  abelth2  26359  reeff1olem  26363  reeff1o  26364  sinhalfpilem  26379  tangtx  26421  sincos4thpi  26429  pige3ALT  26436  coskpi  26439  cos0pilt1  26448  recosf1o  26451  tanregt0  26455  efif1olem3  26460  efif1olem4  26461  loge  26502  logdivlti  26536  logcnlem4  26561  logf1o2  26566  logtayl  26576  logccv  26579  recxpcl  26591  cxplea  26612  cxpcn3lem  26664  cxpaddlelem  26668  loglesqrt  26678  ang180lem2  26727  angpined  26747  acosrecl  26820  atancj  26827  atanlogaddlem  26830  atantan  26840  atans2  26848  ressatans  26851  leibpi  26859  log2le1  26867  birthdaylem3  26870  cxp2lim  26894  cxploglim  26895  cxploglim2  26896  divsqrtsumlem  26897  cvxcl  26902  scvxcvx  26903  jensenlem2  26905  amgmlem  26907  emcllem2  26914  emcllem4  26916  emcllem6  26918  emcllem7  26919  emre  26923  emgt0  26924  harmonicbnd3  26925  harmonicubnd  26927  harmonicbnd4  26928  zetacvg  26932  ftalem1  26990  ftalem2  26991  ftalem5  26994  issqf  27053  cht1  27082  chp1  27084  ppiltx  27094  mumullem2  27097  ppiublem1  27120  ppiub  27122  chtublem  27129  chtub  27130  logfacbnd3  27141  logexprlim  27143  perfectlem2  27148  dchrinv  27179  dchr1re  27181  efexple  27199  bposlem1  27202  bposlem2  27203  bposlem5  27206  bposlem8  27209  lgsdir2lem1  27243  lgsdir2lem5  27247  lgsdir  27250  lgsne0  27253  lgsabs1  27254  lgsdinn0  27263  gausslemma2dlem0i  27282  lgseisen  27297  m1lgs  27306  2lgslem3  27322  addsq2nreurex  27362  2sqreultblem  27366  2sqreunnltblem  27369  chebbnd1lem3  27389  chebbnd1  27390  chtppilimlem1  27391  chtppilimlem2  27392  chtppilim  27393  chpchtlim  27397  vmadivsumb  27401  rplogsumlem2  27403  rpvmasumlem  27405  dchrmusumlema  27411  dchrmusum2  27412  dchrvmasumlem2  27416  dchrvmasumiflem1  27419  dchrisum0flblem1  27426  dchrisum0flblem2  27427  dchrisum0fno1  27429  rpvmasum2  27430  dchrisum0re  27431  dchrisum0lema  27432  dchrisum0lem1b  27433  dchrisum0lem1  27434  dchrisum0lem2a  27435  dchrisum0lem2  27436  logdivsum  27451  mulog2sumlem2  27453  2vmadivsumlem  27458  log2sumbnd  27462  selbergb  27467  selberg2b  27470  chpdifbndlem1  27471  selberg3lem1  27475  selberg3lem2  27476  selberg4lem1  27478  pntrmax  27482  pntrsumo1  27483  selbergsb  27493  pntrlog2bndlem3  27497  pntrlog2bndlem5  27499  pntpbnd1a  27503  pntpbnd2  27505  pntibndlem1  27507  pntibndlem3  27510  pntlemd  27512  pntlemc  27513  pntlemb  27515  pntlemr  27520  pntlemf  27523  pntlemk  27524  pntlemo  27525  pntlem3  27527  pntleml  27529  abvcxp  27533  ostth2lem1  27536  ostth1  27551  ostth2lem2  27552  ostth2lem3  27553  ostth2lem4  27554  ostth2  27555  ostth3  27556  ostth  27557  slotsinbpsd  28375  slotslnbpsd  28376  trgcgrg  28449  brbtwn2  28839  colinearalglem4  28843  ax5seglem2  28863  ax5seglem3  28865  axpaschlem  28874  axpasch  28875  axlowdimlem6  28881  axlowdimlem10  28885  axlowdimlem16  28891  axlowdim1  28893  axlowdim2  28894  axlowdim  28895  axcontlem2  28899  elntg2  28919  lfgrnloop  29059  lfuhgr1v0e  29188  usgrexmpldifpr  29192  usgrexmplef  29193  1loopgrvd2  29438  vdegp1bi  29472  lfgrwlkprop  29622  pthdlem1  29703  pthdlem2  29705  clwlkclwwlkf  29944  upgr4cycl4dv4e  30121  konigsberglem2  30189  konigsberglem3  30190  konigsberglem5  30192  frgrreg  30330  ex-dif  30359  ex-in  30361  ex-pss  30364  ex-res  30377  ex-fl  30383  nv1  30611  smcnlem  30633  ipidsq  30646  nmlno0lem  30729  norm-ii-i  31073  bcs2  31118  norm1  31185  nmopub2tALT  31845  nmfnleub2  31862  nmlnop0iALT  31931  unopbd  31951  nmopadjlem  32025  nmopcoadji  32037  pjnmopi  32084  pjbdlni  32085  hstle1  32162  hstle  32166  hstles  32167  stge1i  32174  stlesi  32177  staddi  32182  stadd3i  32184  strlem1  32186  strlem5  32191  jplem1  32204  cdj1i  32369  addltmulALT  32382  xlt2addrd  32689  pr01ssre  32756  sgnclre  32764  sgnnbi  32770  sgnpbi  32771  sgnmulsgp  32775  indf  32785  indfval  32786  dp2lt10  32811  dp2ltsuc  32813  dp2ltc  32814  dplti  32832  dpmul4  32841  cshw1s2  32889  xrsmulgzz  32954  rearchi  33324  xrge0slmod  33326  prmidl0  33428  evl1deg3  33554  constrconj  33742  2sqr3minply  33777  submateqlem1  33804  xrge0iifcnv  33930  xrge0iifcv  33931  xrge0iifiso  33932  xrge0iifhom  33934  zrhre  34016  esumcst  34060  cntnevol  34225  omssubadd  34298  iwrdsplit  34385  dstfrvclim1  34476  coinfliprv  34481  ballotlem2  34487  ballotlem4  34497  ballotlemi1  34501  ballotlemic  34505  plymulx0  34545  plymulx  34546  signswch  34559  signstf  34564  signsvfn  34580  itgexpif  34604  hgt750lemd  34646  logdivsqrle  34648  hgt750lem  34649  hgt750lem2  34650  hgt750leme  34656  tgoldbachgnn  34657  subfacp1lem1  35173  subfacp1lem5  35178  resconn  35240  iisconn  35246  iillysconn  35247  problem2  35660  problem3  35661  sinccvglem  35666  fz0n  35725  dnibndlem12  36484  knoppcnlem4  36491  knoppndvlem13  36519  cnndvlem1  36532  irrdiff  37321  relowlpssretop  37359  sin2h  37611  cos2h  37612  tan2h  37613  poimirlem7  37628  poimirlem16  37637  poimirlem17  37638  poimirlem19  37640  poimirlem20  37641  poimirlem22  37643  poimirlem23  37644  poimirlem29  37650  poimirlem31  37652  itg2addnclem3  37674  asindmre  37704  dvasin  37705  dvacos  37706  dvreasin  37707  dvreacos  37708  fdc  37746  geomcau  37760  cntotbnd  37797  heiborlem8  37819  bfplem2  37824  bfp  37825  aks4d1p1p7  42069  1t1e1ALT  42250  ine1  42309  re1m1e0m0  42392  sn-00idlem1  42393  sn-00idlem2  42394  remul02  42400  sn-0ne2  42401  reixi  42418  rei4  42419  remullid  42429  ipiiie0  42433  sn-0tie0  42446  sn-nnne0  42455  mulgt0b1d  42467  sn-0lt1  42470  sn-ltp1  42471  reneg1lt0  42475  sn-inelr  42482  rabren3dioph  42810  pellexlem5  42828  pellexlem6  42829  pell1qrgaplem  42868  pell14qrgap  42870  pellqrex  42874  pellfundre  42876  pellfundlb  42879  pellfund14gap  42882  jm2.17a  42956  acongeq  42979  jm2.23  42992  jm3.1lem2  43014  sqrtcval  43637  sqrtcval2  43638  resqrtval  43639  imsqrtval  43640  relexp01min  43709  cvgdvgrat  44309  lhe4.4ex1a  44325  binomcxplemnotnn0  44352  isosctrlem1ALT  44930  supxrgelem  45340  xrlexaddrp  45355  infxr  45370  infleinflem2  45374  sumnnodd  45635  limsup10exlem  45777  limsup10ex  45778  dvnprodlem3  45953  stoweidlem1  46006  stoweidlem18  46023  stoweidlem19  46024  stoweidlem26  46031  stoweidlem34  46039  stoweidlem40  46045  stoweidlem41  46046  stoweidlem59  46064  stoweid  46068  stirlinglem10  46088  stirlinglem11  46089  dirkercncflem1  46108  fourierdlem16  46128  fourierdlem21  46133  fourierdlem22  46134  fourierdlem42  46154  fourierdlem68  46179  fourierdlem83  46194  fourierdlem103  46214  sqwvfourb  46234  fouriersw  46236  etransclem23  46262  salgencntex  46348  ovn0lem  46570  smfmullem3  46798  smfmullem4  46799  zm1nn  47307  ceilhalf1  47339  m1mod0mod1  47359  fmtnosqrt  47544  perfectALTVlem2  47727  2exp340mod341  47738  8exp8mod9  47741  nfermltl8rev  47747  nnsum3primesprm  47795  nnsum4primesodd  47801  nnsum4primesoddALTV  47802  nnsum4primeseven  47805  nnsum4primesevenALTV  47806  tgblthelfgott  47820  tgoldbach  47822  usgrexmpl1lem  48016  usgrexmpl2lem  48021  usgrexmpl2nb1  48027  usgrexmpl2nb3  48029  usgrexmpl2nb4  48030  usgrexmpl2nb5  48031  usgrexmpl2trifr  48032  gpg3kgrtriexlem3  48080  pgnbgreunbgrlem2lem1  48108  pgnbgreunbgrlem2lem2  48109  rege1logbrege0  48551  rege1logbzge0  48552  blennnelnn  48569  dignnld  48596  nn0sumshdiglemA  48612  nn0sumshdiglem1  48614  rrx2xpref1o  48711  rrxlines  48726  eenglngeehlnmlem1  48730  eenglngeehlnmlem2  48731  line2ylem  48744  line2x  48747  icccldii  48911  io1ii  48913  sepfsepc  48920