Metamath Proof Explorer

Definition df-iccp

Description: Define partitions of a closed interval of extended reals. Such partitions are finite increasing sequences of extended reals. (Contributed by AV, 8-Jul-2020)

Ref Expression
Assertion df-iccp ⊢ RePart = m ∈ ℕ ⟼ p ∈ ℝ * 0 … m | ∀ i ∈ 0 ..^ m p ⁡ i < p ⁡ i + 1

Detailed syntax breakdown

Step Hyp Ref Expression
0 ciccp class RePart
1 vm setvar m
2 cn class ℕ
3 vp setvar p
4 cxr class ℝ *
5 cmap class ↑ 𝑚
6 cc0 class 0
7 cfz class …
8 1 cv setvar m
9 6 8 7 co class 0 … m
10 4 9 5 co class ℝ * 0 … m
11 vi setvar i
12 cfzo class ..^
13 6 8 12 co class 0 ..^ m
14 3 cv setvar p
15 11 cv setvar i
16 15 14 cfv class p ⁡ i
17 clt class <
18 caddc class +
19 c1 class 1
20 15 19 18 co class i + 1
21 20 14 cfv class p ⁡ i + 1
22 16 21 17 wbr wff p ⁡ i < p ⁡ i + 1
23 22 11 13 wral wff ∀ i ∈ 0 ..^ m p ⁡ i < p ⁡ i + 1
24 23 3 10 crab class p ∈ ℝ * 0 … m | ∀ i ∈ 0 ..^ m p ⁡ i < p ⁡ i + 1
25 1 2 24 cmpt class m ∈ ℕ ⟼ p ∈ ℝ * 0 … m | ∀ i ∈ 0 ..^ m p ⁡ i < p ⁡ i + 1
26 0 25 wceq wff RePart = m ∈ ℕ ⟼ p ∈ ℝ * 0 … m | ∀ i ∈ 0 ..^ m p ⁡ i < p ⁡ i + 1