# Metamath Proof Explorer

## Theorem iccpartgtprec

Description: If there is a partition, then all intermediate points and the upper bound are strictly greater than the preceeding intermediate points or lower bound. (Contributed by AV, 11-Jul-2020)

Ref Expression
Hypotheses iccpartgtprec.m ${⊢}{\phi }\to {M}\in ℕ$
iccpartgtprec.p ${⊢}{\phi }\to {P}\in \mathrm{RePart}\left({M}\right)$
iccpartgtprec.i ${⊢}{\phi }\to {I}\in \left(1\dots {M}\right)$
Assertion iccpartgtprec ${⊢}{\phi }\to {P}\left({I}-1\right)<{P}\left({I}\right)$

### Proof

Step Hyp Ref Expression
1 iccpartgtprec.m ${⊢}{\phi }\to {M}\in ℕ$
2 iccpartgtprec.p ${⊢}{\phi }\to {P}\in \mathrm{RePart}\left({M}\right)$
3 iccpartgtprec.i ${⊢}{\phi }\to {I}\in \left(1\dots {M}\right)$
4 1 nnzd ${⊢}{\phi }\to {M}\in ℤ$
5 fzval3 ${⊢}{M}\in ℤ\to \left(1\dots {M}\right)=\left(1..^{M}+1\right)$
6 5 eleq2d ${⊢}{M}\in ℤ\to \left({I}\in \left(1\dots {M}\right)↔{I}\in \left(1..^{M}+1\right)\right)$
7 4 6 syl ${⊢}{\phi }\to \left({I}\in \left(1\dots {M}\right)↔{I}\in \left(1..^{M}+1\right)\right)$
8 3 7 mpbid ${⊢}{\phi }\to {I}\in \left(1..^{M}+1\right)$
9 1 nncnd ${⊢}{\phi }\to {M}\in ℂ$
10 pncan1 ${⊢}{M}\in ℂ\to {M}+1-1={M}$
11 9 10 syl ${⊢}{\phi }\to {M}+1-1={M}$
12 11 eqcomd ${⊢}{\phi }\to {M}={M}+1-1$
13 12 oveq2d ${⊢}{\phi }\to \left(0..^{M}\right)=\left(0..^{M}+1-1\right)$
14 13 eleq2d ${⊢}{\phi }\to \left({I}-1\in \left(0..^{M}\right)↔{I}-1\in \left(0..^{M}+1-1\right)\right)$
15 elfzelz ${⊢}{I}\in \left(1\dots {M}\right)\to {I}\in ℤ$
16 3 15 syl ${⊢}{\phi }\to {I}\in ℤ$
17 4 peano2zd ${⊢}{\phi }\to {M}+1\in ℤ$
18 elfzom1b ${⊢}\left({I}\in ℤ\wedge {M}+1\in ℤ\right)\to \left({I}\in \left(1..^{M}+1\right)↔{I}-1\in \left(0..^{M}+1-1\right)\right)$
19 16 17 18 syl2anc ${⊢}{\phi }\to \left({I}\in \left(1..^{M}+1\right)↔{I}-1\in \left(0..^{M}+1-1\right)\right)$
20 14 19 bitr4d ${⊢}{\phi }\to \left({I}-1\in \left(0..^{M}\right)↔{I}\in \left(1..^{M}+1\right)\right)$
21 8 20 mpbird ${⊢}{\phi }\to {I}-1\in \left(0..^{M}\right)$
22 iccpartimp ${⊢}\left({M}\in ℕ\wedge {P}\in \mathrm{RePart}\left({M}\right)\wedge {I}-1\in \left(0..^{M}\right)\right)\to \left({P}\in \left({{ℝ}^{*}}^{\left(0\dots {M}\right)}\right)\wedge {P}\left({I}-1\right)<{P}\left({I}-1+1\right)\right)$
23 1 2 21 22 syl3anc ${⊢}{\phi }\to \left({P}\in \left({{ℝ}^{*}}^{\left(0\dots {M}\right)}\right)\wedge {P}\left({I}-1\right)<{P}\left({I}-1+1\right)\right)$
24 23 simprd ${⊢}{\phi }\to {P}\left({I}-1\right)<{P}\left({I}-1+1\right)$
25 16 zcnd ${⊢}{\phi }\to {I}\in ℂ$
26 npcan1 ${⊢}{I}\in ℂ\to {I}-1+1={I}$
27 25 26 syl ${⊢}{\phi }\to {I}-1+1={I}$
28 27 eqcomd ${⊢}{\phi }\to {I}={I}-1+1$
29 28 fveq2d ${⊢}{\phi }\to {P}\left({I}\right)={P}\left({I}-1+1\right)$
30 24 29 breqtrrd ${⊢}{\phi }\to {P}\left({I}-1\right)<{P}\left({I}\right)$