Metamath Proof Explorer

Theorem signsvtn

Description: Adding a letter of a different sign as the highest coefficient changes the sign. (Contributed by Thierry Arnoux, 12-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
signsvf.e ⊢ φ → E ∈ Word ℝ ∖ ∅
signsvf.0 ⊢ φ → E ⁡ 0 ≠ 0
signsvf.f ⊢ φ → F = E ++ ⟨“ A ”⟩
signsvf.a ⊢ φ → A ∈ ℝ
signsvf.n ⊢ N = E
signsvt.b ⊢ B = T ⁡ E ⁡ N − 1
Assertion signsvtn ⊢ φ ∧ A ⁢ B < 0 → V ⁡ F − V ⁡ E = 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 signsvf.e ⊢ φ → E ∈ Word ℝ ∖ ∅
6 signsvf.0 ⊢ φ → E ⁡ 0 ≠ 0
7 signsvf.f ⊢ φ → F = E ++ ⟨“ A ”⟩
8 signsvf.a ⊢ φ → A ∈ ℝ
9 signsvf.n ⊢ N = E
10 signsvt.b ⊢ B = T ⁡ E ⁡ N − 1
11 7 fveq2d ⊢ φ → V ⁡ F = V ⁡ E ++ ⟨“ A ”⟩
12 1 2 3 4 signsvfn ⊢ E ∈ Word ℝ ∖ ∅ ∧ E ⁡ 0 ≠ 0 ∧ A ∈ ℝ → V ⁡ E ++ ⟨“ A ”⟩ = V ⁡ E + if T ⁡ E ⁡ E − 1 ⁢ A < 0 1 0
13 5 6 8 12 syl21anc ⊢ φ → V ⁡ E ++ ⟨“ A ”⟩ = V ⁡ E + if T ⁡ E ⁡ E − 1 ⁢ A < 0 1 0
14 11 13 eqtrd ⊢ φ → V ⁡ F = V ⁡ E + if T ⁡ E ⁡ E − 1 ⁢ A < 0 1 0
15 14 adantr ⊢ φ ∧ A ⁢ B < 0 → V ⁡ F = V ⁡ E + if T ⁡ E ⁡ E − 1 ⁢ A < 0 1 0
16 9 oveq1i ⊢ N − 1 = E − 1
17 16 fveq2i ⊢ T ⁡ E ⁡ N − 1 = T ⁡ E ⁡ E − 1
18 10 17 eqtri ⊢ B = T ⁡ E ⁡ E − 1
19 18 oveq1i ⊢ B ⁢ A = T ⁡ E ⁡ E − 1 ⁢ A
20 5 adantr ⊢ φ ∧ A ⁢ B < 0 → E ∈ Word ℝ ∖ ∅
21 20 eldifad ⊢ φ ∧ A ⁢ B < 0 → E ∈ Word ℝ
22 1 2 3 4 signstf ⊢ E ∈ Word ℝ → T ⁡ E ∈ Word ℝ
23 wrdf ⊢ T ⁡ E ∈ Word ℝ → T ⁡ E : 0 ..^ T ⁡ E ⟶ ℝ
24 21 22 23 3syl ⊢ φ ∧ A ⁢ B < 0 → T ⁡ E : 0 ..^ T ⁡ E ⟶ ℝ
25 eldifsn ⊢ E ∈ Word ℝ ∖ ∅ ↔ E ∈ Word ℝ ∧ E ≠ ∅
26 5 25 sylib ⊢ φ → E ∈ Word ℝ ∧ E ≠ ∅
27 26 adantr ⊢ φ ∧ A ⁢ B < 0 → E ∈ Word ℝ ∧ E ≠ ∅
28 lennncl ⊢ E ∈ Word ℝ ∧ E ≠ ∅ → E ∈ ℕ
29 fzo0end ⊢ E ∈ ℕ → E − 1 ∈ 0 ..^ E
30 27 28 29 3syl ⊢ φ ∧ A ⁢ B < 0 → E − 1 ∈ 0 ..^ E
31 1 2 3 4 signstlen ⊢ E ∈ Word ℝ → T ⁡ E = E
32 21 31 syl ⊢ φ ∧ A ⁢ B < 0 → T ⁡ E = E
33 32 oveq2d ⊢ φ ∧ A ⁢ B < 0 → 0 ..^ T ⁡ E = 0 ..^ E
34 30 33 eleqtrrd ⊢ φ ∧ A ⁢ B < 0 → E − 1 ∈ 0 ..^ T ⁡ E
35 24 34 ffvelcdmd ⊢ φ ∧ A ⁢ B < 0 → T ⁡ E ⁡ E − 1 ∈ ℝ
36 18 35 eqeltrid ⊢ φ ∧ A ⁢ B < 0 → B ∈ ℝ
37 36 recnd ⊢ φ ∧ A ⁢ B < 0 → B ∈ ℂ
38 8 adantr ⊢ φ ∧ A ⁢ B < 0 → A ∈ ℝ
39 38 recnd ⊢ φ ∧ A ⁢ B < 0 → A ∈ ℂ
40 37 39 mulcomd ⊢ φ ∧ A ⁢ B < 0 → B ⁢ A = A ⁢ B
41 simpr ⊢ φ ∧ A ⁢ B < 0 → A ⁢ B < 0
42 40 41 eqbrtrd ⊢ φ ∧ A ⁢ B < 0 → B ⁢ A < 0
43 19 42 eqbrtrrid ⊢ φ ∧ A ⁢ B < 0 → T ⁡ E ⁡ E − 1 ⁢ A < 0
44 43 iftrued ⊢ φ ∧ A ⁢ B < 0 → if T ⁡ E ⁡ E − 1 ⁢ A < 0 1 0 = 1
45 44 oveq2d ⊢ φ ∧ A ⁢ B < 0 → V ⁡ E + if T ⁡ E ⁡ E − 1 ⁢ A < 0 1 0 = V ⁡ E + 1
46 15 45 eqtr2d ⊢ φ ∧ A ⁢ B < 0 → V ⁡ E + 1 = V ⁡ F
47 1 2 3 4 signsvvf ⊢ V : Word ℝ ⟶ ℕ 0
48 47 a1i ⊢ φ ∧ A ⁢ B < 0 → V : Word ℝ ⟶ ℕ 0
49 7 adantr ⊢ φ ∧ A ⁢ B < 0 → F = E ++ ⟨“ A ”⟩
50 38 s1cld ⊢ φ ∧ A ⁢ B < 0 → ⟨“ A ”⟩ ∈ Word ℝ
51 ccatcl ⊢ E ∈ Word ℝ ∧ ⟨“ A ”⟩ ∈ Word ℝ → E ++ ⟨“ A ”⟩ ∈ Word ℝ
52 21 50 51 syl2anc ⊢ φ ∧ A ⁢ B < 0 → E ++ ⟨“ A ”⟩ ∈ Word ℝ
53 49 52 eqeltrd ⊢ φ ∧ A ⁢ B < 0 → F ∈ Word ℝ
54 48 53 ffvelcdmd ⊢ φ ∧ A ⁢ B < 0 → V ⁡ F ∈ ℕ 0
55 54 nn0cnd ⊢ φ ∧ A ⁢ B < 0 → V ⁡ F ∈ ℂ
56 48 21 ffvelcdmd ⊢ φ ∧ A ⁢ B < 0 → V ⁡ E ∈ ℕ 0
57 56 nn0cnd ⊢ φ ∧ A ⁢ B < 0 → V ⁡ E ∈ ℂ
58 1cnd ⊢ φ ∧ A ⁢ B < 0 → 1 ∈ ℂ
59 55 57 58 subaddd ⊢ φ ∧ A ⁢ B < 0 → V ⁡ F − V ⁡ E = 1 ↔ V ⁡ E + 1 = V ⁡ F
60 46 59 mpbird ⊢ φ ∧ A ⁢ B < 0 → V ⁡ F − V ⁡ E = 1