Theorem 1re 11318

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 11268, 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 11279	. . 3 ⊢ 1 ≠ 0
2		ax-1cn 11268	. . . . 5 ⊢ 1 ∈ ℂ
3		cnre 11315	. . . . 5 ⊢ (1 ∈ ℂ → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)))
4	2, 3	ax-mp 5	. . . 4 ⊢ ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏))
5		neeq1 3020	. . . . . . . 8 ⊢ (1 = (𝑎 + (i · 𝑏)) → (1 ≠ 0 ↔ (𝑎 + (i · 𝑏)) ≠ 0))
6	5	biimpcd 252	. . . . . . 7 ⊢ (1 ≠ 0 → (1 = (𝑎 + (i · 𝑏)) → (𝑎 + (i · 𝑏)) ≠ 0))
7		0cn 11308	. . . . . . . 8 ⊢ 0 ∈ ℂ
8		cnre 11315	. . . . . . . 8 ⊢ (0 ∈ ℂ → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)))
9	7, 8	ax-mp 5	. . . . . . 7 ⊢ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑))
10		neeq2 3021	. . . . . . . . . 10 ⊢ (0 = (𝑐 + (i · 𝑑)) → ((𝑎 + (i · 𝑏)) ≠ 0 ↔ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
11	10	biimpcd 252	. . . . . . . . 9 ⊢ ((𝑎 + (i · 𝑏)) ≠ 0 → (0 = (𝑐 + (i · 𝑑)) → (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
12	11	reximdv 3180	. . . . . . . 8 ⊢ ((𝑎 + (i · 𝑏)) ≠ 0 → (∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)) → ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
13	12	reximdv 3180	. . . . . . 7 ⊢ ((𝑎 + (i · 𝑏)) ≠ 0 → (∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)) → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
14	6, 9, 13	syl6mpi 68	. . . . . 6 ⊢ (1 ≠ 0 → (1 = (𝑎 + (i · 𝑏)) → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
15	14	reximdv 3180	. . . . 5 ⊢ (1 ≠ 0 → (∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)) → ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
16	15	reximdv 3180	. . . 4 ⊢ (1 ≠ 0 → (∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)) → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
17	4, 16	mpi 21	. . 3 ⊢ (1 ≠ 0 → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)))
18		id 23	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑐 → 𝑎 = 𝑐)
19		oveq2 7435	. . . . . . . . . . . 12 ⊢ (𝑏 = 𝑑 → (i · 𝑏) = (i · 𝑑))
20	18, 19	oveqan12d 7446	. . . . . . . . . . 11 ⊢ ((𝑎 = 𝑐 ∧ 𝑏 = 𝑑) → (𝑎 + (i · 𝑏)) = (𝑐 + (i · 𝑑)))
21	20	expcom 419	. . . . . . . . . 10 ⊢ (𝑏 = 𝑑 → (𝑎 = 𝑐 → (𝑎 + (i · 𝑏)) = (𝑐 + (i · 𝑑))))
22	21	necon3d 2979	. . . . . . . . 9 ⊢ (𝑏 = 𝑑 → ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → 𝑎 ≠ 𝑐))
23	22	com12 33	. . . . . . . 8 ⊢ ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → (𝑏 = 𝑑 → 𝑎 ≠ 𝑐))
24	23	necon3bd 2972	. . . . . . 7 ⊢ ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → (¬ 𝑎 ≠ 𝑐 → 𝑏 ≠ 𝑑))
25	24	orrd 877	. . . . . 6 ⊢ ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → (𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑))
26		neeq1 3020	. . . . . . . . . 10 ⊢ (𝑥 = 𝑎 → (𝑥 ≠ 𝑦 ↔ 𝑎 ≠ 𝑦))
27		neeq2 3021	. . . . . . . . . 10 ⊢ (𝑦 = 𝑐 → (𝑎 ≠ 𝑦 ↔ 𝑎 ≠ 𝑐))
28	26, 27	rspc2ev 3591	. . . . . . . . 9 ⊢ ((𝑎 ∈ ℝ ∧ 𝑐 ∈ ℝ ∧ 𝑎 ≠ 𝑐) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦)
29	28	3expia 1139	. . . . . . . 8 ⊢ ((𝑎 ∈ ℝ ∧ 𝑐 ∈ ℝ) → (𝑎 ≠ 𝑐 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
30	29	ad2ant2r 760	. . . . . . 7 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → (𝑎 ≠ 𝑐 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
31		neeq1 3020	. . . . . . . . . 10 ⊢ (𝑥 = 𝑏 → (𝑥 ≠ 𝑦 ↔ 𝑏 ≠ 𝑦))
32		neeq2 3021	. . . . . . . . . 10 ⊢ (𝑦 = 𝑑 → (𝑏 ≠ 𝑦 ↔ 𝑏 ≠ 𝑑))
33	31, 32	rspc2ev 3591	. . . . . . . . 9 ⊢ ((𝑏 ∈ ℝ ∧ 𝑑 ∈ ℝ ∧ 𝑏 ≠ 𝑑) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦)
34	33	3expia 1139	. . . . . . . 8 ⊢ ((𝑏 ∈ ℝ ∧ 𝑑 ∈ ℝ) → (𝑏 ≠ 𝑑 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
35	34	ad2ant2l 759	. . . . . . 7 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → (𝑏 ≠ 𝑑 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
36	30, 35	jaod 873	. . . . . 6 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → ((𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
37	25, 36	syl5 35	. . . . 5 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
38	37	rexlimdvva 3222	. . . 4 ⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
39	38	rexlimivv 3207	. . 3 ⊢ (∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦)
40	1, 17, 39	mp2b 10	. 2 ⊢ ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦
41		eqtr3 2785	. . . . . . . . 9 ⊢ ((𝑥 = 0 ∧ 𝑦 = 0) → 𝑥 = 𝑦)
42	41	ex 418	. . . . . . . 8 ⊢ (𝑥 = 0 → (𝑦 = 0 → 𝑥 = 𝑦))
43	42	necon3d 2979	. . . . . . 7 ⊢ (𝑥 = 0 → (𝑥 ≠ 𝑦 → 𝑦 ≠ 0))
44		neeq1 3020	. . . . . . . . 9 ⊢ (𝑧 = 𝑦 → (𝑧 ≠ 0 ↔ 𝑦 ≠ 0))
45	44	rspcev 3579	. . . . . . . 8 ⊢ ((𝑦 ∈ ℝ ∧ 𝑦 ≠ 0) → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)
46	45	expcom 419	. . . . . . 7 ⊢ (𝑦 ≠ 0 → (𝑦 ∈ ℝ → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
47	43, 46	syl6 36	. . . . . 6 ⊢ (𝑥 = 0 → (𝑥 ≠ 𝑦 → (𝑦 ∈ ℝ → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
48	47	com23 87	. . . . 5 ⊢ (𝑥 = 0 → (𝑦 ∈ ℝ → (𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
49	48	adantld 496	. . . 4 ⊢ (𝑥 = 0 → ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
50		neeq1 3020	. . . . . . . 8 ⊢ (𝑧 = 𝑥 → (𝑧 ≠ 0 ↔ 𝑥 ≠ 0))
51	50	rspcev 3579	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)
52	51	expcom 419	. . . . . 6 ⊢ (𝑥 ≠ 0 → (𝑥 ∈ ℝ → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
53	52	adantrd 497	. . . . 5 ⊢ (𝑥 ≠ 0 → ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
54	53	a1dd 51	. . . 4 ⊢ (𝑥 ≠ 0 → ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
55	49, 54	pm2.61ine 3041	. . 3 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
56	55	rexlimivv 3207	. 2 ⊢ (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)
57		ax-rrecex 11282	. . . 4 ⊢ ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → ∃𝑥 ∈ ℝ (𝑧 · 𝑥) = 1)
58		remulcl 11295	. . . . . . 7 ⊢ ((𝑧 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (𝑧 · 𝑥) ∈ ℝ)
59	58	adantlr 728	. . . . . 6 ⊢ (((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) ∧ 𝑥 ∈ ℝ) → (𝑧 · 𝑥) ∈ ℝ)
60		eleq1 2851	. . . . . 6 ⊢ ((𝑧 · 𝑥) = 1 → ((𝑧 · 𝑥) ∈ ℝ ↔ 1 ∈ ℝ))
61	59, 60	syl5ibcom 248	. . . . 5 ⊢ (((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) ∧ 𝑥 ∈ ℝ) → ((𝑧 · 𝑥) = 1 → 1 ∈ ℝ))
62	61	rexlimdva 3166	. . . 4 ⊢ ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → (∃𝑥 ∈ ℝ (𝑧 · 𝑥) = 1 → 1 ∈ ℝ))
63	57, 62	mpd 16	. . 3 ⊢ ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → 1 ∈ ℝ)
64	63	rexlimiva 3158	. 2 ⊢ (∃𝑧 ∈ ℝ 𝑧 ≠ 0 → 1 ∈ ℝ)
65	40, 56, 64	mp2b 10	1 ⊢ 1 ∈ ℝ

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∨ wo 861   = wceq 1569   ∈ wcel 2146   ≠ wne 2958  ∃wrex 3089  (class class class)co 7427  ℂcc 11208  ℝcr 11209  0cc0 11210  1c1 11211  ici 11212   + caddc 11213   · cmul 11215

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735  ax-1cn 11268  ax-icn 11269  ax-addcl 11270  ax-mulcl 11272  ax-mulrcl 11273  ax-i2m1 11278  ax-1ne0 11279  ax-rrecex 11282  ax-cnre 11283

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3416  df-v 3455  df-ss 3900  df-dif 4049  df-un 4153  df-nul 4281  df-if 4485  df-sn 4588  df-pr 4590  df-op 4838  df-uni 4870  df-br 5106  df-iota 6500  df-fv 6554  df-ov 7430

This theorem is used by:  1red  11319  pr01ssre  11322  1xr  11378  dedekind  11483  peano2re  11493  mul02lem2  11497  addrid  11500  renegcl  11631  peano2rem  11635  0reALT  11665  0lt1  11848  0le1  11849  relin01  11850  1le1  11954  eqneg  12047  ltp1  12167  ltm1  12169  recgt0  12173  ltmulgt11  12186  lemulge11  12189  reclt1  12222  recgt1  12223  recgt1i  12224  recp1lt1  12225  recreclt  12226  recgt0ii  12233  ledivp1i  12252  ltdivp1i  12253  neg1rr  12316  neg1lt0  12318  cju  12326  indf  12336  indfval  12337  nnssre  12349  nnge1  12376  nngt1ne1  12377  nnle1eq1  12378  nngt0  12379  nnnlt1  12380  nnne0  12382  nnrecre  12390  nnrecgt0  12391  nnsub  12392  1t1e1ALT  12403  2re  12427  3re  12433  4re  12437  5re  12440  6re  12443  7re  12446  8re  12449  9re  12452  0le2OLD  12456  2posOLD  12458  1lt2  12525  1lt3  12528  1lt4  12531  1lt5  12535  1lt6  12540  1lt7  12546  1lt8  12553  1lt9  12561  1ne2  12563  1le2  12564  1le3  12567  halflt1  12573  addltmul  12592  nnunb  12612  elnnnn0c  12661  nn0ge2m1nn  12686  elnnz1  12732  znnnlt1  12733  zltp1le  12756  zleltp1  12757  nn0lt2  12772  recnz  12784  gtndiv  12786  3halfnz  12788  10re  12847  1lt10  12969  1lt10OLD  12970  eluzp1m1  13001  eluzp1p1  13003  eluz2b2  13058  zbtwnre  13083  rebtwnz  13084  1rp  13134  divlt1lt  13201  divle1le  13202  nnledivrp  13244  qbtwnxr  13340  xmulrid  13419  xmulm1  13421  x2times  13439  xrub  13452  elicc01  13607  1elunit  13611  divelunit  13635  lincmb01cmp  13636  unitssre  13640  0nelfz1  13686  fzpreddisj  13717  fznatpl1  13722  fztpval  13730  fraclt1  13952  fracle1  13953  flbi2  13967  fldiv4p1lem1div2  13985  fldiv4lem1div2  13987  fldiv  14010  modid  14046  1mod  14053  m1modnnsub1  14070  modm1p1mod0  14075  seqf1olem1  14194  reexpcl  14231  reexpclz  14235  expge0  14251  expge1  14252  expgt1  14253  bernneq  14383  bernneq2  14384  expnbnd  14386  expnlbnd  14387  expnlbnd2  14388  expmulnbnd  14389  discr1  14393  facwordi  14443  faclbnd3  14446  faclbnd4lem1  14447  faclbnd4lem4  14450  faclbnd6  14453  facavg  14455  hashv01gt1  14499  hashnn0n0nn  14545  hashunsnggt  14548  hash1snb  14574  hashgt12el  14577  hashgt12el2  14578  hashfun  14592  hashge2el2dif  14635  tpf1ofv2  14653  lsw0  14720  f1oun2prg  15080  sgnclre  15267  sgnnbi  15269  sgnpbi  15270  cjexp  15329  re1  15333  im1  15334  rei  15335  imi  15336  01sqrexlem1  15421  01sqrexlem2  15422  01sqrexlem3  15423  01sqrexlem4  15424  01sqrexlem7  15427  resqrex  15429  sqrt1  15450  sqrt2gt1lt2  15453  sqrtm1  15454  abs1  15476  absrdbnd  15521  caubnd2  15537  mulcn2  15775  reccn2  15776  rlimno1  15833  o1fsum  15992  expcnv  16045  geolim  16051  geolim2  16052  georeclim  16053  geomulcvg  16057  geoisumr  16059  geoisum1c  16061  fprodge0  16172  fprodge1  16174  rerisefaccl  16196  refallfaccl  16197  ere  16267  ege2le3  16268  efgt1  16296  resin4p  16318  recos4p  16319  tanhbnd  16341  sinbnd  16360  cosbnd  16361  sinbnd2  16362  cosbnd2  16363  ef01bndlem  16364  sin01bnd  16365  cos01bnd  16366  cos1bnd  16367  cos2bnd  16368  sinltx  16369  sin01gt0  16370  cos01gt0  16371  sin02gt0  16372  sincos1sgn  16373  ene1  16390  rpnnen2lem2  16395  rpnnen2lem3  16396  rpnnen2lem4  16397  rpnnen2lem9  16402  rpnnen2lem12  16405  ruclem6  16415  ruclem11  16420  ruclem12  16421  3dvds  16513  flodddiv4  16597  sadcadd  16640  isprm3  16870  sqnprm  16890  coprm  16899  phibndlem  16959  pythagtriplem3  17008  pcmpt  17082  fldivp1  17087  pockthi  17097  infpn2  17103  basendxnmulrndx  17479  starvndxnbasendx  17487  scandxnbasendx  17499  vscandxnbasendx  17504  ipndxnbasendx  17515  basendxnocndx  17566  slotsbhcdif  17598  lt6abl  20121  srgbinomlem4  20467  0ringnnzr  20788  abvneg  21095  abvtrivd  21101  prmidl0  21646  xrsmcmn  21713  xrsnsgrp  21726  gzrngunitlem  21750  gzrngunit  21751  rge0srg  21756  psgnodpmr  21908  remulg  21925  resubdrg  21926  psdmvr  22502  dscmet  24903  dscopn  24904  nrginvrcnlem  25022  idnghm  25074  tgioo  25127  blcvx  25129  iicmp  25219  iiconn  25220  iirev  25262  iihalf1  25264  iihalf2  25266  elii1  25268  elii2  25269  iimulcl  25270  icopnfcnv  25275  icopnfhmeo  25276  iccpnfhmeo  25278  xrhmeo  25279  xrhmph  25280  evth  25292  xlebnum  25298  htpycc  25313  reparphti  25330  pcoval1  25346  pco1  25348  pcoval2  25349  pcocn  25350  pcohtpylem  25352  pcopt  25355  pcopt2  25356  pcoass  25357  pcorevlem  25359  nmhmcn  25453  ncvs1  25490  ovolunlem1a  25829  vitalilem2  25942  vitalilem4  25944  vitalilem5  25945  vitali  25946  i1f1  26023  itg11  26024  itg2const  26073  dveflem  26311  dvlipcn  26326  dvcvx  26352  ply1remlem  26495  fta1blem  26501  plyn0mulidp  26614  plymulidp  26615  vieta1lem2  26646  aalioulem3  26673  aalioulem5  26675  aaliou3lem2  26682  ulmbdd  26737  iblulm  26746  radcnvlem1  26752  dvradcnv  26760  abelthlem2  26771  abelthlem3  26772  abelthlem5  26774  abelthlem7  26777  abelth  26780  abelth2  26781  reeff1olem  26785  reeff1o  26786  sinhalfpilem  26804  tangtx  26846  sincos4thpi  26854  pige3ALT  26860  coskpi  26863  recosf1o  26875  tanregt0  26879  efif1olem3  26884  efif1olem4  26885  loge  26926  logdivlti  26960  logcnlem4  26985  logf1o2  26990  logtayl  27000  logccv  27003  recxpcl  27015  cxplea  27036  cxpcn3lem  27087  cxpaddlelem  27091  loglesqrt  27101  ang180lem2  27150  angpined  27170  acosrecl  27243  atancj  27250  atanlogaddlem  27253  atantan  27263  atans2  27271  ressatans  27274  leibpi  27282  log2le1  27290  birthdaylem3  27293  cxp2lim  27316  cxploglim  27317  cxploglim2  27318  divsqrtsumlem  27319  cvxcl  27324  scvxcvx  27325  jensenlem2  27327  amgmlem  27329  emcllem2  27336  emcllem4  27338  emcllem6  27340  emcllem7  27341  emre  27345  emgt0  27346  harmonicbnd3  27347  harmonicubnd  27349  harmonicbnd4  27350  zetacvg  27354  ftalem1  27412  ftalem2  27413  ftalem5  27416  issqf  27475  cht1  27504  chp1  27506  ppiltx  27516  mumullem2  27519  ppiublem1  27541  ppiub  27543  chtublem  27550  chtub  27551  logfacbnd3  27562  logexprlim  27564  perfectlem2  27569  dchrinv  27600  dchr1re  27602  efexple  27620  bposlem1  27623  bposlem2  27624  bposlem5  27627  bposlem8  27630  lgsdir2lem1  27664  lgsdir2lem5  27668  lgsdir  27671  lgsne0  27674  lgsabs1  27675  lgsdinn0  27684  gausslemma2dlem0i  27703  lgseisen  27718  m1lgs  27727  2lgslem3  27743  addsq2nreurex  27783  2sqreultblem  27787  2sqreunnltblem  27790  chebbnd1lem3  27810  chebbnd1  27811  chtppilimlem1  27812  chtppilimlem2  27813  chtppilim  27814  chpchtlim  27818  vmadivsumb  27822  rplogsumlem2  27824  rpvmasumlem  27826  dchrmusumlema  27832  dchrmusum2  27833  dchrvmasumlem2  27837  dchrvmasumiflem1  27840  dchrisum0flblem1  27847  dchrisum0flblem2  27848  dchrisum0fno1  27850  rpvmasum2  27851  dchrisum0re  27852  dchrisum0lema  27853  dchrisum0lem1b  27854  dchrisum0lem1  27855  dchrisum0lem2a  27856  dchrisum0lem2  27857  logdivsum  27872  mulog2sumlem2  27874  2vmadivsumlem  27879  log2sumbnd  27883  selbergb  27888  selberg2b  27891  chpdifbndlem1  27892  selberg3lem1  27896  selberg3lem2  27897  selberg4lem1  27899  pntrmax  27903  pntrsumo1  27904  selbergsb  27914  pntrlog2bndlem3  27918  pntrlog2bndlem5  27920  pntpbnd1a  27924  pntpbnd2  27926  pntibndlem1  27928  pntibndlem3  27931  pntlemd  27933  pntlemc  27934  pntlemb  27936  pntlemr  27941  pntlemf  27944  pntlemk  27945  pntlemo  27946  pntlem3  27948  pntleml  27950  abvcxp  27954  ostth2lem1  27957  ostth1  27972  ostth2lem2  27973  ostth2lem3  27974  ostth2lem4  27975  ostth2  27976  ostth3  27977  ostth  27978  slotsinbpsd  28915  slotslnbpsd  28916  trgcgrg  28990  brbtwn2  29495  colinearalglem4  29499  ax5seglem2  29519  ax5seglem3  29521  axpaschlem  29530  axpasch  29531  axlowdimlem6  29537  axlowdimlem10  29541  axlowdimlem16  29547  axlowdim1  29549  axlowdim2  29550  axlowdim  29551  axcontlem2  29555  elntg2  29575  lfgrnloop  29715  lfuhgr1v0e  29847  usgrexmpldifpr  29851  usgrexmplef  29852  1loopgrvd2  30096  vdegp1bi  30130  lfgrwlkprop  30282  pthdlem1  30364  pthdlem2  30366  clwlkclwwlkf  30611  upgr4cycl4dv4e  30798  konigsberglem2  30866  konigsberglem3  30867  konigsberglem5  30869  frgrreg  31007  ex-dif  31036  ex-in  31038  ex-pss  31041  ex-res  31054  ex-fl  31060  nv1  31289  smcnlem  31311  ipidsq  31324  nmlno0lem  31407  norm-ii-i  31751  bcs2  31796  norm1  31863  nmopub2tALT  32523  nmfnleub2  32540  nmlnop0iALT  32609  unopbd  32629  nmopadjlem  32703  nmopcoadji  32715  pjnmopi  32762  pjbdlni  32763  hstle1  32840  hstle  32844  hstles  32845  stge1i  32852  stlesi  32855  staddi  32860  stadd3i  32862  strlem1  32864  strlem5  32869  jplem1  32882  cdj1i  33047  addltmulALT  33102  xlt2addrd  33404  sgnmulsgp  33476  dp2lt10  33503  dp2ltsuc  33505  dp2ltc  33506  dplti  33524  dpmul4  33533  cshw1s2  33574  xrsmulgzz  33623  rearchi  33960  xrge0slmod  33962  evl1deg3  34163  constrconj  34430  2sqr3minply  34465  submateqlem1  34492  xrge0iifcnv  34618  xrge0iifcv  34619  xrge0iifiso  34620  xrge0iifhom  34622  zrhre  34704  esumcst  34748  cntnevol  34914  iwrdsplit  35072  dstfrvclim1  35163  coinfliprv  35168  ballotlem2  35174  ballotlem4  35184  ballotlemi1  35188  ballotlemic  35192  signswch  35243  signstf  35248  signsvfn  35264  itgexpif  35288  hgt750lemd  35330  logdivsqrle  35332  hgt750lem  35333  hgt750lem2  35334  hgt750leme  35340  tgoldbachgnn  35341  subfacp1lem1  36065  subfacp1lem5  36070  resconn  36132  iisconn  36138  iillysconn  36139  problem2  36552  problem3  36553  sinccvglem  36558  fz0n  36623  dnibndlem12  37482  knoppcnlem4  37489  knoppndvlem13  37517  cnndvlem1  37530  irrdiff  38387  relowlpssretop  38427  sin2h  38673  cos2h  38674  tan2h  38675  poimirlem7  38685  poimirlem16  38694  poimirlem17  38695  poimirlem19  38697  poimirlem20  38698  poimirlem22  38700  poimirlem23  38701  poimirlem29  38707  poimirlem31  38709  itg2addnclem3  38731  asindmre  38761  dvasin  38762  dvacos  38763  dvreasin  38764  dvreacos  38765  fdc  38819  geomcau  38833  cntotbnd  38870  heiborlem8  38892  bfplem2  38897  bfp  38898  aks4d1p1p7  43264  ine1  43511  re1m1e0m0  43588  sn-00idlem1  43589  sn-00idlem2  43590  remul02  43596  sn-0ne2  43597  reixi  43614  rei4  43615  remullid  43625  ipiiie0  43629  sn-0tie0  43655  sn-nnne0  43664  mulgt0b1d  43676  sn-0lt1  43679  sn-ltp1  43680  reneg1lt0  43684  sn-inelr  43691  rabren3dioph  43962  pellexlem5  43980  pellexlem6  43981  pell1qrgaplem  44020  pell14qrgap  44022  pellqrex  44026  pellfundre  44028  pellfundlb  44031  pellfund14gap  44034  jm2.17a  44107  acongeq  44130  jm2.23  44143  jm3.1lem2  44165  sqrtcval  44781  sqrtcval2  44782  resqrtval  44783  imsqrtval  44784  relexp01min  44853  cvgdvgrat  45437  lhe4.4ex1a  45453  binomcxplemnotnn0  45480  isosctrlem1ALT  46055  supxrgelem  46488  xrlexaddrp  46503  infxr  46517  infleinflem2  46521  sumnnodd  46781  limsup10exlem  46921  limsup10ex  46922  dvnprodlem3  47097  stoweidlem1  47150  stoweidlem18  47167  stoweidlem19  47168  stoweidlem26  47175  stoweidlem34  47183  stoweidlem40  47189  stoweidlem41  47190  stoweidlem59  47208  stoweid  47212  stirlinglem10  47232  stirlinglem11  47233  dirkercncflem1  47252  fourierdlem16  47272  fourierdlem21  47277  fourierdlem22  47278  fourierdlem42  47298  fourierdlem68  47323  fourierdlem83  47338  fourierdlem103  47358  sqwvfourb  47378  fouriersw  47380  etransclem23  47406  salgencntex  47492  ovn0lem  47714  smfmullem3  47942  smfmullem4  47943  numtowerdt  48055  goldratval  48075  cjnpoly  48078  zm1nn  48511  ceilhalf1  48547  m1mod0mod1  48569  muldvdsfacgt  48595  fmtnosqrt  48763  nprmdvdsfacm1lem4  48847  perfectALTVlem2  48959  2exp340mod341  48970  8exp8mod9  48973  nfermltl8rev  48979  nnsum3primesprm  49027  nnsum4primesodd  49033  nnsum4primesoddALTV  49034  nnsum4primeseven  49037  nnsum4primesevenALTV  49038  tgblthelfgott  49052  tgoldbach  49054  usgrexmpl1lem  49258  usgrexmpl2lem  49263  usgrexmpl2nb1  49269  usgrexmpl2nb3  49271  usgrexmpl2nb4  49272  usgrexmpl2nb5  49273  usgrexmpl2trifr  49274  gpg3kgrtriexlem3  49322  pgnbgreunbgrlem2lem1  49351  pgnbgreunbgrlem2lem2  49352  rege1logbrege0  49809  rege1logbzge0  49810  blennnelnn  49827  dignnld  49854  nn0sumshdiglemA  49870  nn0sumshdiglem1  49872  rrxlines  49985  eenglngeehlnmlem1  49989  eenglngeehlnmlem2  49990  line2ylem  50002  line2  50003  line2xlem  50004  line2x  50005  icccldii  50172  io1ii  50174  sepfsepc  50181  1ne3  51155  veronesev1lem  51187  veronesev4lem  51190  veronesev5lem  51191  veronesev6lem  51192  veronesevrowd  51193  veronesematrowd  51195  veroquadgsumlem  51197  veroquadmodzerod  51198  veroquadnolindfd  51199