Theorem climub

Description: The limit of a monotonic sequence is an upper bound. (Contributed by NM, 18-Mar-2005) (Revised by Mario Carneiro, 10-Feb-2014)

	Ref	Expression
Hypotheses	clim2ser.1	$$⊢Z={\mathbb{Z}}_{\ge M}$$
	climub.2	$$⊢\phi \to N\in Z$$
	climub.3	$$⊢\phi \to F⇝A$$
	climub.4	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k\right)\in ℝ$$
	climub.5	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k\right)\le F\left(k+1\right)$$
Assertion	climub	$$⊢\phi \to F\left(N\right)\le A$$

Proof

Step	Hyp	Ref	Expression
1		clim2ser.1	$$⊢Z={\mathbb{Z}}_{\ge M}$$
2		climub.2	$$⊢\phi \to N\in Z$$
3		climub.3	$$⊢\phi \to F⇝A$$
4		climub.4	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k\right)\in ℝ$$
5		climub.5	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k\right)\le F\left(k+1\right)$$
6		eqid	$$⊢{\mathbb{Z}}_{\ge N}={\mathbb{Z}}_{\ge N}$$
7	2 1	eleqtrdi	$$⊢\phi \to N\in {\mathbb{Z}}_{\ge M}$$
8		eluzelz	$$⊢N\in {\mathbb{Z}}_{\ge M}\to N\in \mathbb{Z}$$
9	7 8	syl	$$⊢\phi \to N\in \mathbb{Z}$$
10		fveq2	$$⊢k=N\to F\left(k\right)=F\left(N\right)$$
11	10	eleq1d	$$⊢k=N\to \left(F\left(k\right)\in ℝ\leftrightarrow F\left(N\right)\in ℝ\right)$$
12	11	imbi2d	$$⊢k=N\to \left(\left(\phi \to F\left(k\right)\in ℝ\right)\leftrightarrow \left(\phi \to F\left(N\right)\in ℝ\right)\right)$$
13	4	expcom	$$⊢k\in Z\to \left(\phi \to F\left(k\right)\in ℝ\right)$$
14	12 13	vtoclga	$$⊢N\in Z\to \left(\phi \to F\left(N\right)\in ℝ\right)$$
15	2 14	mpcom	$$⊢\phi \to F\left(N\right)\in ℝ$$
16	1	uztrn2	$$⊢\left(N\in Z\wedge j\in {\mathbb{Z}}_{\ge N}\right)\to j\in Z$$
17	2 16	sylan	$$⊢\left(\phi \wedge j\in {\mathbb{Z}}_{\ge N}\right)\to j\in Z$$
18		fveq2	$$⊢k=j\to F\left(k\right)=F\left(j\right)$$
19	18	eleq1d	$$⊢k=j\to \left(F\left(k\right)\in ℝ\leftrightarrow F\left(j\right)\in ℝ\right)$$
20	19	imbi2d	$$⊢k=j\to \left(\left(\phi \to F\left(k\right)\in ℝ\right)\leftrightarrow \left(\phi \to F\left(j\right)\in ℝ\right)\right)$$
21	20 13	vtoclga	$$⊢j\in Z\to \left(\phi \to F\left(j\right)\in ℝ\right)$$
22	21	impcom	$$⊢\left(\phi \wedge j\in Z\right)\to F\left(j\right)\in ℝ$$
23	17 22	syldan	$$⊢\left(\phi \wedge j\in {\mathbb{Z}}_{\ge N}\right)\to F\left(j\right)\in ℝ$$
24		simpr	$$⊢\left(\phi \wedge j\in {\mathbb{Z}}_{\ge N}\right)\to j\in {\mathbb{Z}}_{\ge N}$$
25		elfzuz	$$⊢k\in \left(N\dots j\right)\to k\in {\mathbb{Z}}_{\ge N}$$
26	1	uztrn2	$$⊢\left(N\in Z\wedge k\in {\mathbb{Z}}_{\ge N}\right)\to k\in Z$$
27	2 26	sylan	$$⊢\left(\phi \wedge k\in {\mathbb{Z}}_{\ge N}\right)\to k\in Z$$
28	27 4	syldan	$$⊢\left(\phi \wedge k\in {\mathbb{Z}}_{\ge N}\right)\to F\left(k\right)\in ℝ$$
29	25 28	sylan2	$$⊢\left(\phi \wedge k\in \left(N\dots j\right)\right)\to F\left(k\right)\in ℝ$$
30	29	adantlr	$$⊢\left(\left(\phi \wedge j\in {\mathbb{Z}}_{\ge N}\right)\wedge k\in \left(N\dots j\right)\right)\to F\left(k\right)\in ℝ$$
31		elfzuz	$$⊢k\in \left(N\dots j-1\right)\to k\in {\mathbb{Z}}_{\ge N}$$
32	27 5	syldan	$$⊢\left(\phi \wedge k\in {\mathbb{Z}}_{\ge N}\right)\to F\left(k\right)\le F\left(k+1\right)$$
33	31 32	sylan2	$$⊢\left(\phi \wedge k\in \left(N\dots j-1\right)\right)\to F\left(k\right)\le F\left(k+1\right)$$
34	33	adantlr	$$⊢\left(\left(\phi \wedge j\in {\mathbb{Z}}_{\ge N}\right)\wedge k\in \left(N\dots j-1\right)\right)\to F\left(k\right)\le F\left(k+1\right)$$
35	24 30 34	monoord	$$⊢\left(\phi \wedge j\in {\mathbb{Z}}_{\ge N}\right)\to F\left(N\right)\le F\left(j\right)$$
36	6 9 15 3 23 35	climlec2	$$⊢\phi \to F\left(N\right)\le A$$