Metamath Proof Explorer

Theorem caubl

Description: Sufficient condition to ensure a sequence of nested balls is Cauchy. (Contributed by Mario Carneiro, 18-Jan-2014) (Revised by Mario Carneiro, 1-May-2014)

Ref Expression
Hypotheses caubl.2 
|- ( ph -> D e. ( *Met ` X ) )
caubl.3 
|- ( ph -> F : NN --> ( X X. RR+ ) )
caubl.4 
|- ( ph -> A. n e. NN ( ( ball ` D ) ` ( F ` ( n + 1 ) ) ) C_ ( ( ball ` D ) ` ( F ` n ) ) )
caubl.5 
|- ( ph -> A. r e. RR+ E. n e. NN ( 2nd ` ( F ` n ) ) < r )
Assertion caubl 
|- ( ph -> ( 1st o. F ) e. ( Cau ` D ) )

Proof

Step Hyp Ref Expression
1 caubl.2 
 |-  ( ph -> D e. ( *Met ` X ) )
2 caubl.3 
 |-  ( ph -> F : NN --> ( X X. RR+ ) )
3 caubl.4 
 |-  ( ph -> A. n e. NN ( ( ball ` D ) ` ( F ` ( n + 1 ) ) ) C_ ( ( ball ` D ) ` ( F ` n ) ) )
4 caubl.5 
 |-  ( ph -> A. r e. RR+ E. n e. NN ( 2nd ` ( F ` n ) ) < r )
5 2fveq3 
 |-  ( r = n -> ( ( ball ` D ) ` ( F ` r ) ) = ( ( ball ` D ) ` ( F ` n ) ) )
6 5 sseq1d 
 |-  ( r = n -> ( ( ( ball ` D ) ` ( F ` r ) ) C_ ( ( ball ` D ) ` ( F ` n ) ) <-> ( ( ball ` D ) ` ( F ` n ) ) C_ ( ( ball ` D ) ` ( F ` n ) ) ) )
7 6 imbi2d 
 |-  ( r = n -> ( ( ( ph /\ n e. NN ) -> ( ( ball ` D ) ` ( F ` r ) ) C_ ( ( ball ` D ) ` ( F ` n ) ) ) <-> ( ( ph /\ n e. NN ) -> ( ( ball ` D ) ` ( F ` n ) ) C_ ( ( ball ` D ) ` ( F ` n ) ) ) ) )
8 2fveq3 
 |-  ( r = k -> ( ( ball ` D ) ` ( F ` r ) ) = ( ( ball ` D ) ` ( F ` k ) ) )
9 8 sseq1d 
 |-  ( r = k -> ( ( ( ball ` D ) ` ( F ` r ) ) C_ ( ( ball ` D ) ` ( F ` n ) ) <-> ( ( ball ` D ) ` ( F ` k ) ) C_ ( ( ball ` D ) ` ( F ` n ) ) ) )
10 9 imbi2d 
 |-  ( r = k -> ( ( ( ph /\ n e. NN ) -> ( ( ball ` D ) ` ( F ` r ) ) C_ ( ( ball ` D ) ` ( F ` n ) ) ) <-> ( ( ph /\ n e. NN ) -> ( ( ball ` D ) ` ( F ` k ) ) C_ ( ( ball ` D ) ` ( F ` n ) ) ) ) )
11 2fveq3 
 |-  ( r = ( k + 1 ) -> ( ( ball ` D ) ` ( F ` r ) ) = ( ( ball ` D ) ` ( F ` ( k + 1 ) ) ) )
12 11 sseq1d 
 |-  ( r = ( k + 1 ) -> ( ( ( ball ` D ) ` ( F ` r ) ) C_ ( ( ball ` D ) ` ( F ` n ) ) <-> ( ( ball ` D ) ` ( F ` ( k + 1 ) ) ) C_ ( ( ball ` D ) ` ( F ` n ) ) ) )
13 12 imbi2d 
 |-  ( r = ( k + 1 ) -> ( ( ( ph /\ n e. NN ) -> ( ( ball ` D ) ` ( F ` r ) ) C_ ( ( ball ` D ) ` ( F ` n ) ) ) <-> ( ( ph /\ n e. NN ) -> ( ( ball ` D ) ` ( F ` ( k + 1 ) ) ) C_ ( ( ball ` D ) ` ( F ` n ) ) ) ) )
14 ssid 
 |-  ( ( ball ` D ) ` ( F ` n ) ) C_ ( ( ball ` D ) ` ( F ` n ) )
15 14 2a1i 
 |-  ( n e. ZZ -> ( ( ph /\ n e. NN ) -> ( ( ball ` D ) ` ( F ` n ) ) C_ ( ( ball ` D ) ` ( F ` n ) ) ) )
16 eluznn 
 |-  ( ( n e. NN /\ k e. ( ZZ>= ` n ) ) -> k e. NN )
17 fvoveq1 
 |-  ( n = k -> ( F ` ( n + 1 ) ) = ( F ` ( k + 1 ) ) )
18 17 fveq2d 
 |-  ( n = k -> ( ( ball ` D ) ` ( F ` ( n + 1 ) ) ) = ( ( ball ` D ) ` ( F ` ( k + 1 ) ) ) )
19 2fveq3 
 |-  ( n = k -> ( ( ball ` D ) ` ( F ` n ) ) = ( ( ball ` D ) ` ( F ` k ) ) )
20 18 19 sseq12d 
 |-  ( n = k -> ( ( ( ball ` D ) ` ( F ` ( n + 1 ) ) ) C_ ( ( ball ` D ) ` ( F ` n ) ) <-> ( ( ball ` D ) ` ( F ` ( k + 1 ) ) ) C_ ( ( ball ` D ) ` ( F ` k ) ) ) )
21 20 rspccva 
 |-  ( ( A. n e. NN ( ( ball ` D ) ` ( F ` ( n + 1 ) ) ) C_ ( ( ball ` D ) ` ( F ` n ) ) /\ k e. NN ) -> ( ( ball ` D ) ` ( F ` ( k + 1 ) ) ) C_ ( ( ball ` D ) ` ( F ` k ) ) )
22 3 16 21 syl2an 
 |-  ( ( ph /\ ( n e. NN /\ k e. ( ZZ>= ` n ) ) ) -> ( ( ball ` D ) ` ( F ` ( k + 1 ) ) ) C_ ( ( ball ` D ) ` ( F ` k ) ) )
23 22 anassrs 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( ZZ>= ` n ) ) -> ( ( ball ` D ) ` ( F ` ( k + 1 ) ) ) C_ ( ( ball ` D ) ` ( F ` k ) ) )
24 sstr2 
 |-  ( ( ( ball ` D ) ` ( F ` ( k + 1 ) ) ) C_ ( ( ball ` D ) ` ( F ` k ) ) -> ( ( ( ball ` D ) ` ( F ` k ) ) C_ ( ( ball ` D ) ` ( F ` n ) ) -> ( ( ball ` D ) ` ( F ` ( k + 1 ) ) ) C_ ( ( ball ` D ) ` ( F ` n ) ) ) )
25 23 24 syl 
 |-  ( ( ( ph /\ n e. NN ) /\ k e. ( ZZ>= ` n ) ) -> ( ( ( ball ` D ) ` ( F ` k ) ) C_ ( ( ball ` D ) ` ( F ` n ) ) -> ( ( ball ` D ) ` ( F ` ( k + 1 ) ) ) C_ ( ( ball ` D ) ` ( F ` n ) ) ) )
26 25 expcom 
 |-  ( k e. ( ZZ>= ` n ) -> ( ( ph /\ n e. NN ) -> ( ( ( ball ` D ) ` ( F ` k ) ) C_ ( ( ball ` D ) ` ( F ` n ) ) -> ( ( ball ` D ) ` ( F ` ( k + 1 ) ) ) C_ ( ( ball ` D ) ` ( F ` n ) ) ) ) )
27 26 a2d 
 |-  ( k e. ( ZZ>= ` n ) -> ( ( ( ph /\ n e. NN ) -> ( ( ball ` D ) ` ( F ` k ) ) C_ ( ( ball ` D ) ` ( F ` n ) ) ) -> ( ( ph /\ n e. NN ) -> ( ( ball ` D ) ` ( F ` ( k + 1 ) ) ) C_ ( ( ball ` D ) ` ( F ` n ) ) ) ) )
28 7 10 13 10 15 27 uzind4 
 |-  ( k e. ( ZZ>= ` n ) -> ( ( ph /\ n e. NN ) -> ( ( ball ` D ) ` ( F ` k ) ) C_ ( ( ball ` D ) ` ( F ` n ) ) ) )
29 28 com12 
 |-  ( ( ph /\ n e. NN ) -> ( k e. ( ZZ>= ` n ) -> ( ( ball ` D ) ` ( F ` k ) ) C_ ( ( ball ` D ) ` ( F ` n ) ) ) )
30 29 ad2ant2r 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( n e. NN /\ ( 2nd ` ( F ` n ) ) < r ) ) -> ( k e. ( ZZ>= ` n ) -> ( ( ball ` D ) ` ( F ` k ) ) C_ ( ( ball ` D ) ` ( F ` n ) ) ) )
31 relxp 
 |-  Rel ( X X. RR+ )
32 2 ad3antrrr 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( n e. NN /\ ( 2nd ` ( F ` n ) ) < r ) ) /\ k e. ( ZZ>= ` n ) ) -> F : NN --> ( X X. RR+ ) )
33 simplrl 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( n e. NN /\ ( 2nd ` ( F ` n ) ) < r ) ) /\ k e. ( ZZ>= ` n ) ) -> n e. NN )
34 32 33 ffvelrnd 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( n e. NN /\ ( 2nd ` ( F ` n ) ) < r ) ) /\ k e. ( ZZ>= ` n ) ) -> ( F ` n ) e. ( X X. RR+ ) )
35 1st2nd 
 |-  ( ( Rel ( X X. RR+ ) /\ ( F ` n ) e. ( X X. RR+ ) ) -> ( F ` n ) = <. ( 1st ` ( F ` n ) ) , ( 2nd ` ( F ` n ) ) >. )
36 31 34 35 sylancr 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( n e. NN /\ ( 2nd ` ( F ` n ) ) < r ) ) /\ k e. ( ZZ>= ` n ) ) -> ( F ` n ) = <. ( 1st ` ( F ` n ) ) , ( 2nd ` ( F ` n ) ) >. )
37 36 fveq2d 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( n e. NN /\ ( 2nd ` ( F ` n ) ) < r ) ) /\ k e. ( ZZ>= ` n ) ) -> ( ( ball ` D ) ` ( F ` n ) ) = ( ( ball ` D ) ` <. ( 1st ` ( F ` n ) ) , ( 2nd ` ( F ` n ) ) >. ) )
38 df-ov 
 |-  ( ( 1st ` ( F ` n ) ) ( ball ` D ) ( 2nd ` ( F ` n ) ) ) = ( ( ball ` D ) ` <. ( 1st ` ( F ` n ) ) , ( 2nd ` ( F ` n ) ) >. )
39 37 38 eqtr4di 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( n e. NN /\ ( 2nd ` ( F ` n ) ) < r ) ) /\ k e. ( ZZ>= ` n ) ) -> ( ( ball ` D ) ` ( F ` n ) ) = ( ( 1st ` ( F ` n ) ) ( ball ` D ) ( 2nd ` ( F ` n ) ) ) )
40 1 ad3antrrr 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( n e. NN /\ ( 2nd ` ( F ` n ) ) < r ) ) /\ k e. ( ZZ>= ` n ) ) -> D e. ( *Met ` X ) )
41 xp1st 
 |-  ( ( F ` n ) e. ( X X. RR+ ) -> ( 1st ` ( F ` n ) ) e. X )
42 34 41 syl 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( n e. NN /\ ( 2nd ` ( F ` n ) ) < r ) ) /\ k e. ( ZZ>= ` n ) ) -> ( 1st ` ( F ` n ) ) e. X )
43 xp2nd 
 |-  ( ( F ` n ) e. ( X X. RR+ ) -> ( 2nd ` ( F ` n ) ) e. RR+ )
44 34 43 syl 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( n e. NN /\ ( 2nd ` ( F ` n ) ) < r ) ) /\ k e. ( ZZ>= ` n ) ) -> ( 2nd ` ( F ` n ) ) e. RR+ )
45 44 rpxrd 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( n e. NN /\ ( 2nd ` ( F ` n ) ) < r ) ) /\ k e. ( ZZ>= ` n ) ) -> ( 2nd ` ( F ` n ) ) e. RR* )
46 simpllr 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( n e. NN /\ ( 2nd ` ( F ` n ) ) < r ) ) /\ k e. ( ZZ>= ` n ) ) -> r e. RR+ )
47 46 rpxrd 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( n e. NN /\ ( 2nd ` ( F ` n ) ) < r ) ) /\ k e. ( ZZ>= ` n ) ) -> r e. RR* )
48 simplrr 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( n e. NN /\ ( 2nd ` ( F ` n ) ) < r ) ) /\ k e. ( ZZ>= ` n ) ) -> ( 2nd ` ( F ` n ) ) < r )
49 rpre 
 |-  ( ( 2nd ` ( F ` n ) ) e. RR+ -> ( 2nd ` ( F ` n ) ) e. RR )
50 rpre 
 |-  ( r e. RR+ -> r e. RR )
51 ltle 
 |-  ( ( ( 2nd ` ( F ` n ) ) e. RR /\ r e. RR ) -> ( ( 2nd ` ( F ` n ) ) < r -> ( 2nd ` ( F ` n ) ) <_ r ) )
52 49 50 51 syl2an 
 |-  ( ( ( 2nd ` ( F ` n ) ) e. RR+ /\ r e. RR+ ) -> ( ( 2nd ` ( F ` n ) ) < r -> ( 2nd ` ( F ` n ) ) <_ r ) )
53 44 46 52 syl2anc 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( n e. NN /\ ( 2nd ` ( F ` n ) ) < r ) ) /\ k e. ( ZZ>= ` n ) ) -> ( ( 2nd ` ( F ` n ) ) < r -> ( 2nd ` ( F ` n ) ) <_ r ) )
54 48 53 mpd 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( n e. NN /\ ( 2nd ` ( F ` n ) ) < r ) ) /\ k e. ( ZZ>= ` n ) ) -> ( 2nd ` ( F ` n ) ) <_ r )
55 ssbl 
 |-  ( ( ( D e. ( *Met ` X ) /\ ( 1st ` ( F ` n ) ) e. X ) /\ ( ( 2nd ` ( F ` n ) ) e. RR* /\ r e. RR* ) /\ ( 2nd ` ( F ` n ) ) <_ r ) -> ( ( 1st ` ( F ` n ) ) ( ball ` D ) ( 2nd ` ( F ` n ) ) ) C_ ( ( 1st ` ( F ` n ) ) ( ball ` D ) r ) )
56 40 42 45 47 54 55 syl221anc 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( n e. NN /\ ( 2nd ` ( F ` n ) ) < r ) ) /\ k e. ( ZZ>= ` n ) ) -> ( ( 1st ` ( F ` n ) ) ( ball ` D ) ( 2nd ` ( F ` n ) ) ) C_ ( ( 1st ` ( F ` n ) ) ( ball ` D ) r ) )
57 39 56 eqsstrd 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( n e. NN /\ ( 2nd ` ( F ` n ) ) < r ) ) /\ k e. ( ZZ>= ` n ) ) -> ( ( ball ` D ) ` ( F ` n ) ) C_ ( ( 1st ` ( F ` n ) ) ( ball ` D ) r ) )
58 sstr2 
 |-  ( ( ( ball ` D ) ` ( F ` k ) ) C_ ( ( ball ` D ) ` ( F ` n ) ) -> ( ( ( ball ` D ) ` ( F ` n ) ) C_ ( ( 1st ` ( F ` n ) ) ( ball ` D ) r ) -> ( ( ball ` D ) ` ( F ` k ) ) C_ ( ( 1st ` ( F ` n ) ) ( ball ` D ) r ) ) )
59 57 58 syl5com 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( n e. NN /\ ( 2nd ` ( F ` n ) ) < r ) ) /\ k e. ( ZZ>= ` n ) ) -> ( ( ( ball ` D ) ` ( F ` k ) ) C_ ( ( ball ` D ) ` ( F ` n ) ) -> ( ( ball ` D ) ` ( F ` k ) ) C_ ( ( 1st ` ( F ` n ) ) ( ball ` D ) r ) ) )
60 simprl 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( n e. NN /\ ( 2nd ` ( F ` n ) ) < r ) ) -> n e. NN )
61 60 16 sylan 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( n e. NN /\ ( 2nd ` ( F ` n ) ) < r ) ) /\ k e. ( ZZ>= ` n ) ) -> k e. NN )
62 32 61 ffvelrnd 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( n e. NN /\ ( 2nd ` ( F ` n ) ) < r ) ) /\ k e. ( ZZ>= ` n ) ) -> ( F ` k ) e. ( X X. RR+ ) )
63 xp1st 
 |-  ( ( F ` k ) e. ( X X. RR+ ) -> ( 1st ` ( F ` k ) ) e. X )
64 62 63 syl 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( n e. NN /\ ( 2nd ` ( F ` n ) ) < r ) ) /\ k e. ( ZZ>= ` n ) ) -> ( 1st ` ( F ` k ) ) e. X )
65 xp2nd 
 |-  ( ( F ` k ) e. ( X X. RR+ ) -> ( 2nd ` ( F ` k ) ) e. RR+ )
66 62 65 syl 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( n e. NN /\ ( 2nd ` ( F ` n ) ) < r ) ) /\ k e. ( ZZ>= ` n ) ) -> ( 2nd ` ( F ` k ) ) e. RR+ )
67 blcntr 
 |-  ( ( D e. ( *Met ` X ) /\ ( 1st ` ( F ` k ) ) e. X /\ ( 2nd ` ( F ` k ) ) e. RR+ ) -> ( 1st ` ( F ` k ) ) e. ( ( 1st ` ( F ` k ) ) ( ball ` D ) ( 2nd ` ( F ` k ) ) ) )
68 40 64 66 67 syl3anc 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( n e. NN /\ ( 2nd ` ( F ` n ) ) < r ) ) /\ k e. ( ZZ>= ` n ) ) -> ( 1st ` ( F ` k ) ) e. ( ( 1st ` ( F ` k ) ) ( ball ` D ) ( 2nd ` ( F ` k ) ) ) )
69 1st2nd 
 |-  ( ( Rel ( X X. RR+ ) /\ ( F ` k ) e. ( X X. RR+ ) ) -> ( F ` k ) = <. ( 1st ` ( F ` k ) ) , ( 2nd ` ( F ` k ) ) >. )
70 31 62 69 sylancr 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( n e. NN /\ ( 2nd ` ( F ` n ) ) < r ) ) /\ k e. ( ZZ>= ` n ) ) -> ( F ` k ) = <. ( 1st ` ( F ` k ) ) , ( 2nd ` ( F ` k ) ) >. )
71 70 fveq2d 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( n e. NN /\ ( 2nd ` ( F ` n ) ) < r ) ) /\ k e. ( ZZ>= ` n ) ) -> ( ( ball ` D ) ` ( F ` k ) ) = ( ( ball ` D ) ` <. ( 1st ` ( F ` k ) ) , ( 2nd ` ( F ` k ) ) >. ) )
72 df-ov 
 |-  ( ( 1st ` ( F ` k ) ) ( ball ` D ) ( 2nd ` ( F ` k ) ) ) = ( ( ball ` D ) ` <. ( 1st ` ( F ` k ) ) , ( 2nd ` ( F ` k ) ) >. )
73 71 72 eqtr4di 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( n e. NN /\ ( 2nd ` ( F ` n ) ) < r ) ) /\ k e. ( ZZ>= ` n ) ) -> ( ( ball ` D ) ` ( F ` k ) ) = ( ( 1st ` ( F ` k ) ) ( ball ` D ) ( 2nd ` ( F ` k ) ) ) )
74 68 73 eleqtrrd 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( n e. NN /\ ( 2nd ` ( F ` n ) ) < r ) ) /\ k e. ( ZZ>= ` n ) ) -> ( 1st ` ( F ` k ) ) e. ( ( ball ` D ) ` ( F ` k ) ) )
75 ssel 
 |-  ( ( ( ball ` D ) ` ( F ` k ) ) C_ ( ( 1st ` ( F ` n ) ) ( ball ` D ) r ) -> ( ( 1st ` ( F ` k ) ) e. ( ( ball ` D ) ` ( F ` k ) ) -> ( 1st ` ( F ` k ) ) e. ( ( 1st ` ( F ` n ) ) ( ball ` D ) r ) ) )
76 59 74 75 syl6ci 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( n e. NN /\ ( 2nd ` ( F ` n ) ) < r ) ) /\ k e. ( ZZ>= ` n ) ) -> ( ( ( ball ` D ) ` ( F ` k ) ) C_ ( ( ball ` D ) ` ( F ` n ) ) -> ( 1st ` ( F ` k ) ) e. ( ( 1st ` ( F ` n ) ) ( ball ` D ) r ) ) )
77 elbl2 
 |-  ( ( ( D e. ( *Met ` X ) /\ r e. RR* ) /\ ( ( 1st ` ( F ` n ) ) e. X /\ ( 1st ` ( F ` k ) ) e. X ) ) -> ( ( 1st ` ( F ` k ) ) e. ( ( 1st ` ( F ` n ) ) ( ball ` D ) r ) <-> ( ( 1st ` ( F ` n ) ) D ( 1st ` ( F ` k ) ) ) < r ) )
78 40 47 42 64 77 syl22anc 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( n e. NN /\ ( 2nd ` ( F ` n ) ) < r ) ) /\ k e. ( ZZ>= ` n ) ) -> ( ( 1st ` ( F ` k ) ) e. ( ( 1st ` ( F ` n ) ) ( ball ` D ) r ) <-> ( ( 1st ` ( F ` n ) ) D ( 1st ` ( F ` k ) ) ) < r ) )
79 76 78 sylibd 
 |-  ( ( ( ( ph /\ r e. RR+ ) /\ ( n e. NN /\ ( 2nd ` ( F ` n ) ) < r ) ) /\ k e. ( ZZ>= ` n ) ) -> ( ( ( ball ` D ) ` ( F ` k ) ) C_ ( ( ball ` D ) ` ( F ` n ) ) -> ( ( 1st ` ( F ` n ) ) D ( 1st ` ( F ` k ) ) ) < r ) )
80 79 ex 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( n e. NN /\ ( 2nd ` ( F ` n ) ) < r ) ) -> ( k e. ( ZZ>= ` n ) -> ( ( ( ball ` D ) ` ( F ` k ) ) C_ ( ( ball ` D ) ` ( F ` n ) ) -> ( ( 1st ` ( F ` n ) ) D ( 1st ` ( F ` k ) ) ) < r ) ) )
81 30 80 mpdd 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( n e. NN /\ ( 2nd ` ( F ` n ) ) < r ) ) -> ( k e. ( ZZ>= ` n ) -> ( ( 1st ` ( F ` n ) ) D ( 1st ` ( F ` k ) ) ) < r ) )
82 81 ralrimiv 
 |-  ( ( ( ph /\ r e. RR+ ) /\ ( n e. NN /\ ( 2nd ` ( F ` n ) ) < r ) ) -> A. k e. ( ZZ>= ` n ) ( ( 1st ` ( F ` n ) ) D ( 1st ` ( F ` k ) ) ) < r )
83 82 expr 
 |-  ( ( ( ph /\ r e. RR+ ) /\ n e. NN ) -> ( ( 2nd ` ( F ` n ) ) < r -> A. k e. ( ZZ>= ` n ) ( ( 1st ` ( F ` n ) ) D ( 1st ` ( F ` k ) ) ) < r ) )
84 83 reximdva 
 |-  ( ( ph /\ r e. RR+ ) -> ( E. n e. NN ( 2nd ` ( F ` n ) ) < r -> E. n e. NN A. k e. ( ZZ>= ` n ) ( ( 1st ` ( F ` n ) ) D ( 1st ` ( F ` k ) ) ) < r ) )
85 84 ralimdva 
 |-  ( ph -> ( A. r e. RR+ E. n e. NN ( 2nd ` ( F ` n ) ) < r -> A. r e. RR+ E. n e. NN A. k e. ( ZZ>= ` n ) ( ( 1st ` ( F ` n ) ) D ( 1st ` ( F ` k ) ) ) < r ) )
86 4 85 mpd 
 |-  ( ph -> A. r e. RR+ E. n e. NN A. k e. ( ZZ>= ` n ) ( ( 1st ` ( F ` n ) ) D ( 1st ` ( F ` k ) ) ) < r )
87 nnuz 
 |-  NN = ( ZZ>= ` 1 )
88 1zzd 
 |-  ( ph -> 1 e. ZZ )
89 fvco3 
 |-  ( ( F : NN --> ( X X. RR+ ) /\ k e. NN ) -> ( ( 1st o. F ) ` k ) = ( 1st ` ( F ` k ) ) )
90 2 89 sylan 
 |-  ( ( ph /\ k e. NN ) -> ( ( 1st o. F ) ` k ) = ( 1st ` ( F ` k ) ) )
91 fvco3 
 |-  ( ( F : NN --> ( X X. RR+ ) /\ n e. NN ) -> ( ( 1st o. F ) ` n ) = ( 1st ` ( F ` n ) ) )
92 2 91 sylan 
 |-  ( ( ph /\ n e. NN ) -> ( ( 1st o. F ) ` n ) = ( 1st ` ( F ` n ) ) )
93 1stcof 
 |-  ( F : NN --> ( X X. RR+ ) -> ( 1st o. F ) : NN --> X )
94 2 93 syl 
 |-  ( ph -> ( 1st o. F ) : NN --> X )
95 87 1 88 90 92 94 iscauf 
 |-  ( ph -> ( ( 1st o. F ) e. ( Cau ` D ) <-> A. r e. RR+ E. n e. NN A. k e. ( ZZ>= ` n ) ( ( 1st ` ( F ` n ) ) D ( 1st ` ( F ` k ) ) ) < r ) )
96 86 95 mpbird 
 |-  ( ph -> ( 1st o. F ) e. ( Cau ` D ) )