Proof of Theorem signsvfpn
Step | Hyp | Ref
| Expression |
1 | | signsvf.a |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈ ℝ) |
2 | 1 | recnd 11003 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ ℂ) |
3 | | signsvf.b |
. . . . . . . . 9
⊢ 𝐵 = (𝐸‘(𝑁 − 1)) |
4 | | signsvf.e |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐸 ∈ (Word ℝ ∖
{∅})) |
5 | 4 | eldifad 3899 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐸 ∈ Word ℝ) |
6 | | wrdf 14222 |
. . . . . . . . . . . 12
⊢ (𝐸 ∈ Word ℝ →
𝐸:(0..^(♯‘𝐸))⟶ℝ) |
7 | 5, 6 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐸:(0..^(♯‘𝐸))⟶ℝ) |
8 | | signsvf.n |
. . . . . . . . . . . . 13
⊢ 𝑁 = (♯‘𝐸) |
9 | 8 | oveq1i 7285 |
. . . . . . . . . . . 12
⊢ (𝑁 − 1) =
((♯‘𝐸) −
1) |
10 | | eldifsn 4720 |
. . . . . . . . . . . . . 14
⊢ (𝐸 ∈ (Word ℝ ∖
{∅}) ↔ (𝐸 ∈
Word ℝ ∧ 𝐸 ≠
∅)) |
11 | 4, 10 | sylib 217 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐸 ∈ Word ℝ ∧ 𝐸 ≠ ∅)) |
12 | | lennncl 14237 |
. . . . . . . . . . . . 13
⊢ ((𝐸 ∈ Word ℝ ∧ 𝐸 ≠ ∅) →
(♯‘𝐸) ∈
ℕ) |
13 | | fzo0end 13479 |
. . . . . . . . . . . . 13
⊢
((♯‘𝐸)
∈ ℕ → ((♯‘𝐸) − 1) ∈
(0..^(♯‘𝐸))) |
14 | 11, 12, 13 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((♯‘𝐸) − 1) ∈
(0..^(♯‘𝐸))) |
15 | 9, 14 | eqeltrid 2843 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑁 − 1) ∈ (0..^(♯‘𝐸))) |
16 | 7, 15 | ffvelrnd 6962 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐸‘(𝑁 − 1)) ∈
ℝ) |
17 | 16 | recnd 11003 |
. . . . . . . . 9
⊢ (𝜑 → (𝐸‘(𝑁 − 1)) ∈
ℂ) |
18 | 3, 17 | eqeltrid 2843 |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ∈ ℂ) |
19 | 2, 18 | mulcomd 10996 |
. . . . . . 7
⊢ (𝜑 → (𝐴 · 𝐵) = (𝐵 · 𝐴)) |
20 | 19 | breq2d 5086 |
. . . . . 6
⊢ (𝜑 → (0 < (𝐴 · 𝐵) ↔ 0 < (𝐵 · 𝐴))) |
21 | 3, 16 | eqeltrid 2843 |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈ ℝ) |
22 | | sgnmulsgp 32517 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (0 <
(𝐴 · 𝐵) ↔ 0 <
((sgn‘𝐴) ·
(sgn‘𝐵)))) |
23 | 1, 21, 22 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → (0 < (𝐴 · 𝐵) ↔ 0 < ((sgn‘𝐴) · (sgn‘𝐵)))) |
24 | 20, 23 | bitr3d 280 |
. . . . 5
⊢ (𝜑 → (0 < (𝐵 · 𝐴) ↔ 0 < ((sgn‘𝐴) · (sgn‘𝐵)))) |
25 | 24 | biimpa 477 |
. . . 4
⊢ ((𝜑 ∧ 0 < (𝐵 · 𝐴)) → 0 < ((sgn‘𝐴) · (sgn‘𝐵))) |
26 | 4 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 0 < (𝐵 · 𝐴)) → 𝐸 ∈ (Word ℝ ∖
{∅})) |
27 | 18 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 0 < (𝐵 · 𝐴)) → 𝐵 ∈ ℂ) |
28 | 2 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 0 < (𝐵 · 𝐴)) → 𝐴 ∈ ℂ) |
29 | | simpr 485 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 0 < (𝐵 · 𝐴)) → 0 < (𝐵 · 𝐴)) |
30 | 29 | gt0ne0d 11539 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 0 < (𝐵 · 𝐴)) → (𝐵 · 𝐴) ≠ 0) |
31 | 27, 28, 30 | mulne0bad 11630 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 0 < (𝐵 · 𝐴)) → 𝐵 ≠ 0) |
32 | 3, 31 | eqnetrrid 3019 |
. . . . . . . 8
⊢ ((𝜑 ∧ 0 < (𝐵 · 𝐴)) → (𝐸‘(𝑁 − 1)) ≠ 0) |
33 | | signsv.p |
. . . . . . . . . 10
⊢ ⨣ =
(𝑎 ∈ {-1, 0, 1}, 𝑏 ∈ {-1, 0, 1} ↦
if(𝑏 = 0, 𝑎, 𝑏)) |
34 | | signsv.w |
. . . . . . . . . 10
⊢ 𝑊 = {〈(Base‘ndx), {-1,
0, 1}〉, 〈(+g‘ndx), ⨣
〉} |
35 | | signsv.t |
. . . . . . . . . 10
⊢ 𝑇 = (𝑓 ∈ Word ℝ ↦ (𝑛 ∈
(0..^(♯‘𝑓))
↦ (𝑊
Σg (𝑖 ∈ (0...𝑛) ↦ (sgn‘(𝑓‘𝑖)))))) |
36 | | signsv.v |
. . . . . . . . . 10
⊢ 𝑉 = (𝑓 ∈ Word ℝ ↦ Σ𝑗 ∈
(1..^(♯‘𝑓))if(((𝑇‘𝑓)‘𝑗) ≠ ((𝑇‘𝑓)‘(𝑗 − 1)), 1, 0)) |
37 | 33, 34, 35, 36, 8 | signsvtn0 32549 |
. . . . . . . . 9
⊢ ((𝐸 ∈ (Word ℝ ∖
{∅}) ∧ (𝐸‘(𝑁 − 1)) ≠ 0) → ((𝑇‘𝐸)‘(𝑁 − 1)) = (sgn‘(𝐸‘(𝑁 − 1)))) |
38 | 3 | fveq2i 6777 |
. . . . . . . . 9
⊢
(sgn‘𝐵) =
(sgn‘(𝐸‘(𝑁 − 1))) |
39 | 37, 38 | eqtr4di 2796 |
. . . . . . . 8
⊢ ((𝐸 ∈ (Word ℝ ∖
{∅}) ∧ (𝐸‘(𝑁 − 1)) ≠ 0) → ((𝑇‘𝐸)‘(𝑁 − 1)) = (sgn‘𝐵)) |
40 | 26, 32, 39 | syl2anc 584 |
. . . . . . 7
⊢ ((𝜑 ∧ 0 < (𝐵 · 𝐴)) → ((𝑇‘𝐸)‘(𝑁 − 1)) = (sgn‘𝐵)) |
41 | 40 | fveq2d 6778 |
. . . . . 6
⊢ ((𝜑 ∧ 0 < (𝐵 · 𝐴)) → (sgn‘((𝑇‘𝐸)‘(𝑁 − 1))) = (sgn‘(sgn‘𝐵))) |
42 | 21 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 0 < (𝐵 · 𝐴)) → 𝐵 ∈ ℝ) |
43 | 42 | rexrd 11025 |
. . . . . . 7
⊢ ((𝜑 ∧ 0 < (𝐵 · 𝐴)) → 𝐵 ∈
ℝ*) |
44 | | sgnsgn 32515 |
. . . . . . 7
⊢ (𝐵 ∈ ℝ*
→ (sgn‘(sgn‘𝐵)) = (sgn‘𝐵)) |
45 | 43, 44 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 0 < (𝐵 · 𝐴)) → (sgn‘(sgn‘𝐵)) = (sgn‘𝐵)) |
46 | 41, 45 | eqtrd 2778 |
. . . . 5
⊢ ((𝜑 ∧ 0 < (𝐵 · 𝐴)) → (sgn‘((𝑇‘𝐸)‘(𝑁 − 1))) = (sgn‘𝐵)) |
47 | 46 | oveq2d 7291 |
. . . 4
⊢ ((𝜑 ∧ 0 < (𝐵 · 𝐴)) → ((sgn‘𝐴) · (sgn‘((𝑇‘𝐸)‘(𝑁 − 1)))) = ((sgn‘𝐴) · (sgn‘𝐵))) |
48 | 25, 47 | breqtrrd 5102 |
. . 3
⊢ ((𝜑 ∧ 0 < (𝐵 · 𝐴)) → 0 < ((sgn‘𝐴) · (sgn‘((𝑇‘𝐸)‘(𝑁 − 1))))) |
49 | 1 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 0 < (𝐵 · 𝐴)) → 𝐴 ∈ ℝ) |
50 | | sgnclre 32506 |
. . . . . 6
⊢ (𝐵 ∈ ℝ →
(sgn‘𝐵) ∈
ℝ) |
51 | 42, 50 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 0 < (𝐵 · 𝐴)) → (sgn‘𝐵) ∈ ℝ) |
52 | 40, 51 | eqeltrd 2839 |
. . . 4
⊢ ((𝜑 ∧ 0 < (𝐵 · 𝐴)) → ((𝑇‘𝐸)‘(𝑁 − 1)) ∈
ℝ) |
53 | | sgnmulsgp 32517 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ ((𝑇‘𝐸)‘(𝑁 − 1)) ∈ ℝ) → (0 <
(𝐴 · ((𝑇‘𝐸)‘(𝑁 − 1))) ↔ 0 <
((sgn‘𝐴) ·
(sgn‘((𝑇‘𝐸)‘(𝑁 − 1)))))) |
54 | 49, 52, 53 | syl2anc 584 |
. . 3
⊢ ((𝜑 ∧ 0 < (𝐵 · 𝐴)) → (0 < (𝐴 · ((𝑇‘𝐸)‘(𝑁 − 1))) ↔ 0 <
((sgn‘𝐴) ·
(sgn‘((𝑇‘𝐸)‘(𝑁 − 1)))))) |
55 | 48, 54 | mpbird 256 |
. 2
⊢ ((𝜑 ∧ 0 < (𝐵 · 𝐴)) → 0 < (𝐴 · ((𝑇‘𝐸)‘(𝑁 − 1)))) |
56 | | signsvf.0 |
. . 3
⊢ (𝜑 → (𝐸‘0) ≠ 0) |
57 | | signsvf.f |
. . 3
⊢ (𝜑 → 𝐹 = (𝐸 ++ 〈“𝐴”〉)) |
58 | | eqid 2738 |
. . 3
⊢ ((𝑇‘𝐸)‘(𝑁 − 1)) = ((𝑇‘𝐸)‘(𝑁 − 1)) |
59 | 33, 34, 35, 36, 4, 56, 57, 1, 8, 58 | signsvtp 32562 |
. 2
⊢ ((𝜑 ∧ 0 < (𝐴 · ((𝑇‘𝐸)‘(𝑁 − 1)))) → (𝑉‘𝐹) = (𝑉‘𝐸)) |
60 | 55, 59 | syldan 591 |
1
⊢ ((𝜑 ∧ 0 < (𝐵 · 𝐴)) → (𝑉‘𝐹) = (𝑉‘𝐸)) |