Metamath Proof Explorer

Theorem iccpartigtl

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

Ref Expression
Hypotheses iccpartgtprec.m 
|- ( ph -> M e. NN )
iccpartgtprec.p 
|- ( ph -> P e. ( RePart ` M ) )
Assertion iccpartigtl 
|- ( ph -> A. i e. ( 1 ..^ 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 ral0 
 |-  A. i e. (/) ( P ` 0 ) < ( P ` i )
4 oveq2 
 |-  ( M = 1 -> ( 1 ..^ M ) = ( 1 ..^ 1 ) )
5 fzo0 
 |-  ( 1 ..^ 1 ) = (/)
6 4 5 eqtrdi 
 |-  ( M = 1 -> ( 1 ..^ M ) = (/) )
7 6 raleqdv 
 |-  ( M = 1 -> ( A. i e. ( 1 ..^ M ) ( P ` 0 ) < ( P ` i ) <-> A. i e. (/) ( P ` 0 ) < ( P ` i ) ) )
8 3 7 mpbiri 
 |-  ( M = 1 -> A. i e. ( 1 ..^ M ) ( P ` 0 ) < ( P ` i ) )
9 8 a1d 
 |-  ( M = 1 -> ( ph -> A. i e. ( 1 ..^ M ) ( P ` 0 ) < ( P ` i ) ) )
10 1 nnnn0d 
 |-  ( ph -> M e. NN0 )
11 0elfz 
 |-  ( M e. NN0 -> 0 e. ( 0 ... M ) )
12 10 11 syl 
 |-  ( ph -> 0 e. ( 0 ... M ) )
13 1 2 12 iccpartxr 
 |-  ( ph -> ( P ` 0 ) e. RR* )
14 13 adantr 
 |-  ( ( ph /\ -. M = 1 ) -> ( P ` 0 ) e. RR* )
15 elxr 
 |-  ( ( P ` 0 ) e. RR* <-> ( ( P ` 0 ) e. RR \/ ( P ` 0 ) = +oo \/ ( P ` 0 ) = -oo ) )
16 0zd 
 |-  ( ( ( ( P ` 0 ) e. RR /\ ( ph /\ -. M = 1 ) ) /\ i e. ( 1 ..^ M ) ) -> 0 e. ZZ )
17 elfzouz 
 |-  ( i e. ( 1 ..^ M ) -> i e. ( ZZ>= ` 1 ) )
18 0p1e1 
 |-  ( 0 + 1 ) = 1
19 18 fveq2i 
 |-  ( ZZ>= ` ( 0 + 1 ) ) = ( ZZ>= ` 1 )
20 17 19 eleqtrrdi 
 |-  ( i e. ( 1 ..^ M ) -> i e. ( ZZ>= ` ( 0 + 1 ) ) )
21 20 adantl 
 |-  ( ( ( ( P ` 0 ) e. RR /\ ( ph /\ -. M = 1 ) ) /\ i e. ( 1 ..^ M ) ) -> i e. ( ZZ>= ` ( 0 + 1 ) ) )
22 fveq2 
 |-  ( k = 0 -> ( P ` k ) = ( P ` 0 ) )
23 22 eqcomd 
 |-  ( k = 0 -> ( P ` 0 ) = ( P ` k ) )
24 23 eleq1d 
 |-  ( k = 0 -> ( ( P ` 0 ) e. RR <-> ( P ` k ) e. RR ) )
25 24 biimpcd 
 |-  ( ( P ` 0 ) e. RR -> ( k = 0 -> ( P ` k ) e. RR ) )
26 25 ad3antrrr 
 |-  ( ( ( ( ( P ` 0 ) e. RR /\ ( ph /\ -. M = 1 ) ) /\ i e. ( 1 ..^ M ) ) /\ k e. ( 0 ... i ) ) -> ( k = 0 -> ( P ` k ) e. RR ) )
27 1 adantr 
 |-  ( ( ph /\ ( i e. ( 1 ..^ M ) /\ ( k e. ( 0 ... i ) /\ k =/= 0 ) ) ) -> M e. NN )
28 2 adantr 
 |-  ( ( ph /\ ( i e. ( 1 ..^ M ) /\ ( k e. ( 0 ... i ) /\ k =/= 0 ) ) ) -> P e. ( RePart ` M ) )
29 elfz2nn0 
 |-  ( k e. ( 0 ... i ) <-> ( k e. NN0 /\ i e. NN0 /\ k <_ i ) )
30 elfzo2 
 |-  ( i e. ( 1 ..^ M ) <-> ( i e. ( ZZ>= ` 1 ) /\ M e. ZZ /\ i < M ) )
31 simpl1 
 |-  ( ( ( k e. NN0 /\ i e. NN0 /\ k <_ i ) /\ ( i e. ( ZZ>= ` 1 ) /\ M e. ZZ /\ i < M ) ) -> k e. NN0 )
32 simpr2 
 |-  ( ( ( k e. NN0 /\ i e. NN0 /\ k <_ i ) /\ ( i e. ( ZZ>= ` 1 ) /\ M e. ZZ /\ i < M ) ) -> M e. ZZ )
33 nn0ge0 
 |-  ( i e. NN0 -> 0 <_ i )
34 0red 
 |-  ( ( i e. ( ZZ>= ` 1 ) /\ M e. ZZ ) -> 0 e. RR )
35 eluzelre 
 |-  ( i e. ( ZZ>= ` 1 ) -> i e. RR )
36 35 adantr 
 |-  ( ( i e. ( ZZ>= ` 1 ) /\ M e. ZZ ) -> i e. RR )
37 zre 
 |-  ( M e. ZZ -> M e. RR )
38 37 adantl 
 |-  ( ( i e. ( ZZ>= ` 1 ) /\ M e. ZZ ) -> M e. RR )
39 lelttr 
 |-  ( ( 0 e. RR /\ i e. RR /\ M e. RR ) -> ( ( 0 <_ i /\ i < M ) -> 0 < M ) )
40 34 36 38 39 syl3anc 
 |-  ( ( i e. ( ZZ>= ` 1 ) /\ M e. ZZ ) -> ( ( 0 <_ i /\ i < M ) -> 0 < M ) )
41 40 expcomd 
 |-  ( ( i e. ( ZZ>= ` 1 ) /\ M e. ZZ ) -> ( i < M -> ( 0 <_ i -> 0 < M ) ) )
42 41 3impia 
 |-  ( ( i e. ( ZZ>= ` 1 ) /\ M e. ZZ /\ i < M ) -> ( 0 <_ i -> 0 < M ) )
43 33 42 syl5com 
 |-  ( i e. NN0 -> ( ( i e. ( ZZ>= ` 1 ) /\ M e. ZZ /\ i < M ) -> 0 < M ) )
44 43 3ad2ant2 
 |-  ( ( k e. NN0 /\ i e. NN0 /\ k <_ i ) -> ( ( i e. ( ZZ>= ` 1 ) /\ M e. ZZ /\ i < M ) -> 0 < M ) )
45 44 imp 
 |-  ( ( ( k e. NN0 /\ i e. NN0 /\ k <_ i ) /\ ( i e. ( ZZ>= ` 1 ) /\ M e. ZZ /\ i < M ) ) -> 0 < M )
46 elnnz 
 |-  ( M e. NN <-> ( M e. ZZ /\ 0 < M ) )
47 32 45 46 sylanbrc 
 |-  ( ( ( k e. NN0 /\ i e. NN0 /\ k <_ i ) /\ ( i e. ( ZZ>= ` 1 ) /\ M e. ZZ /\ i < M ) ) -> M e. NN )
48 nn0re 
 |-  ( k e. NN0 -> k e. RR )
49 48 ad2antrl 
 |-  ( ( ( i e. ( ZZ>= ` 1 ) /\ M e. ZZ ) /\ ( k e. NN0 /\ i e. NN0 ) ) -> k e. RR )
50 nn0re 
 |-  ( i e. NN0 -> i e. RR )
51 50 adantl 
 |-  ( ( k e. NN0 /\ i e. NN0 ) -> i e. RR )
52 51 adantl 
 |-  ( ( ( i e. ( ZZ>= ` 1 ) /\ M e. ZZ ) /\ ( k e. NN0 /\ i e. NN0 ) ) -> i e. RR )
53 38 adantr 
 |-  ( ( ( i e. ( ZZ>= ` 1 ) /\ M e. ZZ ) /\ ( k e. NN0 /\ i e. NN0 ) ) -> M e. RR )
54 lelttr 
 |-  ( ( k e. RR /\ i e. RR /\ M e. RR ) -> ( ( k <_ i /\ i < M ) -> k < M ) )
55 54 expd 
 |-  ( ( k e. RR /\ i e. RR /\ M e. RR ) -> ( k <_ i -> ( i < M -> k < M ) ) )
56 49 52 53 55 syl3anc 
 |-  ( ( ( i e. ( ZZ>= ` 1 ) /\ M e. ZZ ) /\ ( k e. NN0 /\ i e. NN0 ) ) -> ( k <_ i -> ( i < M -> k < M ) ) )
57 56 exp31 
 |-  ( i e. ( ZZ>= ` 1 ) -> ( M e. ZZ -> ( ( k e. NN0 /\ i e. NN0 ) -> ( k <_ i -> ( i < M -> k < M ) ) ) ) )
58 57 com34 
 |-  ( i e. ( ZZ>= ` 1 ) -> ( M e. ZZ -> ( k <_ i -> ( ( k e. NN0 /\ i e. NN0 ) -> ( i < M -> k < M ) ) ) ) )
59 58 com35 
 |-  ( i e. ( ZZ>= ` 1 ) -> ( M e. ZZ -> ( i < M -> ( ( k e. NN0 /\ i e. NN0 ) -> ( k <_ i -> k < M ) ) ) ) )
60 59 3imp 
 |-  ( ( i e. ( ZZ>= ` 1 ) /\ M e. ZZ /\ i < M ) -> ( ( k e. NN0 /\ i e. NN0 ) -> ( k <_ i -> k < M ) ) )
61 60 expdcom 
 |-  ( k e. NN0 -> ( i e. NN0 -> ( ( i e. ( ZZ>= ` 1 ) /\ M e. ZZ /\ i < M ) -> ( k <_ i -> k < M ) ) ) )
62 61 com34 
 |-  ( k e. NN0 -> ( i e. NN0 -> ( k <_ i -> ( ( i e. ( ZZ>= ` 1 ) /\ M e. ZZ /\ i < M ) -> k < M ) ) ) )
63 62 3imp1 
 |-  ( ( ( k e. NN0 /\ i e. NN0 /\ k <_ i ) /\ ( i e. ( ZZ>= ` 1 ) /\ M e. ZZ /\ i < M ) ) -> k < M )
64 elfzo0 
 |-  ( k e. ( 0 ..^ M ) <-> ( k e. NN0 /\ M e. NN /\ k < M ) )
65 31 47 63 64 syl3anbrc 
 |-  ( ( ( k e. NN0 /\ i e. NN0 /\ k <_ i ) /\ ( i e. ( ZZ>= ` 1 ) /\ M e. ZZ /\ i < M ) ) -> k e. ( 0 ..^ M ) )
66 65 ex 
 |-  ( ( k e. NN0 /\ i e. NN0 /\ k <_ i ) -> ( ( i e. ( ZZ>= ` 1 ) /\ M e. ZZ /\ i < M ) -> k e. ( 0 ..^ M ) ) )
67 30 66 syl5bi 
 |-  ( ( k e. NN0 /\ i e. NN0 /\ k <_ i ) -> ( i e. ( 1 ..^ M ) -> k e. ( 0 ..^ M ) ) )
68 29 67 sylbi 
 |-  ( k e. ( 0 ... i ) -> ( i e. ( 1 ..^ M ) -> k e. ( 0 ..^ M ) ) )
69 68 adantr 
 |-  ( ( k e. ( 0 ... i ) /\ k =/= 0 ) -> ( i e. ( 1 ..^ M ) -> k e. ( 0 ..^ M ) ) )
70 69 impcom 
 |-  ( ( i e. ( 1 ..^ M ) /\ ( k e. ( 0 ... i ) /\ k =/= 0 ) ) -> k e. ( 0 ..^ M ) )
71 simpr 
 |-  ( ( k e. ( 0 ... i ) /\ k =/= 0 ) -> k =/= 0 )
72 71 adantl 
 |-  ( ( i e. ( 1 ..^ M ) /\ ( k e. ( 0 ... i ) /\ k =/= 0 ) ) -> k =/= 0 )
73 fzo1fzo0n0 
 |-  ( k e. ( 1 ..^ M ) <-> ( k e. ( 0 ..^ M ) /\ k =/= 0 ) )
74 70 72 73 sylanbrc 
 |-  ( ( i e. ( 1 ..^ M ) /\ ( k e. ( 0 ... i ) /\ k =/= 0 ) ) -> k e. ( 1 ..^ M ) )
75 74 adantl 
 |-  ( ( ph /\ ( i e. ( 1 ..^ M ) /\ ( k e. ( 0 ... i ) /\ k =/= 0 ) ) ) -> k e. ( 1 ..^ M ) )
76 27 28 75 iccpartipre 
 |-  ( ( ph /\ ( i e. ( 1 ..^ M ) /\ ( k e. ( 0 ... i ) /\ k =/= 0 ) ) ) -> ( P ` k ) e. RR )
77 76 exp32 
 |-  ( ph -> ( i e. ( 1 ..^ M ) -> ( ( k e. ( 0 ... i ) /\ k =/= 0 ) -> ( P ` k ) e. RR ) ) )
78 77 ad2antrl 
 |-  ( ( ( P ` 0 ) e. RR /\ ( ph /\ -. M = 1 ) ) -> ( i e. ( 1 ..^ M ) -> ( ( k e. ( 0 ... i ) /\ k =/= 0 ) -> ( P ` k ) e. RR ) ) )
79 78 imp 
 |-  ( ( ( ( P ` 0 ) e. RR /\ ( ph /\ -. M = 1 ) ) /\ i e. ( 1 ..^ M ) ) -> ( ( k e. ( 0 ... i ) /\ k =/= 0 ) -> ( P ` k ) e. RR ) )
80 79 expdimp 
 |-  ( ( ( ( ( P ` 0 ) e. RR /\ ( ph /\ -. M = 1 ) ) /\ i e. ( 1 ..^ M ) ) /\ k e. ( 0 ... i ) ) -> ( k =/= 0 -> ( P ` k ) e. RR ) )
81 26 80 pm2.61dne 
 |-  ( ( ( ( ( P ` 0 ) e. RR /\ ( ph /\ -. M = 1 ) ) /\ i e. ( 1 ..^ M ) ) /\ k e. ( 0 ... i ) ) -> ( P ` k ) e. RR )
82 1 adantr 
 |-  ( ( ph /\ -. M = 1 ) -> M e. NN )
83 82 ad3antlr 
 |-  ( ( ( ( ( P ` 0 ) e. RR /\ ( ph /\ -. M = 1 ) ) /\ i e. ( 1 ..^ M ) ) /\ k e. ( 0 ... ( i - 1 ) ) ) -> M e. NN )
84 2 adantr 
 |-  ( ( ph /\ -. M = 1 ) -> P e. ( RePart ` M ) )
85 84 ad3antlr 
 |-  ( ( ( ( ( P ` 0 ) e. RR /\ ( ph /\ -. M = 1 ) ) /\ i e. ( 1 ..^ M ) ) /\ k e. ( 0 ... ( i - 1 ) ) ) -> P e. ( RePart ` M ) )
86 elfzoelz 
 |-  ( i e. ( 1 ..^ M ) -> i e. ZZ )
87 86 adantl 
 |-  ( ( ( ( P ` 0 ) e. RR /\ ( ph /\ -. M = 1 ) ) /\ i e. ( 1 ..^ M ) ) -> i e. ZZ )
88 fzoval 
 |-  ( i e. ZZ -> ( 0 ..^ i ) = ( 0 ... ( i - 1 ) ) )
89 88 eqcomd 
 |-  ( i e. ZZ -> ( 0 ... ( i - 1 ) ) = ( 0 ..^ i ) )
90 87 89 syl 
 |-  ( ( ( ( P ` 0 ) e. RR /\ ( ph /\ -. M = 1 ) ) /\ i e. ( 1 ..^ M ) ) -> ( 0 ... ( i - 1 ) ) = ( 0 ..^ i ) )
91 90 eleq2d 
 |-  ( ( ( ( P ` 0 ) e. RR /\ ( ph /\ -. M = 1 ) ) /\ i e. ( 1 ..^ M ) ) -> ( k e. ( 0 ... ( i - 1 ) ) <-> k e. ( 0 ..^ i ) ) )
92 elfzouz2 
 |-  ( i e. ( 1 ..^ M ) -> M e. ( ZZ>= ` i ) )
93 92 adantl 
 |-  ( ( ( ( P ` 0 ) e. RR /\ ( ph /\ -. M = 1 ) ) /\ i e. ( 1 ..^ M ) ) -> M e. ( ZZ>= ` i ) )
94 fzoss2 
 |-  ( M e. ( ZZ>= ` i ) -> ( 0 ..^ i ) C_ ( 0 ..^ M ) )
95 93 94 syl 
 |-  ( ( ( ( P ` 0 ) e. RR /\ ( ph /\ -. M = 1 ) ) /\ i e. ( 1 ..^ M ) ) -> ( 0 ..^ i ) C_ ( 0 ..^ M ) )
96 95 sseld 
 |-  ( ( ( ( P ` 0 ) e. RR /\ ( ph /\ -. M = 1 ) ) /\ i e. ( 1 ..^ M ) ) -> ( k e. ( 0 ..^ i ) -> k e. ( 0 ..^ M ) ) )
97 91 96 sylbid 
 |-  ( ( ( ( P ` 0 ) e. RR /\ ( ph /\ -. M = 1 ) ) /\ i e. ( 1 ..^ M ) ) -> ( k e. ( 0 ... ( i - 1 ) ) -> k e. ( 0 ..^ M ) ) )
98 97 imp 
 |-  ( ( ( ( ( P ` 0 ) e. RR /\ ( ph /\ -. M = 1 ) ) /\ i e. ( 1 ..^ M ) ) /\ k e. ( 0 ... ( i - 1 ) ) ) -> k e. ( 0 ..^ M ) )
99 iccpartimp 
 |-  ( ( M e. NN /\ P e. ( RePart ` M ) /\ k e. ( 0 ..^ M ) ) -> ( P e. ( RR* ^m ( 0 ... M ) ) /\ ( P ` k ) < ( P ` ( k + 1 ) ) ) )
100 83 85 98 99 syl3anc 
 |-  ( ( ( ( ( P ` 0 ) e. RR /\ ( ph /\ -. M = 1 ) ) /\ i e. ( 1 ..^ M ) ) /\ k e. ( 0 ... ( i - 1 ) ) ) -> ( P e. ( RR* ^m ( 0 ... M ) ) /\ ( P ` k ) < ( P ` ( k + 1 ) ) ) )
101 100 simprd 
 |-  ( ( ( ( ( P ` 0 ) e. RR /\ ( ph /\ -. M = 1 ) ) /\ i e. ( 1 ..^ M ) ) /\ k e. ( 0 ... ( i - 1 ) ) ) -> ( P ` k ) < ( P ` ( k + 1 ) ) )
102 16 21 81 101 smonoord 
 |-  ( ( ( ( P ` 0 ) e. RR /\ ( ph /\ -. M = 1 ) ) /\ i e. ( 1 ..^ M ) ) -> ( P ` 0 ) < ( P ` i ) )
103 102 ralrimiva 
 |-  ( ( ( P ` 0 ) e. RR /\ ( ph /\ -. M = 1 ) ) -> A. i e. ( 1 ..^ M ) ( P ` 0 ) < ( P ` i ) )
104 103 ex 
 |-  ( ( P ` 0 ) e. RR -> ( ( ph /\ -. M = 1 ) -> A. i e. ( 1 ..^ M ) ( P ` 0 ) < ( P ` i ) ) )
105 lbfzo0 
 |-  ( 0 e. ( 0 ..^ M ) <-> M e. NN )
106 1 105 sylibr 
 |-  ( ph -> 0 e. ( 0 ..^ M ) )
107 1 2 106 3jca 
 |-  ( ph -> ( M e. NN /\ P e. ( RePart ` M ) /\ 0 e. ( 0 ..^ M ) ) )
108 107 ad2antrl 
 |-  ( ( ( P ` 0 ) = +oo /\ ( ph /\ -. M = 1 ) ) -> ( M e. NN /\ P e. ( RePart ` M ) /\ 0 e. ( 0 ..^ M ) ) )
109 108 adantr 
 |-  ( ( ( ( P ` 0 ) = +oo /\ ( ph /\ -. M = 1 ) ) /\ i e. ( 1 ..^ M ) ) -> ( M e. NN /\ P e. ( RePart ` M ) /\ 0 e. ( 0 ..^ M ) ) )
110 iccpartimp 
 |-  ( ( M e. NN /\ P e. ( RePart ` M ) /\ 0 e. ( 0 ..^ M ) ) -> ( P e. ( RR* ^m ( 0 ... M ) ) /\ ( P ` 0 ) < ( P ` ( 0 + 1 ) ) ) )
111 109 110 syl 
 |-  ( ( ( ( P ` 0 ) = +oo /\ ( ph /\ -. M = 1 ) ) /\ i e. ( 1 ..^ M ) ) -> ( P e. ( RR* ^m ( 0 ... M ) ) /\ ( P ` 0 ) < ( P ` ( 0 + 1 ) ) ) )
112 111 simprd 
 |-  ( ( ( ( P ` 0 ) = +oo /\ ( ph /\ -. M = 1 ) ) /\ i e. ( 1 ..^ M ) ) -> ( P ` 0 ) < ( P ` ( 0 + 1 ) ) )
113 breq1 
 |-  ( ( P ` 0 ) = +oo -> ( ( P ` 0 ) < ( P ` ( 0 + 1 ) ) <-> +oo < ( P ` ( 0 + 1 ) ) ) )
114 113 adantr 
 |-  ( ( ( P ` 0 ) = +oo /\ ( ph /\ -. M = 1 ) ) -> ( ( P ` 0 ) < ( P ` ( 0 + 1 ) ) <-> +oo < ( P ` ( 0 + 1 ) ) ) )
115 114 adantr 
 |-  ( ( ( ( P ` 0 ) = +oo /\ ( ph /\ -. M = 1 ) ) /\ i e. ( 1 ..^ M ) ) -> ( ( P ` 0 ) < ( P ` ( 0 + 1 ) ) <-> +oo < ( P ` ( 0 + 1 ) ) ) )
116 112 115 mpbid 
 |-  ( ( ( ( P ` 0 ) = +oo /\ ( ph /\ -. M = 1 ) ) /\ i e. ( 1 ..^ M ) ) -> +oo < ( P ` ( 0 + 1 ) ) )
117 1 ad2antrl 
 |-  ( ( ( P ` 0 ) = +oo /\ ( ph /\ -. M = 1 ) ) -> M e. NN )
118 117 adantr 
 |-  ( ( ( ( P ` 0 ) = +oo /\ ( ph /\ -. M = 1 ) ) /\ i e. ( 1 ..^ M ) ) -> M e. NN )
119 2 ad2antrl 
 |-  ( ( ( P ` 0 ) = +oo /\ ( ph /\ -. M = 1 ) ) -> P e. ( RePart ` M ) )
120 119 adantr 
 |-  ( ( ( ( P ` 0 ) = +oo /\ ( ph /\ -. M = 1 ) ) /\ i e. ( 1 ..^ M ) ) -> P e. ( RePart ` M ) )
121 1nn0 
 |-  1 e. NN0
122 121 a1i 
 |-  ( M e. NN -> 1 e. NN0 )
123 nnnn0 
 |-  ( M e. NN -> M e. NN0 )
124 nnge1 
 |-  ( M e. NN -> 1 <_ M )
125 122 123 124 3jca 
 |-  ( M e. NN -> ( 1 e. NN0 /\ M e. NN0 /\ 1 <_ M ) )
126 1 125 syl 
 |-  ( ph -> ( 1 e. NN0 /\ M e. NN0 /\ 1 <_ M ) )
127 elfz2nn0 
 |-  ( 1 e. ( 0 ... M ) <-> ( 1 e. NN0 /\ M e. NN0 /\ 1 <_ M ) )
128 126 127 sylibr 
 |-  ( ph -> 1 e. ( 0 ... M ) )
129 18 128 eqeltrid 
 |-  ( ph -> ( 0 + 1 ) e. ( 0 ... M ) )
130 129 ad2antrl 
 |-  ( ( ( P ` 0 ) = +oo /\ ( ph /\ -. M = 1 ) ) -> ( 0 + 1 ) e. ( 0 ... M ) )
131 130 adantr 
 |-  ( ( ( ( P ` 0 ) = +oo /\ ( ph /\ -. M = 1 ) ) /\ i e. ( 1 ..^ M ) ) -> ( 0 + 1 ) e. ( 0 ... M ) )
132 118 120 131 iccpartxr 
 |-  ( ( ( ( P ` 0 ) = +oo /\ ( ph /\ -. M = 1 ) ) /\ i e. ( 1 ..^ M ) ) -> ( P ` ( 0 + 1 ) ) e. RR* )
133 pnfnlt 
 |-  ( ( P ` ( 0 + 1 ) ) e. RR* -> -. +oo < ( P ` ( 0 + 1 ) ) )
134 132 133 syl 
 |-  ( ( ( ( P ` 0 ) = +oo /\ ( ph /\ -. M = 1 ) ) /\ i e. ( 1 ..^ M ) ) -> -. +oo < ( P ` ( 0 + 1 ) ) )
135 116 134 pm2.21dd 
 |-  ( ( ( ( P ` 0 ) = +oo /\ ( ph /\ -. M = 1 ) ) /\ i e. ( 1 ..^ M ) ) -> ( P ` 0 ) < ( P ` i ) )
136 135 ralrimiva 
 |-  ( ( ( P ` 0 ) = +oo /\ ( ph /\ -. M = 1 ) ) -> A. i e. ( 1 ..^ M ) ( P ` 0 ) < ( P ` i ) )
137 136 ex 
 |-  ( ( P ` 0 ) = +oo -> ( ( ph /\ -. M = 1 ) -> A. i e. ( 1 ..^ M ) ( P ` 0 ) < ( P ` i ) ) )
138 1 adantr 
 |-  ( ( ph /\ i e. ( 1 ..^ M ) ) -> M e. NN )
139 2 adantr 
 |-  ( ( ph /\ i e. ( 1 ..^ M ) ) -> P e. ( RePart ` M ) )
140 simpr 
 |-  ( ( ph /\ i e. ( 1 ..^ M ) ) -> i e. ( 1 ..^ M ) )
141 138 139 140 iccpartipre 
 |-  ( ( ph /\ i e. ( 1 ..^ M ) ) -> ( P ` i ) e. RR )
142 mnflt 
 |-  ( ( P ` i ) e. RR -> -oo < ( P ` i ) )
143 141 142 syl 
 |-  ( ( ph /\ i e. ( 1 ..^ M ) ) -> -oo < ( P ` i ) )
144 143 ralrimiva 
 |-  ( ph -> A. i e. ( 1 ..^ M ) -oo < ( P ` i ) )
145 144 ad2antrl 
 |-  ( ( ( P ` 0 ) = -oo /\ ( ph /\ -. M = 1 ) ) -> A. i e. ( 1 ..^ M ) -oo < ( P ` i ) )
146 breq1 
 |-  ( ( P ` 0 ) = -oo -> ( ( P ` 0 ) < ( P ` i ) <-> -oo < ( P ` i ) ) )
147 146 adantr 
 |-  ( ( ( P ` 0 ) = -oo /\ ( ph /\ -. M = 1 ) ) -> ( ( P ` 0 ) < ( P ` i ) <-> -oo < ( P ` i ) ) )
148 147 ralbidv 
 |-  ( ( ( P ` 0 ) = -oo /\ ( ph /\ -. M = 1 ) ) -> ( A. i e. ( 1 ..^ M ) ( P ` 0 ) < ( P ` i ) <-> A. i e. ( 1 ..^ M ) -oo < ( P ` i ) ) )
149 145 148 mpbird 
 |-  ( ( ( P ` 0 ) = -oo /\ ( ph /\ -. M = 1 ) ) -> A. i e. ( 1 ..^ M ) ( P ` 0 ) < ( P ` i ) )
150 149 ex 
 |-  ( ( P ` 0 ) = -oo -> ( ( ph /\ -. M = 1 ) -> A. i e. ( 1 ..^ M ) ( P ` 0 ) < ( P ` i ) ) )
151 104 137 150 3jaoi 
 |-  ( ( ( P ` 0 ) e. RR \/ ( P ` 0 ) = +oo \/ ( P ` 0 ) = -oo ) -> ( ( ph /\ -. M = 1 ) -> A. i e. ( 1 ..^ M ) ( P ` 0 ) < ( P ` i ) ) )
152 15 151 sylbi 
 |-  ( ( P ` 0 ) e. RR* -> ( ( ph /\ -. M = 1 ) -> A. i e. ( 1 ..^ M ) ( P ` 0 ) < ( P ` i ) ) )
153 14 152 mpcom 
 |-  ( ( ph /\ -. M = 1 ) -> A. i e. ( 1 ..^ M ) ( P ` 0 ) < ( P ` i ) )
154 153 expcom 
 |-  ( -. M = 1 -> ( ph -> A. i e. ( 1 ..^ M ) ( P ` 0 ) < ( P ` i ) ) )
155 9 154 pm2.61i 
 |-  ( ph -> A. i e. ( 1 ..^ M ) ( P ` 0 ) < ( P ` i ) )