Metamath Proof Explorer

Theorem climrlim2

Description: Produce a real limit from an integer limit, where the real function is only dependent on the integer part of x . (Contributed by Mario Carneiro, 2-May-2016)

Ref Expression
Hypotheses climrlim2.1 
|- Z = ( ZZ>= ` M )
climrlim2.2 
|- ( n = ( |_ ` x ) -> B = C )
climrlim2.3 
|- ( ph -> A C_ RR )
climrlim2.4 
|- ( ph -> M e. ZZ )
climrlim2.5 
|- ( ph -> ( n e. Z |-> B ) ~~> D )
climrlim2.6 
|- ( ( ph /\ n e. Z ) -> B e. CC )
climrlim2.7 
|- ( ( ph /\ x e. A ) -> M <_ x )
Assertion climrlim2 
|- ( ph -> ( x e. A |-> C ) ~~>r D )

Proof

Step Hyp Ref Expression
1 climrlim2.1 
 |-  Z = ( ZZ>= ` M )
2 climrlim2.2 
 |-  ( n = ( |_ ` x ) -> B = C )
3 climrlim2.3 
 |-  ( ph -> A C_ RR )
4 climrlim2.4 
 |-  ( ph -> M e. ZZ )
5 climrlim2.5 
 |-  ( ph -> ( n e. Z |-> B ) ~~> D )
6 climrlim2.6 
 |-  ( ( ph /\ n e. Z ) -> B e. CC )
7 climrlim2.7 
 |-  ( ( ph /\ x e. A ) -> M <_ x )
8 eluzelz 
 |-  ( j e. ( ZZ>= ` M ) -> j e. ZZ )
9 8 1 eleq2s 
 |-  ( j e. Z -> j e. ZZ )
10 9 ad2antlr 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ j e. Z ) /\ ( x e. A /\ j <_ x ) ) -> j e. ZZ )
11 3 sselda 
 |-  ( ( ph /\ x e. A ) -> x e. RR )
12 11 flcld 
 |-  ( ( ph /\ x e. A ) -> ( |_ ` x ) e. ZZ )
13 12 adantlr 
 |-  ( ( ( ph /\ y e. RR+ ) /\ x e. A ) -> ( |_ ` x ) e. ZZ )
14 13 ad2ant2r 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ j e. Z ) /\ ( x e. A /\ j <_ x ) ) -> ( |_ ` x ) e. ZZ )
15 simprr 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ j e. Z ) /\ ( x e. A /\ j <_ x ) ) -> j <_ x )
16 11 adantlr 
 |-  ( ( ( ph /\ y e. RR+ ) /\ x e. A ) -> x e. RR )
17 16 ad2ant2r 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ j e. Z ) /\ ( x e. A /\ j <_ x ) ) -> x e. RR )
18 flge 
 |-  ( ( x e. RR /\ j e. ZZ ) -> ( j <_ x <-> j <_ ( |_ ` x ) ) )
19 17 10 18 syl2anc 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ j e. Z ) /\ ( x e. A /\ j <_ x ) ) -> ( j <_ x <-> j <_ ( |_ ` x ) ) )
20 15 19 mpbid 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ j e. Z ) /\ ( x e. A /\ j <_ x ) ) -> j <_ ( |_ ` x ) )
21 eluz2 
 |-  ( ( |_ ` x ) e. ( ZZ>= ` j ) <-> ( j e. ZZ /\ ( |_ ` x ) e. ZZ /\ j <_ ( |_ ` x ) ) )
22 10 14 20 21 syl3anbrc 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ j e. Z ) /\ ( x e. A /\ j <_ x ) ) -> ( |_ ` x ) e. ( ZZ>= ` j ) )
23 simpr 
 |-  ( ( ( ( n e. Z |-> B ) ` k ) e. CC /\ ( abs ` ( ( ( n e. Z |-> B ) ` k ) - D ) ) < y ) -> ( abs ` ( ( ( n e. Z |-> B ) ` k ) - D ) ) < y )
24 23 ralimi 
 |-  ( A. k e. ( ZZ>= ` j ) ( ( ( n e. Z |-> B ) ` k ) e. CC /\ ( abs ` ( ( ( n e. Z |-> B ) ` k ) - D ) ) < y ) -> A. k e. ( ZZ>= ` j ) ( abs ` ( ( ( n e. Z |-> B ) ` k ) - D ) ) < y )
25 fveq2 
 |-  ( k = ( |_ ` x ) -> ( ( n e. Z |-> B ) ` k ) = ( ( n e. Z |-> B ) ` ( |_ ` x ) ) )
26 25 fvoveq1d 
 |-  ( k = ( |_ ` x ) -> ( abs ` ( ( ( n e. Z |-> B ) ` k ) - D ) ) = ( abs ` ( ( ( n e. Z |-> B ) ` ( |_ ` x ) ) - D ) ) )
27 26 breq1d 
 |-  ( k = ( |_ ` x ) -> ( ( abs ` ( ( ( n e. Z |-> B ) ` k ) - D ) ) < y <-> ( abs ` ( ( ( n e. Z |-> B ) ` ( |_ ` x ) ) - D ) ) < y ) )
28 27 rspcv 
 |-  ( ( |_ ` x ) e. ( ZZ>= ` j ) -> ( A. k e. ( ZZ>= ` j ) ( abs ` ( ( ( n e. Z |-> B ) ` k ) - D ) ) < y -> ( abs ` ( ( ( n e. Z |-> B ) ` ( |_ ` x ) ) - D ) ) < y ) )
29 22 24 28 syl2im 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ j e. Z ) /\ ( x e. A /\ j <_ x ) ) -> ( A. k e. ( ZZ>= ` j ) ( ( ( n e. Z |-> B ) ` k ) e. CC /\ ( abs ` ( ( ( n e. Z |-> B ) ` k ) - D ) ) < y ) -> ( abs ` ( ( ( n e. Z |-> B ) ` ( |_ ` x ) ) - D ) ) < y ) )
30 eqid 
 |-  ( n e. Z |-> B ) = ( n e. Z |-> B )
31 4 adantr 
 |-  ( ( ph /\ x e. A ) -> M e. ZZ )
32 flge 
 |-  ( ( x e. RR /\ M e. ZZ ) -> ( M <_ x <-> M <_ ( |_ ` x ) ) )
33 11 31 32 syl2anc 
 |-  ( ( ph /\ x e. A ) -> ( M <_ x <-> M <_ ( |_ ` x ) ) )
34 7 33 mpbid 
 |-  ( ( ph /\ x e. A ) -> M <_ ( |_ ` x ) )
35 eluz2 
 |-  ( ( |_ ` x ) e. ( ZZ>= ` M ) <-> ( M e. ZZ /\ ( |_ ` x ) e. ZZ /\ M <_ ( |_ ` x ) ) )
36 31 12 34 35 syl3anbrc 
 |-  ( ( ph /\ x e. A ) -> ( |_ ` x ) e. ( ZZ>= ` M ) )
37 36 1 eleqtrrdi 
 |-  ( ( ph /\ x e. A ) -> ( |_ ` x ) e. Z )
38 2 eleq1d 
 |-  ( n = ( |_ ` x ) -> ( B e. CC <-> C e. CC ) )
39 6 ralrimiva 
 |-  ( ph -> A. n e. Z B e. CC )
40 39 adantr 
 |-  ( ( ph /\ x e. A ) -> A. n e. Z B e. CC )
41 38 40 37 rspcdva 
 |-  ( ( ph /\ x e. A ) -> C e. CC )
42 30 2 37 41 fvmptd3 
 |-  ( ( ph /\ x e. A ) -> ( ( n e. Z |-> B ) ` ( |_ ` x ) ) = C )
43 42 adantlr 
 |-  ( ( ( ph /\ y e. RR+ ) /\ x e. A ) -> ( ( n e. Z |-> B ) ` ( |_ ` x ) ) = C )
44 43 ad2ant2r 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ j e. Z ) /\ ( x e. A /\ j <_ x ) ) -> ( ( n e. Z |-> B ) ` ( |_ ` x ) ) = C )
45 44 fvoveq1d 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ j e. Z ) /\ ( x e. A /\ j <_ x ) ) -> ( abs ` ( ( ( n e. Z |-> B ) ` ( |_ ` x ) ) - D ) ) = ( abs ` ( C - D ) ) )
46 45 breq1d 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ j e. Z ) /\ ( x e. A /\ j <_ x ) ) -> ( ( abs ` ( ( ( n e. Z |-> B ) ` ( |_ ` x ) ) - D ) ) < y <-> ( abs ` ( C - D ) ) < y ) )
47 29 46 sylibd 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ j e. Z ) /\ ( x e. A /\ j <_ x ) ) -> ( A. k e. ( ZZ>= ` j ) ( ( ( n e. Z |-> B ) ` k ) e. CC /\ ( abs ` ( ( ( n e. Z |-> B ) ` k ) - D ) ) < y ) -> ( abs ` ( C - D ) ) < y ) )
48 47 expr 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ j e. Z ) /\ x e. A ) -> ( j <_ x -> ( A. k e. ( ZZ>= ` j ) ( ( ( n e. Z |-> B ) ` k ) e. CC /\ ( abs ` ( ( ( n e. Z |-> B ) ` k ) - D ) ) < y ) -> ( abs ` ( C - D ) ) < y ) ) )
49 48 com23 
 |-  ( ( ( ( ph /\ y e. RR+ ) /\ j e. Z ) /\ x e. A ) -> ( A. k e. ( ZZ>= ` j ) ( ( ( n e. Z |-> B ) ` k ) e. CC /\ ( abs ` ( ( ( n e. Z |-> B ) ` k ) - D ) ) < y ) -> ( j <_ x -> ( abs ` ( C - D ) ) < y ) ) )
50 49 ralrimdva 
 |-  ( ( ( ph /\ y e. RR+ ) /\ j e. Z ) -> ( A. k e. ( ZZ>= ` j ) ( ( ( n e. Z |-> B ) ` k ) e. CC /\ ( abs ` ( ( ( n e. Z |-> B ) ` k ) - D ) ) < y ) -> A. x e. A ( j <_ x -> ( abs ` ( C - D ) ) < y ) ) )
51 eluzelre 
 |-  ( j e. ( ZZ>= ` M ) -> j e. RR )
52 51 1 eleq2s 
 |-  ( j e. Z -> j e. RR )
53 52 adantl 
 |-  ( ( ( ph /\ y e. RR+ ) /\ j e. Z ) -> j e. RR )
54 50 53 jctild 
 |-  ( ( ( ph /\ y e. RR+ ) /\ j e. Z ) -> ( A. k e. ( ZZ>= ` j ) ( ( ( n e. Z |-> B ) ` k ) e. CC /\ ( abs ` ( ( ( n e. Z |-> B ) ` k ) - D ) ) < y ) -> ( j e. RR /\ A. x e. A ( j <_ x -> ( abs ` ( C - D ) ) < y ) ) ) )
55 54 expimpd 
 |-  ( ( ph /\ y e. RR+ ) -> ( ( j e. Z /\ A. k e. ( ZZ>= ` j ) ( ( ( n e. Z |-> B ) ` k ) e. CC /\ ( abs ` ( ( ( n e. Z |-> B ) ` k ) - D ) ) < y ) ) -> ( j e. RR /\ A. x e. A ( j <_ x -> ( abs ` ( C - D ) ) < y ) ) ) )
56 55 reximdv2 
 |-  ( ( ph /\ y e. RR+ ) -> ( E. j e. Z A. k e. ( ZZ>= ` j ) ( ( ( n e. Z |-> B ) ` k ) e. CC /\ ( abs ` ( ( ( n e. Z |-> B ) ` k ) - D ) ) < y ) -> E. j e. RR A. x e. A ( j <_ x -> ( abs ` ( C - D ) ) < y ) ) )
57 56 ralimdva 
 |-  ( ph -> ( A. y e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( ( ( n e. Z |-> B ) ` k ) e. CC /\ ( abs ` ( ( ( n e. Z |-> B ) ` k ) - D ) ) < y ) -> A. y e. RR+ E. j e. RR A. x e. A ( j <_ x -> ( abs ` ( C - D ) ) < y ) ) )
58 57 adantld 
 |-  ( ph -> ( ( D e. CC /\ A. y e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( ( ( n e. Z |-> B ) ` k ) e. CC /\ ( abs ` ( ( ( n e. Z |-> B ) ` k ) - D ) ) < y ) ) -> A. y e. RR+ E. j e. RR A. x e. A ( j <_ x -> ( abs ` ( C - D ) ) < y ) ) )
59 climrel 
 |-  Rel ~~>
60 59 brrelex1i 
 |-  ( ( n e. Z |-> B ) ~~> D -> ( n e. Z |-> B ) e. _V )
61 5 60 syl 
 |-  ( ph -> ( n e. Z |-> B ) e. _V )
62 eqidd 
 |-  ( ( ph /\ k e. Z ) -> ( ( n e. Z |-> B ) ` k ) = ( ( n e. Z |-> B ) ` k ) )
63 1 4 61 62 clim2 
 |-  ( ph -> ( ( n e. Z |-> B ) ~~> D <-> ( D e. CC /\ A. y e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( ( ( n e. Z |-> B ) ` k ) e. CC /\ ( abs ` ( ( ( n e. Z |-> B ) ` k ) - D ) ) < y ) ) ) )
64 41 ralrimiva 
 |-  ( ph -> A. x e. A C e. CC )
65 climcl 
 |-  ( ( n e. Z |-> B ) ~~> D -> D e. CC )
66 5 65 syl 
 |-  ( ph -> D e. CC )
67 64 3 66 rlim2 
 |-  ( ph -> ( ( x e. A |-> C ) ~~>r D <-> A. y e. RR+ E. j e. RR A. x e. A ( j <_ x -> ( abs ` ( C - D ) ) < y ) ) )
68 58 63 67 3imtr4d 
 |-  ( ph -> ( ( n e. Z |-> B ) ~~> D -> ( x e. A |-> C ) ~~>r D ) )
69 5 68 mpd 
 |-  ( ph -> ( x e. A |-> C ) ~~>r D )