This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑁 ) ≤ ( 𝐹 ‘ 𝑀 ) )