Step | Hyp | Ref
| Expression |
1 | | simpll 763 |
. . 3
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝑁 ∈ (0..^(♯‘𝐹))) → 𝐹 ∈ (Word ℝ ∖
{∅})) |
2 | 1 | eldifad 3871 |
. 2
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝑁 ∈ (0..^(♯‘𝐹))) → 𝐹 ∈ Word ℝ) |
3 | | eldifsni 4629 |
. . . 4
⊢ (𝐹 ∈ (Word ℝ ∖
{∅}) → 𝐹 ≠
∅) |
4 | 3 | ad2antrr 722 |
. . 3
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝑁 ∈ (0..^(♯‘𝐹))) → 𝐹 ≠ ∅) |
5 | | simplr 765 |
. . 3
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝑁 ∈ (0..^(♯‘𝐹))) → (𝐹‘0) ≠ 0) |
6 | 4, 5 | jca 512 |
. 2
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝑁 ∈ (0..^(♯‘𝐹))) → (𝐹 ≠ ∅ ∧ (𝐹‘0) ≠ 0)) |
7 | | simpr 485 |
. 2
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝑁 ∈ (0..^(♯‘𝐹))) → 𝑁 ∈ (0..^(♯‘𝐹))) |
8 | | simprr 769 |
. . 3
⊢ ((𝐹 ∈ Word ℝ ∧
((𝐹 ≠ ∅ ∧
(𝐹‘0) ≠ 0) ∧
𝑁 ∈
(0..^(♯‘𝐹))))
→ 𝑁 ∈
(0..^(♯‘𝐹))) |
9 | | neeq1 3046 |
. . . . . . . 8
⊢ (𝑔 = ∅ → (𝑔 ≠ ∅ ↔ ∅
≠ ∅)) |
10 | | fveq1 6537 |
. . . . . . . . 9
⊢ (𝑔 = ∅ → (𝑔‘0) =
(∅‘0)) |
11 | 10 | neeq1d 3043 |
. . . . . . . 8
⊢ (𝑔 = ∅ → ((𝑔‘0) ≠ 0 ↔
(∅‘0) ≠ 0)) |
12 | 9, 11 | anbi12d 630 |
. . . . . . 7
⊢ (𝑔 = ∅ → ((𝑔 ≠ ∅ ∧ (𝑔‘0) ≠ 0) ↔
(∅ ≠ ∅ ∧ (∅‘0) ≠ 0))) |
13 | | fveq2 6538 |
. . . . . . . . 9
⊢ (𝑔 = ∅ →
(♯‘𝑔) =
(♯‘∅)) |
14 | 13 | oveq2d 7032 |
. . . . . . . 8
⊢ (𝑔 = ∅ →
(0..^(♯‘𝑔)) =
(0..^(♯‘∅))) |
15 | | fveq2 6538 |
. . . . . . . . . 10
⊢ (𝑔 = ∅ → (𝑇‘𝑔) = (𝑇‘∅)) |
16 | 15 | fveq1d 6540 |
. . . . . . . . 9
⊢ (𝑔 = ∅ → ((𝑇‘𝑔)‘𝑚) = ((𝑇‘∅)‘𝑚)) |
17 | 16 | neeq1d 3043 |
. . . . . . . 8
⊢ (𝑔 = ∅ → (((𝑇‘𝑔)‘𝑚) ≠ 0 ↔ ((𝑇‘∅)‘𝑚) ≠ 0)) |
18 | 14, 17 | raleqbidv 3361 |
. . . . . . 7
⊢ (𝑔 = ∅ → (∀𝑚 ∈
(0..^(♯‘𝑔))((𝑇‘𝑔)‘𝑚) ≠ 0 ↔ ∀𝑚 ∈ (0..^(♯‘∅))((𝑇‘∅)‘𝑚) ≠ 0)) |
19 | 12, 18 | imbi12d 346 |
. . . . . 6
⊢ (𝑔 = ∅ → (((𝑔 ≠ ∅ ∧ (𝑔‘0) ≠ 0) →
∀𝑚 ∈
(0..^(♯‘𝑔))((𝑇‘𝑔)‘𝑚) ≠ 0) ↔ ((∅ ≠ ∅ ∧
(∅‘0) ≠ 0) → ∀𝑚 ∈ (0..^(♯‘∅))((𝑇‘∅)‘𝑚) ≠ 0))) |
20 | | neeq1 3046 |
. . . . . . . 8
⊢ (𝑔 = 𝑒 → (𝑔 ≠ ∅ ↔ 𝑒 ≠ ∅)) |
21 | | fveq1 6537 |
. . . . . . . . 9
⊢ (𝑔 = 𝑒 → (𝑔‘0) = (𝑒‘0)) |
22 | 21 | neeq1d 3043 |
. . . . . . . 8
⊢ (𝑔 = 𝑒 → ((𝑔‘0) ≠ 0 ↔ (𝑒‘0) ≠ 0)) |
23 | 20, 22 | anbi12d 630 |
. . . . . . 7
⊢ (𝑔 = 𝑒 → ((𝑔 ≠ ∅ ∧ (𝑔‘0) ≠ 0) ↔ (𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0))) |
24 | | fveq2 6538 |
. . . . . . . . 9
⊢ (𝑔 = 𝑒 → (♯‘𝑔) = (♯‘𝑒)) |
25 | 24 | oveq2d 7032 |
. . . . . . . 8
⊢ (𝑔 = 𝑒 → (0..^(♯‘𝑔)) = (0..^(♯‘𝑒))) |
26 | | fveq2 6538 |
. . . . . . . . . 10
⊢ (𝑔 = 𝑒 → (𝑇‘𝑔) = (𝑇‘𝑒)) |
27 | 26 | fveq1d 6540 |
. . . . . . . . 9
⊢ (𝑔 = 𝑒 → ((𝑇‘𝑔)‘𝑚) = ((𝑇‘𝑒)‘𝑚)) |
28 | 27 | neeq1d 3043 |
. . . . . . . 8
⊢ (𝑔 = 𝑒 → (((𝑇‘𝑔)‘𝑚) ≠ 0 ↔ ((𝑇‘𝑒)‘𝑚) ≠ 0)) |
29 | 25, 28 | raleqbidv 3361 |
. . . . . . 7
⊢ (𝑔 = 𝑒 → (∀𝑚 ∈ (0..^(♯‘𝑔))((𝑇‘𝑔)‘𝑚) ≠ 0 ↔ ∀𝑚 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑚) ≠ 0)) |
30 | 23, 29 | imbi12d 346 |
. . . . . 6
⊢ (𝑔 = 𝑒 → (((𝑔 ≠ ∅ ∧ (𝑔‘0) ≠ 0) → ∀𝑚 ∈
(0..^(♯‘𝑔))((𝑇‘𝑔)‘𝑚) ≠ 0) ↔ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑚 ∈
(0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑚) ≠ 0))) |
31 | | neeq1 3046 |
. . . . . . . 8
⊢ (𝑔 = (𝑒 ++ 〈“𝑘”〉) → (𝑔 ≠ ∅ ↔ (𝑒 ++ 〈“𝑘”〉) ≠
∅)) |
32 | | fveq1 6537 |
. . . . . . . . 9
⊢ (𝑔 = (𝑒 ++ 〈“𝑘”〉) → (𝑔‘0) = ((𝑒 ++ 〈“𝑘”〉)‘0)) |
33 | 32 | neeq1d 3043 |
. . . . . . . 8
⊢ (𝑔 = (𝑒 ++ 〈“𝑘”〉) → ((𝑔‘0) ≠ 0 ↔ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠
0)) |
34 | 31, 33 | anbi12d 630 |
. . . . . . 7
⊢ (𝑔 = (𝑒 ++ 〈“𝑘”〉) → ((𝑔 ≠ ∅ ∧ (𝑔‘0) ≠ 0) ↔ ((𝑒 ++ 〈“𝑘”〉) ≠ ∅ ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠
0))) |
35 | | fveq2 6538 |
. . . . . . . . 9
⊢ (𝑔 = (𝑒 ++ 〈“𝑘”〉) → (♯‘𝑔) = (♯‘(𝑒 ++ 〈“𝑘”〉))) |
36 | 35 | oveq2d 7032 |
. . . . . . . 8
⊢ (𝑔 = (𝑒 ++ 〈“𝑘”〉) →
(0..^(♯‘𝑔)) =
(0..^(♯‘(𝑒 ++
〈“𝑘”〉)))) |
37 | | fveq2 6538 |
. . . . . . . . . 10
⊢ (𝑔 = (𝑒 ++ 〈“𝑘”〉) → (𝑇‘𝑔) = (𝑇‘(𝑒 ++ 〈“𝑘”〉))) |
38 | 37 | fveq1d 6540 |
. . . . . . . . 9
⊢ (𝑔 = (𝑒 ++ 〈“𝑘”〉) → ((𝑇‘𝑔)‘𝑚) = ((𝑇‘(𝑒 ++ 〈“𝑘”〉))‘𝑚)) |
39 | 38 | neeq1d 3043 |
. . . . . . . 8
⊢ (𝑔 = (𝑒 ++ 〈“𝑘”〉) → (((𝑇‘𝑔)‘𝑚) ≠ 0 ↔ ((𝑇‘(𝑒 ++ 〈“𝑘”〉))‘𝑚) ≠ 0)) |
40 | 36, 39 | raleqbidv 3361 |
. . . . . . 7
⊢ (𝑔 = (𝑒 ++ 〈“𝑘”〉) → (∀𝑚 ∈
(0..^(♯‘𝑔))((𝑇‘𝑔)‘𝑚) ≠ 0 ↔ ∀𝑚 ∈ (0..^(♯‘(𝑒 ++ 〈“𝑘”〉)))((𝑇‘(𝑒 ++ 〈“𝑘”〉))‘𝑚) ≠ 0)) |
41 | 34, 40 | imbi12d 346 |
. . . . . 6
⊢ (𝑔 = (𝑒 ++ 〈“𝑘”〉) → (((𝑔 ≠ ∅ ∧ (𝑔‘0) ≠ 0) → ∀𝑚 ∈
(0..^(♯‘𝑔))((𝑇‘𝑔)‘𝑚) ≠ 0) ↔ (((𝑒 ++ 〈“𝑘”〉) ≠ ∅ ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0)
→ ∀𝑚 ∈
(0..^(♯‘(𝑒 ++
〈“𝑘”〉)))((𝑇‘(𝑒 ++ 〈“𝑘”〉))‘𝑚) ≠ 0))) |
42 | | neeq1 3046 |
. . . . . . . 8
⊢ (𝑔 = 𝐹 → (𝑔 ≠ ∅ ↔ 𝐹 ≠ ∅)) |
43 | | fveq1 6537 |
. . . . . . . . 9
⊢ (𝑔 = 𝐹 → (𝑔‘0) = (𝐹‘0)) |
44 | 43 | neeq1d 3043 |
. . . . . . . 8
⊢ (𝑔 = 𝐹 → ((𝑔‘0) ≠ 0 ↔ (𝐹‘0) ≠ 0)) |
45 | 42, 44 | anbi12d 630 |
. . . . . . 7
⊢ (𝑔 = 𝐹 → ((𝑔 ≠ ∅ ∧ (𝑔‘0) ≠ 0) ↔ (𝐹 ≠ ∅ ∧ (𝐹‘0) ≠ 0))) |
46 | | fveq2 6538 |
. . . . . . . . 9
⊢ (𝑔 = 𝐹 → (♯‘𝑔) = (♯‘𝐹)) |
47 | 46 | oveq2d 7032 |
. . . . . . . 8
⊢ (𝑔 = 𝐹 → (0..^(♯‘𝑔)) = (0..^(♯‘𝐹))) |
48 | | fveq2 6538 |
. . . . . . . . . 10
⊢ (𝑔 = 𝐹 → (𝑇‘𝑔) = (𝑇‘𝐹)) |
49 | 48 | fveq1d 6540 |
. . . . . . . . 9
⊢ (𝑔 = 𝐹 → ((𝑇‘𝑔)‘𝑚) = ((𝑇‘𝐹)‘𝑚)) |
50 | 49 | neeq1d 3043 |
. . . . . . . 8
⊢ (𝑔 = 𝐹 → (((𝑇‘𝑔)‘𝑚) ≠ 0 ↔ ((𝑇‘𝐹)‘𝑚) ≠ 0)) |
51 | 47, 50 | raleqbidv 3361 |
. . . . . . 7
⊢ (𝑔 = 𝐹 → (∀𝑚 ∈ (0..^(♯‘𝑔))((𝑇‘𝑔)‘𝑚) ≠ 0 ↔ ∀𝑚 ∈ (0..^(♯‘𝐹))((𝑇‘𝐹)‘𝑚) ≠ 0)) |
52 | 45, 51 | imbi12d 346 |
. . . . . 6
⊢ (𝑔 = 𝐹 → (((𝑔 ≠ ∅ ∧ (𝑔‘0) ≠ 0) → ∀𝑚 ∈
(0..^(♯‘𝑔))((𝑇‘𝑔)‘𝑚) ≠ 0) ↔ ((𝐹 ≠ ∅ ∧ (𝐹‘0) ≠ 0) → ∀𝑚 ∈
(0..^(♯‘𝐹))((𝑇‘𝐹)‘𝑚) ≠ 0))) |
53 | | neirr 2993 |
. . . . . . . 8
⊢ ¬
∅ ≠ ∅ |
54 | 53 | intnanr 488 |
. . . . . . 7
⊢ ¬
(∅ ≠ ∅ ∧ (∅‘0) ≠ 0) |
55 | 54 | pm2.21i 119 |
. . . . . 6
⊢ ((∅
≠ ∅ ∧ (∅‘0) ≠ 0) → ∀𝑚 ∈ (0..^(♯‘∅))((𝑇‘∅)‘𝑚) ≠ 0) |
56 | | fveq2 6538 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑚 → ((𝑇‘𝑒)‘𝑛) = ((𝑇‘𝑒)‘𝑚)) |
57 | 56 | neeq1d 3043 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑚 → (((𝑇‘𝑒)‘𝑛) ≠ 0 ↔ ((𝑇‘𝑒)‘𝑚) ≠ 0)) |
58 | 57 | cbvralv 3403 |
. . . . . . . . . 10
⊢
(∀𝑛 ∈
(0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0 ↔ ∀𝑚 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑚) ≠ 0) |
59 | 58 | imbi2i 337 |
. . . . . . . . 9
⊢ (((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) →
∀𝑛 ∈
(0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0) ↔ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑚 ∈
(0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑚) ≠ 0)) |
60 | 59 | anbi2i 622 |
. . . . . . . 8
⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) →
∀𝑛 ∈
(0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ↔ ((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑚 ∈
(0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑚) ≠ 0))) |
61 | | simplr 765 |
. . . . . . . . . . . 12
⊢
(((((((𝑒 ∈ Word
ℝ ∧ 𝑘 ∈
ℝ) ∧ ((𝑒 ≠
∅ ∧ (𝑒‘0)
≠ 0) → ∀𝑛
∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ 〈“𝑘”〉) ≠ ∅ ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0))
∧ 𝑚 ∈
(0..^(♯‘(𝑒 ++
〈“𝑘”〉)))) ∧ 𝑚 ∈ (0..^(♯‘𝑒))) ∧ 𝑒 = ∅) → 𝑚 ∈ (0..^(♯‘𝑒))) |
62 | | noel 4216 |
. . . . . . . . . . . . . 14
⊢ ¬
𝑚 ∈
∅ |
63 | | fveq2 6538 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑒 = ∅ →
(♯‘𝑒) =
(♯‘∅)) |
64 | | hash0 13578 |
. . . . . . . . . . . . . . . . . 18
⊢
(♯‘∅) = 0 |
65 | 63, 64 | syl6eq 2847 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑒 = ∅ →
(♯‘𝑒) =
0) |
66 | 65 | oveq2d 7032 |
. . . . . . . . . . . . . . . 16
⊢ (𝑒 = ∅ →
(0..^(♯‘𝑒)) =
(0..^0)) |
67 | | fzo0 12911 |
. . . . . . . . . . . . . . . 16
⊢ (0..^0) =
∅ |
68 | 66, 67 | syl6eq 2847 |
. . . . . . . . . . . . . . 15
⊢ (𝑒 = ∅ →
(0..^(♯‘𝑒)) =
∅) |
69 | 68 | eleq2d 2868 |
. . . . . . . . . . . . . 14
⊢ (𝑒 = ∅ → (𝑚 ∈
(0..^(♯‘𝑒))
↔ 𝑚 ∈
∅)) |
70 | 62, 69 | mtbiri 328 |
. . . . . . . . . . . . 13
⊢ (𝑒 = ∅ → ¬ 𝑚 ∈
(0..^(♯‘𝑒))) |
71 | 70 | adantl 482 |
. . . . . . . . . . . 12
⊢
(((((((𝑒 ∈ Word
ℝ ∧ 𝑘 ∈
ℝ) ∧ ((𝑒 ≠
∅ ∧ (𝑒‘0)
≠ 0) → ∀𝑛
∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ 〈“𝑘”〉) ≠ ∅ ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0))
∧ 𝑚 ∈
(0..^(♯‘(𝑒 ++
〈“𝑘”〉)))) ∧ 𝑚 ∈ (0..^(♯‘𝑒))) ∧ 𝑒 = ∅) → ¬ 𝑚 ∈ (0..^(♯‘𝑒))) |
72 | 61, 71 | pm2.21dd 196 |
. . . . . . . . . . 11
⊢
(((((((𝑒 ∈ Word
ℝ ∧ 𝑘 ∈
ℝ) ∧ ((𝑒 ≠
∅ ∧ (𝑒‘0)
≠ 0) → ∀𝑛
∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ 〈“𝑘”〉) ≠ ∅ ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0))
∧ 𝑚 ∈
(0..^(♯‘(𝑒 ++
〈“𝑘”〉)))) ∧ 𝑚 ∈ (0..^(♯‘𝑒))) ∧ 𝑒 = ∅) → ((𝑇‘(𝑒 ++ 〈“𝑘”〉))‘𝑚) ≠ 0) |
73 | | simp-6l 783 |
. . . . . . . . . . . . 13
⊢
(((((((𝑒 ∈ Word
ℝ ∧ 𝑘 ∈
ℝ) ∧ ((𝑒 ≠
∅ ∧ (𝑒‘0)
≠ 0) → ∀𝑛
∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ 〈“𝑘”〉) ≠ ∅ ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0))
∧ 𝑚 ∈
(0..^(♯‘(𝑒 ++
〈“𝑘”〉)))) ∧ 𝑚 ∈ (0..^(♯‘𝑒))) ∧ 𝑒 ≠ ∅) → 𝑒 ∈ Word ℝ) |
74 | | simp-6r 784 |
. . . . . . . . . . . . 13
⊢
(((((((𝑒 ∈ Word
ℝ ∧ 𝑘 ∈
ℝ) ∧ ((𝑒 ≠
∅ ∧ (𝑒‘0)
≠ 0) → ∀𝑛
∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ 〈“𝑘”〉) ≠ ∅ ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0))
∧ 𝑚 ∈
(0..^(♯‘(𝑒 ++
〈“𝑘”〉)))) ∧ 𝑚 ∈ (0..^(♯‘𝑒))) ∧ 𝑒 ≠ ∅) → 𝑘 ∈ ℝ) |
75 | | simplr 765 |
. . . . . . . . . . . . 13
⊢
(((((((𝑒 ∈ Word
ℝ ∧ 𝑘 ∈
ℝ) ∧ ((𝑒 ≠
∅ ∧ (𝑒‘0)
≠ 0) → ∀𝑛
∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ 〈“𝑘”〉) ≠ ∅ ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0))
∧ 𝑚 ∈
(0..^(♯‘(𝑒 ++
〈“𝑘”〉)))) ∧ 𝑚 ∈ (0..^(♯‘𝑒))) ∧ 𝑒 ≠ ∅) → 𝑚 ∈ (0..^(♯‘𝑒))) |
76 | | signsv.p |
. . . . . . . . . . . . . 14
⊢ ⨣ =
(𝑎 ∈ {-1, 0, 1}, 𝑏 ∈ {-1, 0, 1} ↦
if(𝑏 = 0, 𝑎, 𝑏)) |
77 | | signsv.w |
. . . . . . . . . . . . . 14
⊢ 𝑊 = {〈(Base‘ndx), {-1,
0, 1}〉, 〈(+g‘ndx), ⨣
〉} |
78 | | signsv.t |
. . . . . . . . . . . . . 14
⊢ 𝑇 = (𝑓 ∈ Word ℝ ↦ (𝑛 ∈
(0..^(♯‘𝑓))
↦ (𝑊
Σg (𝑖 ∈ (0...𝑛) ↦ (sgn‘(𝑓‘𝑖)))))) |
79 | | signsv.v |
. . . . . . . . . . . . . 14
⊢ 𝑉 = (𝑓 ∈ Word ℝ ↦ Σ𝑗 ∈
(1..^(♯‘𝑓))if(((𝑇‘𝑓)‘𝑗) ≠ ((𝑇‘𝑓)‘(𝑗 − 1)), 1, 0)) |
80 | 76, 77, 78, 79 | signstfvp 31458 |
. . . . . . . . . . . . 13
⊢ ((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ ∧ 𝑚 ∈
(0..^(♯‘𝑒)))
→ ((𝑇‘(𝑒 ++ 〈“𝑘”〉))‘𝑚) = ((𝑇‘𝑒)‘𝑚)) |
81 | 73, 74, 75, 80 | syl3anc 1364 |
. . . . . . . . . . . 12
⊢
(((((((𝑒 ∈ Word
ℝ ∧ 𝑘 ∈
ℝ) ∧ ((𝑒 ≠
∅ ∧ (𝑒‘0)
≠ 0) → ∀𝑛
∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ 〈“𝑘”〉) ≠ ∅ ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0))
∧ 𝑚 ∈
(0..^(♯‘(𝑒 ++
〈“𝑘”〉)))) ∧ 𝑚 ∈ (0..^(♯‘𝑒))) ∧ 𝑒 ≠ ∅) → ((𝑇‘(𝑒 ++ 〈“𝑘”〉))‘𝑚) = ((𝑇‘𝑒)‘𝑚)) |
82 | | simpr 485 |
. . . . . . . . . . . . . 14
⊢
(((((((𝑒 ∈ Word
ℝ ∧ 𝑘 ∈
ℝ) ∧ ((𝑒 ≠
∅ ∧ (𝑒‘0)
≠ 0) → ∀𝑛
∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ 〈“𝑘”〉) ≠ ∅ ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0))
∧ 𝑚 ∈
(0..^(♯‘(𝑒 ++
〈“𝑘”〉)))) ∧ 𝑚 ∈ (0..^(♯‘𝑒))) ∧ 𝑒 ≠ ∅) → 𝑒 ≠ ∅) |
83 | | simplll 771 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑒 ∈ Word
ℝ ∧ 𝑘 ∈
ℝ) ∧ ((𝑒 ≠
∅ ∧ (𝑒‘0)
≠ 0) → ∀𝑛
∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ 〈“𝑘”〉) ≠ ∅ ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0))
∧ 𝑚 ∈
(0..^(♯‘(𝑒 ++
〈“𝑘”〉)))) → (𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ)) |
84 | 83 | ad2antrr 722 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝑒 ∈ Word
ℝ ∧ 𝑘 ∈
ℝ) ∧ ((𝑒 ≠
∅ ∧ (𝑒‘0)
≠ 0) → ∀𝑛
∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ 〈“𝑘”〉) ≠ ∅ ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0))
∧ 𝑚 ∈
(0..^(♯‘(𝑒 ++
〈“𝑘”〉)))) ∧ 𝑚 ∈ (0..^(♯‘𝑒))) ∧ 𝑒 ≠ ∅) → (𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ)) |
85 | | simplrr 774 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑒 ∈ Word
ℝ ∧ 𝑘 ∈
ℝ) ∧ ((𝑒 ≠
∅ ∧ (𝑒‘0)
≠ 0) → ∀𝑛
∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ 〈“𝑘”〉) ≠ ∅ ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0))
∧ (𝑚 ∈
(0..^(♯‘(𝑒 ++
〈“𝑘”〉))) ∧ 𝑚 ∈ (0..^(♯‘𝑒)) ∧ 𝑒 ≠ ∅)) → ((𝑒 ++ 〈“𝑘”〉)‘0) ≠
0) |
86 | 85 | 3anassrs 1353 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝑒 ∈ Word
ℝ ∧ 𝑘 ∈
ℝ) ∧ ((𝑒 ≠
∅ ∧ (𝑒‘0)
≠ 0) → ∀𝑛
∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ 〈“𝑘”〉) ≠ ∅ ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0))
∧ 𝑚 ∈
(0..^(♯‘(𝑒 ++
〈“𝑘”〉)))) ∧ 𝑚 ∈ (0..^(♯‘𝑒))) ∧ 𝑒 ≠ ∅) → ((𝑒 ++ 〈“𝑘”〉)‘0) ≠
0) |
87 | | simpll 763 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ 𝑒 ≠ ∅) → 𝑒 ∈ Word
ℝ) |
88 | | simplr 765 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ 𝑒 ≠ ∅) → 𝑘 ∈
ℝ) |
89 | 88 | s1cld 13801 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ 𝑒 ≠ ∅) →
〈“𝑘”〉
∈ Word ℝ) |
90 | | lennncl 13730 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑒 ∈ Word ℝ ∧ 𝑒 ≠ ∅) →
(♯‘𝑒) ∈
ℕ) |
91 | 90 | adantlr 711 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ 𝑒 ≠ ∅) →
(♯‘𝑒) ∈
ℕ) |
92 | | fzo0end 12979 |
. . . . . . . . . . . . . . . . . . 19
⊢
((♯‘𝑒)
∈ ℕ → ((♯‘𝑒) − 1) ∈ (0..^(♯‘𝑒))) |
93 | | elfzolt3b 12900 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((♯‘𝑒)
− 1) ∈ (0..^(♯‘𝑒)) → 0 ∈ (0..^(♯‘𝑒))) |
94 | 91, 92, 93 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ 𝑒 ≠ ∅) → 0 ∈
(0..^(♯‘𝑒))) |
95 | | ccatval1 13775 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑒 ∈ Word ℝ ∧
〈“𝑘”〉
∈ Word ℝ ∧ 0 ∈ (0..^(♯‘𝑒))) → ((𝑒 ++ 〈“𝑘”〉)‘0) = (𝑒‘0)) |
96 | 87, 89, 94, 95 | syl3anc 1364 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ 𝑒 ≠ ∅) → ((𝑒 ++ 〈“𝑘”〉)‘0) = (𝑒‘0)) |
97 | 96 | neeq1d 3043 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ 𝑒 ≠ ∅) → (((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0
↔ (𝑒‘0) ≠
0)) |
98 | 97 | biimpa 477 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ 𝑒 ≠ ∅) ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0)
→ (𝑒‘0) ≠
0) |
99 | 84, 82, 86, 98 | syl21anc 834 |
. . . . . . . . . . . . . 14
⊢
(((((((𝑒 ∈ Word
ℝ ∧ 𝑘 ∈
ℝ) ∧ ((𝑒 ≠
∅ ∧ (𝑒‘0)
≠ 0) → ∀𝑛
∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ 〈“𝑘”〉) ≠ ∅ ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0))
∧ 𝑚 ∈
(0..^(♯‘(𝑒 ++
〈“𝑘”〉)))) ∧ 𝑚 ∈ (0..^(♯‘𝑒))) ∧ 𝑒 ≠ ∅) → (𝑒‘0) ≠ 0) |
100 | | simp-5r 782 |
. . . . . . . . . . . . . 14
⊢
(((((((𝑒 ∈ Word
ℝ ∧ 𝑘 ∈
ℝ) ∧ ((𝑒 ≠
∅ ∧ (𝑒‘0)
≠ 0) → ∀𝑛
∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ 〈“𝑘”〉) ≠ ∅ ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0))
∧ 𝑚 ∈
(0..^(♯‘(𝑒 ++
〈“𝑘”〉)))) ∧ 𝑚 ∈ (0..^(♯‘𝑒))) ∧ 𝑒 ≠ ∅) → ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈
(0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) |
101 | 82, 99, 100 | mp2and 695 |
. . . . . . . . . . . . 13
⊢
(((((((𝑒 ∈ Word
ℝ ∧ 𝑘 ∈
ℝ) ∧ ((𝑒 ≠
∅ ∧ (𝑒‘0)
≠ 0) → ∀𝑛
∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ 〈“𝑘”〉) ≠ ∅ ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0))
∧ 𝑚 ∈
(0..^(♯‘(𝑒 ++
〈“𝑘”〉)))) ∧ 𝑚 ∈ (0..^(♯‘𝑒))) ∧ 𝑒 ≠ ∅) → ∀𝑛 ∈
(0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0) |
102 | 57 | rspcva 3557 |
. . . . . . . . . . . . 13
⊢ ((𝑚 ∈
(0..^(♯‘𝑒))
∧ ∀𝑛 ∈
(0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0) → ((𝑇‘𝑒)‘𝑚) ≠ 0) |
103 | 75, 101, 102 | syl2anc 584 |
. . . . . . . . . . . 12
⊢
(((((((𝑒 ∈ Word
ℝ ∧ 𝑘 ∈
ℝ) ∧ ((𝑒 ≠
∅ ∧ (𝑒‘0)
≠ 0) → ∀𝑛
∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ 〈“𝑘”〉) ≠ ∅ ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0))
∧ 𝑚 ∈
(0..^(♯‘(𝑒 ++
〈“𝑘”〉)))) ∧ 𝑚 ∈ (0..^(♯‘𝑒))) ∧ 𝑒 ≠ ∅) → ((𝑇‘𝑒)‘𝑚) ≠ 0) |
104 | 81, 103 | eqnetrd 3051 |
. . . . . . . . . . 11
⊢
(((((((𝑒 ∈ Word
ℝ ∧ 𝑘 ∈
ℝ) ∧ ((𝑒 ≠
∅ ∧ (𝑒‘0)
≠ 0) → ∀𝑛
∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ 〈“𝑘”〉) ≠ ∅ ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0))
∧ 𝑚 ∈
(0..^(♯‘(𝑒 ++
〈“𝑘”〉)))) ∧ 𝑚 ∈ (0..^(♯‘𝑒))) ∧ 𝑒 ≠ ∅) → ((𝑇‘(𝑒 ++ 〈“𝑘”〉))‘𝑚) ≠ 0) |
105 | 72, 104 | pm2.61dane 3072 |
. . . . . . . . . 10
⊢
((((((𝑒 ∈ Word
ℝ ∧ 𝑘 ∈
ℝ) ∧ ((𝑒 ≠
∅ ∧ (𝑒‘0)
≠ 0) → ∀𝑛
∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ 〈“𝑘”〉) ≠ ∅ ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0))
∧ 𝑚 ∈
(0..^(♯‘(𝑒 ++
〈“𝑘”〉)))) ∧ 𝑚 ∈ (0..^(♯‘𝑒))) → ((𝑇‘(𝑒 ++ 〈“𝑘”〉))‘𝑚) ≠ 0) |
106 | | simpr 485 |
. . . . . . . . . . . 12
⊢
((((((𝑒 ∈ Word
ℝ ∧ 𝑘 ∈
ℝ) ∧ ((𝑒 ≠
∅ ∧ (𝑒‘0)
≠ 0) → ∀𝑛
∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ 〈“𝑘”〉) ≠ ∅ ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0))
∧ 𝑚 ∈
(0..^(♯‘(𝑒 ++
〈“𝑘”〉)))) ∧ 𝑚 = (♯‘𝑒)) → 𝑚 = (♯‘𝑒)) |
107 | 106 | fveq2d 6542 |
. . . . . . . . . . 11
⊢
((((((𝑒 ∈ Word
ℝ ∧ 𝑘 ∈
ℝ) ∧ ((𝑒 ≠
∅ ∧ (𝑒‘0)
≠ 0) → ∀𝑛
∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ 〈“𝑘”〉) ≠ ∅ ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0))
∧ 𝑚 ∈
(0..^(♯‘(𝑒 ++
〈“𝑘”〉)))) ∧ 𝑚 = (♯‘𝑒)) → ((𝑇‘(𝑒 ++ 〈“𝑘”〉))‘𝑚) = ((𝑇‘(𝑒 ++ 〈“𝑘”〉))‘(♯‘𝑒))) |
108 | | simpr 485 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑒 ∈ Word
ℝ ∧ 𝑘 ∈
ℝ) ∧ ((𝑒 ≠
∅ ∧ (𝑒‘0)
≠ 0) → ∀𝑛
∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ 〈“𝑘”〉) ≠ ∅ ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0)
∧ 𝑚 ∈
(0..^(♯‘(𝑒 ++
〈“𝑘”〉))))) ∧ 𝑒 = ∅) → 𝑒 = ∅) |
109 | | simp-4r 780 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑒 ∈ Word
ℝ ∧ 𝑘 ∈
ℝ) ∧ ((𝑒 ≠
∅ ∧ (𝑒‘0)
≠ 0) → ∀𝑛
∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ 〈“𝑘”〉) ≠ ∅ ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0)
∧ 𝑚 ∈
(0..^(♯‘(𝑒 ++
〈“𝑘”〉))))) ∧ 𝑒 = ∅) → 𝑘 ∈ ℝ) |
110 | | simplrl 773 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑒 ∈ Word
ℝ ∧ 𝑘 ∈
ℝ) ∧ ((𝑒 ≠
∅ ∧ (𝑒‘0)
≠ 0) → ∀𝑛
∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ 〈“𝑘”〉) ≠ ∅ ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0)
∧ 𝑚 ∈
(0..^(♯‘(𝑒 ++
〈“𝑘”〉))))) ∧ 𝑒 = ∅) → ((𝑒 ++ 〈“𝑘”〉) ≠ ∅ ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠
0)) |
111 | 110 | simprd 496 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑒 ∈ Word
ℝ ∧ 𝑘 ∈
ℝ) ∧ ((𝑒 ≠
∅ ∧ (𝑒‘0)
≠ 0) → ∀𝑛
∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ 〈“𝑘”〉) ≠ ∅ ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0)
∧ 𝑚 ∈
(0..^(♯‘(𝑒 ++
〈“𝑘”〉))))) ∧ 𝑒 = ∅) → ((𝑒 ++ 〈“𝑘”〉)‘0) ≠
0) |
112 | | oveq1 7023 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑒 = ∅ → (𝑒 ++ 〈“𝑘”〉) = (∅ ++
〈“𝑘”〉)) |
113 | | s1cl 13800 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑘 ∈ ℝ →
〈“𝑘”〉
∈ Word ℝ) |
114 | | ccatlid 13784 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(〈“𝑘”〉 ∈ Word ℝ →
(∅ ++ 〈“𝑘”〉) = 〈“𝑘”〉) |
115 | 113, 114 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑘 ∈ ℝ → (∅
++ 〈“𝑘”〉) = 〈“𝑘”〉) |
116 | 112, 115 | sylan9eq 2851 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) → (𝑒 ++ 〈“𝑘”〉) =
〈“𝑘”〉) |
117 | 116 | fveq2d 6542 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) → (𝑇‘(𝑒 ++ 〈“𝑘”〉)) = (𝑇‘〈“𝑘”〉)) |
118 | 117 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0)
→ (𝑇‘(𝑒 ++ 〈“𝑘”〉)) = (𝑇‘〈“𝑘”〉)) |
119 | | simplr 765 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0)
→ 𝑘 ∈
ℝ) |
120 | 76, 77, 78, 79 | signstf0 31455 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 ∈ ℝ → (𝑇‘〈“𝑘”〉) =
〈“(sgn‘𝑘)”〉) |
121 | 119, 120 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0)
→ (𝑇‘〈“𝑘”〉) =
〈“(sgn‘𝑘)”〉) |
122 | 118, 121 | eqtrd 2831 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0)
→ (𝑇‘(𝑒 ++ 〈“𝑘”〉)) =
〈“(sgn‘𝑘)”〉) |
123 | 65 | ad2antrr 722 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0)
→ (♯‘𝑒) =
0) |
124 | 122, 123 | fveq12d 6545 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0)
→ ((𝑇‘(𝑒 ++ 〈“𝑘”〉))‘(♯‘𝑒)) =
(〈“(sgn‘𝑘)”〉‘0)) |
125 | | sgnclre 31414 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ ℝ →
(sgn‘𝑘) ∈
ℝ) |
126 | | s1fv 13808 |
. . . . . . . . . . . . . . . . . 18
⊢
((sgn‘𝑘)
∈ ℝ → (〈“(sgn‘𝑘)”〉‘0) = (sgn‘𝑘)) |
127 | 119, 125,
126 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0)
→ (〈“(sgn‘𝑘)”〉‘0) = (sgn‘𝑘)) |
128 | 124, 127 | eqtrd 2831 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0)
→ ((𝑇‘(𝑒 ++ 〈“𝑘”〉))‘(♯‘𝑒)) = (sgn‘𝑘)) |
129 | 116 | fveq1d 6540 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) → ((𝑒 ++ 〈“𝑘”〉)‘0) =
(〈“𝑘”〉‘0)) |
130 | | s1fv 13808 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 ∈ ℝ →
(〈“𝑘”〉‘0) = 𝑘) |
131 | 130 | adantl 482 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) →
(〈“𝑘”〉‘0) = 𝑘) |
132 | 129, 131 | eqtrd 2831 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) → ((𝑒 ++ 〈“𝑘”〉)‘0) = 𝑘) |
133 | 132 | neeq1d 3043 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) → (((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0
↔ 𝑘 ≠
0)) |
134 | 133 | biimpa 477 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0)
→ 𝑘 ≠
0) |
135 | | rexr 10533 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 ∈ ℝ → 𝑘 ∈
ℝ*) |
136 | | sgn0bi 31422 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 ∈ ℝ*
→ ((sgn‘𝑘) = 0
↔ 𝑘 =
0)) |
137 | 135, 136 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 ∈ ℝ →
((sgn‘𝑘) = 0 ↔
𝑘 = 0)) |
138 | 137 | necon3bid 3028 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ ℝ →
((sgn‘𝑘) ≠ 0
↔ 𝑘 ≠
0)) |
139 | 138 | biimpar 478 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘 ∈ ℝ ∧ 𝑘 ≠ 0) → (sgn‘𝑘) ≠ 0) |
140 | 119, 134,
139 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0)
→ (sgn‘𝑘) ≠
0) |
141 | 128, 140 | eqnetrd 3051 |
. . . . . . . . . . . . . . 15
⊢ (((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0)
→ ((𝑇‘(𝑒 ++ 〈“𝑘”〉))‘(♯‘𝑒)) ≠ 0) |
142 | 108, 109,
111, 141 | syl21anc 834 |
. . . . . . . . . . . . . 14
⊢
(((((𝑒 ∈ Word
ℝ ∧ 𝑘 ∈
ℝ) ∧ ((𝑒 ≠
∅ ∧ (𝑒‘0)
≠ 0) → ∀𝑛
∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ 〈“𝑘”〉) ≠ ∅ ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0)
∧ 𝑚 ∈
(0..^(♯‘(𝑒 ++
〈“𝑘”〉))))) ∧ 𝑒 = ∅) → ((𝑇‘(𝑒 ++ 〈“𝑘”〉))‘(♯‘𝑒)) ≠ 0) |
143 | | simplll 771 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (((𝑒 ++ 〈“𝑘”〉) ≠ ∅
∧ ((𝑒 ++
〈“𝑘”〉)‘0) ≠ 0) ∧ 𝑚 ∈
(0..^(♯‘(𝑒 ++
〈“𝑘”〉))))) ∧ ¬ 𝑒 = ∅) → 𝑒 ∈ Word
ℝ) |
144 | | simpr 485 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (((𝑒 ++ 〈“𝑘”〉) ≠ ∅
∧ ((𝑒 ++
〈“𝑘”〉)‘0) ≠ 0) ∧ 𝑚 ∈
(0..^(♯‘(𝑒 ++
〈“𝑘”〉))))) ∧ ¬ 𝑒 = ∅) → ¬ 𝑒 = ∅) |
145 | | velsn 4488 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑒 ∈ {∅} ↔ 𝑒 = ∅) |
146 | 144, 145 | sylnibr 330 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (((𝑒 ++ 〈“𝑘”〉) ≠ ∅
∧ ((𝑒 ++
〈“𝑘”〉)‘0) ≠ 0) ∧ 𝑚 ∈
(0..^(♯‘(𝑒 ++
〈“𝑘”〉))))) ∧ ¬ 𝑒 = ∅) → ¬ 𝑒 ∈
{∅}) |
147 | 143, 146 | eldifd 3870 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (((𝑒 ++ 〈“𝑘”〉) ≠ ∅
∧ ((𝑒 ++
〈“𝑘”〉)‘0) ≠ 0) ∧ 𝑚 ∈
(0..^(♯‘(𝑒 ++
〈“𝑘”〉))))) ∧ ¬ 𝑒 = ∅) → 𝑒 ∈ (Word ℝ ∖
{∅})) |
148 | | simpllr 772 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (((𝑒 ++ 〈“𝑘”〉) ≠ ∅
∧ ((𝑒 ++
〈“𝑘”〉)‘0) ≠ 0) ∧ 𝑚 ∈
(0..^(♯‘(𝑒 ++
〈“𝑘”〉))))) ∧ ¬ 𝑒 = ∅) → 𝑘 ∈
ℝ) |
149 | 76, 77, 78, 79 | signstfvn 31456 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑒 ∈ (Word ℝ ∖
{∅}) ∧ 𝑘 ∈
ℝ) → ((𝑇‘(𝑒 ++ 〈“𝑘”〉))‘(♯‘𝑒)) = (((𝑇‘𝑒)‘((♯‘𝑒) − 1)) ⨣ (sgn‘𝑘))) |
150 | 147, 148,
149 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (((𝑒 ++ 〈“𝑘”〉) ≠ ∅
∧ ((𝑒 ++
〈“𝑘”〉)‘0) ≠ 0) ∧ 𝑚 ∈
(0..^(♯‘(𝑒 ++
〈“𝑘”〉))))) ∧ ¬ 𝑒 = ∅) → ((𝑇‘(𝑒 ++ 〈“𝑘”〉))‘(♯‘𝑒)) = (((𝑇‘𝑒)‘((♯‘𝑒) − 1)) ⨣ (sgn‘𝑘))) |
151 | 150 | adantllr 715 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑒 ∈ Word
ℝ ∧ 𝑘 ∈
ℝ) ∧ ((𝑒 ≠
∅ ∧ (𝑒‘0)
≠ 0) → ∀𝑛
∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ 〈“𝑘”〉) ≠ ∅ ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0)
∧ 𝑚 ∈
(0..^(♯‘(𝑒 ++
〈“𝑘”〉))))) ∧ ¬ 𝑒 = ∅) → ((𝑇‘(𝑒 ++ 〈“𝑘”〉))‘(♯‘𝑒)) = (((𝑇‘𝑒)‘((♯‘𝑒) − 1)) ⨣ (sgn‘𝑘))) |
152 | 144 | neqned 2991 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (((𝑒 ++ 〈“𝑘”〉) ≠ ∅
∧ ((𝑒 ++
〈“𝑘”〉)‘0) ≠ 0) ∧ 𝑚 ∈
(0..^(♯‘(𝑒 ++
〈“𝑘”〉))))) ∧ ¬ 𝑒 = ∅) → 𝑒 ≠ ∅) |
153 | 143, 152,
90 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (((𝑒 ++ 〈“𝑘”〉) ≠ ∅
∧ ((𝑒 ++
〈“𝑘”〉)‘0) ≠ 0) ∧ 𝑚 ∈
(0..^(♯‘(𝑒 ++
〈“𝑘”〉))))) ∧ ¬ 𝑒 = ∅) →
(♯‘𝑒) ∈
ℕ) |
154 | 153, 92 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (((𝑒 ++ 〈“𝑘”〉) ≠ ∅
∧ ((𝑒 ++
〈“𝑘”〉)‘0) ≠ 0) ∧ 𝑚 ∈
(0..^(♯‘(𝑒 ++
〈“𝑘”〉))))) ∧ ¬ 𝑒 = ∅) →
((♯‘𝑒) −
1) ∈ (0..^(♯‘𝑒))) |
155 | 76, 77, 78, 79 | signstcl 31452 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑒 ∈ Word ℝ ∧
((♯‘𝑒) −
1) ∈ (0..^(♯‘𝑒))) → ((𝑇‘𝑒)‘((♯‘𝑒) − 1)) ∈ {-1, 0,
1}) |
156 | 143, 154,
155 | syl2anc 584 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (((𝑒 ++ 〈“𝑘”〉) ≠ ∅
∧ ((𝑒 ++
〈“𝑘”〉)‘0) ≠ 0) ∧ 𝑚 ∈
(0..^(♯‘(𝑒 ++
〈“𝑘”〉))))) ∧ ¬ 𝑒 = ∅) → ((𝑇‘𝑒)‘((♯‘𝑒) − 1)) ∈ {-1, 0,
1}) |
157 | 156 | adantllr 715 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑒 ∈ Word
ℝ ∧ 𝑘 ∈
ℝ) ∧ ((𝑒 ≠
∅ ∧ (𝑒‘0)
≠ 0) → ∀𝑛
∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ 〈“𝑘”〉) ≠ ∅ ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0)
∧ 𝑚 ∈
(0..^(♯‘(𝑒 ++
〈“𝑘”〉))))) ∧ ¬ 𝑒 = ∅) → ((𝑇‘𝑒)‘((♯‘𝑒) − 1)) ∈ {-1, 0,
1}) |
158 | 148 | rexrd 10537 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (((𝑒 ++ 〈“𝑘”〉) ≠ ∅
∧ ((𝑒 ++
〈“𝑘”〉)‘0) ≠ 0) ∧ 𝑚 ∈
(0..^(♯‘(𝑒 ++
〈“𝑘”〉))))) ∧ ¬ 𝑒 = ∅) → 𝑘 ∈
ℝ*) |
159 | | sgncl 31413 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ ℝ*
→ (sgn‘𝑘) ∈
{-1, 0, 1}) |
160 | 158, 159 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (((𝑒 ++ 〈“𝑘”〉) ≠ ∅
∧ ((𝑒 ++
〈“𝑘”〉)‘0) ≠ 0) ∧ 𝑚 ∈
(0..^(♯‘(𝑒 ++
〈“𝑘”〉))))) ∧ ¬ 𝑒 = ∅) →
(sgn‘𝑘) ∈ {-1,
0, 1}) |
161 | 160 | adantllr 715 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑒 ∈ Word
ℝ ∧ 𝑘 ∈
ℝ) ∧ ((𝑒 ≠
∅ ∧ (𝑒‘0)
≠ 0) → ∀𝑛
∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ 〈“𝑘”〉) ≠ ∅ ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0)
∧ 𝑚 ∈
(0..^(♯‘(𝑒 ++
〈“𝑘”〉))))) ∧ ¬ 𝑒 = ∅) →
(sgn‘𝑘) ∈ {-1,
0, 1}) |
162 | 154 | adantllr 715 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝑒 ∈ Word
ℝ ∧ 𝑘 ∈
ℝ) ∧ ((𝑒 ≠
∅ ∧ (𝑒‘0)
≠ 0) → ∀𝑛
∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ 〈“𝑘”〉) ≠ ∅ ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0)
∧ 𝑚 ∈
(0..^(♯‘(𝑒 ++
〈“𝑘”〉))))) ∧ ¬ 𝑒 = ∅) →
((♯‘𝑒) −
1) ∈ (0..^(♯‘𝑒))) |
163 | 152 | adantllr 715 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝑒 ∈ Word
ℝ ∧ 𝑘 ∈
ℝ) ∧ ((𝑒 ≠
∅ ∧ (𝑒‘0)
≠ 0) → ∀𝑛
∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ 〈“𝑘”〉) ≠ ∅ ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0)
∧ 𝑚 ∈
(0..^(♯‘(𝑒 ++
〈“𝑘”〉))))) ∧ ¬ 𝑒 = ∅) → 𝑒 ≠ ∅) |
164 | | simplll 771 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝑒 ∈ Word
ℝ ∧ 𝑘 ∈
ℝ) ∧ ((𝑒 ≠
∅ ∧ (𝑒‘0)
≠ 0) → ∀𝑛
∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ 〈“𝑘”〉) ≠ ∅ ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0)
∧ 𝑚 ∈
(0..^(♯‘(𝑒 ++
〈“𝑘”〉))))) ∧ ¬ 𝑒 = ∅) → (𝑒 ∈ Word ℝ ∧ 𝑘 ∈
ℝ)) |
165 | | simplrl 773 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝑒 ∈ Word
ℝ ∧ 𝑘 ∈
ℝ) ∧ ((𝑒 ≠
∅ ∧ (𝑒‘0)
≠ 0) → ∀𝑛
∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ 〈“𝑘”〉) ≠ ∅ ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0)
∧ 𝑚 ∈
(0..^(♯‘(𝑒 ++
〈“𝑘”〉))))) ∧ ¬ 𝑒 = ∅) → ((𝑒 ++ 〈“𝑘”〉) ≠ ∅
∧ ((𝑒 ++
〈“𝑘”〉)‘0) ≠
0)) |
166 | 165 | simprd 496 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝑒 ∈ Word
ℝ ∧ 𝑘 ∈
ℝ) ∧ ((𝑒 ≠
∅ ∧ (𝑒‘0)
≠ 0) → ∀𝑛
∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ 〈“𝑘”〉) ≠ ∅ ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0)
∧ 𝑚 ∈
(0..^(♯‘(𝑒 ++
〈“𝑘”〉))))) ∧ ¬ 𝑒 = ∅) → ((𝑒 ++ 〈“𝑘”〉)‘0) ≠
0) |
167 | 164, 163,
166, 98 | syl21anc 834 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝑒 ∈ Word
ℝ ∧ 𝑘 ∈
ℝ) ∧ ((𝑒 ≠
∅ ∧ (𝑒‘0)
≠ 0) → ∀𝑛
∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ 〈“𝑘”〉) ≠ ∅ ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0)
∧ 𝑚 ∈
(0..^(♯‘(𝑒 ++
〈“𝑘”〉))))) ∧ ¬ 𝑒 = ∅) → (𝑒‘0) ≠
0) |
168 | | simpllr 772 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝑒 ∈ Word
ℝ ∧ 𝑘 ∈
ℝ) ∧ ((𝑒 ≠
∅ ∧ (𝑒‘0)
≠ 0) → ∀𝑛
∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ 〈“𝑘”〉) ≠ ∅ ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0)
∧ 𝑚 ∈
(0..^(♯‘(𝑒 ++
〈“𝑘”〉))))) ∧ ¬ 𝑒 = ∅) → ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) →
∀𝑛 ∈
(0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) |
169 | 163, 167,
168 | mp2and 695 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝑒 ∈ Word
ℝ ∧ 𝑘 ∈
ℝ) ∧ ((𝑒 ≠
∅ ∧ (𝑒‘0)
≠ 0) → ∀𝑛
∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ 〈“𝑘”〉) ≠ ∅ ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0)
∧ 𝑚 ∈
(0..^(♯‘(𝑒 ++
〈“𝑘”〉))))) ∧ ¬ 𝑒 = ∅) → ∀𝑛 ∈
(0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0) |
170 | | fveq2 6538 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 = ((♯‘𝑒) − 1) → ((𝑇‘𝑒)‘𝑛) = ((𝑇‘𝑒)‘((♯‘𝑒) − 1))) |
171 | 170 | neeq1d 3043 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = ((♯‘𝑒) − 1) → (((𝑇‘𝑒)‘𝑛) ≠ 0 ↔ ((𝑇‘𝑒)‘((♯‘𝑒) − 1)) ≠ 0)) |
172 | 171 | rspcva 3557 |
. . . . . . . . . . . . . . . . 17
⊢
((((♯‘𝑒)
− 1) ∈ (0..^(♯‘𝑒)) ∧ ∀𝑛 ∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0) → ((𝑇‘𝑒)‘((♯‘𝑒) − 1)) ≠ 0) |
173 | 162, 169,
172 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑒 ∈ Word
ℝ ∧ 𝑘 ∈
ℝ) ∧ ((𝑒 ≠
∅ ∧ (𝑒‘0)
≠ 0) → ∀𝑛
∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ 〈“𝑘”〉) ≠ ∅ ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0)
∧ 𝑚 ∈
(0..^(♯‘(𝑒 ++
〈“𝑘”〉))))) ∧ ¬ 𝑒 = ∅) → ((𝑇‘𝑒)‘((♯‘𝑒) − 1)) ≠ 0) |
174 | 76, 77 | signswn0 31447 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑇‘𝑒)‘((♯‘𝑒) − 1)) ∈ {-1, 0, 1}
∧ (sgn‘𝑘) ∈
{-1, 0, 1}) ∧ ((𝑇‘𝑒)‘((♯‘𝑒) − 1)) ≠ 0) → (((𝑇‘𝑒)‘((♯‘𝑒) − 1)) ⨣ (sgn‘𝑘)) ≠ 0) |
175 | 157, 161,
173, 174 | syl21anc 834 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑒 ∈ Word
ℝ ∧ 𝑘 ∈
ℝ) ∧ ((𝑒 ≠
∅ ∧ (𝑒‘0)
≠ 0) → ∀𝑛
∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ 〈“𝑘”〉) ≠ ∅ ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0)
∧ 𝑚 ∈
(0..^(♯‘(𝑒 ++
〈“𝑘”〉))))) ∧ ¬ 𝑒 = ∅) → (((𝑇‘𝑒)‘((♯‘𝑒) − 1)) ⨣ (sgn‘𝑘)) ≠ 0) |
176 | 151, 175 | eqnetrd 3051 |
. . . . . . . . . . . . . 14
⊢
(((((𝑒 ∈ Word
ℝ ∧ 𝑘 ∈
ℝ) ∧ ((𝑒 ≠
∅ ∧ (𝑒‘0)
≠ 0) → ∀𝑛
∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ 〈“𝑘”〉) ≠ ∅ ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0)
∧ 𝑚 ∈
(0..^(♯‘(𝑒 ++
〈“𝑘”〉))))) ∧ ¬ 𝑒 = ∅) → ((𝑇‘(𝑒 ++ 〈“𝑘”〉))‘(♯‘𝑒)) ≠ 0) |
177 | 142, 176 | pm2.61dan 809 |
. . . . . . . . . . . . 13
⊢ ((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) →
∀𝑛 ∈
(0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ 〈“𝑘”〉) ≠ ∅ ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0)
∧ 𝑚 ∈
(0..^(♯‘(𝑒 ++
〈“𝑘”〉))))) → ((𝑇‘(𝑒 ++ 〈“𝑘”〉))‘(♯‘𝑒)) ≠ 0) |
178 | 177 | anassrs 468 |
. . . . . . . . . . . 12
⊢
(((((𝑒 ∈ Word
ℝ ∧ 𝑘 ∈
ℝ) ∧ ((𝑒 ≠
∅ ∧ (𝑒‘0)
≠ 0) → ∀𝑛
∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ 〈“𝑘”〉) ≠ ∅ ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0))
∧ 𝑚 ∈
(0..^(♯‘(𝑒 ++
〈“𝑘”〉)))) → ((𝑇‘(𝑒 ++ 〈“𝑘”〉))‘(♯‘𝑒)) ≠ 0) |
179 | 178 | adantr 481 |
. . . . . . . . . . 11
⊢
((((((𝑒 ∈ Word
ℝ ∧ 𝑘 ∈
ℝ) ∧ ((𝑒 ≠
∅ ∧ (𝑒‘0)
≠ 0) → ∀𝑛
∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ 〈“𝑘”〉) ≠ ∅ ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0))
∧ 𝑚 ∈
(0..^(♯‘(𝑒 ++
〈“𝑘”〉)))) ∧ 𝑚 = (♯‘𝑒)) → ((𝑇‘(𝑒 ++ 〈“𝑘”〉))‘(♯‘𝑒)) ≠ 0) |
180 | 107, 179 | eqnetrd 3051 |
. . . . . . . . . 10
⊢
((((((𝑒 ∈ Word
ℝ ∧ 𝑘 ∈
ℝ) ∧ ((𝑒 ≠
∅ ∧ (𝑒‘0)
≠ 0) → ∀𝑛
∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ 〈“𝑘”〉) ≠ ∅ ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0))
∧ 𝑚 ∈
(0..^(♯‘(𝑒 ++
〈“𝑘”〉)))) ∧ 𝑚 = (♯‘𝑒)) → ((𝑇‘(𝑒 ++ 〈“𝑘”〉))‘𝑚) ≠ 0) |
181 | | lencl 13729 |
. . . . . . . . . . . . 13
⊢ (𝑒 ∈ Word ℝ →
(♯‘𝑒) ∈
ℕ0) |
182 | | nn0uz 12129 |
. . . . . . . . . . . . 13
⊢
ℕ0 = (ℤ≥‘0) |
183 | 181, 182 | syl6eleq 2893 |
. . . . . . . . . . . 12
⊢ (𝑒 ∈ Word ℝ →
(♯‘𝑒) ∈
(ℤ≥‘0)) |
184 | 183 | ad4antr 728 |
. . . . . . . . . . 11
⊢
(((((𝑒 ∈ Word
ℝ ∧ 𝑘 ∈
ℝ) ∧ ((𝑒 ≠
∅ ∧ (𝑒‘0)
≠ 0) → ∀𝑛
∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ 〈“𝑘”〉) ≠ ∅ ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0))
∧ 𝑚 ∈
(0..^(♯‘(𝑒 ++
〈“𝑘”〉)))) → (♯‘𝑒) ∈
(ℤ≥‘0)) |
185 | | simpr 485 |
. . . . . . . . . . . 12
⊢
(((((𝑒 ∈ Word
ℝ ∧ 𝑘 ∈
ℝ) ∧ ((𝑒 ≠
∅ ∧ (𝑒‘0)
≠ 0) → ∀𝑛
∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ 〈“𝑘”〉) ≠ ∅ ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0))
∧ 𝑚 ∈
(0..^(♯‘(𝑒 ++
〈“𝑘”〉)))) → 𝑚 ∈ (0..^(♯‘(𝑒 ++ 〈“𝑘”〉)))) |
186 | | ccatws1len 13818 |
. . . . . . . . . . . . . . . 16
⊢ (𝑒 ∈ Word ℝ →
(♯‘(𝑒 ++
〈“𝑘”〉)) = ((♯‘𝑒) + 1)) |
187 | 186 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) →
(♯‘(𝑒 ++
〈“𝑘”〉)) = ((♯‘𝑒) + 1)) |
188 | 187 | oveq2d 7032 |
. . . . . . . . . . . . . 14
⊢ ((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) →
(0..^(♯‘(𝑒 ++
〈“𝑘”〉))) = (0..^((♯‘𝑒) + 1))) |
189 | 188 | eleq2d 2868 |
. . . . . . . . . . . . 13
⊢ ((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) → (𝑚 ∈
(0..^(♯‘(𝑒 ++
〈“𝑘”〉))) ↔ 𝑚 ∈ (0..^((♯‘𝑒) + 1)))) |
190 | 189 | biimpa 477 |
. . . . . . . . . . . 12
⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ 𝑚 ∈
(0..^(♯‘(𝑒 ++
〈“𝑘”〉)))) → 𝑚 ∈ (0..^((♯‘𝑒) + 1))) |
191 | 83, 185, 190 | syl2anc 584 |
. . . . . . . . . . 11
⊢
(((((𝑒 ∈ Word
ℝ ∧ 𝑘 ∈
ℝ) ∧ ((𝑒 ≠
∅ ∧ (𝑒‘0)
≠ 0) → ∀𝑛
∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ 〈“𝑘”〉) ≠ ∅ ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0))
∧ 𝑚 ∈
(0..^(♯‘(𝑒 ++
〈“𝑘”〉)))) → 𝑚 ∈ (0..^((♯‘𝑒) + 1))) |
192 | | fzosplitsni 12998 |
. . . . . . . . . . . 12
⊢
((♯‘𝑒)
∈ (ℤ≥‘0) → (𝑚 ∈ (0..^((♯‘𝑒) + 1)) ↔ (𝑚 ∈
(0..^(♯‘𝑒))
∨ 𝑚 =
(♯‘𝑒)))) |
193 | 192 | biimpa 477 |
. . . . . . . . . . 11
⊢
(((♯‘𝑒)
∈ (ℤ≥‘0) ∧ 𝑚 ∈ (0..^((♯‘𝑒) + 1))) → (𝑚 ∈
(0..^(♯‘𝑒))
∨ 𝑚 =
(♯‘𝑒))) |
194 | 184, 191,
193 | syl2anc 584 |
. . . . . . . . . 10
⊢
(((((𝑒 ∈ Word
ℝ ∧ 𝑘 ∈
ℝ) ∧ ((𝑒 ≠
∅ ∧ (𝑒‘0)
≠ 0) → ∀𝑛
∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ 〈“𝑘”〉) ≠ ∅ ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0))
∧ 𝑚 ∈
(0..^(♯‘(𝑒 ++
〈“𝑘”〉)))) → (𝑚 ∈ (0..^(♯‘𝑒)) ∨ 𝑚 = (♯‘𝑒))) |
195 | 105, 180,
194 | mpjaodan 953 |
. . . . . . . . 9
⊢
(((((𝑒 ∈ Word
ℝ ∧ 𝑘 ∈
ℝ) ∧ ((𝑒 ≠
∅ ∧ (𝑒‘0)
≠ 0) → ∀𝑛
∈ (0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ 〈“𝑘”〉) ≠ ∅ ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0))
∧ 𝑚 ∈
(0..^(♯‘(𝑒 ++
〈“𝑘”〉)))) → ((𝑇‘(𝑒 ++ 〈“𝑘”〉))‘𝑚) ≠ 0) |
196 | 195 | ralrimiva 3149 |
. . . . . . . 8
⊢ ((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) →
∀𝑛 ∈
(0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ 〈“𝑘”〉) ≠ ∅ ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0))
→ ∀𝑚 ∈
(0..^(♯‘(𝑒 ++
〈“𝑘”〉)))((𝑇‘(𝑒 ++ 〈“𝑘”〉))‘𝑚) ≠ 0) |
197 | 60, 196 | sylanbr 582 |
. . . . . . 7
⊢ ((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) →
∀𝑚 ∈
(0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑚) ≠ 0)) ∧ ((𝑒 ++ 〈“𝑘”〉) ≠ ∅ ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0))
→ ∀𝑚 ∈
(0..^(♯‘(𝑒 ++
〈“𝑘”〉)))((𝑇‘(𝑒 ++ 〈“𝑘”〉))‘𝑚) ≠ 0) |
198 | 197 | exp31 420 |
. . . . . 6
⊢ ((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) → (((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) →
∀𝑚 ∈
(0..^(♯‘𝑒))((𝑇‘𝑒)‘𝑚) ≠ 0) → (((𝑒 ++ 〈“𝑘”〉) ≠ ∅ ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0)
→ ∀𝑚 ∈
(0..^(♯‘(𝑒 ++
〈“𝑘”〉)))((𝑇‘(𝑒 ++ 〈“𝑘”〉))‘𝑚) ≠ 0))) |
199 | 19, 30, 41, 52, 55, 198 | wrdind 13920 |
. . . . 5
⊢ (𝐹 ∈ Word ℝ →
((𝐹 ≠ ∅ ∧
(𝐹‘0) ≠ 0) →
∀𝑚 ∈
(0..^(♯‘𝐹))((𝑇‘𝐹)‘𝑚) ≠ 0)) |
200 | 199 | imp 407 |
. . . 4
⊢ ((𝐹 ∈ Word ℝ ∧
(𝐹 ≠ ∅ ∧
(𝐹‘0) ≠ 0)) →
∀𝑚 ∈
(0..^(♯‘𝐹))((𝑇‘𝐹)‘𝑚) ≠ 0) |
201 | 200 | adantrr 713 |
. . 3
⊢ ((𝐹 ∈ Word ℝ ∧
((𝐹 ≠ ∅ ∧
(𝐹‘0) ≠ 0) ∧
𝑁 ∈
(0..^(♯‘𝐹))))
→ ∀𝑚 ∈
(0..^(♯‘𝐹))((𝑇‘𝐹)‘𝑚) ≠ 0) |
202 | | fveq2 6538 |
. . . . 5
⊢ (𝑚 = 𝑁 → ((𝑇‘𝐹)‘𝑚) = ((𝑇‘𝐹)‘𝑁)) |
203 | 202 | neeq1d 3043 |
. . . 4
⊢ (𝑚 = 𝑁 → (((𝑇‘𝐹)‘𝑚) ≠ 0 ↔ ((𝑇‘𝐹)‘𝑁) ≠ 0)) |
204 | 203 | rspcva 3557 |
. . 3
⊢ ((𝑁 ∈
(0..^(♯‘𝐹))
∧ ∀𝑚 ∈
(0..^(♯‘𝐹))((𝑇‘𝐹)‘𝑚) ≠ 0) → ((𝑇‘𝐹)‘𝑁) ≠ 0) |
205 | 8, 201, 204 | syl2anc 584 |
. 2
⊢ ((𝐹 ∈ Word ℝ ∧
((𝐹 ≠ ∅ ∧
(𝐹‘0) ≠ 0) ∧
𝑁 ∈
(0..^(♯‘𝐹))))
→ ((𝑇‘𝐹)‘𝑁) ≠ 0) |
206 | 2, 6, 7, 205 | syl12anc 833 |
1
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝑁 ∈ (0..^(♯‘𝐹))) → ((𝑇‘𝐹)‘𝑁) ≠ 0) |