Theorem 1re 11130

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 11082, 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 11093	. . 3 ⊢ 1 ≠ 0
2		ax-1cn 11082	. . . . 5 ⊢ 1 ∈ ℂ
3		cnre 11127	. . . . 5 ⊢ (1 ∈ ℂ → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)))
4	2, 3	ax-mp 5	. . . 4 ⊢ ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏))
5		neeq1 2992	. . . . . . . 8 ⊢ (1 = (𝑎 + (i · 𝑏)) → (1 ≠ 0 ↔ (𝑎 + (i · 𝑏)) ≠ 0))
6	5	biimpcd 249	. . . . . . 7 ⊢ (1 ≠ 0 → (1 = (𝑎 + (i · 𝑏)) → (𝑎 + (i · 𝑏)) ≠ 0))
7		0cn 11122	. . . . . . . 8 ⊢ 0 ∈ ℂ
8		cnre 11127	. . . . . . . 8 ⊢ (0 ∈ ℂ → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)))
9	7, 8	ax-mp 5	. . . . . . 7 ⊢ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑))
10		neeq2 2993	. . . . . . . . . 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 7364	. . . . . . . . . . . 12 ⊢ (𝑏 = 𝑑 → (i · 𝑏) = (i · 𝑑))
20	18, 19	oveqan12d 7375	. . . . . . . . . . 11 ⊢ ((𝑎 = 𝑐 ∧ 𝑏 = 𝑑) → (𝑎 + (i · 𝑏)) = (𝑐 + (i · 𝑑)))
21	20	expcom 413	. . . . . . . . . 10 ⊢ (𝑏 = 𝑑 → (𝑎 = 𝑐 → (𝑎 + (i · 𝑏)) = (𝑐 + (i · 𝑑))))
22	21	necon3d 2951	. . . . . . . . 9 ⊢ (𝑏 = 𝑑 → ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → 𝑎 ≠ 𝑐))
23	22	com12 32	. . . . . . . 8 ⊢ ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → (𝑏 = 𝑑 → 𝑎 ≠ 𝑐))
24	23	necon3bd 2944	. . . . . . 7 ⊢ ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → (¬ 𝑎 ≠ 𝑐 → 𝑏 ≠ 𝑑))
25	24	orrd 863	. . . . . 6 ⊢ ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → (𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑))
26		neeq1 2992	. . . . . . . . . 10 ⊢ (𝑥 = 𝑎 → (𝑥 ≠ 𝑦 ↔ 𝑎 ≠ 𝑦))
27		neeq2 2993	. . . . . . . . . 10 ⊢ (𝑦 = 𝑐 → (𝑎 ≠ 𝑦 ↔ 𝑎 ≠ 𝑐))
28	26, 27	rspc2ev 3587	. . . . . . . . 9 ⊢ ((𝑎 ∈ ℝ ∧ 𝑐 ∈ ℝ ∧ 𝑎 ≠ 𝑐) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦)
29	28	3expia 1121	. . . . . . . 8 ⊢ ((𝑎 ∈ ℝ ∧ 𝑐 ∈ ℝ) → (𝑎 ≠ 𝑐 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
30	29	ad2ant2r 747	. . . . . . 7 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → (𝑎 ≠ 𝑐 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
31		neeq1 2992	. . . . . . . . . 10 ⊢ (𝑥 = 𝑏 → (𝑥 ≠ 𝑦 ↔ 𝑏 ≠ 𝑦))
32		neeq2 2993	. . . . . . . . . 10 ⊢ (𝑦 = 𝑑 → (𝑏 ≠ 𝑦 ↔ 𝑏 ≠ 𝑑))
33	31, 32	rspc2ev 3587	. . . . . . . . 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 3191	. . . 4 ⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
39	38	rexlimivv 3176	. . 3 ⊢ (∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦)
40	1, 17, 39	mp2b 10	. 2 ⊢ ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦
41		eqtr3 2756	. . . . . . . . 9 ⊢ ((𝑥 = 0 ∧ 𝑦 = 0) → 𝑥 = 𝑦)
42	41	ex 412	. . . . . . . 8 ⊢ (𝑥 = 0 → (𝑦 = 0 → 𝑥 = 𝑦))
43	42	necon3d 2951	. . . . . . 7 ⊢ (𝑥 = 0 → (𝑥 ≠ 𝑦 → 𝑦 ≠ 0))
44		neeq1 2992	. . . . . . . . 9 ⊢ (𝑧 = 𝑦 → (𝑧 ≠ 0 ↔ 𝑦 ≠ 0))
45	44	rspcev 3574	. . . . . . . 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 2992	. . . . . . . 8 ⊢ (𝑧 = 𝑥 → (𝑧 ≠ 0 ↔ 𝑥 ≠ 0))
51	50	rspcev 3574	. . . . . . 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 3013	. . 3 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
56	55	rexlimivv 3176	. 2 ⊢ (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)
57		ax-rrecex 11096	. . . 4 ⊢ ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → ∃𝑥 ∈ ℝ (𝑧 · 𝑥) = 1)
58		remulcl 11109	. . . . . . 7 ⊢ ((𝑧 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (𝑧 · 𝑥) ∈ ℝ)
59	58	adantlr 715	. . . . . 6 ⊢ (((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) ∧ 𝑥 ∈ ℝ) → (𝑧 · 𝑥) ∈ ℝ)
60		eleq1 2822	. . . . . 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 1541   ∈ wcel 2113   ≠ wne 2930  ∃wrex 3058  (class class class)co 7356  ℂcc 11022  ℝcr 11023  0cc0 11024  1c1 11025  ici 11026   + caddc 11027   · cmul 11029

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 2706  ax-1cn 11082  ax-icn 11083  ax-addcl 11084  ax-mulcl 11086  ax-mulrcl 11087  ax-i2m1 11092  ax-1ne0 11093  ax-rrecex 11096  ax-cnre 11097

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 2713  df-cleq 2726  df-clel 2809  df-ne 2931  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-br 5097  df-iota 6446  df-fv 6498  df-ov 7359

This theorem is referenced by:  1red  11131  1xr  11189  dedekind  11294  peano2re  11304  mul02lem2  11308  addrid  11311  renegcl  11442  peano2rem  11446  0reALT  11476  0lt1  11657  0le1  11658  relin01  11659  1le1  11763  eqneg  11859  ltp1  11979  ltm1  11981  recgt0  11985  mulgt1OLD  11998  ltmulgt11  11999  lemulge11  12002  reclt1  12035  recgt1  12036  recgt1i  12037  recp1lt1  12038  recreclt  12039  recgt0ii  12046  ledivp1i  12065  ltdivp1i  12066  neg1rr  12129  neg1lt0  12131  cju  12139  nnssre  12147  nnge1  12171  nngt1ne1  12172  nnle1eq1  12173  nngt0  12174  nnnlt1  12175  nnne0  12177  nnrecre  12185  nnrecgt0  12186  nnsub  12187  2re  12217  3re  12223  4re  12227  5re  12230  6re  12233  7re  12236  8re  12239  9re  12242  0le2  12245  2pos  12246  3pos  12248  4pos  12250  5pos  12252  6pos  12253  7pos  12254  8pos  12255  9pos  12256  1lt2  12309  1lt3  12311  1lt4  12314  1lt5  12318  1lt6  12323  1lt7  12329  1lt8  12336  1lt9  12344  1ne2  12346  1le2  12347  1le3  12350  halflt1  12356  addltmul  12375  nnunb  12395  elnnnn0c  12444  nn0ge2m1nn  12469  elnnz1  12515  znnnlt1  12516  zltp1le  12539  zleltp1  12540  nn0lt2  12553  recnz  12565  gtndiv  12567  3halfnz  12569  10re  12624  1lt10  12744  eluzp1m1  12775  eluzp1p1  12777  eluz2b2  12832  zbtwnre  12857  rebtwnz  12858  1rp  12907  divlt1lt  12974  divle1le  12975  nnledivrp  13017  qbtwnxr  13113  xmulrid  13192  xmulm1  13194  x2times  13212  xrub  13225  elicc01  13380  1elunit  13384  divelunit  13408  lincmb01cmp  13409  unitssre  13413  0nelfz1  13457  fzpreddisj  13487  fznatpl1  13492  fztpval  13500  fraclt1  13720  fracle1  13721  flbi2  13735  fldiv4p1lem1div2  13753  fldiv4lem1div2  13755  fldiv  13778  modid  13814  1mod  13821  m1modnnsub1  13838  modm1p1mod0  13843  seqf1olem1  13962  reexpcl  13999  reexpclz  14003  expge0  14019  expge1  14020  expgt1  14021  bernneq  14150  bernneq2  14151  expnbnd  14153  expnlbnd  14154  expnlbnd2  14155  expmulnbnd  14156  discr1  14160  facwordi  14210  faclbnd3  14213  faclbnd4lem1  14214  faclbnd4lem4  14217  faclbnd6  14220  facavg  14222  hashv01gt1  14266  hashnn0n0nn  14312  hashunsnggt  14315  hash1snb  14340  hashgt12el  14343  hashgt12el2  14344  hashfun  14358  hashge2el2dif  14401  tpf1ofv2  14419  lsw0  14486  f1oun2prg  14838  cjexp  15071  re1  15075  im1  15076  rei  15077  imi  15078  01sqrexlem1  15163  01sqrexlem2  15164  01sqrexlem3  15165  01sqrexlem4  15166  01sqrexlem7  15169  resqrex  15171  sqrt1  15192  sqrt2gt1lt2  15195  sqrtm1  15196  abs1  15218  absrdbnd  15263  caubnd2  15279  mulcn2  15517  reccn2  15518  rlimno1  15575  o1fsum  15734  expcnv  15785  geolim  15791  geolim2  15792  georeclim  15793  geomulcvg  15797  geoisumr  15799  geoisum1c  15801  fprodge0  15914  fprodge1  15916  rerisefaccl  15938  refallfaccl  15939  ere  16010  ege2le3  16011  efgt1  16039  resin4p  16061  recos4p  16062  tanhbnd  16084  sinbnd  16103  cosbnd  16104  sinbnd2  16105  cosbnd2  16106  ef01bndlem  16107  sin01bnd  16108  cos01bnd  16109  cos1bnd  16110  cos2bnd  16111  sinltx  16112  sin01gt0  16113  cos01gt0  16114  sin02gt0  16115  sincos1sgn  16116  ene1  16133  rpnnen2lem2  16138  rpnnen2lem3  16139  rpnnen2lem4  16140  rpnnen2lem9  16145  rpnnen2lem12  16148  ruclem6  16158  ruclem11  16163  ruclem12  16164  3dvds  16256  flodddiv4  16340  sadcadd  16383  isprm3  16608  sqnprm  16627  coprm  16636  phibndlem  16695  pythagtriplem3  16744  pcmpt  16818  fldivp1  16823  pockthi  16833  infpn2  16839  basendxnmulrndx  17214  starvndxnbasendx  17222  scandxnbasendx  17234  vscandxnbasendx  17239  ipndxnbasendx  17250  basendxnocndx  17301  slotsbhcdif  17333  lt6abl  19822  srgbinomlem4  20162  0ringnnzr  20456  abvneg  20757  abvtrivd  20763  xrsmcmn  21344  xrsnsgrp  21360  gzrngunitlem  21385  gzrngunit  21386  rge0srg  21391  psgnodpmr  21543  remulg  21560  resubdrg  21561  psdmvr  22110  dscmet  24514  dscopn  24515  nrginvrcnlem  24633  idnghm  24685  tgioo  24738  blcvx  24740  iicmp  24833  iiconn  24834  iirev  24877  iihalf1  24879  iihalf2  24882  iihalf2cnOLD  24884  elii1  24885  elii2  24886  iimulcl  24887  icopnfcnv  24894  icopnfhmeo  24895  iccpnfhmeo  24897  xrhmeo  24898  xrhmph  24899  evth  24912  xlebnum  24918  htpycc  24933  reparphti  24950  reparphtiOLD  24951  pcoval1  24967  pco1  24969  pcoval2  24970  pcocn  24971  pcohtpylem  24973  pcopt  24976  pcopt2  24977  pcoass  24978  pcorevlem  24980  nmhmcn  25074  ncvs1  25111  ovolunlem1a  25451  vitalilem2  25564  vitalilem4  25566  vitalilem5  25567  vitali  25568  i1f1  25645  itg11  25646  itg2const  25695  dveflem  25937  dvlipcn  25953  dvcvx  25979  ply1remlem  26124  fta1blem  26130  vieta1lem2  26273  aalioulem3  26296  aalioulem5  26298  aaliou3lem2  26305  ulmbdd  26361  iblulm  26370  radcnvlem1  26376  dvradcnv  26384  abelthlem2  26396  abelthlem3  26397  abelthlem5  26399  abelthlem7  26402  abelth  26405  abelth2  26406  reeff1olem  26410  reeff1o  26411  sinhalfpilem  26426  tangtx  26468  sincos4thpi  26476  pige3ALT  26483  coskpi  26486  cos0pilt1  26495  recosf1o  26498  tanregt0  26502  efif1olem3  26507  efif1olem4  26508  loge  26549  logdivlti  26583  logcnlem4  26608  logf1o2  26613  logtayl  26623  logccv  26626  recxpcl  26638  cxplea  26659  cxpcn3lem  26711  cxpaddlelem  26715  loglesqrt  26725  ang180lem2  26774  angpined  26794  acosrecl  26867  atancj  26874  atanlogaddlem  26877  atantan  26887  atans2  26895  ressatans  26898  leibpi  26906  log2le1  26914  birthdaylem3  26917  cxp2lim  26941  cxploglim  26942  cxploglim2  26943  divsqrtsumlem  26944  cvxcl  26949  scvxcvx  26950  jensenlem2  26952  amgmlem  26954  emcllem2  26961  emcllem4  26963  emcllem6  26965  emcllem7  26966  emre  26970  emgt0  26971  harmonicbnd3  26972  harmonicubnd  26974  harmonicbnd4  26975  zetacvg  26979  ftalem1  27037  ftalem2  27038  ftalem5  27041  issqf  27100  cht1  27129  chp1  27131  ppiltx  27141  mumullem2  27144  ppiublem1  27167  ppiub  27169  chtublem  27176  chtub  27177  logfacbnd3  27188  logexprlim  27190  perfectlem2  27195  dchrinv  27226  dchr1re  27228  efexple  27246  bposlem1  27249  bposlem2  27250  bposlem5  27253  bposlem8  27256  lgsdir2lem1  27290  lgsdir2lem5  27294  lgsdir  27297  lgsne0  27300  lgsabs1  27301  lgsdinn0  27310  gausslemma2dlem0i  27329  lgseisen  27344  m1lgs  27353  2lgslem3  27369  addsq2nreurex  27409  2sqreultblem  27413  2sqreunnltblem  27416  chebbnd1lem3  27436  chebbnd1  27437  chtppilimlem1  27438  chtppilimlem2  27439  chtppilim  27440  chpchtlim  27444  vmadivsumb  27448  rplogsumlem2  27450  rpvmasumlem  27452  dchrmusumlema  27458  dchrmusum2  27459  dchrvmasumlem2  27463  dchrvmasumiflem1  27466  dchrisum0flblem1  27473  dchrisum0flblem2  27474  dchrisum0fno1  27476  rpvmasum2  27477  dchrisum0re  27478  dchrisum0lema  27479  dchrisum0lem1b  27480  dchrisum0lem1  27481  dchrisum0lem2a  27482  dchrisum0lem2  27483  logdivsum  27498  mulog2sumlem2  27500  2vmadivsumlem  27505  log2sumbnd  27509  selbergb  27514  selberg2b  27517  chpdifbndlem1  27518  selberg3lem1  27522  selberg3lem2  27523  selberg4lem1  27525  pntrmax  27529  pntrsumo1  27530  selbergsb  27540  pntrlog2bndlem3  27544  pntrlog2bndlem5  27546  pntpbnd1a  27550  pntpbnd2  27552  pntibndlem1  27554  pntibndlem3  27557  pntlemd  27559  pntlemc  27560  pntlemb  27562  pntlemr  27567  pntlemf  27570  pntlemk  27571  pntlemo  27572  pntlem3  27574  pntleml  27576  abvcxp  27580  ostth2lem1  27583  ostth1  27598  ostth2lem2  27599  ostth2lem3  27600  ostth2lem4  27601  ostth2  27602  ostth3  27603  ostth  27604  slotsinbpsd  28462  slotslnbpsd  28463  trgcgrg  28536  brbtwn2  28927  colinearalglem4  28931  ax5seglem2  28951  ax5seglem3  28953  axpaschlem  28962  axpasch  28963  axlowdimlem6  28969  axlowdimlem10  28973  axlowdimlem16  28979  axlowdim1  28981  axlowdim2  28982  axlowdim  28983  axcontlem2  28987  elntg2  29007  lfgrnloop  29147  lfuhgr1v0e  29276  usgrexmpldifpr  29280  usgrexmplef  29281  1loopgrvd2  29526  vdegp1bi  29560  lfgrwlkprop  29708  pthdlem1  29788  pthdlem2  29790  clwlkclwwlkf  30032  upgr4cycl4dv4e  30209  konigsberglem2  30277  konigsberglem3  30278  konigsberglem5  30280  frgrreg  30418  ex-dif  30447  ex-in  30449  ex-pss  30452  ex-res  30465  ex-fl  30471  nv1  30699  smcnlem  30721  ipidsq  30734  nmlno0lem  30817  norm-ii-i  31161  bcs2  31206  norm1  31273  nmopub2tALT  31933  nmfnleub2  31950  nmlnop0iALT  32019  unopbd  32039  nmopadjlem  32113  nmopcoadji  32125  pjnmopi  32172  pjbdlni  32173  hstle1  32250  hstle  32254  hstles  32255  stge1i  32262  stlesi  32265  staddi  32270  stadd3i  32272  strlem1  32274  strlem5  32279  jplem1  32292  cdj1i  32457  addltmulALT  32470  xlt2addrd  32788  pr01ssre  32854  sgnclre  32862  sgnnbi  32868  sgnpbi  32869  sgnmulsgp  32873  indf  32883  indfval  32884  dp2lt10  32914  dp2ltsuc  32916  dp2ltc  32917  dplti  32935  dpmul4  32944  cshw1s2  32991  xrsmulgzz  33040  rearchi  33376  xrge0slmod  33378  prmidl0  33480  evl1deg3  33608  constrconj  33851  2sqr3minply  33886  submateqlem1  33913  xrge0iifcnv  34039  xrge0iifcv  34040  xrge0iifiso  34041  xrge0iifhom  34043  zrhre  34125  esumcst  34169  cntnevol  34334  omssubadd  34406  iwrdsplit  34493  dstfrvclim1  34584  coinfliprv  34589  ballotlem2  34595  ballotlem4  34605  ballotlemi1  34609  ballotlemic  34613  plymulx0  34653  plymulx  34654  signswch  34667  signstf  34672  signsvfn  34688  itgexpif  34712  hgt750lemd  34754  logdivsqrle  34756  hgt750lem  34757  hgt750lem2  34758  hgt750leme  34764  tgoldbachgnn  34765  subfacp1lem1  35322  subfacp1lem5  35327  resconn  35389  iisconn  35395  iillysconn  35396  problem2  35809  problem3  35810  sinccvglem  35815  fz0n  35874  dnibndlem12  36632  knoppcnlem4  36639  knoppndvlem13  36667  cnndvlem1  36680  irrdiff  37470  relowlpssretop  37508  sin2h  37750  cos2h  37751  tan2h  37752  poimirlem7  37767  poimirlem16  37776  poimirlem17  37777  poimirlem19  37779  poimirlem20  37780  poimirlem22  37782  poimirlem23  37783  poimirlem29  37789  poimirlem31  37791  itg2addnclem3  37813  asindmre  37843  dvasin  37844  dvacos  37845  dvreasin  37846  dvreacos  37847  fdc  37885  geomcau  37899  cntotbnd  37936  heiborlem8  37958  bfplem2  37963  bfp  37964  aks4d1p1p7  42267  1t1e1ALT  42452  ine1  42511  re1m1e0m0  42594  sn-00idlem1  42595  sn-00idlem2  42596  remul02  42602  sn-0ne2  42603  reixi  42620  rei4  42621  remullid  42631  ipiiie0  42635  sn-0tie0  42648  sn-nnne0  42657  mulgt0b1d  42669  sn-0lt1  42672  sn-ltp1  42673  reneg1lt0  42677  sn-inelr  42684  rabren3dioph  42999  pellexlem5  43017  pellexlem6  43018  pell1qrgaplem  43057  pell14qrgap  43059  pellqrex  43063  pellfundre  43065  pellfundlb  43068  pellfund14gap  43071  jm2.17a  43144  acongeq  43167  jm2.23  43180  jm3.1lem2  43202  sqrtcval  43824  sqrtcval2  43825  resqrtval  43826  imsqrtval  43827  relexp01min  43896  cvgdvgrat  44496  lhe4.4ex1a  44512  binomcxplemnotnn0  44539  isosctrlem1ALT  45116  supxrgelem  45524  xrlexaddrp  45539  infxr  45553  infleinflem2  45557  sumnnodd  45818  limsup10exlem  45958  limsup10ex  45959  dvnprodlem3  46134  stoweidlem1  46187  stoweidlem18  46204  stoweidlem19  46205  stoweidlem26  46212  stoweidlem34  46220  stoweidlem40  46226  stoweidlem41  46227  stoweidlem59  46245  stoweid  46249  stirlinglem10  46269  stirlinglem11  46270  dirkercncflem1  46289  fourierdlem16  46309  fourierdlem21  46314  fourierdlem22  46315  fourierdlem42  46335  fourierdlem68  46360  fourierdlem83  46375  fourierdlem103  46395  sqwvfourb  46415  fouriersw  46417  etransclem23  46443  salgencntex  46529  ovn0lem  46751  smfmullem3  46979  smfmullem4  46980  nthrucw  47072  cjnpoly  47077  zm1nn  47490  ceilhalf1  47522  m1mod0mod1  47542  fmtnosqrt  47727  perfectALTVlem2  47910  2exp340mod341  47921  8exp8mod9  47924  nfermltl8rev  47930  nnsum3primesprm  47978  nnsum4primesodd  47984  nnsum4primesoddALTV  47985  nnsum4primeseven  47988  nnsum4primesevenALTV  47989  tgblthelfgott  48003  tgoldbach  48005  usgrexmpl1lem  48209  usgrexmpl2lem  48214  usgrexmpl2nb1  48220  usgrexmpl2nb3  48222  usgrexmpl2nb4  48223  usgrexmpl2nb5  48224  usgrexmpl2trifr  48225  gpg3kgrtriexlem3  48273  pgnbgreunbgrlem2lem1  48302  pgnbgreunbgrlem2lem2  48303  rege1logbrege0  48746  rege1logbzge0  48747  blennnelnn  48764  dignnld  48791  nn0sumshdiglemA  48807  nn0sumshdiglem1  48809  rrx2xpref1o  48906  rrxlines  48921  eenglngeehlnmlem1  48925  eenglngeehlnmlem2  48926  line2ylem  48939  line2x  48942  icccldii  49106  io1ii  49108  sepfsepc  49115