signsvfnn

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	⊢ ⨣ = ( 𝑎 ∈ { - 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 ) )
	signsvf.e	⊢ ( 𝜑 → 𝐸 ∈ ( Word ℝ ∖ { ∅ } ) )
	signsvf.0	⊢ ( 𝜑 → ( 𝐸 ‘ 0 ) ≠ 0 )
	signsvf.f	⊢ ( 𝜑 → 𝐹 = ( 𝐸 ++ ⟨“ 𝐴 ”⟩ ) )
	signsvf.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	signsvf.n	⊢ 𝑁 = ( ♯ ‘ 𝐸 )
	signsvf.b	⊢ 𝐵 = ( 𝐸 ‘ ( 𝑁 − 1 ) )
Assertion	signsvfnn	⊢ ( ( 𝜑 ∧ ( 𝐵 · 𝐴 ) < 0 ) → ( ( 𝑉 ‘ 𝐹 ) − ( 𝑉 ‘ 𝐸 ) ) = 1 )

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		signsvf.e	⊢ ( 𝜑 → 𝐸 ∈ ( Word ℝ ∖ { ∅ } ) )
6		signsvf.0	⊢ ( 𝜑 → ( 𝐸 ‘ 0 ) ≠ 0 )
7		signsvf.f	⊢ ( 𝜑 → 𝐹 = ( 𝐸 ++ ⟨“ 𝐴 ”⟩ ) )
8		signsvf.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
9		signsvf.n	⊢ 𝑁 = ( ♯ ‘ 𝐸 )
10		signsvf.b	⊢ 𝐵 = ( 𝐸 ‘ ( 𝑁 − 1 ) )
11	5	adantr	⊢ ( ( 𝜑 ∧ ( 𝐵 · 𝐴 ) < 0 ) → 𝐸 ∈ ( Word ℝ ∖ { ∅ } ) )
12	5	eldifad	⊢ ( 𝜑 → 𝐸 ∈ Word ℝ )
13		wrdf	⊢ ( 𝐸 ∈ Word ℝ → 𝐸 : ( 0 ..^ ( ♯ ‘ 𝐸 ) ) ⟶ ℝ )
14	12 13	syl	⊢ ( 𝜑 → 𝐸 : ( 0 ..^ ( ♯ ‘ 𝐸 ) ) ⟶ ℝ )
15	9	oveq1i	⊢ ( 𝑁 − 1 ) = ( ( ♯ ‘ 𝐸 ) − 1 )
16		eldifsn	⊢ ( 𝐸 ∈ ( Word ℝ ∖ { ∅ } ) ↔ ( 𝐸 ∈ Word ℝ ∧ 𝐸 ≠ ∅ ) )
17	5 16	sylib	⊢ ( 𝜑 → ( 𝐸 ∈ Word ℝ ∧ 𝐸 ≠ ∅ ) )
18		lennncl	⊢ ( ( 𝐸 ∈ Word ℝ ∧ 𝐸 ≠ ∅ ) → ( ♯ ‘ 𝐸 ) ∈ ℕ )
19		fzo0end	⊢ ( ( ♯ ‘ 𝐸 ) ∈ ℕ → ( ( ♯ ‘ 𝐸 ) − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐸 ) ) )
20	17 18 19	3syl	⊢ ( 𝜑 → ( ( ♯ ‘ 𝐸 ) − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐸 ) ) )
21	15 20	eqeltrid	⊢ ( 𝜑 → ( 𝑁 − 1 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐸 ) ) )
22	14 21	ffvelcdmd	⊢ ( 𝜑 → ( 𝐸 ‘ ( 𝑁 − 1 ) ) ∈ ℝ )
23	22	recnd	⊢ ( 𝜑 → ( 𝐸 ‘ ( 𝑁 − 1 ) ) ∈ ℂ )
24	10 23	eqeltrid	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
25	24	adantr	⊢ ( ( 𝜑 ∧ ( 𝐵 · 𝐴 ) < 0 ) → 𝐵 ∈ ℂ )
26	8	recnd	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
27	26	adantr	⊢ ( ( 𝜑 ∧ ( 𝐵 · 𝐴 ) < 0 ) → 𝐴 ∈ ℂ )
28		simpr	⊢ ( ( 𝜑 ∧ ( 𝐵 · 𝐴 ) < 0 ) → ( 𝐵 · 𝐴 ) < 0 )
29	28	lt0ne0d	⊢ ( ( 𝜑 ∧ ( 𝐵 · 𝐴 ) < 0 ) → ( 𝐵 · 𝐴 ) ≠ 0 )
30	25 27 29	mulne0bad	⊢ ( ( 𝜑 ∧ ( 𝐵 · 𝐴 ) < 0 ) → 𝐵 ≠ 0 )
31	10 30	eqnetrrid	⊢ ( ( 𝜑 ∧ ( 𝐵 · 𝐴 ) < 0 ) → ( 𝐸 ‘ ( 𝑁 − 1 ) ) ≠ 0 )
32	1 2 3 4 9	signsvtn0	⊢ ( ( 𝐸 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐸 ‘ ( 𝑁 − 1 ) ) ≠ 0 ) → ( ( 𝑇 ‘ 𝐸 ) ‘ ( 𝑁 − 1 ) ) = ( sgn ‘ ( 𝐸 ‘ ( 𝑁 − 1 ) ) ) )
33	10	fveq2i	⊢ ( sgn ‘ 𝐵 ) = ( sgn ‘ ( 𝐸 ‘ ( 𝑁 − 1 ) ) )
34	32 33	eqtr4di	⊢ ( ( 𝐸 ∈ ( Word ℝ ∖ { ∅ } ) ∧ ( 𝐸 ‘ ( 𝑁 − 1 ) ) ≠ 0 ) → ( ( 𝑇 ‘ 𝐸 ) ‘ ( 𝑁 − 1 ) ) = ( sgn ‘ 𝐵 ) )
35	11 31 34	syl2anc	⊢ ( ( 𝜑 ∧ ( 𝐵 · 𝐴 ) < 0 ) → ( ( 𝑇 ‘ 𝐸 ) ‘ ( 𝑁 − 1 ) ) = ( sgn ‘ 𝐵 ) )
36	35	fveq2d	⊢ ( ( 𝜑 ∧ ( 𝐵 · 𝐴 ) < 0 ) → ( sgn ‘ ( ( 𝑇 ‘ 𝐸 ) ‘ ( 𝑁 − 1 ) ) ) = ( sgn ‘ ( sgn ‘ 𝐵 ) ) )
37	10 22	eqeltrid	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
38	37	adantr	⊢ ( ( 𝜑 ∧ ( 𝐵 · 𝐴 ) < 0 ) → 𝐵 ∈ ℝ )
39	38	rexrd	⊢ ( ( 𝜑 ∧ ( 𝐵 · 𝐴 ) < 0 ) → 𝐵 ∈ ℝ^* )
40		sgnsgn	⊢ ( 𝐵 ∈ ℝ^* → ( sgn ‘ ( sgn ‘ 𝐵 ) ) = ( sgn ‘ 𝐵 ) )
41	39 40	syl	⊢ ( ( 𝜑 ∧ ( 𝐵 · 𝐴 ) < 0 ) → ( sgn ‘ ( sgn ‘ 𝐵 ) ) = ( sgn ‘ 𝐵 ) )
42	36 41	eqtrd	⊢ ( ( 𝜑 ∧ ( 𝐵 · 𝐴 ) < 0 ) → ( sgn ‘ ( ( 𝑇 ‘ 𝐸 ) ‘ ( 𝑁 − 1 ) ) ) = ( sgn ‘ 𝐵 ) )
43	42	oveq2d	⊢ ( ( 𝜑 ∧ ( 𝐵 · 𝐴 ) < 0 ) → ( ( sgn ‘ 𝐴 ) · ( sgn ‘ ( ( 𝑇 ‘ 𝐸 ) ‘ ( 𝑁 − 1 ) ) ) ) = ( ( sgn ‘ 𝐴 ) · ( sgn ‘ 𝐵 ) ) )
44	26 24	mulcomd	⊢ ( 𝜑 → ( 𝐴 · 𝐵 ) = ( 𝐵 · 𝐴 ) )
45	44	breq1d	⊢ ( 𝜑 → ( ( 𝐴 · 𝐵 ) < 0 ↔ ( 𝐵 · 𝐴 ) < 0 ) )
46		sgnmulsgn	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 · 𝐵 ) < 0 ↔ ( ( sgn ‘ 𝐴 ) · ( sgn ‘ 𝐵 ) ) < 0 ) )
47	8 37 46	syl2anc	⊢ ( 𝜑 → ( ( 𝐴 · 𝐵 ) < 0 ↔ ( ( sgn ‘ 𝐴 ) · ( sgn ‘ 𝐵 ) ) < 0 ) )
48	45 47	bitr3d	⊢ ( 𝜑 → ( ( 𝐵 · 𝐴 ) < 0 ↔ ( ( sgn ‘ 𝐴 ) · ( sgn ‘ 𝐵 ) ) < 0 ) )
49	48	biimpa	⊢ ( ( 𝜑 ∧ ( 𝐵 · 𝐴 ) < 0 ) → ( ( sgn ‘ 𝐴 ) · ( sgn ‘ 𝐵 ) ) < 0 )
50	43 49	eqbrtrd	⊢ ( ( 𝜑 ∧ ( 𝐵 · 𝐴 ) < 0 ) → ( ( sgn ‘ 𝐴 ) · ( sgn ‘ ( ( 𝑇 ‘ 𝐸 ) ‘ ( 𝑁 − 1 ) ) ) ) < 0 )
51	8	adantr	⊢ ( ( 𝜑 ∧ ( 𝐵 · 𝐴 ) < 0 ) → 𝐴 ∈ ℝ )
52		sgnclre	⊢ ( 𝐵 ∈ ℝ → ( sgn ‘ 𝐵 ) ∈ ℝ )
53	38 52	syl	⊢ ( ( 𝜑 ∧ ( 𝐵 · 𝐴 ) < 0 ) → ( sgn ‘ 𝐵 ) ∈ ℝ )
54	35 53	eqeltrd	⊢ ( ( 𝜑 ∧ ( 𝐵 · 𝐴 ) < 0 ) → ( ( 𝑇 ‘ 𝐸 ) ‘ ( 𝑁 − 1 ) ) ∈ ℝ )
55		sgnmulsgn	⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝑇 ‘ 𝐸 ) ‘ ( 𝑁 − 1 ) ) ∈ ℝ ) → ( ( 𝐴 · ( ( 𝑇 ‘ 𝐸 ) ‘ ( 𝑁 − 1 ) ) ) < 0 ↔ ( ( sgn ‘ 𝐴 ) · ( sgn ‘ ( ( 𝑇 ‘ 𝐸 ) ‘ ( 𝑁 − 1 ) ) ) ) < 0 ) )
56	51 54 55	syl2anc	⊢ ( ( 𝜑 ∧ ( 𝐵 · 𝐴 ) < 0 ) → ( ( 𝐴 · ( ( 𝑇 ‘ 𝐸 ) ‘ ( 𝑁 − 1 ) ) ) < 0 ↔ ( ( sgn ‘ 𝐴 ) · ( sgn ‘ ( ( 𝑇 ‘ 𝐸 ) ‘ ( 𝑁 − 1 ) ) ) ) < 0 ) )
57	50 56	mpbird	⊢ ( ( 𝜑 ∧ ( 𝐵 · 𝐴 ) < 0 ) → ( 𝐴 · ( ( 𝑇 ‘ 𝐸 ) ‘ ( 𝑁 − 1 ) ) ) < 0 )
58		eqid	⊢ ( ( 𝑇 ‘ 𝐸 ) ‘ ( 𝑁 − 1 ) ) = ( ( 𝑇 ‘ 𝐸 ) ‘ ( 𝑁 − 1 ) )
59	1 2 3 4 5 6 7 8 9 58	signsvtn	⊢ ( ( 𝜑 ∧ ( 𝐴 · ( ( 𝑇 ‘ 𝐸 ) ‘ ( 𝑁 − 1 ) ) ) < 0 ) → ( ( 𝑉 ‘ 𝐹 ) − ( 𝑉 ‘ 𝐸 ) ) = 1 )
60	57 59	syldan	⊢ ( ( 𝜑 ∧ ( 𝐵 · 𝐴 ) < 0 ) → ( ( 𝑉 ‘ 𝐹 ) − ( 𝑉 ‘ 𝐸 ) ) = 1 )

Metamath Proof Explorer

Theorem signsvfnn

Proof