Proof of Theorem pthdivtx
Step | Hyp | Ref
| Expression |
1 | | ispth 26619 |
. . 3
Paths Trails ..^ ..^ |
2 | | trliswlk 26594 |
. . . . 5
Trails Walks |
3 | | eqid 2622 |
. . . . . 6
Vtx Vtx |
4 | 3 | wlkp 26512 |
. . . . 5
Walks Vtx |
5 | | elfz0lmr 12583 |
. . . . . . . . 9
..^ |
6 | | elfzo1 12517 |
. . . . . . . . . . . . . . . . . . . . 21
..^ |
7 | | nnnn0 11299 |
. . . . . . . . . . . . . . . . . . . . . 22
|
8 | 7 | 3ad2ant2 1083 |
. . . . . . . . . . . . . . . . . . . . 21
|
9 | 6, 8 | sylbi 207 |
. . . . . . . . . . . . . . . . . . . 20
..^
|
10 | 9 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
..^ |
11 | | fvinim0ffz 12587 |
. . . . . . . . . . . . . . . . . . 19
Vtx ..^ ..^ ..^ |
12 | 10, 11 | sylan2 491 |
. . . . . . . . . . . . . . . . . 18
Vtx
..^ ..^
..^ ..^ |
13 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
14 | 13 | eqeq2d 2632 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
15 | 14 | ad2antrl 764 |
. . . . . . . . . . . . . . . . . . . . . 22
Vtx
..^ |
16 | | ffun 6048 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
Vtx |
17 | 16 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
Vtx ..^
|
18 | | fdm 6051 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
Vtx |
19 | | fzo0ss1 12498 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
..^ ..^ |
20 | | fzossfz 12488 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
..^ |
21 | 19, 20 | sstri 3612 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
..^ |
22 | 21 | sseli 3599 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
..^
|
23 | | eleq2 2690 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
24 | 22, 23 | syl5ibr 236 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
..^ |
25 | 18, 24 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
Vtx ..^ |
26 | 25 | imp 445 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
Vtx ..^ |
27 | 17, 26 | jca 554 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
Vtx ..^
|
28 | 27 | adantrl 752 |
. . . . . . . . . . . . . . . . . . . . . . . 24
Vtx
..^
|
29 | | simprr 796 |
. . . . . . . . . . . . . . . . . . . . . . . 24
Vtx
..^ ..^ |
30 | | funfvima 6492 |
. . . . . . . . . . . . . . . . . . . . . . . 24
..^ ..^ |
31 | 28, 29, 30 | sylc 65 |
. . . . . . . . . . . . . . . . . . . . . . 23
Vtx
..^ ..^ |
32 | | eleq1 2689 |
. . . . . . . . . . . . . . . . . . . . . . 23
..^
..^ |
33 | 31, 32 | syl5ibcom 235 |
. . . . . . . . . . . . . . . . . . . . . 22
Vtx
..^
..^ |
34 | 15, 33 | sylbid 230 |
. . . . . . . . . . . . . . . . . . . . 21
Vtx
..^
..^ |
35 | | nnel 2906 |
. . . . . . . . . . . . . . . . . . . . 21
..^ ..^ |
36 | 34, 35 | syl6ibr 242 |
. . . . . . . . . . . . . . . . . . . 20
Vtx
..^
..^ |
37 | 36 | necon2ad 2809 |
. . . . . . . . . . . . . . . . . . 19
Vtx
..^ ..^ |
38 | 37 | adantrd 484 |
. . . . . . . . . . . . . . . . . 18
Vtx
..^ ..^ ..^ |
39 | 12, 38 | sylbid 230 |
. . . . . . . . . . . . . . . . 17
Vtx
..^ ..^
|
40 | 39 | ex 450 |
. . . . . . . . . . . . . . . 16
Vtx ..^ ..^
|
41 | 40 | com23 86 |
. . . . . . . . . . . . . . 15
Vtx ..^ ..^ |
42 | 41 | a1d 25 |
. . . . . . . . . . . . . 14
Vtx ..^ ..^
..^ |
43 | 42 | 3imp 1256 |
. . . . . . . . . . . . 13
Vtx ..^ ..^
..^ |
44 | 43 | com12 32 |
. . . . . . . . . . . 12
..^ Vtx ..^ ..^ |
45 | 44 | a1d 25 |
. . . . . . . . . . 11
..^ Vtx ..^ ..^ |
46 | 45 | ex 450 |
. . . . . . . . . 10
..^ Vtx ..^ ..^ |
47 | | fvres 6207 |
. . . . . . . . . . . . . . . . . . . 20
..^
..^ |
48 | 47 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
..^ ..^ ..^ |
49 | 48 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
Vtx ..^ ..^
..^ ..^
..^ |
50 | 49 | eqcomd 2628 |
. . . . . . . . . . . . . . . . 17
Vtx ..^ ..^
..^ ..^
..^ |
51 | | fvres 6207 |
. . . . . . . . . . . . . . . . . . 19
..^
..^ |
52 | 51 | ad2antrl 764 |
. . . . . . . . . . . . . . . . . 18
Vtx ..^ ..^
..^ ..^
..^ |
53 | 52 | eqcomd 2628 |
. . . . . . . . . . . . . . . . 17
Vtx ..^ ..^
..^ ..^
..^ |
54 | 50, 53 | eqeq12d 2637 |
. . . . . . . . . . . . . . . 16
Vtx ..^ ..^
..^ ..^
..^
..^ |
55 | | fssres 6070 |
. . . . . . . . . . . . . . . . . . . 20
Vtx ..^ ..^..^Vtx |
56 | 21, 55 | mpan2 707 |
. . . . . . . . . . . . . . . . . . 19
Vtx ..^..^Vtx |
57 | | df-f1 5893 |
. . . . . . . . . . . . . . . . . . . 20
..^..^Vtx
..^..^Vtx ..^ |
58 | 57 | biimpri 218 |
. . . . . . . . . . . . . . . . . . 19
..^..^Vtx ..^ ..^..^Vtx |
59 | 56, 58 | sylan 488 |
. . . . . . . . . . . . . . . . . 18
Vtx ..^ ..^..^Vtx |
60 | 59 | 3adant3 1081 |
. . . . . . . . . . . . . . . . 17
Vtx ..^ ..^
..^..^Vtx |
61 | | simpr 477 |
. . . . . . . . . . . . . . . . . 18
Vtx ..^ ..^
..^ ..^
..^
..^ |
62 | 61 | ancomd 467 |
. . . . . . . . . . . . . . . . 17
Vtx ..^ ..^
..^ ..^
..^
..^ |
63 | | f1veqaeq 6514 |
. . . . . . . . . . . . . . . . 17
..^..^Vtx
..^ ..^
..^ ..^ |
64 | 60, 62, 63 | syl2an2r 876 |
. . . . . . . . . . . . . . . 16
Vtx ..^ ..^
..^ ..^
..^ ..^ |
65 | 54, 64 | sylbid 230 |
. . . . . . . . . . . . . . 15
Vtx ..^ ..^
..^ ..^
|
66 | 65 | ancoms 469 |
. . . . . . . . . . . . . 14
..^ ..^ Vtx ..^ ..^ |
67 | 66 | necon3d 2815 |
. . . . . . . . . . . . 13
..^ ..^ Vtx ..^ ..^ |
68 | 67 | ex 450 |
. . . . . . . . . . . 12
..^ ..^ Vtx ..^ ..^
|
69 | 68 | com23 86 |
. . . . . . . . . . 11
..^ ..^
Vtx ..^ ..^
|
70 | 69 | ex 450 |
. . . . . . . . . 10
..^
..^ Vtx ..^ ..^ |
71 | 9 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
..^ |
72 | 71, 11 | sylan2 491 |
. . . . . . . . . . . . . . . . . 18
Vtx
..^ ..^
..^ ..^ |
73 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
74 | 73 | eqeq2d 2632 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
75 | 74 | ad2antrl 764 |
. . . . . . . . . . . . . . . . . . . . . 22
Vtx
..^ |
76 | 27 | adantrl 752 |
. . . . . . . . . . . . . . . . . . . . . . . 24
Vtx
..^
|
77 | | simprr 796 |
. . . . . . . . . . . . . . . . . . . . . . . 24
Vtx
..^ ..^ |
78 | 76, 77, 30 | sylc 65 |
. . . . . . . . . . . . . . . . . . . . . . 23
Vtx
..^ ..^ |
79 | | eleq1 2689 |
. . . . . . . . . . . . . . . . . . . . . . 23
..^
..^ |
80 | 78, 79 | syl5ibcom 235 |
. . . . . . . . . . . . . . . . . . . . . 22
Vtx
..^ ..^ |
81 | 75, 80 | sylbid 230 |
. . . . . . . . . . . . . . . . . . . . 21
Vtx
..^
..^ |
82 | | nnel 2906 |
. . . . . . . . . . . . . . . . . . . . 21
..^ ..^ |
83 | 81, 82 | syl6ibr 242 |
. . . . . . . . . . . . . . . . . . . 20
Vtx
..^
..^ |
84 | 83 | necon2ad 2809 |
. . . . . . . . . . . . . . . . . . 19
Vtx
..^ ..^ |
85 | 84 | adantld 483 |
. . . . . . . . . . . . . . . . . 18
Vtx
..^ ..^ ..^ |
86 | 72, 85 | sylbid 230 |
. . . . . . . . . . . . . . . . 17
Vtx
..^ ..^
|
87 | 86 | ex 450 |
. . . . . . . . . . . . . . . 16
Vtx
..^ ..^
|
88 | 87 | com23 86 |
. . . . . . . . . . . . . . 15
Vtx ..^
..^ |
89 | 88 | a1d 25 |
. . . . . . . . . . . . . 14
Vtx ..^ ..^
..^ |
90 | 89 | 3imp 1256 |
. . . . . . . . . . . . 13
Vtx ..^ ..^
..^ |
91 | 90 | com12 32 |
. . . . . . . . . . . 12
..^ Vtx ..^ ..^
|
92 | 91 | a1d 25 |
. . . . . . . . . . 11
..^
Vtx ..^ ..^
|
93 | 92 | ex 450 |
. . . . . . . . . 10
..^ Vtx ..^ ..^ |
94 | 46, 70, 93 | 3jaoi 1391 |
. . . . . . . . 9
..^ ..^ Vtx ..^ ..^ |
95 | 5, 94 | syl 17 |
. . . . . . . 8
..^ Vtx ..^ ..^ |
96 | 95 | 3imp21 1277 |
. . . . . . 7
..^
Vtx ..^ ..^
|
97 | 96 | com12 32 |
. . . . . 6
Vtx ..^ ..^
..^
|
98 | 97 | 3exp 1264 |
. . . . 5
Vtx ..^ ..^
..^
|
99 | 2, 4, 98 | 3syl 18 |
. . . 4
Trails
..^ ..^
..^
|
100 | 99 | 3imp 1256 |
. . 3
Trails ..^ ..^
..^
|
101 | 1, 100 | sylbi 207 |
. 2
Paths ..^
|
102 | 101 | imp 445 |
1
Paths ..^ |