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 ⊢ φ → M ∈ ℕ
iccpartgtprec.p ⊢ φ → P ∈ RePart ⁡ M
iccpartxr.i ⊢ φ → I ∈ 0 … M
Assertion iccpartxr ⊢ φ → P ⁡ I ∈ ℝ *

Proof

Step Hyp Ref Expression
1 iccpartgtprec.m ⊢ φ → M ∈ ℕ
2 iccpartgtprec.p ⊢ φ → P ∈ RePart ⁡ M
3 iccpartxr.i ⊢ φ → I ∈ 0 … M
4 iccpart ⊢ M ∈ ℕ → P ∈ RePart ⁡ M ↔ P ∈ ℝ * 0 … M ∧ ∀ i ∈ 0 ..^ M P ⁡ i < P ⁡ i + 1
5 1 4 syl ⊢ φ → P ∈ RePart ⁡ M ↔ P ∈ ℝ * 0 … M ∧ ∀ i ∈ 0 ..^ M P ⁡ i < P ⁡ i + 1
6 2 5 mpbid ⊢ φ → P ∈ ℝ * 0 … M ∧ ∀ i ∈ 0 ..^ M P ⁡ i < P ⁡ i + 1
7 6 simpld ⊢ φ → P ∈ ℝ * 0 … M
8 elmapi ⊢ P ∈ ℝ * 0 … M → P : 0 … M ⟶ ℝ *
9 7 8 syl ⊢ φ → P : 0 … M ⟶ ℝ *
10 9 3 ffvelcdmd ⊢ φ → P ⁡ I ∈ ℝ *