Metamath Proof Explorer

Table of Contents - 16.5.4. Huneke's Proof of the Friendship Theorem

In this section, the friendship theorem friendship is proven by formalizing Huneke's proof, see [Huneke] pp. 1-2. The three claims (see frgrncvvdeq, frgrregorufr and frrusgrord0) and additional statements (numbered in the order of their occurrence in the paper) in Huneke's proof are cited in the corresponding theorems.

  1. frgrncvvdeqlem1
  2. frgrncvvdeqlem2
  3. frgrncvvdeqlem3
  4. frgrncvvdeqlem4
  5. frgrncvvdeqlem5
  6. frgrncvvdeqlem6
  7. frgrncvvdeqlem7
  8. frgrncvvdeqlem8
  9. frgrncvvdeqlem9
  10. frgrncvvdeqlem10
  11. frgrncvvdeq
  12. frgrwopreglem4a
  13. frgrwopreglem5a
  14. frgrwopreglem1
  15. frgrwopreglem2
  16. frgrwopreglem3
  17. frgrwopreglem4
  18. frgrwopregasn
  19. frgrwopregbsn
  20. frgrwopreg1
  21. frgrwopreg2
  22. frgrwopreglem5lem
  23. frgrwopreglem5
  24. frgrwopreglem5ALT
  25. frgrwopreg
  26. frgrregorufr0
  27. frgrregorufr
  28. frgrregorufrg
  29. frgr2wwlkeu
  30. frgr2wwlkn0
  31. frgr2wwlk1
  32. frgr2wsp1
  33. frgr2wwlkeqm
  34. frgrhash2wsp
  35. fusgreg2wsplem
  36. fusgr2wsp2nb
  37. fusgreghash2wspv
  38. fusgreg2wsp
  39. 2wspmdisj
  40. fusgreghash2wsp
  41. frrusgrord0lem
  42. frrusgrord0
  43. frrusgrord
  44. numclwwlk2lem1lem
  45. 2clwwlklem
  46. clwwnrepclwwn
  47. clwwnonrepclwwnon
  48. 2clwwlk2clwwlklem
  49. 2clwwlk
  50. 2clwwlk2
  51. 2clwwlkel
  52. 2clwwlk2clwwlk
  53. numclwwlk1lem2foalem
  54. extwwlkfab
  55. extwwlkfabel
  56. numclwwlk1lem2foa
  57. numclwwlk1lem2f
  58. numclwwlk1lem2fv
  59. numclwwlk1lem2f1
  60. numclwwlk1lem2fo
  61. numclwwlk1lem2f1o
  62. numclwwlk1lem2
  63. numclwwlk1
  64. clwwlknonclwlknonf1o
  65. clwwlknonclwlknonen
  66. dlwwlknondlwlknonf1olem1
  67. dlwwlknondlwlknonf1o
  68. dlwwlknondlwlknonen
  69. wlkl0
  70. clwlknon2num
  71. numclwlk1lem1
  72. numclwlk1lem2
  73. numclwlk1
  74. numclwwlkovh0
  75. numclwwlkovh
  76. numclwwlkovq
  77. numclwwlkqhash
  78. numclwwlk2lem1
  79. numclwlk2lem2f
  80. numclwlk2lem2fv
  81. numclwlk2lem2f1o
  82. numclwwlk2lem3
  83. numclwwlk2
  84. numclwwlk3lem1
  85. numclwwlk3lem2lem
  86. numclwwlk3lem2
  87. numclwwlk3
  88. numclwwlk4
  89. numclwwlk5lem
  90. numclwwlk5
  91. numclwwlk7lem
  92. numclwwlk6
  93. numclwwlk7
  94. numclwwlk8
  95. frgrreggt1
  96. frgrreg
  97. frgrregord013
  98. frgrregord13
  99. frgrogt3nreg
  100. friendshipgt3
  101. friendship