# Metamath Proof Explorer

## Theorem iccpartrn

Description: If there is a partition, then all intermediate points and bounds are contained in a closed interval of extended reals. (Contributed by AV, 14-Jul-2020)

Ref Expression
Hypotheses iccpartgtprec.m ${⊢}{\phi }\to {M}\in ℕ$
iccpartgtprec.p ${⊢}{\phi }\to {P}\in \mathrm{RePart}\left({M}\right)$
Assertion iccpartrn ${⊢}{\phi }\to \mathrm{ran}{P}\subseteq \left[{P}\left(0\right),{P}\left({M}\right)\right]$

### 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 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)$
4 1 3 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)$
5 elmapfn ${⊢}{P}\in \left({{ℝ}^{*}}^{\left(0\dots {M}\right)}\right)\to {P}Fn\left(0\dots {M}\right)$
6 5 adantr ${⊢}\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)\to {P}Fn\left(0\dots {M}\right)$
7 4 6 syl6bi ${⊢}{\phi }\to \left({P}\in \mathrm{RePart}\left({M}\right)\to {P}Fn\left(0\dots {M}\right)\right)$
8 2 7 mpd ${⊢}{\phi }\to {P}Fn\left(0\dots {M}\right)$
9 fvelrnb ${⊢}{P}Fn\left(0\dots {M}\right)\to \left({p}\in \mathrm{ran}{P}↔\exists {i}\in \left(0\dots {M}\right)\phantom{\rule{.4em}{0ex}}{P}\left({i}\right)={p}\right)$
10 8 9 syl ${⊢}{\phi }\to \left({p}\in \mathrm{ran}{P}↔\exists {i}\in \left(0\dots {M}\right)\phantom{\rule{.4em}{0ex}}{P}\left({i}\right)={p}\right)$
11 1 adantr ${⊢}\left({\phi }\wedge {i}\in \left(0\dots {M}\right)\right)\to {M}\in ℕ$
12 2 adantr ${⊢}\left({\phi }\wedge {i}\in \left(0\dots {M}\right)\right)\to {P}\in \mathrm{RePart}\left({M}\right)$
13 simpr ${⊢}\left({\phi }\wedge {i}\in \left(0\dots {M}\right)\right)\to {i}\in \left(0\dots {M}\right)$
14 11 12 13 iccpartxr ${⊢}\left({\phi }\wedge {i}\in \left(0\dots {M}\right)\right)\to {P}\left({i}\right)\in {ℝ}^{*}$
15 1 2 iccpartgel ${⊢}{\phi }\to \forall {k}\in \left(0\dots {M}\right)\phantom{\rule{.4em}{0ex}}{P}\left(0\right)\le {P}\left({k}\right)$
16 fveq2 ${⊢}{k}={i}\to {P}\left({k}\right)={P}\left({i}\right)$
17 16 breq2d ${⊢}{k}={i}\to \left({P}\left(0\right)\le {P}\left({k}\right)↔{P}\left(0\right)\le {P}\left({i}\right)\right)$
18 17 rspcva ${⊢}\left({i}\in \left(0\dots {M}\right)\wedge \forall {k}\in \left(0\dots {M}\right)\phantom{\rule{.4em}{0ex}}{P}\left(0\right)\le {P}\left({k}\right)\right)\to {P}\left(0\right)\le {P}\left({i}\right)$
19 18 expcom ${⊢}\forall {k}\in \left(0\dots {M}\right)\phantom{\rule{.4em}{0ex}}{P}\left(0\right)\le {P}\left({k}\right)\to \left({i}\in \left(0\dots {M}\right)\to {P}\left(0\right)\le {P}\left({i}\right)\right)$
20 15 19 syl ${⊢}{\phi }\to \left({i}\in \left(0\dots {M}\right)\to {P}\left(0\right)\le {P}\left({i}\right)\right)$
21 20 imp ${⊢}\left({\phi }\wedge {i}\in \left(0\dots {M}\right)\right)\to {P}\left(0\right)\le {P}\left({i}\right)$
22 1 2 iccpartleu ${⊢}{\phi }\to \forall {k}\in \left(0\dots {M}\right)\phantom{\rule{.4em}{0ex}}{P}\left({k}\right)\le {P}\left({M}\right)$
23 16 breq1d ${⊢}{k}={i}\to \left({P}\left({k}\right)\le {P}\left({M}\right)↔{P}\left({i}\right)\le {P}\left({M}\right)\right)$
24 23 rspcva ${⊢}\left({i}\in \left(0\dots {M}\right)\wedge \forall {k}\in \left(0\dots {M}\right)\phantom{\rule{.4em}{0ex}}{P}\left({k}\right)\le {P}\left({M}\right)\right)\to {P}\left({i}\right)\le {P}\left({M}\right)$
25 24 expcom ${⊢}\forall {k}\in \left(0\dots {M}\right)\phantom{\rule{.4em}{0ex}}{P}\left({k}\right)\le {P}\left({M}\right)\to \left({i}\in \left(0\dots {M}\right)\to {P}\left({i}\right)\le {P}\left({M}\right)\right)$
26 22 25 syl ${⊢}{\phi }\to \left({i}\in \left(0\dots {M}\right)\to {P}\left({i}\right)\le {P}\left({M}\right)\right)$
27 26 imp ${⊢}\left({\phi }\wedge {i}\in \left(0\dots {M}\right)\right)\to {P}\left({i}\right)\le {P}\left({M}\right)$
28 nnnn0 ${⊢}{M}\in ℕ\to {M}\in {ℕ}_{0}$
29 0elfz ${⊢}{M}\in {ℕ}_{0}\to 0\in \left(0\dots {M}\right)$
30 1 28 29 3syl ${⊢}{\phi }\to 0\in \left(0\dots {M}\right)$
31 1 2 30 iccpartxr ${⊢}{\phi }\to {P}\left(0\right)\in {ℝ}^{*}$
32 nn0fz0 ${⊢}{M}\in {ℕ}_{0}↔{M}\in \left(0\dots {M}\right)$
33 28 32 sylib ${⊢}{M}\in ℕ\to {M}\in \left(0\dots {M}\right)$
34 1 33 syl ${⊢}{\phi }\to {M}\in \left(0\dots {M}\right)$
35 1 2 34 iccpartxr ${⊢}{\phi }\to {P}\left({M}\right)\in {ℝ}^{*}$
36 31 35 jca ${⊢}{\phi }\to \left({P}\left(0\right)\in {ℝ}^{*}\wedge {P}\left({M}\right)\in {ℝ}^{*}\right)$
37 36 adantr ${⊢}\left({\phi }\wedge {i}\in \left(0\dots {M}\right)\right)\to \left({P}\left(0\right)\in {ℝ}^{*}\wedge {P}\left({M}\right)\in {ℝ}^{*}\right)$
38 elicc1 ${⊢}\left({P}\left(0\right)\in {ℝ}^{*}\wedge {P}\left({M}\right)\in {ℝ}^{*}\right)\to \left({P}\left({i}\right)\in \left[{P}\left(0\right),{P}\left({M}\right)\right]↔\left({P}\left({i}\right)\in {ℝ}^{*}\wedge {P}\left(0\right)\le {P}\left({i}\right)\wedge {P}\left({i}\right)\le {P}\left({M}\right)\right)\right)$
39 37 38 syl ${⊢}\left({\phi }\wedge {i}\in \left(0\dots {M}\right)\right)\to \left({P}\left({i}\right)\in \left[{P}\left(0\right),{P}\left({M}\right)\right]↔\left({P}\left({i}\right)\in {ℝ}^{*}\wedge {P}\left(0\right)\le {P}\left({i}\right)\wedge {P}\left({i}\right)\le {P}\left({M}\right)\right)\right)$
40 14 21 27 39 mpbir3and ${⊢}\left({\phi }\wedge {i}\in \left(0\dots {M}\right)\right)\to {P}\left({i}\right)\in \left[{P}\left(0\right),{P}\left({M}\right)\right]$
41 eleq1 ${⊢}{P}\left({i}\right)={p}\to \left({P}\left({i}\right)\in \left[{P}\left(0\right),{P}\left({M}\right)\right]↔{p}\in \left[{P}\left(0\right),{P}\left({M}\right)\right]\right)$
42 40 41 syl5ibcom ${⊢}\left({\phi }\wedge {i}\in \left(0\dots {M}\right)\right)\to \left({P}\left({i}\right)={p}\to {p}\in \left[{P}\left(0\right),{P}\left({M}\right)\right]\right)$
43 42 rexlimdva ${⊢}{\phi }\to \left(\exists {i}\in \left(0\dots {M}\right)\phantom{\rule{.4em}{0ex}}{P}\left({i}\right)={p}\to {p}\in \left[{P}\left(0\right),{P}\left({M}\right)\right]\right)$
44 10 43 sylbid ${⊢}{\phi }\to \left({p}\in \mathrm{ran}{P}\to {p}\in \left[{P}\left(0\right),{P}\left({M}\right)\right]\right)$
45 44 ssrdv ${⊢}{\phi }\to \mathrm{ran}{P}\subseteq \left[{P}\left(0\right),{P}\left({M}\right)\right]$