Metamath Proof Explorer


Theorem monoordxr

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

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

Proof

Step Hyp Ref Expression
1 monoordxr.p 𝑘 𝜑
2 monoordxr.k 𝑘 𝐹
3 monoordxr.n ( 𝜑𝑁 ∈ ( ℤ𝑀 ) )
4 monoordxr.x ( ( 𝜑𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹𝑘 ) ∈ ℝ* )
5 monoordxr.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 𝑘
22 nfcv 𝑘 ( 𝑗 + 1 )
23 2 22 nffv 𝑘 ( 𝐹 ‘ ( 𝑗 + 1 ) )
24 9 21 23 nfbr 𝑘 ( 𝐹𝑗 ) ≤ ( 𝐹 ‘ ( 𝑗 + 1 ) )
25 20 24 nfim 𝑘 ( ( 𝜑𝑗 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ) → ( 𝐹𝑗 ) ≤ ( 𝐹 ‘ ( 𝑗 + 1 ) ) )
26 eleq1w ( 𝑘 = 𝑗 → ( 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ↔ 𝑗 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ) )
27 26 anbi2d ( 𝑘 = 𝑗 → ( ( 𝜑𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ) ↔ ( 𝜑𝑗 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ) ) )
28 fvoveq1 ( 𝑘 = 𝑗 → ( 𝐹 ‘ ( 𝑘 + 1 ) ) = ( 𝐹 ‘ ( 𝑗 + 1 ) ) )
29 15 28 breq12d ( 𝑘 = 𝑗 → ( ( 𝐹𝑘 ) ≤ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ↔ ( 𝐹𝑗 ) ≤ ( 𝐹 ‘ ( 𝑗 + 1 ) ) ) )
30 27 29 imbi12d ( 𝑘 = 𝑗 → ( ( ( 𝜑𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ) → ( 𝐹𝑘 ) ≤ ( 𝐹 ‘ ( 𝑘 + 1 ) ) ) ↔ ( ( 𝜑𝑗 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ) → ( 𝐹𝑗 ) ≤ ( 𝐹 ‘ ( 𝑗 + 1 ) ) ) ) )
31 25 30 5 chvarfv ( ( 𝜑𝑗 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ) → ( 𝐹𝑗 ) ≤ ( 𝐹 ‘ ( 𝑗 + 1 ) ) )
32 3 18 31 monoordxrv ( 𝜑 → ( 𝐹𝑀 ) ≤ ( 𝐹𝑁 ) )