Step | Hyp | Ref
| Expression |
1 | | wwlknbp1 29098 |
. . . . 5
⢠(ð â ((ð + 1) WWalksN ðº) â ((ð + 1) â â0 ⧠ð â Word (Vtxâðº) ⧠(â¯âð) = ((ð + 1) + 1))) |
2 | | simpl2 1193 |
. . . . . . 7
⢠((((ð + 1) â â0
⧠ð â Word
(Vtxâðº) â§
(â¯âð) = ((ð + 1) + 1)) ⧠ð â â0)
â ð â Word
(Vtxâðº)) |
3 | | peano2nn0 12512 |
. . . . . . . . . . 11
⢠((ð + 1) â â0
â ((ð + 1) + 1) â
â0) |
4 | 3 | 3ad2ant1 1134 |
. . . . . . . . . 10
⢠(((ð + 1) â â0
⧠ð â Word
(Vtxâðº) â§
(â¯âð) = ((ð + 1) + 1)) â ((ð + 1) + 1) â
â0) |
5 | | eleq1 2822 |
. . . . . . . . . . 11
â¢
((â¯âð) =
((ð + 1) + 1) â
((â¯âð) â
â0 â ((ð + 1) + 1) â
â0)) |
6 | 5 | 3ad2ant3 1136 |
. . . . . . . . . 10
⢠(((ð + 1) â â0
⧠ð â Word
(Vtxâðº) â§
(â¯âð) = ((ð + 1) + 1)) â
((â¯âð) â
â0 â ((ð + 1) + 1) â
â0)) |
7 | 4, 6 | mpbird 257 |
. . . . . . . . 9
⢠(((ð + 1) â â0
⧠ð â Word
(Vtxâðº) â§
(â¯âð) = ((ð + 1) + 1)) â
(â¯âð) â
â0) |
8 | 7 | adantr 482 |
. . . . . . . 8
⢠((((ð + 1) â â0
⧠ð â Word
(Vtxâðº) â§
(â¯âð) = ((ð + 1) + 1)) ⧠ð â â0)
â (â¯âð)
â â0) |
9 | | simpr 486 |
. . . . . . . . 9
⢠((((ð + 1) â â0
⧠ð â Word
(Vtxâðº) â§
(â¯âð) = ((ð + 1) + 1)) ⧠ð â â0)
â ð â
â0) |
10 | | nn0re 12481 |
. . . . . . . . . . . . 13
⢠((ð + 1) â â0
â (ð + 1) â
â) |
11 | 10 | lep1d 12145 |
. . . . . . . . . . . 12
⢠((ð + 1) â â0
â (ð + 1) †((ð + 1) + 1)) |
12 | 11 | 3ad2ant1 1134 |
. . . . . . . . . . 11
⢠(((ð + 1) â â0
⧠ð â Word
(Vtxâðº) â§
(â¯âð) = ((ð + 1) + 1)) â (ð + 1) †((ð + 1) + 1)) |
13 | | breq2 5153 |
. . . . . . . . . . . 12
â¢
((â¯âð) =
((ð + 1) + 1) â
((ð + 1) â€
(â¯âð) â
(ð + 1) †((ð + 1) + 1))) |
14 | 13 | 3ad2ant3 1136 |
. . . . . . . . . . 11
⢠(((ð + 1) â â0
⧠ð â Word
(Vtxâðº) â§
(â¯âð) = ((ð + 1) + 1)) â ((ð + 1) †(â¯âð) â (ð + 1) †((ð + 1) + 1))) |
15 | 12, 14 | mpbird 257 |
. . . . . . . . . 10
⢠(((ð + 1) â â0
⧠ð â Word
(Vtxâðº) â§
(â¯âð) = ((ð + 1) + 1)) â (ð + 1) †(â¯âð)) |
16 | 15 | adantr 482 |
. . . . . . . . 9
⢠((((ð + 1) â â0
⧠ð â Word
(Vtxâðº) â§
(â¯âð) = ((ð + 1) + 1)) ⧠ð â â0)
â (ð + 1) â€
(â¯âð)) |
17 | | nn0p1elfzo 13675 |
. . . . . . . . 9
⢠((ð â â0
⧠(â¯âð)
â â0 ⧠(ð + 1) †(â¯âð)) â ð â (0..^(â¯âð))) |
18 | 9, 8, 16, 17 | syl3anc 1372 |
. . . . . . . 8
⢠((((ð + 1) â â0
⧠ð â Word
(Vtxâðº) â§
(â¯âð) = ((ð + 1) + 1)) ⧠ð â â0)
â ð â
(0..^(â¯âð))) |
19 | | fz0add1fz1 13702 |
. . . . . . . 8
â¢
(((â¯âð)
â â0 ⧠ð â (0..^(â¯âð))) â (ð + 1) â (1...(â¯âð))) |
20 | 8, 18, 19 | syl2anc 585 |
. . . . . . 7
⢠((((ð + 1) â â0
⧠ð â Word
(Vtxâðº) â§
(â¯âð) = ((ð + 1) + 1)) ⧠ð â â0)
â (ð + 1) â
(1...(â¯âð))) |
21 | 2, 20 | jca 513 |
. . . . . 6
⢠((((ð + 1) â â0
⧠ð â Word
(Vtxâðº) â§
(â¯âð) = ((ð + 1) + 1)) ⧠ð â â0)
â (ð â Word
(Vtxâðº) ⧠(ð + 1) â
(1...(â¯âð)))) |
22 | 21 | ex 414 |
. . . . 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 2852 |
. . 3
⢠(ð â ð â (ð â â0 â (ð â Word (Vtxâðº) ⧠(ð + 1) â (1...(â¯âð))))) |
26 | 25 | imp 408 |
. 2
⢠((ð â ð ⧠ð â â0) â (ð â Word (Vtxâðº) ⧠(ð + 1) â (1...(â¯âð)))) |
27 | | pfxfv0 14642 |
. 2
⢠((ð â Word (Vtxâðº) ⧠(ð + 1) â (1...(â¯âð))) â ((ð prefix (ð + 1))â0) = (ðâ0)) |
28 | 26, 27 | syl 17 |
1
⢠((ð â ð ⧠ð â â0) â ((ð prefix (ð + 1))â0) = (ðâ0)) |