Theorem 1re 11138

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 11090, 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 11101	. . 3 ⊢ 1 ≠ 0
2		ax-1cn 11090	. . . . 5 ⊢ 1 ∈ ℂ
3		cnre 11135	. . . . 5 ⊢ (1 ∈ ℂ → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)))
4	2, 3	ax-mp 5	. . . 4 ⊢ ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏))
5		neeq1 2995	. . . . . . . 8 ⊢ (1 = (𝑎 + (i · 𝑏)) → (1 ≠ 0 ↔ (𝑎 + (i · 𝑏)) ≠ 0))
6	5	biimpcd 249	. . . . . . 7 ⊢ (1 ≠ 0 → (1 = (𝑎 + (i · 𝑏)) → (𝑎 + (i · 𝑏)) ≠ 0))
7		0cn 11130	. . . . . . . 8 ⊢ 0 ∈ ℂ
8		cnre 11135	. . . . . . . 8 ⊢ (0 ∈ ℂ → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)))
9	7, 8	ax-mp 5	. . . . . . 7 ⊢ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑))
10		neeq2 2996	. . . . . . . . . 10 ⊢ (0 = (𝑐 + (i · 𝑑)) → ((𝑎 + (i · 𝑏)) ≠ 0 ↔ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
11	10	biimpcd 249	. . . . . . . . 9 ⊢ ((𝑎 + (i · 𝑏)) ≠ 0 → (0 = (𝑐 + (i · 𝑑)) → (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
12	11	reximdv 3153	. . . . . . . 8 ⊢ ((𝑎 + (i · 𝑏)) ≠ 0 → (∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)) → ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
13	12	reximdv 3153	. . . . . . 7 ⊢ ((𝑎 + (i · 𝑏)) ≠ 0 → (∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)) → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
14	6, 9, 13	syl6mpi 67	. . . . . 6 ⊢ (1 ≠ 0 → (1 = (𝑎 + (i · 𝑏)) → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
15	14	reximdv 3153	. . . . 5 ⊢ (1 ≠ 0 → (∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)) → ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
16	15	reximdv 3153	. . . 4 ⊢ (1 ≠ 0 → (∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)) → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
17	4, 16	mpi 20	. . 3 ⊢ (1 ≠ 0 → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)))
18		id 22	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑐 → 𝑎 = 𝑐)
19		oveq2 7369	. . . . . . . . . . . 12 ⊢ (𝑏 = 𝑑 → (i · 𝑏) = (i · 𝑑))
20	18, 19	oveqan12d 7380	. . . . . . . . . . 11 ⊢ ((𝑎 = 𝑐 ∧ 𝑏 = 𝑑) → (𝑎 + (i · 𝑏)) = (𝑐 + (i · 𝑑)))
21	20	expcom 413	. . . . . . . . . 10 ⊢ (𝑏 = 𝑑 → (𝑎 = 𝑐 → (𝑎 + (i · 𝑏)) = (𝑐 + (i · 𝑑))))
22	21	necon3d 2954	. . . . . . . . 9 ⊢ (𝑏 = 𝑑 → ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → 𝑎 ≠ 𝑐))
23	22	com12 32	. . . . . . . 8 ⊢ ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → (𝑏 = 𝑑 → 𝑎 ≠ 𝑐))
24	23	necon3bd 2947	. . . . . . 7 ⊢ ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → (¬ 𝑎 ≠ 𝑐 → 𝑏 ≠ 𝑑))
25	24	orrd 864	. . . . . 6 ⊢ ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → (𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑))
26		neeq1 2995	. . . . . . . . . 10 ⊢ (𝑥 = 𝑎 → (𝑥 ≠ 𝑦 ↔ 𝑎 ≠ 𝑦))
27		neeq2 2996	. . . . . . . . . 10 ⊢ (𝑦 = 𝑐 → (𝑎 ≠ 𝑦 ↔ 𝑎 ≠ 𝑐))
28	26, 27	rspc2ev 3578	. . . . . . . . 9 ⊢ ((𝑎 ∈ ℝ ∧ 𝑐 ∈ ℝ ∧ 𝑎 ≠ 𝑐) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦)
29	28	3expia 1122	. . . . . . . 8 ⊢ ((𝑎 ∈ ℝ ∧ 𝑐 ∈ ℝ) → (𝑎 ≠ 𝑐 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
30	29	ad2ant2r 748	. . . . . . 7 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → (𝑎 ≠ 𝑐 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
31		neeq1 2995	. . . . . . . . . 10 ⊢ (𝑥 = 𝑏 → (𝑥 ≠ 𝑦 ↔ 𝑏 ≠ 𝑦))
32		neeq2 2996	. . . . . . . . . 10 ⊢ (𝑦 = 𝑑 → (𝑏 ≠ 𝑦 ↔ 𝑏 ≠ 𝑑))
33	31, 32	rspc2ev 3578	. . . . . . . . 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 3195	. . . 4 ⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
39	38	rexlimivv 3180	. . 3 ⊢ (∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦)
40	1, 17, 39	mp2b 10	. 2 ⊢ ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦
41		eqtr3 2759	. . . . . . . . 9 ⊢ ((𝑥 = 0 ∧ 𝑦 = 0) → 𝑥 = 𝑦)
42	41	ex 412	. . . . . . . 8 ⊢ (𝑥 = 0 → (𝑦 = 0 → 𝑥 = 𝑦))
43	42	necon3d 2954	. . . . . . 7 ⊢ (𝑥 = 0 → (𝑥 ≠ 𝑦 → 𝑦 ≠ 0))
44		neeq1 2995	. . . . . . . . 9 ⊢ (𝑧 = 𝑦 → (𝑧 ≠ 0 ↔ 𝑦 ≠ 0))
45	44	rspcev 3565	. . . . . . . 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 2995	. . . . . . . 8 ⊢ (𝑧 = 𝑥 → (𝑧 ≠ 0 ↔ 𝑥 ≠ 0))
51	50	rspcev 3565	. . . . . . 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 3016	. . 3 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
56	55	rexlimivv 3180	. 2 ⊢ (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)
57		ax-rrecex 11104	. . . 4 ⊢ ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → ∃𝑥 ∈ ℝ (𝑧 · 𝑥) = 1)
58		remulcl 11117	. . . . . . 7 ⊢ ((𝑧 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (𝑧 · 𝑥) ∈ ℝ)
59	58	adantlr 716	. . . . . 6 ⊢ (((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) ∧ 𝑥 ∈ ℝ) → (𝑧 · 𝑥) ∈ ℝ)
60		eleq1 2825	. . . . . 6 ⊢ ((𝑧 · 𝑥) = 1 → ((𝑧 · 𝑥) ∈ ℝ ↔ 1 ∈ ℝ))
61	59, 60	syl5ibcom 245	. . . . 5 ⊢ (((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) ∧ 𝑥 ∈ ℝ) → ((𝑧 · 𝑥) = 1 → 1 ∈ ℝ))
62	61	rexlimdva 3139	. . . 4 ⊢ ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → (∃𝑥 ∈ ℝ (𝑧 · 𝑥) = 1 → 1 ∈ ℝ))
63	57, 62	mpd 15	. . 3 ⊢ ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → 1 ∈ ℝ)
64	63	rexlimiva 3131	. 2 ⊢ (∃𝑧 ∈ ℝ 𝑧 ≠ 0 → 1 ∈ ℝ)
65	40, 56, 64	mp2b 10	1 ⊢ 1 ∈ ℝ

Syntax hints:   → wi 4   ∧ wa 395   ∨ wo 848   = wceq 1542   ∈ wcel 2114   ≠ wne 2933  ∃wrex 3062  (class class class)co 7361  ℂcc 11030  ℝcr 11031  0cc0 11032  1c1 11033  ici 11034   + caddc 11035   · cmul 11037

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 2709  ax-1cn 11090  ax-icn 11091  ax-addcl 11092  ax-mulcl 11094  ax-mulrcl 11095  ax-i2m1 11100  ax-1ne0 11101  ax-rrecex 11104  ax-cnre 11105

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 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-iota 6449  df-fv 6501  df-ov 7364

This theorem is referenced by:  1red  11139  pr01ssre  11142  1xr  11198  dedekind  11303  peano2re  11313  mul02lem2  11317  addrid  11320  renegcl  11451  peano2rem  11455  0reALT  11485  0lt1  11666  0le1  11667  relin01  11668  1le1  11772  eqneg  11869  ltp1  11989  ltm1  11991  recgt0  11995  mulgt1OLD  12008  ltmulgt11  12009  lemulge11  12012  reclt1  12045  recgt1  12046  recgt1i  12047  recp1lt1  12048  recreclt  12049  recgt0ii  12056  ledivp1i  12075  ltdivp1i  12076  neg1rr  12139  neg1lt0  12141  cju  12149  indf  12159  indfval  12160  nnssre  12172  nnge1  12199  nngt1ne1  12200  nnle1eq1  12201  nngt0  12202  nnnlt1  12203  nnne0  12205  nnrecre  12213  nnrecgt0  12214  nnsub  12215  1t1e1ALT  12226  2re  12249  3re  12255  4re  12259  5re  12262  6re  12265  7re  12268  8re  12271  9re  12274  0le2  12277  2pos  12278  3pos  12280  4pos  12282  5pos  12284  6pos  12285  7pos  12286  8pos  12287  9pos  12288  1lt2  12341  1lt3  12343  1lt4  12346  1lt5  12350  1lt6  12355  1lt7  12361  1lt8  12368  1lt9  12376  1ne2  12378  1le2  12379  1le3  12382  halflt1  12388  addltmul  12407  nnunb  12427  elnnnn0c  12476  nn0ge2m1nn  12501  elnnz1  12547  znnnlt1  12548  zltp1le  12571  zleltp1  12572  nn0lt2  12586  recnz  12598  gtndiv  12600  3halfnz  12602  10re  12657  1lt10  12777  eluzp1m1  12808  eluzp1p1  12810  eluz2b2  12865  zbtwnre  12890  rebtwnz  12891  1rp  12940  divlt1lt  13007  divle1le  13008  nnledivrp  13050  qbtwnxr  13146  xmulrid  13225  xmulm1  13227  x2times  13245  xrub  13258  elicc01  13413  1elunit  13417  divelunit  13441  lincmb01cmp  13442  unitssre  13446  0nelfz1  13491  fzpreddisj  13521  fznatpl1  13526  fztpval  13534  fraclt1  13755  fracle1  13756  flbi2  13770  fldiv4p1lem1div2  13788  fldiv4lem1div2  13790  fldiv  13813  modid  13849  1mod  13856  m1modnnsub1  13873  modm1p1mod0  13878  seqf1olem1  13997  reexpcl  14034  reexpclz  14038  expge0  14054  expge1  14055  expgt1  14056  bernneq  14185  bernneq2  14186  expnbnd  14188  expnlbnd  14189  expnlbnd2  14190  expmulnbnd  14191  discr1  14195  facwordi  14245  faclbnd3  14248  faclbnd4lem1  14249  faclbnd4lem4  14252  faclbnd6  14255  facavg  14257  hashv01gt1  14301  hashnn0n0nn  14347  hashunsnggt  14350  hash1snb  14375  hashgt12el  14378  hashgt12el2  14379  hashfun  14393  hashge2el2dif  14436  tpf1ofv2  14454  lsw0  14521  f1oun2prg  14873  cjexp  15106  re1  15110  im1  15111  rei  15112  imi  15113  01sqrexlem1  15198  01sqrexlem2  15199  01sqrexlem3  15200  01sqrexlem4  15201  01sqrexlem7  15204  resqrex  15206  sqrt1  15227  sqrt2gt1lt2  15230  sqrtm1  15231  abs1  15253  absrdbnd  15298  caubnd2  15314  mulcn2  15552  reccn2  15553  rlimno1  15610  o1fsum  15770  expcnv  15823  geolim  15829  geolim2  15830  georeclim  15831  geomulcvg  15835  geoisumr  15837  geoisum1c  15839  fprodge0  15952  fprodge1  15954  rerisefaccl  15976  refallfaccl  15977  ere  16048  ege2le3  16049  efgt1  16077  resin4p  16099  recos4p  16100  tanhbnd  16122  sinbnd  16141  cosbnd  16142  sinbnd2  16143  cosbnd2  16144  ef01bndlem  16145  sin01bnd  16146  cos01bnd  16147  cos1bnd  16148  cos2bnd  16149  sinltx  16150  sin01gt0  16151  cos01gt0  16152  sin02gt0  16153  sincos1sgn  16154  ene1  16171  rpnnen2lem2  16176  rpnnen2lem3  16177  rpnnen2lem4  16178  rpnnen2lem9  16183  rpnnen2lem12  16186  ruclem6  16196  ruclem11  16201  ruclem12  16202  3dvds  16294  flodddiv4  16378  sadcadd  16421  isprm3  16646  sqnprm  16666  coprm  16675  phibndlem  16734  pythagtriplem3  16783  pcmpt  16857  fldivp1  16862  pockthi  16872  infpn2  16878  basendxnmulrndx  17253  starvndxnbasendx  17261  scandxnbasendx  17273  vscandxnbasendx  17278  ipndxnbasendx  17289  basendxnocndx  17340  slotsbhcdif  17372  lt6abl  19864  srgbinomlem4  20204  0ringnnzr  20496  abvneg  20797  abvtrivd  20803  xrsmcmn  21384  xrsnsgrp  21400  gzrngunitlem  21425  gzrngunit  21426  rge0srg  21431  psgnodpmr  21583  remulg  21600  resubdrg  21601  psdmvr  22148  dscmet  24550  dscopn  24551  nrginvrcnlem  24669  idnghm  24721  tgioo  24774  blcvx  24776  iicmp  24866  iiconn  24867  iirev  24909  iihalf1  24911  iihalf2  24913  elii1  24915  elii2  24916  iimulcl  24917  icopnfcnv  24922  icopnfhmeo  24923  iccpnfhmeo  24925  xrhmeo  24926  xrhmph  24927  evth  24939  xlebnum  24945  htpycc  24960  reparphti  24977  pcoval1  24993  pco1  24995  pcoval2  24996  pcocn  24997  pcohtpylem  24999  pcopt  25002  pcopt2  25003  pcoass  25004  pcorevlem  25006  nmhmcn  25100  ncvs1  25137  ovolunlem1a  25476  vitalilem2  25589  vitalilem4  25591  vitalilem5  25592  vitali  25593  i1f1  25670  itg11  25671  itg2const  25720  dveflem  25959  dvlipcn  25974  dvcvx  26000  ply1remlem  26143  fta1blem  26149  vieta1lem2  26291  aalioulem3  26314  aalioulem5  26316  aaliou3lem2  26323  ulmbdd  26379  iblulm  26388  radcnvlem1  26394  dvradcnv  26402  abelthlem2  26413  abelthlem3  26414  abelthlem5  26416  abelthlem7  26419  abelth  26422  abelth2  26423  reeff1olem  26427  reeff1o  26428  sinhalfpilem  26443  tangtx  26485  sincos4thpi  26493  pige3ALT  26500  coskpi  26503  cos0pilt1  26512  recosf1o  26515  tanregt0  26519  efif1olem3  26524  efif1olem4  26525  loge  26566  logdivlti  26600  logcnlem4  26625  logf1o2  26630  logtayl  26640  logccv  26643  recxpcl  26655  cxplea  26676  cxpcn3lem  26727  cxpaddlelem  26731  loglesqrt  26741  ang180lem2  26790  angpined  26810  acosrecl  26883  atancj  26890  atanlogaddlem  26893  atantan  26903  atans2  26911  ressatans  26914  leibpi  26922  log2le1  26930  birthdaylem3  26933  cxp2lim  26957  cxploglim  26958  cxploglim2  26959  divsqrtsumlem  26960  cvxcl  26965  scvxcvx  26966  jensenlem2  26968  amgmlem  26970  emcllem2  26977  emcllem4  26979  emcllem6  26981  emcllem7  26982  emre  26986  emgt0  26987  harmonicbnd3  26988  harmonicubnd  26990  harmonicbnd4  26991  zetacvg  26995  ftalem1  27053  ftalem2  27054  ftalem5  27057  issqf  27116  cht1  27145  chp1  27147  ppiltx  27157  mumullem2  27160  ppiublem1  27182  ppiub  27184  chtublem  27191  chtub  27192  logfacbnd3  27203  logexprlim  27205  perfectlem2  27210  dchrinv  27241  dchr1re  27243  efexple  27261  bposlem1  27264  bposlem2  27265  bposlem5  27268  bposlem8  27271  lgsdir2lem1  27305  lgsdir2lem5  27309  lgsdir  27312  lgsne0  27315  lgsabs1  27316  lgsdinn0  27325  gausslemma2dlem0i  27344  lgseisen  27359  m1lgs  27368  2lgslem3  27384  addsq2nreurex  27424  2sqreultblem  27428  2sqreunnltblem  27431  chebbnd1lem3  27451  chebbnd1  27452  chtppilimlem1  27453  chtppilimlem2  27454  chtppilim  27455  chpchtlim  27459  vmadivsumb  27463  rplogsumlem2  27465  rpvmasumlem  27467  dchrmusumlema  27473  dchrmusum2  27474  dchrvmasumlem2  27478  dchrvmasumiflem1  27481  dchrisum0flblem1  27488  dchrisum0flblem2  27489  dchrisum0fno1  27491  rpvmasum2  27492  dchrisum0re  27493  dchrisum0lema  27494  dchrisum0lem1b  27495  dchrisum0lem1  27496  dchrisum0lem2a  27497  dchrisum0lem2  27498  logdivsum  27513  mulog2sumlem2  27515  2vmadivsumlem  27520  log2sumbnd  27524  selbergb  27529  selberg2b  27532  chpdifbndlem1  27533  selberg3lem1  27537  selberg3lem2  27538  selberg4lem1  27540  pntrmax  27544  pntrsumo1  27545  selbergsb  27555  pntrlog2bndlem3  27559  pntrlog2bndlem5  27561  pntpbnd1a  27565  pntpbnd2  27567  pntibndlem1  27569  pntibndlem3  27572  pntlemd  27574  pntlemc  27575  pntlemb  27577  pntlemr  27582  pntlemf  27585  pntlemk  27586  pntlemo  27587  pntlem3  27589  pntleml  27591  abvcxp  27595  ostth2lem1  27598  ostth1  27613  ostth2lem2  27614  ostth2lem3  27615  ostth2lem4  27616  ostth2  27617  ostth3  27618  ostth  27619  slotsinbpsd  28526  slotslnbpsd  28527  trgcgrg  28600  brbtwn2  28991  colinearalglem4  28995  ax5seglem2  29015  ax5seglem3  29017  axpaschlem  29026  axpasch  29027  axlowdimlem6  29033  axlowdimlem10  29037  axlowdimlem16  29043  axlowdim1  29045  axlowdim2  29046  axlowdim  29047  axcontlem2  29051  elntg2  29071  lfgrnloop  29211  lfuhgr1v0e  29340  usgrexmpldifpr  29344  usgrexmplef  29345  1loopgrvd2  29590  vdegp1bi  29624  lfgrwlkprop  29772  pthdlem1  29852  pthdlem2  29854  clwlkclwwlkf  30096  upgr4cycl4dv4e  30273  konigsberglem2  30341  konigsberglem3  30342  konigsberglem5  30344  frgrreg  30482  ex-dif  30511  ex-in  30513  ex-pss  30516  ex-res  30529  ex-fl  30535  nv1  30764  smcnlem  30786  ipidsq  30799  nmlno0lem  30882  norm-ii-i  31226  bcs2  31271  norm1  31338  nmopub2tALT  31998  nmfnleub2  32015  nmlnop0iALT  32084  unopbd  32104  nmopadjlem  32178  nmopcoadji  32190  pjnmopi  32237  pjbdlni  32238  hstle1  32315  hstle  32319  hstles  32320  stge1i  32327  stlesi  32330  staddi  32335  stadd3i  32337  strlem1  32339  strlem5  32344  jplem1  32357  cdj1i  32522  addltmulALT  32535  xlt2addrd  32850  sgnclre  32923  sgnnbi  32929  sgnpbi  32930  sgnmulsgp  32934  dp2lt10  32961  dp2ltsuc  32963  dp2ltc  32964  dplti  32982  dpmul4  32991  cshw1s2  33038  xrsmulgzz  33087  rearchi  33424  xrge0slmod  33426  prmidl0  33528  evl1deg3  33656  constrconj  33908  2sqr3minply  33943  submateqlem1  33970  xrge0iifcnv  34096  xrge0iifcv  34097  xrge0iifiso  34098  xrge0iifhom  34100  zrhre  34182  esumcst  34226  cntnevol  34391  omssubadd  34463  iwrdsplit  34550  dstfrvclim1  34641  coinfliprv  34646  ballotlem2  34652  ballotlem4  34662  ballotlemi1  34666  ballotlemic  34670  plymulx0  34710  plymulx  34711  signswch  34724  signstf  34729  signsvfn  34745  itgexpif  34769  hgt750lemd  34811  logdivsqrle  34813  hgt750lem  34814  hgt750lem2  34815  hgt750leme  34821  tgoldbachgnn  34822  subfacp1lem1  35380  subfacp1lem5  35385  resconn  35447  iisconn  35453  iillysconn  35454  problem2  35867  problem3  35868  sinccvglem  35873  fz0n  35932  dnibndlem12  36768  knoppcnlem4  36775  knoppndvlem13  36803  cnndvlem1  36816  irrdiff  37659  relowlpssretop  37697  sin2h  37948  cos2h  37949  tan2h  37950  poimirlem7  37965  poimirlem16  37974  poimirlem17  37975  poimirlem19  37977  poimirlem20  37978  poimirlem22  37980  poimirlem23  37981  poimirlem29  37987  poimirlem31  37989  itg2addnclem3  38011  asindmre  38041  dvasin  38042  dvacos  38043  dvreasin  38044  dvreacos  38045  fdc  38083  geomcau  38097  cntotbnd  38134  heiborlem8  38156  bfplem2  38161  bfp  38162  aks4d1p1p7  42530  ine1  42763  re1m1e0m0  42846  sn-00idlem1  42847  sn-00idlem2  42848  remul02  42854  sn-0ne2  42855  reixi  42872  rei4  42873  remullid  42883  ipiiie0  42887  sn-0tie0  42913  sn-nnne0  42922  mulgt0b1d  42934  sn-0lt1  42937  sn-ltp1  42938  reneg1lt0  42942  sn-inelr  42949  rabren3dioph  43264  pellexlem5  43282  pellexlem6  43283  pell1qrgaplem  43322  pell14qrgap  43324  pellqrex  43328  pellfundre  43330  pellfundlb  43333  pellfund14gap  43336  jm2.17a  43409  acongeq  43432  jm2.23  43445  jm3.1lem2  43467  sqrtcval  44089  sqrtcval2  44090  resqrtval  44091  imsqrtval  44092  relexp01min  44161  cvgdvgrat  44761  lhe4.4ex1a  44777  binomcxplemnotnn0  44804  isosctrlem1ALT  45381  supxrgelem  45788  xrlexaddrp  45803  infxr  45817  infleinflem2  45821  sumnnodd  46081  limsup10exlem  46221  limsup10ex  46222  dvnprodlem3  46397  stoweidlem1  46450  stoweidlem18  46467  stoweidlem19  46468  stoweidlem26  46475  stoweidlem34  46483  stoweidlem40  46489  stoweidlem41  46490  stoweidlem59  46508  stoweid  46512  stirlinglem10  46532  stirlinglem11  46533  dirkercncflem1  46552  fourierdlem16  46572  fourierdlem21  46577  fourierdlem22  46578  fourierdlem42  46598  fourierdlem68  46623  fourierdlem83  46638  fourierdlem103  46658  sqwvfourb  46678  fouriersw  46680  etransclem23  46706  salgencntex  46792  ovn0lem  47014  smfmullem3  47242  smfmullem4  47243  nthrucw  47335  cjnpoly  47352  zm1nn  47765  ceilhalf1  47801  m1mod0mod1  47823  muldvdsfacgt  47849  fmtnosqrt  48017  nprmdvdsfacm1lem4  48101  perfectALTVlem2  48213  2exp340mod341  48224  8exp8mod9  48227  nfermltl8rev  48233  nnsum3primesprm  48281  nnsum4primesodd  48287  nnsum4primesoddALTV  48288  nnsum4primeseven  48291  nnsum4primesevenALTV  48292  tgblthelfgott  48306  tgoldbach  48308  usgrexmpl1lem  48512  usgrexmpl2lem  48517  usgrexmpl2nb1  48523  usgrexmpl2nb3  48525  usgrexmpl2nb4  48526  usgrexmpl2nb5  48527  usgrexmpl2trifr  48528  gpg3kgrtriexlem3  48576  pgnbgreunbgrlem2lem1  48605  pgnbgreunbgrlem2lem2  48606  rege1logbrege0  49049  rege1logbzge0  49050  blennnelnn  49067  dignnld  49094  nn0sumshdiglemA  49110  nn0sumshdiglem1  49112  rrx2xpref1o  49209  rrxlines  49224  eenglngeehlnmlem1  49228  eenglngeehlnmlem2  49229  line2ylem  49242  line2x  49245  icccldii  49409  io1ii  49411  sepfsepc  49418