# Metamath Proof Explorer

## Theorem iccpartgtl

Description: If there is a partition, then all intermediate points and the upper bound are strictly greater than 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 iccpartgtl ${⊢}{\phi }\to \forall {i}\in \left(1\dots {M}\right)\phantom{\rule{.4em}{0ex}}{P}\left(0\right)<{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 elnnuz ${⊢}{M}\in ℕ↔{M}\in {ℤ}_{\ge 1}$
4 1 3 sylib ${⊢}{\phi }\to {M}\in {ℤ}_{\ge 1}$
5 fzisfzounsn ${⊢}{M}\in {ℤ}_{\ge 1}\to \left(1\dots {M}\right)=\left(1..^{M}\right)\cup \left\{{M}\right\}$
6 4 5 syl ${⊢}{\phi }\to \left(1\dots {M}\right)=\left(1..^{M}\right)\cup \left\{{M}\right\}$
7 6 eleq2d ${⊢}{\phi }\to \left({i}\in \left(1\dots {M}\right)↔{i}\in \left(\left(1..^{M}\right)\cup \left\{{M}\right\}\right)\right)$
8 elun ${⊢}{i}\in \left(\left(1..^{M}\right)\cup \left\{{M}\right\}\right)↔\left({i}\in \left(1..^{M}\right)\vee {i}\in \left\{{M}\right\}\right)$
9 8 a1i ${⊢}{\phi }\to \left({i}\in \left(\left(1..^{M}\right)\cup \left\{{M}\right\}\right)↔\left({i}\in \left(1..^{M}\right)\vee {i}\in \left\{{M}\right\}\right)\right)$
10 velsn ${⊢}{i}\in \left\{{M}\right\}↔{i}={M}$
11 10 a1i ${⊢}{\phi }\to \left({i}\in \left\{{M}\right\}↔{i}={M}\right)$
12 11 orbi2d ${⊢}{\phi }\to \left(\left({i}\in \left(1..^{M}\right)\vee {i}\in \left\{{M}\right\}\right)↔\left({i}\in \left(1..^{M}\right)\vee {i}={M}\right)\right)$
13 7 9 12 3bitrd ${⊢}{\phi }\to \left({i}\in \left(1\dots {M}\right)↔\left({i}\in \left(1..^{M}\right)\vee {i}={M}\right)\right)$
14 fveq2 ${⊢}{k}={i}\to {P}\left({k}\right)={P}\left({i}\right)$
15 14 breq2d ${⊢}{k}={i}\to \left({P}\left(0\right)<{P}\left({k}\right)↔{P}\left(0\right)<{P}\left({i}\right)\right)$
16 15 rspccv ${⊢}\forall {k}\in \left(1..^{M}\right)\phantom{\rule{.4em}{0ex}}{P}\left(0\right)<{P}\left({k}\right)\to \left({i}\in \left(1..^{M}\right)\to {P}\left(0\right)<{P}\left({i}\right)\right)$
17 1 2 iccpartigtl ${⊢}{\phi }\to \forall {k}\in \left(1..^{M}\right)\phantom{\rule{.4em}{0ex}}{P}\left(0\right)<{P}\left({k}\right)$
18 16 17 syl11 ${⊢}{i}\in \left(1..^{M}\right)\to \left({\phi }\to {P}\left(0\right)<{P}\left({i}\right)\right)$
19 1 2 iccpartlt ${⊢}{\phi }\to {P}\left(0\right)<{P}\left({M}\right)$
20 19 adantl ${⊢}\left({i}={M}\wedge {\phi }\right)\to {P}\left(0\right)<{P}\left({M}\right)$
21 fveq2 ${⊢}{i}={M}\to {P}\left({i}\right)={P}\left({M}\right)$
22 21 adantr ${⊢}\left({i}={M}\wedge {\phi }\right)\to {P}\left({i}\right)={P}\left({M}\right)$
23 20 22 breqtrrd ${⊢}\left({i}={M}\wedge {\phi }\right)\to {P}\left(0\right)<{P}\left({i}\right)$
24 23 ex ${⊢}{i}={M}\to \left({\phi }\to {P}\left(0\right)<{P}\left({i}\right)\right)$
25 18 24 jaoi ${⊢}\left({i}\in \left(1..^{M}\right)\vee {i}={M}\right)\to \left({\phi }\to {P}\left(0\right)<{P}\left({i}\right)\right)$
26 25 com12 ${⊢}{\phi }\to \left(\left({i}\in \left(1..^{M}\right)\vee {i}={M}\right)\to {P}\left(0\right)<{P}\left({i}\right)\right)$
27 13 26 sylbid ${⊢}{\phi }\to \left({i}\in \left(1\dots {M}\right)\to {P}\left(0\right)<{P}\left({i}\right)\right)$
28 27 ralrimiv ${⊢}{\phi }\to \forall {i}\in \left(1\dots {M}\right)\phantom{\rule{.4em}{0ex}}{P}\left(0\right)<{P}\left({i}\right)$