Proof of Theorem signsvtp
Step | Hyp | Ref
| Expression |
1 | | signsvf.f |
. . . . 5
⊢ (𝜑 → 𝐹 = (𝐸 ++ 〈“𝐴”〉)) |
2 | 1 | fveq2d 6195 |
. . . 4
⊢ (𝜑 → (𝑉‘𝐹) = (𝑉‘(𝐸 ++ 〈“𝐴”〉))) |
3 | | signsvf.e |
. . . . 5
⊢ (𝜑 → 𝐸 ∈ (Word ℝ ∖
{∅})) |
4 | | signsvf.0 |
. . . . 5
⊢ (𝜑 → (𝐸‘0) ≠ 0) |
5 | | signsvf.a |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ ℝ) |
6 | | signsv.p |
. . . . . 6
⊢ ⨣ =
(𝑎 ∈ {-1, 0, 1}, 𝑏 ∈ {-1, 0, 1} ↦
if(𝑏 = 0, 𝑎, 𝑏)) |
7 | | signsv.w |
. . . . . 6
⊢ 𝑊 = {〈(Base‘ndx), {-1,
0, 1}〉, 〈(+g‘ndx), ⨣
〉} |
8 | | signsv.t |
. . . . . 6
⊢ 𝑇 = (𝑓 ∈ Word ℝ ↦ (𝑛 ∈ (0..^(#‘𝑓)) ↦ (𝑊 Σg (𝑖 ∈ (0...𝑛) ↦ (sgn‘(𝑓‘𝑖)))))) |
9 | | signsv.v |
. . . . . 6
⊢ 𝑉 = (𝑓 ∈ Word ℝ ↦ Σ𝑗 ∈ (1..^(#‘𝑓))if(((𝑇‘𝑓)‘𝑗) ≠ ((𝑇‘𝑓)‘(𝑗 − 1)), 1, 0)) |
10 | 6, 7, 8, 9 | signsvfn 30659 |
. . . . 5
⊢ (((𝐸 ∈ (Word ℝ ∖
{∅}) ∧ (𝐸‘0) ≠ 0) ∧ 𝐴 ∈ ℝ) → (𝑉‘(𝐸 ++ 〈“𝐴”〉)) = ((𝑉‘𝐸) + if((((𝑇‘𝐸)‘((#‘𝐸) − 1)) · 𝐴) < 0, 1, 0))) |
11 | 3, 4, 5, 10 | syl21anc 1325 |
. . . 4
⊢ (𝜑 → (𝑉‘(𝐸 ++ 〈“𝐴”〉)) = ((𝑉‘𝐸) + if((((𝑇‘𝐸)‘((#‘𝐸) − 1)) · 𝐴) < 0, 1, 0))) |
12 | 2, 11 | eqtrd 2656 |
. . 3
⊢ (𝜑 → (𝑉‘𝐹) = ((𝑉‘𝐸) + if((((𝑇‘𝐸)‘((#‘𝐸) − 1)) · 𝐴) < 0, 1, 0))) |
13 | 12 | adantr 481 |
. 2
⊢ ((𝜑 ∧ 0 < (𝐴 · 𝐵)) → (𝑉‘𝐹) = ((𝑉‘𝐸) + if((((𝑇‘𝐸)‘((#‘𝐸) − 1)) · 𝐴) < 0, 1, 0))) |
14 | | 0red 10041 |
. . . . 5
⊢ ((𝜑 ∧ 0 < (𝐴 · 𝐵)) → 0 ∈ ℝ) |
15 | 3 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 0 < (𝐴 · 𝐵)) → 𝐸 ∈ (Word ℝ ∖
{∅})) |
16 | 15 | eldifad 3586 |
. . . . . . . 8
⊢ ((𝜑 ∧ 0 < (𝐴 · 𝐵)) → 𝐸 ∈ Word ℝ) |
17 | 6, 7, 8, 9 | signstf 30643 |
. . . . . . . 8
⊢ (𝐸 ∈ Word ℝ →
(𝑇‘𝐸) ∈ Word ℝ) |
18 | | wrdf 13310 |
. . . . . . . 8
⊢ ((𝑇‘𝐸) ∈ Word ℝ → (𝑇‘𝐸):(0..^(#‘(𝑇‘𝐸)))⟶ℝ) |
19 | 16, 17, 18 | 3syl 18 |
. . . . . . 7
⊢ ((𝜑 ∧ 0 < (𝐴 · 𝐵)) → (𝑇‘𝐸):(0..^(#‘(𝑇‘𝐸)))⟶ℝ) |
20 | | eldifsn 4317 |
. . . . . . . . . . 11
⊢ (𝐸 ∈ (Word ℝ ∖
{∅}) ↔ (𝐸 ∈
Word ℝ ∧ 𝐸 ≠
∅)) |
21 | 3, 20 | sylib 208 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐸 ∈ Word ℝ ∧ 𝐸 ≠ ∅)) |
22 | 21 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 0 < (𝐴 · 𝐵)) → (𝐸 ∈ Word ℝ ∧ 𝐸 ≠ ∅)) |
23 | | lennncl 13325 |
. . . . . . . . 9
⊢ ((𝐸 ∈ Word ℝ ∧ 𝐸 ≠ ∅) →
(#‘𝐸) ∈
ℕ) |
24 | | fzo0end 12560 |
. . . . . . . . 9
⊢
((#‘𝐸) ∈
ℕ → ((#‘𝐸)
− 1) ∈ (0..^(#‘𝐸))) |
25 | 22, 23, 24 | 3syl 18 |
. . . . . . . 8
⊢ ((𝜑 ∧ 0 < (𝐴 · 𝐵)) → ((#‘𝐸) − 1) ∈ (0..^(#‘𝐸))) |
26 | 6, 7, 8, 9 | signstlen 30644 |
. . . . . . . . . 10
⊢ (𝐸 ∈ Word ℝ →
(#‘(𝑇‘𝐸)) = (#‘𝐸)) |
27 | 16, 26 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 0 < (𝐴 · 𝐵)) → (#‘(𝑇‘𝐸)) = (#‘𝐸)) |
28 | 27 | oveq2d 6666 |
. . . . . . . 8
⊢ ((𝜑 ∧ 0 < (𝐴 · 𝐵)) → (0..^(#‘(𝑇‘𝐸))) = (0..^(#‘𝐸))) |
29 | 25, 28 | eleqtrrd 2704 |
. . . . . . 7
⊢ ((𝜑 ∧ 0 < (𝐴 · 𝐵)) → ((#‘𝐸) − 1) ∈ (0..^(#‘(𝑇‘𝐸)))) |
30 | 19, 29 | ffvelrnd 6360 |
. . . . . 6
⊢ ((𝜑 ∧ 0 < (𝐴 · 𝐵)) → ((𝑇‘𝐸)‘((#‘𝐸) − 1)) ∈
ℝ) |
31 | 5 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 0 < (𝐴 · 𝐵)) → 𝐴 ∈ ℝ) |
32 | 30, 31 | remulcld 10070 |
. . . . 5
⊢ ((𝜑 ∧ 0 < (𝐴 · 𝐵)) → (((𝑇‘𝐸)‘((#‘𝐸) − 1)) · 𝐴) ∈ ℝ) |
33 | | simpr 477 |
. . . . . . 7
⊢ ((𝜑 ∧ 0 < (𝐴 · 𝐵)) → 0 < (𝐴 · 𝐵)) |
34 | | signsvt.b |
. . . . . . . . . . 11
⊢ 𝐵 = ((𝑇‘𝐸)‘(𝑁 − 1)) |
35 | | signsvf.n |
. . . . . . . . . . . . 13
⊢ 𝑁 = (#‘𝐸) |
36 | 35 | oveq1i 6660 |
. . . . . . . . . . . 12
⊢ (𝑁 − 1) = ((#‘𝐸) − 1) |
37 | 36 | fveq2i 6194 |
. . . . . . . . . . 11
⊢ ((𝑇‘𝐸)‘(𝑁 − 1)) = ((𝑇‘𝐸)‘((#‘𝐸) − 1)) |
38 | 34, 37 | eqtri 2644 |
. . . . . . . . . 10
⊢ 𝐵 = ((𝑇‘𝐸)‘((#‘𝐸) − 1)) |
39 | 38, 30 | syl5eqel 2705 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 0 < (𝐴 · 𝐵)) → 𝐵 ∈ ℝ) |
40 | 39 | recnd 10068 |
. . . . . . . 8
⊢ ((𝜑 ∧ 0 < (𝐴 · 𝐵)) → 𝐵 ∈ ℂ) |
41 | 31 | recnd 10068 |
. . . . . . . 8
⊢ ((𝜑 ∧ 0 < (𝐴 · 𝐵)) → 𝐴 ∈ ℂ) |
42 | 40, 41 | mulcomd 10061 |
. . . . . . 7
⊢ ((𝜑 ∧ 0 < (𝐴 · 𝐵)) → (𝐵 · 𝐴) = (𝐴 · 𝐵)) |
43 | 33, 42 | breqtrrd 4681 |
. . . . . 6
⊢ ((𝜑 ∧ 0 < (𝐴 · 𝐵)) → 0 < (𝐵 · 𝐴)) |
44 | 38 | oveq1i 6660 |
. . . . . 6
⊢ (𝐵 · 𝐴) = (((𝑇‘𝐸)‘((#‘𝐸) − 1)) · 𝐴) |
45 | 43, 44 | syl6breq 4694 |
. . . . 5
⊢ ((𝜑 ∧ 0 < (𝐴 · 𝐵)) → 0 < (((𝑇‘𝐸)‘((#‘𝐸) − 1)) · 𝐴)) |
46 | 14, 32, 45 | ltnsymd 10186 |
. . . 4
⊢ ((𝜑 ∧ 0 < (𝐴 · 𝐵)) → ¬ (((𝑇‘𝐸)‘((#‘𝐸) − 1)) · 𝐴) < 0) |
47 | 46 | iffalsed 4097 |
. . 3
⊢ ((𝜑 ∧ 0 < (𝐴 · 𝐵)) → if((((𝑇‘𝐸)‘((#‘𝐸) − 1)) · 𝐴) < 0, 1, 0) = 0) |
48 | 47 | oveq2d 6666 |
. 2
⊢ ((𝜑 ∧ 0 < (𝐴 · 𝐵)) → ((𝑉‘𝐸) + if((((𝑇‘𝐸)‘((#‘𝐸) − 1)) · 𝐴) < 0, 1, 0)) = ((𝑉‘𝐸) + 0)) |
49 | 6, 7, 8, 9 | signsvvf 30656 |
. . . . . 6
⊢ 𝑉:Word
ℝ⟶ℕ0 |
50 | 49 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 0 < (𝐴 · 𝐵)) → 𝑉:Word
ℝ⟶ℕ0) |
51 | 50, 16 | ffvelrnd 6360 |
. . . 4
⊢ ((𝜑 ∧ 0 < (𝐴 · 𝐵)) → (𝑉‘𝐸) ∈
ℕ0) |
52 | 51 | nn0cnd 11353 |
. . 3
⊢ ((𝜑 ∧ 0 < (𝐴 · 𝐵)) → (𝑉‘𝐸) ∈ ℂ) |
53 | 52 | addid1d 10236 |
. 2
⊢ ((𝜑 ∧ 0 < (𝐴 · 𝐵)) → ((𝑉‘𝐸) + 0) = (𝑉‘𝐸)) |
54 | 13, 48, 53 | 3eqtrd 2660 |
1
⊢ ((𝜑 ∧ 0 < (𝐴 · 𝐵)) → (𝑉‘𝐹) = (𝑉‘𝐸)) |