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

Theorem climub 11106
 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
clim2iser.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 2137 . 2
2 climub.2 . . . 4
3 clim2iser.1 . . . 4
42, 3eleqtrdi 2230 . . 3
5 eluzelz 9328 . . 3
64, 5syl 14 . 2
7 fveq2 5414 . . . . . 6
87eleq1d 2206 . . . . 5
98imbi2d 229 . . . 4
10 climub.4 . . . . 5
1110expcom 115 . . . 4
129, 11vtoclga 2747 . . 3
132, 12mpcom 36 . 2
14 climub.3 . 2
153uztrn2 9336 . . . 4
162, 15sylan 281 . . 3
17 fveq2 5414 . . . . . . 7
1817eleq1d 2206 . . . . . 6
1918imbi2d 229 . . . . 5
2019, 11vtoclga 2747 . . . 4
2120impcom 124 . . 3
2216, 21syldan 280 . 2
23 simpr 109 . . 3
24 elfzuz 9795 . . . . 5
253uztrn2 9336 . . . . . . 7
262, 25sylan 281 . . . . . 6
2726, 10syldan 280 . . . . 5
2824, 27sylan2 284 . . . 4