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	ffvelrnd	⊢ ( 𝜑 → ( 𝑃 ‘ 𝐼 ) ∈ ℝ* )