Theorem minveclem25 8513

Description: Lemma for minvecex 8522.

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

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 8503	. . . 4 |- ((F ~~> P /\ (B / ((2 x. P) + 1)) e. RR+) -> E.k e. NN A.n e. NN (k <_ n -> (abs` ((F` n) - P)) < (B / ((2 x. P) + 1))))
11		2re 5934	. . . . . . . 8 |- 2 e. RR
12	1, 2, 3, 4, 5, 6, 7, 8, 9	minveclem12 8500	. . . . . . . 8 |- P e. RR
13	11, 12	remulcl 5315	. . . . . . 7 |- (2 x. P) e. RR
14		1re 5415	. . . . . . 7 |- 1 e. RR
15	13, 14	readdcl 5314	. . . . . 6 |- ((2 x. P) + 1) e. RR
16		0re 5420	. . . . . . . . 9 |- 0 e. RR
17		2pos 5944	. . . . . . . . 9 |- 0 < 2
18	16, 11, 17	ltlei 5562	. . . . . . . 8 |- 0 <_ 2
19	1, 2, 3, 4, 5, 6, 7, 8, 9	minveclem14 8502	. . . . . . . 8 |- 0 <_ P
20	11, 12	mulge0 5589	. . . . . . . 8 |- ((0 <_ 2 /\ 0 <_ P) -> 0 <_ (2 x. P))
21	18, 19, 20	mp2an 696	. . . . . . 7 |- 0 <_ (2 x. P)
22		lt01 5661	. . . . . . 7 |- 0 < 1
23	13, 14	addgegt0 5582	. . . . . . 7 |- ((0 <_ (2 x. P) /\ 0 < 1) -> 0 < ((2 x. P) + 1))
24	21, 22, 23	mp2an 696	. . . . . 6 |- 0 < ((2 x. P) + 1)
25	15, 24	elrpi 6229	. . . . 5 |- ((2 x. P) + 1) e. RR+
26		rpdivclt 6237	. . . . 5 |- ((B e. RR+ /\ ((2 x. P) + 1) e. RR+) -> (B / ((2 x. P) + 1)) e. RR+)
27	25, 26	mpan2 695	. . . 4 |- (B e. RR+ -> (B / ((2 x. P) + 1)) e. RR+)
28	10, 27	sylan2 451	. . 3 |- ((F ~~> P /\ B e. RR+) -> E.k e. NN A.n e. NN (k <_ n -> (abs` ((F` n) - P)) < (B / ((2 x. P) + 1))))
29	28	3adant1 796	. 2 |- ((f:NN-->Y /\ F ~~> P /\ B e. RR+) -> E.k e. NN A.n e. NN (k <_ n -> (abs` ((F` n) - P)) < (B / ((2 x. P) + 1))))
30		ltmuldiv2t 5826	. . . . . . . . . . . 12 |- (((((2 x. P) + 1) e. RR /\ (abs` ((F` n) - P)) e. RR /\ B e. RR) /\ 0 < ((2 x. P) + 1)) -> ((((2 x. P) + 1) x. (abs` ((F` n) - P))) < B <-> (abs` ((F` n) - P)) < (B / ((2 x. P) + 1))))
31	24, 30	mpan2 695	. . . . . . . . . . 11 |- ((((2 x. P) + 1) e. RR /\ (abs` ((F` n) - P)) e. RR /\ B e. RR) -> ((((2 x. P) + 1) x. (abs` ((F` n) - P))) < B <-> (abs` ((F` n) - P)) < (B / ((2 x. P) + 1))))
32	15, 31	mp3an1 901	. . . . . . . . . 10 |- (((abs` ((F` n) - P)) e. RR /\ B e. RR) -> ((((2 x. P) + 1) x. (abs` ((F` n) - P))) < B <-> (abs` ((F` n) - P)) < (B / ((2 x. P) + 1))))
33		resubclt 5418	. . . . . . . . . . . . 13 |- (((F` n) e. RR /\ P e. RR) -> ((F` n) - P) e. RR)
34	12, 33	mpan2 695	. . . . . . . . . . . 12 |- ((F` n) e. RR -> ((F` n) - P) e. RR)
35	34	recnd 5295	. . . . . . . . . . 11 |- ((F` n) e. RR -> ((F` n) - P) e. CC)
36		absclt 6776	. . . . . . . . . . 11 |- (((F` n) - P) e. CC -> (abs` ((F` n) - P)) e. RR)
37	35, 36	syl 10	. . . . . . . . . 10 |- ((F` n) e. RR -> (abs` ((F` n) - P)) e. RR)
38		rpret 6230	. . . . . . . . . 10 |- (B e. RR+ -> B e. RR)
39	32, 37, 38	syl2an 454	. . . . . . . . 9 |- (((F` n) e. RR /\ B e. RR+) -> ((((2 x. P) + 1) x. (abs` ((F` n) - P))) < B <-> (abs` ((F` n) - P)) < (B / ((2 x. P) + 1))))
40		leabst 6807	. . . . . . . . . . . . 13 |- (((F` n) - P) e. RR -> ((F` n) - P) <_ (abs` ((F` n) - P)))
41	34, 40	syl 10	. . . . . . . . . . . 12 |- ((F` n) e. RR -> ((F` n) - P) <_ (abs` ((F` n) - P)))
42	13	ltp1 5777	. . . . . . . . . . . . . 14 |- (2 x. P) < ((2 x. P) + 1)
43	13, 15, 42	ltlei 5562	. . . . . . . . . . . . 13 |- (2 x. P) <_ ((2 x. P) + 1)
44	13, 21	pm3.2i 285	. . . . . . . . . . . . . . 15 |- ((2 x. P) e. RR /\ 0 <_ (2 x. P))
45		lemul12ait 5806	. . . . . . . . . . . . . . 15 |- (((((2 x. P) e. RR /\ 0 <_ (2 x. P)) /\ ((2 x. P) + 1) e. RR) /\ (((F` n) - P) e. RR /\ ((abs` ((F` n) - P)) e. RR /\ 0 <_ (abs` ((F` n) - P))))) -> (((2 x. P) <_ ((2 x. P) + 1) /\ ((F` n) - P) <_ (abs` ((F` n) - P))) -> ((2 x. P) x. ((F` n) - P)) <_ (((2 x. P) + 1) x. (abs` ((F` n) - P)))))
46	44, 15, 45	mpanl12 707	. . . . . . . . . . . . . 14 |- ((((F` n) - P) e. RR /\ ((abs` ((F` n) - P)) e. RR /\ 0 <_ (abs` ((F` n) - P)))) -> (((2 x. P) <_ ((2 x. P) + 1) /\ ((F` n) - P) <_ (abs` ((F` n) - P))) -> ((2 x. P) x. ((F` n) - P)) <_ (((2 x. P) + 1) x. (abs` ((F` n) - P)))))
47		absge0t 6797	. . . . . . . . . . . . . . . 16 |- (((F` n) - P) e. CC -> 0 <_ (abs` ((F` n) - P)))
48	35, 47	syl 10	. . . . . . . . . . . . . . 15 |- ((F` n) e. RR -> 0 <_ (abs` ((F` n) - P)))
49	37, 48	jca 288	. . . . . . . . . . . . . 14 |- ((F` n) e. RR -> ((abs` ((F` n) - P)) e. RR /\ 0 <_ (abs` ((F` n) - P))))
50	46, 34, 49	sylanc 471	. . . . . . . . . . . . 13 |- ((F` n) e. RR -> (((2 x. P) <_ ((2 x. P) + 1) /\ ((F` n) - P) <_ (abs` ((F` n) - P))) -> ((2 x. P) x. ((F` n) - P)) <_ (((2 x. P) + 1) x. (abs` ((F` n) - P)))))
51	43, 50	mpani 697	. . . . . . . . . . . 12 |- ((F` n) e. RR -> (((F` n) - P) <_ (abs` ((F` n) - P)) -> ((2 x. P) x. ((F` n) - P)) <_ (((2 x. P) + 1) x. (abs` ((F` n) - P)))))
52	41, 51	mpd 26	. . . . . . . . . . 11 |- ((F` n) e. RR -> ((2 x. P) x. ((F` n) - P)) <_ (((2 x. P) + 1) x. (abs` ((F` n) - P))))
53	52	adantr 389	. . . . . . . . . 10 |- (((F` n) e. RR /\ B e. RR+) -> ((2 x. P) x. ((F` n) - P)) <_ (((2 x. P) + 1) x. (abs` ((F` n) - P))))
54		lelttrt 5504	. . . . . . . . . . 11 |- ((((2 x. P) x. ((F` n) - P)) e. RR /\ (((2 x. P) + 1) x. (abs` ((F` n) - P))) e. RR /\ B e. RR) -> ((((2 x. P) x. ((F` n) - P))