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	$$⊢\phi \to M\in \mathbb{N}$$
	iccpartgtprec.p	$$⊢\phi \to P\in \mathrm{RePart}\left(M\right)$$
	iccpartxr.i	$$⊢\phi \to I\in \left(0\dots M\right)$$
Assertion	iccpartxr	$$⊢\phi \to P\left(I\right)\in {ℝ}^{*}$$

Proof

Step	Hyp	Ref	Expression
1		iccpartgtprec.m	$$⊢\phi \to M\in \mathbb{N}$$
2		iccpartgtprec.p	$$⊢\phi \to P\in \mathrm{RePart}\left(M\right)$$
3		iccpartxr.i	$$⊢\phi \to I\in \left(0\dots M\right)$$
4		iccpart	$$⊢M\in \mathbb{N}\to \left(P\in \mathrm{RePart}\left(M\right)\leftrightarrow \left(P\in \left({{ℝ}^{*}}^{\left(0\dots M\right)}\right)\wedge \forall i\in \left(0..^M\right)P\left(i\right)<P\left(i+1\right)\right)\right)$$
5	1 4	syl	$$⊢\phi \to \left(P\in \mathrm{RePart}\left(M\right)\leftrightarrow \left(P\in \left({{ℝ}^{*}}^{\left(0\dots M\right)}\right)\wedge \forall i\in \left(0..^M\right)P\left(i\right)<P\left(i+1\right)\right)\right)$$
6	2 5	mpbid	$$⊢\phi \to \left(P\in \left({{ℝ}^{*}}^{\left(0\dots M\right)}\right)\wedge \forall i\in \left(0..^M\right)P\left(i\right)<P\left(i+1\right)\right)$$
7	6	simpld	$$⊢\phi \to P\in \left({{ℝ}^{*}}^{\left(0\dots M\right)}\right)$$
8		elmapi	$$⊢P\in \left({{ℝ}^{*}}^{\left(0\dots M\right)}\right)\to P:\left(0\dots M\right)⟶{ℝ}^{*}$$
9	7 8	syl	$$⊢\phi \to P:\left(0\dots M\right)⟶{ℝ}^{*}$$
10	9 3	ffvelcdmd	$$⊢\phi \to P\left(I\right)\in {ℝ}^{*}$$