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

Metamath Proof Explorer

Theorem iccpartxr

Description: If there is a partition, then all intermediate points and bounds are extended real numbers. (Contributed by AV, 11-Jul-2020)

Ref Expression
Hypotheses iccpartgtprec.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
iccpartgtprec.p ⊢ ( 𝜑 → 𝑃 ∈ ( RePart ‘ 𝑀 ) )
iccpartxr.i ⊢ ( 𝜑 → 𝐼 ∈ ( 0 ... 𝑀 ) )
Assertion iccpartxr ( 𝜑 → ( 𝑃 ‘ 𝐼 ) ∈ ℝ* )

Proof

Step Hyp Ref Expression
1 iccpartgtprec.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
2 iccpartgtprec.p ⊢ ( 𝜑 → 𝑃 ∈ ( RePart ‘ 𝑀 ) )
3 iccpartxr.i ⊢ ( 𝜑 → 𝐼 ∈ ( 0 ... 𝑀 ) )
4 iccpart ⊢ ( 𝑀 ∈ ℕ → ( 𝑃 ∈ ( RePart ‘ 𝑀 ) ↔ ( 𝑃 ∈ ( ℝ* ↑m ( 0 ... 𝑀 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) ) )
5 1 4 syl ⊢ ( 𝜑 → ( 𝑃 ∈ ( RePart ‘ 𝑀 ) ↔ ( 𝑃 ∈ ( ℝ* ↑m ( 0 ... 𝑀 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) ) )
6 2 5 mpbid ⊢ ( 𝜑 → ( 𝑃 ∈ ( ℝ* ↑m ( 0 ... 𝑀 ) ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑃 ‘ 𝑖 ) < ( 𝑃 ‘ ( 𝑖 + 1 ) ) ) )
7 6 simpld ⊢ ( 𝜑 → 𝑃 ∈ ( ℝ* ↑m ( 0 ... 𝑀 ) ) )
8 elmapi ⊢ ( 𝑃 ∈ ( ℝ* ↑m ( 0 ... 𝑀 ) ) → 𝑃 : ( 0 ... 𝑀 ) ⟶ ℝ* )
9 7 8 syl ⊢ ( 𝜑 → 𝑃 : ( 0 ... 𝑀 ) ⟶ ℝ* )
10 9 3 ffvelcdmd ⊢ ( 𝜑 → ( 𝑃 ‘ 𝐼 ) ∈ ℝ* )