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