Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Alexander van der Vekens
Partitions of real intervals
iccpartimp
Next ⟩
iccpartres
Metamath Proof Explorer
Ascii
Unicode
Theorem
iccpartimp
Description:
Implications for a class being a partition.
(Contributed by
AV
, 11-Jul-2020)
Ref
Expression
Assertion
iccpartimp
⊢
M
∈
ℕ
∧
P
∈
RePart
⁡
M
∧
I
∈
0
..^
M
→
P
∈
ℝ
*
0
…
M
∧
P
⁡
I
<
P
⁡
I
+
1
Proof
Step
Hyp
Ref
Expression
1
iccpart
⊢
M
∈
ℕ
→
P
∈
RePart
⁡
M
↔
P
∈
ℝ
*
0
…
M
∧
∀
i
∈
0
..^
M
P
⁡
i
<
P
⁡
i
+
1
2
fveq2
⊢
i
=
I
→
P
⁡
i
=
P
⁡
I
3
fvoveq1
⊢
i
=
I
→
P
⁡
i
+
1
=
P
⁡
I
+
1
4
2
3
breq12d
⊢
i
=
I
→
P
⁡
i
<
P
⁡
i
+
1
↔
P
⁡
I
<
P
⁡
I
+
1
5
4
rspccv
⊢
∀
i
∈
0
..^
M
P
⁡
i
<
P
⁡
i
+
1
→
I
∈
0
..^
M
→
P
⁡
I
<
P
⁡
I
+
1
6
5
adantl
⊢
P
∈
ℝ
*
0
…
M
∧
∀
i
∈
0
..^
M
P
⁡
i
<
P
⁡
i
+
1
→
I
∈
0
..^
M
→
P
⁡
I
<
P
⁡
I
+
1
7
simpl
⊢
P
∈
ℝ
*
0
…
M
∧
∀
i
∈
0
..^
M
P
⁡
i
<
P
⁡
i
+
1
→
P
∈
ℝ
*
0
…
M
8
6
7
jctild
⊢
P
∈
ℝ
*
0
…
M
∧
∀
i
∈
0
..^
M
P
⁡
i
<
P
⁡
i
+
1
→
I
∈
0
..^
M
→
P
∈
ℝ
*
0
…
M
∧
P
⁡
I
<
P
⁡
I
+
1
9
1
8
syl6bi
⊢
M
∈
ℕ
→
P
∈
RePart
⁡
M
→
I
∈
0
..^
M
→
P
∈
ℝ
*
0
…
M
∧
P
⁡
I
<
P
⁡
I
+
1
10
9
3imp
⊢
M
∈
ℕ
∧
P
∈
RePart
⁡
M
∧
I
∈
0
..^
M
→
P
∈
ℝ
*
0
…
M
∧
P
⁡
I
<
P
⁡
I
+
1