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 2995	. . . . . . . 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 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 7376	. . . . . . . . . . . 12 ⊢ (𝑏 = 𝑑 → (i · 𝑏) = (i · 𝑑))
20	18, 19	oveqan12d 7387	. . . . . . . . . . 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 3591	. . . . . . . . 9 ⊢ ((𝑎 ∈ ℝ ∧ 𝑐 ∈ ℝ ∧ 𝑎 ≠ 𝑐) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦)
29	28	3expia 1122	. . . . . . . 8 ⊢ ((𝑎 ∈ ℝ ∧ 𝑐 ∈ ℝ) → (𝑎 ≠ 𝑐 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
30	29	ad2ant2r 748	. . . . . . 7 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → (𝑎 ≠ 𝑐 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
31		neeq1 2995	. . . . . . . . . 10 ⊢ (𝑥 = 𝑏 → (𝑥 ≠ 𝑦 ↔ 𝑏 ≠ 𝑦))
32		neeq2 2996	. . . . . . . . . 10 ⊢ (𝑦 = 𝑑 → (𝑏 ≠ 𝑦 ↔ 𝑏 ≠ 𝑑))
33	31, 32	rspc2ev 3591	. . . . . . . . 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 3578	. . . . . . . 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 3578	. . . . . . 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 11110	. . . 4 ⊢ ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → ∃𝑥 ∈ ℝ (𝑧 · 𝑥) = 1)
58		remulcl 11123	. . . . . . 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 7368  ℂ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 2709  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 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-iota 6456  df-fv 6508  df-ov 7371

This theorem is referenced by:  1red  11145  1xr  11203  dedekind  11308  peano2re  11318  mul02lem2  11322  addrid  11325  renegcl  11456  peano2rem  11460  0reALT  11490  0lt1  11671  0le1  11672  relin01  11673  1le1  11777  eqneg  11873  ltp1  11993  ltm1  11995  recgt0  11999  mulgt1OLD  12012  ltmulgt11  12013  lemulge11  12016  reclt1  12049  recgt1  12050  recgt1i  12051  recp1lt1  12052  recreclt  12053  recgt0ii  12060  ledivp1i  12079  ltdivp1i  12080  neg1rr  12143  neg1lt0  12145  cju  12153  nnssre  12161  nnge1  12185  nngt1ne1  12186  nnle1eq1  12187  nngt0  12188  nnnlt1  12189  nnne0  12191  nnrecre  12199  nnrecgt0  12200  nnsub  12201  2re  12231  3re  12237  4re  12241  5re  12244  6re  12247  7re  12250  8re  12253  9re  12256  0le2  12259  2pos  12260  3pos  12262  4pos  12264  5pos  12266  6pos  12267  7pos  12268  8pos  12269  9pos  12270  1lt2  12323  1lt3  12325  1lt4  12328  1lt5  12332  1lt6  12337  1lt7  12343  1lt8  12350  1lt9  12358  1ne2  12360  1le2  12361  1le3  12364  halflt1  12370  addltmul  12389  nnunb  12409  elnnnn0c  12458  nn0ge2m1nn  12483  elnnz1  12529  znnnlt1  12530  zltp1le  12553  zleltp1  12554  nn0lt2  12567  recnz  12579  gtndiv  12581  3halfnz  12583  10re  12638  1lt10  12758  eluzp1m1  12789  eluzp1p1  12791  eluz2b2  12846  zbtwnre  12871  rebtwnz  12872  1rp  12921  divlt1lt  12988  divle1le  12989  nnledivrp  13031  qbtwnxr  13127  xmulrid  13206  xmulm1  13208  x2times  13226  xrub  13239  elicc01  13394  1elunit  13398  divelunit  13422  lincmb01cmp  13423  unitssre  13427  0nelfz1  13471  fzpreddisj  13501  fznatpl1  13506  fztpval  13514  fraclt1  13734  fracle1  13735  flbi2  13749  fldiv4p1lem1div2  13767  fldiv4lem1div2  13769  fldiv  13792  modid  13828  1mod  13835  m1modnnsub1  13852  modm1p1mod0  13857  seqf1olem1  13976  reexpcl  14013  reexpclz  14017  expge0  14033  expge1  14034  expgt1  14035  bernneq  14164  bernneq2  14165  expnbnd  14167  expnlbnd  14168  expnlbnd2  14169  expmulnbnd  14170  discr1  14174  facwordi  14224  faclbnd3  14227  faclbnd4lem1  14228  faclbnd4lem4  14231  faclbnd6  14234  facavg  14236  hashv01gt1  14280  hashnn0n0nn  14326  hashunsnggt  14329  hash1snb  14354  hashgt12el  14357  hashgt12el2  14358  hashfun  14372  hashge2el2dif  14415  tpf1ofv2  14433  lsw0  14500  f1oun2prg  14852  cjexp  15085  re1  15089  im1  15090  rei  15091  imi  15092  01sqrexlem1  15177  01sqrexlem2  15178  01sqrexlem3  15179  01sqrexlem4  15180  01sqrexlem7  15183  resqrex  15185  sqrt1  15206  sqrt2gt1lt2  15209  sqrtm1  15210  abs1  15232  absrdbnd  15277  caubnd2  15293  mulcn2  15531  reccn2  15532  rlimno1  15589  o1fsum  15748  expcnv  15799  geolim  15805  geolim2  15806  georeclim  15807  geomulcvg  15811  geoisumr  15813  geoisum1c  15815  fprodge0  15928  fprodge1  15930  rerisefaccl  15952  refallfaccl  15953  ere  16024  ege2le3  16025  efgt1  16053  resin4p  16075  recos4p  16076  tanhbnd  16098  sinbnd  16117  cosbnd  16118  sinbnd2  16119  cosbnd2  16120  ef01bndlem  16121  sin01bnd  16122  cos01bnd  16123  cos1bnd  16124  cos2bnd  16125  sinltx  16126  sin01gt0  16127  cos01gt0  16128  sin02gt0  16129  sincos1sgn  16130  ene1  16147  rpnnen2lem2  16152  rpnnen2lem3  16153  rpnnen2lem4  16154  rpnnen2lem9  16159  rpnnen2lem12  16162  ruclem6  16172  ruclem11  16177  ruclem12  16178  3dvds  16270  flodddiv4  16354  sadcadd  16397  isprm3  16622  sqnprm  16641  coprm  16650  phibndlem  16709  pythagtriplem3  16758  pcmpt  16832  fldivp1  16837  pockthi  16847  infpn2  16853  basendxnmulrndx  17228  starvndxnbasendx  17236  scandxnbasendx  17248  vscandxnbasendx  17253  ipndxnbasendx  17264  basendxnocndx  17315  slotsbhcdif  17347  lt6abl  19836  srgbinomlem4  20176  0ringnnzr  20470  abvneg  20771  abvtrivd  20777  xrsmcmn  21358  xrsnsgrp  21374  gzrngunitlem  21399  gzrngunit  21400  rge0srg  21405  psgnodpmr  21557  remulg  21574  resubdrg  21575  psdmvr  22124  dscmet  24528  dscopn  24529  nrginvrcnlem  24647  idnghm  24699  tgioo  24752  blcvx  24754  iicmp  24847  iiconn  24848  iirev  24891  iihalf1  24893  iihalf2  24896  iihalf2cnOLD  24898  elii1  24899  elii2  24900  iimulcl  24901  icopnfcnv  24908  icopnfhmeo  24909  iccpnfhmeo  24911  xrhmeo  24912  xrhmph  24913  evth  24926  xlebnum  24932  htpycc  24947  reparphti  24964  reparphtiOLD  24965  pcoval1  24981  pco1  24983  pcoval2  24984  pcocn  24985  pcohtpylem  24987  pcopt  24990  pcopt2  24991  pcoass  24992  pcorevlem  24994  nmhmcn  25088  ncvs1  25125  ovolunlem1a  25465  vitalilem2  25578  vitalilem4  25580  vitalilem5  25581  vitali  25582  i1f1  25659  itg11  25660  itg2const  25709  dveflem  25951  dvlipcn  25967  dvcvx  25993  ply1remlem  26138  fta1blem  26144  vieta1lem2  26287  aalioulem3  26310  aalioulem5  26312  aaliou3lem2  26319  ulmbdd  26375  iblulm  26384  radcnvlem1  26390  dvradcnv  26398  abelthlem2  26410  abelthlem3  26411  abelthlem5  26413  abelthlem7  26416  abelth  26419  abelth2  26420  reeff1olem  26424  reeff1o  26425  sinhalfpilem  26440  tangtx  26482  sincos4thpi  26490  pige3ALT  26497  coskpi  26500  cos0pilt1  26509  recosf1o  26512  tanregt0  26516  efif1olem3  26521  efif1olem4  26522  loge  26563  logdivlti  26597  logcnlem4  26622  logf1o2  26627  logtayl  26637  logccv  26640  recxpcl  26652  cxplea  26673  cxpcn3lem  26725  cxpaddlelem  26729  loglesqrt  26739  ang180lem2  26788  angpined  26808  acosrecl  26881  atancj  26888  atanlogaddlem  26891  atantan  26901  atans2  26909  ressatans  26912  leibpi  26920  log2le1  26928  birthdaylem3  26931  cxp2lim  26955  cxploglim  26956  cxploglim2  26957  divsqrtsumlem  26958  cvxcl  26963  scvxcvx  26964  jensenlem2  26966  amgmlem  26968  emcllem2  26975  emcllem4  26977  emcllem6  26979  emcllem7  26980  emre  26984  emgt0  26985  harmonicbnd3  26986  harmonicubnd  26988  harmonicbnd4  26989  zetacvg  26993  ftalem1  27051  ftalem2  27052  ftalem5  27055  issqf  27114  cht1  27143  chp1  27145  ppiltx  27155  mumullem2  27158  ppiublem1  27181  ppiub  27183  chtublem  27190  chtub  27191  logfacbnd3  27202  logexprlim  27204  perfectlem2  27209  dchrinv  27240  dchr1re  27242  efexple  27260  bposlem1  27263  bposlem2  27264  bposlem5  27267  bposlem8  27270  lgsdir2lem1  27304  lgsdir2lem5  27308  lgsdir  27311  lgsne0  27314  lgsabs1  27315  lgsdinn0  27324  gausslemma2dlem0i  27343  lgseisen  27358  m1lgs  27367  2lgslem3  27383  addsq2nreurex  27423  2sqreultblem  27427  2sqreunnltblem  27430  chebbnd1lem3  27450  chebbnd1  27451  chtppilimlem1  27452  chtppilimlem2  27453  chtppilim  27454  chpchtlim  27458  vmadivsumb  27462  rplogsumlem2  27464  rpvmasumlem  27466  dchrmusumlema  27472  dchrmusum2  27473  dchrvmasumlem2  27477  dchrvmasumiflem1  27480  dchrisum0flblem1  27487  dchrisum0flblem2  27488  dchrisum0fno1  27490  rpvmasum2  27491  dchrisum0re  27492  dchrisum0lema  27493  dchrisum0lem1b  27494  dchrisum0lem1  27495  dchrisum0lem2a  27496  dchrisum0lem2  27497  logdivsum  27512  mulog2sumlem2  27514  2vmadivsumlem  27519  log2sumbnd  27523  selbergb  27528  selberg2b  27531  chpdifbndlem1  27532  selberg3lem1  27536  selberg3lem2  27537  selberg4lem1  27539  pntrmax  27543  pntrsumo1  27544  selbergsb  27554  pntrlog2bndlem3  27558  pntrlog2bndlem5  27560  pntpbnd1a  27564  pntpbnd2  27566  pntibndlem1  27568  pntibndlem3  27571  pntlemd  27573  pntlemc  27574  pntlemb  27576  pntlemr  27581  pntlemf  27584  pntlemk  27585  pntlemo  27586  pntlem3  27588  pntleml  27590  abvcxp  27594  ostth2lem1  27597  ostth1  27612  ostth2lem2  27613  ostth2lem3  27614  ostth2lem4  27615  ostth2  27616  ostth3  27617  ostth  27618  slotsinbpsd  28525  slotslnbpsd  28526  trgcgrg  28599  brbtwn2  28990  colinearalglem4  28994  ax5seglem2  29014  ax5seglem3  29016  axpaschlem  29025  axpasch  29026  axlowdimlem6  29032  axlowdimlem10  29036  axlowdimlem16  29042  axlowdim1  29044  axlowdim2  29045  axlowdim  29046  axcontlem2  29050  elntg2  29070  lfgrnloop  29210  lfuhgr1v0e  29339  usgrexmpldifpr  29343  usgrexmplef  29344  1loopgrvd2  29589  vdegp1bi  29623  lfgrwlkprop  29771  pthdlem1  29851  pthdlem2  29853  clwlkclwwlkf  30095  upgr4cycl4dv4e  30272  konigsberglem2  30340  konigsberglem3  30341  konigsberglem5  30343  frgrreg  30481  ex-dif  30510  ex-in  30512  ex-pss  30515  ex-res  30528  ex-fl  30534  nv1  30763  smcnlem  30785  ipidsq  30798  nmlno0lem  30881  norm-ii-i  31225  bcs2  31270  norm1  31337  nmopub2tALT  31997  nmfnleub2  32014  nmlnop0iALT  32083  unopbd  32103  nmopadjlem  32177  nmopcoadji  32189  pjnmopi  32236  pjbdlni  32237  hstle1  32314  hstle  32318  hstles  32319  stge1i  32326  stlesi  32329  staddi  32334  stadd3i  32336  strlem1  32338  strlem5  32343  jplem1  32356  cdj1i  32521  addltmulALT  32534  xlt2addrd  32850  pr01ssre  32916  sgnclre  32924  sgnnbi  32930  sgnpbi  32931  sgnmulsgp  32935  indf  32945  indfval  32946  dp2lt10  32976  dp2ltsuc  32978  dp2ltc  32979  dplti  32997  dpmul4  33006  cshw1s2  33053  xrsmulgzz  33102  rearchi  33439  xrge0slmod  33441  prmidl0  33543  evl1deg3  33671  constrconj  33923  2sqr3minply  33958  submateqlem1  33985  xrge0iifcnv  34111  xrge0iifcv  34112  xrge0iifiso  34113  xrge0iifhom  34115  zrhre  34197  esumcst  34241  cntnevol  34406  omssubadd  34478  iwrdsplit  34565  dstfrvclim1  34656  coinfliprv  34661  ballotlem2  34667  ballotlem4  34677  ballotlemi1  34681  ballotlemic  34685  plymulx0  34725  plymulx  34726  signswch  34739  signstf  34744  signsvfn  34760  itgexpif  34784  hgt750lemd  34826  logdivsqrle  34828  hgt750lem  34829  hgt750lem2  34830  hgt750leme  34836  tgoldbachgnn  34837  subfacp1lem1  35395  subfacp1lem5  35400  resconn  35462  iisconn  35468  iillysconn  35469  problem2  35882  problem3  35883  sinccvglem  35888  fz0n  35947  dnibndlem12  36711  knoppcnlem4  36718  knoppndvlem13  36746  cnndvlem1  36759  irrdiff  37581  relowlpssretop  37619  sin2h  37861  cos2h  37862  tan2h  37863  poimirlem7  37878  poimirlem16  37887  poimirlem17  37888  poimirlem19  37890  poimirlem20  37891  poimirlem22  37893  poimirlem23  37894  poimirlem29  37900  poimirlem31  37902  itg2addnclem3  37924  asindmre  37954  dvasin  37955  dvacos  37956  dvreasin  37957  dvreacos  37958  fdc  37996  geomcau  38010  cntotbnd  38047  heiborlem8  38069  bfplem2  38074  bfp  38075  aks4d1p1p7  42444  1t1e1ALT  42625  ine1  42684  re1m1e0m0  42767  sn-00idlem1  42768  sn-00idlem2  42769  remul02  42775  sn-0ne2  42776  reixi  42793  rei4  42794  remullid  42804  ipiiie0  42808  sn-0tie0  42821  sn-nnne0  42830  mulgt0b1d  42842  sn-0lt1  42845  sn-ltp1  42846  reneg1lt0  42850  sn-inelr  42857  rabren3dioph  43172  pellexlem5  43190  pellexlem6  43191  pell1qrgaplem  43230  pell14qrgap  43232  pellqrex  43236  pellfundre  43238  pellfundlb  43241  pellfund14gap  43244  jm2.17a  43317  acongeq  43340  jm2.23  43353  jm3.1lem2  43375  sqrtcval  43997  sqrtcval2  43998  resqrtval  43999  imsqrtval  44000  relexp01min  44069  cvgdvgrat  44669  lhe4.4ex1a  44685  binomcxplemnotnn0  44712  isosctrlem1ALT  45289  supxrgelem  45696  xrlexaddrp  45711  infxr  45725  infleinflem2  45729  sumnnodd  45990  limsup10exlem  46130  limsup10ex  46131  dvnprodlem3  46306  stoweidlem1  46359  stoweidlem18  46376  stoweidlem19  46377  stoweidlem26  46384  stoweidlem34  46392  stoweidlem40  46398  stoweidlem41  46399  stoweidlem59  46417  stoweid  46421  stirlinglem10  46441  stirlinglem11  46442  dirkercncflem1  46461  fourierdlem16  46481  fourierdlem21  46486  fourierdlem22  46487  fourierdlem42  46507  fourierdlem68  46532  fourierdlem83  46547  fourierdlem103  46567  sqwvfourb  46587  fouriersw  46589  etransclem23  46615  salgencntex  46701  ovn0lem  46923  smfmullem3  47151  smfmullem4  47152  nthrucw  47244  cjnpoly  47249  zm1nn  47662  ceilhalf1  47694  m1mod0mod1  47714  fmtnosqrt  47899  perfectALTVlem2  48082  2exp340mod341  48093  8exp8mod9  48096  nfermltl8rev  48102  nnsum3primesprm  48150  nnsum4primesodd  48156  nnsum4primesoddALTV  48157  nnsum4primeseven  48160  nnsum4primesevenALTV  48161  tgblthelfgott  48175  tgoldbach  48177  usgrexmpl1lem  48381  usgrexmpl2lem  48386  usgrexmpl2nb1  48392  usgrexmpl2nb3  48394  usgrexmpl2nb4  48395  usgrexmpl2nb5  48396  usgrexmpl2trifr  48397  gpg3kgrtriexlem3  48445  pgnbgreunbgrlem2lem1  48474  pgnbgreunbgrlem2lem2  48475  rege1logbrege0  48918  rege1logbzge0  48919  blennnelnn  48936  dignnld  48963  nn0sumshdiglemA  48979  nn0sumshdiglem1  48981  rrx2xpref1o  49078  rrxlines  49093  eenglngeehlnmlem1  49097  eenglngeehlnmlem2  49098  line2ylem  49111  line2x  49114  icccldii  49278  io1ii  49280  sepfsepc  49287