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	ffvelrnd	|- ( ph -> ( P ` I ) e. RR* )