Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  climub Structured version   Unicode version

Theorem climub 12460
 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 2438 . 2
2 climub.2 . . . 4
3 clim2ser.1 . . . 4
42, 3syl6eleq 2528 . . 3
5 eluzelz 10501 . . 3
64, 5syl 16 . 2
7 fveq2 5731 . . . . . 6
87eleq1d 2504 . . . . 5
98imbi2d 309 . . . 4
10 climub.4 . . . . 5
1110expcom 426 . . . 4
129, 11vtoclga 3019 . . 3
132, 12mpcom 35 . 2
14 climub.3 . 2
153uztrn2 10508 . . . 4
162, 15sylan 459 . . 3
17 fveq2 5731 . . . . . . 7
1817eleq1d 2504 . . . . . 6
1918imbi2d 309 . . . . 5
2019, 11vtoclga 3019 . . . 4
2120impcom 421 . . 3
2216, 21syldan 458 . 2
23 simpr 449 . . 3
24 elfzuz 11060 . . . . 5
253uztrn2 10508 . . . . . . 7
262, 25sylan 459 . . . . . 6
2726, 10syldan 458 . . . . 5
2824, 27sylan2 462 . . . 4