Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Alexander van der Vekens
Partitions of real intervals
iccpval
Next ⟩
iccpart
Metamath Proof Explorer
Ascii
Unicode
Theorem
iccpval
Description:
Partition consisting of a fixed number
M
of parts.
(Contributed by
AV
, 9-Jul-2020)
Ref
Expression
Assertion
iccpval
⊢
M
∈
ℕ
→
RePart
⁡
M
=
p
∈
ℝ
*
0
…
M
|
∀
i
∈
0
..^
M
p
⁡
i
<
p
⁡
i
+
1
Proof
Step
Hyp
Ref
Expression
1
oveq2
⊢
m
=
M
→
0
…
m
=
0
…
M
2
1
oveq2d
⊢
m
=
M
→
ℝ
*
0
…
m
=
ℝ
*
0
…
M
3
oveq2
⊢
m
=
M
→
0
..^
m
=
0
..^
M
4
3
raleqdv
⊢
m
=
M
→
∀
i
∈
0
..^
m
p
⁡
i
<
p
⁡
i
+
1
↔
∀
i
∈
0
..^
M
p
⁡
i
<
p
⁡
i
+
1
5
2
4
rabeqbidv
⊢
m
=
M
→
p
∈
ℝ
*
0
…
m
|
∀
i
∈
0
..^
m
p
⁡
i
<
p
⁡
i
+
1
=
p
∈
ℝ
*
0
…
M
|
∀
i
∈
0
..^
M
p
⁡
i
<
p
⁡
i
+
1
6
df-iccp
⊢
RePart
=
m
∈
ℕ
⟼
p
∈
ℝ
*
0
…
m
|
∀
i
∈
0
..^
m
p
⁡
i
<
p
⁡
i
+
1
7
ovex
⊢
ℝ
*
0
…
M
∈
V
8
7
rabex
⊢
p
∈
ℝ
*
0
…
M
|
∀
i
∈
0
..^
M
p
⁡
i
<
p
⁡
i
+
1
∈
V
9
5
6
8
fvmpt
⊢
M
∈
ℕ
→
RePart
⁡
M
=
p
∈
ℝ
*
0
…
M
|
∀
i
∈
0
..^
M
p
⁡
i
<
p
⁡
i
+
1