monoord2xr

Description: Ordering relation for a monotonic sequence, decreasing case. (Contributed by Glauco Siliprandi, 13-Feb-2022)

	Ref	Expression
Hypotheses	monoord2xr.p	$⊢ Ⅎ k φ$
	monoord2xr.k	$⊢ \underline{Ⅎ} k F$
	monoord2xr.n	$⊢ φ \to N \in ℤ_{\geq M}$
	monoord2xr.x	$⊢ (φ \land k \in (M \dots N)) \to F (k) \in ℝ^{*}$
	monoord2xr.l	$⊢ (φ \land k \in (M \dots N - 1)) \to F (k + 1) \leq F (k)$
Assertion	monoord2xr	$⊢ φ \to F (N) \leq F (M)$

Proof

Step	Hyp	Ref	Expression
1		monoord2xr.p	$⊢ Ⅎ k φ$
2		monoord2xr.k	$⊢ \underline{Ⅎ} k F$
3		monoord2xr.n	$⊢ φ \to N \in ℤ_{\geq M}$
4		monoord2xr.x	$⊢ (φ \land k \in (M \dots N)) \to F (k) \in ℝ^{*}$
5		monoord2xr.l	$⊢ (φ \land k \in (M \dots N - 1)) \to F (k + 1) \leq F (k)$
6		nfv	$⊢ Ⅎ k j \in (M \dots N)$
7	1 6	nfan	$⊢ Ⅎ k (φ \land j \in (M \dots N))$
8		nfcv	$⊢ \underline{Ⅎ} k j$
9	2 8	nffv	$⊢ \underline{Ⅎ} k F (j)$
10		nfcv	$⊢ \underline{Ⅎ} k ℝ^{*}$
11	9 10	nfel	$⊢ Ⅎ k F (j) \in ℝ^{*}$
12	7 11	nfim	$⊢ Ⅎ k ((φ \land j \in (M \dots N)) \to F (j) \in ℝ^{*})$
13		eleq1w	$⊢ k = j \to (k \in (M \dots N) \leftrightarrow j \in (M \dots N))$
14	13	anbi2d	$⊢ k = j \to ((φ \land k \in (M \dots N)) \leftrightarrow (φ \land j \in (M \dots N)))$
15		fveq2	$⊢ k = j \to F (k) = F (j)$
16	15	eleq1d	$⊢ k = j \to (F (k) \in ℝ^{} \leftrightarrow F (j) \in ℝ^{})$
17	14 16	imbi12d	$⊢ k = j \to (((φ \land k \in (M \dots N)) \to F (k) \in ℝ^{}) \leftrightarrow ((φ \land j \in (M \dots N)) \to F (j) \in ℝ^{}))$
18	12 17 4	chvarfv	$⊢ (φ \land j \in (M \dots N)) \to F (j) \in ℝ^{*}$
19		nfv	$⊢ Ⅎ k j \in (M \dots N - 1)$
20	1 19	nfan	$⊢ Ⅎ k (φ \land j \in (M \dots N - 1))$
21		nfcv	$⊢ \underline{Ⅎ} k (j + 1)$
22	2 21	nffv	$⊢ \underline{Ⅎ} k F (j + 1)$
23		nfcv	$⊢ \underline{Ⅎ} k \leq$
24	22 23 9	nfbr	$⊢ Ⅎ k F (j + 1) \leq F (j)$
25	20 24	nfim	$⊢ Ⅎ k ((φ \land j \in (M \dots N - 1)) \to F (j + 1) \leq F (j))$
26		eleq1w	$⊢ k = j \to (k \in (M \dots N - 1) \leftrightarrow j \in (M \dots N - 1))$
27	26	anbi2d	$⊢ k = j \to ((φ \land k \in (M \dots N - 1)) \leftrightarrow (φ \land j \in (M \dots N - 1)))$
28		fvoveq1	$⊢ k = j \to F (k + 1) = F (j + 1)$
29	28 15	breq12d	$⊢ k = j \to (F (k + 1) \leq F (k) \leftrightarrow F (j + 1) \leq F (j))$
30	27 29	imbi12d	$⊢ k = j \to (((φ \land k \in (M \dots N - 1)) \to F (k + 1) \leq F (k)) \leftrightarrow ((φ \land j \in (M \dots N - 1)) \to F (j + 1) \leq F (j)))$
31	25 30 5	chvarfv	$⊢ (φ \land j \in (M \dots N - 1)) \to F (j + 1) \leq F (j)$
32	3 18 31	monoord2xrv	$⊢ φ \to F (N) \leq F (M)$

Metamath Proof Explorer

Theorem monoord2xr

Proof