climinf3

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

	Ref	Expression
Hypotheses	climinf3.1	$⊢ Ⅎ k φ$
	climinf3.2	$⊢ \underline{Ⅎ} k F$
	climinf3.3	$⊢ φ \to M \in ℤ$
	climinf3.4	$⊢ Z = ℤ_{\geq M}$
	climinf3.5	$⊢ φ \to F : Z ⟶ ℝ$
	climinf3.6	$⊢ (φ \land k \in Z) \to F (k + 1) \leq F (k)$
	climinf3.7	$⊢ φ \to F \in dom ⇝$
Assertion	climinf3	$⊢ φ \to F ⇝ inf (ran F ℝ^{*} <)$

Proof

Step	Hyp	Ref	Expression
1		climinf3.1	$⊢ Ⅎ k φ$
2		climinf3.2	$⊢ \underline{Ⅎ} k F$
3		climinf3.3	$⊢ φ \to M \in ℤ$
4		climinf3.4	$⊢ Z = ℤ_{\geq M}$
5		climinf3.5	$⊢ φ \to F : Z ⟶ ℝ$
6		climinf3.6	$⊢ (φ \land k \in Z) \to F (k + 1) \leq F (k)$
7		climinf3.7	$⊢ φ \to F \in dom ⇝$
8	5	ffvelcdmda	$⊢ (φ \land k \in Z) \to F (k) \in ℝ$
9	8	recnd	$⊢ (φ \land k \in Z) \to F (k) \in ℂ$
10	1 9	ralrimia	$⊢ φ \to \forall k \in Z F (k) \in ℂ$
11	2 4	climbddf	$⊢ (M \in ℤ \land F \in dom ⇝ \land \forall k \in Z F (k) \in ℂ) \to \exists x \in ℝ \forall k \in Z \|F (k)\| \leq x$
12	3 7 10 11	syl3anc	$⊢ φ \to \exists x \in ℝ \forall k \in Z \|F (k)\| \leq x$
13		renegcl	$⊢ x \in ℝ \to - x \in ℝ$
14	13	ad2antlr	$⊢ ((φ \land x \in ℝ) \land \forall k \in Z \|F (k)\| \leq x) \to - x \in ℝ$
15		nfv	$⊢ Ⅎ k x \in ℝ$
16	1 15	nfan	$⊢ Ⅎ k (φ \land x \in ℝ)$
17		nfra1	$⊢ Ⅎ k \forall k \in Z \|F (k)\| \leq x$
18	16 17	nfan	$⊢ Ⅎ k ((φ \land x \in ℝ) \land \forall k \in Z \|F (k)\| \leq x)$
19		simpll	$⊢ (((φ \land x \in ℝ) \land \forall k \in Z \|F (k)\| \leq x) \land k \in Z) \to (φ \land x \in ℝ)$
20		simpr	$⊢ (((φ \land x \in ℝ) \land \forall k \in Z \|F (k)\| \leq x) \land k \in Z) \to k \in Z$
21		rspa	$⊢ (\forall k \in Z \|F (k)\| \leq x \land k \in Z) \to \|F (k)\| \leq x$
22	21	adantll	$⊢ (((φ \land x \in ℝ) \land \forall k \in Z \|F (k)\| \leq x) \land k \in Z) \to \|F (k)\| \leq x$
23		simpr	$⊢ (((φ \land x \in ℝ) \land k \in Z) \land \|F (k)\| \leq x) \to \|F (k)\| \leq x$
24	8	ad4ant13	$⊢ (((φ \land x \in ℝ) \land k \in Z) \land \|F (k)\| \leq x) \to F (k) \in ℝ$
25		simpllr	$⊢ (((φ \land x \in ℝ) \land k \in Z) \land \|F (k)\| \leq x) \to x \in ℝ$
26	24 25	absled	$⊢ (((φ \land x \in ℝ) \land k \in Z) \land \|F (k)\| \leq x) \to (\|F (k)\| \leq x \leftrightarrow (- x \leq F (k) \land F (k) \leq x))$
27	23 26	mpbid	$⊢ (((φ \land x \in ℝ) \land k \in Z) \land \|F (k)\| \leq x) \to (- x \leq F (k) \land F (k) \leq x)$
28	27	simpld	$⊢ (((φ \land x \in ℝ) \land k \in Z) \land \|F (k)\| \leq x) \to - x \leq F (k)$
29	19 20 22 28	syl21anc	$⊢ (((φ \land x \in ℝ) \land \forall k \in Z \|F (k)\| \leq x) \land k \in Z) \to - x \leq F (k)$
30	29	ex	$⊢ ((φ \land x \in ℝ) \land \forall k \in Z \|F (k)\| \leq x) \to (k \in Z \to - x \leq F (k))$
31	18 30	ralrimi	$⊢ ((φ \land x \in ℝ) \land \forall k \in Z \|F (k)\| \leq x) \to \forall k \in Z - x \leq F (k)$
32		breq1	$⊢ y = - x \to (y \leq F (k) \leftrightarrow - x \leq F (k))$
33	32	ralbidv	$⊢ y = - x \to (\forall k \in Z y \leq F (k) \leftrightarrow \forall k \in Z - x \leq F (k))$
34	33	rspcev	$⊢ (- x \in ℝ \land \forall k \in Z - x \leq F (k)) \to \exists y \in ℝ \forall k \in Z y \leq F (k)$
35	14 31 34	syl2anc	$⊢ ((φ \land x \in ℝ) \land \forall k \in Z \|F (k)\| \leq x) \to \exists y \in ℝ \forall k \in Z y \leq F (k)$
36	35	rexlimdva2	$⊢ φ \to (\exists x \in ℝ \forall k \in Z \|F (k)\| \leq x \to \exists y \in ℝ \forall k \in Z y \leq F (k))$
37	12 36	mpd	$⊢ φ \to \exists y \in ℝ \forall k \in Z y \leq F (k)$
38	1 2 4 3 5 6 37	climinf2	$⊢ φ \to F ⇝ inf (ran F ℝ^{*} <)$

Metamath Proof Explorer

Theorem climinf3

Proof