This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝑀 ∈ ℕ → ( 𝑃 ∈ ( RePart ‘ 𝑀 ) ↔ ( 𝑃 ∈ ( ℝ* ↑m ( 0 ... 𝑀 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 iccpval ⊢ ( 𝑀 ∈ ℕ → ( RePart ‘ 𝑀 ) = { 𝑝 ∈ ( ℝ* ↑m ( 0 ... 𝑀 ) ) ∣ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) } )
2 1 eleq2d ⊢ ( 𝑀 ∈ ℕ → ( 𝑃 ∈ ( RePart ‘ 𝑀 ) ↔ 𝑃 ∈ { 𝑝 ∈ ( ℝ* ↑m ( 0 ... 𝑀 ) ) ∣ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) } ) )
3 fveq1 ⊢ ( 𝑝 = 𝑃 → ( 𝑝 ‘ 𝑖 ) = ( 𝑃 ‘ 𝑖 ) )
4 fveq1 ⊢ ( 𝑝 = 𝑃 → ( 𝑝 ‘ ( 𝑖 + 1 ) ) = ( 𝑃 ‘ ( 𝑖 + 1 ) ) )
5 3 4 breq12d ⊢ ( 𝑝 = 𝑃 → ( ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ↔ ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) )
6 5 ralbidv ⊢ ( 𝑝 = 𝑃 → ( ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ↔ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) )
7 6 elrab ⊢ ( 𝑃 ∈ { 𝑝 ∈ ( ℝ* ↑m ( 0 ... 𝑀 ) ) ∣ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) } ↔ ( 𝑃 ∈ ( ℝ* ↑m ( 0 ... 𝑀 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) )
8 2 7 bitrdi ⊢ ( 𝑀 ∈ ℕ → ( 𝑃 ∈ ( RePart ‘ 𝑀 ) ↔ ( 𝑃 ∈ ( ℝ* ↑m ( 0 ... 𝑀 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) ) )