Theorem climinf2

Description: A convergent, nonincreasing sequence, converges to the infimum of its range. (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypotheses	climinf2.k	$$⊢Ⅎk\phi$$
	climinf2.n	$$⊢\underset{\_}{Ⅎ}kF$$
	climinf2.z	$$⊢Z={\mathbb{Z}}_{\ge M}$$
	climinf2.m	$$⊢\phi \to M\in \mathbb{Z}$$
	climinf2.f	$$⊢\phi \to F:Z⟶ℝ$$
	climinf2.l	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k+1\right)\le F\left(k\right)$$
	climinf2.e	$$⊢\phi \to \exists x\in ℝ\forall k\in Zx\le F\left(k\right)$$
Assertion	climinf2	$$⊢\phi \to F⇝inf\left(\mathrm{ran}F,{ℝ}^{*},<\right)$$

Proof

Step	Hyp	Ref	Expression
1		climinf2.k	$$⊢Ⅎk\phi$$
2		climinf2.n	$$⊢\underset{\_}{Ⅎ}kF$$
3		climinf2.z	$$⊢Z={\mathbb{Z}}_{\ge M}$$
4		climinf2.m	$$⊢\phi \to M\in \mathbb{Z}$$
5		climinf2.f	$$⊢\phi \to F:Z⟶ℝ$$
6		climinf2.l	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k+1\right)\le F\left(k\right)$$
7		climinf2.e	$$⊢\phi \to \exists x\in ℝ\forall k\in Zx\le F\left(k\right)$$
8		nfv	$$⊢Ⅎkj\in Z$$
9	1 8	nfan	$$⊢Ⅎk\left(\phi \wedge j\in Z\right)$$
10		nfcv	$$⊢\underset{\_}{Ⅎ}k\left(j+1\right)$$
11	2 10	nffv	$$⊢\underset{\_}{Ⅎ}kF\left(j+1\right)$$
12		nfcv	$$⊢\underset{\_}{Ⅎ}k\le$$
13		nfcv	$$⊢\underset{\_}{Ⅎ}kj$$
14	2 13	nffv	$$⊢\underset{\_}{Ⅎ}kF\left(j\right)$$
15	11 12 14	nfbr	$$⊢ℲkF\left(j+1\right)\le F\left(j\right)$$
16	9 15	nfim	$$⊢Ⅎk\left(\left(\phi \wedge j\in Z\right)\to F\left(j+1\right)\le F\left(j\right)\right)$$
17		eleq1w	$$⊢k=j\to \left(k\in Z\leftrightarrow j\in Z\right)$$
18	17	anbi2d	$$⊢k=j\to \left(\left(\phi \wedge k\in Z\right)\leftrightarrow \left(\phi \wedge j\in Z\right)\right)$$
19		fvoveq1	$$⊢k=j\to F\left(k+1\right)=F\left(j+1\right)$$
20		fveq2	$$⊢k=j\to F\left(k\right)=F\left(j\right)$$
21	19 20	breq12d	$$⊢k=j\to \left(F\left(k+1\right)\le F\left(k\right)\leftrightarrow F\left(j+1\right)\le F\left(j\right)\right)$$
22	18 21	imbi12d	$$⊢k=j\to \left(\left(\left(\phi \wedge k\in Z\right)\to F\left(k+1\right)\le F\left(k\right)\right)\leftrightarrow \left(\left(\phi \wedge j\in Z\right)\to F\left(j+1\right)\le F\left(j\right)\right)\right)$$
23	16 22 6	chvarfv	$$⊢\left(\phi \wedge j\in Z\right)\to F\left(j+1\right)\le F\left(j\right)$$
24		breq1	$$⊢x=y\to \left(x\le F\left(k\right)\leftrightarrow y\le F\left(k\right)\right)$$
25	24	ralbidv	$$⊢x=y\to \left(\forall k\in Zx\le F\left(k\right)\leftrightarrow \forall k\in Zy\le F\left(k\right)\right)$$
26		nfv	$$⊢Ⅎjy\le F\left(k\right)$$
27		nfcv	$$⊢\underset{\_}{Ⅎ}ky$$
28	27 12 14	nfbr	$$⊢Ⅎky\le F\left(j\right)$$
29	20	breq2d	$$⊢k=j\to \left(y\le F\left(k\right)\leftrightarrow y\le F\left(j\right)\right)$$
30	26 28 29	cbvralw	$$⊢\forall k\in Zy\le F\left(k\right)\leftrightarrow \forall j\in Zy\le F\left(j\right)$$
31	30	a1i	$$⊢x=y\to \left(\forall k\in Zy\le F\left(k\right)\leftrightarrow \forall j\in Zy\le F\left(j\right)\right)$$
32	25 31	bitrd	$$⊢x=y\to \left(\forall k\in Zx\le F\left(k\right)\leftrightarrow \forall j\in Zy\le F\left(j\right)\right)$$
33	32	cbvrexvw	$$⊢\exists x\in ℝ\forall k\in Zx\le F\left(k\right)\leftrightarrow \exists y\in ℝ\forall j\in Zy\le F\left(j\right)$$
34	7 33	sylib	$$⊢\phi \to \exists y\in ℝ\forall j\in Zy\le F\left(j\right)$$
35	3 4 5 23 34	climinf2lem	$$⊢\phi \to F⇝inf\left(\mathrm{ran}F,{ℝ}^{*},<\right)$$