Step |
Hyp |
Ref |
Expression |
1 |
|
iccpart |
⊢ ( 𝑀 ∈ ℕ → ( 𝑃 ∈ ( RePart ‘ 𝑀 ) ↔ ( 𝑃 ∈ ( ℝ* ↑m ( 0 ... 𝑀 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) ) ) |
2 |
|
fveq2 |
⊢ ( 𝑖 = 𝐼 → ( 𝑃 ‘ 𝑖 ) = ( 𝑃 ‘ 𝐼 ) ) |
3 |
|
fvoveq1 |
⊢ ( 𝑖 = 𝐼 → ( 𝑃 ‘ ( 𝑖 + 1 ) ) = ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) |
4 |
2 3
|
breq12d |
⊢ ( 𝑖 = 𝐼 → ( ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ ( 𝑖 + 1 ) ) ↔ ( 𝑃 ‘ 𝐼 ) < ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) ) |
5 |
4
|
rspccv |
⊢ ( ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ ( 𝑖 + 1 ) ) → ( 𝐼 ∈ ( 0 ..^ 𝑀 ) → ( 𝑃 ‘ 𝐼 ) < ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) ) |
6 |
5
|
adantl |
⊢ ( ( 𝑃 ∈ ( ℝ* ↑m ( 0 ... 𝑀 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) → ( 𝐼 ∈ ( 0 ..^ 𝑀 ) → ( 𝑃 ‘ 𝐼 ) < ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) ) |
7 |
|
simpl |
⊢ ( ( 𝑃 ∈ ( ℝ* ↑m ( 0 ... 𝑀 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) → 𝑃 ∈ ( ℝ* ↑m ( 0 ... 𝑀 ) ) ) |
8 |
6 7
|
jctild |
⊢ ( ( 𝑃 ∈ ( ℝ* ↑m ( 0 ... 𝑀 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) → ( 𝐼 ∈ ( 0 ..^ 𝑀 ) → ( 𝑃 ∈ ( ℝ* ↑m ( 0 ... 𝑀 ) ) ∧ ( 𝑃 ‘ 𝐼 ) < ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) ) ) |
9 |
1 8
|
syl6bi |
⊢ ( 𝑀 ∈ ℕ → ( 𝑃 ∈ ( RePart ‘ 𝑀 ) → ( 𝐼 ∈ ( 0 ..^ 𝑀 ) → ( 𝑃 ∈ ( ℝ* ↑m ( 0 ... 𝑀 ) ) ∧ ( 𝑃 ‘ 𝐼 ) < ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) ) ) ) |
10 |
9
|
3imp |
⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑃 ∈ ( RePart ‘ 𝑀 ) ∧ 𝐼 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑃 ∈ ( ℝ* ↑m ( 0 ... 𝑀 ) ) ∧ ( 𝑃 ‘ 𝐼 ) < ( 𝑃 ‘ ( 𝐼 + 1 ) ) ) ) |