Metamath Proof Explorer

Theorem signsvfn

Description: Number of changes in a word compared to a shorter word. (Contributed by Thierry Arnoux, 12-Oct-2018)

Ref Expression
Hypotheses signsv.p ⊢ ⨣ = ( 𝑎 ∈ { - 1 , 0 , 1 } , 𝑏 ∈ { - 1 , 0 , 1 } ↦ if ( 𝑏 = 0 , 𝑎 , 𝑏 ) )
signsv.w ⊢ 𝑊 = { ⟨ ( Base ‘ ndx ) , { - 1 , 0 , 1 } ⟩ , ⟨ ( +g ‘ ndx ) , ⨣ ⟩ }
signsv.t ⊢ 𝑇 = ( 𝑓 ∈ Word ℝ ↦ ( 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ↦ ( 𝑊 Σg ( 𝑖 ∈ ( 0 ... 𝑛 ) ↦ ( sgn ‘ ( 𝑓 ‘ 𝑖 ) ) ) ) ) )
signsv.v ⊢ 𝑉 = ( 𝑓 ∈ Word ℝ ↦ Σ 𝑗 ∈ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) if ( ( ( 𝑇 ‘ 𝑓 ) ‘ 𝑗 ) ≠ ( ( 𝑇 ‘ 𝑓 ) ‘ ( 𝑗 − 1 ) ) , 1 , 0 ) )
Assertion signsvfn ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ∧ 𝐾 ∈ ℝ ) → ( 𝑉 ‘ ( 𝐹 ++ ⟨“ 𝐾 ”⟩ ) ) = ( ( 𝑉 ‘ 𝐹 ) + if ( ( ( ( 𝑇 ‘ 𝐹 ) ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) · 𝐾 ) < 0 , 1 , 0 ) ) )

Proof

Step Hyp Ref Expression
1 signsv.p ⊢ ⨣ = ( 𝑎 ∈ { - 1 , 0 , 1 } , 𝑏 ∈ { - 1 , 0 , 1 } ↦ if ( 𝑏 = 0 , 𝑎 , 𝑏 ) )
2 signsv.w ⊢ 𝑊 = { ⟨ ( Base ‘ ndx ) , { - 1 , 0 , 1 } ⟩ , ⟨ ( +g ‘ ndx ) , ⨣ ⟩ }
3 signsv.t ⊢ 𝑇 = ( 𝑓 ∈ Word ℝ ↦ ( 𝑛 ∈ ( 0 ..^ ( ♯ ‘ 𝑓 ) ) ↦ ( 𝑊 Σg ( 𝑖 ∈ ( 0 ... 𝑛 ) ↦ ( sgn ‘ ( 𝑓 ‘ 𝑖 ) ) ) ) ) )
4 signsv.v ⊢ 𝑉 = ( 𝑓 ∈ Word ℝ ↦ Σ 𝑗 ∈ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) if ( ( ( 𝑇 ‘ 𝑓 ) ‘ 𝑗 ) ≠ ( ( 𝑇 ‘ 𝑓 ) ‘ ( 𝑗 − 1 ) ) , 1 , 0 ) )
5 eldifi ⊢ ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) → 𝐹 ∈ Word ℝ )
6 s1cl ⊢ ( 𝐾 ∈ ℝ → ⟨“ 𝐾 ”⟩ ∈ Word ℝ )
7 ccatcl ⊢ ( ( 𝐹 ∈ Word ℝ ∧ ⟨“ 𝐾 ”⟩ ∈ Word ℝ ) → ( 𝐹 ++ ⟨“ 𝐾 ”⟩ ) ∈ Word ℝ )
8 5 6 7 syl2an ⊢ ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ 𝐾 ∈ ℝ ) → ( 𝐹 ++ ⟨“ 𝐾 ”⟩ ) ∈ Word ℝ )
9 1 2 3 4 signsvvfval ⊢ ( ( 𝐹 ++ ⟨“ 𝐾 ”⟩ ) ∈ Word ℝ → ( 𝑉 ‘ ( 𝐹 ++ ⟨“ 𝐾 ”⟩ ) ) = Σ 𝑗 ∈ ( 1 ..^ ( ♯ ‘ ( 𝐹 ++ ⟨“ 𝐾 ”⟩ ) ) ) if ( ( ( 𝑇 ‘ ( 𝐹 ++ ⟨“ 𝐾 ”⟩ ) ) ‘ 𝑗 ) ≠ ( ( 𝑇 ‘ ( 𝐹 ++ ⟨“ 𝐾 ”⟩ ) ) ‘ ( 𝑗 − 1 ) ) , 1 , 0 ) )
10 8 9 syl ⊢ ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ 𝐾 ∈ ℝ ) → ( 𝑉 ‘ ( 𝐹 ++ ⟨“ 𝐾 ”⟩ ) ) = Σ 𝑗 ∈ ( 1 ..^ ( ♯ ‘ ( 𝐹 ++ ⟨“ 𝐾 ”⟩ ) ) ) if ( ( ( 𝑇 ‘ ( 𝐹 ++ ⟨“ 𝐾 ”⟩ ) ) ‘ 𝑗 ) ≠ ( ( 𝑇 ‘ ( 𝐹 ++ ⟨“ 𝐾 ”⟩ ) ) ‘ ( 𝑗 − 1 ) ) , 1 , 0 ) )
11 ccatlen ⊢ ( ( 𝐹 ∈ Word ℝ ∧ ⟨“ 𝐾 ”⟩ ∈ Word ℝ ) → ( ♯ ‘ ( 𝐹 ++ ⟨“ 𝐾 ”⟩ ) ) = ( ( ♯ ‘ 𝐹 ) + ( ♯ ‘ ⟨“ 𝐾 ”⟩ ) ) )
12 5 6 11 syl2an ⊢ ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ 𝐾 ∈ ℝ ) → ( ♯ ‘ ( 𝐹 ++ ⟨“ 𝐾 ”⟩ ) ) = ( ( ♯ ‘ 𝐹 ) + ( ♯ ‘ ⟨“ 𝐾 ”⟩ ) ) )
13 s1len ⊢ ( ♯ ‘ ⟨“ 𝐾 ”⟩ ) = 1
14 13 oveq2i ⊢ ( ( ♯ ‘ 𝐹 ) + ( ♯ ‘ ⟨“ 𝐾 ”⟩ ) ) = ( ( ♯ ‘ 𝐹 ) + 1 )
15 12 14 eqtrdi ⊢ ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ 𝐾 ∈ ℝ ) → ( ♯ ‘ ( 𝐹 ++ ⟨“ 𝐾 ”⟩ ) ) = ( ( ♯ ‘ 𝐹 ) + 1 ) )
16 15 oveq2d ⊢ ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ 𝐾 ∈ ℝ ) → ( 1 ..^ ( ♯ ‘ ( 𝐹 ++ ⟨“ 𝐾 ”⟩ ) ) ) = ( 1 ..^ ( ( ♯ ‘ 𝐹 ) + 1 ) ) )
17 16 sumeq1d ⊢ ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ 𝐾 ∈ ℝ ) → Σ 𝑗 ∈ ( 1 ..^ ( ♯ ‘ ( 𝐹 ++ ⟨“ 𝐾 ”⟩ ) ) ) if ( ( ( 𝑇 ‘ ( 𝐹 ++ ⟨“ 𝐾 ”⟩ ) ) ‘ 𝑗 ) ≠ ( ( 𝑇 ‘ ( 𝐹 ++ ⟨“ 𝐾 ”⟩ ) ) ‘ ( 𝑗 − 1 ) ) , 1 , 0 ) = Σ 𝑗 ∈ ( 1 ..^ ( ( ♯ ‘ 𝐹 ) + 1 ) ) if ( ( ( 𝑇 ‘ ( 𝐹 ++ ⟨“ 𝐾 ”⟩ ) ) ‘ 𝑗 ) ≠ ( ( 𝑇 ‘ ( 𝐹 ++ ⟨“ 𝐾 ”⟩ ) ) ‘ ( 𝑗 − 1 ) ) , 1 , 0 ) )
18 eldifsn ⊢ ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ↔ ( 𝐹 ∈ Word ℝ ∧ 𝐹 ≠ ∅ ) )
19 lennncl ⊢ ( ( 𝐹 ∈ Word ℝ ∧ 𝐹 ≠ ∅ ) → ( ♯ ‘ 𝐹 ) ∈ ℕ )
20 18 19 sylbi ⊢ ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) → ( ♯ ‘ 𝐹 ) ∈ ℕ )
21 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
22 20 21 eleqtrdi ⊢ ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) → ( ♯ ‘ 𝐹 ) ∈ ( ℤ≥ ‘ 1 ) )
23 22 adantr ⊢ ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ 𝐾 ∈ ℝ ) → ( ♯ ‘ 𝐹 ) ∈ ( ℤ≥ ‘ 1 ) )
24 1cnd ⊢ ( ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ 𝐾 ∈ ℝ ) ∧ 𝑗 ∈ ( 1 ... ( ♯ ‘ 𝐹 ) ) ) ∧ ( ( 𝑇 ‘ ( 𝐹 ++ ⟨“ 𝐾 ”⟩ ) ) ‘ 𝑗 ) ≠ ( ( 𝑇 ‘ ( 𝐹 ++ ⟨“ 𝐾 ”⟩ ) ) ‘ ( 𝑗 − 1 ) ) ) → 1 ∈ ℂ )
25 0cnd ⊢ ( ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ 𝐾 ∈ ℝ ) ∧ 𝑗 ∈ ( 1 ... ( ♯ ‘ 𝐹 ) ) ) ∧ ¬ ( ( 𝑇 ‘ ( 𝐹 ++ ⟨“ 𝐾 ”⟩ ) ) ‘ 𝑗 ) ≠ ( ( 𝑇 ‘ ( 𝐹 ++ ⟨“ 𝐾 ”⟩ ) ) ‘ ( 𝑗 − 1 ) ) ) → 0 ∈ ℂ )
26 24 25 ifclda ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ 𝐾 ∈ ℝ ) ∧ 𝑗 ∈ ( 1 ... ( ♯ ‘ 𝐹 ) ) ) → if ( ( ( 𝑇 ‘ ( 𝐹 ++ ⟨“ 𝐾 ”⟩ ) ) ‘ 𝑗 ) ≠ ( ( 𝑇 ‘ ( 𝐹 ++ ⟨“ 𝐾 ”⟩ ) ) ‘ ( 𝑗 − 1 ) ) , 1 , 0 ) ∈ ℂ )
27 fveq2 ⊢ ( 𝑗 = ( ♯ ‘ 𝐹 ) → ( ( 𝑇 ‘ ( 𝐹 ++ ⟨“ 𝐾 ”⟩ ) ) ‘ 𝑗 ) = ( ( 𝑇 ‘ ( 𝐹 ++ ⟨“ 𝐾 ”⟩ ) ) ‘ ( ♯ ‘ 𝐹 ) ) )
28 fvoveq1 ⊢ ( 𝑗 = ( ♯ ‘ 𝐹 ) → ( ( 𝑇 ‘ ( 𝐹 ++ ⟨“ 𝐾 ”⟩ ) ) ‘ ( 𝑗 − 1 ) ) = ( ( 𝑇 ‘ ( 𝐹 ++ ⟨“ 𝐾 ”⟩ ) ) ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) )
29 27 28 neeq12d ⊢ ( 𝑗 = ( ♯ ‘ 𝐹 ) → ( ( ( 𝑇 ‘ ( 𝐹 ++ ⟨“ 𝐾 ”⟩ ) ) ‘ 𝑗 ) ≠ ( ( 𝑇 ‘ ( 𝐹 ++ ⟨“ 𝐾 ”⟩ ) ) ‘ ( 𝑗 − 1 ) ) ↔ ( ( 𝑇 ‘ ( 𝐹 ++ ⟨“ 𝐾 ”⟩ ) ) ‘ ( ♯ ‘ 𝐹 ) ) ≠ ( ( 𝑇 ‘ ( 𝐹 ++ ⟨“ 𝐾 ”⟩ ) ) ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) )
30 29 ifbid ⊢ ( 𝑗 = ( ♯ ‘ 𝐹 ) → if ( ( ( 𝑇 ‘ ( 𝐹 ++ ⟨“ 𝐾 ”⟩ ) ) ‘ 𝑗 ) ≠ ( ( 𝑇 ‘ ( 𝐹 ++ ⟨“ 𝐾 ”⟩ ) ) ‘ ( 𝑗 − 1 ) ) , 1 , 0 ) = if ( ( ( 𝑇 ‘ ( 𝐹 ++ ⟨“ 𝐾 ”⟩ ) ) ‘ ( ♯ ‘ 𝐹 ) ) ≠ ( ( 𝑇 ‘ ( 𝐹 ++ ⟨“ 𝐾 ”⟩ ) ) ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) , 1 , 0 ) )
31 23 26 30 fzosump1 ⊢ ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ 𝐾 ∈ ℝ ) → Σ 𝑗 ∈ ( 1 ..^ ( ( ♯ ‘ 𝐹 ) + 1 ) ) if ( ( ( 𝑇 ‘ ( 𝐹 ++ ⟨“ 𝐾 ”⟩ ) ) ‘ 𝑗 ) ≠ ( ( 𝑇 ‘ ( 𝐹 ++ ⟨“ 𝐾 ”⟩ ) ) ‘ ( 𝑗 − 1 ) ) , 1 , 0 ) = ( Σ 𝑗 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) if ( ( ( 𝑇 ‘ ( 𝐹 ++ ⟨“ 𝐾 ”⟩ ) ) ‘ 𝑗 ) ≠ ( ( 𝑇 ‘ ( 𝐹 ++ ⟨“ 𝐾 ”⟩ ) ) ‘ ( 𝑗 − 1 ) ) , 1 , 0 ) + if ( ( ( 𝑇 ‘ ( 𝐹 ++ ⟨“ 𝐾 ”⟩ ) ) ‘ ( ♯ ‘ 𝐹 ) ) ≠ ( ( 𝑇 ‘ ( 𝐹 ++ ⟨“ 𝐾 ”⟩ ) ) ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) , 1 , 0 ) ) )
32 10 17 31 3eqtrd ⊢ ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ 𝐾 ∈ ℝ ) → ( 𝑉 ‘ ( 𝐹 ++ ⟨“ 𝐾 ”⟩ ) ) = ( Σ 𝑗 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) if ( ( ( 𝑇 ‘ ( 𝐹 ++ ⟨“ 𝐾 ”⟩ ) ) ‘ 𝑗 ) ≠ ( ( 𝑇 ‘ ( 𝐹 ++ ⟨“ 𝐾 ”⟩ ) ) ‘ ( 𝑗 − 1 ) ) , 1 , 0 ) + if ( ( ( 𝑇 ‘ ( 𝐹 ++ ⟨“ 𝐾 ”⟩ ) ) ‘ ( ♯ ‘ 𝐹 ) ) ≠ ( ( 𝑇 ‘ ( 𝐹 ++ ⟨“ 𝐾 ”⟩ ) ) ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) , 1 , 0 ) ) )
33 32 adantlr ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ∧ 𝐾 ∈ ℝ ) → ( 𝑉 ‘ ( 𝐹 ++ ⟨“ 𝐾 ”⟩ ) ) = ( Σ 𝑗 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) if ( ( ( 𝑇 ‘ ( 𝐹 ++ ⟨“ 𝐾 ”⟩ ) ) ‘ 𝑗 ) ≠ ( ( 𝑇 ‘ ( 𝐹 ++ ⟨“ 𝐾 ”⟩ ) ) ‘ ( 𝑗 − 1 ) ) , 1 , 0 ) + if ( ( ( 𝑇 ‘ ( 𝐹 ++ ⟨“ 𝐾 ”⟩ ) ) ‘ ( ♯ ‘ 𝐹 ) ) ≠ ( ( 𝑇 ‘ ( 𝐹 ++ ⟨“ 𝐾 ”⟩ ) ) ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) , 1 , 0 ) ) )
34 simpl ⊢ ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ 𝐾 ∈ ℝ ) → 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) )
35 34 eldifad ⊢ ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ 𝐾 ∈ ℝ ) → 𝐹 ∈ Word ℝ )
36 35 adantr ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ 𝐾 ∈ ℝ ) ∧ 𝑗 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) → 𝐹 ∈ Word ℝ )
37 simplr ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ 𝐾 ∈ ℝ ) ∧ 𝑗 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) → 𝐾 ∈ ℝ )
38 fzo0ss1 ⊢ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ⊆ ( 0 ..^ ( ♯ ‘ 𝐹 ) )
39 38 a1i ⊢ ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ 𝐾 ∈ ℝ ) → ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ⊆ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
40 39 sselda ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ 𝐾 ∈ ℝ ) ∧ 𝑗 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) → 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
41 1 2 3 4 signstfvp ⊢ ( ( 𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑗 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( 𝑇 ‘ ( 𝐹 ++ ⟨“ 𝐾 ”⟩ ) ) ‘ 𝑗 ) = ( ( 𝑇 ‘ 𝐹 ) ‘ 𝑗 ) )
42 36 37 40 41 syl3anc ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ 𝐾 ∈ ℝ ) ∧ 𝑗 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( 𝑇 ‘ ( 𝐹 ++ ⟨“ 𝐾 ”⟩ ) ) ‘ 𝑗 ) = ( ( 𝑇 ‘ 𝐹 ) ‘ 𝑗 ) )
43 elfzoel2 ⊢ ( 𝑗 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) → ( ♯ ‘ 𝐹 ) ∈ ℤ )
44 43 adantl ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ 𝐾 ∈ ℝ ) ∧ 𝑗 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ♯ ‘ 𝐹 ) ∈ ℤ )
45 1nn0 ⊢ 1 ∈ ℕ0
46 eluzmn ⊢ ( ( ( ♯ ‘ 𝐹 ) ∈ ℤ ∧ 1 ∈ ℕ0 ) → ( ♯ ‘ 𝐹 ) ∈ ( ℤ≥ ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) )
47 44 45 46 sylancl ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ 𝐾 ∈ ℝ ) ∧ 𝑗 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ♯ ‘ 𝐹 ) ∈ ( ℤ≥ ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) )
48 fzoss2 ⊢ ( ( ♯ ‘ 𝐹 ) ∈ ( ℤ≥ ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) → ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ⊆ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
49 47 48 syl ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ 𝐾 ∈ ℝ ) ∧ 𝑗 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ⊆ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
50 elfzo1elm1fzo0 ⊢ ( 𝑗 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) → ( 𝑗 − 1 ) ∈ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) )
51 50 adantl ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ 𝐾 ∈ ℝ ) ∧ 𝑗 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 𝑗 − 1 ) ∈ ( 0 ..^ ( ( ♯ ‘ 𝐹 ) − 1 ) ) )
52 49 51 sseldd ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ 𝐾 ∈ ℝ ) ∧ 𝑗 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 𝑗 − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
53 1 2 3 4 signstfvp ⊢ ( ( 𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ ∧ ( 𝑗 − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( 𝑇 ‘ ( 𝐹 ++ ⟨“ 𝐾 ”⟩ ) ) ‘ ( 𝑗 − 1 ) ) = ( ( 𝑇 ‘ 𝐹 ) ‘ ( 𝑗 − 1 ) ) )
54 36 37 52 53 syl3anc ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ 𝐾 ∈ ℝ ) ∧ 𝑗 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( 𝑇 ‘ ( 𝐹 ++ ⟨“ 𝐾 ”⟩ ) ) ‘ ( 𝑗 − 1 ) ) = ( ( 𝑇 ‘ 𝐹 ) ‘ ( 𝑗 − 1 ) ) )
55 42 54 neeq12d ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ 𝐾 ∈ ℝ ) ∧ 𝑗 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( ( 𝑇 ‘ ( 𝐹 ++ ⟨“ 𝐾 ”⟩ ) ) ‘ 𝑗 ) ≠ ( ( 𝑇 ‘ ( 𝐹 ++ ⟨“ 𝐾 ”⟩ ) ) ‘ ( 𝑗 − 1 ) ) ↔ ( ( 𝑇 ‘ 𝐹 ) ‘ 𝑗 ) ≠ ( ( 𝑇 ‘ 𝐹 ) ‘ ( 𝑗 − 1 ) ) ) )
56 55 ifbid ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ 𝐾 ∈ ℝ ) ∧ 𝑗 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) → if ( ( ( 𝑇 ‘ ( 𝐹 ++ ⟨“ 𝐾 ”⟩ ) ) ‘ 𝑗 ) ≠ ( ( 𝑇 ‘ ( 𝐹 ++ ⟨“ 𝐾 ”⟩ ) ) ‘ ( 𝑗 − 1 ) ) , 1 , 0 ) = if ( ( ( 𝑇 ‘ 𝐹 ) ‘ 𝑗 ) ≠ ( ( 𝑇 ‘ 𝐹 ) ‘ ( 𝑗 − 1 ) ) , 1 , 0 ) )
57 56 sumeq2dv ⊢ ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ 𝐾 ∈ ℝ ) → Σ 𝑗 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) if ( ( ( 𝑇 ‘ ( 𝐹 ++ ⟨“ 𝐾 ”⟩ ) ) ‘ 𝑗 ) ≠ ( ( 𝑇 ‘ ( 𝐹 ++ ⟨“ 𝐾 ”⟩ ) ) ‘ ( 𝑗 − 1 ) ) , 1 , 0 ) = Σ 𝑗 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) if ( ( ( 𝑇 ‘ 𝐹 ) ‘ 𝑗 ) ≠ ( ( 𝑇 ‘ 𝐹 ) ‘ ( 𝑗 − 1 ) ) , 1 , 0 ) )
58 1 2 3 4 signsvvfval ⊢ ( 𝐹 ∈ Word ℝ → ( 𝑉 ‘ 𝐹 ) = Σ 𝑗 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) if ( ( ( 𝑇 ‘ 𝐹 ) ‘ 𝑗 ) ≠ ( ( 𝑇 ‘ 𝐹 ) ‘ ( 𝑗 − 1 ) ) , 1 , 0 ) )
59 35 58 syl ⊢ ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ 𝐾 ∈ ℝ ) → ( 𝑉 ‘ 𝐹 ) = Σ 𝑗 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) if ( ( ( 𝑇 ‘ 𝐹 ) ‘ 𝑗 ) ≠ ( ( 𝑇 ‘ 𝐹 ) ‘ ( 𝑗 − 1 ) ) , 1 , 0 ) )
60 57 59 eqtr4d ⊢ ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ 𝐾 ∈ ℝ ) → Σ 𝑗 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) if ( ( ( 𝑇 ‘ ( 𝐹 ++ ⟨“ 𝐾 ”⟩ ) ) ‘ 𝑗 ) ≠ ( ( 𝑇 ‘ ( 𝐹 ++ ⟨“ 𝐾 ”⟩ ) ) ‘ ( 𝑗 − 1 ) ) , 1 , 0 ) = ( 𝑉 ‘ 𝐹 ) )
61 60 adantlr ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ∧ 𝐾 ∈ ℝ ) → Σ 𝑗 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) if ( ( ( 𝑇 ‘ ( 𝐹 ++ ⟨“ 𝐾 ”⟩ ) ) ‘ 𝑗 ) ≠ ( ( 𝑇 ‘ ( 𝐹 ++ ⟨“ 𝐾 ”⟩ ) ) ‘ ( 𝑗 − 1 ) ) , 1 , 0 ) = ( 𝑉 ‘ 𝐹 ) )
62 1 2 3 4 signstfvn ⊢ ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ 𝐾 ∈ ℝ ) → ( ( 𝑇 ‘ ( 𝐹 ++ ⟨“ 𝐾 ”⟩ ) ) ‘ ( ♯ ‘ 𝐹 ) ) = ( ( ( 𝑇 ‘ 𝐹 ) ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ⨣ ( sgn ‘ 𝐾 ) ) )
63 62 adantlr ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ∧ 𝐾 ∈ ℝ ) → ( ( 𝑇 ‘ ( 𝐹 ++ ⟨“ 𝐾 ”⟩ ) ) ‘ ( ♯ ‘ 𝐹 ) ) = ( ( ( 𝑇 ‘ 𝐹 ) ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ⨣ ( sgn ‘ 𝐾 ) ) )
64 35 adantlr ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ∧ 𝐾 ∈ ℝ ) → 𝐹 ∈ Word ℝ )
65 simpr ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ∧ 𝐾 ∈ ℝ ) → 𝐾 ∈ ℝ )
66 fzo0end ⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ → ( ( ♯ ‘ 𝐹 ) − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
67 20 66 syl ⊢ ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) → ( ( ♯ ‘ 𝐹 ) − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
68 67 ad2antrr ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ∧ 𝐾 ∈ ℝ ) → ( ( ♯ ‘ 𝐹 ) − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) )
69 1 2 3 4 signstfvp ⊢ ( ( 𝐹 ∈ Word ℝ ∧ 𝐾 ∈ ℝ ∧ ( ( ♯ ‘ 𝐹 ) − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( 𝑇 ‘ ( 𝐹 ++ ⟨“ 𝐾 ”⟩ ) ) ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) = ( ( 𝑇 ‘ 𝐹 ) ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) )
70 64 65 68 69 syl3anc ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ∧ 𝐾 ∈ ℝ ) → ( ( 𝑇 ‘ ( 𝐹 ++ ⟨“ 𝐾 ”⟩ ) ) ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) = ( ( 𝑇 ‘ 𝐹 ) ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) )
71 63 70 neeq12d ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ∧ 𝐾 ∈ ℝ ) → ( ( ( 𝑇 ‘ ( 𝐹 ++ ⟨“ 𝐾 ”⟩ ) ) ‘ ( ♯ ‘ 𝐹 ) ) ≠ ( ( 𝑇 ‘ ( 𝐹 ++ ⟨“ 𝐾 ”⟩ ) ) ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ↔ ( ( ( 𝑇 ‘ 𝐹 ) ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ⨣ ( sgn ‘ 𝐾 ) ) ≠ ( ( 𝑇 ‘ 𝐹 ) ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) )
72 1 2 3 4 signstfvcl ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ∧ ( ( ♯ ‘ 𝐹 ) − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( 𝑇 ‘ 𝐹 ) ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ∈ { - 1 , 1 } )
73 68 72 syldan ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ∧ 𝐾 ∈ ℝ ) → ( ( 𝑇 ‘ 𝐹 ) ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ∈ { - 1 , 1 } )
74 rexr ⊢ ( 𝐾 ∈ ℝ → 𝐾 ∈ ℝ* )
75 sgncl ⊢ ( 𝐾 ∈ ℝ* → ( sgn ‘ 𝐾 ) ∈ { - 1 , 0 , 1 } )
76 74 75 syl ⊢ ( 𝐾 ∈ ℝ → ( sgn ‘ 𝐾 ) ∈ { - 1 , 0 , 1 } )
77 76 adantl ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ∧ 𝐾 ∈ ℝ ) → ( sgn ‘ 𝐾 ) ∈ { - 1 , 0 , 1 } )
78 1 2 signswch ⊢ ( ( ( ( 𝑇 ‘ 𝐹 ) ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ∈ { - 1 , 1 } ∧ ( sgn ‘ 𝐾 ) ∈ { - 1 , 0 , 1 } ) → ( ( ( ( 𝑇 ‘ 𝐹 ) ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ⨣ ( sgn ‘ 𝐾 ) ) ≠ ( ( 𝑇 ‘ 𝐹 ) ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ↔ ( ( ( 𝑇 ‘ 𝐹 ) ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) · ( sgn ‘ 𝐾 ) ) < 0 ) )
79 73 77 78 syl2anc ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ∧ 𝐾 ∈ ℝ ) → ( ( ( ( 𝑇 ‘ 𝐹 ) ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ⨣ ( sgn ‘ 𝐾 ) ) ≠ ( ( 𝑇 ‘ 𝐹 ) ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ↔ ( ( ( 𝑇 ‘ 𝐹 ) ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) · ( sgn ‘ 𝐾 ) ) < 0 ) )
80 65 rexrd ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ∧ 𝐾 ∈ ℝ ) → 𝐾 ∈ ℝ* )
81 sgnsgn ⊢ ( 𝐾 ∈ ℝ* → ( sgn ‘ ( sgn ‘ 𝐾 ) ) = ( sgn ‘ 𝐾 ) )
82 80 81 syl ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ∧ 𝐾 ∈ ℝ ) → ( sgn ‘ ( sgn ‘ 𝐾 ) ) = ( sgn ‘ 𝐾 ) )
83 82 oveq2d ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ∧ 𝐾 ∈ ℝ ) → ( ( sgn ‘ ( ( 𝑇 ‘ 𝐹 ) ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) · ( sgn ‘ ( sgn ‘ 𝐾 ) ) ) = ( ( sgn ‘ ( ( 𝑇 ‘ 𝐹 ) ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) · ( sgn ‘ 𝐾 ) ) )
84 83 breq1d ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ∧ 𝐾 ∈ ℝ ) → ( ( ( sgn ‘ ( ( 𝑇 ‘ 𝐹 ) ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) · ( sgn ‘ ( sgn ‘ 𝐾 ) ) ) < 0 ↔ ( ( sgn ‘ ( ( 𝑇 ‘ 𝐹 ) ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) · ( sgn ‘ 𝐾 ) ) < 0 ) )
85 neg1rr ⊢ - 1 ∈ ℝ
86 1re ⊢ 1 ∈ ℝ
87 prssi ⊢ ( ( - 1 ∈ ℝ ∧ 1 ∈ ℝ ) → { - 1 , 1 } ⊆ ℝ )
88 85 86 87 mp2an ⊢ { - 1 , 1 } ⊆ ℝ
89 88 73 sselid ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ∧ 𝐾 ∈ ℝ ) → ( ( 𝑇 ‘ 𝐹 ) ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ∈ ℝ )
90 sgnclre ⊢ ( 𝐾 ∈ ℝ → ( sgn ‘ 𝐾 ) ∈ ℝ )
91 90 adantl ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ∧ 𝐾 ∈ ℝ ) → ( sgn ‘ 𝐾 ) ∈ ℝ )
92 sgnmulsgn ⊢ ( ( ( ( 𝑇 ‘ 𝐹 ) ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ∈ ℝ ∧ ( sgn ‘ 𝐾 ) ∈ ℝ ) → ( ( ( ( 𝑇 ‘ 𝐹 ) ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) · ( sgn ‘ 𝐾 ) ) < 0 ↔ ( ( sgn ‘ ( ( 𝑇 ‘ 𝐹 ) ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) · ( sgn ‘ ( sgn ‘ 𝐾 ) ) ) < 0 ) )
93 89 91 92 syl2anc ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ∧ 𝐾 ∈ ℝ ) → ( ( ( ( 𝑇 ‘ 𝐹 ) ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) · ( sgn ‘ 𝐾 ) ) < 0 ↔ ( ( sgn ‘ ( ( 𝑇 ‘ 𝐹 ) ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) · ( sgn ‘ ( sgn ‘ 𝐾 ) ) ) < 0 ) )
94 sgnmulsgn ⊢ ( ( ( ( 𝑇 ‘ 𝐹 ) ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ∈ ℝ ∧ 𝐾 ∈ ℝ ) → ( ( ( ( 𝑇 ‘ 𝐹 ) ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) · 𝐾 ) < 0 ↔ ( ( sgn ‘ ( ( 𝑇 ‘ 𝐹 ) ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) · ( sgn ‘ 𝐾 ) ) < 0 ) )
95 89 94 sylancom ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ∧ 𝐾 ∈ ℝ ) → ( ( ( ( 𝑇 ‘ 𝐹 ) ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) · 𝐾 ) < 0 ↔ ( ( sgn ‘ ( ( 𝑇 ‘ 𝐹 ) ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) · ( sgn ‘ 𝐾 ) ) < 0 ) )
96 84 93 95 3bitr4d ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ∧ 𝐾 ∈ ℝ ) → ( ( ( ( 𝑇 ‘ 𝐹 ) ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) · ( sgn ‘ 𝐾 ) ) < 0 ↔ ( ( ( 𝑇 ‘ 𝐹 ) ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) · 𝐾 ) < 0 ) )
97 71 79 96 3bitrd ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ∧ 𝐾 ∈ ℝ ) → ( ( ( 𝑇 ‘ ( 𝐹 ++ ⟨“ 𝐾 ”⟩ ) ) ‘ ( ♯ ‘ 𝐹 ) ) ≠ ( ( 𝑇 ‘ ( 𝐹 ++ ⟨“ 𝐾 ”⟩ ) ) ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) ↔ ( ( ( 𝑇 ‘ 𝐹 ) ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) · 𝐾 ) < 0 ) )
98 97 ifbid ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ∧ 𝐾 ∈ ℝ ) → if ( ( ( 𝑇 ‘ ( 𝐹 ++ ⟨“ 𝐾 ”⟩ ) ) ‘ ( ♯ ‘ 𝐹 ) ) ≠ ( ( 𝑇 ‘ ( 𝐹 ++ ⟨“ 𝐾 ”⟩ ) ) ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) , 1 , 0 ) = if ( ( ( ( 𝑇 ‘ 𝐹 ) ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) · 𝐾 ) < 0 , 1 , 0 ) )
99 61 98 oveq12d ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ∧ 𝐾 ∈ ℝ ) → ( Σ 𝑗 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) if ( ( ( 𝑇 ‘ ( 𝐹 ++ ⟨“ 𝐾 ”⟩ ) ) ‘ 𝑗 ) ≠ ( ( 𝑇 ‘ ( 𝐹 ++ ⟨“ 𝐾 ”⟩ ) ) ‘ ( 𝑗 − 1 ) ) , 1 , 0 ) + if ( ( ( 𝑇 ‘ ( 𝐹 ++ ⟨“ 𝐾 ”⟩ ) ) ‘ ( ♯ ‘ 𝐹 ) ) ≠ ( ( 𝑇 ‘ ( 𝐹 ++ ⟨“ 𝐾 ”⟩ ) ) ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) , 1 , 0 ) ) = ( ( 𝑉 ‘ 𝐹 ) + if ( ( ( ( 𝑇 ‘ 𝐹 ) ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) · 𝐾 ) < 0 , 1 , 0 ) ) )
100 33 99 eqtrd ⊢ ( ( ( 𝐹 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐹 ‘ 0 ) ≠ 0 ) ∧ 𝐾 ∈ ℝ ) → ( 𝑉 ‘ ( 𝐹 ++ ⟨“ 𝐾 ”⟩ ) ) = ( ( 𝑉 ‘ 𝐹 ) + if ( ( ( ( 𝑇 ‘ 𝐹 ) ‘ ( ( ♯ ‘ 𝐹 ) − 1 ) ) · 𝐾 ) < 0 , 1 , 0 ) ) )