Step | Hyp | Ref
| Expression |
1 | | eqid 2736 |
. . . 4
β’
(VtxβπΊ) =
(VtxβπΊ) |
2 | 1 | wwlknbp 28787 |
. . 3
β’ (π β (π WWalksN πΊ) β (πΊ β V β§ π β β0 β§ π β Word (VtxβπΊ))) |
3 | | iswwlksn 28783 |
. . . . . 6
β’ (π β β0
β (π β (π WWalksN πΊ) β (π β (WWalksβπΊ) β§ (β―βπ) = (π + 1)))) |
4 | 3 | adantr 481 |
. . . . 5
β’ ((π β β0
β§ π β Word
(VtxβπΊ)) β
(π β (π WWalksN πΊ) β (π β (WWalksβπΊ) β§ (β―βπ) = (π + 1)))) |
5 | | lencl 14421 |
. . . . . . . . . . . . . 14
β’ (π β Word (VtxβπΊ) β (β―βπ) β
β0) |
6 | 5 | nn0cnd 12475 |
. . . . . . . . . . . . 13
β’ (π β Word (VtxβπΊ) β (β―βπ) β
β) |
7 | 6 | adantl 482 |
. . . . . . . . . . . 12
β’ ((π β β0
β§ π β Word
(VtxβπΊ)) β
(β―βπ) β
β) |
8 | | 1cnd 11150 |
. . . . . . . . . . . 12
β’ ((π β β0
β§ π β Word
(VtxβπΊ)) β 1
β β) |
9 | | nn0cn 12423 |
. . . . . . . . . . . . 13
β’ (π β β0
β π β
β) |
10 | 9 | adantr 481 |
. . . . . . . . . . . 12
β’ ((π β β0
β§ π β Word
(VtxβπΊ)) β π β
β) |
11 | 7, 8, 10 | subadd2d 11531 |
. . . . . . . . . . 11
β’ ((π β β0
β§ π β Word
(VtxβπΊ)) β
(((β―βπ) β
1) = π β (π + 1) = (β―βπ))) |
12 | | eqcom 2743 |
. . . . . . . . . . 11
β’ ((π + 1) = (β―βπ) β (β―βπ) = (π + 1)) |
13 | 11, 12 | bitr2di 287 |
. . . . . . . . . 10
β’ ((π β β0
β§ π β Word
(VtxβπΊ)) β
((β―βπ) = (π + 1) β
((β―βπ) β
1) = π)) |
14 | 13 | biimpcd 248 |
. . . . . . . . 9
β’
((β―βπ) =
(π + 1) β ((π β β0
β§ π β Word
(VtxβπΊ)) β
((β―βπ) β
1) = π)) |
15 | 14 | adantl 482 |
. . . . . . . 8
β’ ((π β (WWalksβπΊ) β§ (β―βπ) = (π + 1)) β ((π β β0 β§ π β Word (VtxβπΊ)) β ((β―βπ) β 1) = π)) |
16 | 15 | impcom 408 |
. . . . . . 7
β’ (((π β β0
β§ π β Word
(VtxβπΊ)) β§ (π β (WWalksβπΊ) β§ (β―βπ) = (π + 1))) β ((β―βπ) β 1) = π) |
17 | | wlklnwwlkln2lem.1 |
. . . . . . . . . . . . . 14
β’ (π β (π β (WWalksβπΊ) β βπ π(WalksβπΊ)π)) |
18 | 17 | com12 32 |
. . . . . . . . . . . . 13
β’ (π β (WWalksβπΊ) β (π β βπ π(WalksβπΊ)π)) |
19 | 18 | adantr 481 |
. . . . . . . . . . . 12
β’ ((π β (WWalksβπΊ) β§ (β―βπ) = (π + 1)) β (π β βπ π(WalksβπΊ)π)) |
20 | 19 | adantl 482 |
. . . . . . . . . . 11
β’ (((π β β0
β§ π β Word
(VtxβπΊ)) β§ (π β (WWalksβπΊ) β§ (β―βπ) = (π + 1))) β (π β βπ π(WalksβπΊ)π)) |
21 | 20 | imp 407 |
. . . . . . . . . 10
β’ ((((π β β0
β§ π β Word
(VtxβπΊ)) β§ (π β (WWalksβπΊ) β§ (β―βπ) = (π + 1))) β§ π) β βπ π(WalksβπΊ)π) |
22 | | simpr 485 |
. . . . . . . . . . . . 13
β’
(((((π β
β0 β§ π
β Word (VtxβπΊ))
β§ (π β
(WWalksβπΊ) β§
(β―βπ) = (π + 1))) β§ π) β§ π(WalksβπΊ)π) β π(WalksβπΊ)π) |
23 | | wlklenvm1 28570 |
. . . . . . . . . . . . 13
β’ (π(WalksβπΊ)π β (β―βπ) = ((β―βπ) β 1)) |
24 | 22, 23 | jccir 522 |
. . . . . . . . . . . 12
β’
(((((π β
β0 β§ π
β Word (VtxβπΊ))
β§ (π β
(WWalksβπΊ) β§
(β―βπ) = (π + 1))) β§ π) β§ π(WalksβπΊ)π) β (π(WalksβπΊ)π β§ (β―βπ) = ((β―βπ) β 1))) |
25 | 24 | ex 413 |
. . . . . . . . . . 11
β’ ((((π β β0
β§ π β Word
(VtxβπΊ)) β§ (π β (WWalksβπΊ) β§ (β―βπ) = (π + 1))) β§ π) β (π(WalksβπΊ)π β (π(WalksβπΊ)π β§ (β―βπ) = ((β―βπ) β 1)))) |
26 | 25 | eximdv 1920 |
. . . . . . . . . 10
β’ ((((π β β0
β§ π β Word
(VtxβπΊ)) β§ (π β (WWalksβπΊ) β§ (β―βπ) = (π + 1))) β§ π) β (βπ π(WalksβπΊ)π β βπ(π(WalksβπΊ)π β§ (β―βπ) = ((β―βπ) β 1)))) |
27 | 21, 26 | mpd 15 |
. . . . . . . . 9
β’ ((((π β β0
β§ π β Word
(VtxβπΊ)) β§ (π β (WWalksβπΊ) β§ (β―βπ) = (π + 1))) β§ π) β βπ(π(WalksβπΊ)π β§ (β―βπ) = ((β―βπ) β 1))) |
28 | | eqeq2 2748 |
. . . . . . . . . . 11
β’
(((β―βπ)
β 1) = π β
((β―βπ) =
((β―βπ) β
1) β (β―βπ)
= π)) |
29 | 28 | anbi2d 629 |
. . . . . . . . . 10
β’
(((β―βπ)
β 1) = π β
((π(WalksβπΊ)π β§ (β―βπ) = ((β―βπ) β 1)) β (π(WalksβπΊ)π β§ (β―βπ) = π))) |
30 | 29 | exbidv 1924 |
. . . . . . . . 9
β’
(((β―βπ)
β 1) = π β
(βπ(π(WalksβπΊ)π β§ (β―βπ) = ((β―βπ) β 1)) β βπ(π(WalksβπΊ)π β§ (β―βπ) = π))) |
31 | 27, 30 | imbitrid 243 |
. . . . . . . 8
β’
(((β―βπ)
β 1) = π β
((((π β
β0 β§ π
β Word (VtxβπΊ))
β§ (π β
(WWalksβπΊ) β§
(β―βπ) = (π + 1))) β§ π) β βπ(π(WalksβπΊ)π β§ (β―βπ) = π))) |
32 | 31 | expd 416 |
. . . . . . 7
β’
(((β―βπ)
β 1) = π β
(((π β
β0 β§ π
β Word (VtxβπΊ))
β§ (π β
(WWalksβπΊ) β§
(β―βπ) = (π + 1))) β (π β βπ(π(WalksβπΊ)π β§ (β―βπ) = π)))) |
33 | 16, 32 | mpcom 38 |
. . . . . 6
β’ (((π β β0
β§ π β Word
(VtxβπΊ)) β§ (π β (WWalksβπΊ) β§ (β―βπ) = (π + 1))) β (π β βπ(π(WalksβπΊ)π β§ (β―βπ) = π))) |
34 | 33 | ex 413 |
. . . . 5
β’ ((π β β0
β§ π β Word
(VtxβπΊ)) β
((π β
(WWalksβπΊ) β§
(β―βπ) = (π + 1)) β (π β βπ(π(WalksβπΊ)π β§ (β―βπ) = π)))) |
35 | 4, 34 | sylbid 239 |
. . . 4
β’ ((π β β0
β§ π β Word
(VtxβπΊ)) β
(π β (π WWalksN πΊ) β (π β βπ(π(WalksβπΊ)π β§ (β―βπ) = π)))) |
36 | 35 | 3adant1 1130 |
. . 3
β’ ((πΊ β V β§ π β β0
β§ π β Word
(VtxβπΊ)) β
(π β (π WWalksN πΊ) β (π β βπ(π(WalksβπΊ)π β§ (β―βπ) = π)))) |
37 | 2, 36 | mpcom 38 |
. 2
β’ (π β (π WWalksN πΊ) β (π β βπ(π(WalksβπΊ)π β§ (β―βπ) = π))) |
38 | 37 | com12 32 |
1
β’ (π β (π β (π WWalksN πΊ) β βπ(π(WalksβπΊ)π β§ (β―βπ) = π))) |