Proof of Theorem wwlksnextproplem1
Step | Hyp | Ref
| Expression |
1 | | wwlknbp1 28195 |
. . . . 5
⊢ (𝑊 ∈ ((𝑁 + 1) WWalksN 𝐺) → ((𝑁 + 1) ∈ ℕ0 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑊) = ((𝑁 + 1) + 1))) |
2 | | simpl2 1191 |
. . . . . . 7
⊢ ((((𝑁 + 1) ∈ ℕ0
∧ 𝑊 ∈ Word
(Vtx‘𝐺) ∧
(♯‘𝑊) = ((𝑁 + 1) + 1)) ∧ 𝑁 ∈ ℕ0)
→ 𝑊 ∈ Word
(Vtx‘𝐺)) |
3 | | peano2nn0 12261 |
. . . . . . . . . . 11
⊢ ((𝑁 + 1) ∈ ℕ0
→ ((𝑁 + 1) + 1) ∈
ℕ0) |
4 | 3 | 3ad2ant1 1132 |
. . . . . . . . . 10
⊢ (((𝑁 + 1) ∈ ℕ0
∧ 𝑊 ∈ Word
(Vtx‘𝐺) ∧
(♯‘𝑊) = ((𝑁 + 1) + 1)) → ((𝑁 + 1) + 1) ∈
ℕ0) |
5 | | eleq1 2826 |
. . . . . . . . . . 11
⊢
((♯‘𝑊) =
((𝑁 + 1) + 1) →
((♯‘𝑊) ∈
ℕ0 ↔ ((𝑁 + 1) + 1) ∈
ℕ0)) |
6 | 5 | 3ad2ant3 1134 |
. . . . . . . . . 10
⊢ (((𝑁 + 1) ∈ ℕ0
∧ 𝑊 ∈ Word
(Vtx‘𝐺) ∧
(♯‘𝑊) = ((𝑁 + 1) + 1)) →
((♯‘𝑊) ∈
ℕ0 ↔ ((𝑁 + 1) + 1) ∈
ℕ0)) |
7 | 4, 6 | mpbird 256 |
. . . . . . . . 9
⊢ (((𝑁 + 1) ∈ ℕ0
∧ 𝑊 ∈ Word
(Vtx‘𝐺) ∧
(♯‘𝑊) = ((𝑁 + 1) + 1)) →
(♯‘𝑊) ∈
ℕ0) |
8 | 7 | adantr 481 |
. . . . . . . 8
⊢ ((((𝑁 + 1) ∈ ℕ0
∧ 𝑊 ∈ Word
(Vtx‘𝐺) ∧
(♯‘𝑊) = ((𝑁 + 1) + 1)) ∧ 𝑁 ∈ ℕ0)
→ (♯‘𝑊)
∈ ℕ0) |
9 | | simpr 485 |
. . . . . . . . 9
⊢ ((((𝑁 + 1) ∈ ℕ0
∧ 𝑊 ∈ Word
(Vtx‘𝐺) ∧
(♯‘𝑊) = ((𝑁 + 1) + 1)) ∧ 𝑁 ∈ ℕ0)
→ 𝑁 ∈
ℕ0) |
10 | | nn0re 12230 |
. . . . . . . . . . . . 13
⊢ ((𝑁 + 1) ∈ ℕ0
→ (𝑁 + 1) ∈
ℝ) |
11 | 10 | lep1d 11894 |
. . . . . . . . . . . 12
⊢ ((𝑁 + 1) ∈ ℕ0
→ (𝑁 + 1) ≤ ((𝑁 + 1) + 1)) |
12 | 11 | 3ad2ant1 1132 |
. . . . . . . . . . 11
⊢ (((𝑁 + 1) ∈ ℕ0
∧ 𝑊 ∈ Word
(Vtx‘𝐺) ∧
(♯‘𝑊) = ((𝑁 + 1) + 1)) → (𝑁 + 1) ≤ ((𝑁 + 1) + 1)) |
13 | | breq2 5078 |
. . . . . . . . . . . 12
⊢
((♯‘𝑊) =
((𝑁 + 1) + 1) →
((𝑁 + 1) ≤
(♯‘𝑊) ↔
(𝑁 + 1) ≤ ((𝑁 + 1) + 1))) |
14 | 13 | 3ad2ant3 1134 |
. . . . . . . . . . 11
⊢ (((𝑁 + 1) ∈ ℕ0
∧ 𝑊 ∈ Word
(Vtx‘𝐺) ∧
(♯‘𝑊) = ((𝑁 + 1) + 1)) → ((𝑁 + 1) ≤ (♯‘𝑊) ↔ (𝑁 + 1) ≤ ((𝑁 + 1) + 1))) |
15 | 12, 14 | mpbird 256 |
. . . . . . . . . 10
⊢ (((𝑁 + 1) ∈ ℕ0
∧ 𝑊 ∈ Word
(Vtx‘𝐺) ∧
(♯‘𝑊) = ((𝑁 + 1) + 1)) → (𝑁 + 1) ≤ (♯‘𝑊)) |
16 | 15 | adantr 481 |
. . . . . . . . 9
⊢ ((((𝑁 + 1) ∈ ℕ0
∧ 𝑊 ∈ Word
(Vtx‘𝐺) ∧
(♯‘𝑊) = ((𝑁 + 1) + 1)) ∧ 𝑁 ∈ ℕ0)
→ (𝑁 + 1) ≤
(♯‘𝑊)) |
17 | | nn0p1elfzo 13418 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ (♯‘𝑊)
∈ ℕ0 ∧ (𝑁 + 1) ≤ (♯‘𝑊)) → 𝑁 ∈ (0..^(♯‘𝑊))) |
18 | 9, 8, 16, 17 | syl3anc 1370 |
. . . . . . . 8
⊢ ((((𝑁 + 1) ∈ ℕ0
∧ 𝑊 ∈ Word
(Vtx‘𝐺) ∧
(♯‘𝑊) = ((𝑁 + 1) + 1)) ∧ 𝑁 ∈ ℕ0)
→ 𝑁 ∈
(0..^(♯‘𝑊))) |
19 | | fz0add1fz1 13445 |
. . . . . . . 8
⊢
(((♯‘𝑊)
∈ ℕ0 ∧ 𝑁 ∈ (0..^(♯‘𝑊))) → (𝑁 + 1) ∈ (1...(♯‘𝑊))) |
20 | 8, 18, 19 | syl2anc 584 |
. . . . . . 7
⊢ ((((𝑁 + 1) ∈ ℕ0
∧ 𝑊 ∈ Word
(Vtx‘𝐺) ∧
(♯‘𝑊) = ((𝑁 + 1) + 1)) ∧ 𝑁 ∈ ℕ0)
→ (𝑁 + 1) ∈
(1...(♯‘𝑊))) |
21 | 2, 20 | jca 512 |
. . . . . 6
⊢ ((((𝑁 + 1) ∈ ℕ0
∧ 𝑊 ∈ Word
(Vtx‘𝐺) ∧
(♯‘𝑊) = ((𝑁 + 1) + 1)) ∧ 𝑁 ∈ ℕ0)
→ (𝑊 ∈ Word
(Vtx‘𝐺) ∧ (𝑁 + 1) ∈
(1...(♯‘𝑊)))) |
22 | 21 | ex 413 |
. . . . 5
⊢ (((𝑁 + 1) ∈ ℕ0
∧ 𝑊 ∈ Word
(Vtx‘𝐺) ∧
(♯‘𝑊) = ((𝑁 + 1) + 1)) → (𝑁 ∈ ℕ0
→ (𝑊 ∈ Word
(Vtx‘𝐺) ∧ (𝑁 + 1) ∈
(1...(♯‘𝑊))))) |
23 | 1, 22 | syl 17 |
. . . 4
⊢ (𝑊 ∈ ((𝑁 + 1) WWalksN 𝐺) → (𝑁 ∈ ℕ0 → (𝑊 ∈ Word (Vtx‘𝐺) ∧ (𝑁 + 1) ∈ (1...(♯‘𝑊))))) |
24 | | wwlksnextprop.x |
. . . 4
⊢ 𝑋 = ((𝑁 + 1) WWalksN 𝐺) |
25 | 23, 24 | eleq2s 2857 |
. . 3
⊢ (𝑊 ∈ 𝑋 → (𝑁 ∈ ℕ0 → (𝑊 ∈ Word (Vtx‘𝐺) ∧ (𝑁 + 1) ∈ (1...(♯‘𝑊))))) |
26 | 25 | imp 407 |
. 2
⊢ ((𝑊 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) → (𝑊 ∈ Word (Vtx‘𝐺) ∧ (𝑁 + 1) ∈ (1...(♯‘𝑊)))) |
27 | | pfxfv0 14393 |
. 2
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ (𝑁 + 1) ∈ (1...(♯‘𝑊))) → ((𝑊 prefix (𝑁 + 1))‘0) = (𝑊‘0)) |
28 | 26, 27 | syl 17 |
1
⊢ ((𝑊 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) → ((𝑊 prefix (𝑁 + 1))‘0) = (𝑊‘0)) |