Metamath Proof Explorer

Theorem iccpartleu

Description: If there is a partition, then all intermediate points and the lower and the upper bound are less than or equal to the upper bound. (Contributed by AV, 14-Jul-2020)

Ref Expression
Hypotheses iccpartgtprec.m 
|- ( ph -> M e. NN )
iccpartgtprec.p 
|- ( ph -> P e. ( RePart ` M ) )
Assertion iccpartleu 
|- ( ph -> A. i e. ( 0 ... M ) ( P ` i ) <_ ( P ` M ) )

Proof

Step Hyp Ref Expression
1 iccpartgtprec.m 
 |-  ( ph -> M e. NN )
2 iccpartgtprec.p 
 |-  ( ph -> P e. ( RePart ` M ) )
3 nnnn0 
 |-  ( M e. NN -> M e. NN0 )
4 elnn0uz 
 |-  ( M e. NN0 <-> M e. ( ZZ>= ` 0 ) )
5 3 4 sylib 
 |-  ( M e. NN -> M e. ( ZZ>= ` 0 ) )
6 1 5 syl 
 |-  ( ph -> M e. ( ZZ>= ` 0 ) )
7 fzisfzounsn 
 |-  ( M e. ( ZZ>= ` 0 ) -> ( 0 ... M ) = ( ( 0 ..^ M ) u. { M } ) )
8 6 7 syl 
 |-  ( ph -> ( 0 ... M ) = ( ( 0 ..^ M ) u. { M } ) )
9 8 eleq2d 
 |-  ( ph -> ( i e. ( 0 ... M ) <-> i e. ( ( 0 ..^ M ) u. { M } ) ) )
10 elun 
 |-  ( i e. ( ( 0 ..^ M ) u. { M } ) <-> ( i e. ( 0 ..^ M ) \/ i e. { M } ) )
11 10 a1i 
 |-  ( ph -> ( i e. ( ( 0 ..^ M ) u. { M } ) <-> ( i e. ( 0 ..^ M ) \/ i e. { M } ) ) )
12 velsn 
 |-  ( i e. { M } <-> i = M )
13 12 a1i 
 |-  ( ph -> ( i e. { M } <-> i = M ) )
14 13 orbi2d 
 |-  ( ph -> ( ( i e. ( 0 ..^ M ) \/ i e. { M } ) <-> ( i e. ( 0 ..^ M ) \/ i = M ) ) )
15 9 11 14 3bitrd 
 |-  ( ph -> ( i e. ( 0 ... M ) <-> ( i e. ( 0 ..^ M ) \/ i = M ) ) )
16 1 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> M e. NN )
17 2 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> P e. ( RePart ` M ) )
18 fzossfz 
 |-  ( 0 ..^ M ) C_ ( 0 ... M )
19 18 a1i 
 |-  ( ph -> ( 0 ..^ M ) C_ ( 0 ... M ) )
20 19 sselda 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> i e. ( 0 ... M ) )
21 16 17 20 iccpartxr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( P ` i ) e. RR* )
22 nn0fz0 
 |-  ( M e. NN0 <-> M e. ( 0 ... M ) )
23 3 22 sylib 
 |-  ( M e. NN -> M e. ( 0 ... M ) )
24 1 23 syl 
 |-  ( ph -> M e. ( 0 ... M ) )
25 1 2 24 iccpartxr 
 |-  ( ph -> ( P ` M ) e. RR* )
26 25 adantr 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( P ` M ) e. RR* )
27 1 2 iccpartltu 
 |-  ( ph -> A. k e. ( 0 ..^ M ) ( P ` k ) < ( P ` M ) )
28 fveq2 
 |-  ( k = i -> ( P ` k ) = ( P ` i ) )
29 28 breq1d 
 |-  ( k = i -> ( ( P ` k ) < ( P ` M ) <-> ( P ` i ) < ( P ` M ) ) )
30 29 rspccv 
 |-  ( A. k e. ( 0 ..^ M ) ( P ` k ) < ( P ` M ) -> ( i e. ( 0 ..^ M ) -> ( P ` i ) < ( P ` M ) ) )
31 27 30 syl 
 |-  ( ph -> ( i e. ( 0 ..^ M ) -> ( P ` i ) < ( P ` M ) ) )
32 31 imp 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( P ` i ) < ( P ` M ) )
33 21 26 32 xrltled 
 |-  ( ( ph /\ i e. ( 0 ..^ M ) ) -> ( P ` i ) <_ ( P ` M ) )
34 33 expcom 
 |-  ( i e. ( 0 ..^ M ) -> ( ph -> ( P ` i ) <_ ( P ` M ) ) )
35 fveq2 
 |-  ( i = M -> ( P ` i ) = ( P ` M ) )
36 35 adantr 
 |-  ( ( i = M /\ ph ) -> ( P ` i ) = ( P ` M ) )
37 25 xrleidd 
 |-  ( ph -> ( P ` M ) <_ ( P ` M ) )
38 37 adantl 
 |-  ( ( i = M /\ ph ) -> ( P ` M ) <_ ( P ` M ) )
39 36 38 eqbrtrd 
 |-  ( ( i = M /\ ph ) -> ( P ` i ) <_ ( P ` M ) )
40 39 ex 
 |-  ( i = M -> ( ph -> ( P ` i ) <_ ( P ` M ) ) )
41 34 40 jaoi 
 |-  ( ( i e. ( 0 ..^ M ) \/ i = M ) -> ( ph -> ( P ` i ) <_ ( P ` M ) ) )
42 41 com12 
 |-  ( ph -> ( ( i e. ( 0 ..^ M ) \/ i = M ) -> ( P ` i ) <_ ( P ` M ) ) )
43 15 42 sylbid 
 |-  ( ph -> ( i e. ( 0 ... M ) -> ( P ` i ) <_ ( P ` M ) ) )
44 43 ralrimiv 
 |-  ( ph -> A. i e. ( 0 ... M ) ( P ` i ) <_ ( P ` M ) )