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