Metamath Proof Explorer

Theorem cau4

Description: Change the base of a Cauchy criterion. (Contributed by Mario Carneiro, 18-Mar-2014)

Ref Expression
Hypotheses cau3.1 
|- Z = ( ZZ>= ` M )
cau4.2 
|- W = ( ZZ>= ` N )
Assertion cau4 
|- ( N e. Z -> ( 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. W A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) ) )

Proof

Step Hyp Ref Expression
1 cau3.1 
 |-  Z = ( ZZ>= ` M )
2 cau4.2 
 |-  W = ( ZZ>= ` N )
3 eluzel2 
 |-  ( N e. ( ZZ>= ` M ) -> M e. ZZ )
4 1 rexuz3 
 |-  ( M e. ZZ -> ( E. j e. Z A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ A. y e. ( ZZ>= ` k ) ( abs ` ( ( F ` k ) - ( F ` y ) ) ) < x ) <-> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ A. y e. ( ZZ>= ` k ) ( abs ` ( ( F ` k ) - ( F ` y ) ) ) < x ) ) )
5 3 4 syl 
 |-  ( N e. ( ZZ>= ` M ) -> ( E. j e. Z A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ A. y e. ( ZZ>= ` k ) ( abs ` ( ( F ` k ) - ( F ` y ) ) ) < x ) <-> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ A. y e. ( ZZ>= ` k ) ( abs ` ( ( F ` k ) - ( F ` y ) ) ) < x ) ) )
6 eluzelz 
 |-  ( N e. ( ZZ>= ` M ) -> N e. ZZ )
7 2 rexuz3 
 |-  ( N e. ZZ -> ( E. j e. W A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ A. y e. ( ZZ>= ` k ) ( abs ` ( ( F ` k ) - ( F ` y ) ) ) < x ) <-> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ A. y e. ( ZZ>= ` k ) ( abs ` ( ( F ` k ) - ( F ` y ) ) ) < x ) ) )
8 6 7 syl 
 |-  ( N e. ( ZZ>= ` M ) -> ( E. j e. W A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ A. y e. ( ZZ>= ` k ) ( abs ` ( ( F ` k ) - ( F ` y ) ) ) < x ) <-> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ A. y e. ( ZZ>= ` k ) ( abs ` ( ( F ` k ) - ( F ` y ) ) ) < x ) ) )
9 5 8 bitr4d 
 |-  ( N e. ( ZZ>= ` M ) -> ( E. j e. Z A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ A. y e. ( ZZ>= ` k ) ( abs ` ( ( F ` k ) - ( F ` y ) ) ) < x ) <-> E. j e. W A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ A. y e. ( ZZ>= ` k ) ( abs ` ( ( F ` k ) - ( F ` y ) ) ) < x ) ) )
10 9 1 eleq2s 
 |-  ( N e. Z -> ( E. j e. Z A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ A. y e. ( ZZ>= ` k ) ( abs ` ( ( F ` k ) - ( F ` y ) ) ) < x ) <-> E. j e. W A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ A. y e. ( ZZ>= ` k ) ( abs ` ( ( F ` k ) - ( F ` y ) ) ) < x ) ) )
11 10 ralbidv 
 |-  ( N e. Z -> ( A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ A. y e. ( ZZ>= ` k ) ( abs ` ( ( F ` k ) - ( F ` y ) ) ) < x ) <-> A. x e. RR+ E. j e. W A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ A. y e. ( ZZ>= ` k ) ( abs ` ( ( F ` k ) - ( F ` y ) ) ) < x ) ) )
12 1 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. y e. ( ZZ>= ` k ) ( abs ` ( ( F ` k ) - ( F ` y ) ) ) < x ) )
13 2 cau3 
 |-  ( A. x e. RR+ E. j e. W A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) <-> A. x e. RR+ E. j e. W A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ A. y e. ( ZZ>= ` k ) ( abs ` ( ( F ` k ) - ( F ` y ) ) ) < x ) )
14 11 12 13 3bitr4g 
 |-  ( N e. Z -> ( 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. W A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) ) )