Step | Hyp | Ref
| Expression |
1 | | hashcl 14256 |
. . 3
β’ (π β Fin β
(β―βπ) β
β0) |
2 | | ax-1 6 |
. . . . 5
β’
(((β―βπ)
= 0 β¨ (β―βπ)
= 1 β¨ (β―βπ)
= 3) β ((((β―βπ) β β0 β§ π β Fin β§ πΊ β FriendGraph ) β§
πΊ RegUSGraph πΎ) β ((β―βπ) = 0 β¨ (β―βπ) = 1 β¨ (β―βπ) = 3))) |
3 | | 3ioran 1106 |
. . . . . 6
β’ (Β¬
((β―βπ) = 0 β¨
(β―βπ) = 1 β¨
(β―βπ) = 3)
β (Β¬ (β―βπ) = 0 β§ Β¬ (β―βπ) = 1 β§ Β¬
(β―βπ) =
3)) |
4 | | df-ne 2944 |
. . . . . . . . . . . . 13
β’
((β―βπ)
β 0 β Β¬ (β―βπ) = 0) |
5 | | hasheq0 14263 |
. . . . . . . . . . . . . . . . . 18
β’ (π β Fin β
((β―βπ) = 0
β π =
β
)) |
6 | 5 | necon3bid 2988 |
. . . . . . . . . . . . . . . . 17
β’ (π β Fin β
((β―βπ) β 0
β π β
β
)) |
7 | 6 | biimpa 477 |
. . . . . . . . . . . . . . . 16
β’ ((π β Fin β§
(β―βπ) β 0)
β π β
β
) |
8 | | elnnne0 12427 |
. . . . . . . . . . . . . . . . . . . 20
β’
((β―βπ)
β β β ((β―βπ) β β0 β§
(β―βπ) β
0)) |
9 | | df-ne 2944 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
((β―βπ)
β 1 β Β¬ (β―βπ) = 1) |
10 | | eluz2b3 12847 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
((β―βπ)
β (β€β₯β2) β ((β―βπ) β β β§
(β―βπ) β
1)) |
11 | | hash2prde 14369 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ ((π β Fin β§
(β―βπ) = 2)
β βπβπ(π β π β§ π = {π, π})) |
12 | | vex 3449 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
β’ π β V |
13 | 12 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
β’ (π β π β π β V) |
14 | | vex 3449 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
β’ π β V |
15 | 14 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
β’ (π β π β π β V) |
16 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
β’ (π β π β π β π) |
17 | 13, 15, 16 | 3jca 1128 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’ (π β π β (π β V β§ π β V β§ π β π)) |
18 | | frgrreggt1.v |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
β’ π = (VtxβπΊ) |
19 | 18 | eqeq1i 2741 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
β’ (π = {π, π} β (VtxβπΊ) = {π, π}) |
20 | 19 | biimpi 215 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’ (π = {π, π} β (VtxβπΊ) = {π, π}) |
21 | | nfrgr2v 29216 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’ (((π β V β§ π β V β§ π β π) β§ (VtxβπΊ) = {π, π}) β πΊ β FriendGraph ) |
22 | 17, 20, 21 | syl2an 596 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ ((π β π β§ π = {π, π}) β πΊ β FriendGraph ) |
23 | | df-nel 3050 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ (πΊ β FriendGraph β
Β¬ πΊ β FriendGraph
) |
24 | 22, 23 | sylib 217 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ ((π β π β§ π = {π, π}) β Β¬ πΊ β FriendGraph ) |
25 | 24 | pm2.21d 121 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ ((π β π β§ π = {π, π}) β (πΊ β FriendGraph β (π β β
β (Β¬
(β―βπ) = 3
β (πΊ RegUSGraph πΎ β ((β―βπ) = 0 β¨ (β―βπ) = 1 β¨ (β―βπ) = 3)))))) |
26 | 25 | com23 86 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ ((π β π β§ π = {π, π}) β (π β β
β (πΊ β FriendGraph β (Β¬
(β―βπ) = 3
β (πΊ RegUSGraph πΎ β ((β―βπ) = 0 β¨ (β―βπ) = 1 β¨ (β―βπ) = 3)))))) |
27 | 26 | exlimivv 1935 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’
(βπβπ(π β π β§ π = {π, π}) β (π β β
β (πΊ β FriendGraph β (Β¬
(β―βπ) = 3
β (πΊ RegUSGraph πΎ β ((β―βπ) = 0 β¨ (β―βπ) = 1 β¨ (β―βπ) = 3)))))) |
28 | 11, 27 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((π β Fin β§
(β―βπ) = 2)
β (π β β
β (πΊ β
FriendGraph β (Β¬ (β―βπ) = 3 β (πΊ RegUSGraph πΎ β ((β―βπ) = 0 β¨ (β―βπ) = 1 β¨ (β―βπ) = 3)))))) |
29 | 28 | ex 413 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (π β Fin β
((β―βπ) = 2
β (π β β
β (πΊ β
FriendGraph β (Β¬ (β―βπ) = 3 β (πΊ RegUSGraph πΎ β ((β―βπ) = 0 β¨ (β―βπ) = 1 β¨ (β―βπ) = 3))))))) |
30 | 29 | com23 86 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π β Fin β (π β β
β
((β―βπ) = 2
β (πΊ β
FriendGraph β (Β¬ (β―βπ) = 3 β (πΊ RegUSGraph πΎ β ((β―βπ) = 0 β¨ (β―βπ) = 1 β¨ (β―βπ) = 3))))))) |
31 | 30 | com14 96 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (πΊ β FriendGraph β
(π β β
β
((β―βπ) = 2
β (π β Fin β
(Β¬ (β―βπ) =
3 β (πΊ RegUSGraph
πΎ β
((β―βπ) = 0 β¨
(β―βπ) = 1 β¨
(β―βπ) =
3))))))) |
32 | 31 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’
((β―βπ)
β (β€β₯β2) β (πΊ β FriendGraph β (π β β
β
((β―βπ) = 2
β (π β Fin β
(Β¬ (β―βπ) =
3 β (πΊ RegUSGraph
πΎ β
((β―βπ) = 0 β¨
(β―βπ) = 1 β¨
(β―βπ) =
3)))))))) |
33 | 32 | 3imp 1111 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
(((β―βπ)
β (β€β₯β2) β§ πΊ β FriendGraph β§ π β β
) β ((β―βπ) = 2 β (π β Fin β (Β¬
(β―βπ) = 3
β (πΊ RegUSGraph πΎ β ((β―βπ) = 0 β¨ (β―βπ) = 1 β¨ (β―βπ) = 3)))))) |
34 | 33 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
((β―βπ) =
2 β (((β―βπ) β (β€β₯β2)
β§ πΊ β FriendGraph
β§ π β β
)
β (π β Fin β
(Β¬ (β―βπ) =
3 β (πΊ RegUSGraph
πΎ β
((β―βπ) = 0 β¨
(β―βπ) = 1 β¨
(β―βπ) =
3)))))) |
35 | | eqid 2736 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
β’
(VtxDegβπΊ) =
(VtxDegβπΊ) |
36 | 18, 35 | rusgrprop0 28515 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
β’ (πΊ RegUSGraph πΎ β (πΊ β USGraph β§ πΎ β β0*
β§ βπ£ β
π ((VtxDegβπΊ)βπ£) = πΎ)) |
37 | | eluz2gt1 12845 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . 49
β’
((β―βπ)
β (β€β₯β2) β 1 < (β―βπ)) |
38 | 37 | anim1ci 616 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . 48
β’
(((β―βπ)
β (β€β₯β2) β§ πΊ β FriendGraph ) β (πΊ β FriendGraph β§ 1 <
(β―βπ))) |
39 | 18 | vdgn0frgrv2 29239 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . 50
β’ ((πΊ β FriendGraph β§ π£ β π) β (1 < (β―βπ) β ((VtxDegβπΊ)βπ£) β 0)) |
40 | 39 | impancom 452 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . 49
β’ ((πΊ β FriendGraph β§ 1 <
(β―βπ)) β
(π£ β π β ((VtxDegβπΊ)βπ£) β 0)) |
41 | 40 | ralrimiv 3142 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . 48
β’ ((πΊ β FriendGraph β§ 1 <
(β―βπ)) β
βπ£ β π ((VtxDegβπΊ)βπ£) β 0) |
42 | | eqeq2 2748 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . 51
β’ (πΎ = 0 β
(((VtxDegβπΊ)βπ£) = πΎ β ((VtxDegβπΊ)βπ£) = 0)) |
43 | 42 | ralbidv 3174 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . 50
β’ (πΎ = 0 β (βπ£ β π ((VtxDegβπΊ)βπ£) = πΎ β βπ£ β π ((VtxDegβπΊ)βπ£) = 0)) |
44 | | r19.26 3114 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . 52
β’
(βπ£ β
π (((VtxDegβπΊ)βπ£) = 0 β§ ((VtxDegβπΊ)βπ£) β 0) β (βπ£ β π ((VtxDegβπΊ)βπ£) = 0 β§ βπ£ β π ((VtxDegβπΊ)βπ£) β 0)) |
45 | | nne 2947 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . . 57
β’ (Β¬
((VtxDegβπΊ)βπ£) β 0 β ((VtxDegβπΊ)βπ£) = 0) |
46 | 45 | bicomi 223 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . 56
β’
(((VtxDegβπΊ)βπ£) = 0 β Β¬ ((VtxDegβπΊ)βπ£) β 0) |
47 | 46 | anbi1i 624 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . 55
β’
((((VtxDegβπΊ)βπ£) = 0 β§ ((VtxDegβπΊ)βπ£) β 0) β (Β¬ ((VtxDegβπΊ)βπ£) β 0 β§ ((VtxDegβπΊ)βπ£) β 0)) |
48 | | ancom 461 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . 55
β’ ((Β¬
((VtxDegβπΊ)βπ£) β 0 β§ ((VtxDegβπΊ)βπ£) β 0) β (((VtxDegβπΊ)βπ£) β 0 β§ Β¬ ((VtxDegβπΊ)βπ£) β 0)) |
49 | | pm3.24 403 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . 56
β’ Β¬
(((VtxDegβπΊ)βπ£) β 0 β§ Β¬ ((VtxDegβπΊ)βπ£) β 0) |
50 | 49 | bifal 1557 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . 55
β’
((((VtxDegβπΊ)βπ£) β 0 β§ Β¬ ((VtxDegβπΊ)βπ£) β 0) β β₯) |
51 | 47, 48, 50 | 3bitri 296 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . 54
β’
((((VtxDegβπΊ)βπ£) = 0 β§ ((VtxDegβπΊ)βπ£) β 0) β β₯) |
52 | 51 | ralbii 3096 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . 53
β’
(βπ£ β
π (((VtxDegβπΊ)βπ£) = 0 β§ ((VtxDegβπΊ)βπ£) β 0) β βπ£ β π β₯) |
53 | | r19.3rzv 4456 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . 56
β’ (π β β
β (β₯
β βπ£ β
π β₯)) |
54 | | falim 1558 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . . 56
β’ (β₯
β ((β―βπ) =
0 β¨ (β―βπ) =
1 β¨ (β―βπ) =
3)) |
55 | 53, 54 | syl6bir 253 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . 55
β’ (π β β
β
(βπ£ β π β₯ β
((β―βπ) = 0 β¨
(β―βπ) = 1 β¨
(β―βπ) =
3))) |
56 | 55 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . 54
β’ ((π β Fin β§ π β β
) β
(βπ£ β π β₯ β
((β―βπ) = 0 β¨
(β―βπ) = 1 β¨
(β―βπ) =
3))) |
57 | 56 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . 53
β’
(βπ£ β
π β₯ β ((π β Fin β§ π β β
) β
((β―βπ) = 0 β¨
(β―βπ) = 1 β¨
(β―βπ) =
3))) |
58 | 52, 57 | sylbi 216 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . 52
β’
(βπ£ β
π (((VtxDegβπΊ)βπ£) = 0 β§ ((VtxDegβπΊ)βπ£) β 0) β ((π β Fin β§ π β β
) β ((β―βπ) = 0 β¨ (β―βπ) = 1 β¨ (β―βπ) = 3))) |
59 | 44, 58 | sylbir 234 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . 51
β’
((βπ£ β
π ((VtxDegβπΊ)βπ£) = 0 β§ βπ£ β π ((VtxDegβπΊ)βπ£) β 0) β ((π β Fin β§ π β β
) β ((β―βπ) = 0 β¨ (β―βπ) = 1 β¨ (β―βπ) = 3))) |
60 | 59 | ex 413 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . 50
β’
(βπ£ β
π ((VtxDegβπΊ)βπ£) = 0 β (βπ£ β π ((VtxDegβπΊ)βπ£) β 0 β ((π β Fin β§ π β β
) β ((β―βπ) = 0 β¨ (β―βπ) = 1 β¨ (β―βπ) = 3)))) |
61 | 43, 60 | syl6bi 252 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . 49
β’ (πΎ = 0 β (βπ£ β π ((VtxDegβπΊ)βπ£) = πΎ β (βπ£ β π ((VtxDegβπΊ)βπ£) β 0 β ((π β Fin β§ π β β
) β ((β―βπ) = 0 β¨ (β―βπ) = 1 β¨ (β―βπ) = 3))))) |
62 | 61 | com4t 93 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . 48
β’
(βπ£ β
π ((VtxDegβπΊ)βπ£) β 0 β ((π β Fin β§ π β β
) β (πΎ = 0 β (βπ£ β π ((VtxDegβπΊ)βπ£) = πΎ β ((β―βπ) = 0 β¨ (β―βπ) = 1 β¨ (β―βπ) = 3))))) |
63 | 38, 41, 62 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
β’
(((β―βπ)
β (β€β₯β2) β§ πΊ β FriendGraph ) β ((π β Fin β§ π β β
) β (πΎ = 0 β (βπ£ β π ((VtxDegβπΊ)βπ£) = πΎ β ((β―βπ) = 0 β¨ (β―βπ) = 1 β¨ (β―βπ) = 3))))) |
64 | 63 | ex 413 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
β’
((β―βπ)
β (β€β₯β2) β (πΊ β FriendGraph β ((π β Fin β§ π β β
) β (πΎ = 0 β (βπ£ β π ((VtxDegβπΊ)βπ£) = πΎ β ((β―βπ) = 0 β¨ (β―βπ) = 1 β¨ (β―βπ) = 3)))))) |
65 | 64 | com25 99 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
β’
((β―βπ)
β (β€β₯β2) β (βπ£ β π ((VtxDegβπΊ)βπ£) = πΎ β ((π β Fin β§ π β β
) β (πΎ = 0 β (πΊ β FriendGraph β
((β―βπ) = 0 β¨
(β―βπ) = 1 β¨
(β―βπ) =
3)))))) |
66 | 65 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
β’ (((Β¬
(β―βπ) = 3 β§
Β¬ (β―βπ) =
2) β§ (β―βπ)
β (β€β₯β2)) β (βπ£ β π ((VtxDegβπΊ)βπ£) = πΎ β ((π β Fin β§ π β β
) β (πΎ = 0 β (πΊ β FriendGraph β
((β―βπ) = 0 β¨
(β―βπ) = 1 β¨
(β―βπ) =
3)))))) |
67 | 66 | com15 101 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
β’ (πΊ β FriendGraph β
(βπ£ β π ((VtxDegβπΊ)βπ£) = πΎ β ((π β Fin β§ π β β
) β (πΎ = 0 β (((Β¬ (β―βπ) = 3 β§ Β¬
(β―βπ) = 2)
β§ (β―βπ)
β (β€β₯β2)) β ((β―βπ) = 0 β¨ (β―βπ) = 1 β¨ (β―βπ) = 3)))))) |
68 | 67 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
β’
(βπ£ β
π ((VtxDegβπΊ)βπ£) = πΎ β (πΊ β FriendGraph β ((π β Fin β§ π β β
) β (πΎ = 0 β (((Β¬
(β―βπ) = 3 β§
Β¬ (β―βπ) =
2) β§ (β―βπ)
β (β€β₯β2)) β ((β―βπ) = 0 β¨ (β―βπ) = 1 β¨ (β―βπ) = 3)))))) |
69 | 68 | 3ad2ant3 1135 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
β’ ((πΊ β USGraph β§ πΎ β
β0* β§ βπ£ β π ((VtxDegβπΊ)βπ£) = πΎ) β (πΊ β FriendGraph β ((π β Fin β§ π β β
) β (πΎ = 0 β (((Β¬
(β―βπ) = 3 β§
Β¬ (β―βπ) =
2) β§ (β―βπ)
β (β€β₯β2)) β ((β―βπ) = 0 β¨ (β―βπ) = 1 β¨ (β―βπ) = 3)))))) |
70 | 36, 69 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
β’ (πΊ RegUSGraph πΎ β (πΊ β FriendGraph β ((π β Fin β§ π β β
) β (πΎ = 0 β (((Β¬
(β―βπ) = 3 β§
Β¬ (β―βπ) =
2) β§ (β―βπ)
β (β€β₯β2)) β ((β―βπ) = 0 β¨ (β―βπ) = 1 β¨ (β―βπ) = 3)))))) |
71 | 70 | impcom 408 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
β’ ((πΊ β FriendGraph β§ πΊ RegUSGraph πΎ) β ((π β Fin β§ π β β
) β (πΎ = 0 β (((Β¬ (β―βπ) = 3 β§ Β¬
(β―βπ) = 2)
β§ (β―βπ)
β (β€β₯β2)) β ((β―βπ) = 0 β¨ (β―βπ) = 1 β¨ (β―βπ) = 3))))) |
72 | 71 | impcom 408 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’ (((π β Fin β§ π β β
) β§ (πΊ β FriendGraph β§ πΊ RegUSGraph πΎ)) β (πΎ = 0 β (((Β¬ (β―βπ) = 3 β§ Β¬
(β―βπ) = 2)
β§ (β―βπ)
β (β€β₯β2)) β ((β―βπ) = 0 β¨ (β―βπ) = 1 β¨ (β―βπ) = 3)))) |
73 | 18 | frrusgrord 29285 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
β’ ((π β Fin β§ π β β
) β ((πΊ β FriendGraph β§ πΊ RegUSGraph πΎ) β (β―βπ) = ((πΎ Β· (πΎ β 1)) + 1))) |
74 | 73 | imp 407 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
β’ (((π β Fin β§ π β β
) β§ (πΊ β FriendGraph β§ πΊ RegUSGraph πΎ)) β (β―βπ) = ((πΎ Β· (πΎ β 1)) + 1)) |
75 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
β’ (πΎ = 2 β πΎ = 2) |
76 | | oveq1 7364 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
β’ (πΎ = 2 β (πΎ β 1) = (2 β
1)) |
77 | 75, 76 | oveq12d 7375 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
β’ (πΎ = 2 β (πΎ Β· (πΎ β 1)) = (2 Β· (2 β
1))) |
78 | 77 | oveq1d 7372 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
β’ (πΎ = 2 β ((πΎ Β· (πΎ β 1)) + 1) = ((2 Β· (2 β
1)) + 1)) |
79 | | 2m1e1 12279 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
β’ (2
β 1) = 1 |
80 | 79 | oveq2i 7368 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
β’ (2
Β· (2 β 1)) = (2 Β· 1) |
81 | | 2t1e2 12316 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
β’ (2
Β· 1) = 2 |
82 | 80, 81 | eqtri 2764 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
β’ (2
Β· (2 β 1)) = 2 |
83 | 82 | oveq1i 7367 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
β’ ((2
Β· (2 β 1)) + 1) = (2 + 1) |
84 | | 2p1e3 12295 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
β’ (2 + 1) =
3 |
85 | 83, 84 | eqtri 2764 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
β’ ((2
Β· (2 β 1)) + 1) = 3 |
86 | 78, 85 | eqtrdi 2792 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
β’ (πΎ = 2 β ((πΎ Β· (πΎ β 1)) + 1) = 3) |
87 | 86 | eqeq2d 2747 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
β’ (πΎ = 2 β
((β―βπ) =
((πΎ Β· (πΎ β 1)) + 1) β
(β―βπ) =
3)) |
88 | | pm2.21 123 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
β’ (Β¬
(β―βπ) = 3
β ((β―βπ) =
3 β ((β―βπ)
= 0 β¨ (β―βπ)
= 1 β¨ (β―βπ)
= 3))) |
89 | 88 | ad2antrr 724 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
β’ (((Β¬
(β―βπ) = 3 β§
Β¬ (β―βπ) =
2) β§ (β―βπ)
β (β€β₯β2)) β ((β―βπ) = 3 β
((β―βπ) = 0 β¨
(β―βπ) = 1 β¨
(β―βπ) =
3))) |
90 | 89 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
β’
((β―βπ) =
3 β (((Β¬ (β―βπ) = 3 β§ Β¬ (β―βπ) = 2) β§
(β―βπ) β
(β€β₯β2)) β ((β―βπ) = 0 β¨ (β―βπ) = 1 β¨ (β―βπ) = 3))) |
91 | 87, 90 | syl6bi 252 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
β’ (πΎ = 2 β
((β―βπ) =
((πΎ Β· (πΎ β 1)) + 1) β
(((Β¬ (β―βπ)
= 3 β§ Β¬ (β―βπ) = 2) β§ (β―βπ) β
(β€β₯β2)) β ((β―βπ) = 0 β¨ (β―βπ) = 1 β¨ (β―βπ) = 3)))) |
92 | 74, 91 | syl5com 31 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’ (((π β Fin β§ π β β
) β§ (πΊ β FriendGraph β§ πΊ RegUSGraph πΎ)) β (πΎ = 2 β (((Β¬ (β―βπ) = 3 β§ Β¬
(β―βπ) = 2)
β§ (β―βπ)
β (β€β₯β2)) β ((β―βπ) = 0 β¨ (β―βπ) = 1 β¨ (β―βπ) = 3)))) |
93 | 18 | frgrreg 29338 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
β’ ((π β Fin β§ π β β
) β ((πΊ β FriendGraph β§ πΊ RegUSGraph πΎ) β (πΎ = 0 β¨ πΎ = 2))) |
94 | 93 | imp 407 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’ (((π β Fin β§ π β β
) β§ (πΊ β FriendGraph β§ πΊ RegUSGraph πΎ)) β (πΎ = 0 β¨ πΎ = 2)) |
95 | 72, 92, 94 | mpjaod 858 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ (((π β Fin β§ π β β
) β§ (πΊ β FriendGraph β§ πΊ RegUSGraph πΎ)) β (((Β¬ (β―βπ) = 3 β§ Β¬
(β―βπ) = 2)
β§ (β―βπ)
β (β€β₯β2)) β ((β―βπ) = 0 β¨ (β―βπ) = 1 β¨ (β―βπ) = 3))) |
96 | 95 | exp32 421 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ ((π β Fin β§ π β β
) β (πΊ β FriendGraph β
(πΊ RegUSGraph πΎ β (((Β¬
(β―βπ) = 3 β§
Β¬ (β―βπ) =
2) β§ (β―βπ)
β (β€β₯β2)) β ((β―βπ) = 0 β¨ (β―βπ) = 1 β¨ (β―βπ) = 3))))) |
97 | 96 | com34 91 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ ((π β Fin β§ π β β
) β (πΊ β FriendGraph β
(((Β¬ (β―βπ)
= 3 β§ Β¬ (β―βπ) = 2) β§ (β―βπ) β
(β€β₯β2)) β (πΊ RegUSGraph πΎ β ((β―βπ) = 0 β¨ (β―βπ) = 1 β¨ (β―βπ) = 3))))) |
98 | 97 | com23 86 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ ((π β Fin β§ π β β
) β (((Β¬
(β―βπ) = 3 β§
Β¬ (β―βπ) =
2) β§ (β―βπ)
β (β€β₯β2)) β (πΊ β FriendGraph β (πΊ RegUSGraph πΎ β ((β―βπ) = 0 β¨ (β―βπ) = 1 β¨ (β―βπ) = 3))))) |
99 | 98 | exp4c 433 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ ((π β Fin β§ π β β
) β (Β¬
(β―βπ) = 3
β (Β¬ (β―βπ) = 2 β ((β―βπ) β
(β€β₯β2) β (πΊ β FriendGraph β (πΊ RegUSGraph πΎ β ((β―βπ) = 0 β¨ (β―βπ) = 1 β¨ (β―βπ) = 3))))))) |
100 | 99 | com34 91 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((π β Fin β§ π β β
) β (Β¬
(β―βπ) = 3
β ((β―βπ)
β (β€β₯β2) β (Β¬ (β―βπ) = 2 β (πΊ β FriendGraph β (πΊ RegUSGraph πΎ β ((β―βπ) = 0 β¨ (β―βπ) = 1 β¨ (β―βπ) = 3))))))) |
101 | 100 | com25 99 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((π β Fin β§ π β β
) β (πΊ β FriendGraph β
((β―βπ) β
(β€β₯β2) β (Β¬ (β―βπ) = 2 β (Β¬ (β―βπ) = 3 β (πΊ RegUSGraph πΎ β ((β―βπ) = 0 β¨ (β―βπ) = 1 β¨ (β―βπ) = 3))))))) |
102 | 101 | ex 413 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π β Fin β (π β β
β (πΊ β FriendGraph β
((β―βπ) β
(β€β₯β2) β (Β¬ (β―βπ) = 2 β (Β¬ (β―βπ) = 3 β (πΊ RegUSGraph πΎ β ((β―βπ) = 0 β¨ (β―βπ) = 1 β¨ (β―βπ) = 3)))))))) |
103 | 102 | com23 86 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π β Fin β (πΊ β FriendGraph β
(π β β
β
((β―βπ) β
(β€β₯β2) β (Β¬ (β―βπ) = 2 β (Β¬ (β―βπ) = 3 β (πΊ RegUSGraph πΎ β ((β―βπ) = 0 β¨ (β―βπ) = 1 β¨ (β―βπ) = 3)))))))) |
104 | 103 | com14 96 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’
((β―βπ)
β (β€β₯β2) β (πΊ β FriendGraph β (π β β
β (π β Fin β (Β¬
(β―βπ) = 2
β (Β¬ (β―βπ) = 3 β (πΊ RegUSGraph πΎ β ((β―βπ) = 0 β¨ (β―βπ) = 1 β¨ (β―βπ) = 3)))))))) |
105 | 104 | 3imp 1111 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
(((β―βπ)
β (β€β₯β2) β§ πΊ β FriendGraph β§ π β β
) β (π β Fin β (Β¬
(β―βπ) = 2
β (Β¬ (β―βπ) = 3 β (πΊ RegUSGraph πΎ β ((β―βπ) = 0 β¨ (β―βπ) = 1 β¨ (β―βπ) = 3)))))) |
106 | 105 | com3r 87 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (Β¬
(β―βπ) = 2
β (((β―βπ)
β (β€β₯β2) β§ πΊ β FriendGraph β§ π β β
) β (π β Fin β (Β¬
(β―βπ) = 3
β (πΊ RegUSGraph πΎ β ((β―βπ) = 0 β¨ (β―βπ) = 1 β¨ (β―βπ) = 3)))))) |
107 | 34, 106 | pm2.61i 182 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(((β―βπ)
β (β€β₯β2) β§ πΊ β FriendGraph β§ π β β
) β (π β Fin β (Β¬
(β―βπ) = 3
β (πΊ RegUSGraph πΎ β ((β―βπ) = 0 β¨ (β―βπ) = 1 β¨ (β―βπ) = 3))))) |
108 | 107 | 3exp 1119 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
((β―βπ)
β (β€β₯β2) β (πΊ β FriendGraph β (π β β
β (π β Fin β (Β¬
(β―βπ) = 3
β (πΊ RegUSGraph πΎ β ((β―βπ) = 0 β¨ (β―βπ) = 1 β¨ (β―βπ) = 3))))))) |
109 | 10, 108 | sylbir 234 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(((β―βπ)
β β β§ (β―βπ) β 1) β (πΊ β FriendGraph β (π β β
β (π β Fin β (Β¬
(β―βπ) = 3
β (πΊ RegUSGraph πΎ β ((β―βπ) = 0 β¨ (β―βπ) = 1 β¨ (β―βπ) = 3))))))) |
110 | 109 | ex 413 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
((β―βπ)
β β β ((β―βπ) β 1 β (πΊ β FriendGraph β (π β β
β (π β Fin β (Β¬
(β―βπ) = 3
β (πΊ RegUSGraph πΎ β ((β―βπ) = 0 β¨ (β―βπ) = 1 β¨ (β―βπ) = 3)))))))) |
111 | 9, 110 | biimtrrid 242 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((β―βπ)
β β β (Β¬ (β―βπ) = 1 β (πΊ β FriendGraph β (π β β
β (π β Fin β (Β¬
(β―βπ) = 3
β (πΊ RegUSGraph πΎ β ((β―βπ) = 0 β¨ (β―βπ) = 1 β¨ (β―βπ) = 3)))))))) |
112 | 111 | com25 99 |
. . . . . . . . . . . . . . . . . . . 20
β’
((β―βπ)
β β β (π
β Fin β (πΊ β
FriendGraph β (π β
β
β (Β¬ (β―βπ) = 1 β (Β¬ (β―βπ) = 3 β (πΊ RegUSGraph πΎ β ((β―βπ) = 0 β¨ (β―βπ) = 1 β¨ (β―βπ) = 3)))))))) |
113 | 8, 112 | sylbir 234 |
. . . . . . . . . . . . . . . . . . 19
β’
(((β―βπ)
β β0 β§ (β―βπ) β 0) β (π β Fin β (πΊ β FriendGraph β (π β β
β (Β¬
(β―βπ) = 1
β (Β¬ (β―βπ) = 3 β (πΊ RegUSGraph πΎ β ((β―βπ) = 0 β¨ (β―βπ) = 1 β¨ (β―βπ) = 3)))))))) |
114 | 113 | ex 413 |
. . . . . . . . . . . . . . . . . 18
β’
((β―βπ)
β β0 β ((β―βπ) β 0 β (π β Fin β (πΊ β FriendGraph β (π β β
β (Β¬
(β―βπ) = 1
β (Β¬ (β―βπ) = 3 β (πΊ RegUSGraph πΎ β ((β―βπ) = 0 β¨ (β―βπ) = 1 β¨ (β―βπ) = 3))))))))) |
115 | 114 | impcomd 412 |
. . . . . . . . . . . . . . . . 17
β’
((β―βπ)
β β0 β ((π β Fin β§ (β―βπ) β 0) β (πΊ β FriendGraph β
(π β β
β
(Β¬ (β―βπ) =
1 β (Β¬ (β―βπ) = 3 β (πΊ RegUSGraph πΎ β ((β―βπ) = 0 β¨ (β―βπ) = 1 β¨ (β―βπ) = 3)))))))) |
116 | 115 | com14 96 |
. . . . . . . . . . . . . . . 16
β’ (π β β
β ((π β Fin β§
(β―βπ) β 0)
β (πΊ β
FriendGraph β ((β―βπ) β β0 β (Β¬
(β―βπ) = 1
β (Β¬ (β―βπ) = 3 β (πΊ RegUSGraph πΎ β ((β―βπ) = 0 β¨ (β―βπ) = 1 β¨ (β―βπ) = 3)))))))) |
117 | 7, 116 | mpcom 38 |
. . . . . . . . . . . . . . 15
β’ ((π β Fin β§
(β―βπ) β 0)
β (πΊ β
FriendGraph β ((β―βπ) β β0 β (Β¬
(β―βπ) = 1
β (Β¬ (β―βπ) = 3 β (πΊ RegUSGraph πΎ β ((β―βπ) = 0 β¨ (β―βπ) = 1 β¨ (β―βπ) = 3))))))) |
118 | 117 | ex 413 |
. . . . . . . . . . . . . 14
β’ (π β Fin β
((β―βπ) β 0
β (πΊ β
FriendGraph β ((β―βπ) β β0 β (Β¬
(β―βπ) = 1
β (Β¬ (β―βπ) = 3 β (πΊ RegUSGraph πΎ β ((β―βπ) = 0 β¨ (β―βπ) = 1 β¨ (β―βπ) = 3)))))))) |
119 | 118 | com14 96 |
. . . . . . . . . . . . 13
β’
((β―βπ)
β β0 β ((β―βπ) β 0 β (πΊ β FriendGraph β (π β Fin β (Β¬
(β―βπ) = 1
β (Β¬ (β―βπ) = 3 β (πΊ RegUSGraph πΎ β ((β―βπ) = 0 β¨ (β―βπ) = 1 β¨ (β―βπ) = 3)))))))) |
120 | 4, 119 | biimtrrid 242 |
. . . . . . . . . . . 12
β’
((β―βπ)
β β0 β (Β¬ (β―βπ) = 0 β (πΊ β FriendGraph β (π β Fin β (Β¬
(β―βπ) = 1
β (Β¬ (β―βπ) = 3 β (πΊ RegUSGraph πΎ β ((β―βπ) = 0 β¨ (β―βπ) = 1 β¨ (β―βπ) = 3)))))))) |
121 | 120 | com24 95 |
. . . . . . . . . . 11
β’
((β―βπ)
β β0 β (π β Fin β (πΊ β FriendGraph β (Β¬
(β―βπ) = 0
β (Β¬ (β―βπ) = 1 β (Β¬ (β―βπ) = 3 β (πΊ RegUSGraph πΎ β ((β―βπ) = 0 β¨ (β―βπ) = 1 β¨ (β―βπ) = 3)))))))) |
122 | 121 | 3imp 1111 |
. . . . . . . . . 10
β’
(((β―βπ)
β β0 β§ π β Fin β§ πΊ β FriendGraph ) β (Β¬
(β―βπ) = 0
β (Β¬ (β―βπ) = 1 β (Β¬ (β―βπ) = 3 β (πΊ RegUSGraph πΎ β ((β―βπ) = 0 β¨ (β―βπ) = 1 β¨ (β―βπ) = 3)))))) |
123 | 122 | com25 99 |
. . . . . . . . 9
β’
(((β―βπ)
β β0 β§ π β Fin β§ πΊ β FriendGraph ) β (πΊ RegUSGraph πΎ β (Β¬ (β―βπ) = 1 β (Β¬
(β―βπ) = 3
β (Β¬ (β―βπ) = 0 β ((β―βπ) = 0 β¨ (β―βπ) = 1 β¨ (β―βπ) = 3)))))) |
124 | 123 | imp 407 |
. . . . . . . 8
β’
((((β―βπ)
β β0 β§ π β Fin β§ πΊ β FriendGraph ) β§ πΊ RegUSGraph πΎ) β (Β¬ (β―βπ) = 1 β (Β¬
(β―βπ) = 3
β (Β¬ (β―βπ) = 0 β ((β―βπ) = 0 β¨ (β―βπ) = 1 β¨ (β―βπ) = 3))))) |
125 | 124 | com14 96 |
. . . . . . 7
β’ (Β¬
(β―βπ) = 0
β (Β¬ (β―βπ) = 1 β (Β¬ (β―βπ) = 3 β
((((β―βπ) β
β0 β§ π
β Fin β§ πΊ β
FriendGraph ) β§ πΊ
RegUSGraph πΎ) β
((β―βπ) = 0 β¨
(β―βπ) = 1 β¨
(β―βπ) =
3))))) |
126 | 125 | 3imp 1111 |
. . . . . 6
β’ ((Β¬
(β―βπ) = 0 β§
Β¬ (β―βπ) = 1
β§ Β¬ (β―βπ) = 3) β ((((β―βπ) β β0
β§ π β Fin β§
πΊ β FriendGraph )
β§ πΊ RegUSGraph πΎ) β ((β―βπ) = 0 β¨ (β―βπ) = 1 β¨ (β―βπ) = 3))) |
127 | 3, 126 | sylbi 216 |
. . . . 5
β’ (Β¬
((β―βπ) = 0 β¨
(β―βπ) = 1 β¨
(β―βπ) = 3)
β ((((β―βπ)
β β0 β§ π β Fin β§ πΊ β FriendGraph ) β§ πΊ RegUSGraph πΎ) β ((β―βπ) = 0 β¨ (β―βπ) = 1 β¨ (β―βπ) = 3))) |
128 | 2, 127 | pm2.61i 182 |
. . . 4
β’
((((β―βπ)
β β0 β§ π β Fin β§ πΊ β FriendGraph ) β§ πΊ RegUSGraph πΎ) β ((β―βπ) = 0 β¨ (β―βπ) = 1 β¨ (β―βπ) = 3)) |
129 | 128 | 3exp1 1352 |
. . 3
β’
((β―βπ)
β β0 β (π β Fin β (πΊ β FriendGraph β (πΊ RegUSGraph πΎ β ((β―βπ) = 0 β¨ (β―βπ) = 1 β¨ (β―βπ) = 3))))) |
130 | 1, 129 | mpcom 38 |
. 2
β’ (π β Fin β (πΊ β FriendGraph β
(πΊ RegUSGraph πΎ β ((β―βπ) = 0 β¨ (β―βπ) = 1 β¨ (β―βπ) = 3)))) |
131 | 130 | 3imp21 1114 |
1
β’ ((πΊ β FriendGraph β§ π β Fin β§ πΊ RegUSGraph πΎ) β ((β―βπ) = 0 β¨ (β―βπ) = 1 β¨ (β―βπ) = 3)) |