climsup

Description: A bounded monotonic sequence converges to the supremum of its range. Theorem 12-5.1 of Gleason p. 180. (Contributed by NM, 13-Mar-2005) (Revised by Mario Carneiro, 10-Feb-2014)

	Ref	Expression
Hypotheses	climsup.1	$⊢ Z = ℤ_{\geq M}$
	climsup.2	$⊢ φ \to M \in ℤ$
	climsup.3	$⊢ φ \to F : Z ⟶ ℝ$
	climsup.4	$⊢ (φ \land k \in Z) \to F (k) \leq F (k + 1)$
	climsup.5	$⊢ φ \to \exists x \in ℝ \forall k \in Z F (k) \leq x$
Assertion	climsup	$⊢ φ \to F ⇝ sup (ran F ℝ <)$

Proof

Step	Hyp	Ref	Expression
1		climsup.1	$⊢ Z = ℤ_{\geq M}$
2		climsup.2	$⊢ φ \to M \in ℤ$
3		climsup.3	$⊢ φ \to F : Z ⟶ ℝ$
4		climsup.4	$⊢ (φ \land k \in Z) \to F (k) \leq F (k + 1)$
5		climsup.5	$⊢ φ \to \exists x \in ℝ \forall k \in Z F (k) \leq x$
6	3	frnd	$⊢ φ \to ran F \subseteq ℝ$
7	3	ffnd	$⊢ φ \to F Fn Z$
8		uzid	$⊢ M \in ℤ \to M \in ℤ_{\geq M}$
9	2 8	syl	$⊢ φ \to M \in ℤ_{\geq M}$
10	9 1	eleqtrrdi	$⊢ φ \to M \in Z$
11		fnfvelrn	$⊢ (F Fn Z \land M \in Z) \to F (M) \in ran F$
12	7 10 11	syl2anc	$⊢ φ \to F (M) \in ran F$
13	12	ne0d	$⊢ φ \to ran F \neq \emptyset$
14		breq1	$⊢ y = F (k) \to (y \leq x \leftrightarrow F (k) \leq x)$
15	14	ralrn	$⊢ F Fn Z \to (\forall y \in ran F y \leq x \leftrightarrow \forall k \in Z F (k) \leq x)$
16	15	rexbidv	$⊢ F Fn Z \to (\exists x \in ℝ \forall y \in ran F y \leq x \leftrightarrow \exists x \in ℝ \forall k \in Z F (k) \leq x)$
17	7 16	syl	$⊢ φ \to (\exists x \in ℝ \forall y \in ran F y \leq x \leftrightarrow \exists x \in ℝ \forall k \in Z F (k) \leq x)$
18	5 17	mpbird	$⊢ φ \to \exists x \in ℝ \forall y \in ran F y \leq x$
19	6 13 18	3jca	$⊢ φ \to (ran F \subseteq ℝ \land ran F \neq \emptyset \land \exists x \in ℝ \forall y \in ran F y \leq x)$
20		suprcl	$⊢ (ran F \subseteq ℝ \land ran F \neq \emptyset \land \exists x \in ℝ \forall y \in ran F y \leq x) \to sup (ran F ℝ <) \in ℝ$
21	19 20	syl	$⊢ φ \to sup (ran F ℝ <) \in ℝ$
22		ltsubrp	$⊢ (sup (ran F ℝ <) \in ℝ \land y \in ℝ^{+}) \to sup (ran F ℝ <) - y < sup (ran F ℝ <)$
23	21 22	sylan	$⊢ (φ \land y \in ℝ^{+}) \to sup (ran F ℝ <) - y < sup (ran F ℝ <)$
24	19	adantr	$⊢ (φ \land y \in ℝ^{+}) \to (ran F \subseteq ℝ \land ran F \neq \emptyset \land \exists x \in ℝ \forall y \in ran F y \leq x)$
25		rpre	$⊢ y \in ℝ^{+} \to y \in ℝ$
26		resubcl	$⊢ (sup (ran F ℝ <) \in ℝ \land y \in ℝ) \to sup (ran F ℝ <) - y \in ℝ$
27	21 25 26	syl2an	$⊢ (φ \land y \in ℝ^{+}) \to sup (ran F ℝ <) - y \in ℝ$
28		suprlub	$⊢ ((ran F \subseteq ℝ \land ran F \neq \emptyset \land \exists x \in ℝ \forall y \in ran F y \leq x) \land sup (ran F ℝ <) - y \in ℝ) \to (sup (ran F ℝ <) - y < sup (ran F ℝ <) \leftrightarrow \exists k \in ran F sup (ran F ℝ <) - y < k)$
29	24 27 28	syl2anc	$⊢ (φ \land y \in ℝ^{+}) \to (sup (ran F ℝ <) - y < sup (ran F ℝ <) \leftrightarrow \exists k \in ran F sup (ran F ℝ <) - y < k)$
30	23 29	mpbid	$⊢ (φ \land y \in ℝ^{+}) \to \exists k \in ran F sup (ran F ℝ <) - y < k$
31		breq2	$⊢ k = F (j) \to (sup (ran F ℝ <) - y < k \leftrightarrow sup (ran F ℝ <) - y < F (j))$
32	31	rexrn	$⊢ F Fn Z \to (\exists k \in ran F sup (ran F ℝ <) - y < k \leftrightarrow \exists j \in Z sup (ran F ℝ <) - y < F (j))$
33	7 32	syl	$⊢ φ \to (\exists k \in ran F sup (ran F ℝ <) - y < k \leftrightarrow \exists j \in Z sup (ran F ℝ <) - y < F (j))$
34	33	biimpa	$⊢ (φ \land \exists k \in ran F sup (ran F ℝ <) - y < k) \to \exists j \in Z sup (ran F ℝ <) - y < F (j)$
35	30 34	syldan	$⊢ (φ \land y \in ℝ^{+}) \to \exists j \in Z sup (ran F ℝ <) - y < F (j)$
36		ffvelcdm	$⊢ (F : Z ⟶ ℝ \land j \in Z) \to F (j) \in ℝ$
37	3 36	sylan	$⊢ (φ \land j \in Z) \to F (j) \in ℝ$
38	37	ad2ant2r	$⊢ ((φ \land y \in ℝ^{+}) \land (j \in Z \land k \in ℤ_{\geq j})) \to F (j) \in ℝ$
39	3	adantr	$⊢ (φ \land y \in ℝ^{+}) \to F : Z ⟶ ℝ$
40	1	uztrn2	$⊢ (j \in Z \land k \in ℤ_{\geq j}) \to k \in Z$
41		ffvelcdm	$⊢ (F : Z ⟶ ℝ \land k \in Z) \to F (k) \in ℝ$
42	39 40 41	syl2an	$⊢ ((φ \land y \in ℝ^{+}) \land (j \in Z \land k \in ℤ_{\geq j})) \to F (k) \in ℝ$
43	21	ad2antrr	$⊢ ((φ \land y \in ℝ^{+}) \land (j \in Z \land k \in ℤ_{\geq j})) \to sup (ran F ℝ <) \in ℝ$
44		simprr	$⊢ ((φ \land y \in ℝ^{+}) \land (j \in Z \land k \in ℤ_{\geq j})) \to k \in ℤ_{\geq j}$
45		fzssuz	$⊢ (j \dots k) \subseteq ℤ_{\geq j}$
46		uzss	$⊢ j \in ℤ_{\geq M} \to ℤ_{\geq j} \subseteq ℤ_{\geq M}$
47	46 1	sseqtrrdi	$⊢ j \in ℤ_{\geq M} \to ℤ_{\geq j} \subseteq Z$
48	47 1	eleq2s	$⊢ j \in Z \to ℤ_{\geq j} \subseteq Z$
49	48	ad2antrl	$⊢ ((φ \land y \in ℝ^{+}) \land (j \in Z \land k \in ℤ_{\geq j})) \to ℤ_{\geq j} \subseteq Z$
50	45 49	sstrid	$⊢ ((φ \land y \in ℝ^{+}) \land (j \in Z \land k \in ℤ_{\geq j})) \to (j \dots k) \subseteq Z$
51		ffvelcdm	$⊢ (F : Z ⟶ ℝ \land n \in Z) \to F (n) \in ℝ$
52	51	ralrimiva	$⊢ F : Z ⟶ ℝ \to \forall n \in Z F (n) \in ℝ$
53	3 52	syl	$⊢ φ \to \forall n \in Z F (n) \in ℝ$
54	53	ad2antrr	$⊢ ((φ \land y \in ℝ^{+}) \land (j \in Z \land k \in ℤ_{\geq j})) \to \forall n \in Z F (n) \in ℝ$
55		ssralv	$⊢ (j \dots k) \subseteq Z \to (\forall n \in Z F (n) \in ℝ \to \forall n \in (j \dots k) F (n) \in ℝ)$
56	50 54 55	sylc	$⊢ ((φ \land y \in ℝ^{+}) \land (j \in Z \land k \in ℤ_{\geq j})) \to \forall n \in (j \dots k) F (n) \in ℝ$
57	56	r19.21bi	$⊢ (((φ \land y \in ℝ^{+}) \land (j \in Z \land k \in ℤ_{\geq j})) \land n \in (j \dots k)) \to F (n) \in ℝ$
58		fzssuz	$⊢ (j \dots k - 1) \subseteq ℤ_{\geq j}$
59	58 49	sstrid	$⊢ ((φ \land y \in ℝ^{+}) \land (j \in Z \land k \in ℤ_{\geq j})) \to (j \dots k - 1) \subseteq Z$
60	59	sselda	$⊢ (((φ \land y \in ℝ^{+}) \land (j \in Z \land k \in ℤ_{\geq j})) \land n \in (j \dots k - 1)) \to n \in Z$
61	4	ralrimiva	$⊢ φ \to \forall k \in Z F (k) \leq F (k + 1)$
62	61	ad2antrr	$⊢ ((φ \land y \in ℝ^{+}) \land (j \in Z \land k \in ℤ_{\geq j})) \to \forall k \in Z F (k) \leq F (k + 1)$
63		fveq2	$⊢ k = n \to F (k) = F (n)$
64		fvoveq1	$⊢ k = n \to F (k + 1) = F (n + 1)$
65	63 64	breq12d	$⊢ k = n \to (F (k) \leq F (k + 1) \leftrightarrow F (n) \leq F (n + 1))$
66	65	rspccva	$⊢ (\forall k \in Z F (k) \leq F (k + 1) \land n \in Z) \to F (n) \leq F (n + 1)$
67	62 66	sylan	$⊢ (((φ \land y \in ℝ^{+}) \land (j \in Z \land k \in ℤ_{\geq j})) \land n \in Z) \to F (n) \leq F (n + 1)$
68	60 67	syldan	$⊢ (((φ \land y \in ℝ^{+}) \land (j \in Z \land k \in ℤ_{\geq j})) \land n \in (j \dots k - 1)) \to F (n) \leq F (n + 1)$
69	44 57 68	monoord	$⊢ ((φ \land y \in ℝ^{+}) \land (j \in Z \land k \in ℤ_{\geq j})) \to F (j) \leq F (k)$
70	38 42 43 69	lesub2dd	$⊢ ((φ \land y \in ℝ^{+}) \land (j \in Z \land k \in ℤ_{\geq j})) \to sup (ran F ℝ <) - F (k) \leq sup (ran F ℝ <) - F (j)$
71	43 42	resubcld	$⊢ ((φ \land y \in ℝ^{+}) \land (j \in Z \land k \in ℤ_{\geq j})) \to sup (ran F ℝ <) - F (k) \in ℝ$
72	43 38	resubcld	$⊢ ((φ \land y \in ℝ^{+}) \land (j \in Z \land k \in ℤ_{\geq j})) \to sup (ran F ℝ <) - F (j) \in ℝ$
73	25	ad2antlr	$⊢ ((φ \land y \in ℝ^{+}) \land (j \in Z \land k \in ℤ_{\geq j})) \to y \in ℝ$
74		lelttr	$⊢ (sup (ran F ℝ <) - F (k) \in ℝ \land sup (ran F ℝ <) - F (j) \in ℝ \land y \in ℝ) \to ((sup (ran F ℝ <) - F (k) \leq sup (ran F ℝ <) - F (j) \land sup (ran F ℝ <) - F (j) < y) \to sup (ran F ℝ <) - F (k) < y)$
75	71 72 73 74	syl3anc	$⊢ ((φ \land y \in ℝ^{+}) \land (j \in Z \land k \in ℤ_{\geq j})) \to ((sup (ran F ℝ <) - F (k) \leq sup (ran F ℝ <) - F (j) \land sup (ran F ℝ <) - F (j) < y) \to sup (ran F ℝ <) - F (k) < y)$
76	70 75	mpand	$⊢ ((φ \land y \in ℝ^{+}) \land (j \in Z \land k \in ℤ_{\geq j})) \to (sup (ran F ℝ <) - F (j) < y \to sup (ran F ℝ <) - F (k) < y)$
77		ltsub23	$⊢ (sup (ran F ℝ <) \in ℝ \land y \in ℝ \land F (j) \in ℝ) \to (sup (ran F ℝ <) - y < F (j) \leftrightarrow sup (ran F ℝ <) - F (j) < y)$
78	43 73 38 77	syl3anc	$⊢ ((φ \land y \in ℝ^{+}) \land (j \in Z \land k \in ℤ_{\geq j})) \to (sup (ran F ℝ <) - y < F (j) \leftrightarrow sup (ran F ℝ <) - F (j) < y)$
79	19	ad2antrr	$⊢ ((φ \land y \in ℝ^{+}) \land (j \in Z \land k \in ℤ_{\geq j})) \to (ran F \subseteq ℝ \land ran F \neq \emptyset \land \exists x \in ℝ \forall y \in ran F y \leq x)$
80	7	adantr	$⊢ (φ \land y \in ℝ^{+}) \to F Fn Z$
81		fnfvelrn	$⊢ (F Fn Z \land k \in Z) \to F (k) \in ran F$
82	80 40 81	syl2an	$⊢ ((φ \land y \in ℝ^{+}) \land (j \in Z \land k \in ℤ_{\geq j})) \to F (k) \in ran F$
83		suprub	$⊢ ((ran F \subseteq ℝ \land ran F \neq \emptyset \land \exists x \in ℝ \forall y \in ran F y \leq x) \land F (k) \in ran F) \to F (k) \leq sup (ran F ℝ <)$
84	79 82 83	syl2anc	$⊢ ((φ \land y \in ℝ^{+}) \land (j \in Z \land k \in ℤ_{\geq j})) \to F (k) \leq sup (ran F ℝ <)$
85	42 43 84	abssuble0d	$⊢ ((φ \land y \in ℝ^{+}) \land (j \in Z \land k \in ℤ_{\geq j})) \to \|F (k) - sup (ran F ℝ <)\| = sup (ran F ℝ <) - F (k)$
86	85	breq1d	$⊢ ((φ \land y \in ℝ^{+}) \land (j \in Z \land k \in ℤ_{\geq j})) \to (\|F (k) - sup (ran F ℝ <)\| < y \leftrightarrow sup (ran F ℝ <) - F (k) < y)$
87	76 78 86	3imtr4d	$⊢ ((φ \land y \in ℝ^{+}) \land (j \in Z \land k \in ℤ_{\geq j})) \to (sup (ran F ℝ <) - y < F (j) \to \|F (k) - sup (ran F ℝ <)\| < y)$
88	87	anassrs	$⊢ (((φ \land y \in ℝ^{+}) \land j \in Z) \land k \in ℤ_{\geq j}) \to (sup (ran F ℝ <) - y < F (j) \to \|F (k) - sup (ran F ℝ <)\| < y)$
89	88	ralrimdva	$⊢ ((φ \land y \in ℝ^{+}) \land j \in Z) \to (sup (ran F ℝ <) - y < F (j) \to \forall k \in ℤ_{\geq j} \|F (k) - sup (ran F ℝ <)\| < y)$
90	89	reximdva	$⊢ (φ \land y \in ℝ^{+}) \to (\exists j \in Z sup (ran F ℝ <) - y < F (j) \to \exists j \in Z \forall k \in ℤ_{\geq j} \|F (k) - sup (ran F ℝ <)\| < y)$
91	35 90	mpd	$⊢ (φ \land y \in ℝ^{+}) \to \exists j \in Z \forall k \in ℤ_{\geq j} \|F (k) - sup (ran F ℝ <)\| < y$
92	91	ralrimiva	$⊢ φ \to \forall y \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \|F (k) - sup (ran F ℝ <)\| < y$
93	1	fvexi	$⊢ Z \in V$
94		fex	$⊢ (F : Z ⟶ ℝ \land Z \in V) \to F \in V$
95	3 93 94	sylancl	$⊢ φ \to F \in V$
96		eqidd	$⊢ (φ \land k \in Z) \to F (k) = F (k)$
97	21	recnd	$⊢ φ \to sup (ran F ℝ <) \in ℂ$
98	3 41	sylan	$⊢ (φ \land k \in Z) \to F (k) \in ℝ$
99	98	recnd	$⊢ (φ \land k \in Z) \to F (k) \in ℂ$
100	1 2 95 96 97 99	clim2c	$⊢ φ \to (F ⇝ sup (ran F ℝ <) \leftrightarrow \forall y \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \|F (k) - sup (ran F ℝ <)\| < y)$
101	92 100	mpbird	$⊢ φ \to F ⇝ sup (ran F ℝ <)$

Metamath Proof Explorer

Theorem climsup

Proof