Metamath Proof Explorer

Theorem climlec3

Description: Comparison of a constant to the limit of a sequence. (Contributed by Scott Fenton, 5-Jan-2018)

Ref Expression
Hypotheses climlec3.1 
|- Z = ( ZZ>= ` M )
climlec3.2 
|- ( ph -> M e. ZZ )
climlec3.3 
|- ( ph -> B e. RR )
climlec3.4 
|- ( ph -> F ~~> A )
climlec3.5 
|- ( ( ph /\ k e. Z ) -> ( F ` k ) e. RR )
climlec3.6 
|- ( ( ph /\ k e. Z ) -> ( F ` k ) <_ B )
Assertion climlec3 
|- ( ph -> A <_ B )

Proof

Step Hyp Ref Expression
1 climlec3.1 
 |-  Z = ( ZZ>= ` M )
2 climlec3.2 
 |-  ( ph -> M e. ZZ )
3 climlec3.3 
 |-  ( ph -> B e. RR )
4 climlec3.4 
 |-  ( ph -> F ~~> A )
5 climlec3.5 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) e. RR )
6 climlec3.6 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) <_ B )
7 3 renegcld 
 |-  ( ph -> -u B e. RR )
8 0cnd 
 |-  ( ph -> 0 e. CC )
9 1 fvexi 
 |-  Z e. _V
10 9 mptex 
 |-  ( m e. Z |-> -u ( F ` m ) ) e. _V
11 10 a1i 
 |-  ( ph -> ( m e. Z |-> -u ( F ` m ) ) e. _V )
12 5 recnd 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )
13 eqid 
 |-  ( m e. Z |-> -u ( F ` m ) ) = ( m e. Z |-> -u ( F ` m ) )
14 fveq2 
 |-  ( m = k -> ( F ` m ) = ( F ` k ) )
15 14 negeqd 
 |-  ( m = k -> -u ( F ` m ) = -u ( F ` k ) )
16 simpr 
 |-  ( ( ph /\ k e. Z ) -> k e. Z )
17 5 renegcld 
 |-  ( ( ph /\ k e. Z ) -> -u ( F ` k ) e. RR )
18 13 15 16 17 fvmptd3 
 |-  ( ( ph /\ k e. Z ) -> ( ( m e. Z |-> -u ( F ` m ) ) ` k ) = -u ( F ` k ) )
19 df-neg 
 |-  -u ( F ` k ) = ( 0 - ( F ` k ) )
20 18 19 eqtrdi 
 |-  ( ( ph /\ k e. Z ) -> ( ( m e. Z |-> -u ( F ` m ) ) ` k ) = ( 0 - ( F ` k ) ) )
21 1 2 4 8 11 12 20 climsubc2 
 |-  ( ph -> ( m e. Z |-> -u ( F ` m ) ) ~~> ( 0 - A ) )
22 df-neg 
 |-  -u A = ( 0 - A )
23 21 22 breqtrrdi 
 |-  ( ph -> ( m e. Z |-> -u ( F ` m ) ) ~~> -u A )
24 18 17 eqeltrd 
 |-  ( ( ph /\ k e. Z ) -> ( ( m e. Z |-> -u ( F ` m ) ) ` k ) e. RR )
25 3 adantr 
 |-  ( ( ph /\ k e. Z ) -> B e. RR )
26 5 25 lenegd 
 |-  ( ( ph /\ k e. Z ) -> ( ( F ` k ) <_ B <-> -u B <_ -u ( F ` k ) ) )
27 6 26 mpbid 
 |-  ( ( ph /\ k e. Z ) -> -u B <_ -u ( F ` k ) )
28 27 18 breqtrrd 
 |-  ( ( ph /\ k e. Z ) -> -u B <_ ( ( m e. Z |-> -u ( F ` m ) ) ` k ) )
29 1 2 7 23 24 28 climlec2 
 |-  ( ph -> -u B <_ -u A )
30 1 2 4 5 climrecl 
 |-  ( ph -> A e. RR )
31 30 3 lenegd 
 |-  ( ph -> ( A <_ B <-> -u B <_ -u A ) )
32 29 31 mpbird 
 |-  ( ph -> A <_ B )