monoord2

Description: Ordering relation for a monotonic sequence, decreasing case. (Contributed by Mario Carneiro, 18-Jul-2014)

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

Proof

Step	Hyp	Ref	Expression
1		monoord2.1	$⊢ φ \to N \in ℤ_{\geq M}$
2		monoord2.2	$⊢ (φ \land k \in (M \dots N)) \to F (k) \in ℝ$
3		monoord2.3	$⊢ (φ \land k \in (M \dots N - 1)) \to F (k + 1) \leq F (k)$
4	2	renegcld	$⊢ (φ \land k \in (M \dots N)) \to - F (k) \in ℝ$
5	4	fmpttd	$⊢ φ \to (k \in (M \dots N) ⟼ - F (k)) : (M \dots N) ⟶ ℝ$
6	5	ffvelcdmda	$⊢ (φ \land n \in (M \dots N)) \to (k \in (M \dots N) ⟼ - F (k)) (n) \in ℝ$
7	3	ralrimiva	$⊢ φ \to \forall k \in (M \dots N - 1) F (k + 1) \leq F (k)$
8		fvoveq1	$⊢ k = n \to F (k + 1) = F (n + 1)$
9		fveq2	$⊢ k = n \to F (k) = F (n)$
10	8 9	breq12d	$⊢ k = n \to (F (k + 1) \leq F (k) \leftrightarrow F (n + 1) \leq F (n))$
11	10	cbvralvw	$⊢ \forall k \in (M \dots N - 1) F (k + 1) \leq F (k) \leftrightarrow \forall n \in (M \dots N - 1) F (n + 1) \leq F (n)$
12	7 11	sylib	$⊢ φ \to \forall n \in (M \dots N - 1) F (n + 1) \leq F (n)$
13	12	r19.21bi	$⊢ (φ \land n \in (M \dots N - 1)) \to F (n + 1) \leq F (n)$
14		fveq2	$⊢ k = n + 1 \to F (k) = F (n + 1)$
15	14	eleq1d	$⊢ k = n + 1 \to (F (k) \in ℝ \leftrightarrow F (n + 1) \in ℝ)$
16	2	ralrimiva	$⊢ φ \to \forall k \in (M \dots N) F (k) \in ℝ$
17	16	adantr	$⊢ (φ \land n \in (M \dots N - 1)) \to \forall k \in (M \dots N) F (k) \in ℝ$
18		fzp1elp1	$⊢ n \in (M \dots N - 1) \to n + 1 \in (M \dots N - 1 + 1)$
19	18	adantl	$⊢ (φ \land n \in (M \dots N - 1)) \to n + 1 \in (M \dots N - 1 + 1)$
20		eluzelz	$⊢ N \in ℤ_{\geq M} \to N \in ℤ$
21	1 20	syl	$⊢ φ \to N \in ℤ$
22	21	zcnd	$⊢ φ \to N \in ℂ$
23		ax-1cn	$⊢ 1 \in ℂ$
24		npcan	$⊢ (N \in ℂ \land 1 \in ℂ) \to N - 1 + 1 = N$
25	22 23 24	sylancl	$⊢ φ \to N - 1 + 1 = N$
26	25	oveq2d	$⊢ φ \to (M \dots N - 1 + 1) = (M \dots N)$
27	26	adantr	$⊢ (φ \land n \in (M \dots N - 1)) \to (M \dots N - 1 + 1) = (M \dots N)$
28	19 27	eleqtrd	$⊢ (φ \land n \in (M \dots N - 1)) \to n + 1 \in (M \dots N)$
29	15 17 28	rspcdva	$⊢ (φ \land n \in (M \dots N - 1)) \to F (n + 1) \in ℝ$
30	9	eleq1d	$⊢ k = n \to (F (k) \in ℝ \leftrightarrow F (n) \in ℝ)$
31		fzssp1	$⊢ (M \dots N - 1) \subseteq (M \dots N - 1 + 1)$
32	31 26	sseqtrid	$⊢ φ \to (M \dots N - 1) \subseteq (M \dots N)$
33	32	sselda	$⊢ (φ \land n \in (M \dots N - 1)) \to n \in (M \dots N)$
34	30 17 33	rspcdva	$⊢ (φ \land n \in (M \dots N - 1)) \to F (n) \in ℝ$
35	29 34	lenegd	$⊢ (φ \land n \in (M \dots N - 1)) \to (F (n + 1) \leq F (n) \leftrightarrow - F (n) \leq - F (n + 1))$
36	13 35	mpbid	$⊢ (φ \land n \in (M \dots N - 1)) \to - F (n) \leq - F (n + 1)$
37	9	negeqd	$⊢ k = n \to - F (k) = - F (n)$
38		eqid	$⊢ (k \in (M \dots N) ⟼ - F (k)) = (k \in (M \dots N) ⟼ - F (k))$
39		negex	$⊢ - F (n) \in V$
40	37 38 39	fvmpt	$⊢ n \in (M \dots N) \to (k \in (M \dots N) ⟼ - F (k)) (n) = - F (n)$
41	33 40	syl	$⊢ (φ \land n \in (M \dots N - 1)) \to (k \in (M \dots N) ⟼ - F (k)) (n) = - F (n)$
42	14	negeqd	$⊢ k = n + 1 \to - F (k) = - F (n + 1)$
43		negex	$⊢ - F (n + 1) \in V$
44	42 38 43	fvmpt	$⊢ n + 1 \in (M \dots N) \to (k \in (M \dots N) ⟼ - F (k)) (n + 1) = - F (n + 1)$
45	28 44	syl	$⊢ (φ \land n \in (M \dots N - 1)) \to (k \in (M \dots N) ⟼ - F (k)) (n + 1) = - F (n + 1)$
46	36 41 45	3brtr4d	$⊢ (φ \land n \in (M \dots N - 1)) \to (k \in (M \dots N) ⟼ - F (k)) (n) \leq (k \in (M \dots N) ⟼ - F (k)) (n + 1)$
47	1 6 46	monoord	$⊢ φ \to (k \in (M \dots N) ⟼ - F (k)) (M) \leq (k \in (M \dots N) ⟼ - F (k)) (N)$
48		eluzfz1	$⊢ N \in ℤ_{\geq M} \to M \in (M \dots N)$
49	1 48	syl	$⊢ φ \to M \in (M \dots N)$
50		fveq2	$⊢ k = M \to F (k) = F (M)$
51	50	negeqd	$⊢ k = M \to - F (k) = - F (M)$
52		negex	$⊢ - F (M) \in V$
53	51 38 52	fvmpt	$⊢ M \in (M \dots N) \to (k \in (M \dots N) ⟼ - F (k)) (M) = - F (M)$
54	49 53	syl	$⊢ φ \to (k \in (M \dots N) ⟼ - F (k)) (M) = - F (M)$
55		eluzfz2	$⊢ N \in ℤ_{\geq M} \to N \in (M \dots N)$
56	1 55	syl	$⊢ φ \to N \in (M \dots N)$
57		fveq2	$⊢ k = N \to F (k) = F (N)$
58	57	negeqd	$⊢ k = N \to - F (k) = - F (N)$
59		negex	$⊢ - F (N) \in V$
60	58 38 59	fvmpt	$⊢ N \in (M \dots N) \to (k \in (M \dots N) ⟼ - F (k)) (N) = - F (N)$
61	56 60	syl	$⊢ φ \to (k \in (M \dots N) ⟼ - F (k)) (N) = - F (N)$
62	47 54 61	3brtr3d	$⊢ φ \to - F (M) \leq - F (N)$
63	57	eleq1d	$⊢ k = N \to (F (k) \in ℝ \leftrightarrow F (N) \in ℝ)$
64	63 16 56	rspcdva	$⊢ φ \to F (N) \in ℝ$
65	50	eleq1d	$⊢ k = M \to (F (k) \in ℝ \leftrightarrow F (M) \in ℝ)$
66	65 16 49	rspcdva	$⊢ φ \to F (M) \in ℝ$
67	64 66	lenegd	$⊢ φ \to (F (N) \leq F (M) \leftrightarrow - F (M) \leq - F (N))$
68	62 67	mpbird	$⊢ φ \to F (N) \leq F (M)$

Metamath Proof Explorer

Theorem monoord2

Proof