Step | Hyp | Ref
| Expression |
1 | | wwlknbp1 28789 |
. . . 4
⢠(ð â (ð WWalksN ðº) â (ð â â0 ⧠ð â Word (Vtxâðº) ⧠(â¯âð) = (ð + 1))) |
2 | | wwlksnwwlksnon.v |
. . . . . . . . . . 11
⢠ð = (Vtxâðº) |
3 | 2 | eqcomi 2745 |
. . . . . . . . . 10
â¢
(Vtxâðº) =
ð |
4 | 3 | wrdeqi 14425 |
. . . . . . . . 9
⢠Word
(Vtxâðº) = Word ð |
5 | 4 | eleq2i 2829 |
. . . . . . . 8
⢠(ð â Word (Vtxâðº) â ð â Word ð) |
6 | 5 | biimpi 215 |
. . . . . . 7
⢠(ð â Word (Vtxâðº) â ð â Word ð) |
7 | 6 | 3ad2ant2 1134 |
. . . . . 6
⢠((ð â â0
⧠ð â Word
(Vtxâðº) â§
(â¯âð) = (ð + 1)) â ð â Word ð) |
8 | | nn0p1nn 12452 |
. . . . . . . . . 10
⢠(ð â â0
â (ð + 1) â
â) |
9 | | lbfzo0 13612 |
. . . . . . . . . 10
⢠(0 â
(0..^(ð + 1)) â (ð + 1) â
â) |
10 | 8, 9 | sylibr 233 |
. . . . . . . . 9
⢠(ð â â0
â 0 â (0..^(ð +
1))) |
11 | 10 | 3ad2ant1 1133 |
. . . . . . . 8
⢠((ð â â0
⧠ð â Word
(Vtxâðº) â§
(â¯âð) = (ð + 1)) â 0 â
(0..^(ð +
1))) |
12 | | oveq2 7365 |
. . . . . . . . . 10
â¢
((â¯âð) =
(ð + 1) â
(0..^(â¯âð)) =
(0..^(ð +
1))) |
13 | 12 | eleq2d 2823 |
. . . . . . . . 9
â¢
((â¯âð) =
(ð + 1) â (0 â
(0..^(â¯âð))
â 0 â (0..^(ð +
1)))) |
14 | 13 | 3ad2ant3 1135 |
. . . . . . . 8
⢠((ð â â0
⧠ð â Word
(Vtxâðº) â§
(â¯âð) = (ð + 1)) â (0 â
(0..^(â¯âð))
â 0 â (0..^(ð +
1)))) |
15 | 11, 14 | mpbird 256 |
. . . . . . 7
⢠((ð â â0
⧠ð â Word
(Vtxâðº) â§
(â¯âð) = (ð + 1)) â 0 â
(0..^(â¯âð))) |
16 | 15 | adantl 482 |
. . . . . 6
⢠((ð â (ð WWalksN ðº) ⧠(ð â â0 ⧠ð â Word (Vtxâðº) ⧠(â¯âð) = (ð + 1))) â 0 â
(0..^(â¯âð))) |
17 | | wrdsymbcl 14415 |
. . . . . 6
⢠((ð â Word ð ⧠0 â (0..^(â¯âð))) â (ðâ0) â ð) |
18 | 7, 16, 17 | syl2an2 684 |
. . . . 5
⢠((ð â (ð WWalksN ðº) ⧠(ð â â0 ⧠ð â Word (Vtxâðº) ⧠(â¯âð) = (ð + 1))) â (ðâ0) â ð) |
19 | | fzonn0p1 13649 |
. . . . . . . . 9
⢠(ð â â0
â ð â (0..^(ð + 1))) |
20 | 19 | 3ad2ant1 1133 |
. . . . . . . 8
⢠((ð â â0
⧠ð â Word
(Vtxâðº) â§
(â¯âð) = (ð + 1)) â ð â (0..^(ð + 1))) |
21 | 12 | eleq2d 2823 |
. . . . . . . . 9
â¢
((â¯âð) =
(ð + 1) â (ð â
(0..^(â¯âð))
â ð â (0..^(ð + 1)))) |
22 | 21 | 3ad2ant3 1135 |
. . . . . . . 8
⢠((ð â â0
⧠ð â Word
(Vtxâðº) â§
(â¯âð) = (ð + 1)) â (ð â (0..^(â¯âð)) â ð â (0..^(ð + 1)))) |
23 | 20, 22 | mpbird 256 |
. . . . . . 7
⢠((ð â â0
⧠ð â Word
(Vtxâðº) â§
(â¯âð) = (ð + 1)) â ð â (0..^(â¯âð))) |
24 | | wrdsymbcl 14415 |
. . . . . . 7
⢠((ð â Word ð ⧠ð â (0..^(â¯âð))) â (ðâð) â ð) |
25 | 7, 23, 24 | syl2anc 584 |
. . . . . 6
⢠((ð â â0
⧠ð â Word
(Vtxâðº) â§
(â¯âð) = (ð + 1)) â (ðâð) â ð) |
26 | 25 | adantl 482 |
. . . . 5
⢠((ð â (ð WWalksN ðº) ⧠(ð â â0 ⧠ð â Word (Vtxâðº) ⧠(â¯âð) = (ð + 1))) â (ðâð) â ð) |
27 | | simpl 483 |
. . . . 5
⢠((ð â (ð WWalksN ðº) ⧠(ð â â0 ⧠ð â Word (Vtxâðº) ⧠(â¯âð) = (ð + 1))) â ð â (ð WWalksN ðº)) |
28 | | eqidd 2737 |
. . . . 5
⢠((ð â (ð WWalksN ðº) ⧠(ð â â0 ⧠ð â Word (Vtxâðº) ⧠(â¯âð) = (ð + 1))) â (ðâ0) = (ðâ0)) |
29 | | eqidd 2737 |
. . . . 5
⢠((ð â (ð WWalksN ðº) ⧠(ð â â0 ⧠ð â Word (Vtxâðº) ⧠(â¯âð) = (ð + 1))) â (ðâð) = (ðâð)) |
30 | | eqeq2 2748 |
. . . . . . 7
⢠(ð = (ðâ0) â ((ðâ0) = ð â (ðâ0) = (ðâ0))) |
31 | 30 | 3anbi2d 1441 |
. . . . . 6
⢠(ð = (ðâ0) â ((ð â (ð WWalksN ðº) ⧠(ðâ0) = ð ⧠(ðâð) = ð) â (ð â (ð WWalksN ðº) ⧠(ðâ0) = (ðâ0) ⧠(ðâð) = ð))) |
32 | | eqeq2 2748 |
. . . . . . 7
⢠(ð = (ðâð) â ((ðâð) = ð â (ðâð) = (ðâð))) |
33 | 32 | 3anbi3d 1442 |
. . . . . 6
⢠(ð = (ðâð) â ((ð â (ð WWalksN ðº) ⧠(ðâ0) = (ðâ0) ⧠(ðâð) = ð) â (ð â (ð WWalksN ðº) ⧠(ðâ0) = (ðâ0) ⧠(ðâð) = (ðâð)))) |
34 | 31, 33 | rspc2ev 3592 |
. . . . 5
⢠(((ðâ0) â ð ⧠(ðâð) â ð ⧠(ð â (ð WWalksN ðº) ⧠(ðâ0) = (ðâ0) ⧠(ðâð) = (ðâð))) â âð â ð âð â ð (ð â (ð WWalksN ðº) ⧠(ðâ0) = ð ⧠(ðâð) = ð)) |
35 | 18, 26, 27, 28, 29, 34 | syl113anc 1382 |
. . . 4
⢠((ð â (ð WWalksN ðº) ⧠(ð â â0 ⧠ð â Word (Vtxâðº) ⧠(â¯âð) = (ð + 1))) â âð â ð âð â ð (ð â (ð WWalksN ðº) ⧠(ðâ0) = ð ⧠(ðâð) = ð)) |
36 | 1, 35 | mpdan 685 |
. . 3
⢠(ð â (ð WWalksN ðº) â âð â ð âð â ð (ð â (ð WWalksN ðº) ⧠(ðâ0) = ð ⧠(ðâð) = ð)) |
37 | | simp1 1136 |
. . . . 5
⢠((ð â (ð WWalksN ðº) ⧠(ðâ0) = ð ⧠(ðâð) = ð) â ð â (ð WWalksN ðº)) |
38 | 37 | a1i 11 |
. . . 4
⢠((ð â ð ⧠ð â ð) â ((ð â (ð WWalksN ðº) ⧠(ðâ0) = ð ⧠(ðâð) = ð) â ð â (ð WWalksN ðº))) |
39 | 38 | rexlimivv 3196 |
. . 3
â¢
(âð â
ð âð â ð (ð â (ð WWalksN ðº) ⧠(ðâ0) = ð ⧠(ðâð) = ð) â ð â (ð WWalksN ðº)) |
40 | 36, 39 | impbii 208 |
. 2
⢠(ð â (ð WWalksN ðº) â âð â ð âð â ð (ð â (ð WWalksN ðº) ⧠(ðâ0) = ð ⧠(ðâð) = ð)) |
41 | | wwlknon 28802 |
. . . 4
⢠(ð â (ð(ð WWalksNOn ðº)ð) â (ð â (ð WWalksN ðº) ⧠(ðâ0) = ð ⧠(ðâð) = ð)) |
42 | 41 | bicomi 223 |
. . 3
⢠((ð â (ð WWalksN ðº) ⧠(ðâ0) = ð ⧠(ðâð) = ð) â ð â (ð(ð WWalksNOn ðº)ð)) |
43 | 42 | 2rexbii 3128 |
. 2
â¢
(âð â
ð âð â ð (ð â (ð WWalksN ðº) ⧠(ðâ0) = ð ⧠(ðâð) = ð) â âð â ð âð â ð ð â (ð(ð WWalksNOn ðº)ð)) |
44 | 40, 43 | bitri 274 |
1
⢠(ð â (ð WWalksN ðº) â âð â ð âð â ð ð â (ð(ð WWalksNOn ðº)ð)) |