Step | Hyp | Ref
| Expression |
1 | | ax-1 6 |
. . 3
⢠(ð â (ðº NeighbVtx ð) â ((ð â ð ⧠ð â ð) â ð â (ðº NeighbVtx ð))) |
2 | 1 | 2a1d 26 |
. 2
⢠(ð â (ðº NeighbVtx ð) â ((ðº â FinUSGraph ⧠ð â ð) â ((â¯â(ðº NeighbVtx ð)) = ((â¯âð) â 1) â ((ð â ð ⧠ð â ð) â ð â (ðº NeighbVtx ð))))) |
3 | | simpr 486 |
. . . . . . . 8
⢠((¬
ð â (ðº NeighbVtx ð) ⧠(ðº â FinUSGraph ⧠ð â ð)) â (ðº â FinUSGraph ⧠ð â ð)) |
4 | 3 | adantr 482 |
. . . . . . 7
⢠(((¬
ð â (ðº NeighbVtx ð) ⧠(ðº â FinUSGraph ⧠ð â ð)) ⧠(ð â ð ⧠ð â ð)) â (ðº â FinUSGraph ⧠ð â ð)) |
5 | | simprl 770 |
. . . . . . 7
⢠(((¬
ð â (ðº NeighbVtx ð) ⧠(ðº â FinUSGraph ⧠ð â ð)) ⧠(ð â ð ⧠ð â ð)) â ð â ð) |
6 | | simpr 486 |
. . . . . . . 8
⢠((ð â ð ⧠ð â ð) â ð â ð) |
7 | 6 | adantl 483 |
. . . . . . 7
⢠(((¬
ð â (ðº NeighbVtx ð) ⧠(ðº â FinUSGraph ⧠ð â ð)) ⧠(ð â ð ⧠ð â ð)) â ð â ð) |
8 | | df-nel 3047 |
. . . . . . . . . 10
⢠(ð â (ðº NeighbVtx ð) â ¬ ð â (ðº NeighbVtx ð)) |
9 | 8 | biimpri 227 |
. . . . . . . . 9
⢠(¬
ð â (ðº NeighbVtx ð) â ð â (ðº NeighbVtx ð)) |
10 | 9 | adantr 482 |
. . . . . . . 8
⢠((¬
ð â (ðº NeighbVtx ð) ⧠(ðº â FinUSGraph ⧠ð â ð)) â ð â (ðº NeighbVtx ð)) |
11 | 10 | adantr 482 |
. . . . . . 7
⢠(((¬
ð â (ðº NeighbVtx ð) ⧠(ðº â FinUSGraph ⧠ð â ð)) ⧠(ð â ð ⧠ð â ð)) â ð â (ðº NeighbVtx ð)) |
12 | | hashnbusgrnn0.v |
. . . . . . . 8
⢠ð = (Vtxâðº) |
13 | 12 | nbfusgrlevtxm2 28368 |
. . . . . . 7
⢠(((ðº â FinUSGraph ⧠ð â ð) ⧠(ð â ð ⧠ð â ð ⧠ð â (ðº NeighbVtx ð))) â (â¯â(ðº NeighbVtx ð)) †((â¯âð) â 2)) |
14 | 4, 5, 7, 11, 13 | syl13anc 1373 |
. . . . . 6
⢠(((¬
ð â (ðº NeighbVtx ð) ⧠(ðº â FinUSGraph ⧠ð â ð)) ⧠(ð â ð ⧠ð â ð)) â (â¯â(ðº NeighbVtx ð)) †((â¯âð) â 2)) |
15 | | breq1 5109 |
. . . . . . . . 9
â¢
((â¯â(ðº
NeighbVtx ð)) =
((â¯âð) â
1) â ((â¯â(ðº NeighbVtx ð)) †((â¯âð) â 2) â ((â¯âð) â 1) â€
((â¯âð) â
2))) |
16 | 15 | adantl 483 |
. . . . . . . 8
⢠((((¬
ð â (ðº NeighbVtx ð) ⧠(ðº â FinUSGraph ⧠ð â ð)) ⧠(ð â ð ⧠ð â ð)) ⧠(â¯â(ðº NeighbVtx ð)) = ((â¯âð) â 1)) â ((â¯â(ðº NeighbVtx ð)) †((â¯âð) â 2) â ((â¯âð) â 1) â€
((â¯âð) â
2))) |
17 | 12 | fusgrvtxfi 28309 |
. . . . . . . . . . . 12
⢠(ðº â FinUSGraph â ð â Fin) |
18 | | hashcl 14262 |
. . . . . . . . . . . 12
⢠(ð â Fin â
(â¯âð) â
â0) |
19 | | nn0re 12427 |
. . . . . . . . . . . . 13
â¢
((â¯âð)
â â0 â (â¯âð) â â) |
20 | | 1red 11161 |
. . . . . . . . . . . . . . 15
â¢
((â¯âð)
â â â 1 â â) |
21 | | 2re 12232 |
. . . . . . . . . . . . . . . 16
⢠2 â
â |
22 | 21 | a1i 11 |
. . . . . . . . . . . . . . 15
â¢
((â¯âð)
â â â 2 â â) |
23 | | id 22 |
. . . . . . . . . . . . . . 15
â¢
((â¯âð)
â â â (â¯âð) â â) |
24 | | 1lt2 12329 |
. . . . . . . . . . . . . . . 16
⢠1 <
2 |
25 | 24 | a1i 11 |
. . . . . . . . . . . . . . 15
â¢
((â¯âð)
â â â 1 < 2) |
26 | 20, 22, 23, 25 | ltsub2dd 11773 |
. . . . . . . . . . . . . 14
â¢
((â¯âð)
â â â ((â¯âð) â 2) < ((â¯âð) â 1)) |
27 | 23, 22 | resubcld 11588 |
. . . . . . . . . . . . . . 15
â¢
((â¯âð)
â â â ((â¯âð) â 2) â
â) |
28 | | peano2rem 11473 |
. . . . . . . . . . . . . . 15
â¢
((â¯âð)
â â â ((â¯âð) â 1) â
â) |
29 | 27, 28 | ltnled 11307 |
. . . . . . . . . . . . . 14
â¢
((â¯âð)
â â â (((â¯âð) â 2) < ((â¯âð) â 1) â ¬
((â¯âð) â
1) †((â¯âð)
â 2))) |
30 | 26, 29 | mpbid 231 |
. . . . . . . . . . . . 13
â¢
((â¯âð)
â â â ¬ ((â¯âð) â 1) †((â¯âð) â 2)) |
31 | 19, 30 | syl 17 |
. . . . . . . . . . . 12
â¢
((â¯âð)
â â0 â ¬ ((â¯âð) â 1) †((â¯âð) â 2)) |
32 | 17, 18, 31 | 3syl 18 |
. . . . . . . . . . 11
⢠(ðº â FinUSGraph â ¬
((â¯âð) â
1) †((â¯âð)
â 2)) |
33 | 32 | pm2.21d 121 |
. . . . . . . . . 10
⢠(ðº â FinUSGraph â
(((â¯âð) â
1) †((â¯âð)
â 2) â ð â
(ðº NeighbVtx ð))) |
34 | 33 | adantr 482 |
. . . . . . . . 9
⢠((ðº â FinUSGraph ⧠ð â ð) â (((â¯âð) â 1) †((â¯âð) â 2) â ð â (ðº NeighbVtx ð))) |
35 | 34 | ad3antlr 730 |
. . . . . . . 8
⢠((((¬
ð â (ðº NeighbVtx ð) ⧠(ðº â FinUSGraph ⧠ð â ð)) ⧠(ð â ð ⧠ð â ð)) ⧠(â¯â(ðº NeighbVtx ð)) = ((â¯âð) â 1)) â (((â¯âð) â 1) â€
((â¯âð) â
2) â ð â (ðº NeighbVtx ð))) |
36 | 16, 35 | sylbid 239 |
. . . . . . 7
⢠((((¬
ð â (ðº NeighbVtx ð) ⧠(ðº â FinUSGraph ⧠ð â ð)) ⧠(ð â ð ⧠ð â ð)) ⧠(â¯â(ðº NeighbVtx ð)) = ((â¯âð) â 1)) â ((â¯â(ðº NeighbVtx ð)) †((â¯âð) â 2) â ð â (ðº NeighbVtx ð))) |
37 | 36 | ex 414 |
. . . . . 6
⢠(((¬
ð â (ðº NeighbVtx ð) ⧠(ðº â FinUSGraph ⧠ð â ð)) ⧠(ð â ð ⧠ð â ð)) â ((â¯â(ðº NeighbVtx ð)) = ((â¯âð) â 1) â ((â¯â(ðº NeighbVtx ð)) †((â¯âð) â 2) â ð â (ðº NeighbVtx ð)))) |
38 | 14, 37 | mpid 44 |
. . . . 5
⢠(((¬
ð â (ðº NeighbVtx ð) ⧠(ðº â FinUSGraph ⧠ð â ð)) ⧠(ð â ð ⧠ð â ð)) â ((â¯â(ðº NeighbVtx ð)) = ((â¯âð) â 1) â ð â (ðº NeighbVtx ð))) |
39 | 38 | ex 414 |
. . . 4
⢠((¬
ð â (ðº NeighbVtx ð) ⧠(ðº â FinUSGraph ⧠ð â ð)) â ((ð â ð ⧠ð â ð) â ((â¯â(ðº NeighbVtx ð)) = ((â¯âð) â 1) â ð â (ðº NeighbVtx ð)))) |
40 | 39 | com23 86 |
. . 3
⢠((¬
ð â (ðº NeighbVtx ð) ⧠(ðº â FinUSGraph ⧠ð â ð)) â ((â¯â(ðº NeighbVtx ð)) = ((â¯âð) â 1) â ((ð â ð ⧠ð â ð) â ð â (ðº NeighbVtx ð)))) |
41 | 40 | ex 414 |
. 2
⢠(¬
ð â (ðº NeighbVtx ð) â ((ðº â FinUSGraph ⧠ð â ð) â ((â¯â(ðº NeighbVtx ð)) = ((â¯âð) â 1) â ((ð â ð ⧠ð â ð) â ð â (ðº NeighbVtx ð))))) |
42 | 2, 41 | pm2.61i 182 |
1
⢠((ðº â FinUSGraph ⧠ð â ð) â ((â¯â(ðº NeighbVtx ð)) = ((â¯âð) â 1) â ((ð â ð ⧠ð â ð) â ð â (ðº NeighbVtx ð)))) |