HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem minveclem27 8502
Description: Lemma for minvecex 8509.
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
minveclem27 |- (((f:NN-->Y /\ F ~~> P) /\ B e. RR+) -> E.k e. NN A.m e. NN (k <_ m -> ((N` ((f` k)M(f` m)))^2) < B))
Distinct variable groups:   f,j,k,m,x,y,A   B,k,m,x,y   j,F,k,m   f,M,j,k,m,x,y   f,N,j,k,m,x,y   P,f,j,k,m   x,U,y   x,W,y   f,Y,j,k,m,x,y   x,P,y
Proof of Theorem minveclem27
StepHypRef 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 minvec22.hf . . . . 5 |- (j e. NN -> (F` j) = (N` (AM(f` j))))
10 minvec23.2 . . . . 5 |- P = -usup(R, RR, < )
111, 2, 3, 4, 5, 6, 7, 8, 9, 10minveclem26 8501 . . . 4 |- ((f:NN-->Y /\ F ~~> P /\ ((B / 2) / 2) e. RR+) -> E.k e. NN A.m e. NN (k <_ m -> (((F` m)^2) - (P^2)) < ((B / 2) / 2)))
12 2re 5926 . . . . . . 7 |- 2 e. RR
13 2pos 5936 . . . . . . 7 |- 0 < 2
1412, 13elrpi 6221 . . . . . 6 |- 2 e. RR+
15 rpdivclt 6229 . . . . . 6 |- ((B e. RR+ /\ 2 e. RR+) -> (B / 2) e. RR+)
1614, 15mpan2 694 . . . . 5 |- (B e. RR+ -> (B / 2) e. RR+)
17 rpdivclt 6229 . . . . . 6 |- (((B / 2) e. RR+ /\ 2 e. RR+) -> ((B / 2) / 2) e. RR+)
1814, 17mpan2 694 . . . . 5 |- ((B / 2) e. RR+ -> ((B / 2) / 2) e. RR+)
1916, 18syl 10 . . . 4 |- (B e. RR+ -> ((B / 2) / 2) e. RR+)
2011, 19syl3an3 859 . . 3 |- ((f:NN-->Y /\ F ~~> P /\ B e. RR+) -> E.k e. NN A.m e. NN (k <_ m -> (((F` m)^2) - (P^2)) < ((B / 2) / 2)))
21203expa 831 . 2 |- (((f:NN-->Y /\ F ~~> P) /\ B e. RR+) -> E.k e. NN A.m e. NN (k <_ m -> (((F` m)^2) - (P^2)) < ((B / 2) / 2)))
22 nnret 5877 . . . . . . . . 9 |- (k e. NN -> k e. RR)
23 leidt 5504 . . . . . . . . 9 |- (k e. RR -> k <_ k)
2422, 23syl 10 . . . . . . . 8 |- (k e. NN -> k <_ k)
25 breq2 2613 . . . . . . . . . 10 |- (m = k -> (k <_ m <-> k <_ k))
26 fveq2 3709 . . . . . . . . . . . . 13 |- (m = k -> (F` m) = (F` k))
2726opreq1d 3960 . . . . . . . . . . . 12 |- (m = k -> ((F` m)^2) = ((F` k)^2))
2827opreq1d 3960 . . . . . . . . . . 11 |- (m = k -> (((F` m)^2) - (P^2)) = (((F` k)^2) - (P^2)))
2928breq1d 2619 . . . . . . . . . 10 |- (m = k -> ((((F` m)^2) - (P^2)) < ((B / 2) / 2) <-> (((F` k)^2) - (P^2)) < ((B / 2) / 2)))
3025, 29imbi12d 624 . . . . . . . . 9 |- (m = k -> ((k <_ m -> (((F` m)^2) - (P^2)) < ((B / 2) / 2)) <-> (k <_ k -> (((F` k)^2) - (P^2)) < ((B / 2) / 2))))
3130rcla4v 1864 . . . . . . . 8 |- (k e. NN -> (A.m e. NN (k <_ m -> (((F` m)^2) - (P^2)) < ((B / 2) / 2)) -> (k <_ k -> (((F` k)^2) - (P^2)) < ((B / 2) / 2))))
3224, 31mpid 47 . . . . . . 7 |- (k e. NN -> (A.m e. NN (k <_ m -> (((F` m)^2) - (P^2)) < ((B / 2) / 2)) -> (((F` k)^2) - (P^2)) < ((B / 2) / 2)))
3332adantl 388 . . . . . 6 |- ((((f:NN-->Y /\ F ~~> P) /\ B e. RR+) /\ k e. NN) -> (A.m e. NN (k <_ m -> (((F` m)^2) - (P^2)) < ((B / 2) / 2)) -> (((F` k)^2) - (P^2)) < ((B / 2) / 2)))
3433ancrd 299 . . . . 5 |- ((((f:NN-->Y /\ F ~~> P) /\ B e. RR+) /\ k e. NN) -> (A.m e. NN (k <_ m -> (((F` m)^2) - (P^2)) < ((B / 2) / 2)) -> ((((F` k)^2) - (P^2)) < ((B / 2) / 2) /\ A.m e. NN (k <_ m -> (((F` m)^2) - (P^2)) < ((B / 2) / 2)))))
35 r19.28av 1747 . . . . 5 |- (((((F` k)^2) - (P^2)) < ((B / 2) / 2) /\ A.m e. NN (k <_ m -> (((F` m)^2) - (P^2)) < ((B / 2) / 2))) -> A.m e. NN ((((F` k)^2) - (P^2)) < ((B / 2) / 2) /\ (k <_ m -> (((F` m)^2) - (P^2)) < ((B / 2) / 2))))
3634, 35syl6 22 . . . 4 |- ((((f:NN-->Y /\ F ~~> P) /\ B e. RR+) /\ k e. NN) -> (A.m e. NN (k <_ m -> (((F` m)^2) - (P^2)) < ((B / 2) / 2)) -> A.m e. NN ((((F` k)^2) - (P^2)) < ((B / 2) / 2) /\ (k <_ m -> (((F` m)^2) - (P^2)) < ((B / 2) / 2)))))
37 pm3.43 601 . . . . . . . 8 |- (((k <_ m -> (((F` k)^2) - (P^2)) < ((B / 2) / 2)) /\ (k <_ m -> (((F` m)^2) - (P^2)) < ((B / 2) / 2))) -> (k <_ m -> ((((F` k)^2) - (P^2)) < ((B / 2) / 2) /\ (((F` m)^2) - (P^2)) < ((B / 2) / 2))))
38 ax-1 4 . . . . . . . 8 |- ((((F` k)^2) - (P^2)) < ((B / 2) / 2) -> (k <_ m -> (((F` k)^2) - (P^2)) < ((B / 2) / 2)))
3937, 38sylan 448 . . . . . . 7 |- (((((F` k)^2) - (P^2)) < ((B / 2) / 2) /\ (k <_ m -> (((F` m)^2) - (P^2)) < ((B / 2) / 2))) -> (k <_ m -> ((((F` k)^2) - (P^2)) < ((B / 2) / 2) /\ (((F` m)^2) - (P^2)) < ((B / 2) / 2))))
40 lt2addt 5617 . . . . . . . . . . . . 13 |- ((((((F` k)^2) - (P^2)) e. RR /\ (((F` m)^2) - (P^2)) e. RR) /\ (((B / 2) / 2) e. RR /\ ((B / 2) / 2) e. RR)) -> (((((F` k)^2) - (P^2)) < ((B / 2) / 2) /\ (((F` m)^2) - (P^2)) < ((B / 2) / 2)) -> ((((F` k)^2) - (P^2)) + (((F` m)^2) - (P^2))) < (((B / 2) / 2) + ((B / 2) / 2))))
41 resqclt 6552 . . . . . . . . . . . . . . 15 |- ((F` k) e. RR -> ((F` k)^2) e. RR)
421, 2, 3, 4, 5, 6, 7, 8, 10minveclem12 8487 . . . . . . . . . . . . . . . . 17 |- P e. RR
4342resqcl 6554 . . . . . . . . . . . . . . . 16 |- (P^2) e. RR
44