monoordxr

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

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

Proof

Step	Hyp	Ref	Expression
1		monoordxr.p	$⊢ Ⅎ k φ$
2		monoordxr.k	$⊢ \underline{Ⅎ} k F$
3		monoordxr.n	$⊢ φ \to N \in ℤ_{\geq M}$
4		monoordxr.x	$⊢ (φ \land k \in (M \dots N)) \to F (k) \in ℝ^{*}$
5		monoordxr.l	$⊢ (φ \land k \in (M \dots N - 1)) \to F (k) \leq F (k + 1)$
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 \leq$
22		nfcv	$⊢ \underline{Ⅎ} k (j + 1)$
23	2 22	nffv	$⊢ \underline{Ⅎ} k F (j + 1)$
24	9 21 23	nfbr	$⊢ Ⅎ k F (j) \leq F (j + 1)$
25	20 24	nfim	$⊢ Ⅎ k ((φ \land j \in (M \dots N - 1)) \to F (j) \leq F (j + 1))$
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	15 28	breq12d	$⊢ k = j \to (F (k) \leq F (k + 1) \leftrightarrow F (j) \leq F (j + 1))$
30	27 29	imbi12d	$⊢ k = j \to (((φ \land k \in (M \dots N - 1)) \to F (k) \leq F (k + 1)) \leftrightarrow ((φ \land j \in (M \dots N - 1)) \to F (j) \leq F (j + 1)))$
31	25 30 5	chvarfv	$⊢ (φ \land j \in (M \dots N - 1)) \to F (j) \leq F (j + 1)$
32	3 18 31	monoordxrv	$⊢ φ \to F (M) \leq F (N)$

Metamath Proof Explorer

Theorem monoordxr

Proof