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