Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Thierry Arnoux
Descartes's rule of signs
Counting sign changes in a word over real numbers
signshnz
Next ⟩
Sign changes in a polynomial with real coefficients
Metamath Proof Explorer
Ascii
Unicode
Theorem
signshnz
Description:
H
is not the empty word.
(Contributed by
Thierry Arnoux
, 14-Oct-2018)
Ref
Expression
Hypotheses
signsv.p
⊢
⨣
˙
=
a
∈
−
1
0
1
,
b
∈
−
1
0
1
⟼
if
b
=
0
a
b
signsv.w
⊢
W
=
Base
ndx
−
1
0
1
+
ndx
⨣
˙
signsv.t
⊢
T
=
f
∈
Word
ℝ
⟼
n
∈
0
..^
f
⟼
∑
W
i
=
0
n
sgn
⁡
f
⁡
i
signsv.v
⊢
V
=
f
∈
Word
ℝ
⟼
∑
j
∈
1
..^
f
if
T
⁡
f
⁡
j
≠
T
⁡
f
⁡
j
−
1
1
0
signs.h
⊢
H
=
〈“
0
”〉
++
F
−
f
F
++
〈“
0
”〉
∘
fc
⁡
×
C
Assertion
signshnz
⊢
F
∈
Word
ℝ
∧
C
∈
ℝ
+
→
H
≠
∅
Proof
Step
Hyp
Ref
Expression
1
signsv.p
⊢
⨣
˙
=
a
∈
−
1
0
1
,
b
∈
−
1
0
1
⟼
if
b
=
0
a
b
2
signsv.w
⊢
W
=
Base
ndx
−
1
0
1
+
ndx
⨣
˙
3
signsv.t
⊢
T
=
f
∈
Word
ℝ
⟼
n
∈
0
..^
f
⟼
∑
W
i
=
0
n
sgn
⁡
f
⁡
i
4
signsv.v
⊢
V
=
f
∈
Word
ℝ
⟼
∑
j
∈
1
..^
f
if
T
⁡
f
⁡
j
≠
T
⁡
f
⁡
j
−
1
1
0
5
signs.h
⊢
H
=
〈“
0
”〉
++
F
−
f
F
++
〈“
0
”〉
∘
fc
⁡
×
C
6
1
2
3
4
5
signshlen
⊢
F
∈
Word
ℝ
∧
C
∈
ℝ
+
→
H
=
F
+
1
7
lencl
⊢
F
∈
Word
ℝ
→
F
∈
ℕ
0
8
7
adantr
⊢
F
∈
Word
ℝ
∧
C
∈
ℝ
+
→
F
∈
ℕ
0
9
nn0p1nn
⊢
F
∈
ℕ
0
→
F
+
1
∈
ℕ
10
8
9
syl
⊢
F
∈
Word
ℝ
∧
C
∈
ℝ
+
→
F
+
1
∈
ℕ
11
6
10
eqeltrd
⊢
F
∈
Word
ℝ
∧
C
∈
ℝ
+
→
H
∈
ℕ
12
11
nnne0d
⊢
F
∈
Word
ℝ
∧
C
∈
ℝ
+
→
H
≠
0
13
1
2
3
4
5
signshwrd
⊢
F
∈
Word
ℝ
∧
C
∈
ℝ
+
→
H
∈
Word
ℝ
14
hasheq0
⊢
H
∈
Word
ℝ
→
H
=
0
↔
H
=
∅
15
13
14
syl
⊢
F
∈
Word
ℝ
∧
C
∈
ℝ
+
→
H
=
0
↔
H
=
∅
16
15
necon3bid
⊢
F
∈
Word
ℝ
∧
C
∈
ℝ
+
→
H
≠
0
↔
H
≠
∅
17
12
16
mpbid
⊢
F
∈
Word
ℝ
∧
C
∈
ℝ
+
→
H
≠
∅