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

Theorem climconst 11066
 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 9347 . . . . . . 7
31, 2syl 14 . . . . . 6
4 climconst.1 . . . . . 6
53, 4eleqtrrdi 2233 . . . . 5
65adantr 274 . . . 4
7 climconst.4 . . . . . . . . . 10
87subidd 8068 . . . . . . . . 9
98fveq2d 5425 . . . . . . . 8
10 abs0 10837 . . . . . . . 8
119, 10syl6eq 2188 . . . . . . 7
1211adantr 274 . . . . . 6
13 rpgt0 9460 . . . . . . 7
1413adantl 275 . . . . . 6
1512, 14eqbrtrd 3950 . . . . 5
1615ralrimivw 2506 . . . 4
17 fveq2 5421 . . . . . . 7
1817, 4syl6eqr 2190 . . . . . 6
1918raleqdv 2632 . . . . 5
2019rspcev 2789 . . . 4
216, 16, 20syl2anc 408 . . 3
2221ralrimiva 2505 . 2
23 climconst.3 . . 3
24 climconst.5 . . 3