Metamath Proof Explorer

Theorem signstfvcl

Description: Closure of the zero skipping sign in case the first letter is not zero. (Contributed by Thierry Arnoux, 10-Oct-2018)

Ref Expression
Hypotheses signsv.p ⊢⨣˙=a∈−101,b∈−101⟼ifb=0ab
signsv.w ⊢W=Basendx−101+ndx⨣˙
signsv.t ⊢T=f∈Wordℝ⟼n∈0..^f⟼∑Wi=0nsgn⁡f⁡i
signsv.v ⊢V=f∈Wordℝ⟼∑j∈1..^fifT⁡f⁡j≠T⁡f⁡j−110
Assertion signstfvcl ⊢F∈Wordℝ∖∅∧F⁡0≠0∧N∈0..^F→T⁡F⁡N∈−11

Proof

Step Hyp Ref Expression
1 signsv.p ⊢⨣˙=a∈−101,b∈−101⟼ifb=0ab
2 signsv.w ⊢W=Basendx−101+ndx⨣˙
3 signsv.t ⊢T=f∈Wordℝ⟼n∈0..^f⟼∑Wi=0nsgn⁡f⁡i
4 signsv.v ⊢V=f∈Wordℝ⟼∑j∈1..^fifT⁡f⁡j≠T⁡f⁡j−110
5 simpll ⊢F∈Wordℝ∖∅∧F⁡0≠0∧N∈0..^F→F∈Wordℝ∖∅
6 5 eldifad ⊢F∈Wordℝ∖∅∧F⁡0≠0∧N∈0..^F→F∈Wordℝ
7 1 2 3 4 signstcl ⊢F∈Wordℝ∧N∈0..^F→T⁡F⁡N∈−101
8 6 7 sylancom ⊢F∈Wordℝ∖∅∧F⁡0≠0∧N∈0..^F→T⁡F⁡N∈−101
9 1 2 3 4 signstfvneq0 ⊢F∈Wordℝ∖∅∧F⁡0≠0∧N∈0..^F→T⁡F⁡N≠0
10 eldifsn ⊢T⁡F⁡N∈−101∖0↔T⁡F⁡N∈−101∧T⁡F⁡N≠0
11 8 9 10 sylanbrc ⊢F∈Wordℝ∖∅∧F⁡0≠0∧N∈0..^F→T⁡F⁡N∈−101∖0
12 tpcomb ⊢−101=−110
13 12 difeq1i ⊢−101∖0=−110∖0
14 neg1ne0 ⊢−1≠0
15 ax-1ne0 ⊢1≠0
16 diftpsn3 ⊢−1≠0∧1≠0→−110∖0=−11
17 14 15 16 mp2an ⊢−110∖0=−11
18 13 17 eqtri ⊢−101∖0=−11
19 11 18 eleqtrdi ⊢F∈Wordℝ∖∅∧F⁡0≠0∧N∈0..^F→T⁡F⁡N∈−11