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. addmulmodb
15. dvds0lem
16. dvds1lem
17. dvds2lem
18. iddvds
19. 1dvds
20. dvds0
21. negdvdsb
22. dvdsnegb
23. absdvdsb
24. dvdsabsb
25. 0dvds
26. dvdsmul1
27. dvdsmul2
28. iddvdsexp
29. muldvds1
30. muldvds2
31. dvdscmul
32. dvdsmulc
33. dvdscmulr
34. dvdsmulcr
35. summodnegmod
36. difmod0
37. modmulconst
38. dvds2ln
39. dvds2add
40. dvds2sub
41. dvds2addd
42. dvds2subd
43. dvdstr
44. dvdstrd
45. dvdsmultr1
46. dvdsmultr1d
47. dvdsmultr2
48. dvdsmultr2d
49. ordvdsmul
50. dvdssub2
51. dvdsadd
52. dvdsaddr
53. dvdssub
54. dvdssubr
55. dvdsadd2b
56. dvdsaddre2b
57. fsumdvds
58. dvdslelem
59. dvdsle
60. dvdsleabs
61. dvdsleabs2
62. dvdsabseq
63. dvdseq
64. divconjdvds
65. dvdsdivcl
66. dvdsflip
67. dvdsssfz1
68. dvds1
69. alzdvds
70. dvdsext
71. fzm1ndvds
72. fzo0dvdseq
73. fzocongeq
74. addmodlteqALT
75. dvdsfac
76. dvdsexp2im
77. dvdsexp
78. dvdsmod
79. mulmoddvds
80. 3dvds
81. 3dvdsdec
82. 3dvds2dec
83. fprodfvdvdsd
84. 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. 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
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. 5ndvds3
22. 5ndvds6
23. flodddiv4
24. fldivndvdslt
25. flodddiv4lt
26. 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. 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. modgcd
40. 1gcd
41. gcdmultipled
42. gcdmultiplez
43. gcdmultiple
44. dvdsgcdidd
45. 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. gcdzeq
15. gcdeq
16. dvdssqim
17. dvdsexpim
18. dvdsmulgcd
19. rpmulgcd
20. rplpwr
21. rprpwr
22. rppwr
23. nn0rppwr
24. sqgcd
25. expgcd
26. nn0expgcd
27. zexpgcd
28. dvdssqlem
29. dvdssq
30. bezoutr
31. 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