Metamath Proof Explorer

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 ≠ ∅