Theorem minveclem26 8570

Description: Lemma for minvecex 8578.

Hypotheses

Ref	Expression
minvec10.1	|- R = {x | E.y e. Y x = -u(N` (AMy))}
minvec10.u	|- U e. CPreHil
minvec10.m	|- M = (-v` U)
minvec10.n	|- N = (norm` U)
minvec10.x	|- X = (Base` U)
minvec10.w1	|- W e. (SubSp` U)
minvec10.y	|- Y = (Base` W)
minvec10.a	|- A e. X
minvec22.hf	|- (j e. NN -> (F` j) = (N` (AM(f` j))))
minvec23.2	|- P = -usup(R, RR, < )

Assertion

Ref	Expression
minveclem26	|- ((f:NN-->Y /\ F ~~> P /\ B e. RR+) -> E.k e. NN A.n e. NN (k <_ n -> (((F` n)^2) - (P^2)) < B))

Distinct variable groups:   f,j,k,x,y,A   k,n,B,x,y   j,n,F,k   f,n,M,j,k,x,y   f,N,j,k,n,x,y   P,f,j,k,n   x,U,y   x,W,y   f,Y,j,k,n,x,y   x,P,y

Proof of Theorem minveclem26

Step	Hyp	Ref	Expression
1		minvec10.1	. . . . . 6 |- R = {x | E.y e. Y x = -u(N` (AMy))}
2		minvec10.u	. . . . . 6 |- U e. CPreHil
3		minvec10.m	. . . . . 6 |- M = (-v` U)
4		minvec10.n	. . . . . 6 |- N = (norm` U)
5		minvec10.x	. . . . . 6 |- X = (Base` U)
6		minvec10.w1	. . . . . 6 |- W e. (SubSp` U)
7		minvec10.y	. . . . . 6 |- Y = (Base` W)
8		minvec10.a	. . . . . 6 |- A e. X
9		minvec22.hf	. . . . . 6 |- (j e. NN -> (F` j) = (N` (AM(f` j))))
10		minvec23.2	. . . . . 6 |- P = -usup(R, RR, < )
11	1, 2, 3, 4, 5, 6, 7, 8, 9, 10	minveclem24 8568	. . . . 5 |- ((f:NN-->Y /\ F ~~> P /\ (B / 2) e. RR+) -> E.k e. NN A.n e. NN (k <_ n -> (((F` n) - P)^2) < (B / 2)))
12	1, 2, 3, 4, 5, 6, 7, 8, 9, 10	minveclem25 8569	. . . . 5 |- ((f:NN-->Y /\ F ~~> P /\ (B / 2) e. RR+) -> E.k e. NN A.n e. NN (k <_ n -> ((2 x. P) x. ((F` n) - P)) < (B / 2)))
13	11, 12	jca 288	. . . 4 |- ((f:NN-->Y /\ F ~~> P /\ (B / 2) e. RR+) -> (E.k e. NN A.n e. NN (k <_ n -> (((F` n) - P)^2) < (B / 2)) /\ E.k e. NN A.n e. NN (k <_ n -> ((2 x. P) x. ((F` n) - P)) < (B / 2))))
14		1z 6159	. . . . 5 |- 1 e. ZZ
15		nnuz 6439	. . . . 5 |- NN = (ZZ>` 1)
16	14, 15	cvganuz 6925	. . . 4 |- ((E.k e. NN A.n e. NN (k <_ n -> (((F` n) - P)^2) < (B / 2)) /\ E.k e. NN A.n e. NN (k <_ n -> ((2 x. P) x. ((F` n) - P)) < (B / 2))) <-> E.k e. NN A.n e. NN (k <_ n -> ((((F` n) - P)^2) < (B / 2) /\ ((2 x. P) x. ((F` n) - P)) < (B / 2))))
17	13, 16	sylib 198	. . 3 |- ((f:NN-->Y /\ F ~~> P /\ (B / 2) e. RR+) -> E.k e. NN A.n e. NN (k <_ n -> ((((F` n) - P)^2) < (B / 2) /\ ((2 x. P) x. ((F` n) - P)) < (B / 2))))
18		2re 5979	. . . . 5 |- 2 e. RR
19		2pos 5989	. . . . 5 |- 0 < 2
20	18, 19	elrpi 6283	. . . 4 |- 2 e. RR+
21		rpdivclt 6292	. . . 4 |- ((B e. RR+ /\ 2 e. RR+) -> (B / 2) e. RR+)
22	20, 21	mpan2 696	. . 3 |- (B e. RR+ -> (B / 2) e. RR+)
23	17, 22	syl3an3 861	. 2 |- ((f:NN-->Y /\ F ~~> P /\ B e. RR+) -> E.k e. NN A.n e. NN (k <_ n -> ((((F` n) - P)^2) < (B / 2) /\ ((2 x. P) x. ((F` n) - P)) < (B / 2))))
24		lt2addt 5643	. . . . . . . . . 10 |- ((((((F` n) - P)^2) e. RR /\ ((2 x. P) x. ((F` n) - P)) e. RR) /\ ((B / 2) e. RR /\ (B / 2) e. RR)) -> (((((F` n) - P)^2) < (B / 2) /\ ((2 x. P) x. ((F` n) - P)) < (B / 2)) -> ((((F` n) - P)^2) + ((2 x. P) x. ((F` n) - P))) < ((B / 2) + (B / 2))))
25	1, 2, 3, 4, 5, 6, 7, 8, 10	minveclem12 8556	. . . . . . . . . . . . 13 |- P e. RR
26		resubclt 5438	. . . . . . . . . . . . 13 |- (((F` n) e. RR /\ P e. RR) -> ((F` n) - P) e. RR)
27	25, 26	mpan2 696	. . . . . . . . . . . 12 |- ((F` n) e. RR -> ((F` n) - P) e. RR)
28		resqclt 6621	. . . . . . . . . . . 12 |- (((F` n) - P) e. RR -> (((F` n) - P)^2) e. RR)
29	27, 28	syl 10	. . . . . . . . . . 11 |- ((F` n) e. RR -> (((F` n) - P)^2) e. RR)
30	18, 25	remulcl 5335	. . . . . . . . . . . . 13 |- (2 x. P) e. RR
31		axmulrcl 5274	. . . . . . . . . . . . 13 |- (((2 x. P) e. RR /\ ((F` n) - P) e. RR) -> ((2 x. P) x. ((F` n) - P)) e. RR)
32	30, 31	mpan 695	. . . . . . . . . . . 12 |- (((F` n) - P) e. RR -> ((2 x. P) x. ((F` n) - P)) e. RR)
33	27, 32	syl 10	. . . . . . . . . . 11 |- ((F` n) e. RR -> ((2 x. P) x. ((F` n) - P)) e. RR)
34	29, 33	jca 288	. . . . . . . . . 10 |- ((F` n) e. RR -> ((((F` n) - P)^2) e. RR /\ ((2 x. P) x. ((F` n) - P)) e. RR))
35		rehalfclt 6034	. . . . . . . . . . 11 |- (B e. RR -> (B / 2) e. RR)
36	35, 35	jca 288	. . . . . . . . . 10 |- (B e. RR -> ((B / 2) e. RR /\ (B / 2) e. RR))
37	24, 34, 36	syl2an 454	. . . . . . . . 9 |- (((F` n) e. RR /\ B e. RR) -> (((((F` n) - P)^2) < (B / 2) /\ ((2 x. P) x. ((F` n) - P)) < (B / 2)) -> ((((F` n) - P)^2) + ((2 x. P) x. ((F` n) - P))) < ((B / 2) + (B / 2))))
38		recnt 5313	. . . . . . . . . . 11 |- ((F` n) e. RR -> (F` n) e. CC)
39	25	recn 5314	. . . . . . . . . . . 12 |- P e. CC
40		subsq2t 6643	. . . . . . . . . . . 12 |- (((F` n) e. CC /\ P e. CC) -> (((F` n)^2) - (P^2)) = ((((F` n) - P)^2) + ((2 x. P) x. ((F` n) - P))))
41	39, 40	mpan2 696	. . . . . . . . . . 11 |- ((F` n) e. CC -> (((F` n)^2) - (P^2)) = ((((F` n) - P)^2) + ((2 x. P) x. ((F` n) - P))))
42	38, 41	syl 10	. . . . . . . . . 10 |- ((F` n) e. RR -> (((F` n)^2) - (P^2)) = ((((F` n) - P)^2) + ((2 x. P) x. ((F` n) - P))))
43		recnt 5313	. . . . . . . . . . . 12 |- (B e. RR -> B e. CC)
44		2halvest 6039	. . . . . . . . . . . 12 |- (B e. CC -> ((B / 2) + (B / 2)) = B)
45	43, 44	syl 10	. . . . . . . . . . 11 |- (B e. RR -> ((B / 2) + (B / 2)) = B)
46	45	eqcomd 1480	. . . . . . . . . 10 |- (B e. RR -> B = ((B / 2) + (B / 2)))
47	42, 46	breqan12d 2632	. . . . . . . . 9 |- (((F` n) e. RR /\ B e. RR) -> ((((F` n)^2) - (P^2)) < B <-> ((((F` n) - P)^2) + ((2 x. P) x. ((F` n) - P))) < ((B / 2) + (B / 2))))
48	37, 47	sylibrd 204	. . . . . . . 8 |- (((F` n) e. RR /\ B e. RR) -> (((((F` n) - P)^2) < (B / 2) /\ ((2 x. P) x. ((F` n) - P)) < (B / 2)) -> (((F` n)^2) - (P^2)) < B))
49	1, 2, 3, 4, 5, 6, 7, 8, 9	minveclem22 8566	. . . . . . . 8 |- ((f:NN-->Y /\ n e. NN) -> (F` n) e. RR)
50		rpret 6284	. . . . . . . 8 |- (B e. RR+ -> B e. RR)
51	48, 49, 50	syl2an 454	. . . . . . 7 |- (((f:NN-->Y /\ n e. NN) /\ B e. RR+) -> (((((F` n) - P)^2) < (B / 2) /\ ((2 x. P) x. ((F` n) - P)) < (B / 2)) -> (((F` n)^2) - (P^2)) < B))
52	51	an1rs 489	. . . . . 6 |- (((f:NN-->Y /\ B e. RR+) /\ n e. NN) -> (