Metamath Proof Explorer

Theorem iccpartiltu

Description: If there is a partition, then all intermediate points are strictly less than the upper bound. (Contributed by AV, 12-Jul-2020)

Ref Expression
Hypotheses iccpartgtprec.m 
|- ( ph -> M e. NN )
iccpartgtprec.p 
|- ( ph -> P e. ( RePart ` M ) )
Assertion iccpartiltu 
|- ( ph -> A. i e. ( 1 ..^ 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 ral0 
 |-  A. i e. (/) ( P ` i ) < ( P ` 1 )
4 oveq2 
 |-  ( M = 1 -> ( 1 ..^ M ) = ( 1 ..^ 1 ) )
5 fzo0 
 |-  ( 1 ..^ 1 ) = (/)
6 4 5 eqtrdi 
 |-  ( M = 1 -> ( 1 ..^ M ) = (/) )
7 fveq2 
 |-  ( M = 1 -> ( P ` M ) = ( P ` 1 ) )
8 7 breq2d 
 |-  ( M = 1 -> ( ( P ` i ) < ( P ` M ) <-> ( P ` i ) < ( P ` 1 ) ) )
9 6 8 raleqbidv 
 |-  ( M = 1 -> ( A. i e. ( 1 ..^ M ) ( P ` i ) < ( P ` M ) <-> A. i e. (/) ( P ` i ) < ( P ` 1 ) ) )
10 3 9 mpbiri 
 |-  ( M = 1 -> A. i e. ( 1 ..^ M ) ( P ` i ) < ( P ` M ) )
11 10 2a1d 
 |-  ( M = 1 -> ( ph -> ( M e. NN -> A. i e. ( 1 ..^ M ) ( P ` i ) < ( P ` M ) ) ) )
12 simpr 
 |-  ( ( ( ph /\ -. M = 1 ) /\ M e. NN ) -> M e. NN )
13 2 adantr 
 |-  ( ( ph /\ -. M = 1 ) -> P e. ( RePart ` M ) )
14 13 adantr 
 |-  ( ( ( ph /\ -. M = 1 ) /\ M e. NN ) -> P e. ( RePart ` M ) )
15 nnnn0 
 |-  ( M e. NN -> M e. NN0 )
16 nn0fz0 
 |-  ( M e. NN0 <-> M e. ( 0 ... M ) )
17 15 16 sylib 
 |-  ( M e. NN -> M e. ( 0 ... M ) )
18 17 adantl 
 |-  ( ( ( ph /\ -. M = 1 ) /\ M e. NN ) -> M e. ( 0 ... M ) )
19 12 14 18 iccpartxr 
 |-  ( ( ( ph /\ -. M = 1 ) /\ M e. NN ) -> ( P ` M ) e. RR* )
20 elxr 
 |-  ( ( P ` M ) e. RR* <-> ( ( P ` M ) e. RR \/ ( P ` M ) = +oo \/ ( P ` M ) = -oo ) )
21 elfzoelz 
 |-  ( i e. ( 1 ..^ M ) -> i e. ZZ )
22 21 ad2antll 
 |-  ( ( ( P ` M ) e. RR /\ ( ( ( ph /\ -. M = 1 ) /\ M e. NN ) /\ i e. ( 1 ..^ M ) ) ) -> i e. ZZ )
23 elfzo2 
 |-  ( i e. ( 1 ..^ M ) <-> ( i e. ( ZZ>= ` 1 ) /\ M e. ZZ /\ i < M ) )
24 eluzelz 
 |-  ( i e. ( ZZ>= ` 1 ) -> i e. ZZ )
25 24 peano2zd 
 |-  ( i e. ( ZZ>= ` 1 ) -> ( i + 1 ) e. ZZ )
26 25 3ad2ant1 
 |-  ( ( i e. ( ZZ>= ` 1 ) /\ M e. ZZ /\ i < M ) -> ( i + 1 ) e. ZZ )
27 simp2 
 |-  ( ( i e. ( ZZ>= ` 1 ) /\ M e. ZZ /\ i < M ) -> M e. ZZ )
28 zltp1le 
 |-  ( ( i e. ZZ /\ M e. ZZ ) -> ( i < M <-> ( i + 1 ) <_ M ) )
29 24 28 sylan 
 |-  ( ( i e. ( ZZ>= ` 1 ) /\ M e. ZZ ) -> ( i < M <-> ( i + 1 ) <_ M ) )
30 29 biimp3a 
 |-  ( ( i e. ( ZZ>= ` 1 ) /\ M e. ZZ /\ i < M ) -> ( i + 1 ) <_ M )
31 eluz2 
 |-  ( M e. ( ZZ>= ` ( i + 1 ) ) <-> ( ( i + 1 ) e. ZZ /\ M e. ZZ /\ ( i + 1 ) <_ M ) )
32 26 27 30 31 syl3anbrc 
 |-  ( ( i e. ( ZZ>= ` 1 ) /\ M e. ZZ /\ i < M ) -> M e. ( ZZ>= ` ( i + 1 ) ) )
33 23 32 sylbi 
 |-  ( i e. ( 1 ..^ M ) -> M e. ( ZZ>= ` ( i + 1 ) ) )
34 33 ad2antll 
 |-  ( ( ( P ` M ) e. RR /\ ( ( ( ph /\ -. M = 1 ) /\ M e. NN ) /\ i e. ( 1 ..^ M ) ) ) -> M e. ( ZZ>= ` ( i + 1 ) ) )
35 fveq2 
 |-  ( k = M -> ( P ` k ) = ( P ` M ) )
36 35 eqcomd 
 |-  ( k = M -> ( P ` M ) = ( P ` k ) )
37 36 eleq1d 
 |-  ( k = M -> ( ( P ` M ) e. RR <-> ( P ` k ) e. RR ) )
38 37 biimpcd 
 |-  ( ( P ` M ) e. RR -> ( k = M -> ( P ` k ) e. RR ) )
39 38 adantr 
 |-  ( ( ( P ` M ) e. RR /\ ( ( ( ph /\ -. M = 1 ) /\ M e. NN ) /\ i e. ( 1 ..^ M ) ) ) -> ( k = M -> ( P ` k ) e. RR ) )
40 39 adantr 
 |-  ( ( ( ( P ` M ) e. RR /\ ( ( ( ph /\ -. M = 1 ) /\ M e. NN ) /\ i e. ( 1 ..^ M ) ) ) /\ k e. ( i ... M ) ) -> ( k = M -> ( P ` k ) e. RR ) )
41 40 com12 
 |-  ( k = M -> ( ( ( ( P ` M ) e. RR /\ ( ( ( ph /\ -. M = 1 ) /\ M e. NN ) /\ i e. ( 1 ..^ M ) ) ) /\ k e. ( i ... M ) ) -> ( P ` k ) e. RR ) )
42 12 adantr 
 |-  ( ( ( ( ph /\ -. M = 1 ) /\ M e. NN ) /\ i e. ( 1 ..^ M ) ) -> M e. NN )
43 42 adantl 
 |-  ( ( ( P ` M ) e. RR /\ ( ( ( ph /\ -. M = 1 ) /\ M e. NN ) /\ i e. ( 1 ..^ M ) ) ) -> M e. NN )
44 43 adantr 
 |-  ( ( ( ( P ` M ) e. RR /\ ( ( ( ph /\ -. M = 1 ) /\ M e. NN ) /\ i e. ( 1 ..^ M ) ) ) /\ k e. ( i ... M ) ) -> M e. NN )
45 44 adantl 
 |-  ( ( -. k = M /\ ( ( ( P ` M ) e. RR /\ ( ( ( ph /\ -. M = 1 ) /\ M e. NN ) /\ i e. ( 1 ..^ M ) ) ) /\ k e. ( i ... M ) ) ) -> M e. NN )
46 14 adantr 
 |-  ( ( ( ( ph /\ -. M = 1 ) /\ M e. NN ) /\ i e. ( 1 ..^ M ) ) -> P e. ( RePart ` M ) )
47 46 adantl 
 |-  ( ( ( P ` M ) e. RR /\ ( ( ( ph /\ -. M = 1 ) /\ M e. NN ) /\ i e. ( 1 ..^ M ) ) ) -> P e. ( RePart ` M ) )
48 47 adantr 
 |-  ( ( ( ( P ` M ) e. RR /\ ( ( ( ph /\ -. M = 1 ) /\ M e. NN ) /\ i e. ( 1 ..^ M ) ) ) /\ k e. ( i ... M ) ) -> P e. ( RePart ` M ) )
49 48 adantl 
 |-  ( ( -. k = M /\ ( ( ( P ` M ) e. RR /\ ( ( ( ph /\ -. M = 1 ) /\ M e. NN ) /\ i e. ( 1 ..^ M ) ) ) /\ k e. ( i ... M ) ) ) -> P e. ( RePart ` M ) )
50 elfz2 
 |-  ( k e. ( i ... M ) <-> ( ( i e. ZZ /\ M e. ZZ /\ k e. ZZ ) /\ ( i <_ k /\ k <_ M ) ) )
51 eluz2 
 |-  ( i e. ( ZZ>= ` 1 ) <-> ( 1 e. ZZ /\ i e. ZZ /\ 1 <_ i ) )
52 1red 
 |-  ( ( i e. ZZ /\ k e. ZZ ) -> 1 e. RR )
53 zre 
 |-  ( i e. ZZ -> i e. RR )
54 53 adantr 
 |-  ( ( i e. ZZ /\ k e. ZZ ) -> i e. RR )
55 zre 
 |-  ( k e. ZZ -> k e. RR )
56 55 adantl 
 |-  ( ( i e. ZZ /\ k e. ZZ ) -> k e. RR )
57 letr 
 |-  ( ( 1 e. RR /\ i e. RR /\ k e. RR ) -> ( ( 1 <_ i /\ i <_ k ) -> 1 <_ k ) )
58 52 54 56 57 syl3anc 
 |-  ( ( i e. ZZ /\ k e. ZZ ) -> ( ( 1 <_ i /\ i <_ k ) -> 1 <_ k ) )
59 58 expcomd 
 |-  ( ( i e. ZZ /\ k e. ZZ ) -> ( i <_ k -> ( 1 <_ i -> 1 <_ k ) ) )
60 59 adantrd 
 |-  ( ( i e. ZZ /\ k e. ZZ ) -> ( ( i <_ k /\ k <_ M ) -> ( 1 <_ i -> 1 <_ k ) ) )
61 60 3adant2 
 |-  ( ( i e. ZZ /\ M e. ZZ /\ k e. ZZ ) -> ( ( i <_ k /\ k <_ M ) -> ( 1 <_ i -> 1 <_ k ) ) )
62 61 imp 
 |-  ( ( ( i e. ZZ /\ M e. ZZ /\ k e. ZZ ) /\ ( i <_ k /\ k <_ M ) ) -> ( 1 <_ i -> 1 <_ k ) )
63 62 com12 
 |-  ( 1 <_ i -> ( ( ( i e. ZZ /\ M e. ZZ /\ k e. ZZ ) /\ ( i <_ k /\ k <_ M ) ) -> 1 <_ k ) )
64 63 3ad2ant3 
 |-  ( ( 1 e. ZZ /\ i e. ZZ /\ 1 <_ i ) -> ( ( ( i e. ZZ /\ M e. ZZ /\ k e. ZZ ) /\ ( i <_ k /\ k <_ M ) ) -> 1 <_ k ) )
65 51 64 sylbi 
 |-  ( i e. ( ZZ>= ` 1 ) -> ( ( ( i e. ZZ /\ M e. ZZ /\ k e. ZZ ) /\ ( i <_ k /\ k <_ M ) ) -> 1 <_ k ) )
66 65 3ad2ant1 
 |-  ( ( i e. ( ZZ>= ` 1 ) /\ M e. ZZ /\ i < M ) -> ( ( ( i e. ZZ /\ M e. ZZ /\ k e. ZZ ) /\ ( i <_ k /\ k <_ M ) ) -> 1 <_ k ) )
67 23 66 sylbi 
 |-  ( i e. ( 1 ..^ M ) -> ( ( ( i e. ZZ /\ M e. ZZ /\ k e. ZZ ) /\ ( i <_ k /\ k <_ M ) ) -> 1 <_ k ) )
68 50 67 biimtrid 
 |-  ( i e. ( 1 ..^ M ) -> ( k e. ( i ... M ) -> 1 <_ k ) )
69 68 imp 
 |-  ( ( i e. ( 1 ..^ M ) /\ k e. ( i ... M ) ) -> 1 <_ k )
70 69 3adant3 
 |-  ( ( i e. ( 1 ..^ M ) /\ k e. ( i ... M ) /\ -. k = M ) -> 1 <_ k )
71 zre 
 |-  ( M e. ZZ -> M e. RR )
72 71 55 anim12ci 
 |-  ( ( M e. ZZ /\ k e. ZZ ) -> ( k e. RR /\ M e. RR ) )
73 72 3adant1 
 |-  ( ( i e. ZZ /\ M e. ZZ /\ k e. ZZ ) -> ( k e. RR /\ M e. RR ) )
74 ltlen 
 |-  ( ( k e. RR /\ M e. RR ) -> ( k < M <-> ( k <_ M /\ M =/= k ) ) )
75 73 74 syl 
 |-  ( ( i e. ZZ /\ M e. ZZ /\ k e. ZZ ) -> ( k < M <-> ( k <_ M /\ M =/= k ) ) )
76 nesym 
 |-  ( M =/= k <-> -. k = M )
77 76 anbi2i 
 |-  ( ( k <_ M /\ M =/= k ) <-> ( k <_ M /\ -. k = M ) )
78 75 77 bitr2di 
 |-  ( ( i e. ZZ /\ M e. ZZ /\ k e. ZZ ) -> ( ( k <_ M /\ -. k = M ) <-> k < M ) )
79 78 biimpd 
 |-  ( ( i e. ZZ /\ M e. ZZ /\ k e. ZZ ) -> ( ( k <_ M /\ -. k = M ) -> k < M ) )
80 79 expd 
 |-  ( ( i e. ZZ /\ M e. ZZ /\ k e. ZZ ) -> ( k <_ M -> ( -. k = M -> k < M ) ) )
81 80 adantld 
 |-  ( ( i e. ZZ /\ M e. ZZ /\ k e. ZZ ) -> ( ( i <_ k /\ k <_ M ) -> ( -. k = M -> k < M ) ) )
82 81 imp 
 |-  ( ( ( i e. ZZ /\ M e. ZZ /\ k e. ZZ ) /\ ( i <_ k /\ k <_ M ) ) -> ( -. k = M -> k < M ) )
83 50 82 sylbi 
 |-  ( k e. ( i ... M ) -> ( -. k = M -> k < M ) )
84 83 imp 
 |-  ( ( k e. ( i ... M ) /\ -. k = M ) -> k < M )
85 84 3adant1 
 |-  ( ( i e. ( 1 ..^ M ) /\ k e. ( i ... M ) /\ -. k = M ) -> k < M )
86 70 85 jca 
 |-  ( ( i e. ( 1 ..^ M ) /\ k e. ( i ... M ) /\ -. k = M ) -> ( 1 <_ k /\ k < M ) )
87 elfzelz 
 |-  ( k e. ( i ... M ) -> k e. ZZ )
88 1zzd 
 |-  ( k e. ( i ... M ) -> 1 e. ZZ )
89 elfzel2 
 |-  ( k e. ( i ... M ) -> M e. ZZ )
90 87 88 89 3jca 
 |-  ( k e. ( i ... M ) -> ( k e. ZZ /\ 1 e. ZZ /\ M e. ZZ ) )
91 90 3ad2ant2 
 |-  ( ( i e. ( 1 ..^ M ) /\ k e. ( i ... M ) /\ -. k = M ) -> ( k e. ZZ /\ 1 e. ZZ /\ M e. ZZ ) )
92 elfzo 
 |-  ( ( k e. ZZ /\ 1 e. ZZ /\ M e. ZZ ) -> ( k e. ( 1 ..^ M ) <-> ( 1 <_ k /\ k < M ) ) )
93 91 92 syl 
 |-  ( ( i e. ( 1 ..^ M ) /\ k e. ( i ... M ) /\ -. k = M ) -> ( k e. ( 1 ..^ M ) <-> ( 1 <_ k /\ k < M ) ) )
94 86 93 mpbird 
 |-  ( ( i e. ( 1 ..^ M ) /\ k e. ( i ... M ) /\ -. k = M ) -> k e. ( 1 ..^ M ) )
95 94 3exp 
 |-  ( i e. ( 1 ..^ M ) -> ( k e. ( i ... M ) -> ( -. k = M -> k e. ( 1 ..^ M ) ) ) )
96 95 ad2antll 
 |-  ( ( ( P ` M ) e. RR /\ ( ( ( ph /\ -. M = 1 ) /\ M e. NN ) /\ i e. ( 1 ..^ M ) ) ) -> ( k e. ( i ... M ) -> ( -. k = M -> k e. ( 1 ..^ M ) ) ) )
97 96 imp 
 |-  ( ( ( ( P ` M ) e. RR /\ ( ( ( ph /\ -. M = 1 ) /\ M e. NN ) /\ i e. ( 1 ..^ M ) ) ) /\ k e. ( i ... M ) ) -> ( -. k = M -> k e. ( 1 ..^ M ) ) )
98 97 impcom 
 |-  ( ( -. k = M /\ ( ( ( P ` M ) e. RR /\ ( ( ( ph /\ -. M = 1 ) /\ M e. NN ) /\ i e. ( 1 ..^ M ) ) ) /\ k e. ( i ... M ) ) ) -> k e. ( 1 ..^ M ) )
99 45 49 98 iccpartipre 
 |-  ( ( -. k = M /\ ( ( ( P ` M ) e. RR /\ ( ( ( ph /\ -. M = 1 ) /\ M e. NN ) /\ i e. ( 1 ..^ M ) ) ) /\ k e. ( i ... M ) ) ) -> ( P ` k ) e. RR )
100 99 ex 
 |-  ( -. k = M -> ( ( ( ( P ` M ) e. RR /\ ( ( ( ph /\ -. M = 1 ) /\ M e. NN ) /\ i e. ( 1 ..^ M ) ) ) /\ k e. ( i ... M ) ) -> ( P ` k ) e. RR ) )
101 41 100 pm2.61i 
 |-  ( ( ( ( P ` M ) e. RR /\ ( ( ( ph /\ -. M = 1 ) /\ M e. NN ) /\ i e. ( 1 ..^ M ) ) ) /\ k e. ( i ... M ) ) -> ( P ` k ) e. RR )
102 43 adantr 
 |-  ( ( ( ( P ` M ) e. RR /\ ( ( ( ph /\ -. M = 1 ) /\ M e. NN ) /\ i e. ( 1 ..^ M ) ) ) /\ k e. ( i ... ( M - 1 ) ) ) -> M e. NN )
103 47 adantr 
 |-  ( ( ( ( P ` M ) e. RR /\ ( ( ( ph /\ -. M = 1 ) /\ M e. NN ) /\ i e. ( 1 ..^ M ) ) ) /\ k e. ( i ... ( M - 1 ) ) ) -> P e. ( RePart ` M ) )
104 1eluzge0 
 |-  1 e. ( ZZ>= ` 0 )
105 fzoss1 
 |-  ( 1 e. ( ZZ>= ` 0 ) -> ( 1 ..^ M ) C_ ( 0 ..^ M ) )
106 104 105 mp1i 
 |-  ( ( i e. ( 1 ..^ M ) /\ k e. ( i ... ( M - 1 ) ) ) -> ( 1 ..^ M ) C_ ( 0 ..^ M ) )
107 elfzoel2 
 |-  ( i e. ( 1 ..^ M ) -> M e. ZZ )
108 fzoval 
 |-  ( M e. ZZ -> ( i ..^ M ) = ( i ... ( M - 1 ) ) )
109 107 108 syl 
 |-  ( i e. ( 1 ..^ M ) -> ( i ..^ M ) = ( i ... ( M - 1 ) ) )
110 109 eqcomd 
 |-  ( i e. ( 1 ..^ M ) -> ( i ... ( M - 1 ) ) = ( i ..^ M ) )
111 110 eleq2d 
 |-  ( i e. ( 1 ..^ M ) -> ( k e. ( i ... ( M - 1 ) ) <-> k e. ( i ..^ M ) ) )
112 elfzouz 
 |-  ( i e. ( 1 ..^ M ) -> i e. ( ZZ>= ` 1 ) )
113 fzoss1 
 |-  ( i e. ( ZZ>= ` 1 ) -> ( i ..^ M ) C_ ( 1 ..^ M ) )
114 112 113 syl 
 |-  ( i e. ( 1 ..^ M ) -> ( i ..^ M ) C_ ( 1 ..^ M ) )
115 114 sseld 
 |-  ( i e. ( 1 ..^ M ) -> ( k e. ( i ..^ M ) -> k e. ( 1 ..^ M ) ) )
116 111 115 sylbid 
 |-  ( i e. ( 1 ..^ M ) -> ( k e. ( i ... ( M - 1 ) ) -> k e. ( 1 ..^ M ) ) )
117 116 imp 
 |-  ( ( i e. ( 1 ..^ M ) /\ k e. ( i ... ( M - 1 ) ) ) -> k e. ( 1 ..^ M ) )
118 106 117 sseldd 
 |-  ( ( i e. ( 1 ..^ M ) /\ k e. ( i ... ( M - 1 ) ) ) -> k e. ( 0 ..^ M ) )
119 118 ex 
 |-  ( i e. ( 1 ..^ M ) -> ( k e. ( i ... ( M - 1 ) ) -> k e. ( 0 ..^ M ) ) )
120 119 ad2antll 
 |-  ( ( ( P ` M ) e. RR /\ ( ( ( ph /\ -. M = 1 ) /\ M e. NN ) /\ i e. ( 1 ..^ M ) ) ) -> ( k e. ( i ... ( M - 1 ) ) -> k e. ( 0 ..^ M ) ) )
121 120 imp 
 |-  ( ( ( ( P ` M ) e. RR /\ ( ( ( ph /\ -. M = 1 ) /\ M e. NN ) /\ i e. ( 1 ..^ M ) ) ) /\ k e. ( i ... ( M - 1 ) ) ) -> k e. ( 0 ..^ M ) )
122 iccpartimp 
 |-  ( ( M e. NN /\ P e. ( RePart ` M ) /\ k e. ( 0 ..^ M ) ) -> ( P e. ( RR* ^m ( 0 ... M ) ) /\ ( P ` k ) < ( P ` ( k + 1 ) ) ) )
123 102 103 121 122 syl3anc 
 |-  ( ( ( ( P ` M ) e. RR /\ ( ( ( ph /\ -. M = 1 ) /\ M e. NN ) /\ i e. ( 1 ..^ M ) ) ) /\ k e. ( i ... ( M - 1 ) ) ) -> ( P e. ( RR* ^m ( 0 ... M ) ) /\ ( P ` k ) < ( P ` ( k + 1 ) ) ) )
124 123 simprd 
 |-  ( ( ( ( P ` M ) e. RR /\ ( ( ( ph /\ -. M = 1 ) /\ M e. NN ) /\ i e. ( 1 ..^ M ) ) ) /\ k e. ( i ... ( M - 1 ) ) ) -> ( P ` k ) < ( P ` ( k + 1 ) ) )
125 22 34 101 124 smonoord 
 |-  ( ( ( P ` M ) e. RR /\ ( ( ( ph /\ -. M = 1 ) /\ M e. NN ) /\ i e. ( 1 ..^ M ) ) ) -> ( P ` i ) < ( P ` M ) )
126 125 ex 
 |-  ( ( P ` M ) e. RR -> ( ( ( ( ph /\ -. M = 1 ) /\ M e. NN ) /\ i e. ( 1 ..^ M ) ) -> ( P ` i ) < ( P ` M ) ) )
127 simpr 
 |-  ( ( ( ( ph /\ -. M = 1 ) /\ M e. NN ) /\ i e. ( 1 ..^ M ) ) -> i e. ( 1 ..^ M ) )
128 42 46 127 iccpartipre 
 |-  ( ( ( ( ph /\ -. M = 1 ) /\ M e. NN ) /\ i e. ( 1 ..^ M ) ) -> ( P ` i ) e. RR )
129 ltpnf 
 |-  ( ( P ` i ) e. RR -> ( P ` i ) < +oo )
130 128 129 syl 
 |-  ( ( ( ( ph /\ -. M = 1 ) /\ M e. NN ) /\ i e. ( 1 ..^ M ) ) -> ( P ` i ) < +oo )
131 breq2 
 |-  ( ( P ` M ) = +oo -> ( ( P ` i ) < ( P ` M ) <-> ( P ` i ) < +oo ) )
132 130 131 imbitrrid 
 |-  ( ( P ` M ) = +oo -> ( ( ( ( ph /\ -. M = 1 ) /\ M e. NN ) /\ i e. ( 1 ..^ M ) ) -> ( P ` i ) < ( P ` M ) ) )
133 42 adantl 
 |-  ( ( ( P ` M ) = -oo /\ ( ( ( ph /\ -. M = 1 ) /\ M e. NN ) /\ i e. ( 1 ..^ M ) ) ) -> M e. NN )
134 46 adantl 
 |-  ( ( ( P ` M ) = -oo /\ ( ( ( ph /\ -. M = 1 ) /\ M e. NN ) /\ i e. ( 1 ..^ M ) ) ) -> P e. ( RePart ` M ) )
135 elfzofz 
 |-  ( i e. ( 1 ..^ M ) -> i e. ( 1 ... M ) )
136 135 ad2antll 
 |-  ( ( ( P ` M ) = -oo /\ ( ( ( ph /\ -. M = 1 ) /\ M e. NN ) /\ i e. ( 1 ..^ M ) ) ) -> i e. ( 1 ... M ) )
137 elfzubelfz 
 |-  ( i e. ( 1 ... M ) -> M e. ( 1 ... M ) )
138 136 137 syl 
 |-  ( ( ( P ` M ) = -oo /\ ( ( ( ph /\ -. M = 1 ) /\ M e. NN ) /\ i e. ( 1 ..^ M ) ) ) -> M e. ( 1 ... M ) )
139 133 134 138 iccpartgtprec 
 |-  ( ( ( P ` M ) = -oo /\ ( ( ( ph /\ -. M = 1 ) /\ M e. NN ) /\ i e. ( 1 ..^ M ) ) ) -> ( P ` ( M - 1 ) ) < ( P ` M ) )
140 breq2 
 |-  ( -oo = ( P ` M ) -> ( ( P ` ( M - 1 ) ) < -oo <-> ( P ` ( M - 1 ) ) < ( P ` M ) ) )
141 140 eqcoms 
 |-  ( ( P ` M ) = -oo -> ( ( P ` ( M - 1 ) ) < -oo <-> ( P ` ( M - 1 ) ) < ( P ` M ) ) )
142 141 adantr 
 |-  ( ( ( P ` M ) = -oo /\ ( ( ( ph /\ -. M = 1 ) /\ M e. NN ) /\ i e. ( 1 ..^ M ) ) ) -> ( ( P ` ( M - 1 ) ) < -oo <-> ( P ` ( M - 1 ) ) < ( P ` M ) ) )
143 139 142 mpbird 
 |-  ( ( ( P ` M ) = -oo /\ ( ( ( ph /\ -. M = 1 ) /\ M e. NN ) /\ i e. ( 1 ..^ M ) ) ) -> ( P ` ( M - 1 ) ) < -oo )
144 15 adantl 
 |-  ( ( ( ph /\ -. M = 1 ) /\ M e. NN ) -> M e. NN0 )
145 144 adantr 
 |-  ( ( ( ( ph /\ -. M = 1 ) /\ M e. NN ) /\ i e. ( 1 ..^ M ) ) -> M e. NN0 )
146 nnne0 
 |-  ( M e. NN -> M =/= 0 )
147 146 adantl 
 |-  ( ( ( ph /\ -. M = 1 ) /\ M e. NN ) -> M =/= 0 )
148 df-ne 
 |-  ( M =/= 1 <-> -. M = 1 )
149 148 biimpri 
 |-  ( -. M = 1 -> M =/= 1 )
150 149 adantl 
 |-  ( ( ph /\ -. M = 1 ) -> M =/= 1 )
151 150 adantr 
 |-  ( ( ( ph /\ -. M = 1 ) /\ M e. NN ) -> M =/= 1 )
152 144 147 151 3jca 
 |-  ( ( ( ph /\ -. M = 1 ) /\ M e. NN ) -> ( M e. NN0 /\ M =/= 0 /\ M =/= 1 ) )
153 152 adantr 
 |-  ( ( ( ( ph /\ -. M = 1 ) /\ M e. NN ) /\ i e. ( 1 ..^ M ) ) -> ( M e. NN0 /\ M =/= 0 /\ M =/= 1 ) )
154 nn0n0n1ge2 
 |-  ( ( M e. NN0 /\ M =/= 0 /\ M =/= 1 ) -> 2 <_ M )
155 153 154 syl 
 |-  ( ( ( ( ph /\ -. M = 1 ) /\ M e. NN ) /\ i e. ( 1 ..^ M ) ) -> 2 <_ M )
156 145 155 jca 
 |-  ( ( ( ( ph /\ -. M = 1 ) /\ M e. NN ) /\ i e. ( 1 ..^ M ) ) -> ( M e. NN0 /\ 2 <_ M ) )
157 156 adantl 
 |-  ( ( ( P ` M ) = -oo /\ ( ( ( ph /\ -. M = 1 ) /\ M e. NN ) /\ i e. ( 1 ..^ M ) ) ) -> ( M e. NN0 /\ 2 <_ M ) )
158 ige2m1fz 
 |-  ( ( M e. NN0 /\ 2 <_ M ) -> ( M - 1 ) e. ( 0 ... M ) )
159 157 158 syl 
 |-  ( ( ( P ` M ) = -oo /\ ( ( ( ph /\ -. M = 1 ) /\ M e. NN ) /\ i e. ( 1 ..^ M ) ) ) -> ( M - 1 ) e. ( 0 ... M ) )
160 133 134 159 iccpartxr 
 |-  ( ( ( P ` M ) = -oo /\ ( ( ( ph /\ -. M = 1 ) /\ M e. NN ) /\ i e. ( 1 ..^ M ) ) ) -> ( P ` ( M - 1 ) ) e. RR* )
161 nltmnf 
 |-  ( ( P ` ( M - 1 ) ) e. RR* -> -. ( P ` ( M - 1 ) ) < -oo )
162 160 161 syl 
 |-  ( ( ( P ` M ) = -oo /\ ( ( ( ph /\ -. M = 1 ) /\ M e. NN ) /\ i e. ( 1 ..^ M ) ) ) -> -. ( P ` ( M - 1 ) ) < -oo )
163 143 162 pm2.21dd 
 |-  ( ( ( P ` M ) = -oo /\ ( ( ( ph /\ -. M = 1 ) /\ M e. NN ) /\ i e. ( 1 ..^ M ) ) ) -> ( P ` i ) < ( P ` M ) )
164 163 ex 
 |-  ( ( P ` M ) = -oo -> ( ( ( ( ph /\ -. M = 1 ) /\ M e. NN ) /\ i e. ( 1 ..^ M ) ) -> ( P ` i ) < ( P ` M ) ) )
165 126 132 164 3jaoi 
 |-  ( ( ( P ` M ) e. RR \/ ( P ` M ) = +oo \/ ( P ` M ) = -oo ) -> ( ( ( ( ph /\ -. M = 1 ) /\ M e. NN ) /\ i e. ( 1 ..^ M ) ) -> ( P ` i ) < ( P ` M ) ) )
166 165 impl 
 |-  ( ( ( ( ( P ` M ) e. RR \/ ( P ` M ) = +oo \/ ( P ` M ) = -oo ) /\ ( ( ph /\ -. M = 1 ) /\ M e. NN ) ) /\ i e. ( 1 ..^ M ) ) -> ( P ` i ) < ( P ` M ) )
167 166 ralrimiva 
 |-  ( ( ( ( P ` M ) e. RR \/ ( P ` M ) = +oo \/ ( P ` M ) = -oo ) /\ ( ( ph /\ -. M = 1 ) /\ M e. NN ) ) -> A. i e. ( 1 ..^ M ) ( P ` i ) < ( P ` M ) )
168 167 ex 
 |-  ( ( ( P ` M ) e. RR \/ ( P ` M ) = +oo \/ ( P ` M ) = -oo ) -> ( ( ( ph /\ -. M = 1 ) /\ M e. NN ) -> A. i e. ( 1 ..^ M ) ( P ` i ) < ( P ` M ) ) )
169 20 168 sylbi 
 |-  ( ( P ` M ) e. RR* -> ( ( ( ph /\ -. M = 1 ) /\ M e. NN ) -> A. i e. ( 1 ..^ M ) ( P ` i ) < ( P ` M ) ) )
170 19 169 mpcom 
 |-  ( ( ( ph /\ -. M = 1 ) /\ M e. NN ) -> A. i e. ( 1 ..^ M ) ( P ` i ) < ( P ` M ) )
171 170 ex 
 |-  ( ( ph /\ -. M = 1 ) -> ( M e. NN -> A. i e. ( 1 ..^ M ) ( P ` i ) < ( P ` M ) ) )
172 171 expcom 
 |-  ( -. M = 1 -> ( ph -> ( M e. NN -> A. i e. ( 1 ..^ M ) ( P ` i ) < ( P ` M ) ) ) )
173 11 172 pm2.61i 
 |-  ( ph -> ( M e. NN -> A. i e. ( 1 ..^ M ) ( P ` i ) < ( P ` M ) ) )
174 1 173 mpd 
 |-  ( ph -> A. i e. ( 1 ..^ M ) ( P ` i ) < ( P ` M ) )