monoord

Description: Ordering relation for a monotonic sequence, increasing case. (Contributed by NM, 13-Mar-2005) (Revised by Mario Carneiro, 9-Feb-2014)

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

Proof

Step	Hyp	Ref	Expression
1		monoord.1	$⊢ φ \to N \in ℤ_{\geq M}$
2		monoord.2	$⊢ (φ \land k \in (M \dots N)) \to F (k) \in ℝ$
3		monoord.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		fveq2	$⊢ k = M \to F (k) = F (M)$
27	26	eleq1d	$⊢ k = M \to (F (k) \in ℝ \leftrightarrow F (M) \in ℝ)$
28	2	ralrimiva	$⊢ φ \to \forall k \in (M \dots N) F (k) \in ℝ$
29		eluzfz1	$⊢ N \in ℤ_{\geq M} \to M \in (M \dots N)$
30	1 29	syl	$⊢ φ \to M \in (M \dots N)$
31	27 28 30	rspcdva	$⊢ φ \to F (M) \in ℝ$
32	31	leidd	$⊢ φ \to F (M) \leq F (M)$
33	32	a1d	$⊢ φ \to (M \in (M \dots N) \to F (M) \leq F (M))$
34		peano2fzr	$⊢ (n \in ℤ_{\geq M} \land n + 1 \in (M \dots N)) \to n \in (M \dots N)$
35	34	adantl	$⊢ (φ \land (n \in ℤ_{\geq M} \land n + 1 \in (M \dots N))) \to n \in (M \dots N)$
36	35	expr	$⊢ (φ \land n \in ℤ_{\geq M}) \to (n + 1 \in (M \dots N) \to n \in (M \dots N))$
37	36	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)))$
38		fveq2	$⊢ k = n \to F (k) = F (n)$
39		fvoveq1	$⊢ k = n \to F (k + 1) = F (n + 1)$
40	38 39	breq12d	$⊢ k = n \to (F (k) \leq F (k + 1) \leftrightarrow F (n) \leq F (n + 1))$
41	3	ralrimiva	$⊢ φ \to \forall k \in (M \dots N - 1) F (k) \leq F (k + 1)$
42	41	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)$
43		simprl	$⊢ (φ \land (n \in ℤ_{\geq M} \land n + 1 \in (M \dots N))) \to n \in ℤ_{\geq M}$
44		eluzelz	$⊢ n \in ℤ_{\geq M} \to n \in ℤ$
45	43 44	syl	$⊢ (φ \land (n \in ℤ_{\geq M} \land n + 1 \in (M \dots N))) \to n \in ℤ$
46		simprr	$⊢ (φ \land (n \in ℤ_{\geq M} \land n + 1 \in (M \dots N))) \to n + 1 \in (M \dots N)$
47		elfzuz3	$⊢ n + 1 \in (M \dots N) \to N \in ℤ_{\geq (n + 1)}$
48	46 47	syl	$⊢ (φ \land (n \in ℤ_{\geq M} \land n + 1 \in (M \dots N))) \to N \in ℤ_{\geq (n + 1)}$
49		eluzp1m1	$⊢ (n \in ℤ \land N \in ℤ_{\geq (n + 1)}) \to N - 1 \in ℤ_{\geq n}$
50	45 48 49	syl2anc	$⊢ (φ \land (n \in ℤ_{\geq M} \land n + 1 \in (M \dots N))) \to N - 1 \in ℤ_{\geq n}$
51		elfzuzb	$⊢ n \in (M \dots N - 1) \leftrightarrow (n \in ℤ_{\geq M} \land N - 1 \in ℤ_{\geq n})$
52	43 50 51	sylanbrc	$⊢ (φ \land (n \in ℤ_{\geq M} \land n + 1 \in (M \dots N))) \to n \in (M \dots N - 1)$
53	40 42 52	rspcdva	$⊢ (φ \land (n \in ℤ_{\geq M} \land n + 1 \in (M \dots N))) \to F (n) \leq F (n + 1)$
54	31	adantr	$⊢ (φ \land (n \in ℤ_{\geq M} \land n + 1 \in (M \dots N))) \to F (M) \in ℝ$
55	38	eleq1d	$⊢ k = n \to (F (k) \in ℝ \leftrightarrow F (n) \in ℝ)$
56	28	adantr	$⊢ (φ \land (n \in ℤ_{\geq M} \land n + 1 \in (M \dots N))) \to \forall k \in (M \dots N) F (k) \in ℝ$
57	55 56 35	rspcdva	$⊢ (φ \land (n \in ℤ_{\geq M} \land n + 1 \in (M \dots N))) \to F (n) \in ℝ$
58		fveq2	$⊢ k = n + 1 \to F (k) = F (n + 1)$
59	58	eleq1d	$⊢ k = n + 1 \to (F (k) \in ℝ \leftrightarrow F (n + 1) \in ℝ)$
60	59 56 46	rspcdva	$⊢ (φ \land (n \in ℤ_{\geq M} \land n + 1 \in (M \dots N))) \to F (n + 1) \in ℝ$
61		letr	$⊢ (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))$
62	54 57 60 61	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))$
63	53 62	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))$
64	37 63	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))))$
65	10 15 20 25 33 64	uzind4i	$⊢ N \in ℤ_{\geq M} \to (φ \to (N \in (M \dots N) \to F (M) \leq F (N)))$
66	1 65	mpcom	$⊢ φ \to (N \in (M \dots N) \to F (M) \leq F (N))$
67	5 66	mpd	$⊢ φ \to F (M) \leq F (N)$

Metamath Proof Explorer

Theorem monoord

Proof