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