Metamath Proof Explorer

Table of Contents - 6.1. Elementary properties of divisibility

Irrationality of square root of 2
Some Number sets are chains of proper subsets
1. nthruc
2. nthruz
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. dvds2subd
40. dvdstr
41. dvdsmultr1
42. dvdsmultr1d
43. dvdsmultr2
44. ordvdsmul
45. dvdssub2
46. dvdsadd
47. dvdsaddr
48. dvdssub
49. dvdssubr
50. dvdsadd2b
51. dvdsaddre2b
52. fsumdvds
53. dvdslelem
54. dvdsle
55. dvdsleabs
56. dvdsleabs2
57. dvdsabseq
58. dvdseq
59. divconjdvds
60. dvdsdivcl
61. dvdsflip
62. dvdsssfz1
63. dvds1
64. alzdvds
65. dvdsext
66. fzm1ndvds
67. fzo0dvdseq
68. fzocongeq
69. addmodlteqALT
70. dvdsfac
71. dvdsexp
72. dvdsmod
73. mulmoddvds
74. 3dvds
75. 3dvdsdec
76. 3dvds2dec
77. fprodfvdvdsd
78. fproddvdsd
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. n2dvds1OLD
35. n2dvdsm1
36. z2even
37. n2dvds3
38. n2dvds3OLD
39. z4even
40. 4dvdseven
41. m1expe
42. m1expo
43. m1exp1
44. nn0enne
45. nn0ehalf
46. nnehalf
47. nn0onn
48. nn0o1gt2
49. nno
50. nn0o
51. nn0ob
52. nn0oddm1d2
53. nnoddm1d2
54. sumeven
55. sumodd
56. evensumodd
57. oddsumodd
58. pwp1fsum
59. oddpwp1fsum
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
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
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. divgcdnn
22. divgcdnnr
23. gcdeq0
24. gcdn0gt0
25. gcd0id
26. gcdid0
27. nn0gcdid0
28. gcdneg
29. neggcd
30. gcdaddmlem
31. gcdaddm
32. gcdadd
33. gcdid
34. gcd1
35. gcdabs
36. gcdabs1
37. gcdabs2
38. modgcd
39. 1gcd
40. gcdmultipled
41. gcdmultiplez
42. gcdmultiple
43. dvdsgcdidd
44. 6gcd4e2
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. rppwr
23. sqgcd
24. dvdssqlem
25. dvdssq
26. bezoutr
27. bezoutr1
Algorithms
1. nn0seqcvgd
2. seq1st
3. algr0
4. algrf
5. algrp1
6. alginv
7. algcvg
8. algcvgblem
9. algcvgb
10. algcvga
11. algfx
Euclid's Algorithm
1. eucalgval2
2. eucalgval
3. eucalgf
4. eucalginv
5. eucalglt
6. eucalgcvga
7. eucalg
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
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
Cancellability of congruences
1. congr
2. divgcdcoprm0
3. divgcdcoprmex
4. cncongr1
5. cncongr2
6. cncongr
7. cncongrcoprm