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 φ M
iccpartgtprec.p φ P RePart M
Assertion iccpartigtl φ i 1 ..^ M P 0 < P i

Proof

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