| Step | Hyp | Ref
| Expression |
| 1 | | fveq2 6906 |
. . . . . 6
⊢ ((𝐼 + 1) = 𝐽 → (𝑃‘(𝐼 + 1)) = (𝑃‘𝐽)) |
| 2 | 1 | olcd 875 |
. . . . 5
⊢ ((𝐼 + 1) = 𝐽 → ((𝑃‘(𝐼 + 1)) < (𝑃‘𝐽) ∨ (𝑃‘(𝐼 + 1)) = (𝑃‘𝐽))) |
| 3 | 2 | a1d 25 |
. . . 4
⊢ ((𝐼 + 1) = 𝐽 → (((𝜑 ∧ (𝐼 ∈ (0..^𝑀) ∧ 𝐽 ∈ (0..^𝑀))) ∧ 𝐼 < 𝐽) → ((𝑃‘(𝐼 + 1)) < (𝑃‘𝐽) ∨ (𝑃‘(𝐼 + 1)) = (𝑃‘𝐽)))) |
| 4 | | elfzoelz 13699 |
. . . . . . . . . . 11
⊢ (𝐼 ∈ (0..^𝑀) → 𝐼 ∈ ℤ) |
| 5 | | elfzoelz 13699 |
. . . . . . . . . . 11
⊢ (𝐽 ∈ (0..^𝑀) → 𝐽 ∈ ℤ) |
| 6 | | zltp1le 12667 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐼 ∈ ℤ ∧ 𝐽 ∈ ℤ) → (𝐼 < 𝐽 ↔ (𝐼 + 1) ≤ 𝐽)) |
| 7 | 6 | biimpcd 249 |
. . . . . . . . . . . . . . . 16
⊢ (𝐼 < 𝐽 → ((𝐼 ∈ ℤ ∧ 𝐽 ∈ ℤ) → (𝐼 + 1) ≤ 𝐽)) |
| 8 | 7 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝐼 < 𝐽 ∧ ¬ (𝐼 + 1) = 𝐽) → ((𝐼 ∈ ℤ ∧ 𝐽 ∈ ℤ) → (𝐼 + 1) ≤ 𝐽)) |
| 9 | 8 | impcom 407 |
. . . . . . . . . . . . . 14
⊢ (((𝐼 ∈ ℤ ∧ 𝐽 ∈ ℤ) ∧ (𝐼 < 𝐽 ∧ ¬ (𝐼 + 1) = 𝐽)) → (𝐼 + 1) ≤ 𝐽) |
| 10 | | df-ne 2941 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐼 + 1) ≠ 𝐽 ↔ ¬ (𝐼 + 1) = 𝐽) |
| 11 | | necom 2994 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐼 + 1) ≠ 𝐽 ↔ 𝐽 ≠ (𝐼 + 1)) |
| 12 | 10, 11 | sylbb1 237 |
. . . . . . . . . . . . . . . 16
⊢ (¬
(𝐼 + 1) = 𝐽 → 𝐽 ≠ (𝐼 + 1)) |
| 13 | 12 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝐼 < 𝐽 ∧ ¬ (𝐼 + 1) = 𝐽) → 𝐽 ≠ (𝐼 + 1)) |
| 14 | 13 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ (((𝐼 ∈ ℤ ∧ 𝐽 ∈ ℤ) ∧ (𝐼 < 𝐽 ∧ ¬ (𝐼 + 1) = 𝐽)) → 𝐽 ≠ (𝐼 + 1)) |
| 15 | 9, 14 | jca 511 |
. . . . . . . . . . . . 13
⊢ (((𝐼 ∈ ℤ ∧ 𝐽 ∈ ℤ) ∧ (𝐼 < 𝐽 ∧ ¬ (𝐼 + 1) = 𝐽)) → ((𝐼 + 1) ≤ 𝐽 ∧ 𝐽 ≠ (𝐼 + 1))) |
| 16 | | peano2z 12658 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐼 ∈ ℤ → (𝐼 + 1) ∈
ℤ) |
| 17 | 16 | zred 12722 |
. . . . . . . . . . . . . . . 16
⊢ (𝐼 ∈ ℤ → (𝐼 + 1) ∈
ℝ) |
| 18 | | zre 12617 |
. . . . . . . . . . . . . . . 16
⊢ (𝐽 ∈ ℤ → 𝐽 ∈
ℝ) |
| 19 | 17, 18 | anim12i 613 |
. . . . . . . . . . . . . . 15
⊢ ((𝐼 ∈ ℤ ∧ 𝐽 ∈ ℤ) → ((𝐼 + 1) ∈ ℝ ∧ 𝐽 ∈
ℝ)) |
| 20 | 19 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝐼 ∈ ℤ ∧ 𝐽 ∈ ℤ) ∧ (𝐼 < 𝐽 ∧ ¬ (𝐼 + 1) = 𝐽)) → ((𝐼 + 1) ∈ ℝ ∧ 𝐽 ∈ ℝ)) |
| 21 | | ltlen 11362 |
. . . . . . . . . . . . . 14
⊢ (((𝐼 + 1) ∈ ℝ ∧ 𝐽 ∈ ℝ) → ((𝐼 + 1) < 𝐽 ↔ ((𝐼 + 1) ≤ 𝐽 ∧ 𝐽 ≠ (𝐼 + 1)))) |
| 22 | 20, 21 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝐼 ∈ ℤ ∧ 𝐽 ∈ ℤ) ∧ (𝐼 < 𝐽 ∧ ¬ (𝐼 + 1) = 𝐽)) → ((𝐼 + 1) < 𝐽 ↔ ((𝐼 + 1) ≤ 𝐽 ∧ 𝐽 ≠ (𝐼 + 1)))) |
| 23 | 15, 22 | mpbird 257 |
. . . . . . . . . . . 12
⊢ (((𝐼 ∈ ℤ ∧ 𝐽 ∈ ℤ) ∧ (𝐼 < 𝐽 ∧ ¬ (𝐼 + 1) = 𝐽)) → (𝐼 + 1) < 𝐽) |
| 24 | 23 | ex 412 |
. . . . . . . . . . 11
⊢ ((𝐼 ∈ ℤ ∧ 𝐽 ∈ ℤ) → ((𝐼 < 𝐽 ∧ ¬ (𝐼 + 1) = 𝐽) → (𝐼 + 1) < 𝐽)) |
| 25 | 4, 5, 24 | syl2an 596 |
. . . . . . . . . 10
⊢ ((𝐼 ∈ (0..^𝑀) ∧ 𝐽 ∈ (0..^𝑀)) → ((𝐼 < 𝐽 ∧ ¬ (𝐼 + 1) = 𝐽) → (𝐼 + 1) < 𝐽)) |
| 26 | 25 | adantl 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝐼 ∈ (0..^𝑀) ∧ 𝐽 ∈ (0..^𝑀))) → ((𝐼 < 𝐽 ∧ ¬ (𝐼 + 1) = 𝐽) → (𝐼 + 1) < 𝐽)) |
| 27 | | iccpartiun.m |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈ ℕ) |
| 28 | | iccpartiun.p |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑃 ∈ (RePart‘𝑀)) |
| 29 | 27, 28 | iccpartgt 47414 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑖 ∈ (0...𝑀)∀𝑗 ∈ (0...𝑀)(𝑖 < 𝑗 → (𝑃‘𝑖) < (𝑃‘𝑗))) |
| 30 | | fzofzp1 13803 |
. . . . . . . . . . 11
⊢ (𝐼 ∈ (0..^𝑀) → (𝐼 + 1) ∈ (0...𝑀)) |
| 31 | | elfzofz 13715 |
. . . . . . . . . . 11
⊢ (𝐽 ∈ (0..^𝑀) → 𝐽 ∈ (0...𝑀)) |
| 32 | | breq1 5146 |
. . . . . . . . . . . . 13
⊢ (𝑖 = (𝐼 + 1) → (𝑖 < 𝑗 ↔ (𝐼 + 1) < 𝑗)) |
| 33 | | fveq2 6906 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = (𝐼 + 1) → (𝑃‘𝑖) = (𝑃‘(𝐼 + 1))) |
| 34 | 33 | breq1d 5153 |
. . . . . . . . . . . . 13
⊢ (𝑖 = (𝐼 + 1) → ((𝑃‘𝑖) < (𝑃‘𝑗) ↔ (𝑃‘(𝐼 + 1)) < (𝑃‘𝑗))) |
| 35 | 32, 34 | imbi12d 344 |
. . . . . . . . . . . 12
⊢ (𝑖 = (𝐼 + 1) → ((𝑖 < 𝑗 → (𝑃‘𝑖) < (𝑃‘𝑗)) ↔ ((𝐼 + 1) < 𝑗 → (𝑃‘(𝐼 + 1)) < (𝑃‘𝑗)))) |
| 36 | | breq2 5147 |
. . . . . . . . . . . . 13
⊢ (𝑗 = 𝐽 → ((𝐼 + 1) < 𝑗 ↔ (𝐼 + 1) < 𝐽)) |
| 37 | | fveq2 6906 |
. . . . . . . . . . . . . 14
⊢ (𝑗 = 𝐽 → (𝑃‘𝑗) = (𝑃‘𝐽)) |
| 38 | 37 | breq2d 5155 |
. . . . . . . . . . . . 13
⊢ (𝑗 = 𝐽 → ((𝑃‘(𝐼 + 1)) < (𝑃‘𝑗) ↔ (𝑃‘(𝐼 + 1)) < (𝑃‘𝐽))) |
| 39 | 36, 38 | imbi12d 344 |
. . . . . . . . . . . 12
⊢ (𝑗 = 𝐽 → (((𝐼 + 1) < 𝑗 → (𝑃‘(𝐼 + 1)) < (𝑃‘𝑗)) ↔ ((𝐼 + 1) < 𝐽 → (𝑃‘(𝐼 + 1)) < (𝑃‘𝐽)))) |
| 40 | 35, 39 | rspc2v 3633 |
. . . . . . . . . . 11
⊢ (((𝐼 + 1) ∈ (0...𝑀) ∧ 𝐽 ∈ (0...𝑀)) → (∀𝑖 ∈ (0...𝑀)∀𝑗 ∈ (0...𝑀)(𝑖 < 𝑗 → (𝑃‘𝑖) < (𝑃‘𝑗)) → ((𝐼 + 1) < 𝐽 → (𝑃‘(𝐼 + 1)) < (𝑃‘𝐽)))) |
| 41 | 30, 31, 40 | syl2an 596 |
. . . . . . . . . 10
⊢ ((𝐼 ∈ (0..^𝑀) ∧ 𝐽 ∈ (0..^𝑀)) → (∀𝑖 ∈ (0...𝑀)∀𝑗 ∈ (0...𝑀)(𝑖 < 𝑗 → (𝑃‘𝑖) < (𝑃‘𝑗)) → ((𝐼 + 1) < 𝐽 → (𝑃‘(𝐼 + 1)) < (𝑃‘𝐽)))) |
| 42 | 29, 41 | mpan9 506 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝐼 ∈ (0..^𝑀) ∧ 𝐽 ∈ (0..^𝑀))) → ((𝐼 + 1) < 𝐽 → (𝑃‘(𝐼 + 1)) < (𝑃‘𝐽))) |
| 43 | 26, 42 | syld 47 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝐼 ∈ (0..^𝑀) ∧ 𝐽 ∈ (0..^𝑀))) → ((𝐼 < 𝐽 ∧ ¬ (𝐼 + 1) = 𝐽) → (𝑃‘(𝐼 + 1)) < (𝑃‘𝐽))) |
| 44 | 43 | expdimp 452 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝐼 ∈ (0..^𝑀) ∧ 𝐽 ∈ (0..^𝑀))) ∧ 𝐼 < 𝐽) → (¬ (𝐼 + 1) = 𝐽 → (𝑃‘(𝐼 + 1)) < (𝑃‘𝐽))) |
| 45 | 44 | impcom 407 |
. . . . . 6
⊢ ((¬
(𝐼 + 1) = 𝐽 ∧ ((𝜑 ∧ (𝐼 ∈ (0..^𝑀) ∧ 𝐽 ∈ (0..^𝑀))) ∧ 𝐼 < 𝐽)) → (𝑃‘(𝐼 + 1)) < (𝑃‘𝐽)) |
| 46 | 45 | orcd 874 |
. . . . 5
⊢ ((¬
(𝐼 + 1) = 𝐽 ∧ ((𝜑 ∧ (𝐼 ∈ (0..^𝑀) ∧ 𝐽 ∈ (0..^𝑀))) ∧ 𝐼 < 𝐽)) → ((𝑃‘(𝐼 + 1)) < (𝑃‘𝐽) ∨ (𝑃‘(𝐼 + 1)) = (𝑃‘𝐽))) |
| 47 | 46 | ex 412 |
. . . 4
⊢ (¬
(𝐼 + 1) = 𝐽 → (((𝜑 ∧ (𝐼 ∈ (0..^𝑀) ∧ 𝐽 ∈ (0..^𝑀))) ∧ 𝐼 < 𝐽) → ((𝑃‘(𝐼 + 1)) < (𝑃‘𝐽) ∨ (𝑃‘(𝐼 + 1)) = (𝑃‘𝐽)))) |
| 48 | 3, 47 | pm2.61i 182 |
. . 3
⊢ (((𝜑 ∧ (𝐼 ∈ (0..^𝑀) ∧ 𝐽 ∈ (0..^𝑀))) ∧ 𝐼 < 𝐽) → ((𝑃‘(𝐼 + 1)) < (𝑃‘𝐽) ∨ (𝑃‘(𝐼 + 1)) = (𝑃‘𝐽))) |
| 49 | 27 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐼 ∈ (0..^𝑀) ∧ 𝐽 ∈ (0..^𝑀))) → 𝑀 ∈ ℕ) |
| 50 | 28 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐼 ∈ (0..^𝑀) ∧ 𝐽 ∈ (0..^𝑀))) → 𝑃 ∈ (RePart‘𝑀)) |
| 51 | 30 | adantr 480 |
. . . . . . . 8
⊢ ((𝐼 ∈ (0..^𝑀) ∧ 𝐽 ∈ (0..^𝑀)) → (𝐼 + 1) ∈ (0...𝑀)) |
| 52 | 51 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐼 ∈ (0..^𝑀) ∧ 𝐽 ∈ (0..^𝑀))) → (𝐼 + 1) ∈ (0...𝑀)) |
| 53 | 49, 50, 52 | iccpartxr 47406 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐼 ∈ (0..^𝑀) ∧ 𝐽 ∈ (0..^𝑀))) → (𝑃‘(𝐼 + 1)) ∈
ℝ*) |
| 54 | 31 | adantl 481 |
. . . . . . . 8
⊢ ((𝐼 ∈ (0..^𝑀) ∧ 𝐽 ∈ (0..^𝑀)) → 𝐽 ∈ (0...𝑀)) |
| 55 | 54 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐼 ∈ (0..^𝑀) ∧ 𝐽 ∈ (0..^𝑀))) → 𝐽 ∈ (0...𝑀)) |
| 56 | 49, 50, 55 | iccpartxr 47406 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐼 ∈ (0..^𝑀) ∧ 𝐽 ∈ (0..^𝑀))) → (𝑃‘𝐽) ∈
ℝ*) |
| 57 | 53, 56 | jca 511 |
. . . . 5
⊢ ((𝜑 ∧ (𝐼 ∈ (0..^𝑀) ∧ 𝐽 ∈ (0..^𝑀))) → ((𝑃‘(𝐼 + 1)) ∈ ℝ* ∧
(𝑃‘𝐽) ∈
ℝ*)) |
| 58 | 57 | adantr 480 |
. . . 4
⊢ (((𝜑 ∧ (𝐼 ∈ (0..^𝑀) ∧ 𝐽 ∈ (0..^𝑀))) ∧ 𝐼 < 𝐽) → ((𝑃‘(𝐼 + 1)) ∈ ℝ* ∧
(𝑃‘𝐽) ∈
ℝ*)) |
| 59 | | xrleloe 13186 |
. . . 4
⊢ (((𝑃‘(𝐼 + 1)) ∈ ℝ* ∧
(𝑃‘𝐽) ∈ ℝ*) → ((𝑃‘(𝐼 + 1)) ≤ (𝑃‘𝐽) ↔ ((𝑃‘(𝐼 + 1)) < (𝑃‘𝐽) ∨ (𝑃‘(𝐼 + 1)) = (𝑃‘𝐽)))) |
| 60 | 58, 59 | syl 17 |
. . 3
⊢ (((𝜑 ∧ (𝐼 ∈ (0..^𝑀) ∧ 𝐽 ∈ (0..^𝑀))) ∧ 𝐼 < 𝐽) → ((𝑃‘(𝐼 + 1)) ≤ (𝑃‘𝐽) ↔ ((𝑃‘(𝐼 + 1)) < (𝑃‘𝐽) ∨ (𝑃‘(𝐼 + 1)) = (𝑃‘𝐽)))) |
| 61 | 48, 60 | mpbird 257 |
. 2
⊢ (((𝜑 ∧ (𝐼 ∈ (0..^𝑀) ∧ 𝐽 ∈ (0..^𝑀))) ∧ 𝐼 < 𝐽) → (𝑃‘(𝐼 + 1)) ≤ (𝑃‘𝐽)) |
| 62 | 61 | exp31 419 |
1
⊢ (𝜑 → ((𝐼 ∈ (0..^𝑀) ∧ 𝐽 ∈ (0..^𝑀)) → (𝐼 < 𝐽 → (𝑃‘(𝐼 + 1)) ≤ (𝑃‘𝐽)))) |