Metamath Proof Explorer


Theorem climconst

Description: An (eventually) constant sequence converges to its value. (Contributed by NM, 28-Aug-2005) (Revised by Mario Carneiro, 31-Jan-2014)

Ref Expression
Hypotheses climconst.1 Z = M
climconst.2 φ M
climconst.3 φ F V
climconst.4 φ A
climconst.5 φ k Z F k = A
Assertion climconst φ F A

Proof

Step Hyp Ref Expression
1 climconst.1 Z = M
2 climconst.2 φ M
3 climconst.3 φ F V
4 climconst.4 φ A
5 climconst.5 φ k Z F k = A
6 uzid M M M
7 2 6 syl φ M M
8 7 1 eleqtrrdi φ M Z
9 4 subidd φ A A = 0
10 9 fveq2d φ A A = 0
11 abs0 0 = 0
12 10 11 eqtrdi φ A A = 0
13 12 adantr φ x + A A = 0
14 rpgt0 x + 0 < x
15 14 adantl φ x + 0 < x
16 13 15 eqbrtrd φ x + A A < x
17 16 ralrimivw φ x + k Z A A < x
18 fveq2 j = M j = M
19 18 1 eqtr4di j = M j = Z
20 19 raleqdv j = M k j A A < x k Z A A < x
21 20 rspcev M Z k Z A A < x j Z k j A A < x
22 8 17 21 syl2an2r φ x + j Z k j A A < x
23 22 ralrimiva φ x + j Z k j A A < x
24 4 adantr φ k Z A
25 1 2 3 5 4 24 clim2c φ F A x + j Z k j A A < x
26 23 25 mpbird φ F A