monoordxrv

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

	Ref	Expression
Hypotheses	monoordxrv.1	$⊢ φ \to N \in ℤ_{\geq M}$
	monoordxrv.2	$⊢ (φ \land k \in (M \dots N)) \to F (k) \in ℝ^{*}$
	monoordxrv.3	$⊢ (φ \land k \in (M \dots N - 1)) \to F (k) \leq F (k + 1)$
Assertion	monoordxrv	$⊢ φ \to F (M) \leq F (N)$

Proof

Step	Hyp	Ref	Expression
1		monoordxrv.1	$⊢ φ \to N \in ℤ_{\geq M}$
2		monoordxrv.2	$⊢ (φ \land k \in (M \dots N)) \to F (k) \in ℝ^{*}$
3		monoordxrv.3	$⊢ (φ \land k \in (M \dots N - 1)) \to F (k) \leq F (k + 1)$
4		eluzfz2	$⊢ N \in ℤ_{\geq M} \to N \in (M \dots N)$
5	1 4	syl	$⊢ φ \to N \in (M \dots N)$
6		eleq1	$⊢ x = M \to (x \in (M \dots N) \leftrightarrow M \in (M \dots N))$
7		fveq2	$⊢ x = M \to F (x) = F (M)$
8	7	breq2d	$⊢ x = M \to (F (M) \leq F (x) \leftrightarrow F (M) \leq F (M))$
9	6 8	imbi12d	$⊢ x = M \to ((x \in (M \dots N) \to F (M) \leq F (x)) \leftrightarrow (M \in (M \dots N) \to F (M) \leq F (M)))$
10	9	imbi2d	$⊢ x = M \to ((φ \to (x \in (M \dots N) \to F (M) \leq F (x))) \leftrightarrow (φ \to (M \in (M \dots N) \to F (M) \leq F (M))))$
11		eleq1	$⊢ x = n \to (x \in (M \dots N) \leftrightarrow n \in (M \dots N))$
12		fveq2	$⊢ x = n \to F (x) = F (n)$
13	12	breq2d	$⊢ x = n \to (F (M) \leq F (x) \leftrightarrow F (M) \leq F (n))$
14	11 13	imbi12d	$⊢ x = n \to ((x \in (M \dots N) \to F (M) \leq F (x)) \leftrightarrow (n \in (M \dots N) \to F (M) \leq F (n)))$
15	14	imbi2d	$⊢ x = n \to ((φ \to (x \in (M \dots N) \to F (M) \leq F (x))) \leftrightarrow (φ \to (n \in (M \dots N) \to F (M) \leq F (n))))$
16		eleq1	$⊢ x = n + 1 \to (x \in (M \dots N) \leftrightarrow n + 1 \in (M \dots N))$
17		fveq2	$⊢ x = n + 1 \to F (x) = F (n + 1)$
18	17	breq2d	$⊢ x = n + 1 \to (F (M) \leq F (x) \leftrightarrow F (M) \leq F (n + 1))$
19	16 18	imbi12d	$⊢ x = n + 1 \to ((x \in (M \dots N) \to F (M) \leq F (x)) \leftrightarrow (n + 1 \in (M \dots N) \to F (M) \leq F (n + 1)))$
20	19	imbi2d	$⊢ x = n + 1 \to ((φ \to (x \in (M \dots N) \to F (M) \leq F (x))) \leftrightarrow (φ \to (n + 1 \in (M \dots N) \to F (M) \leq F (n + 1))))$
21		eleq1	$⊢ x = N \to (x \in (M \dots N) \leftrightarrow N \in (M \dots N))$
22		fveq2	$⊢ x = N \to F (x) = F (N)$
23	22	breq2d	$⊢ x = N \to (F (M) \leq F (x) \leftrightarrow F (M) \leq F (N))$
24	21 23	imbi12d	$⊢ x = N \to ((x \in (M \dots N) \to F (M) \leq F (x)) \leftrightarrow (N \in (M \dots N) \to F (M) \leq F (N)))$
25	24	imbi2d	$⊢ x = N \to ((φ \to (x \in (M \dots N) \to F (M) \leq F (x))) \leftrightarrow (φ \to (N \in (M \dots N) \to F (M) \leq F (N))))$
26		eluzfz1	$⊢ N \in ℤ_{\geq M} \to M \in (M \dots N)$
27	1 26	syl	$⊢ φ \to M \in (M \dots N)$
28	2	ralrimiva	$⊢ φ \to \forall k \in (M \dots N) F (k) \in ℝ^{*}$
29		fveq2	$⊢ k = M \to F (k) = F (M)$
30	29	eleq1d	$⊢ k = M \to (F (k) \in ℝ^{} \leftrightarrow F (M) \in ℝ^{})$
31	30	rspcv	$⊢ M \in (M \dots N) \to (\forall k \in (M \dots N) F (k) \in ℝ^{} \to F (M) \in ℝ^{})$
32	27 28 31	sylc	$⊢ φ \to F (M) \in ℝ^{*}$
33	32	xrleidd	$⊢ φ \to F (M) \leq F (M)$
34	33	a1d	$⊢ φ \to (M \in (M \dots N) \to F (M) \leq F (M))$
35	34	a1i	$⊢ M \in ℤ \to (φ \to (M \in (M \dots N) \to F (M) \leq F (M)))$
36		simprl	$⊢ (φ \land (n \in ℤ_{\geq M} \land n + 1 \in (M \dots N))) \to n \in ℤ_{\geq M}$
37		simprr	$⊢ (φ \land (n \in ℤ_{\geq M} \land n + 1 \in (M \dots N))) \to n + 1 \in (M \dots N)$
38		peano2fzr	$⊢ (n \in ℤ_{\geq M} \land n + 1 \in (M \dots N)) \to n \in (M \dots N)$
39	36 37 38	syl2anc	$⊢ (φ \land (n \in ℤ_{\geq M} \land n + 1 \in (M \dots N))) \to n \in (M \dots N)$
40	39	expr	$⊢ (φ \land n \in ℤ_{\geq M}) \to (n + 1 \in (M \dots N) \to n \in (M \dots N))$
41	40	imim1d	$⊢ (φ \land n \in ℤ_{\geq M}) \to ((n \in (M \dots N) \to F (M) \leq F (n)) \to (n + 1 \in (M \dots N) \to F (M) \leq F (n)))$
42		eluzelz	$⊢ n \in ℤ_{\geq M} \to n \in ℤ$
43	36 42	syl	$⊢ (φ \land (n \in ℤ_{\geq M} \land n + 1 \in (M \dots N))) \to n \in ℤ$
44		elfzuz3	$⊢ n + 1 \in (M \dots N) \to N \in ℤ_{\geq (n + 1)}$
45	37 44	syl	$⊢ (φ \land (n \in ℤ_{\geq M} \land n + 1 \in (M \dots N))) \to N \in ℤ_{\geq (n + 1)}$
46		eluzp1m1	$⊢ (n \in ℤ \land N \in ℤ_{\geq (n + 1)}) \to N - 1 \in ℤ_{\geq n}$
47	43 45 46	syl2anc	$⊢ (φ \land (n \in ℤ_{\geq M} \land n + 1 \in (M \dots N))) \to N - 1 \in ℤ_{\geq n}$
48		elfzuzb	$⊢ n \in (M \dots N - 1) \leftrightarrow (n \in ℤ_{\geq M} \land N - 1 \in ℤ_{\geq n})$
49	36 47 48	sylanbrc	$⊢ (φ \land (n \in ℤ_{\geq M} \land n + 1 \in (M \dots N))) \to n \in (M \dots N - 1)$
50	3	ralrimiva	$⊢ φ \to \forall k \in (M \dots N - 1) F (k) \leq F (k + 1)$
51	50	adantr	$⊢ (φ \land (n \in ℤ_{\geq M} \land n + 1 \in (M \dots N))) \to \forall k \in (M \dots N - 1) F (k) \leq F (k + 1)$
52		fveq2	$⊢ k = n \to F (k) = F (n)$
53		fvoveq1	$⊢ k = n \to F (k + 1) = F (n + 1)$
54	52 53	breq12d	$⊢ k = n \to (F (k) \leq F (k + 1) \leftrightarrow F (n) \leq F (n + 1))$
55	54	rspcv	$⊢ n \in (M \dots N - 1) \to (\forall k \in (M \dots N - 1) F (k) \leq F (k + 1) \to F (n) \leq F (n + 1))$
56	49 51 55	sylc	$⊢ (φ \land (n \in ℤ_{\geq M} \land n + 1 \in (M \dots N))) \to F (n) \leq F (n + 1)$
57	32	adantr	$⊢ (φ \land (n \in ℤ_{\geq M} \land n + 1 \in (M \dots N))) \to F (M) \in ℝ^{*}$
58	28	adantr	$⊢ (φ \land (n \in ℤ_{\geq M} \land n + 1 \in (M \dots N))) \to \forall k \in (M \dots N) F (k) \in ℝ^{*}$
59	52	eleq1d	$⊢ k = n \to (F (k) \in ℝ^{} \leftrightarrow F (n) \in ℝ^{})$
60	59	rspcv	$⊢ n \in (M \dots N) \to (\forall k \in (M \dots N) F (k) \in ℝ^{} \to F (n) \in ℝ^{})$
61	39 58 60	sylc	$⊢ (φ \land (n \in ℤ_{\geq M} \land n + 1 \in (M \dots N))) \to F (n) \in ℝ^{*}$
62		fveq2	$⊢ k = n + 1 \to F (k) = F (n + 1)$
63	62	eleq1d	$⊢ k = n + 1 \to (F (k) \in ℝ^{} \leftrightarrow F (n + 1) \in ℝ^{})$
64	63	rspcv	$⊢ n + 1 \in (M \dots N) \to (\forall k \in (M \dots N) F (k) \in ℝ^{} \to F (n + 1) \in ℝ^{})$
65	37 58 64	sylc	$⊢ (φ \land (n \in ℤ_{\geq M} \land n + 1 \in (M \dots N))) \to F (n + 1) \in ℝ^{*}$
66		xrletr	$⊢ (F (M) \in ℝ^{} \land F (n) \in ℝ^{} \land F (n + 1) \in ℝ^{*}) \to ((F (M) \leq F (n) \land F (n) \leq F (n + 1)) \to F (M) \leq F (n + 1))$
67	57 61 65 66	syl3anc	$⊢ (φ \land (n \in ℤ_{\geq M} \land n + 1 \in (M \dots N))) \to ((F (M) \leq F (n) \land F (n) \leq F (n + 1)) \to F (M) \leq F (n + 1))$
68	56 67	mpan2d	$⊢ (φ \land (n \in ℤ_{\geq M} \land n + 1 \in (M \dots N))) \to (F (M) \leq F (n) \to F (M) \leq F (n + 1))$
69	41 68	animpimp2impd	$⊢ n \in ℤ_{\geq M} \to ((φ \to (n \in (M \dots N) \to F (M) \leq F (n))) \to (φ \to (n + 1 \in (M \dots N) \to F (M) \leq F (n + 1))))$
70	10 15 20 25 35 69	uzind4	$⊢ N \in ℤ_{\geq M} \to (φ \to (N \in (M \dots N) \to F (M) \leq F (N)))$
71	1 70	mpcom	$⊢ φ \to (N \in (M \dots N) \to F (M) \leq F (N))$
72	5 71	mpd	$⊢ φ \to F (M) \leq F (N)$

Metamath Proof Explorer

Theorem monoordxrv

Proof