climinf

Description: A bounded monotonic nonincreasing sequence converges to the infimum of its range. (Contributed by Glauco Siliprandi, 29-Jun-2017) (Revised by AV, 15-Sep-2020)

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

Proof

Step	Hyp	Ref	Expression
1		climinf.3	$⊢ Z = ℤ_{\geq M}$
2		climinf.4	$⊢ φ \to M \in ℤ$
3		climinf.5	$⊢ φ \to F : Z ⟶ ℝ$
4		climinf.6	$⊢ (φ \land k \in Z) \to F (k + 1) \leq F (k)$
5		climinf.7	$⊢ φ \to \exists x \in ℝ \forall k \in Z x \leq F (k)$
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		breq2	$⊢ y = F (k) \to (x \leq y \leftrightarrow x \leq F (k))$
15	14	ralrn	$⊢ F Fn Z \to (\forall y \in ran F x \leq y \leftrightarrow \forall k \in Z x \leq F (k))$
16	15	rexbidv	$⊢ F Fn Z \to (\exists x \in ℝ \forall y \in ran F x \leq y \leftrightarrow \exists x \in ℝ \forall k \in Z x \leq F (k))$
17	7 16	syl	$⊢ φ \to (\exists x \in ℝ \forall y \in ran F x \leq y \leftrightarrow \exists x \in ℝ \forall k \in Z x \leq F (k))$
18	5 17	mpbird	$⊢ φ \to \exists x \in ℝ \forall y \in ran F x \leq y$
19	6 13 18	3jca	$⊢ φ \to (ran F \subseteq ℝ \land ran F \neq \emptyset \land \exists x \in ℝ \forall y \in ran F x \leq y)$
20	19	adantr	$⊢ (φ \land y \in ℝ^{+}) \to (ran F \subseteq ℝ \land ran F \neq \emptyset \land \exists x \in ℝ \forall y \in ran F x \leq y)$
21		infrecl	$⊢ (ran F \subseteq ℝ \land ran F \neq \emptyset \land \exists x \in ℝ \forall y \in ran F x \leq y) \to inf (ran F ℝ <) \in ℝ$
22	20 21	syl	$⊢ (φ \land y \in ℝ^{+}) \to inf (ran F ℝ <) \in ℝ$
23		simpr	$⊢ (φ \land y \in ℝ^{+}) \to y \in ℝ^{+}$
24	22 23	ltaddrpd	$⊢ (φ \land y \in ℝ^{+}) \to inf (ran F ℝ <) < inf (ran F ℝ <) + y$
25		rpre	$⊢ y \in ℝ^{+} \to y \in ℝ$
26	25	adantl	$⊢ (φ \land y \in ℝ^{+}) \to y \in ℝ$
27	22 26	readdcld	$⊢ (φ \land y \in ℝ^{+}) \to inf (ran F ℝ <) + y \in ℝ$
28		infrglb	$⊢ ((ran F \subseteq ℝ \land ran F \neq \emptyset \land \exists x \in ℝ \forall y \in ran F x \leq y) \land inf (ran F ℝ <) + y \in ℝ) \to (inf (ran F ℝ <) < inf (ran F ℝ <) + y \leftrightarrow \exists k \in ran F k < inf (ran F ℝ <) + y)$
29	20 27 28	syl2anc	$⊢ (φ \land y \in ℝ^{+}) \to (inf (ran F ℝ <) < inf (ran F ℝ <) + y \leftrightarrow \exists k \in ran F k < inf (ran F ℝ <) + y)$
30	24 29	mpbid	$⊢ (φ \land y \in ℝ^{+}) \to \exists k \in ran F k < inf (ran F ℝ <) + y$
31	6	sselda	$⊢ (φ \land k \in ran F) \to k \in ℝ$
32	31	adantlr	$⊢ ((φ \land y \in ℝ^{+}) \land k \in ran F) \to k \in ℝ$
33	22	adantr	$⊢ ((φ \land y \in ℝ^{+}) \land k \in ran F) \to inf (ran F ℝ <) \in ℝ$
34	25	ad2antlr	$⊢ ((φ \land y \in ℝ^{+}) \land k \in ran F) \to y \in ℝ$
35	33 34	readdcld	$⊢ ((φ \land y \in ℝ^{+}) \land k \in ran F) \to inf (ran F ℝ <) + y \in ℝ$
36	32 35 34	ltsub1d	$⊢ ((φ \land y \in ℝ^{+}) \land k \in ran F) \to (k < inf (ran F ℝ <) + y \leftrightarrow k - y < inf (ran F ℝ <) + y - y)$
37	6 13 18 21	syl3anc	$⊢ φ \to inf (ran F ℝ <) \in ℝ$
38	37	recnd	$⊢ φ \to inf (ran F ℝ <) \in ℂ$
39	38	ad2antrr	$⊢ ((φ \land y \in ℝ^{+}) \land k \in ran F) \to inf (ran F ℝ <) \in ℂ$
40	34	recnd	$⊢ ((φ \land y \in ℝ^{+}) \land k \in ran F) \to y \in ℂ$
41	39 40	pncand	$⊢ ((φ \land y \in ℝ^{+}) \land k \in ran F) \to inf (ran F ℝ <) + y - y = inf (ran F ℝ <)$
42	41	breq2d	$⊢ ((φ \land y \in ℝ^{+}) \land k \in ran F) \to (k - y < inf (ran F ℝ <) + y - y \leftrightarrow k - y < inf (ran F ℝ <))$
43	36 42	bitrd	$⊢ ((φ \land y \in ℝ^{+}) \land k \in ran F) \to (k < inf (ran F ℝ <) + y \leftrightarrow k - y < inf (ran F ℝ <))$
44	43	biimpd	$⊢ ((φ \land y \in ℝ^{+}) \land k \in ran F) \to (k < inf (ran F ℝ <) + y \to k - y < inf (ran F ℝ <))$
45	44	reximdva	$⊢ (φ \land y \in ℝ^{+}) \to (\exists k \in ran F k < inf (ran F ℝ <) + y \to \exists k \in ran F k - y < inf (ran F ℝ <))$
46	30 45	mpd	$⊢ (φ \land y \in ℝ^{+}) \to \exists k \in ran F k - y < inf (ran F ℝ <)$
47		oveq1	$⊢ k = F (j) \to k - y = F (j) - y$
48	47	breq1d	$⊢ k = F (j) \to (k - y < inf (ran F ℝ <) \leftrightarrow F (j) - y < inf (ran F ℝ <))$
49	48	rexrn	$⊢ F Fn Z \to (\exists k \in ran F k - y < inf (ran F ℝ <) \leftrightarrow \exists j \in Z F (j) - y < inf (ran F ℝ <))$
50	7 49	syl	$⊢ φ \to (\exists k \in ran F k - y < inf (ran F ℝ <) \leftrightarrow \exists j \in Z F (j) - y < inf (ran F ℝ <))$
51	50	biimpa	$⊢ (φ \land \exists k \in ran F k - y < inf (ran F ℝ <)) \to \exists j \in Z F (j) - y < inf (ran F ℝ <)$
52	46 51	syldan	$⊢ (φ \land y \in ℝ^{+}) \to \exists j \in Z F (j) - y < inf (ran F ℝ <)$
53	3	adantr	$⊢ (φ \land y \in ℝ^{+}) \to F : Z ⟶ ℝ$
54	1	uztrn2	$⊢ (j \in Z \land k \in ℤ_{\geq j}) \to k \in Z$
55		ffvelcdm	$⊢ (F : Z ⟶ ℝ \land k \in Z) \to F (k) \in ℝ$
56	53 54 55	syl2an	$⊢ ((φ \land y \in ℝ^{+}) \land (j \in Z \land k \in ℤ_{\geq j})) \to F (k) \in ℝ$
57		simpl	$⊢ (j \in Z \land k \in ℤ_{\geq j}) \to j \in Z$
58		ffvelcdm	$⊢ (F : Z ⟶ ℝ \land j \in Z) \to F (j) \in ℝ$
59	53 57 58	syl2an	$⊢ ((φ \land y \in ℝ^{+}) \land (j \in Z \land k \in ℤ_{\geq j})) \to F (j) \in ℝ$
60	37	ad2antrr	$⊢ ((φ \land y \in ℝ^{+}) \land (j \in Z \land k \in ℤ_{\geq j})) \to inf (ran F ℝ <) \in ℝ$
61		simprr	$⊢ ((φ \land y \in ℝ^{+}) \land (j \in Z \land k \in ℤ_{\geq j})) \to k \in ℤ_{\geq j}$
62		fzssuz	$⊢ (j \dots k) \subseteq ℤ_{\geq j}$
63		uzss	$⊢ j \in ℤ_{\geq M} \to ℤ_{\geq j} \subseteq ℤ_{\geq M}$
64	63 1	sseqtrrdi	$⊢ j \in ℤ_{\geq M} \to ℤ_{\geq j} \subseteq Z$
65	64 1	eleq2s	$⊢ j \in Z \to ℤ_{\geq j} \subseteq Z$
66	65	ad2antrl	$⊢ ((φ \land y \in ℝ^{+}) \land (j \in Z \land k \in ℤ_{\geq j})) \to ℤ_{\geq j} \subseteq Z$
67	62 66	sstrid	$⊢ ((φ \land y \in ℝ^{+}) \land (j \in Z \land k \in ℤ_{\geq j})) \to (j \dots k) \subseteq Z$
68		ffvelcdm	$⊢ (F : Z ⟶ ℝ \land n \in Z) \to F (n) \in ℝ$
69	68	ralrimiva	$⊢ F : Z ⟶ ℝ \to \forall n \in Z F (n) \in ℝ$
70	3 69	syl	$⊢ φ \to \forall n \in Z F (n) \in ℝ$
71	70	ad2antrr	$⊢ ((φ \land y \in ℝ^{+}) \land (j \in Z \land k \in ℤ_{\geq j})) \to \forall n \in Z F (n) \in ℝ$
72		ssralv	$⊢ (j \dots k) \subseteq Z \to (\forall n \in Z F (n) \in ℝ \to \forall n \in (j \dots k) F (n) \in ℝ)$
73	67 71 72	sylc	$⊢ ((φ \land y \in ℝ^{+}) \land (j \in Z \land k \in ℤ_{\geq j})) \to \forall n \in (j \dots k) F (n) \in ℝ$
74	73	r19.21bi	$⊢ (((φ \land y \in ℝ^{+}) \land (j \in Z \land k \in ℤ_{\geq j})) \land n \in (j \dots k)) \to F (n) \in ℝ$
75		fzssuz	$⊢ (j \dots k - 1) \subseteq ℤ_{\geq j}$
76	75 66	sstrid	$⊢ ((φ \land y \in ℝ^{+}) \land (j \in Z \land k \in ℤ_{\geq j})) \to (j \dots k - 1) \subseteq Z$
77	76	sselda	$⊢ (((φ \land y \in ℝ^{+}) \land (j \in Z \land k \in ℤ_{\geq j})) \land n \in (j \dots k - 1)) \to n \in Z$
78	4	ralrimiva	$⊢ φ \to \forall k \in Z F (k + 1) \leq F (k)$
79	78	ad2antrr	$⊢ ((φ \land y \in ℝ^{+}) \land (j \in Z \land k \in ℤ_{\geq j})) \to \forall k \in Z F (k + 1) \leq F (k)$
80		fvoveq1	$⊢ k = n \to F (k + 1) = F (n + 1)$
81		fveq2	$⊢ k = n \to F (k) = F (n)$
82	80 81	breq12d	$⊢ k = n \to (F (k + 1) \leq F (k) \leftrightarrow F (n + 1) \leq F (n))$
83	82	rspccva	$⊢ (\forall k \in Z F (k + 1) \leq F (k) \land n \in Z) \to F (n + 1) \leq F (n)$
84	79 83	sylan	$⊢ (((φ \land y \in ℝ^{+}) \land (j \in Z \land k \in ℤ_{\geq j})) \land n \in Z) \to F (n + 1) \leq F (n)$
85	77 84	syldan	$⊢ (((φ \land y \in ℝ^{+}) \land (j \in Z \land k \in ℤ_{\geq j})) \land n \in (j \dots k - 1)) \to F (n + 1) \leq F (n)$
86	61 74 85	monoord2	$⊢ ((φ \land y \in ℝ^{+}) \land (j \in Z \land k \in ℤ_{\geq j})) \to F (k) \leq F (j)$
87	56 59 60 86	lesub1dd	$⊢ ((φ \land y \in ℝ^{+}) \land (j \in Z \land k \in ℤ_{\geq j})) \to F (k) - inf (ran F ℝ <) \leq F (j) - inf (ran F ℝ <)$
88	56 60	resubcld	$⊢ ((φ \land y \in ℝ^{+}) \land (j \in Z \land k \in ℤ_{\geq j})) \to F (k) - inf (ran F ℝ <) \in ℝ$
89	59 60	resubcld	$⊢ ((φ \land y \in ℝ^{+}) \land (j \in Z \land k \in ℤ_{\geq j})) \to F (j) - inf (ran F ℝ <) \in ℝ$
90	25	ad2antlr	$⊢ ((φ \land y \in ℝ^{+}) \land (j \in Z \land k \in ℤ_{\geq j})) \to y \in ℝ$
91		lelttr	$⊢ (F (k) - inf (ran F ℝ <) \in ℝ \land F (j) - inf (ran F ℝ <) \in ℝ \land y \in ℝ) \to ((F (k) - inf (ran F ℝ <) \leq F (j) - inf (ran F ℝ <) \land F (j) - inf (ran F ℝ <) < y) \to F (k) - inf (ran F ℝ <) < y)$
92	88 89 90 91	syl3anc	$⊢ ((φ \land y \in ℝ^{+}) \land (j \in Z \land k \in ℤ_{\geq j})) \to ((F (k) - inf (ran F ℝ <) \leq F (j) - inf (ran F ℝ <) \land F (j) - inf (ran F ℝ <) < y) \to F (k) - inf (ran F ℝ <) < y)$
93	87 92	mpand	$⊢ ((φ \land y \in ℝ^{+}) \land (j \in Z \land k \in ℤ_{\geq j})) \to (F (j) - inf (ran F ℝ <) < y \to F (k) - inf (ran F ℝ <) < y)$
94		ltsub23	$⊢ (F (j) \in ℝ \land y \in ℝ \land inf (ran F ℝ <) \in ℝ) \to (F (j) - y < inf (ran F ℝ <) \leftrightarrow F (j) - inf (ran F ℝ <) < y)$
95	59 90 60 94	syl3anc	$⊢ ((φ \land y \in ℝ^{+}) \land (j \in Z \land k \in ℤ_{\geq j})) \to (F (j) - y < inf (ran F ℝ <) \leftrightarrow F (j) - inf (ran F ℝ <) < y)$
96	6	ad2antrr	$⊢ ((φ \land y \in ℝ^{+}) \land (j \in Z \land k \in ℤ_{\geq j})) \to ran F \subseteq ℝ$
97	7	adantr	$⊢ (φ \land y \in ℝ^{+}) \to F Fn Z$
98		fnfvelrn	$⊢ (F Fn Z \land k \in Z) \to F (k) \in ran F$
99	97 54 98	syl2an	$⊢ ((φ \land y \in ℝ^{+}) \land (j \in Z \land k \in ℤ_{\geq j})) \to F (k) \in ran F$
100	96 99	sseldd	$⊢ ((φ \land y \in ℝ^{+}) \land (j \in Z \land k \in ℤ_{\geq j})) \to F (k) \in ℝ$
101	18	ad2antrr	$⊢ ((φ \land y \in ℝ^{+}) \land (j \in Z \land k \in ℤ_{\geq j})) \to \exists x \in ℝ \forall y \in ran F x \leq y$
102		infrelb	$⊢ (ran F \subseteq ℝ \land \exists x \in ℝ \forall y \in ran F x \leq y \land F (k) \in ran F) \to inf (ran F ℝ <) \leq F (k)$
103	96 101 99 102	syl3anc	$⊢ ((φ \land y \in ℝ^{+}) \land (j \in Z \land k \in ℤ_{\geq j})) \to inf (ran F ℝ <) \leq F (k)$
104	60 100 103	abssubge0d	$⊢ ((φ \land y \in ℝ^{+}) \land (j \in Z \land k \in ℤ_{\geq j})) \to \|F (k) - inf (ran F ℝ <)\| = F (k) - inf (ran F ℝ <)$
105	104	breq1d	$⊢ ((φ \land y \in ℝ^{+}) \land (j \in Z \land k \in ℤ_{\geq j})) \to (\|F (k) - inf (ran F ℝ <)\| < y \leftrightarrow F (k) - inf (ran F ℝ <) < y)$
106	93 95 105	3imtr4d	$⊢ ((φ \land y \in ℝ^{+}) \land (j \in Z \land k \in ℤ_{\geq j})) \to (F (j) - y < inf (ran F ℝ <) \to \|F (k) - inf (ran F ℝ <)\| < y)$
107	106	anassrs	$⊢ (((φ \land y \in ℝ^{+}) \land j \in Z) \land k \in ℤ_{\geq j}) \to (F (j) - y < inf (ran F ℝ <) \to \|F (k) - inf (ran F ℝ <)\| < y)$
108	107	ralrimdva	$⊢ ((φ \land y \in ℝ^{+}) \land j \in Z) \to (F (j) - y < inf (ran F ℝ <) \to \forall k \in ℤ_{\geq j} \|F (k) - inf (ran F ℝ <)\| < y)$
109	108	reximdva	$⊢ (φ \land y \in ℝ^{+}) \to (\exists j \in Z F (j) - y < inf (ran F ℝ <) \to \exists j \in Z \forall k \in ℤ_{\geq j} \|F (k) - inf (ran F ℝ <)\| < y)$
110	52 109	mpd	$⊢ (φ \land y \in ℝ^{+}) \to \exists j \in Z \forall k \in ℤ_{\geq j} \|F (k) - inf (ran F ℝ <)\| < y$
111	110	ralrimiva	$⊢ φ \to \forall y \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \|F (k) - inf (ran F ℝ <)\| < y$
112	1	fvexi	$⊢ Z \in V$
113		fex	$⊢ (F : Z ⟶ ℝ \land Z \in V) \to F \in V$
114	3 112 113	sylancl	$⊢ φ \to F \in V$
115		eqidd	$⊢ (φ \land k \in Z) \to F (k) = F (k)$
116	3	ffvelcdmda	$⊢ (φ \land k \in Z) \to F (k) \in ℝ$
117	116	recnd	$⊢ (φ \land k \in Z) \to F (k) \in ℂ$
118	1 2 114 115 38 117	clim2c	$⊢ φ \to (F ⇝ inf (ran F ℝ <) \leftrightarrow \forall y \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \|F (k) - inf (ran F ℝ <)\| < y)$
119	111 118	mpbird	$⊢ φ \to F ⇝ inf (ran F ℝ <)$

Metamath Proof Explorer

Theorem climinf

Proof