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..^MP⁡i<P⁡i+1

Proof

Step Hyp Ref Expression
1 iccpval ⊢M∈ℕ→RePart⁡M=p∈ℝ*0…M|∀i∈0..^Mp⁡i<p⁡i+1
2 1 eleq2d ⊢M∈ℕ→P∈RePart⁡M↔P∈p∈ℝ*0…M|∀i∈0..^Mp⁡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..^Mp⁡i<p⁡i+1↔∀i∈0..^MP⁡i<P⁡i+1
7 6 elrab ⊢P∈p∈ℝ*0…M|∀i∈0..^Mp⁡i<p⁡i+1↔P∈ℝ*0…M∧∀i∈0..^MP⁡i<P⁡i+1
8 2 7 bitrdi ⊢M∈ℕ→P∈RePart⁡M↔P∈ℝ*0…M∧∀i∈0..^MP⁡i<P⁡i+1