monoord2xrv

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

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

Proof

Step	Hyp	Ref	Expression
1		monoord2xrv.n	$⊢ φ \to N \in ℤ_{\geq M}$
2		monoord2xrv.x	$⊢ (φ \land k \in (M \dots N)) \to F (k) \in ℝ^{*}$
3		monoord2xrv.l	$⊢ (φ \land k \in (M \dots N - 1)) \to F (k + 1) \leq F (k)$
4	2	xnegcld	$⊢ (φ \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		fzp1elp1	$⊢ n \in (M \dots N - 1) \to n + 1 \in (M \dots N - 1 + 1)$
15	14	adantl	$⊢ (φ \land n \in (M \dots N - 1)) \to n + 1 \in (M \dots N - 1 + 1)$
16		eluzelz	$⊢ N \in ℤ_{\geq M} \to N \in ℤ$
17	1 16	syl	$⊢ φ \to N \in ℤ$
18	17	zcnd	$⊢ φ \to N \in ℂ$
19		ax-1cn	$⊢ 1 \in ℂ$
20		npcan	$⊢ (N \in ℂ \land 1 \in ℂ) \to N - 1 + 1 = N$
21	18 19 20	sylancl	$⊢ φ \to N - 1 + 1 = N$
22	21	oveq2d	$⊢ φ \to (M \dots N - 1 + 1) = (M \dots N)$
23	22	adantr	$⊢ (φ \land n \in (M \dots N - 1)) \to (M \dots N - 1 + 1) = (M \dots N)$
24	15 23	eleqtrd	$⊢ (φ \land n \in (M \dots N - 1)) \to n + 1 \in (M \dots N)$
25	2	ralrimiva	$⊢ φ \to \forall k \in (M \dots N) F (k) \in ℝ^{*}$
26	25	adantr	$⊢ (φ \land n \in (M \dots N - 1)) \to \forall k \in (M \dots N) F (k) \in ℝ^{*}$
27		fveq2	$⊢ k = n + 1 \to F (k) = F (n + 1)$
28	27	eleq1d	$⊢ k = n + 1 \to (F (k) \in ℝ^{} \leftrightarrow F (n + 1) \in ℝ^{})$
29	28	rspcv	$⊢ n + 1 \in (M \dots N) \to (\forall k \in (M \dots N) F (k) \in ℝ^{} \to F (n + 1) \in ℝ^{})$
30	24 26 29	sylc	$⊢ (φ \land n \in (M \dots N - 1)) \to F (n + 1) \in ℝ^{*}$
31		fzssp1	$⊢ (M \dots N - 1) \subseteq (M \dots N - 1 + 1)$
32	31 22	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	9	eleq1d	$⊢ k = n \to (F (k) \in ℝ^{} \leftrightarrow F (n) \in ℝ^{})$
35	34	rspcv	$⊢ n \in (M \dots N) \to (\forall k \in (M \dots N) F (k) \in ℝ^{} \to F (n) \in ℝ^{})$
36	33 26 35	sylc	$⊢ (φ \land n \in (M \dots N - 1)) \to F (n) \in ℝ^{*}$
37		xleneg	$⊢ (F (n + 1) \in ℝ^{} \land F (n) \in ℝ^{}) \to (F (n + 1) \leq F (n) \leftrightarrow - F (n) \leq - F (n + 1))$
38	30 36 37	syl2anc	$⊢ (φ \land n \in (M \dots N - 1)) \to (F (n + 1) \leq F (n) \leftrightarrow - F (n) \leq - F (n + 1))$
39	13 38	mpbid	$⊢ (φ \land n \in (M \dots N - 1)) \to - F (n) \leq - F (n + 1)$
40	9	xnegeqd	$⊢ k = n \to - F (k) = - F (n)$
41		eqid	$⊢ (k \in (M \dots N) ⟼ - F (k)) = (k \in (M \dots N) ⟼ - F (k))$
42		xnegex	$⊢ - F (n) \in V$
43	40 41 42	fvmpt	$⊢ n \in (M \dots N) \to (k \in (M \dots N) ⟼ - F (k)) (n) = - F (n)$
44	33 43	syl	$⊢ (φ \land n \in (M \dots N - 1)) \to (k \in (M \dots N) ⟼ - F (k)) (n) = - F (n)$
45	27	xnegeqd	$⊢ k = n + 1 \to - F (k) = - F (n + 1)$
46		xnegex	$⊢ - F (n + 1) \in V$
47	45 41 46	fvmpt	$⊢ n + 1 \in (M \dots N) \to (k \in (M \dots N) ⟼ - F (k)) (n + 1) = - F (n + 1)$
48	24 47	syl	$⊢ (φ \land n \in (M \dots N - 1)) \to (k \in (M \dots N) ⟼ - F (k)) (n + 1) = - F (n + 1)$
49	39 44 48	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)$
50	1 6 49	monoordxrv	$⊢ φ \to (k \in (M \dots N) ⟼ - F (k)) (M) \leq (k \in (M \dots N) ⟼ - F (k)) (N)$
51		eluzfz1	$⊢ N \in ℤ_{\geq M} \to M \in (M \dots N)$
52	1 51	syl	$⊢ φ \to M \in (M \dots N)$
53		fveq2	$⊢ k = M \to F (k) = F (M)$
54	53	xnegeqd	$⊢ k = M \to - F (k) = - F (M)$
55		xnegex	$⊢ - F (M) \in V$
56	54 41 55	fvmpt	$⊢ M \in (M \dots N) \to (k \in (M \dots N) ⟼ - F (k)) (M) = - F (M)$
57	52 56	syl	$⊢ φ \to (k \in (M \dots N) ⟼ - F (k)) (M) = - F (M)$
58		eluzfz2	$⊢ N \in ℤ_{\geq M} \to N \in (M \dots N)$
59	1 58	syl	$⊢ φ \to N \in (M \dots N)$
60		fveq2	$⊢ k = N \to F (k) = F (N)$
61	60	xnegeqd	$⊢ k = N \to - F (k) = - F (N)$
62		xnegex	$⊢ - F (N) \in V$
63	61 41 62	fvmpt	$⊢ N \in (M \dots N) \to (k \in (M \dots N) ⟼ - F (k)) (N) = - F (N)$
64	59 63	syl	$⊢ φ \to (k \in (M \dots N) ⟼ - F (k)) (N) = - F (N)$
65	50 57 64	3brtr3d	$⊢ φ \to - F (M) \leq - F (N)$
66	60	eleq1d	$⊢ k = N \to (F (k) \in ℝ^{} \leftrightarrow F (N) \in ℝ^{})$
67	66	rspcv	$⊢ N \in (M \dots N) \to (\forall k \in (M \dots N) F (k) \in ℝ^{} \to F (N) \in ℝ^{})$
68	59 25 67	sylc	$⊢ φ \to F (N) \in ℝ^{*}$
69	53	eleq1d	$⊢ k = M \to (F (k) \in ℝ^{} \leftrightarrow F (M) \in ℝ^{})$
70	69	rspcv	$⊢ M \in (M \dots N) \to (\forall k \in (M \dots N) F (k) \in ℝ^{} \to F (M) \in ℝ^{})$
71	52 25 70	sylc	$⊢ φ \to F (M) \in ℝ^{*}$
72		xleneg	$⊢ (F (N) \in ℝ^{} \land F (M) \in ℝ^{}) \to (F (N) \leq F (M) \leftrightarrow - F (M) \leq - F (N))$
73	68 71 72	syl2anc	$⊢ φ \to (F (N) \leq F (M) \leftrightarrow - F (M) \leq - F (N))$
74	65 73	mpbird	$⊢ φ \to F (N) \leq F (M)$

Metamath Proof Explorer

Theorem monoord2xrv

Proof