Metamath Proof Explorer

Theorem iccpartltu

Description: If there is a partition, then all intermediate points and the lower bound are strictly less than 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 iccpartltu 
|- ( 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 0zd 
 |-  ( M e. NN -> 0 e. ZZ )
4 nnz 
 |-  ( M e. NN -> M e. ZZ )
5 nngt0 
 |-  ( M e. NN -> 0 < M )
6 3 4 5 3jca 
 |-  ( M e. NN -> ( 0 e. ZZ /\ M e. ZZ /\ 0 < M ) )
7 1 6 syl 
 |-  ( ph -> ( 0 e. ZZ /\ M e. ZZ /\ 0 < M ) )
8 fzopred 
 |-  ( ( 0 e. ZZ /\ M e. ZZ /\ 0 < M ) -> ( 0 ..^ M ) = ( { 0 } u. ( ( 0 + 1 ) ..^ M ) ) )
9 7 8 syl 
 |-  ( ph -> ( 0 ..^ M ) = ( { 0 } u. ( ( 0 + 1 ) ..^ M ) ) )
10 0p1e1 
 |-  ( 0 + 1 ) = 1
11 10 a1i 
 |-  ( ph -> ( 0 + 1 ) = 1 )
12 11 oveq1d 
 |-  ( ph -> ( ( 0 + 1 ) ..^ M ) = ( 1 ..^ M ) )
13 12 uneq2d 
 |-  ( ph -> ( { 0 } u. ( ( 0 + 1 ) ..^ M ) ) = ( { 0 } u. ( 1 ..^ M ) ) )
14 9 13 eqtrd 
 |-  ( ph -> ( 0 ..^ M ) = ( { 0 } u. ( 1 ..^ M ) ) )
15 14 eleq2d 
 |-  ( ph -> ( i e. ( 0 ..^ M ) <-> i e. ( { 0 } u. ( 1 ..^ M ) ) ) )
16 elun 
 |-  ( i e. ( { 0 } u. ( 1 ..^ M ) ) <-> ( i e. { 0 } \/ i e. ( 1 ..^ M ) ) )
17 elsni 
 |-  ( i e. { 0 } -> i = 0 )
18 fveq2 
 |-  ( i = 0 -> ( P ` i ) = ( P ` 0 ) )
19 18 adantr 
 |-  ( ( i = 0 /\ ph ) -> ( P ` i ) = ( P ` 0 ) )
20 1 2 iccpartlt 
 |-  ( ph -> ( P ` 0 ) < ( P ` M ) )
21 20 adantl 
 |-  ( ( i = 0 /\ ph ) -> ( P ` 0 ) < ( P ` M ) )
22 19 21 eqbrtrd 
 |-  ( ( i = 0 /\ ph ) -> ( P ` i ) < ( P ` M ) )
23 22 ex 
 |-  ( i = 0 -> ( ph -> ( P ` i ) < ( P ` M ) ) )
24 17 23 syl 
 |-  ( i e. { 0 } -> ( ph -> ( P ` i ) < ( P ` M ) ) )
25 fveq2 
 |-  ( k = i -> ( P ` k ) = ( P ` i ) )
26 25 breq1d 
 |-  ( k = i -> ( ( P ` k ) < ( P ` M ) <-> ( P ` i ) < ( P ` M ) ) )
27 26 rspccv 
 |-  ( A. k e. ( 1 ..^ M ) ( P ` k ) < ( P ` M ) -> ( i e. ( 1 ..^ M ) -> ( P ` i ) < ( P ` M ) ) )
28 1 2 iccpartiltu 
 |-  ( ph -> A. k e. ( 1 ..^ M ) ( P ` k ) < ( P ` M ) )
29 27 28 syl11 
 |-  ( i e. ( 1 ..^ M ) -> ( ph -> ( P ` i ) < ( P ` M ) ) )
30 24 29 jaoi 
 |-  ( ( i e. { 0 } \/ i e. ( 1 ..^ M ) ) -> ( ph -> ( P ` i ) < ( P ` M ) ) )
31 30 com12 
 |-  ( ph -> ( ( i e. { 0 } \/ i e. ( 1 ..^ M ) ) -> ( P ` i ) < ( P ` M ) ) )
32 16 31 syl5bi 
 |-  ( ph -> ( i e. ( { 0 } u. ( 1 ..^ M ) ) -> ( P ` i ) < ( P ` M ) ) )
33 15 32 sylbid 
 |-  ( ph -> ( i e. ( 0 ..^ M ) -> ( P ` i ) < ( P ` M ) ) )
34 33 ralrimiv 
 |-  ( ph -> A. i e. ( 0 ..^ M ) ( P ` i ) < ( P ` M ) )