Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  climconst Unicode version

Theorem climconst 9811
 Description: An (eventually) constant sequence converges to its value. (Contributed by NM, 28-Aug-2005.) (Revised by Mario Carneiro, 31-Jan-2014.)
Hypotheses
Ref Expression
climconst.1
climconst.2
climconst.3
climconst.4
climconst.5
Assertion
Ref Expression
climconst
Distinct variable groups:   ,   ,   ,   ,
Allowed substitution hints:   ()   ()

Proof of Theorem climconst
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 climconst.2 . . . . . . 7
2 uzid 8487 . . . . . . 7
31, 2syl 14 . . . . . 6
4 climconst.1 . . . . . 6
53, 4syl6eleqr 2131 . . . . 5
65adantr 261 . . . 4
7 climconst.4 . . . . . . . . . 10
87subidd 7310 . . . . . . . . 9
98fveq2d 5182 . . . . . . . 8
10 abs0 9656 . . . . . . . 8
119, 10syl6eq 2088 . . . . . . 7
1211adantr 261 . . . . . 6
13 rpgt0 8594 . . . . . . 7
1413adantl 262 . . . . . 6
1512, 14eqbrtrd 3784 . . . . 5
1615ralrimivw 2393 . . . 4
17 fveq2 5178 . . . . . . 7
1817, 4syl6eqr 2090 . . . . . 6
1918raleqdv 2511 . . . . 5
2019rspcev 2656 . . . 4
216, 16, 20syl2anc 391 . . 3
2221ralrimiva 2392 . 2
23 climconst.3 . . 3
24 climconst.5 . . 3