Step | Hyp | Ref
| Expression |
1 | | simpll 786 |
. . 3
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝑁 ∈ (0..^(#‘𝐹))) → 𝐹 ∈ (Word ℝ ∖
{∅})) |
2 | 1 | eldifad 3552 |
. 2
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝑁 ∈ (0..^(#‘𝐹))) → 𝐹 ∈ Word ℝ) |
3 | | eldifsni 4261 |
. . . 4
⊢ (𝐹 ∈ (Word ℝ ∖
{∅}) → 𝐹 ≠
∅) |
4 | 3 | ad2antrr 758 |
. . 3
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝑁 ∈ (0..^(#‘𝐹))) → 𝐹 ≠ ∅) |
5 | | simplr 788 |
. . 3
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝑁 ∈ (0..^(#‘𝐹))) → (𝐹‘0) ≠ 0) |
6 | 4, 5 | jca 553 |
. 2
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝑁 ∈ (0..^(#‘𝐹))) → (𝐹 ≠ ∅ ∧ (𝐹‘0) ≠ 0)) |
7 | | simpr 476 |
. 2
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝑁 ∈ (0..^(#‘𝐹))) → 𝑁 ∈ (0..^(#‘𝐹))) |
8 | | simprr 792 |
. . 3
⊢ ((𝐹 ∈ Word ℝ ∧
((𝐹 ≠ ∅ ∧
(𝐹‘0) ≠ 0) ∧
𝑁 ∈
(0..^(#‘𝐹)))) →
𝑁 ∈
(0..^(#‘𝐹))) |
9 | | neeq1 2844 |
. . . . . . . 8
⊢ (𝑔 = ∅ → (𝑔 ≠ ∅ ↔ ∅
≠ ∅)) |
10 | | fveq1 6102 |
. . . . . . . . 9
⊢ (𝑔 = ∅ → (𝑔‘0) =
(∅‘0)) |
11 | 10 | neeq1d 2841 |
. . . . . . . 8
⊢ (𝑔 = ∅ → ((𝑔‘0) ≠ 0 ↔
(∅‘0) ≠ 0)) |
12 | 9, 11 | anbi12d 743 |
. . . . . . 7
⊢ (𝑔 = ∅ → ((𝑔 ≠ ∅ ∧ (𝑔‘0) ≠ 0) ↔
(∅ ≠ ∅ ∧ (∅‘0) ≠ 0))) |
13 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑔 = ∅ → (#‘𝑔) =
(#‘∅)) |
14 | 13 | oveq2d 6565 |
. . . . . . . 8
⊢ (𝑔 = ∅ →
(0..^(#‘𝑔)) =
(0..^(#‘∅))) |
15 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑔 = ∅ → (𝑇‘𝑔) = (𝑇‘∅)) |
16 | 15 | fveq1d 6105 |
. . . . . . . . 9
⊢ (𝑔 = ∅ → ((𝑇‘𝑔)‘𝑚) = ((𝑇‘∅)‘𝑚)) |
17 | 16 | neeq1d 2841 |
. . . . . . . 8
⊢ (𝑔 = ∅ → (((𝑇‘𝑔)‘𝑚) ≠ 0 ↔ ((𝑇‘∅)‘𝑚) ≠ 0)) |
18 | 14, 17 | raleqbidv 3129 |
. . . . . . 7
⊢ (𝑔 = ∅ → (∀𝑚 ∈ (0..^(#‘𝑔))((𝑇‘𝑔)‘𝑚) ≠ 0 ↔ ∀𝑚 ∈ (0..^(#‘∅))((𝑇‘∅)‘𝑚) ≠ 0)) |
19 | 12, 18 | imbi12d 333 |
. . . . . 6
⊢ (𝑔 = ∅ → (((𝑔 ≠ ∅ ∧ (𝑔‘0) ≠ 0) →
∀𝑚 ∈
(0..^(#‘𝑔))((𝑇‘𝑔)‘𝑚) ≠ 0) ↔ ((∅ ≠ ∅ ∧
(∅‘0) ≠ 0) → ∀𝑚 ∈ (0..^(#‘∅))((𝑇‘∅)‘𝑚) ≠ 0))) |
20 | | neeq1 2844 |
. . . . . . . 8
⊢ (𝑔 = 𝑒 → (𝑔 ≠ ∅ ↔ 𝑒 ≠ ∅)) |
21 | | fveq1 6102 |
. . . . . . . . 9
⊢ (𝑔 = 𝑒 → (𝑔‘0) = (𝑒‘0)) |
22 | 21 | neeq1d 2841 |
. . . . . . . 8
⊢ (𝑔 = 𝑒 → ((𝑔‘0) ≠ 0 ↔ (𝑒‘0) ≠ 0)) |
23 | 20, 22 | anbi12d 743 |
. . . . . . 7
⊢ (𝑔 = 𝑒 → ((𝑔 ≠ ∅ ∧ (𝑔‘0) ≠ 0) ↔ (𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0))) |
24 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑔 = 𝑒 → (#‘𝑔) = (#‘𝑒)) |
25 | 24 | oveq2d 6565 |
. . . . . . . 8
⊢ (𝑔 = 𝑒 → (0..^(#‘𝑔)) = (0..^(#‘𝑒))) |
26 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑔 = 𝑒 → (𝑇‘𝑔) = (𝑇‘𝑒)) |
27 | 26 | fveq1d 6105 |
. . . . . . . . 9
⊢ (𝑔 = 𝑒 → ((𝑇‘𝑔)‘𝑚) = ((𝑇‘𝑒)‘𝑚)) |
28 | 27 | neeq1d 2841 |
. . . . . . . 8
⊢ (𝑔 = 𝑒 → (((𝑇‘𝑔)‘𝑚) ≠ 0 ↔ ((𝑇‘𝑒)‘𝑚) ≠ 0)) |
29 | 25, 28 | raleqbidv 3129 |
. . . . . . 7
⊢ (𝑔 = 𝑒 → (∀𝑚 ∈ (0..^(#‘𝑔))((𝑇‘𝑔)‘𝑚) ≠ 0 ↔ ∀𝑚 ∈ (0..^(#‘𝑒))((𝑇‘𝑒)‘𝑚) ≠ 0)) |
30 | 23, 29 | imbi12d 333 |
. . . . . 6
⊢ (𝑔 = 𝑒 → (((𝑔 ≠ ∅ ∧ (𝑔‘0) ≠ 0) → ∀𝑚 ∈ (0..^(#‘𝑔))((𝑇‘𝑔)‘𝑚) ≠ 0) ↔ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑚 ∈ (0..^(#‘𝑒))((𝑇‘𝑒)‘𝑚) ≠ 0))) |
31 | | neeq1 2844 |
. . . . . . . 8
⊢ (𝑔 = (𝑒 ++ 〈“𝑘”〉) → (𝑔 ≠ ∅ ↔ (𝑒 ++ 〈“𝑘”〉) ≠
∅)) |
32 | | fveq1 6102 |
. . . . . . . . 9
⊢ (𝑔 = (𝑒 ++ 〈“𝑘”〉) → (𝑔‘0) = ((𝑒 ++ 〈“𝑘”〉)‘0)) |
33 | 32 | neeq1d 2841 |
. . . . . . . 8
⊢ (𝑔 = (𝑒 ++ 〈“𝑘”〉) → ((𝑔‘0) ≠ 0 ↔ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠
0)) |
34 | 31, 33 | anbi12d 743 |
. . . . . . 7
⊢ (𝑔 = (𝑒 ++ 〈“𝑘”〉) → ((𝑔 ≠ ∅ ∧ (𝑔‘0) ≠ 0) ↔ ((𝑒 ++ 〈“𝑘”〉) ≠ ∅ ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠
0))) |
35 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑔 = (𝑒 ++ 〈“𝑘”〉) → (#‘𝑔) = (#‘(𝑒 ++ 〈“𝑘”〉))) |
36 | 35 | oveq2d 6565 |
. . . . . . . 8
⊢ (𝑔 = (𝑒 ++ 〈“𝑘”〉) → (0..^(#‘𝑔)) = (0..^(#‘(𝑒 ++ 〈“𝑘”〉)))) |
37 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑔 = (𝑒 ++ 〈“𝑘”〉) → (𝑇‘𝑔) = (𝑇‘(𝑒 ++ 〈“𝑘”〉))) |
38 | 37 | fveq1d 6105 |
. . . . . . . . 9
⊢ (𝑔 = (𝑒 ++ 〈“𝑘”〉) → ((𝑇‘𝑔)‘𝑚) = ((𝑇‘(𝑒 ++ 〈“𝑘”〉))‘𝑚)) |
39 | 38 | neeq1d 2841 |
. . . . . . . 8
⊢ (𝑔 = (𝑒 ++ 〈“𝑘”〉) → (((𝑇‘𝑔)‘𝑚) ≠ 0 ↔ ((𝑇‘(𝑒 ++ 〈“𝑘”〉))‘𝑚) ≠ 0)) |
40 | 36, 39 | raleqbidv 3129 |
. . . . . . 7
⊢ (𝑔 = (𝑒 ++ 〈“𝑘”〉) → (∀𝑚 ∈ (0..^(#‘𝑔))((𝑇‘𝑔)‘𝑚) ≠ 0 ↔ ∀𝑚 ∈ (0..^(#‘(𝑒 ++ 〈“𝑘”〉)))((𝑇‘(𝑒 ++ 〈“𝑘”〉))‘𝑚) ≠ 0)) |
41 | 34, 40 | imbi12d 333 |
. . . . . 6
⊢ (𝑔 = (𝑒 ++ 〈“𝑘”〉) → (((𝑔 ≠ ∅ ∧ (𝑔‘0) ≠ 0) → ∀𝑚 ∈ (0..^(#‘𝑔))((𝑇‘𝑔)‘𝑚) ≠ 0) ↔ (((𝑒 ++ 〈“𝑘”〉) ≠ ∅ ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0)
→ ∀𝑚 ∈
(0..^(#‘(𝑒 ++
〈“𝑘”〉)))((𝑇‘(𝑒 ++ 〈“𝑘”〉))‘𝑚) ≠ 0))) |
42 | | neeq1 2844 |
. . . . . . . 8
⊢ (𝑔 = 𝐹 → (𝑔 ≠ ∅ ↔ 𝐹 ≠ ∅)) |
43 | | fveq1 6102 |
. . . . . . . . 9
⊢ (𝑔 = 𝐹 → (𝑔‘0) = (𝐹‘0)) |
44 | 43 | neeq1d 2841 |
. . . . . . . 8
⊢ (𝑔 = 𝐹 → ((𝑔‘0) ≠ 0 ↔ (𝐹‘0) ≠ 0)) |
45 | 42, 44 | anbi12d 743 |
. . . . . . 7
⊢ (𝑔 = 𝐹 → ((𝑔 ≠ ∅ ∧ (𝑔‘0) ≠ 0) ↔ (𝐹 ≠ ∅ ∧ (𝐹‘0) ≠ 0))) |
46 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑔 = 𝐹 → (#‘𝑔) = (#‘𝐹)) |
47 | 46 | oveq2d 6565 |
. . . . . . . 8
⊢ (𝑔 = 𝐹 → (0..^(#‘𝑔)) = (0..^(#‘𝐹))) |
48 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑔 = 𝐹 → (𝑇‘𝑔) = (𝑇‘𝐹)) |
49 | 48 | fveq1d 6105 |
. . . . . . . . 9
⊢ (𝑔 = 𝐹 → ((𝑇‘𝑔)‘𝑚) = ((𝑇‘𝐹)‘𝑚)) |
50 | 49 | neeq1d 2841 |
. . . . . . . 8
⊢ (𝑔 = 𝐹 → (((𝑇‘𝑔)‘𝑚) ≠ 0 ↔ ((𝑇‘𝐹)‘𝑚) ≠ 0)) |
51 | 47, 50 | raleqbidv 3129 |
. . . . . . 7
⊢ (𝑔 = 𝐹 → (∀𝑚 ∈ (0..^(#‘𝑔))((𝑇‘𝑔)‘𝑚) ≠ 0 ↔ ∀𝑚 ∈ (0..^(#‘𝐹))((𝑇‘𝐹)‘𝑚) ≠ 0)) |
52 | 45, 51 | imbi12d 333 |
. . . . . 6
⊢ (𝑔 = 𝐹 → (((𝑔 ≠ ∅ ∧ (𝑔‘0) ≠ 0) → ∀𝑚 ∈ (0..^(#‘𝑔))((𝑇‘𝑔)‘𝑚) ≠ 0) ↔ ((𝐹 ≠ ∅ ∧ (𝐹‘0) ≠ 0) → ∀𝑚 ∈ (0..^(#‘𝐹))((𝑇‘𝐹)‘𝑚) ≠ 0))) |
53 | | neirr 2791 |
. . . . . . . 8
⊢ ¬
∅ ≠ ∅ |
54 | 53 | intnanr 952 |
. . . . . . 7
⊢ ¬
(∅ ≠ ∅ ∧ (∅‘0) ≠ 0) |
55 | 54 | pm2.21i 115 |
. . . . . 6
⊢ ((∅
≠ ∅ ∧ (∅‘0) ≠ 0) → ∀𝑚 ∈ (0..^(#‘∅))((𝑇‘∅)‘𝑚) ≠ 0) |
56 | | fveq2 6103 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑚 → ((𝑇‘𝑒)‘𝑛) = ((𝑇‘𝑒)‘𝑚)) |
57 | 56 | neeq1d 2841 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑚 → (((𝑇‘𝑒)‘𝑛) ≠ 0 ↔ ((𝑇‘𝑒)‘𝑚) ≠ 0)) |
58 | 57 | cbvralv 3147 |
. . . . . . . . . 10
⊢
(∀𝑛 ∈
(0..^(#‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0 ↔ ∀𝑚 ∈ (0..^(#‘𝑒))((𝑇‘𝑒)‘𝑚) ≠ 0) |
59 | 58 | imbi2i 325 |
. . . . . . . . 9
⊢ (((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) →
∀𝑛 ∈
(0..^(#‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0) ↔ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑚 ∈ (0..^(#‘𝑒))((𝑇‘𝑒)‘𝑚) ≠ 0)) |
60 | 59 | anbi2i 726 |
. . . . . . . 8
⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) →
∀𝑛 ∈
(0..^(#‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ↔ ((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑚 ∈ (0..^(#‘𝑒))((𝑇‘𝑒)‘𝑚) ≠ 0))) |
61 | | simplr 788 |
. . . . . . . . . . . 12
⊢
(((((((𝑒 ∈ Word
ℝ ∧ 𝑘 ∈
ℝ) ∧ ((𝑒 ≠
∅ ∧ (𝑒‘0)
≠ 0) → ∀𝑛
∈ (0..^(#‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ 〈“𝑘”〉) ≠ ∅ ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0))
∧ 𝑚 ∈
(0..^(#‘(𝑒 ++
〈“𝑘”〉)))) ∧ 𝑚 ∈ (0..^(#‘𝑒))) ∧ 𝑒 = ∅) → 𝑚 ∈ (0..^(#‘𝑒))) |
62 | | noel 3878 |
. . . . . . . . . . . . . 14
⊢ ¬
𝑚 ∈
∅ |
63 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑒 = ∅ → (#‘𝑒) =
(#‘∅)) |
64 | | hash0 13019 |
. . . . . . . . . . . . . . . . . 18
⊢
(#‘∅) = 0 |
65 | 63, 64 | syl6eq 2660 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑒 = ∅ → (#‘𝑒) = 0) |
66 | 65 | oveq2d 6565 |
. . . . . . . . . . . . . . . 16
⊢ (𝑒 = ∅ →
(0..^(#‘𝑒)) =
(0..^0)) |
67 | | fzo0 12361 |
. . . . . . . . . . . . . . . 16
⊢ (0..^0) =
∅ |
68 | 66, 67 | syl6eq 2660 |
. . . . . . . . . . . . . . 15
⊢ (𝑒 = ∅ →
(0..^(#‘𝑒)) =
∅) |
69 | 68 | eleq2d 2673 |
. . . . . . . . . . . . . 14
⊢ (𝑒 = ∅ → (𝑚 ∈ (0..^(#‘𝑒)) ↔ 𝑚 ∈ ∅)) |
70 | 62, 69 | mtbiri 316 |
. . . . . . . . . . . . 13
⊢ (𝑒 = ∅ → ¬ 𝑚 ∈ (0..^(#‘𝑒))) |
71 | 70 | adantl 481 |
. . . . . . . . . . . 12
⊢
(((((((𝑒 ∈ Word
ℝ ∧ 𝑘 ∈
ℝ) ∧ ((𝑒 ≠
∅ ∧ (𝑒‘0)
≠ 0) → ∀𝑛
∈ (0..^(#‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ 〈“𝑘”〉) ≠ ∅ ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0))
∧ 𝑚 ∈
(0..^(#‘(𝑒 ++
〈“𝑘”〉)))) ∧ 𝑚 ∈ (0..^(#‘𝑒))) ∧ 𝑒 = ∅) → ¬ 𝑚 ∈ (0..^(#‘𝑒))) |
72 | 61, 71 | pm2.21dd 185 |
. . . . . . . . . . 11
⊢
(((((((𝑒 ∈ Word
ℝ ∧ 𝑘 ∈
ℝ) ∧ ((𝑒 ≠
∅ ∧ (𝑒‘0)
≠ 0) → ∀𝑛
∈ (0..^(#‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ 〈“𝑘”〉) ≠ ∅ ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0))
∧ 𝑚 ∈
(0..^(#‘(𝑒 ++
〈“𝑘”〉)))) ∧ 𝑚 ∈ (0..^(#‘𝑒))) ∧ 𝑒 = ∅) → ((𝑇‘(𝑒 ++ 〈“𝑘”〉))‘𝑚) ≠ 0) |
73 | | simp-6l 806 |
. . . . . . . . . . . . 13
⊢
(((((((𝑒 ∈ Word
ℝ ∧ 𝑘 ∈
ℝ) ∧ ((𝑒 ≠
∅ ∧ (𝑒‘0)
≠ 0) → ∀𝑛
∈ (0..^(#‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ 〈“𝑘”〉) ≠ ∅ ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0))
∧ 𝑚 ∈
(0..^(#‘(𝑒 ++
〈“𝑘”〉)))) ∧ 𝑚 ∈ (0..^(#‘𝑒))) ∧ 𝑒 ≠ ∅) → 𝑒 ∈ Word ℝ) |
74 | | simp-6r 807 |
. . . . . . . . . . . . 13
⊢
(((((((𝑒 ∈ Word
ℝ ∧ 𝑘 ∈
ℝ) ∧ ((𝑒 ≠
∅ ∧ (𝑒‘0)
≠ 0) → ∀𝑛
∈ (0..^(#‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ 〈“𝑘”〉) ≠ ∅ ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0))
∧ 𝑚 ∈
(0..^(#‘(𝑒 ++
〈“𝑘”〉)))) ∧ 𝑚 ∈ (0..^(#‘𝑒))) ∧ 𝑒 ≠ ∅) → 𝑘 ∈ ℝ) |
75 | | simplr 788 |
. . . . . . . . . . . . 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 29974 |
. . . . . . . . . . . . 13
⊢ ((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ ∧ 𝑚 ∈ (0..^(#‘𝑒))) → ((𝑇‘(𝑒 ++ 〈“𝑘”〉))‘𝑚) = ((𝑇‘𝑒)‘𝑚)) |
81 | 73, 74, 75, 80 | syl3anc 1318 |
. . . . . . . . . . . 12
⊢
(((((((𝑒 ∈ Word
ℝ ∧ 𝑘 ∈
ℝ) ∧ ((𝑒 ≠
∅ ∧ (𝑒‘0)
≠ 0) → ∀𝑛
∈ (0..^(#‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ 〈“𝑘”〉) ≠ ∅ ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0))
∧ 𝑚 ∈
(0..^(#‘(𝑒 ++
〈“𝑘”〉)))) ∧ 𝑚 ∈ (0..^(#‘𝑒))) ∧ 𝑒 ≠ ∅) → ((𝑇‘(𝑒 ++ 〈“𝑘”〉))‘𝑚) = ((𝑇‘𝑒)‘𝑚)) |
82 | | simpr 476 |
. . . . . . . . . . . . . 14
⊢
(((((((𝑒 ∈ Word
ℝ ∧ 𝑘 ∈
ℝ) ∧ ((𝑒 ≠
∅ ∧ (𝑒‘0)
≠ 0) → ∀𝑛
∈ (0..^(#‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ 〈“𝑘”〉) ≠ ∅ ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0))
∧ 𝑚 ∈
(0..^(#‘(𝑒 ++
〈“𝑘”〉)))) ∧ 𝑚 ∈ (0..^(#‘𝑒))) ∧ 𝑒 ≠ ∅) → 𝑒 ≠ ∅) |
83 | | simplll 794 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑒 ∈ Word
ℝ ∧ 𝑘 ∈
ℝ) ∧ ((𝑒 ≠
∅ ∧ (𝑒‘0)
≠ 0) → ∀𝑛
∈ (0..^(#‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ 〈“𝑘”〉) ≠ ∅ ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0))
∧ 𝑚 ∈
(0..^(#‘(𝑒 ++
〈“𝑘”〉)))) → (𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ)) |
84 | 83 | ad2antrr 758 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝑒 ∈ Word
ℝ ∧ 𝑘 ∈
ℝ) ∧ ((𝑒 ≠
∅ ∧ (𝑒‘0)
≠ 0) → ∀𝑛
∈ (0..^(#‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ 〈“𝑘”〉) ≠ ∅ ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0))
∧ 𝑚 ∈
(0..^(#‘(𝑒 ++
〈“𝑘”〉)))) ∧ 𝑚 ∈ (0..^(#‘𝑒))) ∧ 𝑒 ≠ ∅) → (𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ)) |
85 | | simplrr 797 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑒 ∈ Word
ℝ ∧ 𝑘 ∈
ℝ) ∧ ((𝑒 ≠
∅ ∧ (𝑒‘0)
≠ 0) → ∀𝑛
∈ (0..^(#‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ 〈“𝑘”〉) ≠ ∅ ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0))
∧ (𝑚 ∈
(0..^(#‘(𝑒 ++
〈“𝑘”〉))) ∧ 𝑚 ∈ (0..^(#‘𝑒)) ∧ 𝑒 ≠ ∅)) → ((𝑒 ++ 〈“𝑘”〉)‘0) ≠
0) |
86 | 85 | 3anassrs 1282 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝑒 ∈ Word
ℝ ∧ 𝑘 ∈
ℝ) ∧ ((𝑒 ≠
∅ ∧ (𝑒‘0)
≠ 0) → ∀𝑛
∈ (0..^(#‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ 〈“𝑘”〉) ≠ ∅ ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0))
∧ 𝑚 ∈
(0..^(#‘(𝑒 ++
〈“𝑘”〉)))) ∧ 𝑚 ∈ (0..^(#‘𝑒))) ∧ 𝑒 ≠ ∅) → ((𝑒 ++ 〈“𝑘”〉)‘0) ≠
0) |
87 | | simpll 786 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ 𝑒 ≠ ∅) → 𝑒 ∈ Word
ℝ) |
88 | | simplr 788 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ 𝑒 ≠ ∅) → 𝑘 ∈
ℝ) |
89 | 88 | s1cld 13236 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ 𝑒 ≠ ∅) →
〈“𝑘”〉
∈ Word ℝ) |
90 | | lennncl 13180 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑒 ∈ Word ℝ ∧ 𝑒 ≠ ∅) →
(#‘𝑒) ∈
ℕ) |
91 | 90 | adantlr 747 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ 𝑒 ≠ ∅) →
(#‘𝑒) ∈
ℕ) |
92 | | fzo0end 12426 |
. . . . . . . . . . . . . . . . . . 19
⊢
((#‘𝑒) ∈
ℕ → ((#‘𝑒)
− 1) ∈ (0..^(#‘𝑒))) |
93 | | elfzolt3b 12351 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((#‘𝑒)
− 1) ∈ (0..^(#‘𝑒)) → 0 ∈ (0..^(#‘𝑒))) |
94 | 91, 92, 93 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ 𝑒 ≠ ∅) → 0 ∈
(0..^(#‘𝑒))) |
95 | | ccatval1 13214 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑒 ∈ Word ℝ ∧
〈“𝑘”〉
∈ Word ℝ ∧ 0 ∈ (0..^(#‘𝑒))) → ((𝑒 ++ 〈“𝑘”〉)‘0) = (𝑒‘0)) |
96 | 87, 89, 94, 95 | syl3anc 1318 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ 𝑒 ≠ ∅) → ((𝑒 ++ 〈“𝑘”〉)‘0) = (𝑒‘0)) |
97 | 96 | neeq1d 2841 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ 𝑒 ≠ ∅) → (((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0
↔ (𝑒‘0) ≠
0)) |
98 | 97 | biimpa 500 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ 𝑒 ≠ ∅) ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0)
→ (𝑒‘0) ≠
0) |
99 | 84, 82, 86, 98 | syl21anc 1317 |
. . . . . . . . . . . . . 14
⊢
(((((((𝑒 ∈ Word
ℝ ∧ 𝑘 ∈
ℝ) ∧ ((𝑒 ≠
∅ ∧ (𝑒‘0)
≠ 0) → ∀𝑛
∈ (0..^(#‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ 〈“𝑘”〉) ≠ ∅ ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0))
∧ 𝑚 ∈
(0..^(#‘(𝑒 ++
〈“𝑘”〉)))) ∧ 𝑚 ∈ (0..^(#‘𝑒))) ∧ 𝑒 ≠ ∅) → (𝑒‘0) ≠ 0) |
100 | | simp-5r 805 |
. . . . . . . . . . . . . 14
⊢
(((((((𝑒 ∈ Word
ℝ ∧ 𝑘 ∈
ℝ) ∧ ((𝑒 ≠
∅ ∧ (𝑒‘0)
≠ 0) → ∀𝑛
∈ (0..^(#‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ 〈“𝑘”〉) ≠ ∅ ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0))
∧ 𝑚 ∈
(0..^(#‘(𝑒 ++
〈“𝑘”〉)))) ∧ 𝑚 ∈ (0..^(#‘𝑒))) ∧ 𝑒 ≠ ∅) → ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) → ∀𝑛 ∈ (0..^(#‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) |
101 | 82, 99, 100 | mp2and 711 |
. . . . . . . . . . . . 13
⊢
(((((((𝑒 ∈ Word
ℝ ∧ 𝑘 ∈
ℝ) ∧ ((𝑒 ≠
∅ ∧ (𝑒‘0)
≠ 0) → ∀𝑛
∈ (0..^(#‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ 〈“𝑘”〉) ≠ ∅ ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0))
∧ 𝑚 ∈
(0..^(#‘(𝑒 ++
〈“𝑘”〉)))) ∧ 𝑚 ∈ (0..^(#‘𝑒))) ∧ 𝑒 ≠ ∅) → ∀𝑛 ∈ (0..^(#‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0) |
102 | 57 | rspcva 3280 |
. . . . . . . . . . . . 13
⊢ ((𝑚 ∈ (0..^(#‘𝑒)) ∧ ∀𝑛 ∈ (0..^(#‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0) → ((𝑇‘𝑒)‘𝑚) ≠ 0) |
103 | 75, 101, 102 | syl2anc 691 |
. . . . . . . . . . . 12
⊢
(((((((𝑒 ∈ Word
ℝ ∧ 𝑘 ∈
ℝ) ∧ ((𝑒 ≠
∅ ∧ (𝑒‘0)
≠ 0) → ∀𝑛
∈ (0..^(#‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ 〈“𝑘”〉) ≠ ∅ ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0))
∧ 𝑚 ∈
(0..^(#‘(𝑒 ++
〈“𝑘”〉)))) ∧ 𝑚 ∈ (0..^(#‘𝑒))) ∧ 𝑒 ≠ ∅) → ((𝑇‘𝑒)‘𝑚) ≠ 0) |
104 | 81, 103 | eqnetrd 2849 |
. . . . . . . . . . 11
⊢
(((((((𝑒 ∈ Word
ℝ ∧ 𝑘 ∈
ℝ) ∧ ((𝑒 ≠
∅ ∧ (𝑒‘0)
≠ 0) → ∀𝑛
∈ (0..^(#‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ 〈“𝑘”〉) ≠ ∅ ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0))
∧ 𝑚 ∈
(0..^(#‘(𝑒 ++
〈“𝑘”〉)))) ∧ 𝑚 ∈ (0..^(#‘𝑒))) ∧ 𝑒 ≠ ∅) → ((𝑇‘(𝑒 ++ 〈“𝑘”〉))‘𝑚) ≠ 0) |
105 | 72, 104 | pm2.61dane 2869 |
. . . . . . . . . 10
⊢
((((((𝑒 ∈ Word
ℝ ∧ 𝑘 ∈
ℝ) ∧ ((𝑒 ≠
∅ ∧ (𝑒‘0)
≠ 0) → ∀𝑛
∈ (0..^(#‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ 〈“𝑘”〉) ≠ ∅ ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0))
∧ 𝑚 ∈
(0..^(#‘(𝑒 ++
〈“𝑘”〉)))) ∧ 𝑚 ∈ (0..^(#‘𝑒))) → ((𝑇‘(𝑒 ++ 〈“𝑘”〉))‘𝑚) ≠ 0) |
106 | | simpr 476 |
. . . . . . . . . . . 12
⊢
((((((𝑒 ∈ Word
ℝ ∧ 𝑘 ∈
ℝ) ∧ ((𝑒 ≠
∅ ∧ (𝑒‘0)
≠ 0) → ∀𝑛
∈ (0..^(#‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ 〈“𝑘”〉) ≠ ∅ ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0))
∧ 𝑚 ∈
(0..^(#‘(𝑒 ++
〈“𝑘”〉)))) ∧ 𝑚 = (#‘𝑒)) → 𝑚 = (#‘𝑒)) |
107 | 106 | fveq2d 6107 |
. . . . . . . . . . 11
⊢
((((((𝑒 ∈ Word
ℝ ∧ 𝑘 ∈
ℝ) ∧ ((𝑒 ≠
∅ ∧ (𝑒‘0)
≠ 0) → ∀𝑛
∈ (0..^(#‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ 〈“𝑘”〉) ≠ ∅ ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0))
∧ 𝑚 ∈
(0..^(#‘(𝑒 ++
〈“𝑘”〉)))) ∧ 𝑚 = (#‘𝑒)) → ((𝑇‘(𝑒 ++ 〈“𝑘”〉))‘𝑚) = ((𝑇‘(𝑒 ++ 〈“𝑘”〉))‘(#‘𝑒))) |
108 | | simpr 476 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑒 ∈ Word
ℝ ∧ 𝑘 ∈
ℝ) ∧ ((𝑒 ≠
∅ ∧ (𝑒‘0)
≠ 0) → ∀𝑛
∈ (0..^(#‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ 〈“𝑘”〉) ≠ ∅ ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0)
∧ 𝑚 ∈
(0..^(#‘(𝑒 ++
〈“𝑘”〉))))) ∧ 𝑒 = ∅) → 𝑒 = ∅) |
109 | | simp-4r 803 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑒 ∈ Word
ℝ ∧ 𝑘 ∈
ℝ) ∧ ((𝑒 ≠
∅ ∧ (𝑒‘0)
≠ 0) → ∀𝑛
∈ (0..^(#‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ 〈“𝑘”〉) ≠ ∅ ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0)
∧ 𝑚 ∈
(0..^(#‘(𝑒 ++
〈“𝑘”〉))))) ∧ 𝑒 = ∅) → 𝑘 ∈ ℝ) |
110 | | simplrl 796 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑒 ∈ Word
ℝ ∧ 𝑘 ∈
ℝ) ∧ ((𝑒 ≠
∅ ∧ (𝑒‘0)
≠ 0) → ∀𝑛
∈ (0..^(#‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ 〈“𝑘”〉) ≠ ∅ ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0)
∧ 𝑚 ∈
(0..^(#‘(𝑒 ++
〈“𝑘”〉))))) ∧ 𝑒 = ∅) → ((𝑒 ++ 〈“𝑘”〉) ≠ ∅ ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠
0)) |
111 | 110 | simprd 478 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑒 ∈ Word
ℝ ∧ 𝑘 ∈
ℝ) ∧ ((𝑒 ≠
∅ ∧ (𝑒‘0)
≠ 0) → ∀𝑛
∈ (0..^(#‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ 〈“𝑘”〉) ≠ ∅ ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0)
∧ 𝑚 ∈
(0..^(#‘(𝑒 ++
〈“𝑘”〉))))) ∧ 𝑒 = ∅) → ((𝑒 ++ 〈“𝑘”〉)‘0) ≠
0) |
112 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑒 = ∅ → (𝑒 ++ 〈“𝑘”〉) = (∅ ++
〈“𝑘”〉)) |
113 | | s1cl 13235 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑘 ∈ ℝ →
〈“𝑘”〉
∈ Word ℝ) |
114 | | ccatlid 13222 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(〈“𝑘”〉 ∈ Word ℝ →
(∅ ++ 〈“𝑘”〉) = 〈“𝑘”〉) |
115 | 113, 114 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑘 ∈ ℝ → (∅
++ 〈“𝑘”〉) = 〈“𝑘”〉) |
116 | 112, 115 | sylan9eq 2664 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) → (𝑒 ++ 〈“𝑘”〉) =
〈“𝑘”〉) |
117 | 116 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) → (𝑇‘(𝑒 ++ 〈“𝑘”〉)) = (𝑇‘〈“𝑘”〉)) |
118 | 117 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0)
→ (𝑇‘(𝑒 ++ 〈“𝑘”〉)) = (𝑇‘〈“𝑘”〉)) |
119 | | simplr 788 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0)
→ 𝑘 ∈
ℝ) |
120 | 76, 77, 78, 79 | signstf0 29971 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 ∈ ℝ → (𝑇‘〈“𝑘”〉) =
〈“(sgn‘𝑘)”〉) |
121 | 119, 120 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0)
→ (𝑇‘〈“𝑘”〉) =
〈“(sgn‘𝑘)”〉) |
122 | 118, 121 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0)
→ (𝑇‘(𝑒 ++ 〈“𝑘”〉)) =
〈“(sgn‘𝑘)”〉) |
123 | 65 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0)
→ (#‘𝑒) =
0) |
124 | 122, 123 | fveq12d 6109 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0)
→ ((𝑇‘(𝑒 ++ 〈“𝑘”〉))‘(#‘𝑒)) =
(〈“(sgn‘𝑘)”〉‘0)) |
125 | | sgnclre 29928 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ ℝ →
(sgn‘𝑘) ∈
ℝ) |
126 | | s1fv 13243 |
. . . . . . . . . . . . . . . . . 18
⊢
((sgn‘𝑘)
∈ ℝ → (〈“(sgn‘𝑘)”〉‘0) = (sgn‘𝑘)) |
127 | 119, 125,
126 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0)
→ (〈“(sgn‘𝑘)”〉‘0) = (sgn‘𝑘)) |
128 | 124, 127 | eqtrd 2644 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0)
→ ((𝑇‘(𝑒 ++ 〈“𝑘”〉))‘(#‘𝑒)) = (sgn‘𝑘)) |
129 | 116 | fveq1d 6105 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) → ((𝑒 ++ 〈“𝑘”〉)‘0) =
(〈“𝑘”〉‘0)) |
130 | | s1fv 13243 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 ∈ ℝ →
(〈“𝑘”〉‘0) = 𝑘) |
131 | 130 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) →
(〈“𝑘”〉‘0) = 𝑘) |
132 | 129, 131 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) → ((𝑒 ++ 〈“𝑘”〉)‘0) = 𝑘) |
133 | 132 | neeq1d 2841 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) → (((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0
↔ 𝑘 ≠
0)) |
134 | 133 | biimpa 500 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0)
→ 𝑘 ≠
0) |
135 | | rexr 9964 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 ∈ ℝ → 𝑘 ∈
ℝ*) |
136 | | sgn0bi 29936 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 ∈ ℝ*
→ ((sgn‘𝑘) = 0
↔ 𝑘 =
0)) |
137 | 135, 136 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 ∈ ℝ →
((sgn‘𝑘) = 0 ↔
𝑘 = 0)) |
138 | 137 | necon3bid 2826 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ ℝ →
((sgn‘𝑘) ≠ 0
↔ 𝑘 ≠
0)) |
139 | 138 | biimpar 501 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘 ∈ ℝ ∧ 𝑘 ≠ 0) → (sgn‘𝑘) ≠ 0) |
140 | 119, 134,
139 | syl2anc 691 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0)
→ (sgn‘𝑘) ≠
0) |
141 | 128, 140 | eqnetrd 2849 |
. . . . . . . . . . . . . . 15
⊢ (((𝑒 = ∅ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0)
→ ((𝑇‘(𝑒 ++ 〈“𝑘”〉))‘(#‘𝑒)) ≠ 0) |
142 | 108, 109,
111, 141 | syl21anc 1317 |
. . . . . . . . . . . . . 14
⊢
(((((𝑒 ∈ Word
ℝ ∧ 𝑘 ∈
ℝ) ∧ ((𝑒 ≠
∅ ∧ (𝑒‘0)
≠ 0) → ∀𝑛
∈ (0..^(#‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ 〈“𝑘”〉) ≠ ∅ ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0)
∧ 𝑚 ∈
(0..^(#‘(𝑒 ++
〈“𝑘”〉))))) ∧ 𝑒 = ∅) → ((𝑇‘(𝑒 ++ 〈“𝑘”〉))‘(#‘𝑒)) ≠ 0) |
143 | | simplll 794 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (((𝑒 ++ 〈“𝑘”〉) ≠ ∅
∧ ((𝑒 ++
〈“𝑘”〉)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(#‘(𝑒 ++ 〈“𝑘”〉))))) ∧ ¬
𝑒 = ∅) → 𝑒 ∈ Word
ℝ) |
144 | | simpr 476 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (((𝑒 ++ 〈“𝑘”〉) ≠ ∅
∧ ((𝑒 ++
〈“𝑘”〉)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(#‘(𝑒 ++ 〈“𝑘”〉))))) ∧ ¬
𝑒 = ∅) → ¬
𝑒 =
∅) |
145 | | velsn 4141 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑒 ∈ {∅} ↔ 𝑒 = ∅) |
146 | 144, 145 | sylnibr 318 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (((𝑒 ++ 〈“𝑘”〉) ≠ ∅
∧ ((𝑒 ++
〈“𝑘”〉)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(#‘(𝑒 ++ 〈“𝑘”〉))))) ∧ ¬
𝑒 = ∅) → ¬
𝑒 ∈
{∅}) |
147 | 143, 146 | eldifd 3551 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (((𝑒 ++ 〈“𝑘”〉) ≠ ∅
∧ ((𝑒 ++
〈“𝑘”〉)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(#‘(𝑒 ++ 〈“𝑘”〉))))) ∧ ¬
𝑒 = ∅) → 𝑒 ∈ (Word ℝ ∖
{∅})) |
148 | | simpllr 795 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (((𝑒 ++ 〈“𝑘”〉) ≠ ∅
∧ ((𝑒 ++
〈“𝑘”〉)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(#‘(𝑒 ++ 〈“𝑘”〉))))) ∧ ¬
𝑒 = ∅) → 𝑘 ∈
ℝ) |
149 | 76, 77, 78, 79 | signstfvn 29972 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑒 ∈ (Word ℝ ∖
{∅}) ∧ 𝑘 ∈
ℝ) → ((𝑇‘(𝑒 ++ 〈“𝑘”〉))‘(#‘𝑒)) = (((𝑇‘𝑒)‘((#‘𝑒) − 1)) ⨣ (sgn‘𝑘))) |
150 | 147, 148,
149 | syl2anc 691 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (((𝑒 ++ 〈“𝑘”〉) ≠ ∅
∧ ((𝑒 ++
〈“𝑘”〉)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(#‘(𝑒 ++ 〈“𝑘”〉))))) ∧ ¬
𝑒 = ∅) → ((𝑇‘(𝑒 ++ 〈“𝑘”〉))‘(#‘𝑒)) = (((𝑇‘𝑒)‘((#‘𝑒) − 1)) ⨣ (sgn‘𝑘))) |
151 | 150 | adantllr 751 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑒 ∈ Word
ℝ ∧ 𝑘 ∈
ℝ) ∧ ((𝑒 ≠
∅ ∧ (𝑒‘0)
≠ 0) → ∀𝑛
∈ (0..^(#‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ 〈“𝑘”〉) ≠ ∅ ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0)
∧ 𝑚 ∈
(0..^(#‘(𝑒 ++
〈“𝑘”〉))))) ∧ ¬ 𝑒 = ∅) → ((𝑇‘(𝑒 ++ 〈“𝑘”〉))‘(#‘𝑒)) = (((𝑇‘𝑒)‘((#‘𝑒) − 1)) ⨣ (sgn‘𝑘))) |
152 | 144 | neqned 2789 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (((𝑒 ++ 〈“𝑘”〉) ≠ ∅
∧ ((𝑒 ++
〈“𝑘”〉)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(#‘(𝑒 ++ 〈“𝑘”〉))))) ∧ ¬
𝑒 = ∅) → 𝑒 ≠ ∅) |
153 | 143, 152,
90 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (((𝑒 ++ 〈“𝑘”〉) ≠ ∅
∧ ((𝑒 ++
〈“𝑘”〉)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(#‘(𝑒 ++ 〈“𝑘”〉))))) ∧ ¬
𝑒 = ∅) →
(#‘𝑒) ∈
ℕ) |
154 | 153, 92 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (((𝑒 ++ 〈“𝑘”〉) ≠ ∅
∧ ((𝑒 ++
〈“𝑘”〉)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(#‘(𝑒 ++ 〈“𝑘”〉))))) ∧ ¬
𝑒 = ∅) →
((#‘𝑒) − 1)
∈ (0..^(#‘𝑒))) |
155 | 76, 77, 78, 79 | signstcl 29968 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑒 ∈ Word ℝ ∧
((#‘𝑒) − 1)
∈ (0..^(#‘𝑒)))
→ ((𝑇‘𝑒)‘((#‘𝑒) − 1)) ∈ {-1, 0,
1}) |
156 | 143, 154,
155 | syl2anc 691 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (((𝑒 ++ 〈“𝑘”〉) ≠ ∅
∧ ((𝑒 ++
〈“𝑘”〉)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(#‘(𝑒 ++ 〈“𝑘”〉))))) ∧ ¬
𝑒 = ∅) → ((𝑇‘𝑒)‘((#‘𝑒) − 1)) ∈ {-1, 0,
1}) |
157 | 156 | adantllr 751 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑒 ∈ Word
ℝ ∧ 𝑘 ∈
ℝ) ∧ ((𝑒 ≠
∅ ∧ (𝑒‘0)
≠ 0) → ∀𝑛
∈ (0..^(#‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ 〈“𝑘”〉) ≠ ∅ ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0)
∧ 𝑚 ∈
(0..^(#‘(𝑒 ++
〈“𝑘”〉))))) ∧ ¬ 𝑒 = ∅) → ((𝑇‘𝑒)‘((#‘𝑒) − 1)) ∈ {-1, 0,
1}) |
158 | 148 | rexrd 9968 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (((𝑒 ++ 〈“𝑘”〉) ≠ ∅
∧ ((𝑒 ++
〈“𝑘”〉)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(#‘(𝑒 ++ 〈“𝑘”〉))))) ∧ ¬
𝑒 = ∅) → 𝑘 ∈
ℝ*) |
159 | | sgncl 29927 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ ℝ*
→ (sgn‘𝑘) ∈
{-1, 0, 1}) |
160 | 158, 159 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ (((𝑒 ++ 〈“𝑘”〉) ≠ ∅
∧ ((𝑒 ++
〈“𝑘”〉)‘0) ≠ 0) ∧ 𝑚 ∈ (0..^(#‘(𝑒 ++ 〈“𝑘”〉))))) ∧ ¬
𝑒 = ∅) →
(sgn‘𝑘) ∈ {-1,
0, 1}) |
161 | 160 | adantllr 751 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑒 ∈ Word
ℝ ∧ 𝑘 ∈
ℝ) ∧ ((𝑒 ≠
∅ ∧ (𝑒‘0)
≠ 0) → ∀𝑛
∈ (0..^(#‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ 〈“𝑘”〉) ≠ ∅ ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0)
∧ 𝑚 ∈
(0..^(#‘(𝑒 ++
〈“𝑘”〉))))) ∧ ¬ 𝑒 = ∅) →
(sgn‘𝑘) ∈ {-1,
0, 1}) |
162 | 154 | adantllr 751 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝑒 ∈ Word
ℝ ∧ 𝑘 ∈
ℝ) ∧ ((𝑒 ≠
∅ ∧ (𝑒‘0)
≠ 0) → ∀𝑛
∈ (0..^(#‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ 〈“𝑘”〉) ≠ ∅ ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0)
∧ 𝑚 ∈
(0..^(#‘(𝑒 ++
〈“𝑘”〉))))) ∧ ¬ 𝑒 = ∅) →
((#‘𝑒) − 1)
∈ (0..^(#‘𝑒))) |
163 | 152 | adantllr 751 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝑒 ∈ Word
ℝ ∧ 𝑘 ∈
ℝ) ∧ ((𝑒 ≠
∅ ∧ (𝑒‘0)
≠ 0) → ∀𝑛
∈ (0..^(#‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ 〈“𝑘”〉) ≠ ∅ ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0)
∧ 𝑚 ∈
(0..^(#‘(𝑒 ++
〈“𝑘”〉))))) ∧ ¬ 𝑒 = ∅) → 𝑒 ≠ ∅) |
164 | | simplll 794 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝑒 ∈ Word
ℝ ∧ 𝑘 ∈
ℝ) ∧ ((𝑒 ≠
∅ ∧ (𝑒‘0)
≠ 0) → ∀𝑛
∈ (0..^(#‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ 〈“𝑘”〉) ≠ ∅ ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0)
∧ 𝑚 ∈
(0..^(#‘(𝑒 ++
〈“𝑘”〉))))) ∧ ¬ 𝑒 = ∅) → (𝑒 ∈ Word ℝ ∧ 𝑘 ∈
ℝ)) |
165 | | simplrl 796 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝑒 ∈ Word
ℝ ∧ 𝑘 ∈
ℝ) ∧ ((𝑒 ≠
∅ ∧ (𝑒‘0)
≠ 0) → ∀𝑛
∈ (0..^(#‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ 〈“𝑘”〉) ≠ ∅ ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0)
∧ 𝑚 ∈
(0..^(#‘(𝑒 ++
〈“𝑘”〉))))) ∧ ¬ 𝑒 = ∅) → ((𝑒 ++ 〈“𝑘”〉) ≠ ∅
∧ ((𝑒 ++
〈“𝑘”〉)‘0) ≠
0)) |
166 | 165 | simprd 478 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝑒 ∈ Word
ℝ ∧ 𝑘 ∈
ℝ) ∧ ((𝑒 ≠
∅ ∧ (𝑒‘0)
≠ 0) → ∀𝑛
∈ (0..^(#‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ 〈“𝑘”〉) ≠ ∅ ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0)
∧ 𝑚 ∈
(0..^(#‘(𝑒 ++
〈“𝑘”〉))))) ∧ ¬ 𝑒 = ∅) → ((𝑒 ++ 〈“𝑘”〉)‘0) ≠
0) |
167 | 164, 163,
166, 98 | syl21anc 1317 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝑒 ∈ Word
ℝ ∧ 𝑘 ∈
ℝ) ∧ ((𝑒 ≠
∅ ∧ (𝑒‘0)
≠ 0) → ∀𝑛
∈ (0..^(#‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ 〈“𝑘”〉) ≠ ∅ ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0)
∧ 𝑚 ∈
(0..^(#‘(𝑒 ++
〈“𝑘”〉))))) ∧ ¬ 𝑒 = ∅) → (𝑒‘0) ≠
0) |
168 | | simpllr 795 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝑒 ∈ Word
ℝ ∧ 𝑘 ∈
ℝ) ∧ ((𝑒 ≠
∅ ∧ (𝑒‘0)
≠ 0) → ∀𝑛
∈ (0..^(#‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ 〈“𝑘”〉) ≠ ∅ ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0)
∧ 𝑚 ∈
(0..^(#‘(𝑒 ++
〈“𝑘”〉))))) ∧ ¬ 𝑒 = ∅) → ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) →
∀𝑛 ∈
(0..^(#‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) |
169 | 163, 167,
168 | mp2and 711 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝑒 ∈ Word
ℝ ∧ 𝑘 ∈
ℝ) ∧ ((𝑒 ≠
∅ ∧ (𝑒‘0)
≠ 0) → ∀𝑛
∈ (0..^(#‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ 〈“𝑘”〉) ≠ ∅ ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0)
∧ 𝑚 ∈
(0..^(#‘(𝑒 ++
〈“𝑘”〉))))) ∧ ¬ 𝑒 = ∅) → ∀𝑛 ∈ (0..^(#‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0) |
170 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 = ((#‘𝑒) − 1) → ((𝑇‘𝑒)‘𝑛) = ((𝑇‘𝑒)‘((#‘𝑒) − 1))) |
171 | 170 | neeq1d 2841 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = ((#‘𝑒) − 1) → (((𝑇‘𝑒)‘𝑛) ≠ 0 ↔ ((𝑇‘𝑒)‘((#‘𝑒) − 1)) ≠ 0)) |
172 | 171 | rspcva 3280 |
. . . . . . . . . . . . . . . . 17
⊢
((((#‘𝑒)
− 1) ∈ (0..^(#‘𝑒)) ∧ ∀𝑛 ∈ (0..^(#‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0) → ((𝑇‘𝑒)‘((#‘𝑒) − 1)) ≠ 0) |
173 | 162, 169,
172 | syl2anc 691 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑒 ∈ Word
ℝ ∧ 𝑘 ∈
ℝ) ∧ ((𝑒 ≠
∅ ∧ (𝑒‘0)
≠ 0) → ∀𝑛
∈ (0..^(#‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ 〈“𝑘”〉) ≠ ∅ ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0)
∧ 𝑚 ∈
(0..^(#‘(𝑒 ++
〈“𝑘”〉))))) ∧ ¬ 𝑒 = ∅) → ((𝑇‘𝑒)‘((#‘𝑒) − 1)) ≠ 0) |
174 | 76, 77 | signswn0 29963 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑇‘𝑒)‘((#‘𝑒) − 1)) ∈ {-1, 0, 1}
∧ (sgn‘𝑘) ∈
{-1, 0, 1}) ∧ ((𝑇‘𝑒)‘((#‘𝑒) − 1)) ≠ 0) → (((𝑇‘𝑒)‘((#‘𝑒) − 1)) ⨣ (sgn‘𝑘)) ≠ 0) |
175 | 157, 161,
173, 174 | syl21anc 1317 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑒 ∈ Word
ℝ ∧ 𝑘 ∈
ℝ) ∧ ((𝑒 ≠
∅ ∧ (𝑒‘0)
≠ 0) → ∀𝑛
∈ (0..^(#‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ 〈“𝑘”〉) ≠ ∅ ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0)
∧ 𝑚 ∈
(0..^(#‘(𝑒 ++
〈“𝑘”〉))))) ∧ ¬ 𝑒 = ∅) → (((𝑇‘𝑒)‘((#‘𝑒) − 1)) ⨣ (sgn‘𝑘)) ≠ 0) |
176 | 151, 175 | eqnetrd 2849 |
. . . . . . . . . . . . . 14
⊢
(((((𝑒 ∈ Word
ℝ ∧ 𝑘 ∈
ℝ) ∧ ((𝑒 ≠
∅ ∧ (𝑒‘0)
≠ 0) → ∀𝑛
∈ (0..^(#‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ 〈“𝑘”〉) ≠ ∅ ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0)
∧ 𝑚 ∈
(0..^(#‘(𝑒 ++
〈“𝑘”〉))))) ∧ ¬ 𝑒 = ∅) → ((𝑇‘(𝑒 ++ 〈“𝑘”〉))‘(#‘𝑒)) ≠ 0) |
177 | 142, 176 | pm2.61dan 828 |
. . . . . . . . . . . . 13
⊢ ((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) →
∀𝑛 ∈
(0..^(#‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ (((𝑒 ++ 〈“𝑘”〉) ≠ ∅ ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0)
∧ 𝑚 ∈
(0..^(#‘(𝑒 ++
〈“𝑘”〉))))) → ((𝑇‘(𝑒 ++ 〈“𝑘”〉))‘(#‘𝑒)) ≠ 0) |
178 | 177 | anassrs 678 |
. . . . . . . . . . . 12
⊢
(((((𝑒 ∈ Word
ℝ ∧ 𝑘 ∈
ℝ) ∧ ((𝑒 ≠
∅ ∧ (𝑒‘0)
≠ 0) → ∀𝑛
∈ (0..^(#‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ 〈“𝑘”〉) ≠ ∅ ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0))
∧ 𝑚 ∈
(0..^(#‘(𝑒 ++
〈“𝑘”〉)))) → ((𝑇‘(𝑒 ++ 〈“𝑘”〉))‘(#‘𝑒)) ≠ 0) |
179 | 178 | adantr 480 |
. . . . . . . . . . 11
⊢
((((((𝑒 ∈ Word
ℝ ∧ 𝑘 ∈
ℝ) ∧ ((𝑒 ≠
∅ ∧ (𝑒‘0)
≠ 0) → ∀𝑛
∈ (0..^(#‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ 〈“𝑘”〉) ≠ ∅ ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0))
∧ 𝑚 ∈
(0..^(#‘(𝑒 ++
〈“𝑘”〉)))) ∧ 𝑚 = (#‘𝑒)) → ((𝑇‘(𝑒 ++ 〈“𝑘”〉))‘(#‘𝑒)) ≠ 0) |
180 | 107, 179 | eqnetrd 2849 |
. . . . . . . . . 10
⊢
((((((𝑒 ∈ Word
ℝ ∧ 𝑘 ∈
ℝ) ∧ ((𝑒 ≠
∅ ∧ (𝑒‘0)
≠ 0) → ∀𝑛
∈ (0..^(#‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ 〈“𝑘”〉) ≠ ∅ ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0))
∧ 𝑚 ∈
(0..^(#‘(𝑒 ++
〈“𝑘”〉)))) ∧ 𝑚 = (#‘𝑒)) → ((𝑇‘(𝑒 ++ 〈“𝑘”〉))‘𝑚) ≠ 0) |
181 | | lencl 13179 |
. . . . . . . . . . . . 13
⊢ (𝑒 ∈ Word ℝ →
(#‘𝑒) ∈
ℕ0) |
182 | | nn0uz 11598 |
. . . . . . . . . . . . 13
⊢
ℕ0 = (ℤ≥‘0) |
183 | 181, 182 | syl6eleq 2698 |
. . . . . . . . . . . 12
⊢ (𝑒 ∈ Word ℝ →
(#‘𝑒) ∈
(ℤ≥‘0)) |
184 | 183 | ad4antr 764 |
. . . . . . . . . . 11
⊢
(((((𝑒 ∈ Word
ℝ ∧ 𝑘 ∈
ℝ) ∧ ((𝑒 ≠
∅ ∧ (𝑒‘0)
≠ 0) → ∀𝑛
∈ (0..^(#‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ 〈“𝑘”〉) ≠ ∅ ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0))
∧ 𝑚 ∈
(0..^(#‘(𝑒 ++
〈“𝑘”〉)))) → (#‘𝑒) ∈
(ℤ≥‘0)) |
185 | | simpr 476 |
. . . . . . . . . . . 12
⊢
(((((𝑒 ∈ Word
ℝ ∧ 𝑘 ∈
ℝ) ∧ ((𝑒 ≠
∅ ∧ (𝑒‘0)
≠ 0) → ∀𝑛
∈ (0..^(#‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ 〈“𝑘”〉) ≠ ∅ ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0))
∧ 𝑚 ∈
(0..^(#‘(𝑒 ++
〈“𝑘”〉)))) → 𝑚 ∈ (0..^(#‘(𝑒 ++ 〈“𝑘”〉)))) |
186 | | ccatws1len 13251 |
. . . . . . . . . . . . . . 15
⊢ ((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) →
(#‘(𝑒 ++
〈“𝑘”〉)) = ((#‘𝑒) + 1)) |
187 | 186 | oveq2d 6565 |
. . . . . . . . . . . . . 14
⊢ ((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) →
(0..^(#‘(𝑒 ++
〈“𝑘”〉))) = (0..^((#‘𝑒) + 1))) |
188 | 187 | eleq2d 2673 |
. . . . . . . . . . . . 13
⊢ ((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) → (𝑚 ∈ (0..^(#‘(𝑒 ++ 〈“𝑘”〉))) ↔ 𝑚 ∈ (0..^((#‘𝑒) + 1)))) |
189 | 188 | biimpa 500 |
. . . . . . . . . . . 12
⊢ (((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ 𝑚 ∈ (0..^(#‘(𝑒 ++ 〈“𝑘”〉)))) → 𝑚 ∈ (0..^((#‘𝑒) + 1))) |
190 | 83, 185, 189 | syl2anc 691 |
. . . . . . . . . . 11
⊢
(((((𝑒 ∈ Word
ℝ ∧ 𝑘 ∈
ℝ) ∧ ((𝑒 ≠
∅ ∧ (𝑒‘0)
≠ 0) → ∀𝑛
∈ (0..^(#‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ 〈“𝑘”〉) ≠ ∅ ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0))
∧ 𝑚 ∈
(0..^(#‘(𝑒 ++
〈“𝑘”〉)))) → 𝑚 ∈ (0..^((#‘𝑒) + 1))) |
191 | | fzosplitsni 12444 |
. . . . . . . . . . . 12
⊢
((#‘𝑒) ∈
(ℤ≥‘0) → (𝑚 ∈ (0..^((#‘𝑒) + 1)) ↔ (𝑚 ∈ (0..^(#‘𝑒)) ∨ 𝑚 = (#‘𝑒)))) |
192 | 191 | biimpa 500 |
. . . . . . . . . . 11
⊢
(((#‘𝑒) ∈
(ℤ≥‘0) ∧ 𝑚 ∈ (0..^((#‘𝑒) + 1))) → (𝑚 ∈ (0..^(#‘𝑒)) ∨ 𝑚 = (#‘𝑒))) |
193 | 184, 190,
192 | syl2anc 691 |
. . . . . . . . . 10
⊢
(((((𝑒 ∈ Word
ℝ ∧ 𝑘 ∈
ℝ) ∧ ((𝑒 ≠
∅ ∧ (𝑒‘0)
≠ 0) → ∀𝑛
∈ (0..^(#‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ 〈“𝑘”〉) ≠ ∅ ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0))
∧ 𝑚 ∈
(0..^(#‘(𝑒 ++
〈“𝑘”〉)))) → (𝑚 ∈ (0..^(#‘𝑒)) ∨ 𝑚 = (#‘𝑒))) |
194 | 105, 180,
193 | mpjaodan 823 |
. . . . . . . . 9
⊢
(((((𝑒 ∈ Word
ℝ ∧ 𝑘 ∈
ℝ) ∧ ((𝑒 ≠
∅ ∧ (𝑒‘0)
≠ 0) → ∀𝑛
∈ (0..^(#‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ 〈“𝑘”〉) ≠ ∅ ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0))
∧ 𝑚 ∈
(0..^(#‘(𝑒 ++
〈“𝑘”〉)))) → ((𝑇‘(𝑒 ++ 〈“𝑘”〉))‘𝑚) ≠ 0) |
195 | 194 | ralrimiva 2949 |
. . . . . . . 8
⊢ ((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) →
∀𝑛 ∈
(0..^(#‘𝑒))((𝑇‘𝑒)‘𝑛) ≠ 0)) ∧ ((𝑒 ++ 〈“𝑘”〉) ≠ ∅ ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0))
→ ∀𝑚 ∈
(0..^(#‘(𝑒 ++
〈“𝑘”〉)))((𝑇‘(𝑒 ++ 〈“𝑘”〉))‘𝑚) ≠ 0) |
196 | 60, 195 | sylanbr 489 |
. . . . . . 7
⊢ ((((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) ∧ ((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) →
∀𝑚 ∈
(0..^(#‘𝑒))((𝑇‘𝑒)‘𝑚) ≠ 0)) ∧ ((𝑒 ++ 〈“𝑘”〉) ≠ ∅ ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0))
→ ∀𝑚 ∈
(0..^(#‘(𝑒 ++
〈“𝑘”〉)))((𝑇‘(𝑒 ++ 〈“𝑘”〉))‘𝑚) ≠ 0) |
197 | 196 | exp31 628 |
. . . . . 6
⊢ ((𝑒 ∈ Word ℝ ∧ 𝑘 ∈ ℝ) → (((𝑒 ≠ ∅ ∧ (𝑒‘0) ≠ 0) →
∀𝑚 ∈
(0..^(#‘𝑒))((𝑇‘𝑒)‘𝑚) ≠ 0) → (((𝑒 ++ 〈“𝑘”〉) ≠ ∅ ∧ ((𝑒 ++ 〈“𝑘”〉)‘0) ≠ 0)
→ ∀𝑚 ∈
(0..^(#‘(𝑒 ++
〈“𝑘”〉)))((𝑇‘(𝑒 ++ 〈“𝑘”〉))‘𝑚) ≠ 0))) |
198 | 19, 30, 41, 52, 55, 197 | wrdind 13328 |
. . . . 5
⊢ (𝐹 ∈ Word ℝ →
((𝐹 ≠ ∅ ∧
(𝐹‘0) ≠ 0) →
∀𝑚 ∈
(0..^(#‘𝐹))((𝑇‘𝐹)‘𝑚) ≠ 0)) |
199 | 198 | imp 444 |
. . . 4
⊢ ((𝐹 ∈ Word ℝ ∧
(𝐹 ≠ ∅ ∧
(𝐹‘0) ≠ 0)) →
∀𝑚 ∈
(0..^(#‘𝐹))((𝑇‘𝐹)‘𝑚) ≠ 0) |
200 | 199 | adantrr 749 |
. . 3
⊢ ((𝐹 ∈ Word ℝ ∧
((𝐹 ≠ ∅ ∧
(𝐹‘0) ≠ 0) ∧
𝑁 ∈
(0..^(#‘𝐹)))) →
∀𝑚 ∈
(0..^(#‘𝐹))((𝑇‘𝐹)‘𝑚) ≠ 0) |
201 | | fveq2 6103 |
. . . . 5
⊢ (𝑚 = 𝑁 → ((𝑇‘𝐹)‘𝑚) = ((𝑇‘𝐹)‘𝑁)) |
202 | 201 | neeq1d 2841 |
. . . 4
⊢ (𝑚 = 𝑁 → (((𝑇‘𝐹)‘𝑚) ≠ 0 ↔ ((𝑇‘𝐹)‘𝑁) ≠ 0)) |
203 | 202 | rspcva 3280 |
. . 3
⊢ ((𝑁 ∈ (0..^(#‘𝐹)) ∧ ∀𝑚 ∈ (0..^(#‘𝐹))((𝑇‘𝐹)‘𝑚) ≠ 0) → ((𝑇‘𝐹)‘𝑁) ≠ 0) |
204 | 8, 200, 203 | syl2anc 691 |
. 2
⊢ ((𝐹 ∈ Word ℝ ∧
((𝐹 ≠ ∅ ∧
(𝐹‘0) ≠ 0) ∧
𝑁 ∈
(0..^(#‘𝐹)))) →
((𝑇‘𝐹)‘𝑁) ≠ 0) |
205 | 2, 6, 7, 204 | syl12anc 1316 |
1
⊢ (((𝐹 ∈ (Word ℝ ∖
{∅}) ∧ (𝐹‘0) ≠ 0) ∧ 𝑁 ∈ (0..^(#‘𝐹))) → ((𝑇‘𝐹)‘𝑁) ≠ 0) |