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 
|- ( ph -> M e. NN )
iccpartgtprec.p 
|- ( ph -> P e. ( RePart ` M ) )
iccpartgtprec.i 
|- ( ph -> I e. ( 1 ... M ) )
Assertion iccpartgtprec 
|- ( ph -> ( P ` ( I - 1 ) ) < ( P ` I ) )

Proof

Step Hyp Ref Expression
1 iccpartgtprec.m 
 |-  ( ph -> M e. NN )
2 iccpartgtprec.p 
 |-  ( ph -> P e. ( RePart ` M ) )
3 iccpartgtprec.i 
 |-  ( ph -> I e. ( 1 ... M ) )
4 1 nnzd 
 |-  ( ph -> M e. ZZ )
5 fzval3 
 |-  ( M e. ZZ -> ( 1 ... M ) = ( 1 ..^ ( M + 1 ) ) )
6 5 eleq2d 
 |-  ( M e. ZZ -> ( I e. ( 1 ... M ) <-> I e. ( 1 ..^ ( M + 1 ) ) ) )
7 4 6 syl 
 |-  ( ph -> ( I e. ( 1 ... M ) <-> I e. ( 1 ..^ ( M + 1 ) ) ) )
8 3 7 mpbid 
 |-  ( ph -> I e. ( 1 ..^ ( M + 1 ) ) )
9 1 nncnd 
 |-  ( ph -> M e. CC )
10 pncan1 
 |-  ( M e. CC -> ( ( M + 1 ) - 1 ) = M )
11 9 10 syl 
 |-  ( ph -> ( ( M + 1 ) - 1 ) = M )
12 11 eqcomd 
 |-  ( ph -> M = ( ( M + 1 ) - 1 ) )
13 12 oveq2d 
 |-  ( ph -> ( 0 ..^ M ) = ( 0 ..^ ( ( M + 1 ) - 1 ) ) )
14 13 eleq2d 
 |-  ( ph -> ( ( I - 1 ) e. ( 0 ..^ M ) <-> ( I - 1 ) e. ( 0 ..^ ( ( M + 1 ) - 1 ) ) ) )
15 elfzelz 
 |-  ( I e. ( 1 ... M ) -> I e. ZZ )
16 3 15 syl 
 |-  ( ph -> I e. ZZ )
17 4 peano2zd 
 |-  ( ph -> ( M + 1 ) e. ZZ )
18 elfzom1b 
 |-  ( ( I e. ZZ /\ ( M + 1 ) e. ZZ ) -> ( I e. ( 1 ..^ ( M + 1 ) ) <-> ( I - 1 ) e. ( 0 ..^ ( ( M + 1 ) - 1 ) ) ) )
19 16 17 18 syl2anc 
 |-  ( ph -> ( I e. ( 1 ..^ ( M + 1 ) ) <-> ( I - 1 ) e. ( 0 ..^ ( ( M + 1 ) - 1 ) ) ) )
20 14 19 bitr4d 
 |-  ( ph -> ( ( I - 1 ) e. ( 0 ..^ M ) <-> I e. ( 1 ..^ ( M + 1 ) ) ) )
21 8 20 mpbird 
 |-  ( ph -> ( I - 1 ) e. ( 0 ..^ M ) )
22 iccpartimp 
 |-  ( ( M e. NN /\ P e. ( RePart ` M ) /\ ( I - 1 ) e. ( 0 ..^ M ) ) -> ( P e. ( RR* ^m ( 0 ... M ) ) /\ ( P ` ( I - 1 ) ) < ( P ` ( ( I - 1 ) + 1 ) ) ) )
23 1 2 21 22 syl3anc 
 |-  ( ph -> ( P e. ( RR* ^m ( 0 ... M ) ) /\ ( P ` ( I - 1 ) ) < ( P ` ( ( I - 1 ) + 1 ) ) ) )
24 23 simprd 
 |-  ( ph -> ( P ` ( I - 1 ) ) < ( P ` ( ( I - 1 ) + 1 ) ) )
25 16 zcnd 
 |-  ( ph -> I e. CC )
26 npcan1 
 |-  ( I e. CC -> ( ( I - 1 ) + 1 ) = I )
27 25 26 syl 
 |-  ( ph -> ( ( I - 1 ) + 1 ) = I )
28 27 eqcomd 
 |-  ( ph -> I = ( ( I - 1 ) + 1 ) )
29 28 fveq2d 
 |-  ( ph -> ( P ` I ) = ( P ` ( ( I - 1 ) + 1 ) ) )
30 24 29 breqtrrd 
 |-  ( ph -> ( P ` ( I - 1 ) ) < ( P ` I ) )