Step | Hyp | Ref
| Expression |
1 | | 3anass 1096 |
. . . . . . 7
β’ ((π β π β§ π β π β§ π β π) β (π β π β§ (π β π β§ π β π))) |
2 | 1 | bianass 641 |
. . . . . 6
β’ ((πΊ β ComplUSGraph β§
(π β π β§ π β π β§ π β π)) β ((πΊ β ComplUSGraph β§ π β π) β§ (π β π β§ π β π))) |
3 | | cusgrusgr 28416 |
. . . . . . . . 9
β’ (πΊ β ComplUSGraph β
πΊ β
USGraph) |
4 | | usgrumgr 28179 |
. . . . . . . . 9
β’ (πΊ β USGraph β πΊ β
UMGraph) |
5 | 3, 4 | syl 17 |
. . . . . . . 8
β’ (πΊ β ComplUSGraph β
πΊ β
UMGraph) |
6 | | 3simpc 1151 |
. . . . . . . . . . . . 13
β’ ((π β π β§ π β π β§ π β π) β (π β π β§ π β π)) |
7 | 6 | ancli 550 |
. . . . . . . . . . . 12
β’ ((π β π β§ π β π β§ π β π) β ((π β π β§ π β π β§ π β π) β§ (π β π β§ π β π))) |
8 | | df-3an 1090 |
. . . . . . . . . . . . 13
β’ ((π β π β§ π β π β§ π β π) β ((π β π β§ π β π) β§ π β π)) |
9 | 8 | biimpi 215 |
. . . . . . . . . . . 12
β’ ((π β π β§ π β π β§ π β π) β ((π β π β§ π β π) β§ π β π)) |
10 | | an32 645 |
. . . . . . . . . . . . . . 15
β’ ((((π β π β§ π β π β§ π β π) β§ (π β π β§ π β π)) β§ (π β π β§ π β π)) β (((π β π β§ π β π β§ π β π) β§ (π β π β§ π β π)) β§ (π β π β§ π β π))) |
11 | 10 | anbi1i 625 |
. . . . . . . . . . . . . 14
β’
(((((π β π β§ π β π β§ π β π) β§ (π β π β§ π β π)) β§ (π β π β§ π β π)) β§ π β π) β ((((π β π β§ π β π β§ π β π) β§ (π β π β§ π β π)) β§ (π β π β§ π β π)) β§ π β π)) |
12 | | anass 470 |
. . . . . . . . . . . . . 14
β’
(((((π β π β§ π β π β§ π β π) β§ (π β π β§ π β π)) β§ (π β π β§ π β π)) β§ π β π) β (((π β π β§ π β π β§ π β π) β§ (π β π β§ π β π)) β§ ((π β π β§ π β π) β§ π β π))) |
13 | 11, 12 | sylbb 218 |
. . . . . . . . . . . . 13
β’
(((((π β π β§ π β π β§ π β π) β§ (π β π β§ π β π)) β§ (π β π β§ π β π)) β§ π β π) β (((π β π β§ π β π β§ π β π) β§ (π β π β§ π β π)) β§ ((π β π β§ π β π) β§ π β π))) |
14 | 13 | anasss 468 |
. . . . . . . . . . . 12
β’ ((((π β π β§ π β π β§ π β π) β§ (π β π β§ π β π)) β§ ((π β π β§ π β π) β§ π β π)) β (((π β π β§ π β π β§ π β π) β§ (π β π β§ π β π)) β§ ((π β π β§ π β π) β§ π β π))) |
15 | 7, 9, 14 | syl2an 597 |
. . . . . . . . . . 11
β’ (((π β π β§ π β π β§ π β π) β§ (π β π β§ π β π β§ π β π)) β (((π β π β§ π β π β§ π β π) β§ (π β π β§ π β π)) β§ ((π β π β§ π β π) β§ π β π))) |
16 | | anandi3 1103 |
. . . . . . . . . . . . . . 15
β’ ((π β π β§ π β π β§ π β π) β ((π β π β§ π β π) β§ (π β π β§ π β π))) |
17 | 16 | anbi1i 625 |
. . . . . . . . . . . . . 14
β’ (((π β π β§ π β π β§ π β π) β§ (π β π β§ π β π)) β (((π β π β§ π β π) β§ (π β π β§ π β π)) β§ (π β π β§ π β π))) |
18 | | an4 655 |
. . . . . . . . . . . . . 14
β’ ((((π β π β§ π β π) β§ (π β π β§ π β π)) β§ (π β π β§ π β π)) β (((π β π β§ π β π) β§ π β π) β§ ((π β π β§ π β π) β§ π β π))) |
19 | 17, 18 | sylbb 218 |
. . . . . . . . . . . . 13
β’ (((π β π β§ π β π β§ π β π) β§ (π β π β§ π β π)) β (((π β π β§ π β π) β§ π β π) β§ ((π β π β§ π β π) β§ π β π))) |
20 | | df-3an 1090 |
. . . . . . . . . . . . . . 15
β’ ((π β π β§ π β π β§ π β π) β ((π β π β§ π β π) β§ π β π)) |
21 | | cusgr3cyclex.1 |
. . . . . . . . . . . . . . . 16
β’ π = (VtxβπΊ) |
22 | | eqid 2733 |
. . . . . . . . . . . . . . . 16
β’
(EdgβπΊ) =
(EdgβπΊ) |
23 | 21, 22 | cusgredgex2 33780 |
. . . . . . . . . . . . . . 15
β’ (πΊ β ComplUSGraph β
((π β π β§ π β π β§ π β π) β {π, π} β (EdgβπΊ))) |
24 | 20, 23 | biimtrrid 242 |
. . . . . . . . . . . . . 14
β’ (πΊ β ComplUSGraph β
(((π β π β§ π β π) β§ π β π) β {π, π} β (EdgβπΊ))) |
25 | | df-3an 1090 |
. . . . . . . . . . . . . . 15
β’ ((π β π β§ π β π β§ π β π) β ((π β π β§ π β π) β§ π β π)) |
26 | 21, 22 | cusgredgex2 33780 |
. . . . . . . . . . . . . . 15
β’ (πΊ β ComplUSGraph β
((π β π β§ π β π β§ π β π) β {π, π} β (EdgβπΊ))) |
27 | 25, 26 | biimtrrid 242 |
. . . . . . . . . . . . . 14
β’ (πΊ β ComplUSGraph β
(((π β π β§ π β π) β§ π β π) β {π, π} β (EdgβπΊ))) |
28 | 24, 27 | anim12d 610 |
. . . . . . . . . . . . 13
β’ (πΊ β ComplUSGraph β
((((π β π β§ π β π) β§ π β π) β§ ((π β π β§ π β π) β§ π β π)) β ({π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ)))) |
29 | 19, 28 | syl5 34 |
. . . . . . . . . . . 12
β’ (πΊ β ComplUSGraph β
(((π β π β§ π β π β§ π β π) β§ (π β π β§ π β π)) β ({π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ)))) |
30 | | df-3an 1090 |
. . . . . . . . . . . . 13
β’ ((π β π β§ π β π β§ π β π) β ((π β π β§ π β π) β§ π β π)) |
31 | 21, 22 | cusgredgex2 33780 |
. . . . . . . . . . . . 13
β’ (πΊ β ComplUSGraph β
((π β π β§ π β π β§ π β π) β {π, π} β (EdgβπΊ))) |
32 | 30, 31 | biimtrrid 242 |
. . . . . . . . . . . 12
β’ (πΊ β ComplUSGraph β
(((π β π β§ π β π) β§ π β π) β {π, π} β (EdgβπΊ))) |
33 | 29, 32 | anim12d 610 |
. . . . . . . . . . 11
β’ (πΊ β ComplUSGraph β
((((π β π β§ π β π β§ π β π) β§ (π β π β§ π β π)) β§ ((π β π β§ π β π) β§ π β π)) β (({π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ)) β§ {π, π} β (EdgβπΊ)))) |
34 | 15, 33 | syl5 34 |
. . . . . . . . . 10
β’ (πΊ β ComplUSGraph β
(((π β π β§ π β π β§ π β π) β§ (π β π β§ π β π β§ π β π)) β (({π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ)) β§ {π, π} β (EdgβπΊ)))) |
35 | | 3anan32 1098 |
. . . . . . . . . . 11
β’ (({π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ)) β (({π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ)) β§ {π, π} β (EdgβπΊ))) |
36 | | prcom 4697 |
. . . . . . . . . . . . 13
β’ {π, π} = {π, π} |
37 | 36 | eleq1i 2825 |
. . . . . . . . . . . 12
β’ ({π, π} β (EdgβπΊ) β {π, π} β (EdgβπΊ)) |
38 | 37 | 3anbi3i 1160 |
. . . . . . . . . . 11
β’ (({π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ)) β ({π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ))) |
39 | 35, 38 | bitr3i 277 |
. . . . . . . . . 10
β’ ((({π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ)) β§ {π, π} β (EdgβπΊ)) β ({π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ))) |
40 | 34, 39 | syl6ib 251 |
. . . . . . . . 9
β’ (πΊ β ComplUSGraph β
(((π β π β§ π β π β§ π β π) β§ (π β π β§ π β π β§ π β π)) β ({π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ)))) |
41 | | pm5.3 574 |
. . . . . . . . 9
β’ ((((π β π β§ π β π β§ π β π) β§ (π β π β§ π β π β§ π β π)) β ({π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ))) β (((π β π β§ π β π β§ π β π) β§ (π β π β§ π β π β§ π β π)) β ((π β π β§ π β π β§ π β π) β§ ({π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ))))) |
42 | 40, 41 | sylib 217 |
. . . . . . . 8
β’ (πΊ β ComplUSGraph β
(((π β π β§ π β π β§ π β π) β§ (π β π β§ π β π β§ π β π)) β ((π β π β§ π β π β§ π β π) β§ ({π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ))))) |
43 | 21, 22 | umgr3cyclex 29176 |
. . . . . . . . . 10
β’ ((πΊ β UMGraph β§ (π β π β§ π β π β§ π β π) β§ ({π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ))) β βπβπ(π(CyclesβπΊ)π β§ (β―βπ) = 3 β§ (πβ0) = π)) |
44 | | 3simpa 1149 |
. . . . . . . . . . 11
β’ ((π(CyclesβπΊ)π β§ (β―βπ) = 3 β§ (πβ0) = π) β (π(CyclesβπΊ)π β§ (β―βπ) = 3)) |
45 | 44 | 2eximi 1839 |
. . . . . . . . . 10
β’
(βπβπ(π(CyclesβπΊ)π β§ (β―βπ) = 3 β§ (πβ0) = π) β βπβπ(π(CyclesβπΊ)π β§ (β―βπ) = 3)) |
46 | 43, 45 | syl 17 |
. . . . . . . . 9
β’ ((πΊ β UMGraph β§ (π β π β§ π β π β§ π β π) β§ ({π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ))) β βπβπ(π(CyclesβπΊ)π β§ (β―βπ) = 3)) |
47 | 46 | 3expib 1123 |
. . . . . . . 8
β’ (πΊ β UMGraph β (((π β π β§ π β π β§ π β π) β§ ({π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ))) β βπβπ(π(CyclesβπΊ)π β§ (β―βπ) = 3))) |
48 | 5, 42, 47 | sylsyld 61 |
. . . . . . 7
β’ (πΊ β ComplUSGraph β
(((π β π β§ π β π β§ π β π) β§ (π β π β§ π β π β§ π β π)) β βπβπ(π(CyclesβπΊ)π β§ (β―βπ) = 3))) |
49 | 48 | expdimp 454 |
. . . . . 6
β’ ((πΊ β ComplUSGraph β§
(π β π β§ π β π β§ π β π)) β ((π β π β§ π β π β§ π β π) β βπβπ(π(CyclesβπΊ)π β§ (β―βπ) = 3))) |
50 | 2, 49 | sylbir 234 |
. . . . 5
β’ (((πΊ β ComplUSGraph β§ π β π) β§ (π β π β§ π β π)) β ((π β π β§ π β π β§ π β π) β βπβπ(π(CyclesβπΊ)π β§ (β―βπ) = 3))) |
51 | 50 | reximdvva 3199 |
. . . 4
β’ ((πΊ β ComplUSGraph β§ π β π) β (βπ β π βπ β π (π β π β§ π β π β§ π β π) β βπ β π βπ β π βπβπ(π(CyclesβπΊ)π β§ (β―βπ) = 3))) |
52 | 51 | reximdva 3162 |
. . 3
β’ (πΊ β ComplUSGraph β
(βπ β π βπ β π βπ β π (π β π β§ π β π β§ π β π) β βπ β π βπ β π βπ β π βπβπ(π(CyclesβπΊ)π β§ (β―βπ) = 3))) |
53 | | id 22 |
. . . . . 6
β’
(βπβπ(π(CyclesβπΊ)π β§ (β―βπ) = 3) β βπβπ(π(CyclesβπΊ)π β§ (β―βπ) = 3)) |
54 | 53 | rexlimivw 3145 |
. . . . 5
β’
(βπ β
π βπβπ(π(CyclesβπΊ)π β§ (β―βπ) = 3) β βπβπ(π(CyclesβπΊ)π β§ (β―βπ) = 3)) |
55 | 54 | rexlimivw 3145 |
. . . 4
β’
(βπ β
π βπ β π βπβπ(π(CyclesβπΊ)π β§ (β―βπ) = 3) β βπβπ(π(CyclesβπΊ)π β§ (β―βπ) = 3)) |
56 | 55 | rexlimivw 3145 |
. . 3
β’
(βπ β
π βπ β π βπ β π βπβπ(π(CyclesβπΊ)π β§ (β―βπ) = 3) β βπβπ(π(CyclesβπΊ)π β§ (β―βπ) = 3)) |
57 | 52, 56 | syl6 35 |
. 2
β’ (πΊ β ComplUSGraph β
(βπ β π βπ β π βπ β π (π β π β§ π β π β§ π β π) β βπβπ(π(CyclesβπΊ)π β§ (β―βπ) = 3))) |
58 | 21 | fvexi 6860 |
. . 3
β’ π β V |
59 | | hashgt23el 14333 |
. . 3
β’ ((π β V β§ 2 <
(β―βπ)) β
βπ β π βπ β π βπ β π (π β π β§ π β π β§ π β π)) |
60 | 58, 59 | mpan 689 |
. 2
β’ (2 <
(β―βπ) β
βπ β π βπ β π βπ β π (π β π β§ π β π β§ π β π)) |
61 | 57, 60 | impel 507 |
1
β’ ((πΊ β ComplUSGraph β§ 2
< (β―βπ))
β βπβπ(π(CyclesβπΊ)π β§ (β―βπ) = 3)) |