Metamath Proof Explorer

Theorem iccpartgel

Description: If there is a partition, then all intermediate points and the upper and the lower bound are greater than or equal to the lower bound. (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 iccpartgel ${⊢}{\phi }\to \forall {i}\in \left(0\dots {M}\right)\phantom{\rule{.4em}{0ex}}{P}\left(0\right)\le {P}\left({i}\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 1 nnnn0d ${⊢}{\phi }\to {M}\in {ℕ}_{0}$
4 elnn0uz ${⊢}{M}\in {ℕ}_{0}↔{M}\in {ℤ}_{\ge 0}$
5 3 4 sylib ${⊢}{\phi }\to {M}\in {ℤ}_{\ge 0}$
6 fzpred ${⊢}{M}\in {ℤ}_{\ge 0}\to \left(0\dots {M}\right)=\left\{0\right\}\cup \left(0+1\dots {M}\right)$
7 5 6 syl ${⊢}{\phi }\to \left(0\dots {M}\right)=\left\{0\right\}\cup \left(0+1\dots {M}\right)$
8 7 eleq2d ${⊢}{\phi }\to \left({i}\in \left(0\dots {M}\right)↔{i}\in \left(\left\{0\right\}\cup \left(0+1\dots {M}\right)\right)\right)$
9 elun ${⊢}{i}\in \left(\left\{0\right\}\cup \left(0+1\dots {M}\right)\right)↔\left({i}\in \left\{0\right\}\vee {i}\in \left(0+1\dots {M}\right)\right)$
10 9 a1i ${⊢}{\phi }\to \left({i}\in \left(\left\{0\right\}\cup \left(0+1\dots {M}\right)\right)↔\left({i}\in \left\{0\right\}\vee {i}\in \left(0+1\dots {M}\right)\right)\right)$
11 velsn ${⊢}{i}\in \left\{0\right\}↔{i}=0$
12 11 a1i ${⊢}{\phi }\to \left({i}\in \left\{0\right\}↔{i}=0\right)$
13 0p1e1 ${⊢}0+1=1$
14 13 a1i ${⊢}{\phi }\to 0+1=1$
15 14 oveq1d ${⊢}{\phi }\to \left(0+1\dots {M}\right)=\left(1\dots {M}\right)$
16 15 eleq2d ${⊢}{\phi }\to \left({i}\in \left(0+1\dots {M}\right)↔{i}\in \left(1\dots {M}\right)\right)$
17 12 16 orbi12d ${⊢}{\phi }\to \left(\left({i}\in \left\{0\right\}\vee {i}\in \left(0+1\dots {M}\right)\right)↔\left({i}=0\vee {i}\in \left(1\dots {M}\right)\right)\right)$
18 8 10 17 3bitrd ${⊢}{\phi }\to \left({i}\in \left(0\dots {M}\right)↔\left({i}=0\vee {i}\in \left(1\dots {M}\right)\right)\right)$
19 0elfz ${⊢}{M}\in {ℕ}_{0}\to 0\in \left(0\dots {M}\right)$
20 3 19 syl ${⊢}{\phi }\to 0\in \left(0\dots {M}\right)$
21 1 2 20 iccpartxr ${⊢}{\phi }\to {P}\left(0\right)\in {ℝ}^{*}$
22 21 xrleidd ${⊢}{\phi }\to {P}\left(0\right)\le {P}\left(0\right)$
23 fveq2 ${⊢}{i}=0\to {P}\left({i}\right)={P}\left(0\right)$
24 23 breq2d ${⊢}{i}=0\to \left({P}\left(0\right)\le {P}\left({i}\right)↔{P}\left(0\right)\le {P}\left(0\right)\right)$
25 22 24 syl5ibr ${⊢}{i}=0\to \left({\phi }\to {P}\left(0\right)\le {P}\left({i}\right)\right)$
26 21 adantr ${⊢}\left({\phi }\wedge {i}\in \left(1\dots {M}\right)\right)\to {P}\left(0\right)\in {ℝ}^{*}$
27 1 adantr ${⊢}\left({\phi }\wedge {i}\in \left(1\dots {M}\right)\right)\to {M}\in ℕ$
28 2 adantr ${⊢}\left({\phi }\wedge {i}\in \left(1\dots {M}\right)\right)\to {P}\in \mathrm{RePart}\left({M}\right)$
29 1nn0 ${⊢}1\in {ℕ}_{0}$
30 29 a1i ${⊢}{\phi }\to 1\in {ℕ}_{0}$
31 elnn0uz ${⊢}1\in {ℕ}_{0}↔1\in {ℤ}_{\ge 0}$
32 30 31 sylib ${⊢}{\phi }\to 1\in {ℤ}_{\ge 0}$
33 fzss1 ${⊢}1\in {ℤ}_{\ge 0}\to \left(1\dots {M}\right)\subseteq \left(0\dots {M}\right)$
34 32 33 syl ${⊢}{\phi }\to \left(1\dots {M}\right)\subseteq \left(0\dots {M}\right)$
35 34 sselda ${⊢}\left({\phi }\wedge {i}\in \left(1\dots {M}\right)\right)\to {i}\in \left(0\dots {M}\right)$
36 27 28 35 iccpartxr ${⊢}\left({\phi }\wedge {i}\in \left(1\dots {M}\right)\right)\to {P}\left({i}\right)\in {ℝ}^{*}$
37 1 2 iccpartgtl ${⊢}{\phi }\to \forall {k}\in \left(1\dots {M}\right)\phantom{\rule{.4em}{0ex}}{P}\left(0\right)<{P}\left({k}\right)$
38 fveq2 ${⊢}{k}={i}\to {P}\left({k}\right)={P}\left({i}\right)$
39 38 breq2d ${⊢}{k}={i}\to \left({P}\left(0\right)<{P}\left({k}\right)↔{P}\left(0\right)<{P}\left({i}\right)\right)$
40 39 rspccv ${⊢}\forall {k}\in \left(1\dots {M}\right)\phantom{\rule{.4em}{0ex}}{P}\left(0\right)<{P}\left({k}\right)\to \left({i}\in \left(1\dots {M}\right)\to {P}\left(0\right)<{P}\left({i}\right)\right)$
41 37 40 syl ${⊢}{\phi }\to \left({i}\in \left(1\dots {M}\right)\to {P}\left(0\right)<{P}\left({i}\right)\right)$
42 41 imp ${⊢}\left({\phi }\wedge {i}\in \left(1\dots {M}\right)\right)\to {P}\left(0\right)<{P}\left({i}\right)$
43 26 36 42 xrltled ${⊢}\left({\phi }\wedge {i}\in \left(1\dots {M}\right)\right)\to {P}\left(0\right)\le {P}\left({i}\right)$
44 43 expcom ${⊢}{i}\in \left(1\dots {M}\right)\to \left({\phi }\to {P}\left(0\right)\le {P}\left({i}\right)\right)$
45 25 44 jaoi ${⊢}\left({i}=0\vee {i}\in \left(1\dots {M}\right)\right)\to \left({\phi }\to {P}\left(0\right)\le {P}\left({i}\right)\right)$
46 45 com12 ${⊢}{\phi }\to \left(\left({i}=0\vee {i}\in \left(1\dots {M}\right)\right)\to {P}\left(0\right)\le {P}\left({i}\right)\right)$
47 18 46 sylbid ${⊢}{\phi }\to \left({i}\in \left(0\dots {M}\right)\to {P}\left(0\right)\le {P}\left({i}\right)\right)$
48 47 ralrimiv ${⊢}{\phi }\to \forall {i}\in \left(0\dots {M}\right)\phantom{\rule{.4em}{0ex}}{P}\left(0\right)\le {P}\left({i}\right)$