Theorem minveclem24 8568

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
minveclem24	|- ((f:NN-->Y /\ F ~~> P /\ B e. RR+) -> E.k e. NN A.n e. NN (k <_ n -> (((F` n) - 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

Proof of Theorem minveclem24

Step	Hyp	Ref	Expression
1		minvec10.1	. . . . 5 |- R = {x | E.y e. Y x = -u(N` (AMy))}
2		minvec10.u	. . . . 5 |- U e. CPreHil
3		minvec10.m	. . . . 5 |- M = (-v` U)
4		minvec10.n	. . . . 5 |- N = (norm` U)
5		minvec10.x	. . . . 5 |- X = (Base` U)
6		minvec10.w1	. . . . 5 |- W e. (SubSp` U)
7		minvec10.y	. . . . 5 |- Y = (Base` W)
8		minvec10.a	. . . . 5 |- A e. X
9		minvec23.2	. . . . 5 |- P = -usup(R, RR, < )
10	1, 2, 3, 4, 5, 6, 7, 8, 9	minveclem15 8559	. . . 4 |- ((F ~~> P /\ (sqr` B) e. RR+) -> E.k e. NN A.n e. NN (k <_ n -> (abs` ((F` n) - P)) < (sqr` B)))
11		rpsqrclt 6715	. . . 4 |- (B e. RR+ -> (sqr` B) e. RR+)
12	10, 11	sylan2 451	. . 3 |- ((F ~~> P /\ B e. RR+) -> E.k e. NN A.n e. NN (k <_ n -> (abs` ((F` n) - P)) < (sqr` B)))
13	12	3adant1 797	. 2 |- ((f:NN-->Y /\ F ~~> P /\ B e. RR+) -> E.k e. NN A.n e. NN (k <_ n -> (abs` ((F` n) - P)) < (sqr` B)))
14		lt2sqt 6630	. . . . . . . . . 10 |- ((((abs` ((F` n) - P)) e. RR /\ 0 <_ (abs` ((F` n) - P))) /\ ((sqr` B) e. RR /\ 0 <_ (sqr` B))) -> ((abs` ((F` n) - P)) < (sqr` B) <-> ((abs` ((F` n) - P))^2) < ((sqr` B)^2)))
15		recnt 5313	. . . . . . . . . . . . 13 |- (((F` n) - P) e. RR -> ((F` n) - P) e. CC)
16		absclt 6833	. . . . . . . . . . . . 13 |- (((F` n) - P) e. CC -> (abs` ((F` n) - P)) e. RR)
17	15, 16	syl 10	. . . . . . . . . . . 12 |- (((F` n) - P) e. RR -> (abs` ((F` n) - P)) e. RR)
18		absge0t 6854	. . . . . . . . . . . . 13 |- (((F` n) - P) e. CC -> 0 <_ (abs` ((F` n) - P)))
19	15, 18	syl 10	. . . . . . . . . . . 12 |- (((F` n) - P) e. RR -> 0 <_ (abs` ((F` n) - P)))
20	17, 19	jca 288	. . . . . . . . . . 11 |- (((F` n) - P) e. RR -> ((abs` ((F` n) - P)) e. RR /\ 0 <_ (abs` ((F` n) - P))))
21	20	adantr 389	. . . . . . . . . 10 |- ((((F` n) - P) e. RR /\ (f:NN-->Y /\ n e. NN)) -> ((abs` ((F` n) - P)) e. RR /\ 0 <_ (abs` ((F` n) - P))))
22		sqrclt 6710	. . . . . . . . . . 11 |- ((B e. RR /\ 0 <_ B) -> (sqr` B) e. RR)
23		sqrge0t 6712	. . . . . . . . . . 11 |- ((B e. RR /\ 0 <_ B) -> 0 <_ (sqr` B))
24	22, 23	jca 288	. . . . . . . . . 10 |- ((B e. RR /\ 0 <_ B) -> ((sqr` B) e. RR /\ 0 <_ (sqr` B)))
25	14, 21, 24	syl2an 454	. . . . . . . . 9 |- (((((F` n) - P) e. RR /\ (f:NN-->Y /\ n e. NN)) /\ (B e. RR /\ 0 <_ B)) -> ((abs` ((F` n) - P)) < (sqr` B) <-> ((abs` ((F` n) - P))^2) < ((sqr` B)^2)))
26		absresqt 6867	. . . . . . . . . . 11 |- (((F` n) - P) e. RR -> ((abs` ((F` n) - P))^2) = (((F` n) - P)^2))
27	26	breq1d 2629	. . . . . . . . . 10 |- (((F` n) - P) e. RR -> (((abs` ((F` n) - P))^2) < ((sqr` B)^2) <-> (((F` n) - P)^2) < ((sqr` B)^2)))
28	27	ad2antrr 404	. . . . . . . . 9 |- (((((F` n) - P) e. RR /\ (f:NN-->Y /\ n e. NN)) /\ (B e. RR /\ 0 <_ B)) -> (((abs` ((F` n) - P))^2) < ((sqr` B)^2) <-> (((F` n) - P)^2) < ((sqr` B)^2)))
29		sqsqrt 6723	. . . . . . . . . . 11 |- ((B e. RR /\ 0 <_ B) -> ((sqr` B)^2) = B)
30	29	adantl 388	. . . . . . . . . 10 |- (((((F` n) - P) e. RR /\ (f:NN-->Y /\ n e. NN)) /\ (B e. RR /\ 0 <_ B)) -> ((sqr` B)^2) = B)
31	30	breq2d 2630	. . . . . . . . 9 |- (((((F` n) - P) e. RR /\ (f:NN-->Y /\ n e. NN)) /\ (B e. RR /\ 0 <_ B)) -> ((((F` n) - P)^2) < ((sqr` B)^2) <-> (((F` n) - P)^2) < B))
32	25, 28, 31	3bitrd 544	. . . . . . . 8 |- (((((F` n) - P) e. RR /\ (f:NN-->Y /\ n e. NN)) /\ (B e. RR /\ 0 <_ B)) -> ((abs` ((F` n) - P)) < (sqr` B) <-> (((F` n) - P)^2) < B))
33		minvec22.hf	. . . . . . . . . . 11 |- (j e. NN -> (F` j) = (N` (AM(f` j))))
34	1, 2, 3, 4, 5, 6, 7, 8, 33	minveclem22 8566	. . . . . . . . . 10 |- ((f:NN-->Y /\ n e. NN) -> (F` n) e. RR)
35	1, 2, 3, 4, 5, 6, 7, 8, 9	minveclem12 8556	. . . . . . . . . . 11 |- P e. RR
36		resubclt 5438	. . . . . . . . . . 11 |- (((F` n) e. RR /\ P e. RR) -> ((F` n) - P) e. RR)
37	35, 36	mpan2 696	. . . . . . . . . 10 |- ((F` n) e. RR -> ((F` n) - P) e. RR)
38	34, 37	syl 10	. . . . . . . . 9 |- ((f:NN-->Y /\ n e. NN) -> ((F` n) - P) e. RR)
39	38	ancri 297	. . . . . . . 8 |- ((f:NN-->Y /\ n e. NN) -> (((F` n) - P) e. RR /\ (f:NN-->Y /\ n e. NN)))
40		rpret 6284	. . . . . . . . 9 |- (B e. RR+ -> B e. RR)
41		rpge0t 6287	. . . . . . . . 9 |- (B e. RR+ -> 0 <_ B)
42	40, 41	jca 288	. . . . . . . 8 |- (B e. RR+ -> (B e. RR /\ 0 <_ B))
43	32, 39, 42	syl2an 454	. . . . . . 7 |- (((f:NN-->Y /\ n e. NN) /\ B e. RR+) -> ((abs` ((F` n) - P)) < (sqr` B) <-> (((F` n) - P)^2) < B))
44	43	an1rs 489	. . . . . 6 |- (((f:NN-->Y /\ B e. RR+) /\ n e. NN) -> ((abs` ((F` n) - P)) < (sqr` B) <-> (((F` n) - P)^2) < B))
45	44	3adantl2 804	. . . . 5 |- (((f:NN-->Y /\ F ~~> P /\ B e. RR+) /\ n e. NN) -> ((abs` ((F` n) - P)) < (sqr` B) <-> (((F` n) - P)^2) < B))
46	45	imbi2d 612	. . . 4 |- (((f:NN-->Y /\ F ~~> P /\ B e. RR+) /\ n e. NN) -> ((k <_ n -> (abs` ((F` n) - P)) < (sqr` B)) <-> (k <_ n -> (((F` n) - P)^2) < B)))
47	46	ralbidva 1659	. . 3 |- ((f:NN-->Y /\ F ~~> P /\ B e. RR+) -> (A.n e. NN (k <_ n -> (abs` ((F` n) - P)) < (sqr` B)) <-> A.n e. NN (k <_ n -> (((F` n) - P)^2) < B)))
48	47	rexbidv 1664	. 2 |- ((f:NN-->Y /\ F ~~> P /\ B e. RR+) -> (E.k e. NN A.n e. NN (k <_ n -> (abs` ((F` n) - P)) < (sqr` B)) <-> E.k e. NN A.n e. NN (k <_ n -> (((F` n) - P)^2) < B)))
49	13, 48	mpbid 195	1 |- ((f:NN-->Y /\ F ~~> P /\ B e. RR+) -> E.k e. NN A.n e. NN (k <_ n -> ((