climinf2lem

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

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

Proof

Step	Hyp	Ref	Expression
1		climinf2lem.1	$⊢ Z = ℤ_{\geq M}$
2		climinf2lem.2	$⊢ φ \to M \in ℤ$
3		climinf2lem.3	$⊢ φ \to F : Z ⟶ ℝ$
4		climinf2lem.4	$⊢ (φ \land k \in Z) \to F (k + 1) \leq F (k)$
5		climinf2lem.5	$⊢ φ \to \exists x \in ℝ \forall k \in Z x \leq F (k)$
6	1 2 3 4 5	climinf	$⊢ φ \to F ⇝ sup (ran F ℝ <)$
7	3	frnd	$⊢ φ \to ran F \subseteq ℝ$
8	3	ffnd	$⊢ φ \to F Fn Z$
9	2 1	uzidd2	$⊢ φ \to M \in Z$
10		fnfvelrn	$⊢ (F Fn Z \land M \in Z) \to F (M) \in ran F$
11	8 9 10	syl2anc	$⊢ φ \to F (M) \in ran F$
12	11	ne0d	$⊢ φ \to ran F \neq \emptyset$
13		simpr	$⊢ (φ \land y \in ran F) \to y \in ran F$
14		fvelrnb	$⊢ F Fn Z \to (y \in ran F \leftrightarrow \exists k \in Z F (k) = y)$
15	8 14	syl	$⊢ φ \to (y \in ran F \leftrightarrow \exists k \in Z F (k) = y)$
16	15	adantr	$⊢ (φ \land y \in ran F) \to (y \in ran F \leftrightarrow \exists k \in Z F (k) = y)$
17	13 16	mpbid	$⊢ (φ \land y \in ran F) \to \exists k \in Z F (k) = y$
18	17	adantlr	$⊢ ((φ \land \forall k \in Z x \leq F (k)) \land y \in ran F) \to \exists k \in Z F (k) = y$
19		nfv	$⊢ Ⅎ k φ$
20		nfra1	$⊢ Ⅎ k \forall k \in Z x \leq F (k)$
21	19 20	nfan	$⊢ Ⅎ k (φ \land \forall k \in Z x \leq F (k))$
22		nfv	$⊢ Ⅎ k x \leq y$
23		rspa	$⊢ (\forall k \in Z x \leq F (k) \land k \in Z) \to x \leq F (k)$
24		simpl	$⊢ (x \leq F (k) \land F (k) = y) \to x \leq F (k)$
25		simpr	$⊢ (x \leq F (k) \land F (k) = y) \to F (k) = y$
26	24 25	breqtrd	$⊢ (x \leq F (k) \land F (k) = y) \to x \leq y$
27	26	ex	$⊢ x \leq F (k) \to (F (k) = y \to x \leq y)$
28	23 27	syl	$⊢ (\forall k \in Z x \leq F (k) \land k \in Z) \to (F (k) = y \to x \leq y)$
29	28	ex	$⊢ \forall k \in Z x \leq F (k) \to (k \in Z \to (F (k) = y \to x \leq y))$
30	29	adantl	$⊢ (φ \land \forall k \in Z x \leq F (k)) \to (k \in Z \to (F (k) = y \to x \leq y))$
31	21 22 30	rexlimd	$⊢ (φ \land \forall k \in Z x \leq F (k)) \to (\exists k \in Z F (k) = y \to x \leq y)$
32	31	adantr	$⊢ ((φ \land \forall k \in Z x \leq F (k)) \land y \in ran F) \to (\exists k \in Z F (k) = y \to x \leq y)$
33	18 32	mpd	$⊢ ((φ \land \forall k \in Z x \leq F (k)) \land y \in ran F) \to x \leq y$
34	33	ralrimiva	$⊢ (φ \land \forall k \in Z x \leq F (k)) \to \forall y \in ran F x \leq y$
35	34	adantlr	$⊢ ((φ \land x \in ℝ) \land \forall k \in Z x \leq F (k)) \to \forall y \in ran F x \leq y$
36	35	ex	$⊢ (φ \land x \in ℝ) \to (\forall k \in Z x \leq F (k) \to \forall y \in ran F x \leq y)$
37	36	reximdva	$⊢ φ \to (\exists x \in ℝ \forall k \in Z x \leq F (k) \to \exists x \in ℝ \forall y \in ran F x \leq y)$
38	5 37	mpd	$⊢ φ \to \exists x \in ℝ \forall y \in ran F x \leq y$
39		infxrre	$⊢ (ran F \subseteq ℝ \land ran F \neq \emptyset \land \exists x \in ℝ \forall y \in ran F x \leq y) \to sup (ran F ℝ^{*} <) = sup (ran F ℝ <)$
40	7 12 38 39	syl3anc	$⊢ φ \to sup (ran F ℝ^{*} <) = sup (ran F ℝ <)$
41	6 40	breqtrrd	$⊢ φ \to F ⇝ sup (ran F ℝ^{*} <)$

Metamath Proof Explorer

Theorem climinf2lem

Proof