Theorem 1re 11210

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 11164, 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 11175	. . 3 ⊢ 1 ≠ 0
2		ax-1cn 11164	. . . . 5 ⊢ 1 ∈ ℂ
3		cnre 11207	. . . . 5 ⊢ (1 ∈ ℂ → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)))
4	2, 3	ax-mp 5	. . . 4 ⊢ ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏))
5		neeq1 3004	. . . . . . . 8 ⊢ (1 = (𝑎 + (i · 𝑏)) → (1 ≠ 0 ↔ (𝑎 + (i · 𝑏)) ≠ 0))
6	5	biimpcd 248	. . . . . . 7 ⊢ (1 ≠ 0 → (1 = (𝑎 + (i · 𝑏)) → (𝑎 + (i · 𝑏)) ≠ 0))
7		0cn 11202	. . . . . . . 8 ⊢ 0 ∈ ℂ
8		cnre 11207	. . . . . . . 8 ⊢ (0 ∈ ℂ → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)))
9	7, 8	ax-mp 5	. . . . . . 7 ⊢ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑))
10		neeq2 3005	. . . . . . . . . 10 ⊢ (0 = (𝑐 + (i · 𝑑)) → ((𝑎 + (i · 𝑏)) ≠ 0 ↔ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
11	10	biimpcd 248	. . . . . . . . 9 ⊢ ((𝑎 + (i · 𝑏)) ≠ 0 → (0 = (𝑐 + (i · 𝑑)) → (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
12	11	reximdv 3171	. . . . . . . 8 ⊢ ((𝑎 + (i · 𝑏)) ≠ 0 → (∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)) → ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
13	12	reximdv 3171	. . . . . . 7 ⊢ ((𝑎 + (i · 𝑏)) ≠ 0 → (∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)) → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
14	6, 9, 13	syl6mpi 67	. . . . . 6 ⊢ (1 ≠ 0 → (1 = (𝑎 + (i · 𝑏)) → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
15	14	reximdv 3171	. . . . 5 ⊢ (1 ≠ 0 → (∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)) → ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
16	15	reximdv 3171	. . . 4 ⊢ (1 ≠ 0 → (∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)) → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
17	4, 16	mpi 20	. . 3 ⊢ (1 ≠ 0 → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)))
18		ioran 983	. . . . . . . . 9 ⊢ (¬ (𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑) ↔ (¬ 𝑎 ≠ 𝑐 ∧ ¬ 𝑏 ≠ 𝑑))
19		df-ne 2942	. . . . . . . . . . 11 ⊢ (𝑎 ≠ 𝑐 ↔ ¬ 𝑎 = 𝑐)
20	19	con2bii 358	. . . . . . . . . 10 ⊢ (𝑎 = 𝑐 ↔ ¬ 𝑎 ≠ 𝑐)
21		df-ne 2942	. . . . . . . . . . 11 ⊢ (𝑏 ≠ 𝑑 ↔ ¬ 𝑏 = 𝑑)
22	21	con2bii 358	. . . . . . . . . 10 ⊢ (𝑏 = 𝑑 ↔ ¬ 𝑏 ≠ 𝑑)
23	20, 22	anbi12i 628	. . . . . . . . 9 ⊢ ((𝑎 = 𝑐 ∧ 𝑏 = 𝑑) ↔ (¬ 𝑎 ≠ 𝑐 ∧ ¬ 𝑏 ≠ 𝑑))
24	18, 23	bitr4i 278	. . . . . . . 8 ⊢ (¬ (𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑) ↔ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑))
25		id 22	. . . . . . . . 9 ⊢ (𝑎 = 𝑐 → 𝑎 = 𝑐)
26		oveq2 7412	. . . . . . . . 9 ⊢ (𝑏 = 𝑑 → (i · 𝑏) = (i · 𝑑))
27	25, 26	oveqan12d 7423	. . . . . . . 8 ⊢ ((𝑎 = 𝑐 ∧ 𝑏 = 𝑑) → (𝑎 + (i · 𝑏)) = (𝑐 + (i · 𝑑)))
28	24, 27	sylbi 216	. . . . . . 7 ⊢ (¬ (𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑) → (𝑎 + (i · 𝑏)) = (𝑐 + (i · 𝑑)))
29	28	necon1ai 2969	. . . . . 6 ⊢ ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → (𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑))
30		neeq1 3004	. . . . . . . . . 10 ⊢ (𝑥 = 𝑎 → (𝑥 ≠ 𝑦 ↔ 𝑎 ≠ 𝑦))
31		neeq2 3005	. . . . . . . . . 10 ⊢ (𝑦 = 𝑐 → (𝑎 ≠ 𝑦 ↔ 𝑎 ≠ 𝑐))
32	30, 31	rspc2ev 3623	. . . . . . . . 9 ⊢ ((𝑎 ∈ ℝ ∧ 𝑐 ∈ ℝ ∧ 𝑎 ≠ 𝑐) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦)
33	32	3expia 1122	. . . . . . . 8 ⊢ ((𝑎 ∈ ℝ ∧ 𝑐 ∈ ℝ) → (𝑎 ≠ 𝑐 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
34	33	ad2ant2r 746	. . . . . . 7 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → (𝑎 ≠ 𝑐 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
35		neeq1 3004	. . . . . . . . . 10 ⊢ (𝑥 = 𝑏 → (𝑥 ≠ 𝑦 ↔ 𝑏 ≠ 𝑦))
36		neeq2 3005	. . . . . . . . . 10 ⊢ (𝑦 = 𝑑 → (𝑏 ≠ 𝑦 ↔ 𝑏 ≠ 𝑑))
37	35, 36	rspc2ev 3623	. . . . . . . . 9 ⊢ ((𝑏 ∈ ℝ ∧ 𝑑 ∈ ℝ ∧ 𝑏 ≠ 𝑑) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦)
38	37	3expia 1122	. . . . . . . 8 ⊢ ((𝑏 ∈ ℝ ∧ 𝑑 ∈ ℝ) → (𝑏 ≠ 𝑑 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
39	38	ad2ant2l 745	. . . . . . 7 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → (𝑏 ≠ 𝑑 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
40	34, 39	jaod 858	. . . . . 6 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → ((𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
41	29, 40	syl5 34	. . . . 5 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
42	41	rexlimdvva 3212	. . . 4 ⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
43	42	rexlimivv 3200	. . 3 ⊢ (∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦)
44	1, 17, 43	mp2b 10	. 2 ⊢ ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦
45		eqtr3 2759	. . . . . . . . 9 ⊢ ((𝑥 = 0 ∧ 𝑦 = 0) → 𝑥 = 𝑦)
46	45	ex 414	. . . . . . . 8 ⊢ (𝑥 = 0 → (𝑦 = 0 → 𝑥 = 𝑦))
47	46	necon3d 2962	. . . . . . 7 ⊢ (𝑥 = 0 → (𝑥 ≠ 𝑦 → 𝑦 ≠ 0))
48		neeq1 3004	. . . . . . . . 9 ⊢ (𝑧 = 𝑦 → (𝑧 ≠ 0 ↔ 𝑦 ≠ 0))
49	48	rspcev 3612	. . . . . . . 8 ⊢ ((𝑦 ∈ ℝ ∧ 𝑦 ≠ 0) → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)
50	49	expcom 415	. . . . . . 7 ⊢ (𝑦 ≠ 0 → (𝑦 ∈ ℝ → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
51	47, 50	syl6 35	. . . . . 6 ⊢ (𝑥 = 0 → (𝑥 ≠ 𝑦 → (𝑦 ∈ ℝ → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
52	51	com23 86	. . . . 5 ⊢ (𝑥 = 0 → (𝑦 ∈ ℝ → (𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
53	52	adantld 492	. . . 4 ⊢ (𝑥 = 0 → ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
54		neeq1 3004	. . . . . . . 8 ⊢ (𝑧 = 𝑥 → (𝑧 ≠ 0 ↔ 𝑥 ≠ 0))
55	54	rspcev 3612	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)
56	55	expcom 415	. . . . . 6 ⊢ (𝑥 ≠ 0 → (𝑥 ∈ ℝ → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
57	56	adantrd 493	. . . . 5 ⊢ (𝑥 ≠ 0 → ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
58	57	a1dd 50	. . . 4 ⊢ (𝑥 ≠ 0 → ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
59	53, 58	pm2.61ine 3026	. . 3 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
60	59	rexlimivv 3200	. 2 ⊢ (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)
61		ax-rrecex 11178	. . . 4 ⊢ ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → ∃𝑥 ∈ ℝ (𝑧 · 𝑥) = 1)
62		remulcl 11191	. . . . . . 7 ⊢ ((𝑧 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (𝑧 · 𝑥) ∈ ℝ)
63	62	adantlr 714	. . . . . 6 ⊢ (((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) ∧ 𝑥 ∈ ℝ) → (𝑧 · 𝑥) ∈ ℝ)
64		eleq1 2822	. . . . . 6 ⊢ ((𝑧 · 𝑥) = 1 → ((𝑧 · 𝑥) ∈ ℝ ↔ 1 ∈ ℝ))
65	63, 64	syl5ibcom 244	. . . . 5 ⊢ (((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) ∧ 𝑥 ∈ ℝ) → ((𝑧 · 𝑥) = 1 → 1 ∈ ℝ))
66	65	rexlimdva 3156	. . . 4 ⊢ ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → (∃𝑥 ∈ ℝ (𝑧 · 𝑥) = 1 → 1 ∈ ℝ))
67	61, 66	mpd 15	. . 3 ⊢ ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → 1 ∈ ℝ)
68	67	rexlimiva 3148	. 2 ⊢ (∃𝑧 ∈ ℝ 𝑧 ≠ 0 → 1 ∈ ℝ)
69	44, 60, 68	mp2b 10	1 ⊢ 1 ∈ ℝ

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 397   ∨ wo 846   = wceq 1542   ∈ wcel 2107   ≠ wne 2941  ∃wrex 3071  (class class class)co 7404  ℂcc 11104  ℝcr 11105  0cc0 11106  1c1 11107  ici 11108   + caddc 11109   · cmul 11111

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-mulcl 11168  ax-mulrcl 11169  ax-i2m1 11174  ax-1ne0 11175  ax-rrecex 11178  ax-cnre 11179

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-iota 6492  df-fv 6548  df-ov 7407

This theorem is referenced by:  1red  11211  1xr  11269  dedekind  11373  peano2re  11383  mul02lem2  11387  addrid  11390  renegcl  11519  peano2rem  11523  0reALT  11553  0lt1  11732  0le1  11733  relin01  11734  1le1  11838  eqneg  11930  ltp1  12050  ltm1  12052  recgt0  12056  mulgt1  12069  ltmulgt11  12070  lemulge11  12072  reclt1  12105  recgt1  12106  recgt1i  12107  recp1lt1  12108  recreclt  12109  recgt0ii  12116  ledivp1i  12135  ltdivp1i  12136  inelr  12198  cju  12204  nnssre  12212  nnge1  12236  nngt1ne1  12237  nnle1eq1  12238  nngt0  12239  nnnlt1  12240  nnne0  12242  nnrecre  12250  nnrecgt0  12251  nnsub  12252  2re  12282  3re  12288  4re  12292  5re  12295  6re  12298  7re  12301  8re  12304  9re  12307  0le2  12310  2pos  12311  3pos  12313  4pos  12315  5pos  12317  6pos  12318  7pos  12319  8pos  12320  9pos  12321  neg1rr  12323  neg1lt0  12325  1lt2  12379  1lt3  12381  1lt4  12384  1lt5  12388  1lt6  12393  1lt7  12399  1lt8  12406  1lt9  12414  1ne2  12416  1le2  12417  1le3  12420  halflt1  12426  addltmul  12444  nnunb  12464  elnnnn0c  12513  nn0ge2m1nn  12537  elnnz1  12584  znnnlt1  12585  zltp1le  12608  zleltp1  12609  nn0lt2  12621  recnz  12633  gtndiv  12635  3halfnz  12637  10re  12692  1lt10  12812  eluzp1m1  12844  eluzp1p1  12846  eluz2b2  12901  zbtwnre  12926  rebtwnz  12927  1rp  12974  divlt1lt  13039  divle1le  13040  nnledivrp  13082  qbtwnxr  13175  xmulrid  13254  xmulm1  13256  x2times  13274  xrub  13287  elicc01  13439  1elunit  13443  divelunit  13467  lincmb01cmp  13468  unitssre  13472  0nelfz1  13516  fzpreddisj  13546  fznatpl1  13551  fztpval  13559  fraclt1  13763  fracle1  13764  flbi2  13778  fldiv4p1lem1div2  13796  fldiv4lem1div2  13798  fldiv  13821  modid  13857  1mod  13864  m1modnnsub1  13878  modm1p1mod0  13883  seqf1olem1  14003  reexpcl  14040  reexpclz  14044  expge0  14060  expge1  14061  expgt1  14062  bernneq  14188  bernneq2  14189  expnbnd  14191  expnlbnd  14192  expnlbnd2  14193  expmulnbnd  14194  discr1  14198  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  14437  lsw0  14511  f1oun2prg  14864  cjexp  15093  re1  15097  im1  15098  rei  15099  imi  15100  01sqrexlem1  15185  01sqrexlem2  15186  01sqrexlem3  15187  01sqrexlem4  15188  01sqrexlem7  15191  resqrex  15193  sqrt1  15214  sqrt2gt1lt2  15217  sqrtm1  15218  abs1  15240  absrdbnd  15284  caubnd2  15300  mulcn2  15536  reccn2  15537  rlimno1  15596  o1fsum  15755  expcnv  15806  geolim  15812  geolim2  15813  georeclim  15814  geomulcvg  15818  geoisumr  15820  geoisum1c  15822  fprodge0  15933  fprodge1  15935  rerisefaccl  15957  refallfaccl  15958  ere  16028  ege2le3  16029  efgt1  16055  resin4p  16077  recos4p  16078  tanhbnd  16100  sinbnd  16119  cosbnd  16120  sinbnd2  16121  cosbnd2  16122  ef01bndlem  16123  sin01bnd  16124  cos01bnd  16125  cos1bnd  16126  cos2bnd  16127  sinltx  16128  sin01gt0  16129  cos01gt0  16130  sin02gt0  16131  sincos1sgn  16132  ene1  16149  rpnnen2lem2  16154  rpnnen2lem3  16155  rpnnen2lem4  16156  rpnnen2lem9  16161  rpnnen2lem12  16164  ruclem6  16174  ruclem11  16179  ruclem12  16180  3dvds  16270  flodddiv4  16352  sadcadd  16395  isprm3  16616  sqnprm  16635  coprm  16644  phibndlem  16699  pythagtriplem3  16747  pcmpt  16821  fldivp1  16826  pockthi  16836  infpn2  16842  resslemOLD  17183  basendxnmulrndx  17236  basendxnmulrndxOLD  17237  starvndxnbasendx  17245  scandxnbasendx  17257  vscandxnbasendx  17262  ipndxnbasendx  17273  basendxnocndx  17324  slotsbhcdif  17356  slotsbhcdifOLD  17357  oppcbasOLD  17660  rescbasOLD  17773  rescabsOLD  17779  odubasOLD  18241  symgvalstructOLD  19258  lt6abl  19755  srgbinomlem4  20043  0ringnnzr  20291  abvneg  20430  abvtrivd  20436  rmodislmodOLD  20529  cnfldfunALTOLD  20943  xrsmcmn  20953  xrsnsgrp  20966  gzrngunitlem  20995  gzrngunit  20996  rge0srg  21001  psgnodpmr  21127  remulg  21144  resubdrg  21145  thlbasOLD  21234  tuslemOLD  23754  setsmsbasOLD  23964  dscmet  24063  dscopn  24064  nrginvrcnlem  24190  idnghm  24242  tgioo  24294  blcvx  24296  iicmp  24384  iiconn  24385  iirev  24427  iihalf1  24429  iihalf2  24431  iihalf2cn  24432  elii1  24433  elii2  24434  iimulcl  24435  icopnfcnv  24440  icopnfhmeo  24441  iccpnfhmeo  24443  xrhmeo  24444  xrhmph  24445  evth  24457  xlebnum  24463  htpycc  24478  reparphti  24495  pcoval1  24511  pco1  24513  pcoval2  24514  pcocn  24515  pcohtpylem  24517  pcopt  24520  pcopt2  24521  pcoass  24522  pcorevlem  24524  nmhmcn  24618  ncvs1  24656  ovolunlem1a  24995  vitalilem2  25108  vitalilem4  25110  vitalilem5  25111  vitali  25112  i1f1  25189  itg11  25190  itg2const  25240  dveflem  25478  dvlipcn  25493  dvcvx  25519  ply1remlem  25662  fta1blem  25668  vieta1lem2  25806  aalioulem3  25829  aalioulem5  25831  aaliou3lem2  25838  ulmbdd  25892  iblulm  25901  radcnvlem1  25907  dvradcnv  25915  abelthlem2  25926  abelthlem3  25927  abelthlem5  25929  abelthlem7  25932  abelth  25935  abelth2  25936  reeff1olem  25940  reeff1o  25941  sinhalfpilem  25955  tangtx  25997  sincos4thpi  26005  pige3ALT  26011  coskpi  26014  cos0pilt1  26023  recosf1o  26026  tanregt0  26030  efif1olem3  26035  efif1olem4  26036  loge  26077  logdivlti  26110  logcnlem4  26135  logf1o2  26140  logtayl  26150  logccv  26153  recxpcl  26165  cxplea  26186  cxpcn3lem  26235  cxpaddlelem  26239  loglesqrt  26246  ang180lem2  26295  angpined  26315  acosrecl  26388  atancj  26395  atanlogaddlem  26398  atantan  26408  atans2  26416  ressatans  26419  leibpi  26427  log2le1  26435  birthdaylem3  26438  cxp2lim  26461  cxploglim  26462  cxploglim2  26463  divsqrtsumlem  26464  cvxcl  26469  scvxcvx  26470  jensenlem2  26472  amgmlem  26474  emcllem2  26481  emcllem4  26483  emcllem6  26485  emcllem7  26486  emre  26490  emgt0  26491  harmonicbnd3  26492  harmonicubnd  26494  harmonicbnd4  26495  zetacvg  26499  ftalem1  26557  ftalem2  26558  ftalem5  26561  issqf  26620  cht1  26649  chp1  26651  ppiltx  26661  mumullem2  26664  ppiublem1  26685  ppiub  26687  chtublem  26694  chtub  26695  logfacbnd3  26706  logexprlim  26708  perfectlem2  26713  dchrinv  26744  dchr1re  26746  efexple  26764  bposlem1  26767  bposlem2  26768  bposlem5  26771  bposlem8  26774  lgsdir2lem1  26808  lgsdir2lem5  26812  lgsdir  26815  lgsne0  26818  lgsabs1  26819  lgsdinn0  26828  gausslemma2dlem0i  26847  lgseisen  26862  m1lgs  26871  2lgslem3  26887  addsq2nreurex  26927  2sqreultblem  26931  2sqreunnltblem  26934  chebbnd1lem3  26954  chebbnd1  26955  chtppilimlem1  26956  chtppilimlem2  26957  chtppilim  26958  chpchtlim  26962  vmadivsumb  26966  rplogsumlem2  26968  rpvmasumlem  26970  dchrmusumlema  26976  dchrmusum2  26977  dchrvmasumlem2  26981  dchrvmasumiflem1  26984  dchrisum0flblem1  26991  dchrisum0flblem2  26992  dchrisum0fno1  26994  rpvmasum2  26995  dchrisum0re  26996  dchrisum0lema  26997  dchrisum0lem1b  26998  dchrisum0lem1  26999  dchrisum0lem2a  27000  dchrisum0lem2  27001  logdivsum  27016  mulog2sumlem2  27018  2vmadivsumlem  27023  log2sumbnd  27027  selbergb  27032  selberg2b  27035  chpdifbndlem1  27036  selberg3lem1  27040  selberg3lem2  27041  selberg4lem1  27043  pntrmax  27047  pntrsumo1  27048  selbergsb  27058  pntrlog2bndlem3  27062  pntrlog2bndlem5  27064  pntpbnd1a  27068  pntpbnd2  27070  pntibndlem1  27072  pntibndlem3  27075  pntlemd  27077  pntlemc  27078  pntlemb  27080  pntlemr  27085  pntlemf  27088  pntlemk  27089  pntlemo  27090  pntlem3  27092  pntleml  27094  abvcxp  27098  ostth2lem1  27101  ostth1  27116  ostth2lem2  27117  ostth2lem3  27118  ostth2lem4  27119  ostth2  27120  ostth3  27121  ostth  27122  slotsinbpsd  27672  slotslnbpsd  27673  trgcgrg  27746  brbtwn2  28143  colinearalglem4  28147  ax5seglem2  28167  ax5seglem3  28169  axpaschlem  28178  axpasch  28179  axlowdimlem6  28185  axlowdimlem10  28189  axlowdimlem16  28195  axlowdim1  28197  axlowdim2  28198  axlowdim  28199  axcontlem2  28203  elntg2  28223  lfgrnloop  28365  lfuhgr1v0e  28491  usgrexmpldifpr  28495  usgrexmplef  28496  1loopgrvd2  28740  vdegp1bi  28774  lfgrwlkprop  28924  pthdlem1  29003  pthdlem2  29005  clwlkclwwlkf  29241  upgr4cycl4dv4e  29418  konigsberglem2  29486  konigsberglem3  29487  konigsberglem5  29489  frgrreg  29627  ex-dif  29656  ex-in  29658  ex-pss  29661  ex-res  29674  ex-fl  29680  nv1  29906  smcnlem  29928  ipidsq  29941  nmlno0lem  30024  norm-ii-i  30368  bcs2  30413  norm1  30480  nmopub2tALT  31140  nmfnleub2  31157  nmlnop0iALT  31226  unopbd  31246  nmopadjlem  31320  nmopcoadji  31332  pjnmopi  31379  pjbdlni  31380  hstle1  31457  hstle  31461  hstles  31462  stge1i  31469  stlesi  31472  staddi  31477  stadd3i  31479  strlem1  31481  strlem5  31486  jplem1  31499  cdj1i  31664  addltmulALT  31677  xlt2addrd  31949  pr01ssre  32008  dp2lt10  32028  dp2ltsuc  32030  dp2ltc  32031  dplti  32049  dpmul4  32058  cshw1s2  32102  xrsmulgzz  32157  resvbasOLD  32417  rearchi  32430  xrge0slmod  32432  prmidl0  32527  submateqlem1  32725  xrge0iifcnv  32851  xrge0iifcv  32852  xrge0iifiso  32853  xrge0iifhom  32855  zrhre  32937  indf  32951  indfval  32952  esumcst  32999  cntnevol  33164  omssubadd  33237  iwrdsplit  33324  dstfrvclim1  33414  coinfliprv  33419  ballotlem2  33425  ballotlem4  33435  ballotlemi1  33439  ballotlemic  33443  sgnclre  33476  sgnnbi  33482  sgnpbi  33483  sgnmulsgp  33487  plymulx0  33496  plymulx  33497  signswch  33510  signstf  33515  signsvfn  33531  itgexpif  33556  hgt750lemd  33598  logdivsqrle  33600  hgt750lem  33601  hgt750lem2  33602  hgt750leme  33608  tgoldbachgnn  33609  subfacp1lem1  34108  subfacp1lem5  34113  resconn  34175  iisconn  34181  iillysconn  34182  problem2  34589  problem3  34590  sinccvglem  34595  fz0n  34638  gg-iihalf2cn  35106  gg-reparphti  35110  dnibndlem12  35303  knoppcnlem4  35310  knoppndvlem13  35338  cnndvlem1  35351  irrdiff  36145  relowlpssretop  36183  sin2h  36416  cos2h  36417  tan2h  36418  poimirlem7  36433  poimirlem16  36442  poimirlem17  36443  poimirlem19  36445  poimirlem20  36446  poimirlem22  36448  poimirlem23  36449  poimirlem29  36455  poimirlem31  36457  itg2addnclem3  36479  asindmre  36509  dvasin  36510  dvacos  36511  dvreasin  36512  dvreacos  36513  fdc  36551  geomcau  36565  cntotbnd  36602  heiborlem8  36624  bfplem2  36629  bfp  36630  aks4d1p1p7  40877  2xp3dxp2ge1d  40960  factwoffsmonot  40961  1t1e1ALT  41126  re1m1e0m0  41214  sn-00idlem1  41215  sn-00idlem2  41216  remul02  41222  sn-0ne2  41223  reixi  41239  rei4  41240  remullid  41250  ipiiie0  41254  sn-0tie0  41256  sn-nnne0  41265  mulgt0b2d  41277  sn-0lt1  41279  sn-ltp1  41280  reneg1lt0  41281  sn-inelr  41282  rabren3dioph  41486  pellexlem5  41504  pellexlem6  41505  pell1qrgaplem  41544  pell14qrgap  41546  pellqrex  41550  pellfundre  41552  pellfundlb  41555  pellfund14gap  41558  jm2.17a  41632  acongeq  41655  jm2.23  41668  jm3.1lem2  41690  sqrtcval  42325  sqrtcval2  42326  resqrtval  42327  imsqrtval  42328  relexp01min  42397  mnringbasedOLD  42904  cvgdvgrat  43005  lhe4.4ex1a  43021  binomcxplemnotnn0  43048  isosctrlem1ALT  43628  supxrgelem  43982  xrlexaddrp  43997  infxr  44012  infleinflem2  44016  sumnnodd  44281  limsup10exlem  44423  limsup10ex  44424  dvnprodlem3  44599  stoweidlem1  44652  stoweidlem18  44669  stoweidlem19  44670  stoweidlem26  44677  stoweidlem34  44685  stoweidlem40  44691  stoweidlem41  44692  stoweidlem59  44710  stoweid  44714  stirlinglem10  44734  stirlinglem11  44735  dirkercncflem1  44754  fourierdlem16  44774  fourierdlem21  44779  fourierdlem22  44780  fourierdlem42  44800  fourierdlem68  44825  fourierdlem83  44840  fourierdlem103  44860  sqwvfourb  44880  fouriersw  44882  etransclem23  44908  salgencntex  44994  ovn0lem  45216  smfmullem3  45444  smfmullem4  45445  zm1nn  45945  m1mod0mod1  45972  fmtnosqrt  46142  perfectALTVlem2  46325  2exp340mod341  46336  8exp8mod9  46339  nfermltl8rev  46345  nnsum3primesprm  46393  nnsum4primesodd  46399  nnsum4primesoddALTV  46400  nnsum4primeseven  46403  nnsum4primesevenALTV  46404  tgblthelfgott  46418  tgoldbach  46420  rege1logbrege0  47146  rege1logbzge0  47147  blennnelnn  47164  dignnld  47191  nn0sumshdiglemA  47207  nn0sumshdiglem1  47209  rrx2xpref1o  47306  rrxlines  47321  eenglngeehlnmlem1  47325  eenglngeehlnmlem2  47326  line2ylem  47339  line2x  47342  icccldii  47453  io1ii  47455  sepfsepc  47462