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