Step | Hyp | Ref
| Expression |
1 | | simp1 1137 |
. . . . . . . 8
⢠((ðº â FriendGraph ⧠ð â Fin ⧠3 <
(â¯âð)) â
ðº â FriendGraph
) |
2 | | simp2 1138 |
. . . . . . . 8
⢠((ðº â FriendGraph ⧠ð â Fin ⧠3 <
(â¯âð)) â
ð â
Fin) |
3 | | hashcl 14263 |
. . . . . . . . . . 11
⢠(ð â Fin â
(â¯âð) â
â0) |
4 | | 0red 11165 |
. . . . . . . . . . . . . 14
â¢
((â¯âð)
â â0 â 0 â â) |
5 | | 3re 12240 |
. . . . . . . . . . . . . . . . . . 19
⢠3 â
â |
6 | 5 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
â¢
((â¯âð)
â â0 â 3 â â) |
7 | | nn0re 12429 |
. . . . . . . . . . . . . . . . . 18
â¢
((â¯âð)
â â0 â (â¯âð) â â) |
8 | 4, 6, 7 | 3jca 1129 |
. . . . . . . . . . . . . . . . 17
â¢
((â¯âð)
â â0 â (0 â â ⧠3 â â
⧠(â¯âð)
â â)) |
9 | 8 | adantr 482 |
. . . . . . . . . . . . . . . 16
â¢
(((â¯âð)
â â0 ⧠3 < (â¯âð)) â (0 â â ⧠3 â
â ⧠(â¯âð) â â)) |
10 | | 3pos 12265 |
. . . . . . . . . . . . . . . . 17
⢠0 <
3 |
11 | 10 | a1i 11 |
. . . . . . . . . . . . . . . 16
â¢
(((â¯âð)
â â0 ⧠3 < (â¯âð)) â 0 < 3) |
12 | | simpr 486 |
. . . . . . . . . . . . . . . 16
â¢
(((â¯âð)
â â0 ⧠3 < (â¯âð)) â 3 < (â¯âð)) |
13 | | lttr 11238 |
. . . . . . . . . . . . . . . . 17
⢠((0
â â ⧠3 â â ⧠(â¯âð) â â) â ((0 < 3 ⧠3
< (â¯âð))
â 0 < (â¯âð))) |
14 | 13 | imp 408 |
. . . . . . . . . . . . . . . 16
⢠(((0
â â ⧠3 â â ⧠(â¯âð) â â) ⧠(0 < 3 ⧠3
< (â¯âð)))
â 0 < (â¯âð)) |
15 | 9, 11, 12, 14 | syl12anc 836 |
. . . . . . . . . . . . . . 15
â¢
(((â¯âð)
â â0 ⧠3 < (â¯âð)) â 0 < (â¯âð)) |
16 | 15 | ex 414 |
. . . . . . . . . . . . . 14
â¢
((â¯âð)
â â0 â (3 < (â¯âð) â 0 < (â¯âð))) |
17 | | ltne 11259 |
. . . . . . . . . . . . . 14
⢠((0
â â ⧠0 < (â¯âð)) â (â¯âð) â 0) |
18 | 4, 16, 17 | syl6an 683 |
. . . . . . . . . . . . 13
â¢
((â¯âð)
â â0 â (3 < (â¯âð) â (â¯âð) â 0)) |
19 | | hasheq0 14270 |
. . . . . . . . . . . . . . 15
⢠(ð â Fin â
((â¯âð) = 0
â ð =
â
)) |
20 | 19 | necon3bid 2989 |
. . . . . . . . . . . . . 14
⢠(ð â Fin â
((â¯âð) â 0
â ð â
â
)) |
21 | 20 | biimpcd 249 |
. . . . . . . . . . . . 13
â¢
((â¯âð)
â 0 â (ð â Fin
â ð â
â
)) |
22 | 18, 21 | syl6 35 |
. . . . . . . . . . . 12
â¢
((â¯âð)
â â0 â (3 < (â¯âð) â (ð â Fin â ð â â
))) |
23 | 22 | com23 86 |
. . . . . . . . . . 11
â¢
((â¯âð)
â â0 â (ð â Fin â (3 <
(â¯âð) â
ð â
â
))) |
24 | 3, 23 | mpcom 38 |
. . . . . . . . . 10
⢠(ð â Fin â (3 <
(â¯âð) â
ð â
â
)) |
25 | 24 | a1i 11 |
. . . . . . . . 9
⢠(ðº â FriendGraph â
(ð â Fin â (3
< (â¯âð)
â ð â
â
))) |
26 | 25 | 3imp 1112 |
. . . . . . . 8
⢠((ðº â FriendGraph ⧠ð â Fin ⧠3 <
(â¯âð)) â
ð â
â
) |
27 | 1, 2, 26 | 3jca 1129 |
. . . . . . 7
⢠((ðº â FriendGraph ⧠ð â Fin ⧠3 <
(â¯âð)) â
(ðº â FriendGraph â§
ð â Fin ⧠ð â â
)) |
28 | 27 | ad2antrl 727 |
. . . . . 6
⢠((ðº RegUSGraph ð ⧠((ðº â FriendGraph ⧠ð â Fin ⧠3 <
(â¯âð)) â§
ð â
â0)) â (ðº â FriendGraph ⧠ð â Fin ⧠ð â â
)) |
29 | | simpl 484 |
. . . . . 6
⢠((ðº RegUSGraph ð ⧠((ðº â FriendGraph ⧠ð â Fin ⧠3 <
(â¯âð)) â§
ð â
â0)) â ðº RegUSGraph ð) |
30 | | frgrreggt1.v |
. . . . . . 7
⢠ð = (Vtxâðº) |
31 | 30 | frgrregord13 29382 |
. . . . . 6
⢠(((ðº â FriendGraph ⧠ð â Fin ⧠ð â â
) ⧠ðº RegUSGraph ð) â ((â¯âð) = 1 âš (â¯âð) = 3)) |
32 | 28, 29, 31 | syl2anc 585 |
. . . . 5
⢠((ðº RegUSGraph ð ⧠((ðº â FriendGraph ⧠ð â Fin ⧠3 <
(â¯âð)) â§
ð â
â0)) â ((â¯âð) = 1 âš (â¯âð) = 3)) |
33 | | 1red 11163 |
. . . . . . . . . . . . 13
â¢
(((â¯âð)
â â0 ⧠3 < (â¯âð)) â 1 â â) |
34 | 5 | a1i 11 |
. . . . . . . . . . . . . 14
â¢
(((â¯âð)
â â0 ⧠3 < (â¯âð)) â 3 â â) |
35 | 7 | adantr 482 |
. . . . . . . . . . . . . 14
â¢
(((â¯âð)
â â0 ⧠3 < (â¯âð)) â (â¯âð) â â) |
36 | | 1lt3 12333 |
. . . . . . . . . . . . . . 15
⢠1 <
3 |
37 | 36 | a1i 11 |
. . . . . . . . . . . . . 14
â¢
(((â¯âð)
â â0 ⧠3 < (â¯âð)) â 1 < 3) |
38 | 33, 34, 35, 37, 12 | lttrd 11323 |
. . . . . . . . . . . . 13
â¢
(((â¯âð)
â â0 ⧠3 < (â¯âð)) â 1 < (â¯âð)) |
39 | 33, 38 | gtned 11297 |
. . . . . . . . . . . 12
â¢
(((â¯âð)
â â0 ⧠3 < (â¯âð)) â (â¯âð) â 1) |
40 | | eqneqall 2955 |
. . . . . . . . . . . 12
â¢
((â¯âð) =
1 â ((â¯âð)
â 1 â ¬ ðº
RegUSGraph ð)) |
41 | 39, 40 | syl5com 31 |
. . . . . . . . . . 11
â¢
(((â¯âð)
â â0 ⧠3 < (â¯âð)) â ((â¯âð) = 1 â ¬ ðº RegUSGraph ð)) |
42 | | ltne 11259 |
. . . . . . . . . . . . 13
⢠((3
â â ⧠3 < (â¯âð)) â (â¯âð) â 3) |
43 | 6, 42 | sylan 581 |
. . . . . . . . . . . 12
â¢
(((â¯âð)
â â0 ⧠3 < (â¯âð)) â (â¯âð) â 3) |
44 | | eqneqall 2955 |
. . . . . . . . . . . 12
â¢
((â¯âð) =
3 â ((â¯âð)
â 3 â ¬ ðº
RegUSGraph ð)) |
45 | 43, 44 | syl5com 31 |
. . . . . . . . . . 11
â¢
(((â¯âð)
â â0 ⧠3 < (â¯âð)) â ((â¯âð) = 3 â ¬ ðº RegUSGraph ð)) |
46 | 41, 45 | jaod 858 |
. . . . . . . . . 10
â¢
(((â¯âð)
â â0 ⧠3 < (â¯âð)) â (((â¯âð) = 1 âš (â¯âð) = 3) â ¬ ðº RegUSGraph ð)) |
47 | 46 | ex 414 |
. . . . . . . . 9
â¢
((â¯âð)
â â0 â (3 < (â¯âð) â (((â¯âð) = 1 âš (â¯âð) = 3) â ¬ ðº RegUSGraph ð))) |
48 | 3, 47 | syl 17 |
. . . . . . . 8
⢠(ð â Fin â (3 <
(â¯âð) â
(((â¯âð) = 1
âš (â¯âð) = 3)
â ¬ ðº RegUSGraph
ð))) |
49 | 48 | a1i 11 |
. . . . . . 7
⢠(ðº â FriendGraph â
(ð â Fin â (3
< (â¯âð)
â (((â¯âð)
= 1 âš (â¯âð)
= 3) â ¬ ðº
RegUSGraph ð)))) |
50 | 49 | 3imp 1112 |
. . . . . 6
⢠((ðº â FriendGraph ⧠ð â Fin ⧠3 <
(â¯âð)) â
(((â¯âð) = 1
âš (â¯âð) = 3)
â ¬ ðº RegUSGraph
ð)) |
51 | 50 | ad2antrl 727 |
. . . . 5
⢠((ðº RegUSGraph ð ⧠((ðº â FriendGraph ⧠ð â Fin ⧠3 <
(â¯âð)) â§
ð â
â0)) â (((â¯âð) = 1 âš (â¯âð) = 3) â ¬ ðº RegUSGraph ð)) |
52 | 32, 51 | mpd 15 |
. . . 4
⢠((ðº RegUSGraph ð ⧠((ðº â FriendGraph ⧠ð â Fin ⧠3 <
(â¯âð)) â§
ð â
â0)) â ¬ ðº RegUSGraph ð) |
53 | 52 | ex 414 |
. . 3
⢠(ðº RegUSGraph ð â (((ðº â FriendGraph ⧠ð â Fin ⧠3 <
(â¯âð)) â§
ð â
â0) â ¬ ðº RegUSGraph ð)) |
54 | | ax-1 6 |
. . 3
⢠(¬
ðº RegUSGraph ð â (((ðº â FriendGraph ⧠ð â Fin ⧠3 <
(â¯âð)) â§
ð â
â0) â ¬ ðº RegUSGraph ð)) |
55 | 53, 54 | pm2.61i 182 |
. 2
⢠(((ðº â FriendGraph ⧠ð â Fin ⧠3 <
(â¯âð)) â§
ð â
â0) â ¬ ðº RegUSGraph ð) |
56 | 55 | ralrimiva 3144 |
1
⢠((ðº â FriendGraph ⧠ð â Fin ⧠3 <
(â¯âð)) â
âð â
â0 ¬ ðº
RegUSGraph ð) |