Step | Hyp | Ref
| Expression |
1 | | nnnn0 12479 |
. . . 4
β’ (π β β β π β
β0) |
2 | | wwlksn 29091 |
. . . 4
β’ (π β β0
β (π WWalksN πΊ) = {π€ β (WWalksβπΊ) β£ (β―βπ€) = (π + 1)}) |
3 | 1, 2 | syl 17 |
. . 3
β’ (π β β β (π WWalksN πΊ) = {π€ β (WWalksβπΊ) β£ (β―βπ€) = (π + 1)}) |
4 | 3 | adantl 483 |
. 2
β’
(((EdgβπΊ) =
β
β§ π β
β) β (π WWalksN
πΊ) = {π€ β (WWalksβπΊ) β£ (β―βπ€) = (π + 1)}) |
5 | | eqid 2733 |
. . . . . . . 8
β’
(VtxβπΊ) =
(VtxβπΊ) |
6 | | eqid 2733 |
. . . . . . . 8
β’
(EdgβπΊ) =
(EdgβπΊ) |
7 | 5, 6 | iswwlks 29090 |
. . . . . . 7
β’ (π€ β (WWalksβπΊ) β (π€ β β
β§ π€ β Word (VtxβπΊ) β§ βπ β (0..^((β―βπ€) β 1)){(π€βπ), (π€β(π + 1))} β (EdgβπΊ))) |
8 | | nncn 12220 |
. . . . . . . . . . . . . . . . 17
β’ (π β β β π β
β) |
9 | | pncan1 11638 |
. . . . . . . . . . . . . . . . 17
β’ (π β β β ((π + 1) β 1) = π) |
10 | 8, 9 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (π β β β ((π + 1) β 1) = π) |
11 | | id 22 |
. . . . . . . . . . . . . . . 16
β’ (π β β β π β
β) |
12 | 10, 11 | eqeltrd 2834 |
. . . . . . . . . . . . . . 15
β’ (π β β β ((π + 1) β 1) β
β) |
13 | 12 | adantl 483 |
. . . . . . . . . . . . . 14
β’
(((EdgβπΊ) =
β
β§ π β
β) β ((π + 1)
β 1) β β) |
14 | 13 | adantl 483 |
. . . . . . . . . . . . 13
β’
(((β―βπ€)
= (π + 1) β§
((EdgβπΊ) = β
β§ π β β))
β ((π + 1) β 1)
β β) |
15 | | oveq1 7416 |
. . . . . . . . . . . . . . 15
β’
((β―βπ€) =
(π + 1) β
((β―βπ€) β
1) = ((π + 1) β
1)) |
16 | 15 | eleq1d 2819 |
. . . . . . . . . . . . . 14
β’
((β―βπ€) =
(π + 1) β
(((β―βπ€) β
1) β β β ((π + 1) β 1) β
β)) |
17 | 16 | adantr 482 |
. . . . . . . . . . . . 13
β’
(((β―βπ€)
= (π + 1) β§
((EdgβπΊ) = β
β§ π β β))
β (((β―βπ€)
β 1) β β β ((π + 1) β 1) β
β)) |
18 | 14, 17 | mpbird 257 |
. . . . . . . . . . . 12
β’
(((β―βπ€)
= (π + 1) β§
((EdgβπΊ) = β
β§ π β β))
β ((β―βπ€)
β 1) β β) |
19 | | lbfzo0 13672 |
. . . . . . . . . . . 12
β’ (0 β
(0..^((β―βπ€)
β 1)) β ((β―βπ€) β 1) β β) |
20 | 18, 19 | sylibr 233 |
. . . . . . . . . . 11
β’
(((β―βπ€)
= (π + 1) β§
((EdgβπΊ) = β
β§ π β β))
β 0 β (0..^((β―βπ€) β 1))) |
21 | | fveq2 6892 |
. . . . . . . . . . . . . 14
β’ (π = 0 β (π€βπ) = (π€β0)) |
22 | | fv0p1e1 12335 |
. . . . . . . . . . . . . 14
β’ (π = 0 β (π€β(π + 1)) = (π€β1)) |
23 | 21, 22 | preq12d 4746 |
. . . . . . . . . . . . 13
β’ (π = 0 β {(π€βπ), (π€β(π + 1))} = {(π€β0), (π€β1)}) |
24 | 23 | eleq1d 2819 |
. . . . . . . . . . . 12
β’ (π = 0 β ({(π€βπ), (π€β(π + 1))} β (EdgβπΊ) β {(π€β0), (π€β1)} β (EdgβπΊ))) |
25 | 24 | adantl 483 |
. . . . . . . . . . 11
β’
((((β―βπ€)
= (π + 1) β§
((EdgβπΊ) = β
β§ π β β))
β§ π = 0) β
({(π€βπ), (π€β(π + 1))} β (EdgβπΊ) β {(π€β0), (π€β1)} β (EdgβπΊ))) |
26 | 20, 25 | rspcdv 3605 |
. . . . . . . . . 10
β’
(((β―βπ€)
= (π + 1) β§
((EdgβπΊ) = β
β§ π β β))
β (βπ β
(0..^((β―βπ€)
β 1)){(π€βπ), (π€β(π + 1))} β (EdgβπΊ) β {(π€β0), (π€β1)} β (EdgβπΊ))) |
27 | | eleq2 2823 |
. . . . . . . . . . . . 13
β’
((EdgβπΊ) =
β
β ({(π€β0), (π€β1)} β (EdgβπΊ) β {(π€β0), (π€β1)} β β
)) |
28 | | noel 4331 |
. . . . . . . . . . . . . 14
β’ Β¬
{(π€β0), (π€β1)} β
β
|
29 | 28 | pm2.21i 119 |
. . . . . . . . . . . . 13
β’ ({(π€β0), (π€β1)} β β
β Β¬
(β―βπ€) = (π + 1)) |
30 | 27, 29 | syl6bi 253 |
. . . . . . . . . . . 12
β’
((EdgβπΊ) =
β
β ({(π€β0), (π€β1)} β (EdgβπΊ) β Β¬
(β―βπ€) = (π + 1))) |
31 | 30 | adantr 482 |
. . . . . . . . . . 11
β’
(((EdgβπΊ) =
β
β§ π β
β) β ({(π€β0), (π€β1)} β (EdgβπΊ) β Β¬
(β―βπ€) = (π + 1))) |
32 | 31 | adantl 483 |
. . . . . . . . . 10
β’
(((β―βπ€)
= (π + 1) β§
((EdgβπΊ) = β
β§ π β β))
β ({(π€β0),
(π€β1)} β
(EdgβπΊ) β Β¬
(β―βπ€) = (π + 1))) |
33 | 26, 32 | syldc 48 |
. . . . . . . . 9
β’
(βπ β
(0..^((β―βπ€)
β 1)){(π€βπ), (π€β(π + 1))} β (EdgβπΊ) β (((β―βπ€) = (π + 1) β§ ((EdgβπΊ) = β
β§ π β β)) β Β¬
(β―βπ€) = (π + 1))) |
34 | 33 | 3ad2ant3 1136 |
. . . . . . . 8
β’ ((π€ β β
β§ π€ β Word (VtxβπΊ) β§ βπ β
(0..^((β―βπ€)
β 1)){(π€βπ), (π€β(π + 1))} β (EdgβπΊ)) β (((β―βπ€) = (π + 1) β§ ((EdgβπΊ) = β
β§ π β β)) β Β¬
(β―βπ€) = (π + 1))) |
35 | 34 | com12 32 |
. . . . . . 7
β’
(((β―βπ€)
= (π + 1) β§
((EdgβπΊ) = β
β§ π β β))
β ((π€ β β
β§ π€ β Word
(VtxβπΊ) β§
βπ β
(0..^((β―βπ€)
β 1)){(π€βπ), (π€β(π + 1))} β (EdgβπΊ)) β Β¬ (β―βπ€) = (π + 1))) |
36 | 7, 35 | biimtrid 241 |
. . . . . 6
β’
(((β―βπ€)
= (π + 1) β§
((EdgβπΊ) = β
β§ π β β))
β (π€ β
(WWalksβπΊ) β
Β¬ (β―βπ€) =
(π + 1))) |
37 | 36 | expimpd 455 |
. . . . 5
β’
((β―βπ€) =
(π + 1) β
((((EdgβπΊ) = β
β§ π β β)
β§ π€ β
(WWalksβπΊ)) β
Β¬ (β―βπ€) =
(π + 1))) |
38 | | ax-1 6 |
. . . . 5
β’ (Β¬
(β―βπ€) = (π + 1) β ((((EdgβπΊ) = β
β§ π β β) β§ π€ β (WWalksβπΊ)) β Β¬
(β―βπ€) = (π + 1))) |
39 | 37, 38 | pm2.61i 182 |
. . . 4
β’
((((EdgβπΊ) =
β
β§ π β
β) β§ π€ β
(WWalksβπΊ)) β
Β¬ (β―βπ€) =
(π + 1)) |
40 | 39 | ralrimiva 3147 |
. . 3
β’
(((EdgβπΊ) =
β
β§ π β
β) β βπ€
β (WWalksβπΊ)
Β¬ (β―βπ€) =
(π + 1)) |
41 | | rabeq0 4385 |
. . 3
β’ ({π€ β (WWalksβπΊ) β£ (β―βπ€) = (π + 1)} = β
β βπ€ β (WWalksβπΊ) Β¬ (β―βπ€) = (π + 1)) |
42 | 40, 41 | sylibr 233 |
. 2
β’
(((EdgβπΊ) =
β
β§ π β
β) β {π€ β
(WWalksβπΊ) β£
(β―βπ€) = (π + 1)} =
β
) |
43 | 4, 42 | eqtrd 2773 |
1
β’
(((EdgβπΊ) =
β
β§ π β
β) β (π WWalksN
πΊ) =
β
) |