Metamath Proof Explorer

Theorem iccpartipre

Description: If there is a partition, then all intermediate points are real numbers. (Contributed by AV, 11-Jul-2020)

Ref Expression
Hypotheses iccpartgtprec.m 
|- ( ph -> M e. NN )
iccpartgtprec.p 
|- ( ph -> P e. ( RePart ` M ) )
iccpartipre.i 
|- ( ph -> I e. ( 1 ..^ M ) )
Assertion iccpartipre 
|- ( ph -> ( P ` I ) e. RR )

Proof

Step Hyp Ref Expression
1 iccpartgtprec.m 
 |-  ( ph -> M e. NN )
2 iccpartgtprec.p 
 |-  ( ph -> P e. ( RePart ` M ) )
3 iccpartipre.i 
 |-  ( ph -> I e. ( 1 ..^ M ) )
4 nnz 
 |-  ( M e. NN -> M e. ZZ )
5 peano2zm 
 |-  ( M e. ZZ -> ( M - 1 ) e. ZZ )
6 id 
 |-  ( M e. ZZ -> M e. ZZ )
7 zre 
 |-  ( M e. ZZ -> M e. RR )
8 7 lem1d 
 |-  ( M e. ZZ -> ( M - 1 ) <_ M )
9 5 6 8 3jca 
 |-  ( M e. ZZ -> ( ( M - 1 ) e. ZZ /\ M e. ZZ /\ ( M - 1 ) <_ M ) )
10 4 9 syl 
 |-  ( M e. NN -> ( ( M - 1 ) e. ZZ /\ M e. ZZ /\ ( M - 1 ) <_ M ) )
11 eluz2 
 |-  ( M e. ( ZZ>= ` ( M - 1 ) ) <-> ( ( M - 1 ) e. ZZ /\ M e. ZZ /\ ( M - 1 ) <_ M ) )
12 10 11 sylibr 
 |-  ( M e. NN -> M e. ( ZZ>= ` ( M - 1 ) ) )
13 1 12 syl 
 |-  ( ph -> M e. ( ZZ>= ` ( M - 1 ) ) )
14 fzss2 
 |-  ( M e. ( ZZ>= ` ( M - 1 ) ) -> ( 0 ... ( M - 1 ) ) C_ ( 0 ... M ) )
15 13 14 syl 
 |-  ( ph -> ( 0 ... ( M - 1 ) ) C_ ( 0 ... M ) )
16 fzossfz 
 |-  ( 1 ..^ M ) C_ ( 1 ... M )
17 16 3 sselid 
 |-  ( ph -> I e. ( 1 ... M ) )
18 elfzoelz 
 |-  ( I e. ( 1 ..^ M ) -> I e. ZZ )
19 3 18 syl 
 |-  ( ph -> I e. ZZ )
20 1 nnzd 
 |-  ( ph -> M e. ZZ )
21 elfzm1b 
 |-  ( ( I e. ZZ /\ M e. ZZ ) -> ( I e. ( 1 ... M ) <-> ( I - 1 ) e. ( 0 ... ( M - 1 ) ) ) )
22 19 20 21 syl2anc 
 |-  ( ph -> ( I e. ( 1 ... M ) <-> ( I - 1 ) e. ( 0 ... ( M - 1 ) ) ) )
23 17 22 mpbid 
 |-  ( ph -> ( I - 1 ) e. ( 0 ... ( M - 1 ) ) )
24 15 23 sseldd 
 |-  ( ph -> ( I - 1 ) e. ( 0 ... M ) )
25 1 2 24 iccpartxr 
 |-  ( ph -> ( P ` ( I - 1 ) ) e. RR* )
26 1eluzge0 
 |-  1 e. ( ZZ>= ` 0 )
27 fzoss1 
 |-  ( 1 e. ( ZZ>= ` 0 ) -> ( 1 ..^ M ) C_ ( 0 ..^ M ) )
28 26 27 mp1i 
 |-  ( ph -> ( 1 ..^ M ) C_ ( 0 ..^ M ) )
29 fzossfz 
 |-  ( 0 ..^ M ) C_ ( 0 ... M )
30 28 29 sstrdi 
 |-  ( ph -> ( 1 ..^ M ) C_ ( 0 ... M ) )
31 30 3 sseldd 
 |-  ( ph -> I e. ( 0 ... M ) )
32 1 2 31 iccpartxr 
 |-  ( ph -> ( P ` I ) e. RR* )
33 28 3 sseldd 
 |-  ( ph -> I e. ( 0 ..^ M ) )
34 fzofzp1 
 |-  ( I e. ( 0 ..^ M ) -> ( I + 1 ) e. ( 0 ... M ) )
35 33 34 syl 
 |-  ( ph -> ( I + 1 ) e. ( 0 ... M ) )
36 1 2 35 iccpartxr 
 |-  ( ph -> ( P ` ( I + 1 ) ) e. RR* )
37 1 2 17 iccpartgtprec 
 |-  ( ph -> ( P ` ( I - 1 ) ) < ( P ` I ) )
38 iccpartimp 
 |-  ( ( M e. NN /\ P e. ( RePart ` M ) /\ I e. ( 0 ..^ M ) ) -> ( P e. ( RR* ^m ( 0 ... M ) ) /\ ( P ` I ) < ( P ` ( I + 1 ) ) ) )
39 1 2 33 38 syl3anc 
 |-  ( ph -> ( P e. ( RR* ^m ( 0 ... M ) ) /\ ( P ` I ) < ( P ` ( I + 1 ) ) ) )
40 39 simprd 
 |-  ( ph -> ( P ` I ) < ( P ` ( I + 1 ) ) )
41 xrre2 
 |-  ( ( ( ( P ` ( I - 1 ) ) e. RR* /\ ( P ` I ) e. RR* /\ ( P ` ( I + 1 ) ) e. RR* ) /\ ( ( P ` ( I - 1 ) ) < ( P ` I ) /\ ( P ` I ) < ( P ` ( I + 1 ) ) ) ) -> ( P ` I ) e. RR )
42 25 32 36 37 40 41 syl32anc 
 |-  ( ph -> ( P ` I ) e. RR )