Theorem climsup 7099

Description: A bounded monotonic sequence converges to the supremum of its range. Theorem 12-5.1 of [Gleason] p. 180.

Hypotheses

Ref	Expression
climsup.1	|- F:NN-->RR
climsup.2	|- (k e. NN -> (F` k) <_ (F` (k + 1)))
climsup.3	|- E.x e. RR A.k e. NN (F` k) <_ x

Assertion

Ref	Expression
climsup	|- F ~~> sup(ran F, RR, < )

Distinct variable group:   x,k,F

Proof of Theorem climsup

Step	Hyp	Ref	Expression
1		climsup.1	. . . 4 |- F:NN-->RR
2		axresscn 5248	. . . 4 |- RR (_ CC
3		fss 3626	. . . 4 |- ((F:NN-->RR /\ RR (_ CC) -> F:NN-->CC)
4	1, 2, 3	mp2an 696	. . 3 |- F:NN-->CC
5		frn 3624	. . . . . . 7 |- (F:NN-->RR -> ran F (_ RR)
6	1, 5	ax-mp 7	. . . . . 6 |- ran F (_ RR
7		1nn 5890	. . . . . . . . 9 |- 1 e. NN
8		ne0i 2282	. . . . . . . . 9 |- (1 e. NN -> NN =/= (/))
9	7, 8	ax-mp 7	. . . . . . . 8 |- NN =/= (/)
10		fdm 3623	. . . . . . . . . 10 |- (F:NN-->RR -> dom F = NN)
11	1, 10	ax-mp 7	. . . . . . . . 9 |- dom F = NN
12	11	neeq1i 1589	. . . . . . . 8 |- (dom F =/= (/) <-> NN =/= (/))
13	9, 12	mpbir 190	. . . . . . 7 |- dom F =/= (/)
14		dm0rn0 3325	. . . . . . . 8 |- (dom F = (/) <-> ran F = (/))
15	14	necon3bii 1595	. . . . . . 7 |- (dom F =/= (/) <-> ran F =/= (/))
16	13, 15	mpbi 189	. . . . . 6 |- ran F =/= (/)
17		climsup.3	. . . . . . 7 |- E.x e. RR A.k e. NN (F` k) <_ x
18		hbra1 1684	. . . . . . . . . . 11 |- (A.k e. NN (F` k) <_ x -> A.kA.k e. NN (F` k) <_ x)
19		ax-17 969	. . . . . . . . . . 11 |- (y <_ x -> A.k y <_ x)
20		ra4 1691	. . . . . . . . . . . 12 |- (A.k e. NN (F` k) <_ x -> (k e. NN -> (F` k) <_ x))
21		breq1 2617	. . . . . . . . . . . . 13 |- ((F` k) = y -> ((F` k) <_ x <-> y <_ x))
22	21	biimpcd 155	. . . . . . . . . . . 12 |- ((F` k) <_ x -> ((F` k) = y -> y <_ x))
23	20, 22	syl6 22	. . . . . . . . . . 11 |- (A.k e. NN (F` k) <_ x -> (k e. NN -> ((F` k) = y -> y <_ x)))
24	18, 19, 23	r19.23ad 1742	. . . . . . . . . 10 |- (A.k e. NN (F` k) <_ x -> (E.k e. NN (F` k) = y -> y <_ x))
25		ffn 3619	. . . . . . . . . . . 12 |- (F:NN-->RR -> F Fn NN)
26	1, 25	ax-mp 7	. . . . . . . . . . 11 |- F Fn NN
27		fvelrnb 3751	. . . . . . . . . . 11 |- (F Fn NN -> (y e. ran F <-> E.k e. NN (F` k) = y))
28	26, 27	ax-mp 7	. . . . . . . . . 10 |- (y e. ran F <-> E.k e. NN (F` k) = y)
29	24, 28	syl5ib 206	. . . . . . . . 9 |- (A.k e. NN (F` k) <_ x -> (y e. ran F -> y <_ x))
30	29	r19.21aiv 1710	. . . . . . . 8 |- (A.k e. NN (F` k) <_ x -> A.y e. ran F y <_ x)
31	30	r19.22si 1731	. . . . . . 7 |- (E.x e. RR A.k e. NN (F` k) <_ x -> E.x e. RR A.y e. ran F y <_ x)
32	17, 31	ax-mp 7	. . . . . 6 |- E.x e. RR A.y e. ran F y <_ x
33	6, 16, 32	3pm3.2i 817	. . . . 5 |- (ran F (_ RR /\ ran F =/= (/) /\ E.x e. RR A.y e. ran F y <_ x)
34	33	suprcli 6016	. . . 4 |- sup(ran F, RR, < ) e. RR
35	34	recn 5294	. . 3 |- sup(ran F, RR, < ) e. CC
36		climfnn 7038	. . 3 |- ((F:NN-->CC /\ sup(ran F, RR, < ) e. CC) -> (F ~~> sup(ran F, RR, < ) <-> A.x e. RR (0 < x -> E.j e. NN A.k e. NN (j <_ k -> (abs` ((F` k) - sup(ran F, RR, < ))) < x))))
37	4, 35, 36	mp2an 696	. 2 |- (F ~~> sup(ran F, RR, < ) <-> A.x e. RR (0 < x -> E.j e. NN A.k e. NN (j <_ k -> (abs` ((F` k) - sup(ran F, RR, < ))) < x)))
38		ltsubpost 5634	. . . . 5 |- ((x e. RR /\ sup(ran F, RR, < ) e. RR) -> (0 < x <-> (sup(ran F, RR, < ) - x) < sup(ran F, RR, < )))
39	34, 38	mpan2 695	. . . 4 |- (x e. RR -> (0 < x <-> (sup(ran F, RR, < ) - x) < sup(ran F, RR, < )))
40		ax-17 969	. . . . . . . . . . . . 13 |- (z <_ x -> A.k z <_ x)
41		breq1 2617	. . . . . . . . . . . . . . 15 |- ((F` k) = z -> ((F` k) <_ x <-> z <_ x))
42	41	biimpcd 155	. . . . . . . . . . . . . 14 |- ((F` k) <_ x -> ((F` k) = z -> z <_ x))
43	20, 42	syl6 22	. . . . . . . . . . . . 13 |- (A.k e. NN (F` k) <_ x -> (k e. NN -> ((F` k) = z -> z <_ x)))
44	18, 40, 43	r19.23ad 1742	. . . . . . . . . . . 12 |- (A.k e. NN (F` k) <_ x -> (E.k e. NN (F` k) = z -> z <_ x))
45		fvelrnb 3751	. . . . . . . . . . . . 13 |- (F Fn NN -> (z e. ran F <-> E.k e. NN (F` k) = z))
46	26, 45	ax-mp 7	. . . . . . . . . . . 12 |- (z e. ran F <-> E.k e. NN (F` k) = z)
47	44, 46	syl5ib 206	. . . . . . . . . . 11 |- (A.k e. NN (F` k) <_ x -> (z e. ran F -> z <_ x))
48	47	r19.21aiv 1710	. . . . . . . . . 10 |- (A.k e. NN (F` k) <_ x -> A.z e. ran F z <_ x)
49	48	r19.22si 1731	. . . . . . . . 9 |- (E.x e. RR A.k e. NN (F` k) <_ x -> E.x e. RR A.z e. ran F z <_ x)
50	17, 49	ax-mp 7	. . . . . . . 8 |- E.x e. RR A.z e. ran F z <_ x
51	6, 16, 50	3pm3.2i 817	. . . . . . 7 |- (ran F (_ RR /\ ran F =/= (/) /\ E.x e. RR A.z e. ran F z <_ x)
52	51	suprlubi 6018	. . . . . 6 |- (((sup(ran F, RR, < ) - x) e. RR /\ (sup(ran F, RR, < ) - x) < sup(ran F, RR, < )) -> E.y e. ran F(sup(ran F, RR, < ) - x) < y)
53		resubclt 5418	. . . . . . 7 |- ((sup(ran F, RR, < ) e. RR /\ x e. RR) -> (sup(ran F, RR, < ) - x) e. RR)
54	34, 53	mpan 694	. . . . . 6 |- (x e. RR -> (sup(ran F, RR, < ) - x) e. RR)
55	52, 54	sylan 448	. . . . 5 |- ((x e. RR /\ (sup(ran F, RR, < ) - x) < sup(ran F, RR, < )) -> E.y e. ran F(sup(ran F, RR, < ) - x) < y)
56	55	ex 373	. . . 4 |- (x e. RR -> ((sup(ran F, RR, < ) - x) < sup(ran F, RR, < ) -> E.y e. ran F(sup(ran F, RR, < ) - x) < y))
57	39, 56	sylbid 203	. . 3 |- (x e. RR -> (0 < x -> E.y e. ran F(sup(ran F, RR, < ) - x) < y))
58	54	adantr 389	. . . . . . . . . . . . . 14 |- ((x e. RR /\ (sup(ran F, RR, < ) - x) < y) -> (sup(ran F, RR, < ) - x) e. RR)
59	58	ad2antrr 404	. . . . . . . . . . . . 13 |- ((((x e. RR /\ (sup(ran F, RR, < ) - x) < y) /\ (j e. NN /\ (F` j) = y)) /\ (k e. NN /\ j <_ k)) -> (sup(ran F, RR, < ) - x) e. RR)
60	1	ffvelrni 3806	. . . . . . . . . . . . . . 15 |- (j e. NN -> (F` j) e. RR)
61	60	adantr 389	. . . . . . . . . . . . . 14 |- ((j e. NN /\ (F` j) = y) -> (F` j) e. RR)
62	61	ad2antlr 405	. . . . . . . . . . . . 13 |- ((((x e. RR /\ (sup(ran F, RR, < ) - x) < y) /\ (j e. NN /\ (F` j) = y)) /\ (k e. NN /\ j <_ k)) -> (F` j) e. RR)
63	1	ffvelrni 3806	. . . . . . . . . . . . . 14 |- (k e. NN -> (F` k) e. RR)
64	63	ad2antrl 406	. . . . . . . . . . . . 13 |- ((((x e. RR /\ (sup(ran F, RR, < ) - x) < y) /\ (j e. NN /\ (F` j) = y)) /\ (k e. NN /\ j <_ k)) -> (F` k) e. RR)
65		breq2 2618	. . . . . . . . . . . . . . . 16 |- ((F` j) = y -> ((sup(ran F, RR, < ) - x) < (F` j) <-> (sup(ran F, RR, < ) - x) < y))
66	65	biimparc 419	. . . . . . . . . . . . . . 15 |- (((sup(ran F, RR, < ) - x) < y /\ (F` j) = y) -> (sup(ran F, RR, < ) - x) < (F` j))
67	66	ad2ant2l 408	. . . . . . . . . . . . . 14 |- (((x e. RR /\ (sup(ran F, RR, < ) - x) < y) /\ (j e. NN /\ (F` j) = y)) -> (sup(ran F, RR, < ) - x) < (F` j))
68	67	adantr 389	. . . . . . . . . . . . 13 |- ((((x e. RR /\ (sup(ran F, RR, < ) - x) < y) /\ (j e. NN /\ (F` j) = y)) /\ (k e. NN /\ j <_ k)) -> (sup(ran F, RR, < ) - x) < (F` j))
69		climsup.2	. . . . . . . . . . . . . . . . 17 |- (k e. NN -> (F` k) <_ (F` (k + 1)))
70	1, 69	monoord 6239	. . . . . . . . . . . . . . . 16 |- ((j e. NN /\ k e. NN /\ j <_ k) -> (F` j) <_ (F` k))
71	70	3expb 833	. . . . . . . . . . . . . . 15 |- ((j e. <