Theorem 1re 11290

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 11242, 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 11253	. . 3 ⊢ 1 ≠ 0
2		ax-1cn 11242	. . . . 5 ⊢ 1 ∈ ℂ
3		cnre 11287	. . . . 5 ⊢ (1 ∈ ℂ → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)))
4	2, 3	ax-mp 5	. . . 4 ⊢ ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏))
5		neeq1 3009	. . . . . . . 8 ⊢ (1 = (𝑎 + (i · 𝑏)) → (1 ≠ 0 ↔ (𝑎 + (i · 𝑏)) ≠ 0))
6	5	biimpcd 249	. . . . . . 7 ⊢ (1 ≠ 0 → (1 = (𝑎 + (i · 𝑏)) → (𝑎 + (i · 𝑏)) ≠ 0))
7		0cn 11282	. . . . . . . 8 ⊢ 0 ∈ ℂ
8		cnre 11287	. . . . . . . 8 ⊢ (0 ∈ ℂ → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)))
9	7, 8	ax-mp 5	. . . . . . 7 ⊢ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑))
10		neeq2 3010	. . . . . . . . . 10 ⊢ (0 = (𝑐 + (i · 𝑑)) → ((𝑎 + (i · 𝑏)) ≠ 0 ↔ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
11	10	biimpcd 249	. . . . . . . . 9 ⊢ ((𝑎 + (i · 𝑏)) ≠ 0 → (0 = (𝑐 + (i · 𝑑)) → (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
12	11	reximdv 3176	. . . . . . . 8 ⊢ ((𝑎 + (i · 𝑏)) ≠ 0 → (∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)) → ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
13	12	reximdv 3176	. . . . . . 7 ⊢ ((𝑎 + (i · 𝑏)) ≠ 0 → (∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)) → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
14	6, 9, 13	syl6mpi 67	. . . . . 6 ⊢ (1 ≠ 0 → (1 = (𝑎 + (i · 𝑏)) → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
15	14	reximdv 3176	. . . . 5 ⊢ (1 ≠ 0 → (∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)) → ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
16	15	reximdv 3176	. . . 4 ⊢ (1 ≠ 0 → (∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)) → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
17	4, 16	mpi 20	. . 3 ⊢ (1 ≠ 0 → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)))
18		ioran 984	. . . . . . . . 9 ⊢ (¬ (𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑) ↔ (¬ 𝑎 ≠ 𝑐 ∧ ¬ 𝑏 ≠ 𝑑))
19		df-ne 2947	. . . . . . . . . . 11 ⊢ (𝑎 ≠ 𝑐 ↔ ¬ 𝑎 = 𝑐)
20	19	con2bii 357	. . . . . . . . . 10 ⊢ (𝑎 = 𝑐 ↔ ¬ 𝑎 ≠ 𝑐)
21		df-ne 2947	. . . . . . . . . . 11 ⊢ (𝑏 ≠ 𝑑 ↔ ¬ 𝑏 = 𝑑)
22	21	con2bii 357	. . . . . . . . . 10 ⊢ (𝑏 = 𝑑 ↔ ¬ 𝑏 ≠ 𝑑)
23	20, 22	anbi12i 627	. . . . . . . . 9 ⊢ ((𝑎 = 𝑐 ∧ 𝑏 = 𝑑) ↔ (¬ 𝑎 ≠ 𝑐 ∧ ¬ 𝑏 ≠ 𝑑))
24	18, 23	bitr4i 278	. . . . . . . 8 ⊢ (¬ (𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑) ↔ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑))
25		id 22	. . . . . . . . 9 ⊢ (𝑎 = 𝑐 → 𝑎 = 𝑐)
26		oveq2 7456	. . . . . . . . 9 ⊢ (𝑏 = 𝑑 → (i · 𝑏) = (i · 𝑑))
27	25, 26	oveqan12d 7467	. . . . . . . 8 ⊢ ((𝑎 = 𝑐 ∧ 𝑏 = 𝑑) → (𝑎 + (i · 𝑏)) = (𝑐 + (i · 𝑑)))
28	24, 27	sylbi 217	. . . . . . 7 ⊢ (¬ (𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑) → (𝑎 + (i · 𝑏)) = (𝑐 + (i · 𝑑)))
29	28	necon1ai 2974	. . . . . 6 ⊢ ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → (𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑))
30		neeq1 3009	. . . . . . . . . 10 ⊢ (𝑥 = 𝑎 → (𝑥 ≠ 𝑦 ↔ 𝑎 ≠ 𝑦))
31		neeq2 3010	. . . . . . . . . 10 ⊢ (𝑦 = 𝑐 → (𝑎 ≠ 𝑦 ↔ 𝑎 ≠ 𝑐))
32	30, 31	rspc2ev 3648	. . . . . . . . 9 ⊢ ((𝑎 ∈ ℝ ∧ 𝑐 ∈ ℝ ∧ 𝑎 ≠ 𝑐) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦)
33	32	3expia 1121	. . . . . . . 8 ⊢ ((𝑎 ∈ ℝ ∧ 𝑐 ∈ ℝ) → (𝑎 ≠ 𝑐 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
34	33	ad2ant2r 746	. . . . . . 7 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → (𝑎 ≠ 𝑐 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
35		neeq1 3009	. . . . . . . . . 10 ⊢ (𝑥 = 𝑏 → (𝑥 ≠ 𝑦 ↔ 𝑏 ≠ 𝑦))
36		neeq2 3010	. . . . . . . . . 10 ⊢ (𝑦 = 𝑑 → (𝑏 ≠ 𝑦 ↔ 𝑏 ≠ 𝑑))
37	35, 36	rspc2ev 3648	. . . . . . . . 9 ⊢ ((𝑏 ∈ ℝ ∧ 𝑑 ∈ ℝ ∧ 𝑏 ≠ 𝑑) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦)
38	37	3expia 1121	. . . . . . . 8 ⊢ ((𝑏 ∈ ℝ ∧ 𝑑 ∈ ℝ) → (𝑏 ≠ 𝑑 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
39	38	ad2ant2l 745	. . . . . . 7 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → (𝑏 ≠ 𝑑 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
40	34, 39	jaod 858	. . . . . 6 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → ((𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
41	29, 40	syl5 34	. . . . 5 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
42	41	rexlimdvva 3219	. . . 4 ⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
43	42	rexlimivv 3207	. . 3 ⊢ (∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦)
44	1, 17, 43	mp2b 10	. 2 ⊢ ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦
45		eqtr3 2766	. . . . . . . . 9 ⊢ ((𝑥 = 0 ∧ 𝑦 = 0) → 𝑥 = 𝑦)
46	45	ex 412	. . . . . . . 8 ⊢ (𝑥 = 0 → (𝑦 = 0 → 𝑥 = 𝑦))
47	46	necon3d 2967	. . . . . . 7 ⊢ (𝑥 = 0 → (𝑥 ≠ 𝑦 → 𝑦 ≠ 0))
48		neeq1 3009	. . . . . . . . 9 ⊢ (𝑧 = 𝑦 → (𝑧 ≠ 0 ↔ 𝑦 ≠ 0))
49	48	rspcev 3635	. . . . . . . 8 ⊢ ((𝑦 ∈ ℝ ∧ 𝑦 ≠ 0) → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)
50	49	expcom 413	. . . . . . 7 ⊢ (𝑦 ≠ 0 → (𝑦 ∈ ℝ → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
51	47, 50	syl6 35	. . . . . 6 ⊢ (𝑥 = 0 → (𝑥 ≠ 𝑦 → (𝑦 ∈ ℝ → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
52	51	com23 86	. . . . 5 ⊢ (𝑥 = 0 → (𝑦 ∈ ℝ → (𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
53	52	adantld 490	. . . 4 ⊢ (𝑥 = 0 → ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
54		neeq1 3009	. . . . . . . 8 ⊢ (𝑧 = 𝑥 → (𝑧 ≠ 0 ↔ 𝑥 ≠ 0))
55	54	rspcev 3635	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)
56	55	expcom 413	. . . . . 6 ⊢ (𝑥 ≠ 0 → (𝑥 ∈ ℝ → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
57	56	adantrd 491	. . . . 5 ⊢ (𝑥 ≠ 0 → ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
58	57	a1dd 50	. . . 4 ⊢ (𝑥 ≠ 0 → ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
59	53, 58	pm2.61ine 3031	. . 3 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
60	59	rexlimivv 3207	. 2 ⊢ (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)
61		ax-rrecex 11256	. . . 4 ⊢ ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → ∃𝑥 ∈ ℝ (𝑧 · 𝑥) = 1)
62		remulcl 11269	. . . . . . 7 ⊢ ((𝑧 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (𝑧 · 𝑥) ∈ ℝ)
63	62	adantlr 714	. . . . . 6 ⊢ (((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) ∧ 𝑥 ∈ ℝ) → (𝑧 · 𝑥) ∈ ℝ)
64		eleq1 2832	. . . . . 6 ⊢ ((𝑧 · 𝑥) = 1 → ((𝑧 · 𝑥) ∈ ℝ ↔ 1 ∈ ℝ))
65	63, 64	syl5ibcom 245	. . . . 5 ⊢ (((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) ∧ 𝑥 ∈ ℝ) → ((𝑧 · 𝑥) = 1 → 1 ∈ ℝ))
66	65	rexlimdva 3161	. . . 4 ⊢ ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → (∃𝑥 ∈ ℝ (𝑧 · 𝑥) = 1 → 1 ∈ ℝ))
67	61, 66	mpd 15	. . 3 ⊢ ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → 1 ∈ ℝ)
68	67	rexlimiva 3153	. 2 ⊢ (∃𝑧 ∈ ℝ 𝑧 ≠ 0 → 1 ∈ ℝ)
69	44, 60, 68	mp2b 10	1 ⊢ 1 ∈ ℝ

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∨ wo 846   = wceq 1537   ∈ wcel 2108   ≠ wne 2946  ∃wrex 3076  (class class class)co 7448  ℂcc 11182  ℝcr 11183  0cc0 11184  1c1 11185  ici 11186   + caddc 11187   · cmul 11189

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-1cn 11242  ax-icn 11243  ax-addcl 11244  ax-mulcl 11246  ax-mulrcl 11247  ax-i2m1 11252  ax-1ne0 11253  ax-rrecex 11256  ax-cnre 11257

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ne 2947  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-iota 6525  df-fv 6581  df-ov 7451

This theorem is referenced by:  1red  11291  1xr  11349  dedekind  11453  peano2re  11463  mul02lem2  11467  addrid  11470  renegcl  11599  peano2rem  11603  0reALT  11633  0lt1  11812  0le1  11813  relin01  11814  1le1  11918  eqneg  12014  ltp1  12134  ltm1  12136  recgt0  12140  mulgt1OLD  12153  ltmulgt11  12154  lemulge11  12157  reclt1  12190  recgt1  12191  recgt1i  12192  recp1lt1  12193  recreclt  12194  recgt0ii  12201  ledivp1i  12220  ltdivp1i  12221  inelr  12283  cju  12289  nnssre  12297  nnge1  12321  nngt1ne1  12322  nnle1eq1  12323  nngt0  12324  nnnlt1  12325  nnne0  12327  nnrecre  12335  nnrecgt0  12336  nnsub  12337  2re  12367  3re  12373  4re  12377  5re  12380  6re  12383  7re  12386  8re  12389  9re  12392  0le2  12395  2pos  12396  3pos  12398  4pos  12400  5pos  12402  6pos  12403  7pos  12404  8pos  12405  9pos  12406  neg1rr  12408  neg1lt0  12410  1lt2  12464  1lt3  12466  1lt4  12469  1lt5  12473  1lt6  12478  1lt7  12484  1lt8  12491  1lt9  12499  1ne2  12501  1le2  12502  1le3  12505  halflt1  12511  addltmul  12529  nnunb  12549  elnnnn0c  12598  nn0ge2m1nn  12622  elnnz1  12669  znnnlt1  12670  zltp1le  12693  zleltp1  12694  nn0lt2  12706  recnz  12718  gtndiv  12720  3halfnz  12722  10re  12777  1lt10  12897  eluzp1m1  12929  eluzp1p1  12931  eluz2b2  12986  zbtwnre  13011  rebtwnz  13012  1rp  13061  divlt1lt  13126  divle1le  13127  nnledivrp  13169  qbtwnxr  13262  xmulrid  13341  xmulm1  13343  x2times  13361  xrub  13374  elicc01  13526  1elunit  13530  divelunit  13554  lincmb01cmp  13555  unitssre  13559  0nelfz1  13603  fzpreddisj  13633  fznatpl1  13638  fztpval  13646  fraclt1  13853  fracle1  13854  flbi2  13868  fldiv4p1lem1div2  13886  fldiv4lem1div2  13888  fldiv  13911  modid  13947  1mod  13954  m1modnnsub1  13968  modm1p1mod0  13973  seqf1olem1  14092  reexpcl  14129  reexpclz  14133  expge0  14149  expge1  14150  expgt1  14151  bernneq  14278  bernneq2  14279  expnbnd  14281  expnlbnd  14282  expnlbnd2  14283  expmulnbnd  14284  discr1  14288  facwordi  14338  faclbnd3  14341  faclbnd4lem1  14342  faclbnd4lem4  14345  faclbnd6  14348  facavg  14350  hashv01gt1  14394  hashnn0n0nn  14440  hashunsnggt  14443  hash1snb  14468  hashgt12el  14471  hashgt12el2  14472  hashfun  14486  hashge2el2dif  14529  tpf1ofv2  14547  lsw0  14613  f1oun2prg  14966  cjexp  15199  re1  15203  im1  15204  rei  15205  imi  15206  01sqrexlem1  15291  01sqrexlem2  15292  01sqrexlem3  15293  01sqrexlem4  15294  01sqrexlem7  15297  resqrex  15299  sqrt1  15320  sqrt2gt1lt2  15323  sqrtm1  15324  abs1  15346  absrdbnd  15390  caubnd2  15406  mulcn2  15642  reccn2  15643  rlimno1  15702  o1fsum  15861  expcnv  15912  geolim  15918  geolim2  15919  georeclim  15920  geomulcvg  15924  geoisumr  15926  geoisum1c  15928  fprodge0  16041  fprodge1  16043  rerisefaccl  16065  refallfaccl  16066  ere  16137  ege2le3  16138  efgt1  16164  resin4p  16186  recos4p  16187  tanhbnd  16209  sinbnd  16228  cosbnd  16229  sinbnd2  16230  cosbnd2  16231  ef01bndlem  16232  sin01bnd  16233  cos01bnd  16234  cos1bnd  16235  cos2bnd  16236  sinltx  16237  sin01gt0  16238  cos01gt0  16239  sin02gt0  16240  sincos1sgn  16241  ene1  16258  rpnnen2lem2  16263  rpnnen2lem3  16264  rpnnen2lem4  16265  rpnnen2lem9  16270  rpnnen2lem12  16273  ruclem6  16283  ruclem11  16288  ruclem12  16289  3dvds  16379  flodddiv4  16461  sadcadd  16504  isprm3  16730  sqnprm  16749  coprm  16758  phibndlem  16817  pythagtriplem3  16865  pcmpt  16939  fldivp1  16944  pockthi  16954  infpn2  16960  resslemOLD  17301  basendxnmulrndx  17354  basendxnmulrndxOLD  17355  starvndxnbasendx  17363  scandxnbasendx  17375  vscandxnbasendx  17380  ipndxnbasendx  17391  basendxnocndx  17442  slotsbhcdif  17474  slotsbhcdifOLD  17475  oppcbasOLD  17778  rescbasOLD  17891  rescabsOLD  17897  odubasOLD  18362  symgvalstructOLD  19439  lt6abl  19937  srgbinomlem4  20256  0ringnnzr  20551  abvneg  20849  abvtrivd  20855  rmodislmodOLD  20951  cnfldfunALTOLDOLD  21416  xrsmcmn  21427  xrsnsgrp  21443  gzrngunitlem  21473  gzrngunit  21474  rge0srg  21479  psgnodpmr  21631  remulg  21648  resubdrg  21649  thlbasOLD  21738  tuslemOLD  24297  setsmsbasOLD  24507  dscmet  24606  dscopn  24607  nrginvrcnlem  24733  idnghm  24785  tgioo  24837  blcvx  24839  iicmp  24931  iiconn  24932  iirev  24975  iihalf1  24977  iihalf2  24980  iihalf2cnOLD  24982  elii1  24983  elii2  24984  iimulcl  24985  icopnfcnv  24992  icopnfhmeo  24993  iccpnfhmeo  24995  xrhmeo  24996  xrhmph  24997  evth  25010  xlebnum  25016  htpycc  25031  reparphti  25048  reparphtiOLD  25049  pcoval1  25065  pco1  25067  pcoval2  25068  pcocn  25069  pcohtpylem  25071  pcopt  25074  pcopt2  25075  pcoass  25076  pcorevlem  25078  nmhmcn  25172  ncvs1  25210  ovolunlem1a  25550  vitalilem2  25663  vitalilem4  25665  vitalilem5  25666  vitali  25667  i1f1  25744  itg11  25745  itg2const  25795  dveflem  26037  dvlipcn  26053  dvcvx  26079  ply1remlem  26224  fta1blem  26230  vieta1lem2  26371  aalioulem3  26394  aalioulem5  26396  aaliou3lem2  26403  ulmbdd  26459  iblulm  26468  radcnvlem1  26474  dvradcnv  26482  abelthlem2  26494  abelthlem3  26495  abelthlem5  26497  abelthlem7  26500  abelth  26503  abelth2  26504  reeff1olem  26508  reeff1o  26509  sinhalfpilem  26523  tangtx  26565  sincos4thpi  26573  pige3ALT  26580  coskpi  26583  cos0pilt1  26592  recosf1o  26595  tanregt0  26599  efif1olem3  26604  efif1olem4  26605  loge  26646  logdivlti  26680  logcnlem4  26705  logf1o2  26710  logtayl  26720  logccv  26723  recxpcl  26735  cxplea  26756  cxpcn3lem  26808  cxpaddlelem  26812  loglesqrt  26822  ang180lem2  26871  angpined  26891  acosrecl  26964  atancj  26971  atanlogaddlem  26974  atantan  26984  atans2  26992  ressatans  26995  leibpi  27003  log2le1  27011  birthdaylem3  27014  cxp2lim  27038  cxploglim  27039  cxploglim2  27040  divsqrtsumlem  27041  cvxcl  27046  scvxcvx  27047  jensenlem2  27049  amgmlem  27051  emcllem2  27058  emcllem4  27060  emcllem6  27062  emcllem7  27063  emre  27067  emgt0  27068  harmonicbnd3  27069  harmonicubnd  27071  harmonicbnd4  27072  zetacvg  27076  ftalem1  27134  ftalem2  27135  ftalem5  27138  issqf  27197  cht1  27226  chp1  27228  ppiltx  27238  mumullem2  27241  ppiublem1  27264  ppiub  27266  chtublem  27273  chtub  27274  logfacbnd3  27285  logexprlim  27287  perfectlem2  27292  dchrinv  27323  dchr1re  27325  efexple  27343  bposlem1  27346  bposlem2  27347  bposlem5  27350  bposlem8  27353  lgsdir2lem1  27387  lgsdir2lem5  27391  lgsdir  27394  lgsne0  27397  lgsabs1  27398  lgsdinn0  27407  gausslemma2dlem0i  27426  lgseisen  27441  m1lgs  27450  2lgslem3  27466  addsq2nreurex  27506  2sqreultblem  27510  2sqreunnltblem  27513  chebbnd1lem3  27533  chebbnd1  27534  chtppilimlem1  27535  chtppilimlem2  27536  chtppilim  27537  chpchtlim  27541  vmadivsumb  27545  rplogsumlem2  27547  rpvmasumlem  27549  dchrmusumlema  27555  dchrmusum2  27556  dchrvmasumlem2  27560  dchrvmasumiflem1  27563  dchrisum0flblem1  27570  dchrisum0flblem2  27571  dchrisum0fno1  27573  rpvmasum2  27574  dchrisum0re  27575  dchrisum0lema  27576  dchrisum0lem1b  27577  dchrisum0lem1  27578  dchrisum0lem2a  27579  dchrisum0lem2  27580  logdivsum  27595  mulog2sumlem2  27597  2vmadivsumlem  27602  log2sumbnd  27606  selbergb  27611  selberg2b  27614  chpdifbndlem1  27615  selberg3lem1  27619  selberg3lem2  27620  selberg4lem1  27622  pntrmax  27626  pntrsumo1  27627  selbergsb  27637  pntrlog2bndlem3  27641  pntrlog2bndlem5  27643  pntpbnd1a  27647  pntpbnd2  27649  pntibndlem1  27651  pntibndlem3  27654  pntlemd  27656  pntlemc  27657  pntlemb  27659  pntlemr  27664  pntlemf  27667  pntlemk  27668  pntlemo  27669  pntlem3  27671  pntleml  27673  abvcxp  27677  ostth2lem1  27680  ostth1  27695  ostth2lem2  27696  ostth2lem3  27697  ostth2lem4  27698  ostth2  27699  ostth3  27700  ostth  27701  slotsinbpsd  28467  slotslnbpsd  28468  trgcgrg  28541  brbtwn2  28938  colinearalglem4  28942  ax5seglem2  28962  ax5seglem3  28964  axpaschlem  28973  axpasch  28974  axlowdimlem6  28980  axlowdimlem10  28984  axlowdimlem16  28990  axlowdim1  28992  axlowdim2  28993  axlowdim  28994  axcontlem2  28998  elntg2  29018  lfgrnloop  29160  lfuhgr1v0e  29289  usgrexmpldifpr  29293  usgrexmplef  29294  1loopgrvd2  29539  vdegp1bi  29573  lfgrwlkprop  29723  pthdlem1  29802  pthdlem2  29804  clwlkclwwlkf  30040  upgr4cycl4dv4e  30217  konigsberglem2  30285  konigsberglem3  30286  konigsberglem5  30288  frgrreg  30426  ex-dif  30455  ex-in  30457  ex-pss  30460  ex-res  30473  ex-fl  30479  nv1  30707  smcnlem  30729  ipidsq  30742  nmlno0lem  30825  norm-ii-i  31169  bcs2  31214  norm1  31281  nmopub2tALT  31941  nmfnleub2  31958  nmlnop0iALT  32027  unopbd  32047  nmopadjlem  32121  nmopcoadji  32133  pjnmopi  32180  pjbdlni  32181  hstle1  32258  hstle  32262  hstles  32263  stge1i  32270  stlesi  32273  staddi  32278  stadd3i  32280  strlem1  32282  strlem5  32287  jplem1  32300  cdj1i  32465  addltmulALT  32478  xlt2addrd  32765  pr01ssre  32828  dp2lt10  32848  dp2ltsuc  32850  dp2ltc  32851  dplti  32869  dpmul4  32878  cshw1s2  32927  xrsmulgzz  32992  resvbasOLD  33325  rearchi  33339  xrge0slmod  33341  prmidl0  33443  evl1deg3  33568  constrconj  33735  2sqr3minply  33738  submateqlem1  33753  xrge0iifcnv  33879  xrge0iifcv  33880  xrge0iifiso  33881  xrge0iifhom  33883  zrhre  33965  indf  33979  indfval  33980  esumcst  34027  cntnevol  34192  omssubadd  34265  iwrdsplit  34352  dstfrvclim1  34442  coinfliprv  34447  ballotlem2  34453  ballotlem4  34463  ballotlemi1  34467  ballotlemic  34471  sgnclre  34504  sgnnbi  34510  sgnpbi  34511  sgnmulsgp  34515  plymulx0  34524  plymulx  34525  signswch  34538  signstf  34543  signsvfn  34559  itgexpif  34583  hgt750lemd  34625  logdivsqrle  34627  hgt750lem  34628  hgt750lem2  34629  hgt750leme  34635  tgoldbachgnn  34636  subfacp1lem1  35147  subfacp1lem5  35152  resconn  35214  iisconn  35220  iillysconn  35221  problem2  35634  problem3  35635  sinccvglem  35640  fz0n  35693  dnibndlem12  36455  knoppcnlem4  36462  knoppndvlem13  36490  cnndvlem1  36503  irrdiff  37292  relowlpssretop  37330  sin2h  37570  cos2h  37571  tan2h  37572  poimirlem7  37587  poimirlem16  37596  poimirlem17  37597  poimirlem19  37599  poimirlem20  37600  poimirlem22  37602  poimirlem23  37603  poimirlem29  37609  poimirlem31  37611  itg2addnclem3  37633  asindmre  37663  dvasin  37664  dvacos  37665  dvreasin  37666  dvreacos  37667  fdc  37705  geomcau  37719  cntotbnd  37756  heiborlem8  37778  bfplem2  37783  bfp  37784  aks4d1p1p7  42031  2xp3dxp2ge1d  42198  factwoffsmonot  42199  1t1e1ALT  42250  ine1  42303  re1m1e0m0  42373  sn-00idlem1  42374  sn-00idlem2  42375  remul02  42381  sn-0ne2  42382  reixi  42398  rei4  42399  remullid  42409  ipiiie0  42413  sn-0tie0  42415  sn-nnne0  42424  mulgt0b2d  42436  sn-0lt1  42439  sn-ltp1  42440  reneg1lt0  42442  sn-inelr  42443  rabren3dioph  42771  pellexlem5  42789  pellexlem6  42790  pell1qrgaplem  42829  pell14qrgap  42831  pellqrex  42835  pellfundre  42837  pellfundlb  42840  pellfund14gap  42843  jm2.17a  42917  acongeq  42940  jm2.23  42953  jm3.1lem2  42975  sqrtcval  43603  sqrtcval2  43604  resqrtval  43605  imsqrtval  43606  relexp01min  43675  mnringbasedOLD  44181  cvgdvgrat  44282  lhe4.4ex1a  44298  binomcxplemnotnn0  44325  isosctrlem1ALT  44905  supxrgelem  45252  xrlexaddrp  45267  infxr  45282  infleinflem2  45286  sumnnodd  45551  limsup10exlem  45693  limsup10ex  45694  dvnprodlem3  45869  stoweidlem1  45922  stoweidlem18  45939  stoweidlem19  45940  stoweidlem26  45947  stoweidlem34  45955  stoweidlem40  45961  stoweidlem41  45962  stoweidlem59  45980  stoweid  45984  stirlinglem10  46004  stirlinglem11  46005  dirkercncflem1  46024  fourierdlem16  46044  fourierdlem21  46049  fourierdlem22  46050  fourierdlem42  46070  fourierdlem68  46095  fourierdlem83  46110  fourierdlem103  46130  sqwvfourb  46150  fouriersw  46152  etransclem23  46178  salgencntex  46264  ovn0lem  46486  smfmullem3  46714  smfmullem4  46715  zm1nn  47217  m1mod0mod1  47243  fmtnosqrt  47413  perfectALTVlem2  47596  2exp340mod341  47607  8exp8mod9  47610  nfermltl8rev  47616  nnsum3primesprm  47664  nnsum4primesodd  47670  nnsum4primesoddALTV  47671  nnsum4primeseven  47674  nnsum4primesevenALTV  47675  tgblthelfgott  47689  tgoldbach  47691  usgrexmpl1lem  47836  usgrexmpl2lem  47841  usgrexmpl2nb1  47847  usgrexmpl2nb3  47849  usgrexmpl2nb4  47850  usgrexmpl2nb5  47851  usgrexmpl2trifr  47852  rege1logbrege0  48292  rege1logbzge0  48293  blennnelnn  48310  dignnld  48337  nn0sumshdiglemA  48353  nn0sumshdiglem1  48355  rrx2xpref1o  48452  rrxlines  48467  eenglngeehlnmlem1  48471  eenglngeehlnmlem2  48472  line2ylem  48485  line2x  48488  icccldii  48598  io1ii  48600  sepfsepc  48607