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

Metamath Proof Explorer

Theorem iccpartf

Description: The range of the partition is between its starting point and its ending point. Corresponds to fourierdlem15 in GS's mathbox. (Contributed by Glauco Siliprandi, 11-Dec-2019) (Revised by AV, 14-Jul-2020)

Ref Expression
Hypotheses iccpartgtprec.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
iccpartgtprec.p ⊢ ( 𝜑 → 𝑃 ∈ ( RePart ‘ 𝑀 ) )
Assertion iccpartf ( 𝜑 → 𝑃 : ( 0 ... 𝑀 ) ⟶ ( ( 𝑃 ‘ 0 ) [,] ( 𝑃 ‘ 𝑀 ) ) )

Proof

Step Hyp Ref Expression
1 iccpartgtprec.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
2 iccpartgtprec.p ⊢ ( 𝜑 → 𝑃 ∈ ( RePart ‘ 𝑀 ) )
3 iccpart ⊢ ( 𝑀 ∈ ℕ → ( 𝑃 ∈ ( RePart ‘ 𝑀 ) ↔ ( 𝑃 ∈ ( ℝ* ↑m ( 0 ... 𝑀 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) ) )
4 elmapfn ⊢ ( 𝑃 ∈ ( ℝ* ↑m ( 0 ... 𝑀 ) ) → 𝑃 Fn ( 0 ... 𝑀 ) )
5 4 adantr ⊢ ( ( 𝑃 ∈ ( ℝ* ↑m ( 0 ... 𝑀 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) → 𝑃 Fn ( 0 ... 𝑀 ) )
6 3 5 biimtrdi ⊢ ( 𝑀 ∈ ℕ → ( 𝑃 ∈ ( RePart ‘ 𝑀 ) → 𝑃 Fn ( 0 ... 𝑀 ) ) )
7 1 2 6 sylc ⊢ ( 𝜑 → 𝑃 Fn ( 0 ... 𝑀 ) )
8 1 2 iccpartrn ⊢ ( 𝜑 → ran 𝑃 ⊆ ( ( 𝑃 ‘ 0 ) [,] ( 𝑃 ‘ 𝑀 ) ) )
9 df-f ⊢ ( 𝑃 : ( 0 ... 𝑀 ) ⟶ ( ( 𝑃 ‘ 0 ) [,] ( 𝑃 ‘ 𝑀 ) ) ↔ ( 𝑃 Fn ( 0 ... 𝑀 ) ∧ ran 𝑃 ⊆ ( ( 𝑃 ‘ 0 ) [,] ( 𝑃 ‘ 𝑀 ) ) ) )
10 7 8 9 sylanbrc ⊢ ( 𝜑 → 𝑃 : ( 0 ... 𝑀 ) ⟶ ( ( 𝑃 ‘ 0 ) [,] ( 𝑃 ‘ 𝑀 ) ) )