Metamath Proof Explorer


Theorem iccpart

Description: A special partition. Corresponds to fourierdlem2 in GS's mathbox. (Contributed by AV, 9-Jul-2020)

Ref Expression
Assertion iccpart M P RePart M P * 0 M i 0 ..^ M P i < P i + 1

Proof

Step Hyp Ref Expression
1 iccpval M RePart M = p * 0 M | i 0 ..^ M p i < p i + 1
2 1 eleq2d M P RePart M P p * 0 M | i 0 ..^ M p i < p i + 1
3 fveq1 p = P p i = P i
4 fveq1 p = P p i + 1 = P i + 1
5 3 4 breq12d p = P p i < p i + 1 P i < P i + 1
6 5 ralbidv p = P i 0 ..^ M p i < p i + 1 i 0 ..^ M P i < P i + 1
7 6 elrab P p * 0 M | i 0 ..^ M p i < p i + 1 P * 0 M i 0 ..^ M P i < P i + 1
8 2 7 bitrdi M P RePart M P * 0 M i 0 ..^ M P i < P i + 1