HomeHome Hilbert Space Explorer < Previous   Next >
Related theorems
Unicode version
Theorem hlimcaui 9027
Description: If a sequence in Hilbert space subset converges to a limit, it is a Cauchy sequence.
Hypotheses
Ref Expression
hlimcau.1 |- A e. V
hlimcau.2 |- F e. V
hlimcaui.4 |- F ~~>v A
Assertion
Ref Expression
hlimcaui |- F e. Cauchy
Proof of Theorem hlimcaui
StepHypRef Expression
1 hcau 8972 . 2 |- (F e. Cauchy <-> (F:NN-->H~ /\ A.x e. RR (0 < x -> E.y e. NN A.z e. NN A.w e. NN ((y <_ z /\ y <_ w) -> (normh` ((F` z) -h (F` w))) < x))))
2 hlimcaui.4 . . 3 |- F ~~>v A
3 hlimcau.2 . . . 4 |- F e. V
4 hlimcau.1 . . . 4 |- A e. V
53, 4hlimseq 8978 . . 3 |- (F ~~>v A -> F:NN-->H~)
62, 5ax-mp 7 . 2 |- F:NN-->H~
7 breq2 2613 . . . . . . . 8 |- (v = (x / 2) -> (0 < v <-> 0 < (x / 2)))
8 breq2 2613 . . . . . . . . . 10 |- (v = (x / 2) -> ((normh` ((F` z) -h A)) < v <-> (normh` ((F` z) -h A)) < (x / 2)))
98imbi2d 610 . . . . . . . . 9 |- (v = (x / 2) -> ((y <_ z -> (normh` ((F` z) -h A)) < v) <-> (y <_ z -> (normh` ((F` z) -h A)) < (x / 2))))
109rexralbidv 1674 . . . . . . . 8 |- (v = (x / 2) -> (E.y e. NN A.z e. NN (y <_ z -> (normh` ((F` z) -h A)) < v) <-> E.y e. NN A.z e. NN (y <_ z -> (normh` ((F` z) -h A)) < (x / 2))))
117, 10imbi12d 624 . . . . . . 7 |- (v = (x / 2) -> ((0 < v -> E.y e. NN A.z e. NN (y <_ z -> (normh` ((F` z) -h A)) < v)) <-> (0 < (x / 2) -> E.y e. NN A.z e. NN (y <_ z -> (normh` ((F` z) -h A)) < (x / 2)))))
123, 4hlimvec 8979 . . . . . . . . 9 |- (F ~~>v A -> A e. H~)
132, 12ax-mp 7 . . . . . . . 8 |- A e. H~
14 hlim2 8981 . . . . . . . . 9 |- ((F:NN-->H~ /\ A e. H~) -> (F ~~>v A <-> A.v e. RR (0 < v -> E.y e. NN A.z e. NN (y <_ z -> (normh` ((F` z) -h A)) < v))))
152, 14mpbii 193 . . . . . . . 8 |- ((F:NN-->H~ /\ A e. H~) -> A.v e. RR (0 < v -> E.y e. NN A.z e. NN (y <_ z -> (normh` ((F` z) -h A)) < v)))
166, 13, 15mp2an 695 . . . . . . 7 |- A.v e. RR (0 < v -> E.y e. NN A.z e. NN (y <_ z -> (normh` ((F` z) -h A)) < v))
1711, 16vtoclri 1850 . . . . . 6 |- ((x / 2) e. RR -> (0 < (x / 2) -> E.y e. NN A.z e. NN (y <_ z -> (normh` ((F` z) -h A)) < (x / 2))))
18 rehalfclt 5981 . . . . . . 7 |- (x e. RR -> (x / 2) e. RR)
1918adantr 389 . . . . . 6 |- ((x e. RR /\ 0 < x) -> (x / 2) e. RR)
20 breq2 2613 . . . . . . . . 9 |- (x = if(x e. RR, x, 0) -> (0 < x <-> 0 < if(x e. RR, x, 0)))
21 opreq1 3953 . . . . . . . . . 10 |- (x = if(x e. RR, x, 0) -> (x / 2) = (if(x e. RR, x, 0) / 2))
2221breq2d 2620 . . . . . . . . 9 |- (x = if(x e. RR, x, 0) -> (0 < (x / 2) <-> 0 < (if(x e. RR, x, 0) / 2)))
2320, 22imbi12d 624 . . . . . . . 8 |- (x = if(x e. RR, x, 0) -> ((0 < x -> 0 < (x / 2)) <-> (0 < if(x e. RR, x, 0) -> 0 < (if(x e. RR, x, 0) / 2))))
24 0re 5412 . . . . . . . . . 10 |- 0 e. RR
2524elimel 2384 . . . . . . . . 9 |- if(x e. RR, x, 0) e. RR
26 2re 5926 . . . . . . . . 9 |- 2 e. RR
27 2pos 5936 . . . . . . . . 9 |- 0 < 2
2825, 26, 27divgt0i2 5813 . . . . . . . 8 |- (0 < if(x e. RR, x, 0) -> 0 < (if(x e. RR, x, 0) / 2))
2923, 28dedth 2373 . . . . . . 7 |- (x e. RR -> (0 < x -> 0 < (x / 2)))
3029imp 350 . . . . . 6 |- ((x e. RR /\ 0 < x) -> 0 < (x / 2))
3117, 19, 30sylc 68 . . . . 5 |- ((x e. RR /\ 0 < x) -> E.y e. NN A.z e. NN (y <_ z -> (normh` ((F` z) -h A)) < (x / 2)))
32 prth 554 . . . . . . . . . . 11 |- (((y <_ z -> (normh` ((F` z) -h A)) < (x / 2)) /\ (y <_ w -> (normh` ((F` w) -h A)) < (x / 2))) -> ((y <_ z /\ y <_ w) -> ((normh` ((F` z) -h A)) < (x / 2) /\ (normh` ((F` w) -h A)) < (x / 2))))
33 normsubt 8931 . . . . . . . . . . . . . . . 16 |- ((A e. H~ /\ (F` w) e. H~) -> (normh` (A -h (F` w))) = (normh` ((F` w) -h A)))
3433breq1d 2619 . . . . . . . . . . . . . . 15 |- ((A e. H~ /\ (F` w) e. H~) -> ((normh` (A -h (F` w))) < (x / 2) <-> (normh` ((F` w) -h A)) < (x / 2)))
3534anbi2d 614 . . . . . . . . . . . . . 14 |- ((A e. H~ /\ (F` w) e. H~) -> (((normh` ((F` z) -h A)) < (x / 2) /\ (normh` (A -h (F` w))) < (x / 2)) <-> ((normh` ((F` z) -h A)) < (x / 2) /\ (normh` ((F` w) -h A)) < (x / 2))))
3635adantl 388 . . . . . . . . . . . . 13 |- (((x e. RR /\ z e. NN) /\ (A e. H~ /\ (F` w) e. H~)) -> (((normh` ((F` z) -h A)) < (x / 2) /\ (normh` (A -h (F` w))) < (x / 2)) <-> ((normh` ((F` z) -h A)) < (x / 2) /\ (normh` ((F` w) -h A)) < (x / 2))))
376ffvelrni 3800 . . . . . . . . . . . . . . . . . . . 20 |- (z e. NN -> (F` z) e. H~)
3837anim1i 334 . . . . . . . . . . . . . . . . . . 19 |- ((z e. NN /\ (F` w) e. H~) -> ((F` z) e. H~ /\ (F` w) e. H~))
3938ancoms 436 . . . . . . . . . . . . . . . . . 18 |- (((F` w) e. H~ /\ z e. NN) -> ((F` z) e. H~ /\ (F` w) e. H~))
4039anim1i 334 . . . . . . . . . . . . . . . . 17 |- ((((F` w) e. H~ /\ z e. NN) /\ (A e. H~ /\ x e. RR)) -> (((F` z) e. H~ /\ (F` w) e. H~) /\ (A e. H~ /\ x e. RR)))
4140ancoms 436 . . . . . . . . . . . . . . . 16 |- (((A e. H~ /\ x e. RR) /\ ((F` w) e. H~ /\ z e. NN)) -> (((F` z) e. H~ /\ (F` w) e. H~) /\ (A e. H~ /\ x e. RR)))
4241an4s 507 . . . . . . . . . . . . . . 15 |- (((A e. H~ /\ (F` w) e. H~) /\ (x e. RR /\ z e. NN)) -> (((F` z) e. H~ /\ (F` w) e. H~) /\ (A e. H~ /\ x e. RR)))
4342ancoms 436 . . . . . . . . . . . . . 14 |- (((x e. RR /\ z e. NN) /\ (A e. H~ /\ (F` w) e. H~)) -> (((F` z) e. H~ /\ (F` w) e. H~) /\ (A e. H~ /\ x e. RR)))
44 norm3lemt 8940 . . . . . . . . . . . . . 14 |- ((((F` z) e. H~ /\ (F` w) e. H~) /\ (A e. H~ /\ x e. RR)) -> (((normh` ((F` z) -h A)) < (x / 2) /\ (normh` (A -h (F` w))) < (x / 2)) -> (normh` ((F` z) -h (F` w))) < x))
4543, 44syl 10 . . . . . . . . . . . . 13 |- (((x e. RR /\ z e. NN) /\ (A e. H~ /\ (F` w) e. H~)) -> (((normh` ((F` z) -h A)) < (x / 2) /\ (normh` (A -h (F` w))) < (x / 2)) -> (normh` ((F` z) -h (F` w))) < x))
4636, 45sylbird 205 . . . . . . . . . . . 12 |- (((x e. RR /\ z e. NN) /\ (A e. H~ /\ (F` w) e. H~)) -> (((normh` ((F` z) -h A)) < (x / 2) /\ (normh` ((F` w) -h A)) < (x / 2)) -> (normh` ((F` z) -h (F` w))) < x))
476ffvelrni 3800 . . . . . . . . . . . . 13 |- (w e. NN -> (F` w) e. H~)
4847, 13jctil 292 . . . . . . . . . . . 12 |- (w e. NN -> (A e. H~ /\ (F` w) e. H~))
4946, 48sylan2 451 . . . . . . . . . . 11 |- (((x