# 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 ${⊢}{\phi }\to {M}\in ℕ$
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 ℕ$
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 ℕ\to \left({P}\in \mathrm{RePart}\left({M}\right)↔\left({P}\in \left({{ℝ}^{*}}^{\left(0\dots {M}\right)}\right)\wedge \forall {i}\in \left(0..^{M}\right)\phantom{\rule{.4em}{0ex}}{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)↔\left({P}\in \left({{ℝ}^{*}}^{\left(0\dots {M}\right)}\right)\wedge \forall {i}\in \left(0..^{M}\right)\phantom{\rule{.4em}{0ex}}{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)\phantom{\rule{.4em}{0ex}}{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 ffvelrnd ${⊢}{\phi }\to {P}\left({I}\right)\in {ℝ}^{*}$