Home

Hilbert Space Explorer

< Previous   Next > Related theorems Unicode version

---

Theorem hlimunii 9029

Description: A Hilbert space sequence converges to at most one limit.

Hypotheses

Ref	Expression
hlimuni.1
hlimuni.2
hlimuni.3
hlimunii.3

Assertion

Ref	Expression
hlimunii

---

Proof of Theorem hlimunii

Step	Hyp	Ref	Expression
1		nn2get 5890	. . . . 5
2	1	rgen2a 1691	. . . 4
3		hlimunii.3	. . . . . . . . . 10
4	3	pm3.26i 320	. . . . . . . . 9
5		hlimuni.3	. . . . . . . . . 10
6		hlimuni.1	. . . . . . . . . 10
7	5, 6	hlimvec 8979	. . . . . . . . 9
8	4, 7	ax-mp 7	. . . . . . . 8
9	3	pm3.27i 324	. . . . . . . . 9
10		hlimuni.2	. . . . . . . . . 10
11	5, 10	hlimvec 8979	. . . . . . . . 9
12	9, 11	ax-mp 7	. . . . . . . 8
13	8, 12	hvsubcl 8812	. . . . . . 7
14	13	normcl 8919	. . . . . 6
15		2re 5926	. . . . . 6
16		2pos 5936	. . . . . 6
17	14, 15, 16	divgt0i2 5813	. . . . 5
18		2ne0 5937	. . . . . . . 8
19	14, 15, 18	redivcl 5754	. . . . . . 7
20	5, 6	hlimconv 8980	. . . . . . . 8
21	4, 20	ax-mp 7	. . . . . . 7
22		breq2 2613	. . . . . . . . 9
23		breq2 2613	. . . . . . . . . . 11
24	23	imbi2d 610	. . . . . . . . . 10
25	24	rexralbidv 1674	. . . . . . . . 9
26	22, 25	imbi12d 624	. . . . . . . 8
27	26	rcla4v 1864	. . . . . . 7
28	19, 21, 27	mp2 43	. . . . . 6
29	5, 10	hlimconv 8980	. . . . . . . 8
30	9, 29	ax-mp 7	. . . . . . 7
31		breq2 2613	. . . . . . . . . . 11
32	31	imbi2d 610	. . . . . . . . . 10
33	32	rexralbidv 1674	. . . . . . . . 9
34	22, 33	imbi12d 624	. . . . . . . 8
35	34	rcla4v 1864	. . . . . . 7
36	19, 30, 35	mp2 43	. . . . . 6
37	28, 36	jca 288	. . . . 5
38		r19.26 1742	. . . . . . . . 9
39		con3 94	. . . . . . . . . . . 12
40	14	ltnr 5583	. . . . . . . . . . . . 13
41	5, 6	hlimseq 8978	. . . . . . . . . . . . . . . . . . 19
42	4, 41	ax-mp 7	. . . . . . . . . . . . . . . . . 18
43	42	ffvelrni 3800	. . . . . . . . . . . . . . . . 17
44		normsubt 8931	. . . . . . . . . . . . . . . . . 18
45	8, 44	mpan2 694	. . . . . . . . . . . . . . . . 17
46	43, 45	syl 10	. . . . . . . . . . . . . . . 16
47	46	breq1d 2619	. . . . . . . . . . . . . . 15