# 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
`|- ( ph -> M e. NN )`
iccpartgtprec.p
`|- ( ph -> P e. ( RePart ` M ) )`
Assertion iccpartgel
`|- ( ph -> A. i e. ( 0 ... M ) ( P ` 0 ) <_ ( P ` i ) )`

### Proof

Step Hyp Ref Expression
1 iccpartgtprec.m
` |-  ( ph -> M e. NN )`
2 iccpartgtprec.p
` |-  ( ph -> P e. ( RePart ` M ) )`
3 1 nnnn0d
` |-  ( ph -> M e. NN0 )`
4 elnn0uz
` |-  ( M e. NN0 <-> M e. ( ZZ>= ` 0 ) )`
5 3 4 sylib
` |-  ( ph -> M e. ( ZZ>= ` 0 ) )`
6 fzpred
` |-  ( M e. ( ZZ>= ` 0 ) -> ( 0 ... M ) = ( { 0 } u. ( ( 0 + 1 ) ... M ) ) )`
7 5 6 syl
` |-  ( ph -> ( 0 ... M ) = ( { 0 } u. ( ( 0 + 1 ) ... M ) ) )`
8 7 eleq2d
` |-  ( ph -> ( i e. ( 0 ... M ) <-> i e. ( { 0 } u. ( ( 0 + 1 ) ... M ) ) ) )`
9 elun
` |-  ( i e. ( { 0 } u. ( ( 0 + 1 ) ... M ) ) <-> ( i e. { 0 } \/ i e. ( ( 0 + 1 ) ... M ) ) )`
10 9 a1i
` |-  ( ph -> ( i e. ( { 0 } u. ( ( 0 + 1 ) ... M ) ) <-> ( i e. { 0 } \/ i e. ( ( 0 + 1 ) ... M ) ) ) )`
11 velsn
` |-  ( i e. { 0 } <-> i = 0 )`
12 11 a1i
` |-  ( ph -> ( i e. { 0 } <-> i = 0 ) )`
13 0p1e1
` |-  ( 0 + 1 ) = 1`
14 13 a1i
` |-  ( ph -> ( 0 + 1 ) = 1 )`
15 14 oveq1d
` |-  ( ph -> ( ( 0 + 1 ) ... M ) = ( 1 ... M ) )`
16 15 eleq2d
` |-  ( ph -> ( i e. ( ( 0 + 1 ) ... M ) <-> i e. ( 1 ... M ) ) )`
17 12 16 orbi12d
` |-  ( ph -> ( ( i e. { 0 } \/ i e. ( ( 0 + 1 ) ... M ) ) <-> ( i = 0 \/ i e. ( 1 ... M ) ) ) )`
18 8 10 17 3bitrd
` |-  ( ph -> ( i e. ( 0 ... M ) <-> ( i = 0 \/ i e. ( 1 ... M ) ) ) )`
19 0elfz
` |-  ( M e. NN0 -> 0 e. ( 0 ... M ) )`
20 3 19 syl
` |-  ( ph -> 0 e. ( 0 ... M ) )`
21 1 2 20 iccpartxr
` |-  ( ph -> ( P ` 0 ) e. RR* )`
22 21 xrleidd
` |-  ( ph -> ( P ` 0 ) <_ ( P ` 0 ) )`
23 fveq2
` |-  ( i = 0 -> ( P ` i ) = ( P ` 0 ) )`
24 23 breq2d
` |-  ( i = 0 -> ( ( P ` 0 ) <_ ( P ` i ) <-> ( P ` 0 ) <_ ( P ` 0 ) ) )`
25 22 24 syl5ibr
` |-  ( i = 0 -> ( ph -> ( P ` 0 ) <_ ( P ` i ) ) )`
` |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( P ` 0 ) e. RR* )`
` |-  ( ( ph /\ i e. ( 1 ... M ) ) -> M e. NN )`
` |-  ( ( ph /\ i e. ( 1 ... M ) ) -> P e. ( RePart ` M ) )`
29 1nn0
` |-  1 e. NN0`
30 29 a1i
` |-  ( ph -> 1 e. NN0 )`
31 elnn0uz
` |-  ( 1 e. NN0 <-> 1 e. ( ZZ>= ` 0 ) )`
32 30 31 sylib
` |-  ( ph -> 1 e. ( ZZ>= ` 0 ) )`
33 fzss1
` |-  ( 1 e. ( ZZ>= ` 0 ) -> ( 1 ... M ) C_ ( 0 ... M ) )`
34 32 33 syl
` |-  ( ph -> ( 1 ... M ) C_ ( 0 ... M ) )`
35 34 sselda
` |-  ( ( ph /\ i e. ( 1 ... M ) ) -> i e. ( 0 ... M ) )`
36 27 28 35 iccpartxr
` |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( P ` i ) e. RR* )`
37 1 2 iccpartgtl
` |-  ( ph -> A. k e. ( 1 ... M ) ( P ` 0 ) < ( P ` k ) )`
38 fveq2
` |-  ( k = i -> ( P ` k ) = ( P ` i ) )`
39 38 breq2d
` |-  ( k = i -> ( ( P ` 0 ) < ( P ` k ) <-> ( P ` 0 ) < ( P ` i ) ) )`
40 39 rspccv
` |-  ( A. k e. ( 1 ... M ) ( P ` 0 ) < ( P ` k ) -> ( i e. ( 1 ... M ) -> ( P ` 0 ) < ( P ` i ) ) )`
41 37 40 syl
` |-  ( ph -> ( i e. ( 1 ... M ) -> ( P ` 0 ) < ( P ` i ) ) )`
42 41 imp
` |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( P ` 0 ) < ( P ` i ) )`
43 26 36 42 xrltled
` |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( P ` 0 ) <_ ( P ` i ) )`
44 43 expcom
` |-  ( i e. ( 1 ... M ) -> ( ph -> ( P ` 0 ) <_ ( P ` i ) ) )`
45 25 44 jaoi
` |-  ( ( i = 0 \/ i e. ( 1 ... M ) ) -> ( ph -> ( P ` 0 ) <_ ( P ` i ) ) )`
46 45 com12
` |-  ( ph -> ( ( i = 0 \/ i e. ( 1 ... M ) ) -> ( P ` 0 ) <_ ( P ` i ) ) )`
47 18 46 sylbid
` |-  ( ph -> ( i e. ( 0 ... M ) -> ( P ` 0 ) <_ ( P ` i ) ) )`
48 47 ralrimiv
` |-  ( ph -> A. i e. ( 0 ... M ) ( P ` 0 ) <_ ( P ` i ) )`