Theorem monoord2xr

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

	Ref	Expression
Hypotheses	monoord2xr.p	⊢ Ⅎ 𝑘 𝜑
	monoord2xr.k	⊢ Ⅎ 𝑘 𝐹
	monoord2xr.n	⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
	monoord2xr.x	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ* )
	monoord2xr.l	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ) → ( 𝐹 ‘ ( 𝑘 + 1 ) ) ≤ ( 𝐹 ‘ 𝑘 ) )
Assertion	monoord2xr	⊢ ( 𝜑 → ( 𝐹 ‘ 𝑁 ) ≤ ( 𝐹 ‘ 𝑀 ) )

Proof

Step	Hyp	Ref	Expression
1		monoord2xr.p	⊢ Ⅎ 𝑘 𝜑
2		monoord2xr.k	⊢ Ⅎ 𝑘 𝐹
3		monoord2xr.n	⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
4		monoord2xr.x	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ* )
5		monoord2xr.l	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ) → ( 𝐹 ‘ ( 𝑘 + 1 ) ) ≤ ( 𝐹 ‘ 𝑘 ) )
6		nfv	⊢ Ⅎ 𝑘 𝑗 ∈ ( 𝑀 ... 𝑁 )
7	1 6	nfan	⊢ Ⅎ 𝑘 ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ... 𝑁 ) )
8		nfcv	⊢ Ⅎ 𝑘 𝑗
9	2 8	nffv	⊢ Ⅎ 𝑘 ( 𝐹 ‘ 𝑗 )
10		nfcv	⊢ Ⅎ 𝑘 ℝ*
11	9 10	nfel	⊢ Ⅎ 𝑘 ( 𝐹 ‘ 𝑗 ) ∈ ℝ*
12	7 11	nfim	⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑗 ) ∈ ℝ* )
13		eleq1w	⊢ ( 𝑘 = 𝑗 → ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ↔ 𝑗 ∈ ( 𝑀 ... 𝑁 ) ) )
14	13	anbi2d	⊢ ( 𝑘 = 𝑗 → ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) ↔ ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ... 𝑁 ) ) ) )
15		fveq2	⊢ ( 𝑘 = 𝑗 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑗 ) )
16	15	eleq1d	⊢ ( 𝑘 = 𝑗 → ( ( 𝐹 ‘ 𝑘 ) ∈ ℝ* ↔ ( 𝐹 ‘ 𝑗 ) ∈ ℝ* ) )
17	14 16	imbi12d	⊢ ( 𝑘 = 𝑗 → ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ* ) ↔ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑗 ) ∈ ℝ* ) ) )
18	12 17 4	chvarfv	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑗 ) ∈ ℝ* )
19		nfv	⊢ Ⅎ 𝑘 𝑗 ∈ ( 𝑀 ... ( 𝑁 − 1 ) )
20	1 19	nfan	⊢ Ⅎ 𝑘 ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) )
21		nfcv	⊢ Ⅎ 𝑘 ( 𝑗 + 1 )
22	2 21	nffv	⊢ Ⅎ 𝑘 ( 𝐹 ‘ ( 𝑗 + 1 ) )
23		nfcv	⊢ Ⅎ 𝑘 ≤
24	22 23 9	nfbr	⊢ Ⅎ 𝑘 ( 𝐹 ‘ ( 𝑗 + 1 ) ) ≤ ( 𝐹 ‘ 𝑗 )
25	20 24	nfim	⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ) → ( 𝐹 ‘ ( 𝑗 + 1 ) ) ≤ ( 𝐹 ‘ 𝑗 ) )
26		eleq1w	⊢ ( 𝑘 = 𝑗 → ( 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ↔ 𝑗 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ) )
27	26	anbi2d	⊢ ( 𝑘 = 𝑗 → ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ) ↔ ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ) ) )
28		fvoveq1	⊢ ( 𝑘 = 𝑗 → ( 𝐹 ‘ ( 𝑘 + 1 ) ) = ( 𝐹 ‘ ( 𝑗 + 1 ) ) )
29	28 15	breq12d	⊢ ( 𝑘 = 𝑗 → ( ( 𝐹 ‘ ( 𝑘 + 1 ) ) ≤ ( 𝐹 ‘ 𝑘 ) ↔ ( 𝐹 ‘ ( 𝑗 + 1 ) ) ≤ ( 𝐹 ‘ 𝑗 ) ) )
30	27 29	imbi12d	⊢ ( 𝑘 = 𝑗 → ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ) → ( 𝐹 ‘ ( 𝑘 + 1 ) ) ≤ ( 𝐹 ‘ 𝑘 ) ) ↔ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ) → ( 𝐹 ‘ ( 𝑗 + 1 ) ) ≤ ( 𝐹 ‘ 𝑗 ) ) ) )
31	25 30 5	chvarfv	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ) → ( 𝐹 ‘ ( 𝑗 + 1 ) ) ≤ ( 𝐹 ‘ 𝑗 ) )
32	3 18 31	monoord2xrv	⊢ ( 𝜑 → ( 𝐹 ‘ 𝑁 ) ≤ ( 𝐹 ‘ 𝑀 ) )