Metamath Proof Explorer


Table of Contents - 6.1. Elementary properties of divisibility

  1. Irrationality of square root of 2
    1. sqrt2irrlem
    2. sqrt2irr
    3. sqrt2re
    4. sqrt2irr0
  2. Some Number sets are chains of proper subsets
    1. nthruc
    2. nthruz
  3. The divides relation
    1. cdvds
    2. df-dvds
    3. divides
    4. dvdsval2
    5. dvdsval3
    6. dvdszrcl
    7. dvdsmod0
    8. p1modz1
    9. dvdsmodexp
    10. nndivdvds
    11. nndivides
    12. moddvds
    13. modm1div
    14. dvds0lem
    15. dvds1lem
    16. dvds2lem
    17. iddvds
    18. 1dvds
    19. dvds0
    20. negdvdsb
    21. dvdsnegb
    22. absdvdsb
    23. dvdsabsb
    24. 0dvds
    25. dvdsmul1
    26. dvdsmul2
    27. iddvdsexp
    28. muldvds1
    29. muldvds2
    30. dvdscmul
    31. dvdsmulc
    32. dvdscmulr
    33. dvdsmulcr
    34. summodnegmod
    35. modmulconst
    36. dvds2ln
    37. dvds2add
    38. dvds2sub
    39. dvds2addd
    40. dvds2subd
    41. dvdstr
    42. dvdstrd
    43. dvdsmultr1
    44. dvdsmultr1d
    45. dvdsmultr2
    46. dvdsmultr2d
    47. ordvdsmul
    48. dvdssub2
    49. dvdsadd
    50. dvdsaddr
    51. dvdssub
    52. dvdssubr
    53. dvdsadd2b
    54. dvdsaddre2b
    55. fsumdvds
    56. dvdslelem
    57. dvdsle
    58. dvdsleabs
    59. dvdsleabs2
    60. dvdsabseq
    61. dvdseq
    62. divconjdvds
    63. dvdsdivcl
    64. dvdsflip
    65. dvdsssfz1
    66. dvds1
    67. alzdvds
    68. dvdsext
    69. fzm1ndvds
    70. fzo0dvdseq
    71. fzocongeq
    72. addmodlteqALT
    73. dvdsfac
    74. dvdsexp2im
    75. dvdsexp
    76. dvdsmod
    77. mulmoddvds
    78. 3dvds
    79. 3dvdsdec
    80. 3dvds2dec
    81. fprodfvdvdsd
    82. fproddvdsd
  4. Even and odd numbers
    1. evenelz
    2. zeo3
    3. zeo4
    4. zeneo
    5. odd2np1lem
    6. odd2np1
    7. even2n
    8. oddm1even
    9. oddp1even
    10. oexpneg
    11. mod2eq0even
    12. mod2eq1n2dvds
    13. oddnn02np1
    14. oddge22np1
    15. evennn02n
    16. evennn2n
    17. 2tp1odd
    18. mulsucdiv2z
    19. sqoddm1div8z
    20. 2teven
    21. zeo5
    22. evend2
    23. oddp1d2
    24. zob
    25. oddm1d2
    26. ltoddhalfle
    27. halfleoddlt
    28. opoe
    29. omoe
    30. opeo
    31. omeo
    32. z0even
    33. n2dvds1
    34. n2dvdsm1
    35. z2even
    36. n2dvds3
    37. z4even
    38. 4dvdseven
    39. m1expe
    40. m1expo
    41. m1exp1
    42. nn0enne
    43. nn0ehalf
    44. nnehalf
    45. nn0onn
    46. nn0o1gt2
    47. nno
    48. nn0o
    49. nn0ob
    50. nn0oddm1d2
    51. nnoddm1d2
    52. sumeven
    53. sumodd
    54. evensumodd
    55. oddsumodd
    56. pwp1fsum
    57. oddpwp1fsum
  5. The division algorithm
    1. divalglem0
    2. divalglem1
    3. divalglem2
    4. divalglem4
    5. divalglem5
    6. divalglem6
    7. divalglem7
    8. divalglem8
    9. divalglem9
    10. divalglem10
    11. divalg
    12. divalgb
    13. divalg2
    14. divalgmod
    15. divalgmodcl
    16. modremain
    17. ndvdssub
    18. ndvdsadd
    19. ndvdsp1
    20. ndvdsi
    21. flodddiv4
    22. fldivndvdslt
    23. flodddiv4lt
    24. flodddiv4t2lthalf
  6. Bit sequences
    1. cbits
    2. csad
    3. csmu
    4. df-bits
    5. bitsfval
    6. bitsval
    7. bitsval2
    8. bitsss
    9. bitsf
    10. bits0
    11. bits0e
    12. bits0o
    13. bitsp1
    14. bitsp1e
    15. bitsp1o
    16. bitsfzolem
    17. bitsfzo
    18. bitsmod
    19. bitsfi
    20. bitscmp
    21. 0bits
    22. m1bits
    23. bitsinv1lem
    24. bitsinv1
    25. bitsinv2
    26. bitsf1ocnv
    27. bitsf1o
    28. bitsf1
    29. 2ebits
    30. bitsinv
    31. bitsinvp1
    32. sadadd2lem2
    33. df-sad
    34. sadfval
    35. sadcf
    36. sadc0
    37. sadcp1
    38. sadval
    39. sadcaddlem
    40. sadcadd
    41. sadadd2lem
    42. sadadd2
    43. sadadd3
    44. sadcl
    45. sadcom
    46. saddisjlem
    47. saddisj
    48. sadaddlem
    49. sadadd
    50. sadid1
    51. sadid2
    52. sadasslem
    53. sadass
    54. sadeq
    55. bitsres
    56. bitsuz
    57. bitsshft
    58. df-smu
    59. smufval
    60. smupf
    61. smup0
    62. smupp1
    63. smuval
    64. smuval2
    65. smupvallem
    66. smucl
    67. smu01lem
    68. smu01
    69. smu02
    70. smupval
    71. smup1
    72. smueqlem
    73. smueq
    74. smumullem
    75. smumul
  7. The greatest common divisor operator
    1. cgcd
    2. df-gcd
    3. gcdval
    4. gcd0val
    5. gcdn0val
    6. gcdcllem1
    7. gcdcllem2
    8. gcdcllem3
    9. gcdn0cl
    10. gcddvds
    11. dvdslegcd
    12. nndvdslegcd
    13. gcdcl
    14. gcdnncl
    15. gcdcld
    16. gcd2n0cl
    17. zeqzmulgcd
    18. divgcdz
    19. gcdf
    20. gcdcom
    21. gcdcomd
    22. divgcdnn
    23. divgcdnnr
    24. gcdeq0
    25. gcdn0gt0
    26. gcd0id
    27. gcdid0
    28. nn0gcdid0
    29. gcdneg
    30. neggcd
    31. gcdaddmlem
    32. gcdaddm
    33. gcdadd
    34. gcdid
    35. gcd1
    36. gcdabs1
    37. gcdabs2
    38. gcdabs
    39. gcdabsOLD
    40. modgcd
    41. 1gcd
    42. gcdmultipled
    43. gcdmultiplez
    44. gcdmultiple
    45. dvdsgcdidd
    46. 6gcd4e2
  8. Bézout's identity
    1. bezoutlem1
    2. bezoutlem2
    3. bezoutlem3
    4. bezoutlem4
    5. bezout
    6. dvdsgcd
    7. dvdsgcdb
    8. dfgcd2
    9. gcdass
    10. mulgcd
    11. absmulgcd
    12. mulgcdr
    13. gcddiv
    14. gcdmultipleOLD
    15. gcdmultiplezOLD
    16. gcdzeq
    17. gcdeq
    18. dvdssqim
    19. dvdsmulgcd
    20. rpmulgcd
    21. rplpwr
    22. rprpwr
    23. rppwr
    24. sqgcd
    25. dvdssqlem
    26. dvdssq
    27. bezoutr
    28. bezoutr1
  9. Algorithms
    1. nn0seqcvgd
    2. seq1st
    3. algr0
    4. algrf
    5. algrp1
    6. alginv
    7. algcvg
    8. algcvgblem
    9. algcvgb
    10. algcvga
    11. algfx
  10. Euclid's Algorithm
    1. eucalgval2
    2. eucalgval
    3. eucalgf
    4. eucalginv
    5. eucalglt
    6. eucalgcvga
    7. eucalg
  11. The least common multiple
    1. clcm
    2. clcmf
    3. df-lcm
    4. df-lcmf
    5. lcmval
    6. lcmcom
    7. lcm0val
    8. lcmn0val
    9. lcmcllem
    10. lcmn0cl
    11. dvdslcm
    12. lcmledvds
    13. lcmeq0
    14. lcmcl
    15. gcddvdslcm
    16. lcmneg
    17. neglcm
    18. lcmabs
    19. lcmgcdlem
    20. lcmgcd
    21. lcmdvds
    22. lcmid
    23. lcm1
    24. lcmgcdnn
    25. lcmgcdeq
    26. lcmdvdsb
    27. lcmass
    28. 3lcm2e6woprm
    29. 6lcm4e12
    30. absproddvds
    31. absprodnn
    32. fissn0dvds
    33. fissn0dvdsn0
    34. lcmfval
    35. lcmf0val
    36. lcmfn0val
    37. lcmfnnval
    38. lcmfcllem
    39. lcmfn0cl
    40. lcmfpr
    41. lcmfcl
    42. lcmfnncl
    43. lcmfeq0b
    44. dvdslcmf
    45. lcmfledvds
    46. lcmf
    47. lcmf0
    48. lcmfsn
    49. lcmftp
    50. lcmfunsnlem1
    51. lcmfunsnlem2lem1
    52. lcmfunsnlem2lem2
    53. lcmfunsnlem2
    54. lcmfunsnlem
    55. lcmfdvds
    56. lcmfdvdsb
    57. lcmfunsn
    58. lcmfun
    59. lcmfass
    60. lcmf2a3a4e12
    61. lcmflefac
  12. Coprimality and Euclid's lemma
    1. coprmgcdb
    2. ncoprmgcdne1b
    3. ncoprmgcdgt1b
    4. coprmdvds1
    5. coprmdvds
    6. coprmdvds2
    7. mulgcddvds
    8. rpmulgcd2
    9. qredeq
    10. qredeu
    11. rpmul
    12. rpdvds
    13. coprmprod
    14. coprmproddvdslem
    15. coprmproddvds
  13. Cancellability of congruences
    1. congr
    2. divgcdcoprm0
    3. divgcdcoprmex
    4. cncongr1
    5. cncongr2
    6. cncongr
    7. cncongrcoprm