Theorem 1re 10798

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 10752, 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 10763	. . 3 ⊢ 1 ≠ 0
2		ax-1cn 10752	. . . . 5 ⊢ 1 ∈ ℂ
3		cnre 10795	. . . . 5 ⊢ (1 ∈ ℂ → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)))
4	2, 3	ax-mp 5	. . . 4 ⊢ ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏))
5		neeq1 2994	. . . . . . . 8 ⊢ (1 = (𝑎 + (i · 𝑏)) → (1 ≠ 0 ↔ (𝑎 + (i · 𝑏)) ≠ 0))
6	5	biimpcd 252	. . . . . . 7 ⊢ (1 ≠ 0 → (1 = (𝑎 + (i · 𝑏)) → (𝑎 + (i · 𝑏)) ≠ 0))
7		0cn 10790	. . . . . . . 8 ⊢ 0 ∈ ℂ
8		cnre 10795	. . . . . . . 8 ⊢ (0 ∈ ℂ → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)))
9	7, 8	ax-mp 5	. . . . . . 7 ⊢ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑))
10		neeq2 2995	. . . . . . . . . 10 ⊢ (0 = (𝑐 + (i · 𝑑)) → ((𝑎 + (i · 𝑏)) ≠ 0 ↔ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
11	10	biimpcd 252	. . . . . . . . 9 ⊢ ((𝑎 + (i · 𝑏)) ≠ 0 → (0 = (𝑐 + (i · 𝑑)) → (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
12	11	reximdv 3182	. . . . . . . 8 ⊢ ((𝑎 + (i · 𝑏)) ≠ 0 → (∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)) → ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
13	12	reximdv 3182	. . . . . . 7 ⊢ ((𝑎 + (i · 𝑏)) ≠ 0 → (∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ 0 = (𝑐 + (i · 𝑑)) → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
14	6, 9, 13	syl6mpi 67	. . . . . 6 ⊢ (1 ≠ 0 → (1 = (𝑎 + (i · 𝑏)) → ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
15	14	reximdv 3182	. . . . 5 ⊢ (1 ≠ 0 → (∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)) → ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
16	15	reximdv 3182	. . . 4 ⊢ (1 ≠ 0 → (∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ 1 = (𝑎 + (i · 𝑏)) → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑))))
17	4, 16	mpi 20	. . 3 ⊢ (1 ≠ 0 → ∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)))
18		ioran 984	. . . . . . . . 9 ⊢ (¬ (𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑) ↔ (¬ 𝑎 ≠ 𝑐 ∧ ¬ 𝑏 ≠ 𝑑))
19		df-ne 2933	. . . . . . . . . . 11 ⊢ (𝑎 ≠ 𝑐 ↔ ¬ 𝑎 = 𝑐)
20	19	con2bii 361	. . . . . . . . . 10 ⊢ (𝑎 = 𝑐 ↔ ¬ 𝑎 ≠ 𝑐)
21		df-ne 2933	. . . . . . . . . . 11 ⊢ (𝑏 ≠ 𝑑 ↔ ¬ 𝑏 = 𝑑)
22	21	con2bii 361	. . . . . . . . . 10 ⊢ (𝑏 = 𝑑 ↔ ¬ 𝑏 ≠ 𝑑)
23	20, 22	anbi12i 630	. . . . . . . . 9 ⊢ ((𝑎 = 𝑐 ∧ 𝑏 = 𝑑) ↔ (¬ 𝑎 ≠ 𝑐 ∧ ¬ 𝑏 ≠ 𝑑))
24	18, 23	bitr4i 281	. . . . . . . 8 ⊢ (¬ (𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑) ↔ (𝑎 = 𝑐 ∧ 𝑏 = 𝑑))
25		id 22	. . . . . . . . 9 ⊢ (𝑎 = 𝑐 → 𝑎 = 𝑐)
26		oveq2 7199	. . . . . . . . 9 ⊢ (𝑏 = 𝑑 → (i · 𝑏) = (i · 𝑑))
27	25, 26	oveqan12d 7210	. . . . . . . 8 ⊢ ((𝑎 = 𝑐 ∧ 𝑏 = 𝑑) → (𝑎 + (i · 𝑏)) = (𝑐 + (i · 𝑑)))
28	24, 27	sylbi 220	. . . . . . 7 ⊢ (¬ (𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑) → (𝑎 + (i · 𝑏)) = (𝑐 + (i · 𝑑)))
29	28	necon1ai 2959	. . . . . 6 ⊢ ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → (𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑))
30		neeq1 2994	. . . . . . . . . 10 ⊢ (𝑥 = 𝑎 → (𝑥 ≠ 𝑦 ↔ 𝑎 ≠ 𝑦))
31		neeq2 2995	. . . . . . . . . 10 ⊢ (𝑦 = 𝑐 → (𝑎 ≠ 𝑦 ↔ 𝑎 ≠ 𝑐))
32	30, 31	rspc2ev 3539	. . . . . . . . 9 ⊢ ((𝑎 ∈ ℝ ∧ 𝑐 ∈ ℝ ∧ 𝑎 ≠ 𝑐) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦)
33	32	3expia 1123	. . . . . . . 8 ⊢ ((𝑎 ∈ ℝ ∧ 𝑐 ∈ ℝ) → (𝑎 ≠ 𝑐 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
34	33	ad2ant2r 747	. . . . . . 7 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → (𝑎 ≠ 𝑐 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
35		neeq1 2994	. . . . . . . . . 10 ⊢ (𝑥 = 𝑏 → (𝑥 ≠ 𝑦 ↔ 𝑏 ≠ 𝑦))
36		neeq2 2995	. . . . . . . . . 10 ⊢ (𝑦 = 𝑑 → (𝑏 ≠ 𝑦 ↔ 𝑏 ≠ 𝑑))
37	35, 36	rspc2ev 3539	. . . . . . . . 9 ⊢ ((𝑏 ∈ ℝ ∧ 𝑑 ∈ ℝ ∧ 𝑏 ≠ 𝑑) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦)
38	37	3expia 1123	. . . . . . . 8 ⊢ ((𝑏 ∈ ℝ ∧ 𝑑 ∈ ℝ) → (𝑏 ≠ 𝑑 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
39	38	ad2ant2l 746	. . . . . . 7 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → (𝑏 ≠ 𝑑 → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
40	34, 39	jaod 859	. . . . . 6 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → ((𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
41	29, 40	syl5 34	. . . . 5 ⊢ (((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → ((𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
42	41	rexlimdvva 3203	. . . 4 ⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦))
43	42	rexlimivv 3201	. . 3 ⊢ (∃𝑎 ∈ ℝ ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ ∃𝑑 ∈ ℝ (𝑎 + (i · 𝑏)) ≠ (𝑐 + (i · 𝑑)) → ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦)
44	1, 17, 43	mp2b 10	. 2 ⊢ ∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦
45		eqtr3 2758	. . . . . . . . 9 ⊢ ((𝑥 = 0 ∧ 𝑦 = 0) → 𝑥 = 𝑦)
46	45	ex 416	. . . . . . . 8 ⊢ (𝑥 = 0 → (𝑦 = 0 → 𝑥 = 𝑦))
47	46	necon3d 2953	. . . . . . 7 ⊢ (𝑥 = 0 → (𝑥 ≠ 𝑦 → 𝑦 ≠ 0))
48		neeq1 2994	. . . . . . . . 9 ⊢ (𝑧 = 𝑦 → (𝑧 ≠ 0 ↔ 𝑦 ≠ 0))
49	48	rspcev 3527	. . . . . . . 8 ⊢ ((𝑦 ∈ ℝ ∧ 𝑦 ≠ 0) → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)
50	49	expcom 417	. . . . . . 7 ⊢ (𝑦 ≠ 0 → (𝑦 ∈ ℝ → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
51	47, 50	syl6 35	. . . . . 6 ⊢ (𝑥 = 0 → (𝑥 ≠ 𝑦 → (𝑦 ∈ ℝ → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
52	51	com23 86	. . . . 5 ⊢ (𝑥 = 0 → (𝑦 ∈ ℝ → (𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
53	52	adantld 494	. . . 4 ⊢ (𝑥 = 0 → ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
54		neeq1 2994	. . . . . . . 8 ⊢ (𝑧 = 𝑥 → (𝑧 ≠ 0 ↔ 𝑥 ≠ 0))
55	54	rspcev 3527	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ ∧ 𝑥 ≠ 0) → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)
56	55	expcom 417	. . . . . 6 ⊢ (𝑥 ≠ 0 → (𝑥 ∈ ℝ → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
57	56	adantrd 495	. . . . 5 ⊢ (𝑥 ≠ 0 → ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
58	57	a1dd 50	. . . 4 ⊢ (𝑥 ≠ 0 → ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)))
59	53, 58	pm2.61ine 3015	. . 3 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0))
60	59	rexlimivv 3201	. 2 ⊢ (∃𝑥 ∈ ℝ ∃𝑦 ∈ ℝ 𝑥 ≠ 𝑦 → ∃𝑧 ∈ ℝ 𝑧 ≠ 0)
61		ax-rrecex 10766	. . . 4 ⊢ ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → ∃𝑥 ∈ ℝ (𝑧 · 𝑥) = 1)
62		remulcl 10779	. . . . . . 7 ⊢ ((𝑧 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (𝑧 · 𝑥) ∈ ℝ)
63	62	adantlr 715	. . . . . 6 ⊢ (((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) ∧ 𝑥 ∈ ℝ) → (𝑧 · 𝑥) ∈ ℝ)
64		eleq1 2818	. . . . . 6 ⊢ ((𝑧 · 𝑥) = 1 → ((𝑧 · 𝑥) ∈ ℝ ↔ 1 ∈ ℝ))
65	63, 64	syl5ibcom 248	. . . . 5 ⊢ (((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) ∧ 𝑥 ∈ ℝ) → ((𝑧 · 𝑥) = 1 → 1 ∈ ℝ))
66	65	rexlimdva 3193	. . . 4 ⊢ ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → (∃𝑥 ∈ ℝ (𝑧 · 𝑥) = 1 → 1 ∈ ℝ))
67	61, 66	mpd 15	. . 3 ⊢ ((𝑧 ∈ ℝ ∧ 𝑧 ≠ 0) → 1 ∈ ℝ)
68	67	rexlimiva 3190	. 2 ⊢ (∃𝑧 ∈ ℝ 𝑧 ≠ 0 → 1 ∈ ℝ)
69	44, 60, 68	mp2b 10	1 ⊢ 1 ∈ ℝ

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 399   ∨ wo 847   = wceq 1543   ∈ wcel 2112   ≠ wne 2932  ∃wrex 3052  (class class class)co 7191  ℂcc 10692  ℝcr 10693  0cc0 10694  1c1 10695  ici 10696   + caddc 10697   · cmul 10699

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708  ax-1cn 10752  ax-icn 10753  ax-addcl 10754  ax-mulcl 10756  ax-mulrcl 10757  ax-i2m1 10762  ax-1ne0 10763  ax-rrecex 10766  ax-cnre 10767

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-ne 2933  df-ral 3056  df-rex 3057  df-rab 3060  df-v 3400  df-dif 3856  df-un 3858  df-in 3860  df-ss 3870  df-nul 4224  df-if 4426  df-sn 4528  df-pr 4530  df-op 4534  df-uni 4806  df-br 5040  df-iota 6316  df-fv 6366  df-ov 7194

This theorem is referenced by:  1red  10799  1xr  10857  dedekind  10960  peano2re  10970  mul02lem2  10974  addid1  10977  renegcl  11106  peano2rem  11110  0reALT  11140  0lt1  11319  0le1  11320  relin01  11321  1le1  11425  eqneg  11517  ltp1  11637  ltm1  11639  recgt0  11643  mulgt1  11656  ltmulgt11  11657  lemulge11  11659  reclt1  11692  recgt1  11693  recgt1i  11694  recp1lt1  11695  recreclt  11696  recgt0ii  11703  ledivp1i  11722  ltdivp1i  11723  inelr  11785  cju  11791  nnssre  11799  nnge1  11823  nngt1ne1  11824  nnle1eq1  11825  nngt0  11826  nnnlt1  11827  nnne0  11829  nnrecre  11837  nnrecgt0  11838  nnsub  11839  2re  11869  3re  11875  4re  11879  5re  11882  6re  11885  7re  11888  8re  11891  9re  11894  0le2  11897  2pos  11898  3pos  11900  4pos  11902  5pos  11904  6pos  11905  7pos  11906  8pos  11907  9pos  11908  neg1rr  11910  neg1lt0  11912  1lt2  11966  1lt3  11968  1lt4  11971  1lt5  11975  1lt6  11980  1lt7  11986  1lt8  11993  1lt9  12001  1ne2  12003  1le2  12004  1le3  12007  halflt1  12013  addltmul  12031  nnunb  12051  elnnnn0c  12100  nn0ge2m1nn  12124  elnnz1  12168  znnnlt1  12169  zltp1le  12192  zleltp1  12193  nn0lt2  12205  recnz  12217  gtndiv  12219  3halfnz  12221  10re  12277  1lt10  12397  eluzp1m1  12429  eluzp1p1  12431  eluz2b2  12482  zbtwnre  12507  rebtwnz  12508  1rp  12555  divlt1lt  12620  divle1le  12621  nnledivrp  12663  qbtwnxr  12755  xmulid1  12834  xmulm1  12836  x2times  12854  xrub  12867  elicc01  13019  1elunit  13023  divelunit  13047  lincmb01cmp  13048  unitssre  13052  0nelfz1  13096  fzpreddisj  13126  fznatpl1  13131  fztpval  13139  fraclt1  13342  fracle1  13343  flbi2  13357  fldiv4p1lem1div2  13375  fldiv4lem1div2  13377  fldiv  13398  modid  13434  1mod  13441  m1modnnsub1  13455  modm1p1mod0  13460  seqf1olem1  13580  reexpcl  13617  reexpclz  13620  expge0  13636  expge1  13637  expgt1  13638  bernneq  13761  bernneq2  13762  expnbnd  13764  expnlbnd  13765  expnlbnd2  13766  expmulnbnd  13767  discr1  13771  facwordi  13820  faclbnd3  13823  faclbnd4lem1  13824  faclbnd4lem4  13827  faclbnd6  13830  facavg  13832  hashv01gt1  13876  hashnn0n0nn  13923  hashunsnggt  13926  hash1snb  13951  hashgt12el  13954  hashgt12el2  13955  hashfun  13969  hashge2el2dif  14011  lsw0  14085  f1oun2prg  14447  cjexp  14678  re1  14682  im1  14683  rei  14684  imi  14685  sqrlem1  14771  sqrlem2  14772  sqrlem3  14773  sqrlem4  14774  sqrlem7  14777  resqrex  14779  sqrt1  14800  sqrt2gt1lt2  14803  sqrtm1  14804  abs1  14826  absrdbnd  14870  caubnd2  14886  mulcn2  15122  reccn2  15123  rlimno1  15182  o1fsum  15340  expcnv  15391  geolim  15397  geolim2  15398  georeclim  15399  geomulcvg  15403  geoisumr  15405  geoisum1c  15407  fprodge0  15518  fprodge1  15520  rerisefaccl  15542  refallfaccl  15543  ere  15613  ege2le3  15614  efgt1  15640  resin4p  15662  recos4p  15663  tanhbnd  15685  sinbnd  15704  cosbnd  15705  sinbnd2  15706  cosbnd2  15707  ef01bndlem  15708  sin01bnd  15709  cos01bnd  15710  cos1bnd  15711  cos2bnd  15712  sinltx  15713  sin01gt0  15714  cos01gt0  15715  sin02gt0  15716  sincos1sgn  15717  ene1  15734  rpnnen2lem2  15739  rpnnen2lem3  15740  rpnnen2lem4  15741  rpnnen2lem9  15746  rpnnen2lem12  15749  ruclem6  15759  ruclem11  15764  ruclem12  15765  3dvds  15855  flodddiv4  15937  sadcadd  15980  isprm3  16203  sqnprm  16222  coprm  16231  phibndlem  16286  pythagtriplem3  16334  pcmpt  16408  fldivp1  16413  pockthi  16423  infpn2  16429  resslem  16741  basendxnmulrndx  16802  slotsbhcdif  16878  oppcbas  17176  rescbas  17288  rescabs  17293  odubas  17753  symgvalstruct  18743  lt6abl  19234  srgbinomlem4  19512  abvneg  19824  abvtrivd  19830  rmodislmod  19921  0ringnnzr  20261  cnfldfun  20329  xrsmcmn  20340  xrsnsgrp  20353  gzrngunitlem  20382  gzrngunit  20383  rge0srg  20388  psgnodpmr  20506  remulg  20523  resubdrg  20524  thlbas  20612  tuslem  23118  setsmsbas  23327  dscmet  23424  dscopn  23425  nrginvrcnlem  23543  idnghm  23595  tgioo  23647  blcvx  23649  iicmp  23737  iiconn  23738  iirev  23780  iihalf1  23782  iihalf2  23784  iihalf2cn  23785  elii1  23786  elii2  23787  iimulcl  23788  icopnfcnv  23793  icopnfhmeo  23794  iccpnfhmeo  23796  xrhmeo  23797  xrhmph  23798  evth  23810  xlebnum  23816  htpycc  23831  reparphti  23848  pcoval1  23864  pco1  23866  pcoval2  23867  pcocn  23868  pcohtpylem  23870  pcopt  23873  pcopt2  23874  pcoass  23875  pcorevlem  23877  nmhmcn  23971  ncvs1  24008  ovolunlem1a  24347  vitalilem2  24460  vitalilem4  24462  vitalilem5  24463  vitali  24464  i1f1  24541  itg11  24542  itg2const  24592  dveflem  24830  dvlipcn  24845  dvcvx  24871  ply1remlem  25014  fta1blem  25020  vieta1lem2  25158  aalioulem3  25181  aalioulem5  25183  aaliou3lem2  25190  ulmbdd  25244  iblulm  25253  radcnvlem1  25259  dvradcnv  25267  abelthlem2  25278  abelthlem3  25279  abelthlem5  25281  abelthlem7  25284  abelth  25287  abelth2  25288  reeff1olem  25292  reeff1o  25293  sinhalfpilem  25307  tangtx  25349  sincos4thpi  25357  pige3ALT  25363  coskpi  25366  cos0pilt1  25375  recosf1o  25378  tanregt0  25382  efif1olem3  25387  efif1olem4  25388  loge  25429  logdivlti  25462  logcnlem4  25487  logf1o2  25492  logtayl  25502  logccv  25505  recxpcl  25517  cxplea  25538  cxpcn3lem  25587  cxpaddlelem  25591  loglesqrt  25598  ang180lem2  25647  angpined  25667  acosrecl  25740  atancj  25747  atanlogaddlem  25750  atantan  25760  atans2  25768  ressatans  25771  leibpi  25779  log2le1  25787  birthdaylem3  25790  cxp2lim  25813  cxploglim  25814  cxploglim2  25815  divsqrtsumlem  25816  cvxcl  25821  scvxcvx  25822  jensenlem2  25824  amgmlem  25826  emcllem2  25833  emcllem4  25835  emcllem6  25837  emcllem7  25838  emre  25842  emgt0  25843  harmonicbnd3  25844  harmonicubnd  25846  harmonicbnd4  25847  zetacvg  25851  ftalem1  25909  ftalem2  25910  ftalem5  25913  issqf  25972  cht1  26001  chp1  26003  ppiltx  26013  mumullem2  26016  ppiublem1  26037  ppiub  26039  chtublem  26046  chtub  26047  logfacbnd3  26058  logexprlim  26060  perfectlem2  26065  dchrinv  26096  dchr1re  26098  efexple  26116  bposlem1  26119  bposlem2  26120  bposlem5  26123  bposlem8  26126  lgsdir2lem1  26160  lgsdir2lem5  26164  lgsdir  26167  lgsne0  26170  lgsabs1  26171  lgsdinn0  26180  gausslemma2dlem0i  26199  lgseisen  26214  m1lgs  26223  2lgslem3  26239  addsq2nreurex  26279  2sqreultblem  26283  2sqreunnltblem  26286  chebbnd1lem3  26306  chebbnd1  26307  chtppilimlem1  26308  chtppilimlem2  26309  chtppilim  26310  chpchtlim  26314  vmadivsumb  26318  rplogsumlem2  26320  rpvmasumlem  26322  dchrmusumlema  26328  dchrmusum2  26329  dchrvmasumlem2  26333  dchrvmasumiflem1  26336  dchrisum0flblem1  26343  dchrisum0flblem2  26344  dchrisum0fno1  26346  rpvmasum2  26347  dchrisum0re  26348  dchrisum0lema  26349  dchrisum0lem1b  26350  dchrisum0lem1  26351  dchrisum0lem2a  26352  dchrisum0lem2  26353  logdivsum  26368  mulog2sumlem2  26370  2vmadivsumlem  26375  log2sumbnd  26379  selbergb  26384  selberg2b  26387  chpdifbndlem1  26388  selberg3lem1  26392  selberg3lem2  26393  selberg4lem1  26395  pntrmax  26399  pntrsumo1  26400  selbergsb  26410  pntrlog2bndlem3  26414  pntrlog2bndlem5  26416  pntpbnd1a  26420  pntpbnd2  26422  pntibndlem1  26424  pntibndlem3  26427  pntlemd  26429  pntlemc  26430  pntlemb  26432  pntlemr  26437  pntlemf  26440  pntlemk  26441  pntlemo  26442  pntlem3  26444  pntleml  26446  abvcxp  26450  ostth2lem1  26453  ostth1  26468  ostth2lem2  26469  ostth2lem3  26470  ostth2lem4  26471  ostth2  26472  ostth3  26473  ostth  26474  trgcgrg  26560  brbtwn2  26950  colinearalglem4  26954  ax5seglem2  26974  ax5seglem3  26976  axpaschlem  26985  axpasch  26986  axlowdimlem6  26992  axlowdimlem10  26996  axlowdimlem16  27002  axlowdim1  27004  axlowdim2  27005  axlowdim  27006  axcontlem2  27010  elntg2  27030  lfgrnloop  27170  lfuhgr1v0e  27296  usgrexmpldifpr  27300  usgrexmplef  27301  1loopgrvd2  27545  vdegp1bi  27579  lfgrwlkprop  27729  pthdlem1  27807  pthdlem2  27809  clwlkclwwlkf  28045  upgr4cycl4dv4e  28222  konigsberglem2  28290  konigsberglem3  28291  konigsberglem5  28293  frgrreg  28431  ex-dif  28460  ex-in  28462  ex-pss  28465  ex-res  28478  ex-fl  28484  nv1  28710  smcnlem  28732  ipidsq  28745  nmlno0lem  28828  norm-ii-i  29172  bcs2  29217  norm1  29284  nmopub2tALT  29944  nmfnleub2  29961  nmlnop0iALT  30030  unopbd  30050  nmopadjlem  30124  nmopcoadji  30136  pjnmopi  30183  pjbdlni  30184  hstle1  30261  hstle  30265  hstles  30266  stge1i  30273  stlesi  30276  staddi  30281  stadd3i  30283  strlem1  30285  strlem5  30290  jplem1  30303  cdj1i  30468  addltmulALT  30481  xlt2addrd  30755  pr01ssre  30812  dp2lt10  30832  dp2ltsuc  30834  dp2ltc  30835  dplti  30853  dpmul4  30862  cshw1s2  30906  xrsmulgzz  30960  resvbas  31204  rearchi  31214  xrge0slmod  31216  prmidl0  31294  submateqlem1  31425  xrge0iifcnv  31551  xrge0iifcv  31552  xrge0iifiso  31553  xrge0iifhom  31555  zrhre  31635  indf  31649  indfval  31650  esumcst  31697  cntnevol  31862  omssubadd  31933  iwrdsplit  32020  dstfrvclim1  32110  coinfliprv  32115  ballotlem2  32121  ballotlem4  32131  ballotlemi1  32135  ballotlemic  32139  sgnclre  32172  sgnnbi  32178  sgnpbi  32179  sgnmulsgp  32183  plymulx0  32192  plymulx  32193  signswch  32206  signstf  32211  signsvfn  32227  itgexpif  32252  hgt750lemd  32294  logdivsqrle  32296  hgt750lem  32297  hgt750lem2  32298  hgt750leme  32304  tgoldbachgnn  32305  subfacp1lem1  32808  subfacp1lem5  32813  resconn  32875  iisconn  32881  iillysconn  32882  problem2  33291  problem3  33292  sinccvglem  33297  fz0n  33365  dnibndlem12  34355  knoppcnlem4  34362  knoppndvlem13  34390  cnndvlem1  34403  irrdiff  35180  relowlpssretop  35221  sin2h  35453  cos2h  35454  tan2h  35455  poimirlem7  35470  poimirlem16  35479  poimirlem17  35480  poimirlem19  35482  poimirlem20  35483  poimirlem22  35485  poimirlem23  35486  poimirlem29  35492  poimirlem31  35494  itg2addnclem3  35516  asindmre  35546  dvasin  35547  dvacos  35548  dvreasin  35549  dvreacos  35550  fdc  35589  geomcau  35603  cntotbnd  35640  heiborlem8  35662  bfplem2  35667  bfp  35668  aks4d1p1p7  39764  2xp3dxp2ge1d  39825  factwoffsmonot  39826  1t1e1ALT  39940  re1m1e0m0  40029  sn-00idlem1  40030  sn-00idlem2  40031  remul02  40037  sn-0ne2  40038  reixi  40053  rei4  40054  remulid2  40064  ipiiie0  40068  sn-0tie0  40070  mulgt0b2d  40079  sn-0lt1  40081  sn-ltp1  40082  reneg1lt0  40083  sn-inelr  40084  rabren3dioph  40281  pellexlem5  40299  pellexlem6  40300  pell1qrgaplem  40339  pell14qrgap  40341  pellqrex  40345  pellfundre  40347  pellfundlb  40350  pellfund14gap  40353  jm2.17a  40426  acongeq  40449  jm2.23  40462  jm3.1lem2  40484  sqrtcval  40866  sqrtcval2  40867  resqrtval  40868  imsqrtval  40869  relexp01min  40939  mnringbased  41447  cvgdvgrat  41545  lhe4.4ex1a  41561  binomcxplemnotnn0  41588  isosctrlem1ALT  42168  supxrgelem  42490  xrlexaddrp  42505  infxr  42520  infleinflem2  42524  sumnnodd  42789  limsup10exlem  42931  limsup10ex  42932  dvnprodlem3  43107  stoweidlem1  43160  stoweidlem18  43177  stoweidlem19  43178  stoweidlem26  43185  stoweidlem34  43193  stoweidlem40  43199  stoweidlem41  43200  stoweidlem59  43218  stoweid  43222  stirlinglem10  43242  stirlinglem11  43243  dirkercncflem1  43262  fourierdlem16  43282  fourierdlem21  43287  fourierdlem22  43288  fourierdlem42  43308  fourierdlem68  43333  fourierdlem83  43348  fourierdlem103  43368  sqwvfourb  43388  fouriersw  43390  etransclem23  43416  salgencntex  43500  ovn0lem  43721  smfmullem3  43942  smfmullem4  43943  zm1nn  44410  m1mod0mod1  44437  fmtnosqrt  44607  perfectALTVlem2  44790  2exp340mod341  44801  8exp8mod9  44804  nfermltl8rev  44810  nnsum3primesprm  44858  nnsum4primesodd  44864  nnsum4primesoddALTV  44865  nnsum4primeseven  44868  nnsum4primesevenALTV  44869  tgblthelfgott  44883  tgoldbach  44885  rege1logbrege0  45520  rege1logbzge0  45521  blennnelnn  45538  dignnld  45565  nn0sumshdiglemA  45581  nn0sumshdiglem1  45583  rrx2xpref1o  45680  rrxlines  45695  eenglngeehlnmlem1  45699  eenglngeehlnmlem2  45700  line2ylem  45713  line2x  45716  icccldii  45828  io1ii  45830  sepfsepc  45837