# 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}\in ℕ\to \left({P}\in \mathrm{RePart}\left({M}\right)↔\left({P}\in \left({{ℝ}^{*}}^{\left(0\dots {M}\right)}\right)\wedge \forall {i}\in \left(0..^{M}\right)\phantom{\rule{.4em}{0ex}}{P}\left({i}\right)<{P}\left({i}+1\right)\right)\right)$

### Proof

Step Hyp Ref Expression
1 iccpval ${⊢}{M}\in ℕ\to \mathrm{RePart}\left({M}\right)=\left\{{p}\in \left({{ℝ}^{*}}^{\left(0\dots {M}\right)}\right)|\forall {i}\in \left(0..^{M}\right)\phantom{\rule{.4em}{0ex}}{p}\left({i}\right)<{p}\left({i}+1\right)\right\}$
2 1 eleq2d ${⊢}{M}\in ℕ\to \left({P}\in \mathrm{RePart}\left({M}\right)↔{P}\in \left\{{p}\in \left({{ℝ}^{*}}^{\left(0\dots {M}\right)}\right)|\forall {i}\in \left(0..^{M}\right)\phantom{\rule{.4em}{0ex}}{p}\left({i}\right)<{p}\left({i}+1\right)\right\}\right)$
3 fveq1 ${⊢}{p}={P}\to {p}\left({i}\right)={P}\left({i}\right)$
4 fveq1 ${⊢}{p}={P}\to {p}\left({i}+1\right)={P}\left({i}+1\right)$
5 3 4 breq12d ${⊢}{p}={P}\to \left({p}\left({i}\right)<{p}\left({i}+1\right)↔{P}\left({i}\right)<{P}\left({i}+1\right)\right)$
6 5 ralbidv ${⊢}{p}={P}\to \left(\forall {i}\in \left(0..^{M}\right)\phantom{\rule{.4em}{0ex}}{p}\left({i}\right)<{p}\left({i}+1\right)↔\forall {i}\in \left(0..^{M}\right)\phantom{\rule{.4em}{0ex}}{P}\left({i}\right)<{P}\left({i}+1\right)\right)$
7 6 elrab ${⊢}{P}\in \left\{{p}\in \left({{ℝ}^{*}}^{\left(0\dots {M}\right)}\right)|\forall {i}\in \left(0..^{M}\right)\phantom{\rule{.4em}{0ex}}{p}\left({i}\right)<{p}\left({i}+1\right)\right\}↔\left({P}\in \left({{ℝ}^{*}}^{\left(0\dots {M}\right)}\right)\wedge \forall {i}\in \left(0..^{M}\right)\phantom{\rule{.4em}{0ex}}{P}\left({i}\right)<{P}\left({i}+1\right)\right)$
8 2 7 syl6bb ${⊢}{M}\in ℕ\to \left({P}\in \mathrm{RePart}\left({M}\right)↔\left({P}\in \left({{ℝ}^{*}}^{\left(0\dots {M}\right)}\right)\wedge \forall {i}\in \left(0..^{M}\right)\phantom{\rule{.4em}{0ex}}{P}\left({i}\right)<{P}\left({i}+1\right)\right)\right)$