Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  numclwwlkovf2ex Structured version   Visualization version   Unicode version

Theorem numclwwlkovf2ex 25814
 Description: Extending a closed walk starting at a fixed vertex by an additional edge (forth and back). (Contributed by AV, 22-Sep-2018.) (Proof shortened by AV, 23-Oct-2018.)
Hypotheses
Ref Expression
numclwwlk.c ClWWalksN
numclwwlk.f
Assertion
Ref Expression
numclwwlkovf2ex USGrph Neighbors ++ ++
Distinct variable groups:   ,   ,   ,   ,   ,   ,,,   ,   ,,,   ,   ,   ,   ,   ,   ,
Allowed substitution hints:   (,)   (,)   ()   (,)

Proof of Theorem numclwwlkovf2ex
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 simp1 1008 . . . . . . 7 USGrph USGrph
2 uzuzle23 11199 . . . . . . . . 9
3 uznn0sub 11190 . . . . . . . . 9
42, 3syl 17 . . . . . . . 8
543ad2ant3 1031 . . . . . . 7 USGrph
6 simp2 1009 . . . . . . 7 USGrph
7 numclwwlk.c . . . . . . . 8 ClWWalksN
8 numclwwlk.f . . . . . . . 8
97, 8numclwwlkovfel2 25811 . . . . . . 7 USGrph Word ..^ lastS
101, 5, 6, 9syl3anc 1268 . . . . . 6 USGrph Word ..^ lastS
11 ccatws1cl 12753 . . . . . . . . . . . . . . . . 17 Word ++ Word
1211ex 436 . . . . . . . . . . . . . . . 16 Word ++ Word
13123ad2ant1 1029 . . . . . . . . . . . . . . 15 Word ..^ lastS ++ Word
14133ad2ant1 1029 . . . . . . . . . . . . . 14 Word ..^ lastS ++ Word
1514com12 32 . . . . . . . . . . . . 13 Word ..^ lastS ++ Word
16153ad2ant2 1030 . . . . . . . . . . . 12 USGrph Word ..^ lastS ++ Word
1716imp 431 . . . . . . . . . . 11 USGrph Word ..^ lastS ++ Word
1817adantr 467 . . . . . . . . . 10 USGrph Word ..^ lastS Neighbors ++ Word
19 nbgraisvtx 25159 . . . . . . . . . . . . . 14 USGrph Neighbors
20 s1cl 12741 . . . . . . . . . . . . . 14 Word
2119, 20syl6 34 . . . . . . . . . . . . 13 USGrph Neighbors Word
22213ad2ant1 1029 . . . . . . . . . . . 12 USGrph Neighbors Word
2322adantr 467 . . . . . . . . . . 11 USGrph Word ..^ lastS Neighbors Word
2423imp 431 . . . . . . . . . 10 USGrph Word ..^ lastS Neighbors Word
25 ccatcl 12720 . . . . . . . . . 10 ++ Word Word ++ ++ Word
2618, 24, 25syl2anc 667 . . . . . . . . 9 USGrph Word ..^ lastS Neighbors ++ ++ Word
27 simpl 459 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Word lastS Word
2827ad2antlr 733 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 Neighbors Word lastS Word
2928ad2antrr 732 . . . . . . . . . . . . . . . . . . . . . . . . . 26 Neighbors Word lastS USGrph ..^ Word
30 elfzonn0 11960 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ..^
3130adantl 468 . . . . . . . . . . . . . . . . . . . . . . . . . 26 Neighbors Word lastS USGrph ..^
32 lencl 12687 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 Word
33 elfzo0 11956 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ..^
34 nn0re 10878 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
3534adantr 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
36 nn0re 10878 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
37 peano2rem 9941 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
3836, 37syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
3938adantl 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
4036adantl 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
4135, 39, 403jca 1188 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
4236ltm1d 10539 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
4342adantl 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
44 lttr 9710 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
4544expcomd 440 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
4641, 43, 45sylc 62 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
4746impancom 442 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
48473adant2 1027 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
4933, 48sylbi 199 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ..^
5032, 49syl5com 31 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 Word ..^
5150ad2antrl 734 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Neighbors Word lastS ..^
5251ad2antrr 732 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 Neighbors Word lastS USGrph ..^
5352imp 431 . . . . . . . . . . . . . . . . . . . . . . . . . 26 Neighbors Word lastS USGrph ..^
5429, 31, 533jca 1188 . . . . . . . . . . . . . . . . . . . . . . . . 25 Neighbors Word lastS USGrph ..^ Word
556adantl 468 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 Neighbors Word lastS USGrph
56193ad2ant1 1029 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 USGrph Neighbors
5756com12 32 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 Neighbors USGrph
5857ad2antrr 732 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Neighbors Word lastS USGrph
5958imp 431 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 Neighbors Word lastS USGrph
6055, 59jca 535 . . . . . . . . . . . . . . . . . . . . . . . . . 26 Neighbors Word lastS USGrph
6160adantr 467 . . . . . . . . . . . . . . . . . . . . . . . . 25 Neighbors Word lastS USGrph ..^
62 ccat2s1fvw 12771 . . . . . . . . . . . . . . . . . . . . . . . . . 26 Word ++ ++
6362eqcomd 2457 . . . . . . . . . . . . . . . . . . . . . . . . 25 Word ++ ++
6454, 61, 63syl2anc 667 . . . . . . . . . . . . . . . . . . . . . . . 24 Neighbors Word lastS USGrph ..^ ++ ++
65 simpl 459 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 Word ..^ Word
66 peano2nn0 10910 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
67663ad2ant1 1029 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
6833, 67sylbi 199 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ..^
6968adantl 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 Word ..^
70 1red 9658 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
7135, 70, 40ltaddsubd 10213 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
7271biimprd 227 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
7372impancom 442 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
74733adant2 1027 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
7533, 74sylbi 199 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ..^
7632, 75mpan9 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 Word ..^
7765, 69, 763jca 1188 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 Word ..^ Word
7877ex 436 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 Word ..^ Word
7978ad2antrl 734 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Neighbors Word lastS ..^ Word
8079ad2antrr 732 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 Neighbors Word lastS USGrph ..^ Word
8180imp 431 . . . . . . . . . . . . . . . . . . . . . . . . . 26 Neighbors Word lastS USGrph ..^ Word
82 ccat2s1fvw 12771 . . . . . . . . . . . . . . . . . . . . . . . . . 26 Word ++ ++
8381, 61, 82syl2anc 667 . . . . . . . . . . . . . . . . . . . . . . . . 25 Neighbors Word lastS USGrph ..^ ++ ++
8483eqcomd 2457 . . . . . . . . . . . . . . . . . . . . . . . 24 Neighbors Word lastS USGrph ..^ ++ ++
8564, 84preq12d 4059 . . . . . . . . . . . . . . . . . . . . . . 23 Neighbors Word lastS USGrph ..^ ++ ++ ++ ++
8685eleq1d 2513 . . . . . . . . . . . . . . . . . . . . . 22 Neighbors Word lastS USGrph ..^ ++ ++ ++ ++
8786ralbidva 2824 . . . . . . . . . . . . . . . . . . . . 21 Neighbors Word lastS USGrph ..^ ..^ ++ ++ ++ ++
8887biimpd 211 . . . . . . . . . . . . . . . . . . . 20 Neighbors Word lastS USGrph ..^ ..^ ++ ++ ++ ++
8988exp41 615 . . . . . . . . . . . . . . . . . . 19 Neighbors Word lastS USGrph ..^ ..^ ++ ++ ++ ++
9089com15 96 . . . . . . . . . . . . . . . . . 18 ..^ Word lastS USGrph Neighbors ..^ ++ ++ ++ ++
9190expd 438 . . . . . . . . . . . . . . . . 17 ..^ Word lastS USGrph Neighbors ..^ ++ ++ ++ ++
9291com12 32 . . . . . . . . . . . . . . . 16 Word ..^ lastS USGrph Neighbors ..^ ++ ++ ++ ++
93923imp 1202 . . . . . . . . . . . . . . 15 Word ..^ lastS USGrph Neighbors ..^ ++ ++ ++ ++
94933impib 1206 . . . . . . . . . . . . . 14 Word ..^ lastS USGrph Neighbors ..^ ++ ++ ++ ++
9594impcom 432 . . . . . . . . . . . . 13 USGrph Word ..^ lastS Neighbors ..^ ++ ++ ++ ++
9695imp 431 . . . . . . . . . . . 12 USGrph Word ..^ lastS Neighbors ..^ ++ ++ ++ ++
97 simpll 760 . . . . . . . . . . . . . . . . . . . . . . . . 25 Word Word
98 oveq1 6297 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
9998adantr 467 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
100 eluzelcn 11170 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
101 2cnd 10682 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
102 1cnd 9659 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
103100, 101, 102subsub4d 10017 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
104 2p1e3 10733 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
105104a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
106105oveq2d 6306 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
107 uznn0sub 11190 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
108106, 107eqeltrd 2529 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
109103, 108eqeltrd 2529 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
110109adantl 468 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
11199, 110eqeltrd 2529 . . . . . . . . . . . . . . . . . . . . . . . . . 26
112111adantll 720 . . . . . . . . . . . . . . . . . . . . . . . . 25 Word
11332, 42syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 Word
114113ad2antrr 732 . . . . . . . . . . . . . . . . . . . . . . . . 25 Word
11597, 112, 1143jca 1188 . . . . . . . . . . . . . . . . . . . . . . . 24 Word Word
116115exp31 609 . . . . . . . . . . . . . . . . . . . . . . 23 Word Word
117116a1dd 47 . . . . . . . . . . . . . . . . . . . . . 22 Word Word
1181173ad2ant1 1029 . . . . . . . . . . . . . . . . . . . . 21 Word ..^ lastS Word
1191183imp 1202 . . . . . . . . . . . . . . . . . . . 20 Word ..^ lastS Word
120119com12 32 . . . . . . . . . . . . . . . . . . 19 Word ..^ lastS Word
1211203ad2ant3 1031 . . . . . . . . . . . . . . . . . 18 USGrph Word ..^ lastS Word
122121imp 431 . . . . . . . . . . . . . . . . 17 USGrph Word ..^ lastS Word
123122adantr 467 . . . . . . . . . . . . . . . 16 USGrph Word ..^ lastS Neighbors Word
12419ad2antrl 734 . . . . . . . . . . . . . . . . . . . . . . 23 Word USGrph Neighbors
125 simpr 463 . . . . . . . . . . . . . . . . . . . . . . . 24 USGrph
126125adantl 468 . . . . . . . . . . . . . . . . . . . . . . 23 Word USGrph
127124, 126jctild 546 . . . . . . . . . . . . . . . . . . . . . 22 Word USGrph Neighbors
128127ex 436 . . . . . . . . . . . . . . . . . . . . 21 Word USGrph Neighbors
1291283ad2ant1 1029 . . . . . . . . . . . . . . . . . . . 20 Word ..^ lastS USGrph Neighbors
1301293ad2ant1 1029 . . . . . . . . . . . . . . . . . . 19 Word ..^ lastS USGrph Neighbors
131130com12 32 . . . . . . . . . . . . . . . . . 18 USGrph Word ..^ lastS Neighbors
1321313adant3 1028 . . . . . . . . . . . . . . . . 17 USGrph Word ..^ lastS Neighbors
133132imp31 434 . . . . . . . . . . . . . . . 16 USGrph Word ..^ lastS Neighbors
134 ccat2s1fvw 12771 . . . . . . . . . . . . . . . 16 Word ++ ++
135123, 133, 134syl2anc 667 . . . . . . . . . . . . . . 15 USGrph Word ..^ lastS Neighbors ++ ++
136 nn0cn 10879 . . . . . . . . . . . . . . . . . . . . . 22
137 ax-1cn 9597 . . . . . . . . . . . . . . . . . . . . . 22
138 npcan 9884 . . . . . . . . . . . . . . . . . . . . . 22
139136, 137, 138sylancl 668 . . . . . . . . . . . . . . . . . . . . 21
14032, 139syl 17 . . . . . . . . . . . . . . . . . . . 20 Word
1411403ad2ant1 1029 . . . . . . . . . . . . . . . . . . 19 Word ..^ lastS
1421413ad2ant1 1029 . . . . . . . . . . . . . . . . . 18 Word ..^ lastS
143142ad2antlr 733 . . . . . . . . . . . . . . . . 17 USGrph Word ..^ lastS Neighbors
144143fveq2d 5869 . . . . . . . . . . . . . . . 16 USGrph Word ..^ lastS Neighbors ++ ++ ++ ++
145 simpr 463 . . . . . . . . . . . . . . . . . . . . . . . . . 26 USGrph Word Word
146 eqidd 2452 . . . . . . . . . . . . . . . . . . . . . . . . . 26 USGrph Word
147145, 146jca 535 . . . . . . . . . . . . . . . . . . . . . . . . 25 USGrph Word Word
148147adantr 467 . . . . . . . . . . . . . . . . . . . . . . . 24 USGrph Word Neighbors Word
149125ad2antrr 732 . . . . . . . . . . . . . . . . . . . . . . . 24 USGrph Word Neighbors
15019ad2antrr 732 . . . . . . . . . . . . . . . . . . . . . . . . 25 USGrph Word Neighbors
151150imp 431 . . . . . . . . . . . . . . . . . . . . . . . 24 USGrph Word Neighbors
152 ccatw2s1p1 12769 . . . . . . . . . . . . . . . . . . . . . . . 24 Word ++ ++
153148, 149, 151, 152syl12anc 1266 . . . . . . . . . . . . . . . . . . . . . . 23 USGrph Word Neighbors ++ ++
154153ex 436 . . . . . . . . . . . . . . . . . . . . . 22 USGrph Word Neighbors ++ ++
155154expcom 437 . . . . . . . . . . . . . . . . . . . . 21 Word USGrph Neighbors ++ ++
1561553ad2ant1 1029 . . . . . . . . . . . . . . . . . . . 20 Word ..^ lastS USGrph Neighbors ++ ++
1571563ad2ant1 1029 . . . . . . . . . . . . . . . . . . 19 Word ..^ lastS USGrph Neighbors ++ ++
158157com12 32 . . . . . . . . . . . . . . . . . 18 USGrph Word ..^ lastS Neighbors ++ ++
1591583adant3 1028 . . . . . . . . . . . . . . . . 17 USGrph Word ..^ lastS Neighbors ++ ++
160159imp31 434 . . . . . . . . . . . . . . . 16 USGrph Word ..^ lastS Neighbors ++ ++
161144, 160eqtrd 2485 . . . . . . . . . . . . . . 15 USGrph Word ..^ lastS Neighbors ++ ++
162135, 161preq12d 4059 . . . . . . . . . . . . . 14 USGrph Word ..^ lastS Neighbors ++ ++ ++ ++
163 lsw 12711 . . . . . . . . . . . . . . . . . . . . . . . . 25 Word lastS
164163adantl 468 . . . . . . . . . . . . . . . . . . . . . . . 24 Word lastS
165 simpl 459 . . . . . . . . . . . . . . . . . . . . . . . 24 Word
166164, 165preq12d 4059 . . . . . . . . . . . . . . . . . . . . . . 23 Word lastS
167166eleq1d 2513 . . . . . . . . . . . . . . . . . . . . . 22 Word lastS
168167biimpd 211 . . . . . . . . . . . . . . . . . . . . 21 Word lastS
169168ex 436 . . . . . . . . . . . . . . . . . . . 20 Word lastS
170169com3l 84 . . . . . . . . . . . . . . . . . . 19 Word lastS
171170imp 431 . . . . . . . . . . . . . . . . . 18 Word lastS
1721713adant2 1027 . . . . . . . . . . . . . . . . 17 Word ..^ lastS
173172a1d 26 . . . . . . . . . . . . . . . 16 Word ..^ lastS
1741733imp 1202 . . . . . . . . . . . . . . 15 Word ..^ lastS
175174ad2antlr 733 . . . . . . . . . . . . . 14 USGrph Word ..^ lastS Neighbors
176162, 175eqeltrd 2529 . . . . . . . . . . . . 13 USGrph Word ..^ lastS Neighbors ++ ++ ++ ++
177 eqid 2451 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
178177, 152mpanl2 687 . . . . . . . . . . . . . . . . . . . . . . . . . 26 Word ++ ++
179 ccatw2s1p2 12770 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 Word ++ ++
180177, 179mpanl2 687 . . . . . . . . . . . . . . . . . . . . . . . . . 26 Word ++ ++
181178, 180preq12d 4059 . . . . . . . . . . . . . . . . . . . . . . . . 25 Word ++ ++ ++ ++
182181expcom 437 . . . . . . . . . . . . . . . . . . . . . . . 24 Word ++ ++ ++ ++
183182expcom 437 . . . . . . . . . . . . . . . . . . . . . . 23 Word ++ ++ ++ ++
18419, 183syl6 34 . . . . . . . . . . . . . . . . . . . . . 22 USGrph Neighbors Word ++ ++ ++ ++
185184com24 90 . . . . . . . . . . . . . . . . . . . . 21 USGrph Word Neighbors ++ ++ ++ ++
186185com12 32 . . . . . . . . . . . . . . . . . . . 20 Word USGrph Neighbors ++ ++ ++ ++
187186impd 433 . . . . . . . . . . . . . . . . . . 19 Word USGrph Neighbors ++ ++ ++ ++
1881873ad2ant1 1029 . . . . . . . . . . . . . . . . . 18 Word ..^ lastS USGrph Neighbors ++ ++ ++ ++
1891883ad2ant1 1029 . . . . . . . . . . . . . . . . 17 Word ..^ lastS USGrph Neighbors ++ ++ ++ ++
190189com12 32 . . . . . . . . . . . . . . . 16 USGrph Word ..^ lastS Neighbors ++ ++ ++ ++
1911903adant3 1028 . . . . . . . . . . . . . . 15 USGrph Word ..^ lastS Neighbors ++ ++ ++ ++
192191imp31 434 . . . . . . . . . . . . . 14 USGrph Word ..^ lastS Neighbors ++ ++ ++ ++
193 nbgraeledg 25158 . . . . . . . . . . . . . . . . . 18 USGrph Neighbors
194 prcom 4050 . . . . . . . . . . . . . . . . . . . 20
195194eleq1i 2520 . . . . . . . . . . . . . . . . . . 19
196195biimpi 198 . . . . . . . . . . . . . . . . . 18
197193, 196syl6bi 232 . . . . . . . . . . . . . . . . 17 USGrph Neighbors
1981973ad2ant1 1029 . . . . . . . . . . . . . . . 16 USGrph Neighbors
199198adantr 467 . . . . . . . . . . . . . . 15 USGrph Word ..^ lastS Neighbors
200199imp 431 . . . . . . . . . . . . . 14 USGrph Word ..^ lastS Neighbors
201192, 200eqeltrd 2529 . . . . . . . . . . . . 13 USGrph Word ..^ lastS Neighbors ++ ++ ++ ++
202 ovex 6318 . . . . . . . . . . . . . 14
203 fvex 5875 . . . . . . . . . . . . . 14
204 fveq2 5865 . . . . . . . . . . . . . . . 16 ++ ++ ++ ++
205 oveq1 6297 . . . . . . . . . . . . . . . . 17
206205fveq2d 5869 . . . . . . . . . . . . . . . 16 ++ ++ ++ ++
207204, 206preq12d 4059 . . . . . . . . . . . . . . 15 ++ ++ ++ ++ ++ ++ ++ ++
208207eleq1d 2513 . . . . . . . . . . . . . 14 ++ ++ ++ ++ ++ ++ ++ ++
209 fveq2 5865 . . . . . . . . . . . . . . . 16 ++ ++ ++ ++
210 oveq1 6297 . . . . . . . . . . . . . . . . 17
211210fveq2d 5869 . . . . . . . . . . . . . . . 16 ++ ++ ++ ++
212209, 211preq12d 4059 . . . . . . . . . . . . . . 15 ++ ++ ++ ++ ++ ++ ++ ++
213212eleq1d 2513 . . . . . . . . . . . . . 14 ++ ++ ++ ++ ++ ++ ++ ++
214202, 203, 208, 213ralpr 4025 . . . . . . . . . . . . 13 ++ ++ ++ ++ ++ ++ ++ ++ ++ ++ ++ ++
215176, 201, 214sylanbrc 670 . . . . . . . . . . . 12 USGrph Word ..^ lastS Neighbors ++ ++ ++ ++
21696, 215jca 535 . . . . . . . . . . 11 USGrph Word ..^ lastS Neighbors ..^ ++ ++ ++ ++ ++ ++ ++ ++
217 2cnd 10682 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
218 1cnd 9659 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
219136, 217, 2183jca 1188 . . . . . . . . . . . . . . . . . . . . . . . . . 26
22032, 219syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 Word
2212203ad2ant1 1029 . . . . . . . . . . . . . . . . . . . . . . . 24 Word ..^ lastS
222221adantr 467 . . . . . . . . . . . . . . . . . . . . . . 23 Word ..^ lastS
223 addsubass 9885 . . . . . . . . . . . . . . . . . . . . . . 23