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 ) ) |