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 ∈ − 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
Assertion signstfvcl ⊢ F ∈ Word ℝ ∖ ∅ ∧ F ⁡ 0 ≠ 0 ∧ N ∈ 0 ..^ F → T ⁡ F ⁡ N ∈ − 1 1

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 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 ∈ − 1 0 1
8 6 7 sylancom ⊢ F ∈ Word ℝ ∖ ∅ ∧ F ⁡ 0 ≠ 0 ∧ N ∈ 0 ..^ F → T ⁡ F ⁡ N ∈ − 1 0 1
9 1 2 3 4 signstfvneq0 ⊢ F ∈ Word ℝ ∖ ∅ ∧ F ⁡ 0 ≠ 0 ∧ N ∈ 0 ..^ F → T ⁡ F ⁡ N ≠ 0
10 eldifsn ⊢ T ⁡ F ⁡ N ∈ − 1 0 1 ∖ 0 ↔ T ⁡ F ⁡ N ∈ − 1 0 1 ∧ T ⁡ F ⁡ N ≠ 0
11 8 9 10 sylanbrc ⊢ F ∈ Word ℝ ∖ ∅ ∧ F ⁡ 0 ≠ 0 ∧ N ∈ 0 ..^ F → T ⁡ F ⁡ N ∈ − 1 0 1 ∖ 0
12 tpcomb ⊢ − 1 0 1 = − 1 1 0
13 12 difeq1i ⊢ − 1 0 1 ∖ 0 = − 1 1 0 ∖ 0
14 neg1ne0 ⊢ − 1 ≠ 0
15 ax-1ne0 ⊢ 1 ≠ 0
16 diftpsn3 ⊢ − 1 ≠ 0 ∧ 1 ≠ 0 → − 1 1 0 ∖ 0 = − 1 1
17 14 15 16 mp2an ⊢ − 1 1 0 ∖ 0 = − 1 1
18 13 17 eqtri ⊢ − 1 0 1 ∖ 0 = − 1 1
19 11 18 eleqtrdi ⊢ F ∈ Word ℝ ∖ ∅ ∧ F ⁡ 0 ≠ 0 ∧ N ∈ 0 ..^ F → T ⁡ F ⁡ N ∈ − 1 1