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

Proof

Step Hyp Ref Expression
1 iccpartgtprec.m φ M
2 iccpartgtprec.p φ P RePart M
3 nnnn0 M M 0
4 elnn0uz M 0 M 0
5 3 4 sylib M M 0
6 1 5 syl φ M 0
7 fzisfzounsn M 0 0 M = 0 ..^ M M
8 6 7 syl φ 0 M = 0 ..^ M M
9 8 eleq2d φ i 0 M i 0 ..^ M M
10 elun i 0 ..^ M M i 0 ..^ M i M
11 10 a1i φ i 0 ..^ M M i 0 ..^ M i M
12 velsn i M i = M
13 12 a1i φ i M i = M
14 13 orbi2d φ i 0 ..^ M i M i 0 ..^ M i = M
15 9 11 14 3bitrd φ i 0 M i 0 ..^ M i = M
16 1 adantr φ i 0 ..^ M M
17 2 adantr φ i 0 ..^ M P RePart M
18 fzossfz 0 ..^ M 0 M
19 18 a1i φ 0 ..^ M 0 M
20 19 sselda φ i 0 ..^ M i 0 M
21 16 17 20 iccpartxr φ i 0 ..^ M P i *
22 nn0fz0 M 0 M 0 M
23 3 22 sylib M M 0 M
24 1 23 syl φ M 0 M
25 1 2 24 iccpartxr φ P M *
26 25 adantr φ i 0 ..^ M P M *
27 1 2 iccpartltu φ k 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 k 0 ..^ M P k < P M i 0 ..^ M P i < P M
31 27 30 syl φ i 0 ..^ M P i < P M
32 31 imp φ i 0 ..^ M P i < P M
33 21 26 32 xrltled φ i 0 ..^ M P i P M
34 33 expcom i 0 ..^ M φ P i P M
35 fveq2 i = M P i = P M
36 35 adantr i = M φ P i = P M
37 25 xrleidd φ P M P M
38 37 adantl i = M φ P M P M
39 36 38 eqbrtrd i = M φ P i P M
40 39 ex i = M φ P i P M
41 34 40 jaoi i 0 ..^ M i = M φ P i P M
42 41 com12 φ i 0 ..^ M i = M P i P M
43 15 42 sylbid φ i 0 M P i P M
44 43 ralrimiv φ i 0 M P i P M