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

Theorem climub 9864
 Description: The limit of a monotonic sequence is an upper bound. (Contributed by NM, 18-Mar-2005.) (Revised by Mario Carneiro, 10-Feb-2014.)
Hypotheses
Ref Expression
clim2ser.1
climub.2
climub.3
climub.4
climub.5
Assertion
Ref Expression
climub
Distinct variable groups:   ,   ,   ,   ,   ,   ,

Proof of Theorem climub
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 eqid 2040 . 2
2 climub.2 . . . 4
3 clim2ser.1 . . . 4
42, 3syl6eleq 2130 . . 3
5 eluzelz 8482 . . 3
64, 5syl 14 . 2
7 fveq2 5178 . . . . . 6
87eleq1d 2106 . . . . 5
98imbi2d 219 . . . 4
10 climub.4 . . . . 5
1110expcom 109 . . . 4
129, 11vtoclga 2619 . . 3
132, 12mpcom 32 . 2
14 climub.3 . 2
153uztrn2 8490 . . . 4
162, 15sylan 267 . . 3
17 fveq2 5178 . . . . . . 7
1817eleq1d 2106 . . . . . 6
1918imbi2d 219 . . . . 5
2019, 11vtoclga 2619 . . . 4
2120impcom 116 . . 3
2216, 21syldan 266 . 2
23 simpr 103 . . 3
24 elfzuz 8886 . . . . 5
253uztrn2 8490 . . . . . . 7
262, 25sylan 267 . . . . . 6
2726, 10syldan 266 . . . . 5
2824, 27sylan2 270 . . . 4