Metamath Proof Explorer

Theorem cau3

Description: Convert between three-quantifier and four-quantifier versions of the Cauchy criterion. (In particular, the four-quantifier version has no occurrence of j in the assertion, so it can be used with rexanuz and friends.) (Contributed by Mario Carneiro, 15-Feb-2014)

Ref Expression
Hypothesis cau3.1 
|- Z = ( ZZ>= ` M )
Assertion cau3 
|- ( A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) <-> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ A. m e. ( ZZ>= ` k ) ( abs ` ( ( F ` k ) - ( F ` m ) ) ) < x ) )

Proof

Step Hyp Ref Expression
1 cau3.1 
 |-  Z = ( ZZ>= ` M )
2 uzssz 
 |-  ( ZZ>= ` M ) C_ ZZ
3 1 2 eqsstri 
 |-  Z C_ ZZ
4 id 
 |-  ( ( F ` k ) e. CC -> ( F ` k ) e. CC )
5 eleq1 
 |-  ( ( F ` k ) = ( F ` j ) -> ( ( F ` k ) e. CC <-> ( F ` j ) e. CC ) )
6 eleq1 
 |-  ( ( F ` k ) = ( F ` m ) -> ( ( F ` k ) e. CC <-> ( F ` m ) e. CC ) )
7 abssub 
 |-  ( ( ( F ` j ) e. CC /\ ( F ` k ) e. CC ) -> ( abs ` ( ( F ` j ) - ( F ` k ) ) ) = ( abs ` ( ( F ` k ) - ( F ` j ) ) ) )
8 7 3adant1 
 |-  ( ( T. /\ ( F ` j ) e. CC /\ ( F ` k ) e. CC ) -> ( abs ` ( ( F ` j ) - ( F ` k ) ) ) = ( abs ` ( ( F ` k ) - ( F ` j ) ) ) )
9 abssub 
 |-  ( ( ( F ` m ) e. CC /\ ( F ` j ) e. CC ) -> ( abs ` ( ( F ` m ) - ( F ` j ) ) ) = ( abs ` ( ( F ` j ) - ( F ` m ) ) ) )
10 9 3adant1 
 |-  ( ( T. /\ ( F ` m ) e. CC /\ ( F ` j ) e. CC ) -> ( abs ` ( ( F ` m ) - ( F ` j ) ) ) = ( abs ` ( ( F ` j ) - ( F ` m ) ) ) )
11 abs3lem 
 |-  ( ( ( ( F ` k ) e. CC /\ ( F ` m ) e. CC ) /\ ( ( F ` j ) e. CC /\ x e. RR ) ) -> ( ( ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < ( x / 2 ) /\ ( abs ` ( ( F ` j ) - ( F ` m ) ) ) < ( x / 2 ) ) -> ( abs ` ( ( F ` k ) - ( F ` m ) ) ) < x ) )
12 11 3adant1 
 |-  ( ( T. /\ ( ( F ` k ) e. CC /\ ( F ` m ) e. CC ) /\ ( ( F ` j ) e. CC /\ x e. RR ) ) -> ( ( ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < ( x / 2 ) /\ ( abs ` ( ( F ` j ) - ( F ` m ) ) ) < ( x / 2 ) ) -> ( abs ` ( ( F ` k ) - ( F ` m ) ) ) < x ) )
13 3 4 5 6 8 10 12 cau3lem 
 |-  ( T. -> ( A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) <-> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ A. m e. ( ZZ>= ` k ) ( abs ` ( ( F ` k ) - ( F ` m ) ) ) < x ) ) )
14 13 mptru 
 |-  ( A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) <-> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ A. m e. ( ZZ>= ` k ) ( abs ` ( ( F ` k ) - ( F ` m ) ) ) < x ) )