Theorem climlec2

Description: Comparison of a constant to the limit of a sequence. (Contributed by NM, 28-Feb-2008) (Revised by Mario Carneiro, 1-Feb-2014)

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

Proof

Step	Hyp	Ref	Expression
1		clim2ser.1	$$⊢Z={\mathbb{Z}}_{\ge M}$$
2		climlec2.2	$$⊢\phi \to M\in \mathbb{Z}$$
3		climlec2.3	$$⊢\phi \to A\in ℝ$$
4		climlec2.4	$$⊢\phi \to F⇝B$$
5		climlec2.5	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k\right)\in ℝ$$
6		climlec2.6	$$⊢\left(\phi \wedge k\in Z\right)\to A\le F\left(k\right)$$
7	3	recnd	$$⊢\phi \to A\in ℂ$$
8		0z	$$⊢0\in \mathbb{Z}$$
9		uzssz	$$⊢{\mathbb{Z}}_{\ge 0}\subseteq \mathbb{Z}$$
10		zex	$$⊢\mathbb{Z}\in \mathrm{V}$$
11	9 10	climconst2	$$⊢\left(A\in ℂ\wedge 0\in \mathbb{Z}\right)\to \left(\mathbb{Z}\times \left\{A\right\}\right)⇝A$$
12	7 8 11	sylancl	$$⊢\phi \to \left(\mathbb{Z}\times \left\{A\right\}\right)⇝A$$
13		eluzelz	$$⊢k\in {\mathbb{Z}}_{\ge M}\to k\in \mathbb{Z}$$
14	13 1	eleq2s	$$⊢k\in Z\to k\in \mathbb{Z}$$
15		fvconst2g	$$⊢\left(A\in ℝ\wedge k\in \mathbb{Z}\right)\to \left(\mathbb{Z}\times \left\{A\right\}\right)\left(k\right)=A$$
16	3 14 15	syl2an	$$⊢\left(\phi \wedge k\in Z\right)\to \left(\mathbb{Z}\times \left\{A\right\}\right)\left(k\right)=A$$
17	3	adantr	$$⊢\left(\phi \wedge k\in Z\right)\to A\in ℝ$$
18	16 17	eqeltrd	$$⊢\left(\phi \wedge k\in Z\right)\to \left(\mathbb{Z}\times \left\{A\right\}\right)\left(k\right)\in ℝ$$
19	16 6	eqbrtrd	$$⊢\left(\phi \wedge k\in Z\right)\to \left(\mathbb{Z}\times \left\{A\right\}\right)\left(k\right)\le F\left(k\right)$$
20	1 2 12 4 18 5 19	climle	$$⊢\phi \to A\le B$$