Metamath Proof Explorer

Theorem iscau3

Description: Express the Cauchy sequence property in the more conventional three-quantifier form. (Contributed by NM, 19-Dec-2006) (Revised by Mario Carneiro, 14-Nov-2013)

Ref Expression
Hypotheses iscau3.2 
|- Z = ( ZZ>= ` M )
iscau3.3 
|- ( ph -> D e. ( *Met ` X ) )
iscau3.4 
|- ( ph -> M e. ZZ )
Assertion iscau3 
|- ( ph -> ( F e. ( Cau ` D ) <-> ( F e. ( X ^pm CC ) /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ A. m e. ( ZZ>= ` k ) ( ( F ` k ) D ( F ` m ) ) < x ) ) ) )

Proof

Step Hyp Ref Expression
1 iscau3.2 
 |-  Z = ( ZZ>= ` M )
2 iscau3.3 
 |-  ( ph -> D e. ( *Met ` X ) )
3 iscau3.4 
 |-  ( ph -> M e. ZZ )
4 iscau2 
 |-  ( D e. ( *Met ` X ) -> ( F e. ( Cau ` D ) <-> ( F e. ( X ^pm CC ) /\ A. x e. RR+ E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` j ) ) < x ) ) ) )
5 2 4 syl 
 |-  ( ph -> ( F e. ( Cau ` D ) <-> ( F e. ( X ^pm CC ) /\ A. x e. RR+ E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` j ) ) < x ) ) ) )
6 2 adantr 
 |-  ( ( ph /\ F e. ( X ^pm CC ) ) -> D e. ( *Met ` X ) )
7 ssid 
 |-  ZZ C_ ZZ
8 simpr 
 |-  ( ( k e. dom F /\ ( F ` k ) e. X ) -> ( F ` k ) e. X )
9 eleq1 
 |-  ( ( F ` k ) = ( F ` j ) -> ( ( F ` k ) e. X <-> ( F ` j ) e. X ) )
10 eleq1 
 |-  ( ( F ` k ) = ( F ` m ) -> ( ( F ` k ) e. X <-> ( F ` m ) e. X ) )
11 xmetsym 
 |-  ( ( D e. ( *Met ` X ) /\ ( F ` j ) e. X /\ ( F ` k ) e. X ) -> ( ( F ` j ) D ( F ` k ) ) = ( ( F ` k ) D ( F ` j ) ) )
12 11 fveq2d 
 |-  ( ( D e. ( *Met ` X ) /\ ( F ` j ) e. X /\ ( F ` k ) e. X ) -> ( _I ` ( ( F ` j ) D ( F ` k ) ) ) = ( _I ` ( ( F ` k ) D ( F ` j ) ) ) )
13 xmetsym 
 |-  ( ( D e. ( *Met ` X ) /\ ( F ` m ) e. X /\ ( F ` j ) e. X ) -> ( ( F ` m ) D ( F ` j ) ) = ( ( F ` j ) D ( F ` m ) ) )
14 13 fveq2d 
 |-  ( ( D e. ( *Met ` X ) /\ ( F ` m ) e. X /\ ( F ` j ) e. X ) -> ( _I ` ( ( F ` m ) D ( F ` j ) ) ) = ( _I ` ( ( F ` j ) D ( F ` m ) ) ) )
15 simp1 
 |-  ( ( D e. ( *Met ` X ) /\ ( ( F ` k ) e. X /\ ( F ` m ) e. X ) /\ ( ( F ` j ) e. X /\ x e. RR ) ) -> D e. ( *Met ` X ) )
16 simp2l 
 |-  ( ( D e. ( *Met ` X ) /\ ( ( F ` k ) e. X /\ ( F ` m ) e. X ) /\ ( ( F ` j ) e. X /\ x e. RR ) ) -> ( F ` k ) e. X )
17 simp3l 
 |-  ( ( D e. ( *Met ` X ) /\ ( ( F ` k ) e. X /\ ( F ` m ) e. X ) /\ ( ( F ` j ) e. X /\ x e. RR ) ) -> ( F ` j ) e. X )
18 xmetcl 
 |-  ( ( D e. ( *Met ` X ) /\ ( F ` k ) e. X /\ ( F ` j ) e. X ) -> ( ( F ` k ) D ( F ` j ) ) e. RR* )
19 15 16 17 18 syl3anc 
 |-  ( ( D e. ( *Met ` X ) /\ ( ( F ` k ) e. X /\ ( F ` m ) e. X ) /\ ( ( F ` j ) e. X /\ x e. RR ) ) -> ( ( F ` k ) D ( F ` j ) ) e. RR* )
20 simp2r 
 |-  ( ( D e. ( *Met ` X ) /\ ( ( F ` k ) e. X /\ ( F ` m ) e. X ) /\ ( ( F ` j ) e. X /\ x e. RR ) ) -> ( F ` m ) e. X )
21 xmetcl 
 |-  ( ( D e. ( *Met ` X ) /\ ( F ` j ) e. X /\ ( F ` m ) e. X ) -> ( ( F ` j ) D ( F ` m ) ) e. RR* )
22 15 17 20 21 syl3anc 
 |-  ( ( D e. ( *Met ` X ) /\ ( ( F ` k ) e. X /\ ( F ` m ) e. X ) /\ ( ( F ` j ) e. X /\ x e. RR ) ) -> ( ( F ` j ) D ( F ` m ) ) e. RR* )
23 simp3r 
 |-  ( ( D e. ( *Met ` X ) /\ ( ( F ` k ) e. X /\ ( F ` m ) e. X ) /\ ( ( F ` j ) e. X /\ x e. RR ) ) -> x e. RR )
24 23 rehalfcld 
 |-  ( ( D e. ( *Met ` X ) /\ ( ( F ` k ) e. X /\ ( F ` m ) e. X ) /\ ( ( F ` j ) e. X /\ x e. RR ) ) -> ( x / 2 ) e. RR )
25 24 rexrd 
 |-  ( ( D e. ( *Met ` X ) /\ ( ( F ` k ) e. X /\ ( F ` m ) e. X ) /\ ( ( F ` j ) e. X /\ x e. RR ) ) -> ( x / 2 ) e. RR* )
26 xlt2add 
 |-  ( ( ( ( ( F ` k ) D ( F ` j ) ) e. RR* /\ ( ( F ` j ) D ( F ` m ) ) e. RR* ) /\ ( ( x / 2 ) e. RR* /\ ( x / 2 ) e. RR* ) ) -> ( ( ( ( F ` k ) D ( F ` j ) ) < ( x / 2 ) /\ ( ( F ` j ) D ( F ` m ) ) < ( x / 2 ) ) -> ( ( ( F ` k ) D ( F ` j ) ) +e ( ( F ` j ) D ( F ` m ) ) ) < ( ( x / 2 ) +e ( x / 2 ) ) ) )
27 19 22 25 25 26 syl22anc 
 |-  ( ( D e. ( *Met ` X ) /\ ( ( F ` k ) e. X /\ ( F ` m ) e. X ) /\ ( ( F ` j ) e. X /\ x e. RR ) ) -> ( ( ( ( F ` k ) D ( F ` j ) ) < ( x / 2 ) /\ ( ( F ` j ) D ( F ` m ) ) < ( x / 2 ) ) -> ( ( ( F ` k ) D ( F ` j ) ) +e ( ( F ` j ) D ( F ` m ) ) ) < ( ( x / 2 ) +e ( x / 2 ) ) ) )
28 24 24 rexaddd 
 |-  ( ( D e. ( *Met ` X ) /\ ( ( F ` k ) e. X /\ ( F ` m ) e. X ) /\ ( ( F ` j ) e. X /\ x e. RR ) ) -> ( ( x / 2 ) +e ( x / 2 ) ) = ( ( x / 2 ) + ( x / 2 ) ) )
29 23 recnd 
 |-  ( ( D e. ( *Met ` X ) /\ ( ( F ` k ) e. X /\ ( F ` m ) e. X ) /\ ( ( F ` j ) e. X /\ x e. RR ) ) -> x e. CC )
30 29 2halvesd 
 |-  ( ( D e. ( *Met ` X ) /\ ( ( F ` k ) e. X /\ ( F ` m ) e. X ) /\ ( ( F ` j ) e. X /\ x e. RR ) ) -> ( ( x / 2 ) + ( x / 2 ) ) = x )
31 28 30 eqtrd 
 |-  ( ( D e. ( *Met ` X ) /\ ( ( F ` k ) e. X /\ ( F ` m ) e. X ) /\ ( ( F ` j ) e. X /\ x e. RR ) ) -> ( ( x / 2 ) +e ( x / 2 ) ) = x )
32 31 breq2d 
 |-  ( ( D e. ( *Met ` X ) /\ ( ( F ` k ) e. X /\ ( F ` m ) e. X ) /\ ( ( F ` j ) e. X /\ x e. RR ) ) -> ( ( ( ( F ` k ) D ( F ` j ) ) +e ( ( F ` j ) D ( F ` m ) ) ) < ( ( x / 2 ) +e ( x / 2 ) ) <-> ( ( ( F ` k ) D ( F ` j ) ) +e ( ( F ` j ) D ( F ` m ) ) ) < x ) )
33 xmettri 
 |-  ( ( D e. ( *Met ` X ) /\ ( ( F ` k ) e. X /\ ( F ` m ) e. X /\ ( F ` j ) e. X ) ) -> ( ( F ` k ) D ( F ` m ) ) <_ ( ( ( F ` k ) D ( F ` j ) ) +e ( ( F ` j ) D ( F ` m ) ) ) )
34 15 16 20 17 33 syl13anc 
 |-  ( ( D e. ( *Met ` X ) /\ ( ( F ` k ) e. X /\ ( F ` m ) e. X ) /\ ( ( F ` j ) e. X /\ x e. RR ) ) -> ( ( F ` k ) D ( F ` m ) ) <_ ( ( ( F ` k ) D ( F ` j ) ) +e ( ( F ` j ) D ( F ` m ) ) ) )
35 xmetcl 
 |-  ( ( D e. ( *Met ` X ) /\ ( F ` k ) e. X /\ ( F ` m ) e. X ) -> ( ( F ` k ) D ( F ` m ) ) e. RR* )
36 15 16 20 35 syl3anc 
 |-  ( ( D e. ( *Met ` X ) /\ ( ( F ` k ) e. X /\ ( F ` m ) e. X ) /\ ( ( F ` j ) e. X /\ x e. RR ) ) -> ( ( F ` k ) D ( F ` m ) ) e. RR* )
37 19 22 xaddcld 
 |-  ( ( D e. ( *Met ` X ) /\ ( ( F ` k ) e. X /\ ( F ` m ) e. X ) /\ ( ( F ` j ) e. X /\ x e. RR ) ) -> ( ( ( F ` k ) D ( F ` j ) ) +e ( ( F ` j ) D ( F ` m ) ) ) e. RR* )
38 23 rexrd 
 |-  ( ( D e. ( *Met ` X ) /\ ( ( F ` k ) e. X /\ ( F ` m ) e. X ) /\ ( ( F ` j ) e. X /\ x e. RR ) ) -> x e. RR* )
39 xrlelttr 
 |-  ( ( ( ( F ` k ) D ( F ` m ) ) e. RR* /\ ( ( ( F ` k ) D ( F ` j ) ) +e ( ( F ` j ) D ( F ` m ) ) ) e. RR* /\ x e. RR* ) -> ( ( ( ( F ` k ) D ( F ` m ) ) <_ ( ( ( F ` k ) D ( F ` j ) ) +e ( ( F ` j ) D ( F ` m ) ) ) /\ ( ( ( F ` k ) D ( F ` j ) ) +e ( ( F ` j ) D ( F ` m ) ) ) < x ) -> ( ( F ` k ) D ( F ` m ) ) < x ) )
40 36 37 38 39 syl3anc 
 |-  ( ( D e. ( *Met ` X ) /\ ( ( F ` k ) e. X /\ ( F ` m ) e. X ) /\ ( ( F ` j ) e. X /\ x e. RR ) ) -> ( ( ( ( F ` k ) D ( F ` m ) ) <_ ( ( ( F ` k ) D ( F ` j ) ) +e ( ( F ` j ) D ( F ` m ) ) ) /\ ( ( ( F ` k ) D ( F ` j ) ) +e ( ( F ` j ) D ( F ` m ) ) ) < x ) -> ( ( F ` k ) D ( F ` m ) ) < x ) )
41 34 40 mpand 
 |-  ( ( D e. ( *Met ` X ) /\ ( ( F ` k ) e. X /\ ( F ` m ) e. X ) /\ ( ( F ` j ) e. X /\ x e. RR ) ) -> ( ( ( ( F ` k ) D ( F ` j ) ) +e ( ( F ` j ) D ( F ` m ) ) ) < x -> ( ( F ` k ) D ( F ` m ) ) < x ) )
42 32 41 sylbid 
 |-  ( ( D e. ( *Met ` X ) /\ ( ( F ` k ) e. X /\ ( F ` m ) e. X ) /\ ( ( F ` j ) e. X /\ x e. RR ) ) -> ( ( ( ( F ` k ) D ( F ` j ) ) +e ( ( F ` j ) D ( F ` m ) ) ) < ( ( x / 2 ) +e ( x / 2 ) ) -> ( ( F ` k ) D ( F ` m ) ) < x ) )
43 27 42 syld 
 |-  ( ( D e. ( *Met ` X ) /\ ( ( F ` k ) e. X /\ ( F ` m ) e. X ) /\ ( ( F ` j ) e. X /\ x e. RR ) ) -> ( ( ( ( F ` k ) D ( F ` j ) ) < ( x / 2 ) /\ ( ( F ` j ) D ( F ` m ) ) < ( x / 2 ) ) -> ( ( F ` k ) D ( F ` m ) ) < x ) )
44 ovex 
 |-  ( ( F ` k ) D ( F ` j ) ) e. _V
45 fvi 
 |-  ( ( ( F ` k ) D ( F ` j ) ) e. _V -> ( _I ` ( ( F ` k ) D ( F ` j ) ) ) = ( ( F ` k ) D ( F ` j ) ) )
46 44 45 ax-mp 
 |-  ( _I ` ( ( F ` k ) D ( F ` j ) ) ) = ( ( F ` k ) D ( F ` j ) )
47 46 breq1i 
 |-  ( ( _I ` ( ( F ` k ) D ( F ` j ) ) ) < ( x / 2 ) <-> ( ( F ` k ) D ( F ` j ) ) < ( x / 2 ) )
48 ovex 
 |-  ( ( F ` j ) D ( F ` m ) ) e. _V
49 fvi 
 |-  ( ( ( F ` j ) D ( F ` m ) ) e. _V -> ( _I ` ( ( F ` j ) D ( F ` m ) ) ) = ( ( F ` j ) D ( F ` m ) ) )
50 48 49 ax-mp 
 |-  ( _I ` ( ( F ` j ) D ( F ` m ) ) ) = ( ( F ` j ) D ( F ` m ) )
51 50 breq1i 
 |-  ( ( _I ` ( ( F ` j ) D ( F ` m ) ) ) < ( x / 2 ) <-> ( ( F ` j ) D ( F ` m ) ) < ( x / 2 ) )
52 47 51 anbi12i 
 |-  ( ( ( _I ` ( ( F ` k ) D ( F ` j ) ) ) < ( x / 2 ) /\ ( _I ` ( ( F ` j ) D ( F ` m ) ) ) < ( x / 2 ) ) <-> ( ( ( F ` k ) D ( F ` j ) ) < ( x / 2 ) /\ ( ( F ` j ) D ( F ` m ) ) < ( x / 2 ) ) )
53 ovex 
 |-  ( ( F ` k ) D ( F ` m ) ) e. _V
54 fvi 
 |-  ( ( ( F ` k ) D ( F ` m ) ) e. _V -> ( _I ` ( ( F ` k ) D ( F ` m ) ) ) = ( ( F ` k ) D ( F ` m ) ) )
55 53 54 ax-mp 
 |-  ( _I ` ( ( F ` k ) D ( F ` m ) ) ) = ( ( F ` k ) D ( F ` m ) )
56 55 breq1i 
 |-  ( ( _I ` ( ( F ` k ) D ( F ` m ) ) ) < x <-> ( ( F ` k ) D ( F ` m ) ) < x )
57 43 52 56 3imtr4g 
 |-  ( ( D e. ( *Met ` X ) /\ ( ( F ` k ) e. X /\ ( F ` m ) e. X ) /\ ( ( F ` j ) e. X /\ x e. RR ) ) -> ( ( ( _I ` ( ( F ` k ) D ( F ` j ) ) ) < ( x / 2 ) /\ ( _I ` ( ( F ` j ) D ( F ` m ) ) ) < ( x / 2 ) ) -> ( _I ` ( ( F ` k ) D ( F ` m ) ) ) < x ) )
58 7 8 9 10 12 14 57 cau3lem 
 |-  ( D e. ( *Met ` X ) -> ( A. x e. RR+ E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ( k e. dom F /\ ( F ` k ) e. X ) /\ ( _I ` ( ( F ` k ) D ( F ` j ) ) ) < x ) <-> A. x e. RR+ E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ( k e. dom F /\ ( F ` k ) e. X ) /\ A. m e. ( ZZ>= ` k ) ( _I ` ( ( F ` k ) D ( F ` m ) ) ) < x ) ) )
59 6 58 syl 
 |-  ( ( ph /\ F e. ( X ^pm CC ) ) -> ( A. x e. RR+ E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ( k e. dom F /\ ( F ` k ) e. X ) /\ ( _I ` ( ( F ` k ) D ( F ` j ) ) ) < x ) <-> A. x e. RR+ E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ( k e. dom F /\ ( F ` k ) e. X ) /\ A. m e. ( ZZ>= ` k ) ( _I ` ( ( F ` k ) D ( F ` m ) ) ) < x ) ) )
60 46 breq1i 
 |-  ( ( _I ` ( ( F ` k ) D ( F ` j ) ) ) < x <-> ( ( F ` k ) D ( F ` j ) ) < x )
61 60 anbi2i 
 |-  ( ( ( k e. dom F /\ ( F ` k ) e. X ) /\ ( _I ` ( ( F ` k ) D ( F ` j ) ) ) < x ) <-> ( ( k e. dom F /\ ( F ` k ) e. X ) /\ ( ( F ` k ) D ( F ` j ) ) < x ) )
62 df-3an 
 |-  ( ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` j ) ) < x ) <-> ( ( k e. dom F /\ ( F ` k ) e. X ) /\ ( ( F ` k ) D ( F ` j ) ) < x ) )
63 61 62 bitr4i 
 |-  ( ( ( k e. dom F /\ ( F ` k ) e. X ) /\ ( _I ` ( ( F ` k ) D ( F ` j ) ) ) < x ) <-> ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` j ) ) < x ) )
64 63 ralbii 
 |-  ( A. k e. ( ZZ>= ` j ) ( ( k e. dom F /\ ( F ` k ) e. X ) /\ ( _I ` ( ( F ` k ) D ( F ` j ) ) ) < x ) <-> A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` j ) ) < x ) )
65 64 rexbii 
 |-  ( E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ( k e. dom F /\ ( F ` k ) e. X ) /\ ( _I ` ( ( F ` k ) D ( F ` j ) ) ) < x ) <-> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` j ) ) < x ) )
66 65 ralbii 
 |-  ( A. x e. RR+ E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ( k e. dom F /\ ( F ` k ) e. X ) /\ ( _I ` ( ( F ` k ) D ( F ` j ) ) ) < x ) <-> A. x e. RR+ E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` j ) ) < x ) )
67 56 ralbii 
 |-  ( A. m e. ( ZZ>= ` k ) ( _I ` ( ( F ` k ) D ( F ` m ) ) ) < x <-> A. m e. ( ZZ>= ` k ) ( ( F ` k ) D ( F ` m ) ) < x )
68 67 anbi2i 
 |-  ( ( ( k e. dom F /\ ( F ` k ) e. X ) /\ A. m e. ( ZZ>= ` k ) ( _I ` ( ( F ` k ) D ( F ` m ) ) ) < x ) <-> ( ( k e. dom F /\ ( F ` k ) e. X ) /\ A. m e. ( ZZ>= ` k ) ( ( F ` k ) D ( F ` m ) ) < x ) )
69 df-3an 
 |-  ( ( k e. dom F /\ ( F ` k ) e. X /\ A. m e. ( ZZ>= ` k ) ( ( F ` k ) D ( F ` m ) ) < x ) <-> ( ( k e. dom F /\ ( F ` k ) e. X ) /\ A. m e. ( ZZ>= ` k ) ( ( F ` k ) D ( F ` m ) ) < x ) )
70 68 69 bitr4i 
 |-  ( ( ( k e. dom F /\ ( F ` k ) e. X ) /\ A. m e. ( ZZ>= ` k ) ( _I ` ( ( F ` k ) D ( F ` m ) ) ) < x ) <-> ( k e. dom F /\ ( F ` k ) e. X /\ A. m e. ( ZZ>= ` k ) ( ( F ` k ) D ( F ` m ) ) < x ) )
71 70 ralbii 
 |-  ( A. k e. ( ZZ>= ` j ) ( ( k e. dom F /\ ( F ` k ) e. X ) /\ A. m e. ( ZZ>= ` k ) ( _I ` ( ( F ` k ) D ( F ` m ) ) ) < x ) <-> A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ A. m e. ( ZZ>= ` k ) ( ( F ` k ) D ( F ` m ) ) < x ) )
72 71 rexbii 
 |-  ( E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ( k e. dom F /\ ( F ` k ) e. X ) /\ A. m e. ( ZZ>= ` k ) ( _I ` ( ( F ` k ) D ( F ` m ) ) ) < x ) <-> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ A. m e. ( ZZ>= ` k ) ( ( F ` k ) D ( F ` m ) ) < x ) )
73 72 ralbii 
 |-  ( A. x e. RR+ E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ( k e. dom F /\ ( F ` k ) e. X ) /\ A. m e. ( ZZ>= ` k ) ( _I ` ( ( F ` k ) D ( F ` m ) ) ) < x ) <-> A. x e. RR+ E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ A. m e. ( ZZ>= ` k ) ( ( F ` k ) D ( F ` m ) ) < x ) )
74 59 66 73 3bitr3g 
 |-  ( ( ph /\ F e. ( X ^pm CC ) ) -> ( A. x e. RR+ E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` j ) ) < x ) <-> A. x e. RR+ E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ A. m e. ( ZZ>= ` k ) ( ( F ` k ) D ( F ` m ) ) < x ) ) )
75 3 adantr 
 |-  ( ( ph /\ F e. ( X ^pm CC ) ) -> M e. ZZ )
76 1 rexuz3 
 |-  ( M e. ZZ -> ( E. j e. Z A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ A. m e. ( ZZ>= ` k ) ( ( F ` k ) D ( F ` m ) ) < x ) <-> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ A. m e. ( ZZ>= ` k ) ( ( F ` k ) D ( F ` m ) ) < x ) ) )
77 75 76 syl 
 |-  ( ( ph /\ F e. ( X ^pm CC ) ) -> ( E. j e. Z A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ A. m e. ( ZZ>= ` k ) ( ( F ` k ) D ( F ` m ) ) < x ) <-> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ A. m e. ( ZZ>= ` k ) ( ( F ` k ) D ( F ` m ) ) < x ) ) )
78 77 ralbidv 
 |-  ( ( ph /\ F e. ( X ^pm CC ) ) -> ( A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ A. m e. ( ZZ>= ` k ) ( ( F ` k ) D ( F ` m ) ) < x ) <-> A. x e. RR+ E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ A. m e. ( ZZ>= ` k ) ( ( F ` k ) D ( F ` m ) ) < x ) ) )
79 74 78 bitr4d 
 |-  ( ( ph /\ F e. ( X ^pm CC ) ) -> ( A. x e. RR+ E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` j ) ) < x ) <-> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ A. m e. ( ZZ>= ` k ) ( ( F ` k ) D ( F ` m ) ) < x ) ) )
80 79 pm5.32da 
 |-  ( ph -> ( ( F e. ( X ^pm CC ) /\ A. x e. RR+ E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` j ) ) < x ) ) <-> ( F e. ( X ^pm CC ) /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ A. m e. ( ZZ>= ` k ) ( ( F ` k ) D ( F ` m ) ) < x ) ) ) )
81 5 80 bitrd 
 |-  ( ph -> ( F e. ( Cau ` D ) <-> ( F e. ( X ^pm CC ) /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ A. m e. ( ZZ>= ` k ) ( ( F ` k ) D ( F ` m ) ) < x ) ) ) )