Theorem norm3lem

Description: Lemma involving norm of differences in Hilbert space. (Contributed by NM, 18-Aug-1999) (New usage is discouraged.)

	Ref	Expression
Hypotheses	norm3dif.1	$$⊢A\in \mathscr{H}$$
	norm3dif.2	$$⊢B\in \mathscr{H}$$
	norm3dif.3	$$⊢C\in \mathscr{H}$$
	norm3lem.4	$$⊢D\in ℝ$$
Assertion	norm3lem	$$⊢\left({norm}_{ℎ}\left(A{-}_{ℎ}C\right)<\frac{D}{2}\wedge {norm}_{ℎ}\left(C{-}_{ℎ}B\right)<\frac{D}{2}\right)\to {norm}_{ℎ}\left(A{-}_{ℎ}B\right)<D$$

Proof

Step	Hyp	Ref	Expression
1		norm3dif.1	$$⊢A\in \mathscr{H}$$
2		norm3dif.2	$$⊢B\in \mathscr{H}$$
3		norm3dif.3	$$⊢C\in \mathscr{H}$$
4		norm3lem.4	$$⊢D\in ℝ$$
5	1 2 3	norm3difi	$$⊢{norm}_{ℎ}\left(A{-}_{ℎ}B\right)\le {norm}_{ℎ}\left(A{-}_{ℎ}C\right)+{norm}_{ℎ}\left(C{-}_{ℎ}B\right)$$
6	1 3	hvsubcli	$$⊢A{-}_{ℎ}C\in \mathscr{H}$$
7	6	normcli	$$⊢{norm}_{ℎ}\left(A{-}_{ℎ}C\right)\in ℝ$$
8	3 2	hvsubcli	$$⊢C{-}_{ℎ}B\in \mathscr{H}$$
9	8	normcli	$$⊢{norm}_{ℎ}\left(C{-}_{ℎ}B\right)\in ℝ$$
10	4	rehalfcli	$$⊢\frac{D}{2}\in ℝ$$
11	7 9 10 10	lt2addi	$$⊢\left({norm}_{ℎ}\left(A{-}_{ℎ}C\right)<\frac{D}{2}\wedge {norm}_{ℎ}\left(C{-}_{ℎ}B\right)<\frac{D}{2}\right)\to {norm}_{ℎ}\left(A{-}_{ℎ}C\right)+{norm}_{ℎ}\left(C{-}_{ℎ}B\right)<\left(\frac{D}{2}\right)+\left(\frac{D}{2}\right)$$
12	1 2	hvsubcli	$$⊢A{-}_{ℎ}B\in \mathscr{H}$$
13	12	normcli	$$⊢{norm}_{ℎ}\left(A{-}_{ℎ}B\right)\in ℝ$$
14	7 9	readdcli	$$⊢{norm}_{ℎ}\left(A{-}_{ℎ}C\right)+{norm}_{ℎ}\left(C{-}_{ℎ}B\right)\in ℝ$$
15	10 10	readdcli	$$⊢\left(\frac{D}{2}\right)+\left(\frac{D}{2}\right)\in ℝ$$
16	13 14 15	lelttri	$$⊢\left({norm}_{ℎ}\left(A{-}_{ℎ}B\right)\le {norm}_{ℎ}\left(A{-}_{ℎ}C\right)+{norm}_{ℎ}\left(C{-}_{ℎ}B\right)\wedge {norm}_{ℎ}\left(A{-}_{ℎ}C\right)+{norm}_{ℎ}\left(C{-}_{ℎ}B\right)<\left(\frac{D}{2}\right)+\left(\frac{D}{2}\right)\right)\to {norm}_{ℎ}\left(A{-}_{ℎ}B\right)<\left(\frac{D}{2}\right)+\left(\frac{D}{2}\right)$$
17	5 11 16	sylancr	$$⊢\left({norm}_{ℎ}\left(A{-}_{ℎ}C\right)<\frac{D}{2}\wedge {norm}_{ℎ}\left(C{-}_{ℎ}B\right)<\frac{D}{2}\right)\to {norm}_{ℎ}\left(A{-}_{ℎ}B\right)<\left(\frac{D}{2}\right)+\left(\frac{D}{2}\right)$$
18	10	recni	$$⊢\frac{D}{2}\in ℂ$$
19	18	2timesi	$$⊢2\left(\frac{D}{2}\right)=\left(\frac{D}{2}\right)+\left(\frac{D}{2}\right)$$
20	4	recni	$$⊢D\in ℂ$$
21		2cn	$$⊢2\in ℂ$$
22		2ne0	$$⊢2\ne 0$$
23	20 21 22	divcan2i	$$⊢2\left(\frac{D}{2}\right)=D$$
24	19 23	eqtr3i	$$⊢\left(\frac{D}{2}\right)+\left(\frac{D}{2}\right)=D$$
25	17 24	breqtrdi	$$⊢\left({norm}_{ℎ}\left(A{-}_{ℎ}C\right)<\frac{D}{2}\wedge {norm}_{ℎ}\left(C{-}_{ℎ}B\right)<\frac{D}{2}\right)\to {norm}_{ℎ}\left(A{-}_{ℎ}B\right)<D$$