Theorem 1re 11144

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 11096, 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 11107	. . 3 ⊢ 1 ≠ 0
2		ax-1cn 11096	. . . . 5 ⊢ 1 ∈ ℂ
3		cnre 11141	. . . . 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 11136	. . . . . . . 8 ⊢ 0 ∈ ℂ
8		cnre 11141	. . . . . . . 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 3152	. . . . . . . 8 ⊢ ((𝑎 + (i · 𝑏)) ≠ 0 → (∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)) → ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
13	12	reximdv 3152	. . . . . . 7 ⊢ ((𝑎 + (i · 𝑏)) ≠ 0 → (∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)) → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
14	6, 9, 13	syl6mpi 67	. . . . . 6 ⊢ (1 ≠ 0 → (1 = (𝑎 + (i · 𝑏)) → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
15	14	reximdv 3152	. . . . 5 ⊢ (1 ≠ 0 → (∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)) → ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
16	15	reximdv 3152	. . . 4 ⊢ (1 ≠ 0 → (∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)) → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
17	4, 16	mpi 20	. . 3 ⊢ (1 ≠ 0 → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)))
18		id 22	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑐 → 𝑎 = 𝑐)
19		oveq2 7375	. . . . . . . . . . . 12 ⊢ (𝑏 = 𝑑 → (i · 𝑏) = (i · 𝑑))
20	18, 19	oveqan12d 7386	. . . . . . . . . . 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 864	. . . . . 6 ⊢ ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → (𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑))
26		neeq1 2994	. . . . . . . . . 10 ⊢ (𝑥 = 𝑎 → (𝑥 ≠ 𝑦 ↔ 𝑎 ≠ 𝑦))
27		neeq2 2995	. . . . . . . . . 10 ⊢ (𝑦 = 𝑐 → (𝑎 ≠ 𝑦 ↔ 𝑎 ≠ 𝑐))
28	26, 27	rspc2ev 3577	. . . . . . . . 9 ⊢ ((𝑎 ∈ ℝ ∧ 𝑐 ∈ ℝ ∧ 𝑎 ≠ 𝑐) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦)
29	28	3expia 1122	. . . . . . . 8 ⊢ ((𝑎 ∈ ℝ ∧ 𝑐 ∈ ℝ) → (𝑎 ≠ 𝑐 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
30	29	ad2ant2r 748	. . . . . . 7 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → (𝑎 ≠ 𝑐 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
31		neeq1 2994	. . . . . . . . . 10 ⊢ (𝑥 = 𝑏 → (𝑥 ≠ 𝑦 ↔ 𝑏 ≠ 𝑦))
32		neeq2 2995	. . . . . . . . . 10 ⊢ (𝑦 = 𝑑 → (𝑏 ≠ 𝑦 ↔ 𝑏 ≠ 𝑑))
33	31, 32	rspc2ev 3577	. . . . . . . . 9 ⊢ ((𝑏 ∈ ℝ ∧ 𝑑 ∈ ℝ ∧ 𝑏 ≠ 𝑑) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦)
34	33	3expia 1122	. . . . . . . 8 ⊢ ((𝑏 ∈ ℝ ∧ 𝑑 ∈ ℝ) → (𝑏 ≠ 𝑑 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
35	34	ad2ant2l 747	. . . . . . 7 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → (𝑏 ≠ 𝑑 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
36	30, 35	jaod 860	. . . . . 6 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → ((𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
37	25, 36	syl5 34	. . . . 5 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
38	37	rexlimdvva 3194	. . . 4 ⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
39	38	rexlimivv 3179	. . 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 3564	. . . . . . . 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 3564	. . . . . . 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 3179	. 2 ⊢ (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)
57		ax-rrecex 11110	. . . 4 ⊢ ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → ∃𝑥 ∈ ℝ (𝑧 · 𝑥) = 1)
58		remulcl 11123	. . . . . . 7 ⊢ ((𝑧 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (𝑧 · 𝑥) ∈ ℝ)
59	58	adantlr 716	. . . . . 6 ⊢ (((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) ∧ 𝑥 ∈ ℝ) → (𝑧 · 𝑥) ∈ ℝ)
60		eleq1 2824	. . . . . 6 ⊢ ((𝑧 · 𝑥) = 1 → ((𝑧 · 𝑥) ∈ ℝ ↔ 1 ∈ ℝ))
61	59, 60	syl5ibcom 245	. . . . 5 ⊢ (((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) ∧ 𝑥 ∈ ℝ) → ((𝑧 · 𝑥) = 1 → 1 ∈ ℝ))
62	61	rexlimdva 3138	. . . 4 ⊢ ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → (∃𝑥 ∈ ℝ (𝑧 · 𝑥) = 1 → 1 ∈ ℝ))
63	57, 62	mpd 15	. . 3 ⊢ ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → 1 ∈ ℝ)
64	63	rexlimiva 3130	. 2 ⊢ (∃𝑧 ∈ ℝ 𝑧 ≠ 0 → 1 ∈ ℝ)
65	40, 56, 64	mp2b 10	1 ⊢ 1 ∈ ℝ

Syntax hints:   → wi 4   ∧ wa 395   ∨ wo 848   = wceq 1542   ∈ wcel 2114   ≠ wne 2932  ∃wrex 3061  (class class class)co 7367  ℂcc 11036  ℝcr 11037  0cc0 11038  1c1 11039  ici 11040   + caddc 11041   · cmul 11043

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-mulcl 11100  ax-mulrcl 11101  ax-i2m1 11106  ax-1ne0 11107  ax-rrecex 11110  ax-cnre 11111

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-iota 6454  df-fv 6506  df-ov 7370

This theorem is referenced by:  1red  11145  pr01ssre  11148  1xr  11204  dedekind  11309  peano2re  11319  mul02lem2  11323  addrid  11326  renegcl  11457  peano2rem  11461  0reALT  11491  0lt1  11672  0le1  11673  relin01  11674  1le1  11778  eqneg  11875  ltp1  11995  ltm1  11997  recgt0  12001  mulgt1OLD  12014  ltmulgt11  12015  lemulge11  12018  reclt1  12051  recgt1  12052  recgt1i  12053  recp1lt1  12054  recreclt  12055  recgt0ii  12062  ledivp1i  12081  ltdivp1i  12082  neg1rr  12145  neg1lt0  12147  cju  12155  indf  12165  indfval  12166  nnssre  12178  nnge1  12205  nngt1ne1  12206  nnle1eq1  12207  nngt0  12208  nnnlt1  12209  nnne0  12211  nnrecre  12219  nnrecgt0  12220  nnsub  12221  1t1e1ALT  12232  2re  12255  3re  12261  4re  12265  5re  12268  6re  12271  7re  12274  8re  12277  9re  12280  0le2  12283  2pos  12284  3pos  12286  4pos  12288  5pos  12290  6pos  12291  7pos  12292  8pos  12293  9pos  12294  1lt2  12347  1lt3  12349  1lt4  12352  1lt5  12356  1lt6  12361  1lt7  12367  1lt8  12374  1lt9  12382  1ne2  12384  1le2  12385  1le3  12388  halflt1  12394  addltmul  12413  nnunb  12433  elnnnn0c  12482  nn0ge2m1nn  12507  elnnz1  12553  znnnlt1  12554  zltp1le  12577  zleltp1  12578  nn0lt2  12592  recnz  12604  gtndiv  12606  3halfnz  12608  10re  12663  1lt10  12783  eluzp1m1  12814  eluzp1p1  12816  eluz2b2  12871  zbtwnre  12896  rebtwnz  12897  1rp  12946  divlt1lt  13013  divle1le  13014  nnledivrp  13056  qbtwnxr  13152  xmulrid  13231  xmulm1  13233  x2times  13251  xrub  13264  elicc01  13419  1elunit  13423  divelunit  13447  lincmb01cmp  13448  unitssre  13452  0nelfz1  13497  fzpreddisj  13527  fznatpl1  13532  fztpval  13540  fraclt1  13761  fracle1  13762  flbi2  13776  fldiv4p1lem1div2  13794  fldiv4lem1div2  13796  fldiv  13819  modid  13855  1mod  13862  m1modnnsub1  13879  modm1p1mod0  13884  seqf1olem1  14003  reexpcl  14040  reexpclz  14044  expge0  14060  expge1  14061  expgt1  14062  bernneq  14191  bernneq2  14192  expnbnd  14194  expnlbnd  14195  expnlbnd2  14196  expmulnbnd  14197  discr1  14201  facwordi  14251  faclbnd3  14254  faclbnd4lem1  14255  faclbnd4lem4  14258  faclbnd6  14261  facavg  14263  hashv01gt1  14307  hashnn0n0nn  14353  hashunsnggt  14356  hash1snb  14381  hashgt12el  14384  hashgt12el2  14385  hashfun  14399  hashge2el2dif  14442  tpf1ofv2  14460  lsw0  14527  f1oun2prg  14879  cjexp  15112  re1  15116  im1  15117  rei  15118  imi  15119  01sqrexlem1  15204  01sqrexlem2  15205  01sqrexlem3  15206  01sqrexlem4  15207  01sqrexlem7  15210  resqrex  15212  sqrt1  15233  sqrt2gt1lt2  15236  sqrtm1  15237  abs1  15259  absrdbnd  15304  caubnd2  15320  mulcn2  15558  reccn2  15559  rlimno1  15616  o1fsum  15776  expcnv  15829  geolim  15835  geolim2  15836  georeclim  15837  geomulcvg  15841  geoisumr  15843  geoisum1c  15845  fprodge0  15958  fprodge1  15960  rerisefaccl  15982  refallfaccl  15983  ere  16054  ege2le3  16055  efgt1  16083  resin4p  16105  recos4p  16106  tanhbnd  16128  sinbnd  16147  cosbnd  16148  sinbnd2  16149  cosbnd2  16150  ef01bndlem  16151  sin01bnd  16152  cos01bnd  16153  cos1bnd  16154  cos2bnd  16155  sinltx  16156  sin01gt0  16157  cos01gt0  16158  sin02gt0  16159  sincos1sgn  16160  ene1  16177  rpnnen2lem2  16182  rpnnen2lem3  16183  rpnnen2lem4  16184  rpnnen2lem9  16189  rpnnen2lem12  16192  ruclem6  16202  ruclem11  16207  ruclem12  16208  3dvds  16300  flodddiv4  16384  sadcadd  16427  isprm3  16652  sqnprm  16672  coprm  16681  phibndlem  16740  pythagtriplem3  16789  pcmpt  16863  fldivp1  16868  pockthi  16878  infpn2  16884  basendxnmulrndx  17259  starvndxnbasendx  17267  scandxnbasendx  17279  vscandxnbasendx  17284  ipndxnbasendx  17295  basendxnocndx  17346  slotsbhcdif  17378  lt6abl  19870  srgbinomlem4  20210  0ringnnzr  20502  abvneg  20803  abvtrivd  20809  xrsmcmn  21375  xrsnsgrp  21388  gzrngunitlem  21412  gzrngunit  21413  rge0srg  21418  psgnodpmr  21570  remulg  21587  resubdrg  21588  psdmvr  22135  dscmet  24537  dscopn  24538  nrginvrcnlem  24656  idnghm  24708  tgioo  24761  blcvx  24763  iicmp  24853  iiconn  24854  iirev  24896  iihalf1  24898  iihalf2  24900  elii1  24902  elii2  24903  iimulcl  24904  icopnfcnv  24909  icopnfhmeo  24910  iccpnfhmeo  24912  xrhmeo  24913  xrhmph  24914  evth  24926  xlebnum  24932  htpycc  24947  reparphti  24964  pcoval1  24980  pco1  24982  pcoval2  24983  pcocn  24984  pcohtpylem  24986  pcopt  24989  pcopt2  24990  pcoass  24991  pcorevlem  24993  nmhmcn  25087  ncvs1  25124  ovolunlem1a  25463  vitalilem2  25576  vitalilem4  25578  vitalilem5  25579  vitali  25580  i1f1  25657  itg11  25658  itg2const  25707  dveflem  25946  dvlipcn  25961  dvcvx  25987  ply1remlem  26130  fta1blem  26136  vieta1lem2  26277  aalioulem3  26300  aalioulem5  26302  aaliou3lem2  26309  ulmbdd  26363  iblulm  26372  radcnvlem1  26378  dvradcnv  26386  abelthlem2  26397  abelthlem3  26398  abelthlem5  26400  abelthlem7  26403  abelth  26406  abelth2  26407  reeff1olem  26411  reeff1o  26412  sinhalfpilem  26427  tangtx  26469  sincos4thpi  26477  pige3ALT  26484  coskpi  26487  cos0pilt1  26496  recosf1o  26499  tanregt0  26503  efif1olem3  26508  efif1olem4  26509  loge  26550  logdivlti  26584  logcnlem4  26609  logf1o2  26614  logtayl  26624  logccv  26627  recxpcl  26639  cxplea  26660  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  26940  cxploglim  26941  cxploglim2  26942  divsqrtsumlem  26943  cvxcl  26948  scvxcvx  26949  jensenlem2  26951  amgmlem  26953  emcllem2  26960  emcllem4  26962  emcllem6  26964  emcllem7  26965  emre  26969  emgt0  26970  harmonicbnd3  26971  harmonicubnd  26973  harmonicbnd4  26974  zetacvg  26978  ftalem1  27036  ftalem2  27037  ftalem5  27040  issqf  27099  cht1  27128  chp1  27130  ppiltx  27140  mumullem2  27143  ppiublem1  27165  ppiub  27167  chtublem  27174  chtub  27175  logfacbnd3  27186  logexprlim  27188  perfectlem2  27193  dchrinv  27224  dchr1re  27226  efexple  27244  bposlem1  27247  bposlem2  27248  bposlem5  27251  bposlem8  27254  lgsdir2lem1  27288  lgsdir2lem5  27292  lgsdir  27295  lgsne0  27298  lgsabs1  27299  lgsdinn0  27308  gausslemma2dlem0i  27327  lgseisen  27342  m1lgs  27351  2lgslem3  27367  addsq2nreurex  27407  2sqreultblem  27411  2sqreunnltblem  27414  chebbnd1lem3  27434  chebbnd1  27435  chtppilimlem1  27436  chtppilimlem2  27437  chtppilim  27438  chpchtlim  27442  vmadivsumb  27446  rplogsumlem2  27448  rpvmasumlem  27450  dchrmusumlema  27456  dchrmusum2  27457  dchrvmasumlem2  27461  dchrvmasumiflem1  27464  dchrisum0flblem1  27471  dchrisum0flblem2  27472  dchrisum0fno1  27474  rpvmasum2  27475  dchrisum0re  27476  dchrisum0lema  27477  dchrisum0lem1b  27478  dchrisum0lem1  27479  dchrisum0lem2a  27480  dchrisum0lem2  27481  logdivsum  27496  mulog2sumlem2  27498  2vmadivsumlem  27503  log2sumbnd  27507  selbergb  27512  selberg2b  27515  chpdifbndlem1  27516  selberg3lem1  27520  selberg3lem2  27521  selberg4lem1  27523  pntrmax  27527  pntrsumo1  27528  selbergsb  27538  pntrlog2bndlem3  27542  pntrlog2bndlem5  27544  pntpbnd1a  27548  pntpbnd2  27550  pntibndlem1  27552  pntibndlem3  27555  pntlemd  27557  pntlemc  27558  pntlemb  27560  pntlemr  27565  pntlemf  27568  pntlemk  27569  pntlemo  27570  pntlem3  27572  pntleml  27574  abvcxp  27578  ostth2lem1  27581  ostth1  27596  ostth2lem2  27597  ostth2lem3  27598  ostth2lem4  27599  ostth2  27600  ostth3  27601  ostth  27602  slotsinbpsd  28509  slotslnbpsd  28510  trgcgrg  28583  brbtwn2  28974  colinearalglem4  28978  ax5seglem2  28998  ax5seglem3  29000  axpaschlem  29009  axpasch  29010  axlowdimlem6  29016  axlowdimlem10  29020  axlowdimlem16  29026  axlowdim1  29028  axlowdim2  29029  axlowdim  29030  axcontlem2  29034  elntg2  29054  lfgrnloop  29194  lfuhgr1v0e  29323  usgrexmpldifpr  29327  usgrexmplef  29328  1loopgrvd2  29572  vdegp1bi  29606  lfgrwlkprop  29754  pthdlem1  29834  pthdlem2  29836  clwlkclwwlkf  30078  upgr4cycl4dv4e  30255  konigsberglem2  30323  konigsberglem3  30324  konigsberglem5  30326  frgrreg  30464  ex-dif  30493  ex-in  30495  ex-pss  30498  ex-res  30511  ex-fl  30517  nv1  30746  smcnlem  30768  ipidsq  30781  nmlno0lem  30864  norm-ii-i  31208  bcs2  31253  norm1  31320  nmopub2tALT  31980  nmfnleub2  31997  nmlnop0iALT  32066  unopbd  32086  nmopadjlem  32160  nmopcoadji  32172  pjnmopi  32219  pjbdlni  32220  hstle1  32297  hstle  32301  hstles  32302  stge1i  32309  stlesi  32312  staddi  32317  stadd3i  32319  strlem1  32321  strlem5  32326  jplem1  32339  cdj1i  32504  addltmulALT  32517  xlt2addrd  32832  sgnclre  32905  sgnnbi  32911  sgnpbi  32912  sgnmulsgp  32916  dp2lt10  32943  dp2ltsuc  32945  dp2ltc  32946  dplti  32964  dpmul4  32973  cshw1s2  33020  xrsmulgzz  33069  rearchi  33406  xrge0slmod  33408  prmidl0  33510  evl1deg3  33638  constrconj  33889  2sqr3minply  33924  submateqlem1  33951  xrge0iifcnv  34077  xrge0iifcv  34078  xrge0iifiso  34079  xrge0iifhom  34081  zrhre  34163  esumcst  34207  cntnevol  34372  omssubadd  34444  iwrdsplit  34531  dstfrvclim1  34622  coinfliprv  34627  ballotlem2  34633  ballotlem4  34643  ballotlemi1  34647  ballotlemic  34651  plymulx0  34691  plymulx  34692  signswch  34705  signstf  34710  signsvfn  34726  itgexpif  34750  hgt750lemd  34792  logdivsqrle  34794  hgt750lem  34795  hgt750lem2  34796  hgt750leme  34802  tgoldbachgnn  34803  subfacp1lem1  35361  subfacp1lem5  35366  resconn  35428  iisconn  35434  iillysconn  35435  problem2  35848  problem3  35849  sinccvglem  35854  fz0n  35913  dnibndlem12  36749  knoppcnlem4  36756  knoppndvlem13  36784  cnndvlem1  36797  irrdiff  37640  relowlpssretop  37680  sin2h  37931  cos2h  37932  tan2h  37933  poimirlem7  37948  poimirlem16  37957  poimirlem17  37958  poimirlem19  37960  poimirlem20  37961  poimirlem22  37963  poimirlem23  37964  poimirlem29  37970  poimirlem31  37972  itg2addnclem3  37994  asindmre  38024  dvasin  38025  dvacos  38026  dvreasin  38027  dvreacos  38028  fdc  38066  geomcau  38080  cntotbnd  38117  heiborlem8  38139  bfplem2  38144  bfp  38145  aks4d1p1p7  42513  ine1  42746  re1m1e0m0  42829  sn-00idlem1  42830  sn-00idlem2  42831  remul02  42837  sn-0ne2  42838  reixi  42855  rei4  42856  remullid  42866  ipiiie0  42870  sn-0tie0  42896  sn-nnne0  42905  mulgt0b1d  42917  sn-0lt1  42920  sn-ltp1  42921  reneg1lt0  42925  sn-inelr  42932  rabren3dioph  43243  pellexlem5  43261  pellexlem6  43262  pell1qrgaplem  43301  pell14qrgap  43303  pellqrex  43307  pellfundre  43309  pellfundlb  43312  pellfund14gap  43315  jm2.17a  43388  acongeq  43411  jm2.23  43424  jm3.1lem2  43446  sqrtcval  44068  sqrtcval2  44069  resqrtval  44070  imsqrtval  44071  relexp01min  44140  cvgdvgrat  44740  lhe4.4ex1a  44756  binomcxplemnotnn0  44783  isosctrlem1ALT  45360  supxrgelem  45767  xrlexaddrp  45782  infxr  45796  infleinflem2  45800  sumnnodd  46060  limsup10exlem  46200  limsup10ex  46201  dvnprodlem3  46376  stoweidlem1  46429  stoweidlem18  46446  stoweidlem19  46447  stoweidlem26  46454  stoweidlem34  46462  stoweidlem40  46468  stoweidlem41  46469  stoweidlem59  46487  stoweid  46491  stirlinglem10  46511  stirlinglem11  46512  dirkercncflem1  46531  fourierdlem16  46551  fourierdlem21  46556  fourierdlem22  46557  fourierdlem42  46577  fourierdlem68  46602  fourierdlem83  46617  fourierdlem103  46637  sqwvfourb  46657  fouriersw  46659  etransclem23  46685  salgencntex  46771  ovn0lem  46993  smfmullem3  47221  smfmullem4  47222  nthrucw  47316  cjnpoly  47337  zm1nn  47750  ceilhalf1  47786  m1mod0mod1  47808  muldvdsfacgt  47834  fmtnosqrt  48002  nprmdvdsfacm1lem4  48086  perfectALTVlem2  48198  2exp340mod341  48209  8exp8mod9  48212  nfermltl8rev  48218  nnsum3primesprm  48266  nnsum4primesodd  48272  nnsum4primesoddALTV  48273  nnsum4primeseven  48276  nnsum4primesevenALTV  48277  tgblthelfgott  48291  tgoldbach  48293  usgrexmpl1lem  48497  usgrexmpl2lem  48502  usgrexmpl2nb1  48508  usgrexmpl2nb3  48510  usgrexmpl2nb4  48511  usgrexmpl2nb5  48512  usgrexmpl2trifr  48513  gpg3kgrtriexlem3  48561  pgnbgreunbgrlem2lem1  48590  pgnbgreunbgrlem2lem2  48591  rege1logbrege0  49034  rege1logbzge0  49035  blennnelnn  49052  dignnld  49079  nn0sumshdiglemA  49095  nn0sumshdiglem1  49097  rrx2xpref1o  49194  rrxlines  49209  eenglngeehlnmlem1  49213  eenglngeehlnmlem2  49214  line2ylem  49227  line2x  49230  icccldii  49394  io1ii  49396  sepfsepc  49403