This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem iccpartxr

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

Ref Expression
Hypotheses iccpartgtprec.m 
|- ( ph -> M e. NN )
iccpartgtprec.p 
|- ( ph -> P e. ( RePart ` M ) )
iccpartxr.i 
|- ( ph -> I e. ( 0 ... M ) )
Assertion iccpartxr 
|- ( 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 iccpartxr.i 
 |-  ( ph -> I e. ( 0 ... M ) )
4 iccpart 
 |-  ( M e. NN -> ( P e. ( RePart ` M ) <-> ( P e. ( RR* ^m ( 0 ... M ) ) /\ A. i e. ( 0 ..^ M ) ( P ` i ) < ( P ` ( i + 1 ) ) ) ) )
5 1 4 syl 
 |-  ( ph -> ( P e. ( RePart ` M ) <-> ( P e. ( RR* ^m ( 0 ... M ) ) /\ A. i e. ( 0 ..^ M ) ( P ` i ) < ( P ` ( i + 1 ) ) ) ) )
6 2 5 mpbid 
 |-  ( ph -> ( P e. ( RR* ^m ( 0 ... M ) ) /\ A. i e. ( 0 ..^ M ) ( P ` i ) < ( P ` ( i + 1 ) ) ) )
7 6 simpld 
 |-  ( ph -> P e. ( RR* ^m ( 0 ... M ) ) )
8 elmapi 
 |-  ( P e. ( RR* ^m ( 0 ... M ) ) -> P : ( 0 ... M ) --> RR* )
9 7 8 syl 
 |-  ( ph -> P : ( 0 ... M ) --> RR* )
10 9 3 ffvelcdmd 
 |-  ( ph -> ( P ` I ) e. RR* )