Step | Hyp | Ref
| Expression |
1 | | numclwwlk.v |
. . . . . 6
β’ π = (VtxβπΊ) |
2 | | numclwwlk.q |
. . . . . 6
β’ π = (π£ β π, π β β β¦ {π€ β (π WWalksN πΊ) β£ ((π€β0) = π£ β§ (lastSβπ€) β π£)}) |
3 | 1, 2 | numclwwlkovq 29318 |
. . . . 5
β’ ((π β π β§ π β β) β (πππ) = {π€ β (π WWalksN πΊ) β£ ((π€β0) = π β§ (lastSβπ€) β π)}) |
4 | 3 | 3adant1 1130 |
. . . 4
β’ ((πΊ β FriendGraph β§ π β π β§ π β β) β (πππ) = {π€ β (π WWalksN πΊ) β£ ((π€β0) = π β§ (lastSβπ€) β π)}) |
5 | 4 | eleq2d 2823 |
. . 3
β’ ((πΊ β FriendGraph β§ π β π β§ π β β) β (π β (πππ) β π β {π€ β (π WWalksN πΊ) β£ ((π€β0) = π β§ (lastSβπ€) β π)})) |
6 | | fveq1 6841 |
. . . . . 6
β’ (π€ = π β (π€β0) = (πβ0)) |
7 | 6 | eqeq1d 2738 |
. . . . 5
β’ (π€ = π β ((π€β0) = π β (πβ0) = π)) |
8 | | fveq2 6842 |
. . . . . 6
β’ (π€ = π β (lastSβπ€) = (lastSβπ)) |
9 | 8 | neeq1d 3003 |
. . . . 5
β’ (π€ = π β ((lastSβπ€) β π β (lastSβπ) β π)) |
10 | 7, 9 | anbi12d 631 |
. . . 4
β’ (π€ = π β (((π€β0) = π β§ (lastSβπ€) β π) β ((πβ0) = π β§ (lastSβπ) β π))) |
11 | 10 | elrab 3645 |
. . 3
β’ (π β {π€ β (π WWalksN πΊ) β£ ((π€β0) = π β§ (lastSβπ€) β π)} β (π β (π WWalksN πΊ) β§ ((πβ0) = π β§ (lastSβπ) β π))) |
12 | 5, 11 | bitrdi 286 |
. 2
β’ ((πΊ β FriendGraph β§ π β π β§ π β β) β (π β (πππ) β (π β (π WWalksN πΊ) β§ ((πβ0) = π β§ (lastSβπ) β π)))) |
13 | | simpl1 1191 |
. . . . 5
β’ (((πΊ β FriendGraph β§ π β π β§ π β β) β§ (π β (π WWalksN πΊ) β§ ((πβ0) = π β§ (lastSβπ) β π))) β πΊ β FriendGraph ) |
14 | | eqid 2736 |
. . . . . . . . . . . . 13
β’
(EdgβπΊ) =
(EdgβπΊ) |
15 | 1, 14 | wwlknp 28788 |
. . . . . . . . . . . 12
β’ (π β (π WWalksN πΊ) β (π β Word π β§ (β―βπ) = (π + 1) β§ βπ β (0..^π){(πβπ), (πβ(π + 1))} β (EdgβπΊ))) |
16 | | peano2nn 12165 |
. . . . . . . . . . . . . . . 16
β’ (π β β β (π + 1) β
β) |
17 | 16 | adantl 482 |
. . . . . . . . . . . . . . 15
β’ (((π β Word π β§ (β―βπ) = (π + 1)) β§ π β β) β (π + 1) β β) |
18 | | simpl 483 |
. . . . . . . . . . . . . . 15
β’ (((π β Word π β§ (β―βπ) = (π + 1)) β§ π β β) β (π β Word π β§ (β―βπ) = (π + 1))) |
19 | 17, 18 | jca 512 |
. . . . . . . . . . . . . 14
β’ (((π β Word π β§ (β―βπ) = (π + 1)) β§ π β β) β ((π + 1) β β β§ (π β Word π β§ (β―βπ) = (π + 1)))) |
20 | 19 | ex 413 |
. . . . . . . . . . . . 13
β’ ((π β Word π β§ (β―βπ) = (π + 1)) β (π β β β ((π + 1) β β β§ (π β Word π β§ (β―βπ) = (π + 1))))) |
21 | 20 | 3adant3 1132 |
. . . . . . . . . . . 12
β’ ((π β Word π β§ (β―βπ) = (π + 1) β§ βπ β (0..^π){(πβπ), (πβ(π + 1))} β (EdgβπΊ)) β (π β β β ((π + 1) β β β§ (π β Word π β§ (β―βπ) = (π + 1))))) |
22 | 15, 21 | syl 17 |
. . . . . . . . . . 11
β’ (π β (π WWalksN πΊ) β (π β β β ((π + 1) β β β§ (π β Word π β§ (β―βπ) = (π + 1))))) |
23 | | lswlgt0cl 14457 |
. . . . . . . . . . 11
β’ (((π + 1) β β β§
(π β Word π β§ (β―βπ) = (π + 1))) β (lastSβπ) β π) |
24 | 22, 23 | syl6 35 |
. . . . . . . . . 10
β’ (π β (π WWalksN πΊ) β (π β β β (lastSβπ) β π)) |
25 | 24 | adantr 481 |
. . . . . . . . 9
β’ ((π β (π WWalksN πΊ) β§ ((πβ0) = π β§ (lastSβπ) β π)) β (π β β β (lastSβπ) β π)) |
26 | 25 | com12 32 |
. . . . . . . 8
β’ (π β β β ((π β (π WWalksN πΊ) β§ ((πβ0) = π β§ (lastSβπ) β π)) β (lastSβπ) β π)) |
27 | 26 | 3ad2ant3 1135 |
. . . . . . 7
β’ ((πΊ β FriendGraph β§ π β π β§ π β β) β ((π β (π WWalksN πΊ) β§ ((πβ0) = π β§ (lastSβπ) β π)) β (lastSβπ) β π)) |
28 | 27 | imp 407 |
. . . . . 6
β’ (((πΊ β FriendGraph β§ π β π β§ π β β) β§ (π β (π WWalksN πΊ) β§ ((πβ0) = π β§ (lastSβπ) β π))) β (lastSβπ) β π) |
29 | | eleq1 2825 |
. . . . . . . . . . 11
β’ ((πβ0) = π β ((πβ0) β π β π β π)) |
30 | 29 | biimprd 247 |
. . . . . . . . . 10
β’ ((πβ0) = π β (π β π β (πβ0) β π)) |
31 | 30 | ad2antrl 726 |
. . . . . . . . 9
β’ ((π β (π WWalksN πΊ) β§ ((πβ0) = π β§ (lastSβπ) β π)) β (π β π β (πβ0) β π)) |
32 | 31 | com12 32 |
. . . . . . . 8
β’ (π β π β ((π β (π WWalksN πΊ) β§ ((πβ0) = π β§ (lastSβπ) β π)) β (πβ0) β π)) |
33 | 32 | 3ad2ant2 1134 |
. . . . . . 7
β’ ((πΊ β FriendGraph β§ π β π β§ π β β) β ((π β (π WWalksN πΊ) β§ ((πβ0) = π β§ (lastSβπ) β π)) β (πβ0) β π)) |
34 | 33 | imp 407 |
. . . . . 6
β’ (((πΊ β FriendGraph β§ π β π β§ π β β) β§ (π β (π WWalksN πΊ) β§ ((πβ0) = π β§ (lastSβπ) β π))) β (πβ0) β π) |
35 | | neeq2 3007 |
. . . . . . . . . 10
β’ (π = (πβ0) β ((lastSβπ) β π β (lastSβπ) β (πβ0))) |
36 | 35 | eqcoms 2744 |
. . . . . . . . 9
β’ ((πβ0) = π β ((lastSβπ) β π β (lastSβπ) β (πβ0))) |
37 | 36 | biimpa 477 |
. . . . . . . 8
β’ (((πβ0) = π β§ (lastSβπ) β π) β (lastSβπ) β (πβ0)) |
38 | 37 | adantl 482 |
. . . . . . 7
β’ ((π β (π WWalksN πΊ) β§ ((πβ0) = π β§ (lastSβπ) β π)) β (lastSβπ) β (πβ0)) |
39 | 38 | adantl 482 |
. . . . . 6
β’ (((πΊ β FriendGraph β§ π β π β§ π β β) β§ (π β (π WWalksN πΊ) β§ ((πβ0) = π β§ (lastSβπ) β π))) β (lastSβπ) β (πβ0)) |
40 | 28, 34, 39 | 3jca 1128 |
. . . . 5
β’ (((πΊ β FriendGraph β§ π β π β§ π β β) β§ (π β (π WWalksN πΊ) β§ ((πβ0) = π β§ (lastSβπ) β π))) β ((lastSβπ) β π β§ (πβ0) β π β§ (lastSβπ) β (πβ0))) |
41 | 1, 14 | frcond2 29211 |
. . . . 5
β’ (πΊ β FriendGraph β
(((lastSβπ) β
π β§ (πβ0) β π β§ (lastSβπ) β (πβ0)) β β!π£ β π ({(lastSβπ), π£} β (EdgβπΊ) β§ {π£, (πβ0)} β (EdgβπΊ)))) |
42 | 13, 40, 41 | sylc 65 |
. . . 4
β’ (((πΊ β FriendGraph β§ π β π β§ π β β) β§ (π β (π WWalksN πΊ) β§ ((πβ0) = π β§ (lastSβπ) β π))) β β!π£ β π ({(lastSβπ), π£} β (EdgβπΊ) β§ {π£, (πβ0)} β (EdgβπΊ))) |
43 | | simpl 483 |
. . . . . . . . . 10
β’ ((π β (π WWalksN πΊ) β§ ((πβ0) = π β§ (lastSβπ) β π)) β π β (π WWalksN πΊ)) |
44 | 43 | ad2antlr 725 |
. . . . . . . . 9
β’ ((((πΊ β FriendGraph β§ π β π β§ π β β) β§ (π β (π WWalksN πΊ) β§ ((πβ0) = π β§ (lastSβπ) β π))) β§ π£ β π) β π β (π WWalksN πΊ)) |
45 | | simpr 485 |
. . . . . . . . 9
β’ ((((πΊ β FriendGraph β§ π β π β§ π β β) β§ (π β (π WWalksN πΊ) β§ ((πβ0) = π β§ (lastSβπ) β π))) β§ π£ β π) β π£ β π) |
46 | | nnnn0 12420 |
. . . . . . . . . . 11
β’ (π β β β π β
β0) |
47 | 46 | 3ad2ant3 1135 |
. . . . . . . . . 10
β’ ((πΊ β FriendGraph β§ π β π β§ π β β) β π β
β0) |
48 | 47 | ad2antrr 724 |
. . . . . . . . 9
β’ ((((πΊ β FriendGraph β§ π β π β§ π β β) β§ (π β (π WWalksN πΊ) β§ ((πβ0) = π β§ (lastSβπ) β π))) β§ π£ β π) β π β
β0) |
49 | 44, 45, 48 | 3jca 1128 |
. . . . . . . 8
β’ ((((πΊ β FriendGraph β§ π β π β§ π β β) β§ (π β (π WWalksN πΊ) β§ ((πβ0) = π β§ (lastSβπ) β π))) β§ π£ β π) β (π β (π WWalksN πΊ) β§ π£ β π β§ π β
β0)) |
50 | 1, 14 | wwlksext2clwwlk 29001 |
. . . . . . . . . 10
β’ ((π β (π WWalksN πΊ) β§ π£ β π) β (({(lastSβπ), π£} β (EdgβπΊ) β§ {π£, (πβ0)} β (EdgβπΊ)) β (π ++ β¨βπ£ββ©) β ((π + 2) ClWWalksN πΊ))) |
51 | 50 | 3adant3 1132 |
. . . . . . . . 9
β’ ((π β (π WWalksN πΊ) β§ π£ β π β§ π β β0) β
(({(lastSβπ), π£} β (EdgβπΊ) β§ {π£, (πβ0)} β (EdgβπΊ)) β (π ++ β¨βπ£ββ©) β ((π + 2) ClWWalksN πΊ))) |
52 | 51 | imp 407 |
. . . . . . . 8
β’ (((π β (π WWalksN πΊ) β§ π£ β π β§ π β β0) β§
({(lastSβπ), π£} β (EdgβπΊ) β§ {π£, (πβ0)} β (EdgβπΊ))) β (π ++ β¨βπ£ββ©) β ((π + 2) ClWWalksN πΊ)) |
53 | 49, 52 | sylan 580 |
. . . . . . 7
β’
(((((πΊ β
FriendGraph β§ π β
π β§ π β β) β§ (π β (π WWalksN πΊ) β§ ((πβ0) = π β§ (lastSβπ) β π))) β§ π£ β π) β§ ({(lastSβπ), π£} β (EdgβπΊ) β§ {π£, (πβ0)} β (EdgβπΊ))) β (π ++ β¨βπ£ββ©) β ((π + 2) ClWWalksN πΊ)) |
54 | 1 | wwlknbp 28787 |
. . . . . . . . . . 11
β’ (π β (π WWalksN πΊ) β (πΊ β V β§ π β β0 β§ π β Word π)) |
55 | 54 | simp3d 1144 |
. . . . . . . . . 10
β’ (π β (π WWalksN πΊ) β π β Word π) |
56 | 55 | ad2antrl 726 |
. . . . . . . . 9
β’ (((πΊ β FriendGraph β§ π β π β§ π β β) β§ (π β (π WWalksN πΊ) β§ ((πβ0) = π β§ (lastSβπ) β π))) β π β Word π) |
57 | 56 | ad2antrr 724 |
. . . . . . . 8
β’
(((((πΊ β
FriendGraph β§ π β
π β§ π β β) β§ (π β (π WWalksN πΊ) β§ ((πβ0) = π β§ (lastSβπ) β π))) β§ π£ β π) β§ (π ++ β¨βπ£ββ©) β ((π + 2) ClWWalksN πΊ)) β π β Word π) |
58 | 45 | adantr 481 |
. . . . . . . 8
β’
(((((πΊ β
FriendGraph β§ π β
π β§ π β β) β§ (π β (π WWalksN πΊ) β§ ((πβ0) = π β§ (lastSβπ) β π))) β§ π£ β π) β§ (π ++ β¨βπ£ββ©) β ((π + 2) ClWWalksN πΊ)) β π£ β π) |
59 | | 2z 12535 |
. . . . . . . . . . 11
β’ 2 β
β€ |
60 | | nn0pzuz 12830 |
. . . . . . . . . . 11
β’ ((π β β0
β§ 2 β β€) β (π + 2) β
(β€β₯β2)) |
61 | 46, 59, 60 | sylancl 586 |
. . . . . . . . . 10
β’ (π β β β (π + 2) β
(β€β₯β2)) |
62 | 61 | 3ad2ant3 1135 |
. . . . . . . . 9
β’ ((πΊ β FriendGraph β§ π β π β§ π β β) β (π + 2) β
(β€β₯β2)) |
63 | 62 | ad3antrrr 728 |
. . . . . . . 8
β’
(((((πΊ β
FriendGraph β§ π β
π β§ π β β) β§ (π β (π WWalksN πΊ) β§ ((πβ0) = π β§ (lastSβπ) β π))) β§ π£ β π) β§ (π ++ β¨βπ£ββ©) β ((π + 2) ClWWalksN πΊ)) β (π + 2) β
(β€β₯β2)) |
64 | | simpr 485 |
. . . . . . . 8
β’
(((((πΊ β
FriendGraph β§ π β
π β§ π β β) β§ (π β (π WWalksN πΊ) β§ ((πβ0) = π β§ (lastSβπ) β π))) β§ π£ β π) β§ (π ++ β¨βπ£ββ©) β ((π + 2) ClWWalksN πΊ)) β (π ++ β¨βπ£ββ©) β ((π + 2) ClWWalksN πΊ)) |
65 | 1, 14 | clwwlkext2edg 29000 |
. . . . . . . 8
β’ (((π β Word π β§ π£ β π β§ (π + 2) β
(β€β₯β2)) β§ (π ++ β¨βπ£ββ©) β ((π + 2) ClWWalksN πΊ)) β ({(lastSβπ), π£} β (EdgβπΊ) β§ {π£, (πβ0)} β (EdgβπΊ))) |
66 | 57, 58, 63, 64, 65 | syl31anc 1373 |
. . . . . . 7
β’
(((((πΊ β
FriendGraph β§ π β
π β§ π β β) β§ (π β (π WWalksN πΊ) β§ ((πβ0) = π β§ (lastSβπ) β π))) β§ π£ β π) β§ (π ++ β¨βπ£ββ©) β ((π + 2) ClWWalksN πΊ)) β ({(lastSβπ), π£} β (EdgβπΊ) β§ {π£, (πβ0)} β (EdgβπΊ))) |
67 | 53, 66 | impbida 799 |
. . . . . 6
β’ ((((πΊ β FriendGraph β§ π β π β§ π β β) β§ (π β (π WWalksN πΊ) β§ ((πβ0) = π β§ (lastSβπ) β π))) β§ π£ β π) β (({(lastSβπ), π£} β (EdgβπΊ) β§ {π£, (πβ0)} β (EdgβπΊ)) β (π ++ β¨βπ£ββ©) β ((π + 2) ClWWalksN πΊ))) |
68 | 45, 1 | eleqtrdi 2847 |
. . . . . . . . . 10
β’ ((((πΊ β FriendGraph β§ π β π β§ π β β) β§ (π β (π WWalksN πΊ) β§ ((πβ0) = π β§ (lastSβπ) β π))) β§ π£ β π) β π£ β (VtxβπΊ)) |
69 | 37 | anim2i 617 |
. . . . . . . . . . . 12
β’ ((π β (π WWalksN πΊ) β§ ((πβ0) = π β§ (lastSβπ) β π)) β (π β (π WWalksN πΊ) β§ (lastSβπ) β (πβ0))) |
70 | 69 | ad2antlr 725 |
. . . . . . . . . . 11
β’ ((((πΊ β FriendGraph β§ π β π β§ π β β) β§ (π β (π WWalksN πΊ) β§ ((πβ0) = π β§ (lastSβπ) β π))) β§ π£ β π) β (π β (π WWalksN πΊ) β§ (lastSβπ) β (πβ0))) |
71 | 70 | simprd 496 |
. . . . . . . . . 10
β’ ((((πΊ β FriendGraph β§ π β π β§ π β β) β§ (π β (π WWalksN πΊ) β§ ((πβ0) = π β§ (lastSβπ) β π))) β§ π£ β π) β (lastSβπ) β (πβ0)) |
72 | | numclwwlk2lem1lem 29286 |
. . . . . . . . . 10
β’ ((π£ β (VtxβπΊ) β§ π β (π WWalksN πΊ) β§ (lastSβπ) β (πβ0)) β (((π ++ β¨βπ£ββ©)β0) = (πβ0) β§ ((π ++ β¨βπ£ββ©)βπ) β (πβ0))) |
73 | 68, 44, 71, 72 | syl3anc 1371 |
. . . . . . . . 9
β’ ((((πΊ β FriendGraph β§ π β π β§ π β β) β§ (π β (π WWalksN πΊ) β§ ((πβ0) = π β§ (lastSβπ) β π))) β§ π£ β π) β (((π ++ β¨βπ£ββ©)β0) = (πβ0) β§ ((π ++ β¨βπ£ββ©)βπ) β (πβ0))) |
74 | | eqeq2 2748 |
. . . . . . . . . . . . 13
β’ (π = (πβ0) β (((π ++ β¨βπ£ββ©)β0) = π β ((π ++ β¨βπ£ββ©)β0) = (πβ0))) |
75 | 74 | eqcoms 2744 |
. . . . . . . . . . . 12
β’ ((πβ0) = π β (((π ++ β¨βπ£ββ©)β0) = π β ((π ++ β¨βπ£ββ©)β0) = (πβ0))) |
76 | 75 | ad2antrl 726 |
. . . . . . . . . . 11
β’ ((π β (π WWalksN πΊ) β§ ((πβ0) = π β§ (lastSβπ) β π)) β (((π ++ β¨βπ£ββ©)β0) = π β ((π ++ β¨βπ£ββ©)β0) = (πβ0))) |
77 | 76 | ad2antlr 725 |
. . . . . . . . . 10
β’ ((((πΊ β FriendGraph β§ π β π β§ π β β) β§ (π β (π WWalksN πΊ) β§ ((πβ0) = π β§ (lastSβπ) β π))) β§ π£ β π) β (((π ++ β¨βπ£ββ©)β0) = π β ((π ++ β¨βπ£ββ©)β0) = (πβ0))) |
78 | 73 | simpld 495 |
. . . . . . . . . . 11
β’ ((((πΊ β FriendGraph β§ π β π β§ π β β) β§ (π β (π WWalksN πΊ) β§ ((πβ0) = π β§ (lastSβπ) β π))) β§ π£ β π) β ((π ++ β¨βπ£ββ©)β0) = (πβ0)) |
79 | 78 | neeq2d 3004 |
. . . . . . . . . 10
β’ ((((πΊ β FriendGraph β§ π β π β§ π β β) β§ (π β (π WWalksN πΊ) β§ ((πβ0) = π β§ (lastSβπ) β π))) β§ π£ β π) β (((π ++ β¨βπ£ββ©)βπ) β ((π ++ β¨βπ£ββ©)β0) β ((π ++ β¨βπ£ββ©)βπ) β (πβ0))) |
80 | 77, 79 | anbi12d 631 |
. . . . . . . . 9
β’ ((((πΊ β FriendGraph β§ π β π β§ π β β) β§ (π β (π WWalksN πΊ) β§ ((πβ0) = π β§ (lastSβπ) β π))) β§ π£ β π) β ((((π ++ β¨βπ£ββ©)β0) = π β§ ((π ++ β¨βπ£ββ©)βπ) β ((π ++ β¨βπ£ββ©)β0)) β (((π ++ β¨βπ£ββ©)β0) = (πβ0) β§ ((π ++ β¨βπ£ββ©)βπ) β (πβ0)))) |
81 | 73, 80 | mpbird 256 |
. . . . . . . 8
β’ ((((πΊ β FriendGraph β§ π β π β§ π β β) β§ (π β (π WWalksN πΊ) β§ ((πβ0) = π β§ (lastSβπ) β π))) β§ π£ β π) β (((π ++ β¨βπ£ββ©)β0) = π β§ ((π ++ β¨βπ£ββ©)βπ) β ((π ++ β¨βπ£ββ©)β0))) |
82 | | nncn 12161 |
. . . . . . . . . . . . . 14
β’ (π β β β π β
β) |
83 | | 2cnd 12231 |
. . . . . . . . . . . . . 14
β’ (π β β β 2 β
β) |
84 | 82, 83 | pncand 11513 |
. . . . . . . . . . . . 13
β’ (π β β β ((π + 2) β 2) = π) |
85 | 84 | 3ad2ant3 1135 |
. . . . . . . . . . . 12
β’ ((πΊ β FriendGraph β§ π β π β§ π β β) β ((π + 2) β 2) = π) |
86 | 85 | ad2antrr 724 |
. . . . . . . . . . 11
β’ ((((πΊ β FriendGraph β§ π β π β§ π β β) β§ (π β (π WWalksN πΊ) β§ ((πβ0) = π β§ (lastSβπ) β π))) β§ π£ β π) β ((π + 2) β 2) = π) |
87 | 86 | fveq2d 6846 |
. . . . . . . . . 10
β’ ((((πΊ β FriendGraph β§ π β π β§ π β β) β§ (π β (π WWalksN πΊ) β§ ((πβ0) = π β§ (lastSβπ) β π))) β§ π£ β π) β ((π ++ β¨βπ£ββ©)β((π + 2) β 2)) = ((π ++ β¨βπ£ββ©)βπ)) |
88 | 87 | neeq1d 3003 |
. . . . . . . . 9
β’ ((((πΊ β FriendGraph β§ π β π β§ π β β) β§ (π β (π WWalksN πΊ) β§ ((πβ0) = π β§ (lastSβπ) β π))) β§ π£ β π) β (((π ++ β¨βπ£ββ©)β((π + 2) β 2)) β ((π ++ β¨βπ£ββ©)β0) β ((π ++ β¨βπ£ββ©)βπ) β ((π ++ β¨βπ£ββ©)β0))) |
89 | 88 | anbi2d 629 |
. . . . . . . 8
β’ ((((πΊ β FriendGraph β§ π β π β§ π β β) β§ (π β (π WWalksN πΊ) β§ ((πβ0) = π β§ (lastSβπ) β π))) β§ π£ β π) β ((((π ++ β¨βπ£ββ©)β0) = π β§ ((π ++ β¨βπ£ββ©)β((π + 2) β 2)) β ((π ++ β¨βπ£ββ©)β0)) β (((π ++ β¨βπ£ββ©)β0) = π β§ ((π ++ β¨βπ£ββ©)βπ) β ((π ++ β¨βπ£ββ©)β0)))) |
90 | 81, 89 | mpbird 256 |
. . . . . . 7
β’ ((((πΊ β FriendGraph β§ π β π β§ π β β) β§ (π β (π WWalksN πΊ) β§ ((πβ0) = π β§ (lastSβπ) β π))) β§ π£ β π) β (((π ++ β¨βπ£ββ©)β0) = π β§ ((π ++ β¨βπ£ββ©)β((π + 2) β 2)) β ((π ++ β¨βπ£ββ©)β0))) |
91 | 90 | biantrud 532 |
. . . . . 6
β’ ((((πΊ β FriendGraph β§ π β π β§ π β β) β§ (π β (π WWalksN πΊ) β§ ((πβ0) = π β§ (lastSβπ) β π))) β§ π£ β π) β ((π ++ β¨βπ£ββ©) β ((π + 2) ClWWalksN πΊ) β ((π ++ β¨βπ£ββ©) β ((π + 2) ClWWalksN πΊ) β§ (((π ++ β¨βπ£ββ©)β0) = π β§ ((π ++ β¨βπ£ββ©)β((π + 2) β 2)) β ((π ++ β¨βπ£ββ©)β0))))) |
92 | 61 | anim2i 617 |
. . . . . . . . . . 11
β’ ((π β π β§ π β β) β (π β π β§ (π + 2) β
(β€β₯β2))) |
93 | 92 | 3adant1 1130 |
. . . . . . . . . 10
β’ ((πΊ β FriendGraph β§ π β π β§ π β β) β (π β π β§ (π + 2) β
(β€β₯β2))) |
94 | 93 | ad2antrr 724 |
. . . . . . . . 9
β’ ((((πΊ β FriendGraph β§ π β π β§ π β β) β§ (π β (π WWalksN πΊ) β§ ((πβ0) = π β§ (lastSβπ) β π))) β§ π£ β π) β (π β π β§ (π + 2) β
(β€β₯β2))) |
95 | | numclwwlk.h |
. . . . . . . . . 10
β’ π» = (π£ β π, π β (β€β₯β2)
β¦ {π€ β (π£(ClWWalksNOnβπΊ)π) β£ (π€β(π β 2)) β π£}) |
96 | 95 | numclwwlkovh 29317 |
. . . . . . . . 9
β’ ((π β π β§ (π + 2) β
(β€β₯β2)) β (ππ»(π + 2)) = {π€ β ((π + 2) ClWWalksN πΊ) β£ ((π€β0) = π β§ (π€β((π + 2) β 2)) β (π€β0))}) |
97 | 94, 96 | syl 17 |
. . . . . . . 8
β’ ((((πΊ β FriendGraph β§ π β π β§ π β β) β§ (π β (π WWalksN πΊ) β§ ((πβ0) = π β§ (lastSβπ) β π))) β§ π£ β π) β (ππ»(π + 2)) = {π€ β ((π + 2) ClWWalksN πΊ) β£ ((π€β0) = π β§ (π€β((π + 2) β 2)) β (π€β0))}) |
98 | 97 | eleq2d 2823 |
. . . . . . 7
β’ ((((πΊ β FriendGraph β§ π β π β§ π β β) β§ (π β (π WWalksN πΊ) β§ ((πβ0) = π β§ (lastSβπ) β π))) β§ π£ β π) β ((π ++ β¨βπ£ββ©) β (ππ»(π + 2)) β (π ++ β¨βπ£ββ©) β {π€ β ((π + 2) ClWWalksN πΊ) β£ ((π€β0) = π β§ (π€β((π + 2) β 2)) β (π€β0))})) |
99 | | fveq1 6841 |
. . . . . . . . . 10
β’ (π€ = (π ++ β¨βπ£ββ©) β (π€β0) = ((π ++ β¨βπ£ββ©)β0)) |
100 | 99 | eqeq1d 2738 |
. . . . . . . . 9
β’ (π€ = (π ++ β¨βπ£ββ©) β ((π€β0) = π β ((π ++ β¨βπ£ββ©)β0) = π)) |
101 | | fveq1 6841 |
. . . . . . . . . 10
β’ (π€ = (π ++ β¨βπ£ββ©) β (π€β((π + 2) β 2)) = ((π ++ β¨βπ£ββ©)β((π + 2) β 2))) |
102 | 101, 99 | neeq12d 3005 |
. . . . . . . . 9
β’ (π€ = (π ++ β¨βπ£ββ©) β ((π€β((π + 2) β 2)) β (π€β0) β ((π ++ β¨βπ£ββ©)β((π + 2) β 2)) β ((π ++ β¨βπ£ββ©)β0))) |
103 | 100, 102 | anbi12d 631 |
. . . . . . . 8
β’ (π€ = (π ++ β¨βπ£ββ©) β (((π€β0) = π β§ (π€β((π + 2) β 2)) β (π€β0)) β (((π ++ β¨βπ£ββ©)β0) = π β§ ((π ++ β¨βπ£ββ©)β((π + 2) β 2)) β ((π ++ β¨βπ£ββ©)β0)))) |
104 | 103 | elrab 3645 |
. . . . . . 7
β’ ((π ++ β¨βπ£ββ©) β {π€ β ((π + 2) ClWWalksN πΊ) β£ ((π€β0) = π β§ (π€β((π + 2) β 2)) β (π€β0))} β ((π ++ β¨βπ£ββ©) β ((π + 2) ClWWalksN πΊ) β§ (((π ++ β¨βπ£ββ©)β0) = π β§ ((π ++ β¨βπ£ββ©)β((π + 2) β 2)) β ((π ++ β¨βπ£ββ©)β0)))) |
105 | 98, 104 | bitr2di 287 |
. . . . . 6
β’ ((((πΊ β FriendGraph β§ π β π β§ π β β) β§ (π β (π WWalksN πΊ) β§ ((πβ0) = π β§ (lastSβπ) β π))) β§ π£ β π) β (((π ++ β¨βπ£ββ©) β ((π + 2) ClWWalksN πΊ) β§ (((π ++ β¨βπ£ββ©)β0) = π β§ ((π ++ β¨βπ£ββ©)β((π + 2) β 2)) β ((π ++ β¨βπ£ββ©)β0))) β (π ++ β¨βπ£ββ©) β (ππ»(π + 2)))) |
106 | 67, 91, 105 | 3bitrd 304 |
. . . . 5
β’ ((((πΊ β FriendGraph β§ π β π β§ π β β) β§ (π β (π WWalksN πΊ) β§ ((πβ0) = π β§ (lastSβπ) β π))) β§ π£ β π) β (({(lastSβπ), π£} β (EdgβπΊ) β§ {π£, (πβ0)} β (EdgβπΊ)) β (π ++ β¨βπ£ββ©) β (ππ»(π + 2)))) |
107 | 106 | reubidva 3369 |
. . . 4
β’ (((πΊ β FriendGraph β§ π β π β§ π β β) β§ (π β (π WWalksN πΊ) β§ ((πβ0) = π β§ (lastSβπ) β π))) β (β!π£ β π ({(lastSβπ), π£} β (EdgβπΊ) β§ {π£, (πβ0)} β (EdgβπΊ)) β β!π£ β π (π ++ β¨βπ£ββ©) β (ππ»(π + 2)))) |
108 | 42, 107 | mpbid 231 |
. . 3
β’ (((πΊ β FriendGraph β§ π β π β§ π β β) β§ (π β (π WWalksN πΊ) β§ ((πβ0) = π β§ (lastSβπ) β π))) β β!π£ β π (π ++ β¨βπ£ββ©) β (ππ»(π + 2))) |
109 | 108 | ex 413 |
. 2
β’ ((πΊ β FriendGraph β§ π β π β§ π β β) β ((π β (π WWalksN πΊ) β§ ((πβ0) = π β§ (lastSβπ) β π)) β β!π£ β π (π ++ β¨βπ£ββ©) β (ππ»(π + 2)))) |
110 | 12, 109 | sylbid 239 |
1
β’ ((πΊ β FriendGraph β§ π β π β§ π β β) β (π β (πππ) β β!π£ β π (π ++ β¨βπ£ββ©) β (ππ»(π + 2)))) |