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 ) ) )
26 21 adantr 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( P ` 0 ) e. RR* )
27 1 adantr 
 |-  ( ( ph /\ i e. ( 1 ... M ) ) -> M e. NN )
28 2 adantr 
 |-  ( ( 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 ) )