P. 119 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 11801-11900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	demoivreALT 11801	Alternate proof of demoivre 11800. It is longer but does not use the exponential function. This is Metamath 100 proof #17. (Contributed by Steve Rodriguez, 10-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ( A e. CC /\ N e. NN0 ) -> ( ( ( cos ` A ) + ( _i x. ( sin ` A ) ) ) ^ N ) = ( ( cos ` ( N x. A ) ) + ( _i x. ( sin ` ( N x. A ) ) ) ) )
4.9.1.1  The circle constant (tau = 2 pi)
Syntax	ctau 11802	Extend class notation to include the constant tau, tau = 6.28318....
class tau
Definition	df-tau 11803	Define the circle constant tau, tau = 6.28318..., which is the smallest positive real number whose cosine is one. Various notations have been used or proposed for this number including tau, a three-legged variant of pi, or 2 pi. Note the difference between this constant tau and the formula variable ta. Following our convention, the constant is displayed in upright font while the variable is in italic font; furthermore, the colors are different. (Contributed by Jim Kingdon, 9-Apr-2018.) (Revised by AV, 1-Oct-2020.)
|- tau = inf ( ( RR+ i^i ( `' cos " { 1 } ) ) , RR , < )
4.9.2  _e is irrational
Theorem	eirraplem 11804*	Lemma for eirrap 11805. (Contributed by Paul Chapman, 9-Feb-2008.) (Revised by Jim Kingdon, 5-Jan-2022.)
|- F = ( n e. NN0 |-> ( 1 / ( ! ` n ) ) )   &    |- ( ph -> P e. ZZ )   &    |- ( ph -> Q e. NN )   =>    |- ( ph -> _e # ( P / Q ) )
Theorem	eirrap 11805	_e is irrational. That is, for any rational number, _e is apart from it. In the absence of excluded middle, we can distinguish between this and saying that _e is not rational, which is eirr 11806. (Contributed by Jim Kingdon, 6-Jan-2023.)
|- ( Q e. QQ -> _e # Q )
Theorem	eirr 11806	_e is not rational. In the absence of excluded middle, we can distinguish between this and saying that _e is irrational in the sense of being apart from any rational number, which is eirrap 11805. (Contributed by Paul Chapman, 9-Feb-2008.) (Revised by Jim Kingdon, 6-Jan-2023.)
|- _e e/ QQ
Theorem	egt2lt3 11807	Euler's constant _e = 2.71828... is bounded by 2 and 3. (Contributed by NM, 28-Nov-2008.) (Revised by Jim Kingdon, 7-Jan-2023.)
|- ( 2 < _e /\ _e < 3 )
Theorem	epos 11808	Euler's constant _e is greater than 0. (Contributed by Jeff Hankins, 22-Nov-2008.)
|- 0 < _e
Theorem	epr 11809	Euler's constant _e is a positive real. (Contributed by Jeff Hankins, 22-Nov-2008.)
|- _e e. RR+
Theorem	ene0 11810	_e is not 0. (Contributed by David A. Wheeler, 17-Oct-2017.)
|- _e =/= 0
Theorem	eap0 11811	_e is apart from 0. (Contributed by Jim Kingdon, 7-Jan-2023.)
|- _e # 0
Theorem	ene1 11812	_e is not 1. (Contributed by David A. Wheeler, 17-Oct-2017.)
|- _e =/= 1
Theorem	eap1 11813	_e is apart from 1. (Contributed by Jim Kingdon, 7-Jan-2023.)
|- _e # 1
PART 5  ELEMENTARY NUMBER THEORY This part introduces elementary number theory, in particular the elementary properties of divisibility and elementary prime number theory.
5.1  Elementary properties of divisibility
5.1.1  The divides relation
Syntax	cdvds 11814	Extend the definition of a class to include the divides relation. See df-dvds 11815.
class ||
Definition	df-dvds 11815*	Define the divides relation, see definition in [ApostolNT] p. 14. (Contributed by Paul Chapman, 21-Mar-2011.)
|- || = { <. x , y >. | ( ( x e. ZZ /\ y e. ZZ ) /\ E. n e. ZZ ( n x. x ) = y ) }
Theorem	divides 11816*	Define the divides relation. M || N means M divides into N with no remainder. For example, 3 || 6 (ex-dvds 14886). As proven in dvdsval3 11818, M || N <-> ( N mod M ) = 0. See divides 11816 and dvdsval2 11817 for other equivalent expressions. (Contributed by Paul Chapman, 21-Mar-2011.)
|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M || N <-> E. n e. ZZ ( n x. M ) = N ) )
Theorem	dvdsval2 11817	One nonzero integer divides another integer if and only if their quotient is an integer. (Contributed by Jeff Hankins, 29-Sep-2013.)
|- ( ( M e. ZZ /\ M =/= 0 /\ N e. ZZ ) -> ( M || N <-> ( N / M ) e. ZZ ) )
Theorem	dvdsval3 11818	One nonzero integer divides another integer if and only if the remainder upon division is zero, see remark in [ApostolNT] p. 106. (Contributed by Mario Carneiro, 22-Feb-2014.) (Revised by Mario Carneiro, 15-Jul-2014.)
|- ( ( M e. NN /\ N e. ZZ ) -> ( M || N <-> ( N mod M ) = 0 ) )
Theorem	dvdszrcl 11819	Reverse closure for the divisibility relation. (Contributed by Stefan O'Rear, 5-Sep-2015.)
|- ( X || Y -> ( X e. ZZ /\ Y e. ZZ ) )
Theorem	dvdsmod0 11820	If a positive integer divides another integer, then the remainder upon division is zero. (Contributed by AV, 3-Mar-2022.)
|- ( ( M e. NN /\ M || N ) -> ( N mod M ) = 0 )
Theorem	p1modz1 11821	If a number greater than 1 divides another number, the second number increased by 1 is 1 modulo the first number. (Contributed by AV, 19-Mar-2022.)
|- ( ( M || A /\ 1 < M ) -> ( ( A + 1 ) mod M ) = 1 )
Theorem	dvdsmodexp 11822	If a positive integer divides another integer, this other integer is equal to its positive powers modulo the positive integer. (Formerly part of the proof for fermltl 12254). (Contributed by Mario Carneiro, 28-Feb-2014.) (Revised by AV, 19-Mar-2022.)
|- ( ( N e. NN /\ B e. NN /\ N || A ) -> ( ( A ^ B ) mod N ) = ( A mod N ) )
Theorem	nndivdvds 11823	Strong form of dvdsval2 11817 for positive integers. (Contributed by Stefan O'Rear, 13-Sep-2014.)
|- ( ( A e. NN /\ B e. NN ) -> ( B || A <-> ( A / B ) e. NN ) )
Theorem	nndivides 11824*	Definition of the divides relation for positive integers. (Contributed by AV, 26-Jul-2021.)
|- ( ( M e. NN /\ N e. NN ) -> ( M || N <-> E. n e. NN ( n x. M ) = N ) )
Theorem	dvdsdc 11825	Divisibility is decidable. (Contributed by Jim Kingdon, 14-Nov-2021.)
|- ( ( M e. NN /\ N e. ZZ ) -> DECID M || N )
Theorem	moddvds 11826	Two ways to say A == B (mod N), see also definition in [ApostolNT] p. 106. (Contributed by Mario Carneiro, 18-Feb-2014.)
|- ( ( N e. NN /\ A e. ZZ /\ B e. ZZ ) -> ( ( A mod N ) = ( B mod N ) <-> N || ( A - B ) ) )
Theorem	modm1div 11827	An integer greater than one divides another integer minus one iff the second integer modulo the first integer is one. (Contributed by AV, 30-May-2023.)
|- ( ( N e. ( ZZ>= ` 2 ) /\ A e. ZZ ) -> ( ( A mod N ) = 1 <-> N || ( A - 1 ) ) )
Theorem	dvds0lem 11828	A lemma to assist theorems of || with no antecedents. (Contributed by Paul Chapman, 21-Mar-2011.)
|- ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( K x. M ) = N ) -> M || N )
Theorem	dvds1lem 11829*	A lemma to assist theorems of || with one antecedent. (Contributed by Paul Chapman, 21-Mar-2011.)
|- ( ph -> ( J e. ZZ /\ K e. ZZ ) )   &    |- ( ph -> ( M e. ZZ /\ N e. ZZ ) )   &    |- ( ( ph /\ x e. ZZ ) -> Z e. ZZ )   &    |- ( ( ph /\ x e. ZZ ) -> ( ( x x. J ) = K -> ( Z x. M ) = N ) )   =>    |- ( ph -> ( J || K -> M || N ) )
Theorem	dvds2lem 11830*	A lemma to assist theorems of || with two antecedents. (Contributed by Paul Chapman, 21-Mar-2011.)
|- ( ph -> ( I e. ZZ /\ J e. ZZ ) )   &    |- ( ph -> ( K e. ZZ /\ L e. ZZ ) )   &    |- ( ph -> ( M e. ZZ /\ N e. ZZ ) )   &    |- ( ( ph /\ ( x e. ZZ /\ y e. ZZ ) ) -> Z e. ZZ )   &    |- ( ( ph /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( ( ( x x. I ) = J /\ ( y x. K ) = L ) -> ( Z x. M ) = N ) )   =>    |- ( ph -> ( ( I || J /\ K || L ) -> M || N ) )
Theorem	iddvds 11831	An integer divides itself. Theorem 1.1(a) in [ApostolNT] p. 14 (reflexive property of the divides relation). (Contributed by Paul Chapman, 21-Mar-2011.)
|- ( N e. ZZ -> N || N )
Theorem	1dvds 11832	1 divides any integer. Theorem 1.1(f) in [ApostolNT] p. 14. (Contributed by Paul Chapman, 21-Mar-2011.)
|- ( N e. ZZ -> 1 || N )
Theorem	dvds0 11833	Any integer divides 0. Theorem 1.1(g) in [ApostolNT] p. 14. (Contributed by Paul Chapman, 21-Mar-2011.)
|- ( N e. ZZ -> N || 0 )
Theorem	negdvdsb 11834	An integer divides another iff its negation does. (Contributed by Paul Chapman, 21-Mar-2011.)
|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M || N <-> -u M || N ) )
Theorem	dvdsnegb 11835	An integer divides another iff it divides its negation. (Contributed by Paul Chapman, 21-Mar-2011.)
|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M || N <-> M || -u N ) )
Theorem	absdvdsb 11836	An integer divides another iff its absolute value does. (Contributed by Paul Chapman, 21-Mar-2011.)
|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M || N <-> ( abs ` M ) || N ) )
Theorem	dvdsabsb 11837	An integer divides another iff it divides its absolute value. (Contributed by Paul Chapman, 21-Mar-2011.)
|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M || N <-> M || ( abs ` N ) ) )
Theorem	0dvds 11838	Only 0 is divisible by 0. Theorem 1.1(h) in [ApostolNT] p. 14. (Contributed by Paul Chapman, 21-Mar-2011.)
|- ( N e. ZZ -> ( 0 || N <-> N = 0 ) )
Theorem	zdvdsdc 11839	Divisibility of integers is decidable. (Contributed by Jim Kingdon, 17-Jan-2022.)
|- ( ( M e. ZZ /\ N e. ZZ ) -> DECID M || N )
Theorem	dvdsmul1 11840	An integer divides a multiple of itself. (Contributed by Paul Chapman, 21-Mar-2011.)
|- ( ( M e. ZZ /\ N e. ZZ ) -> M || ( M x. N ) )
Theorem	dvdsmul2 11841	An integer divides a multiple of itself. (Contributed by Paul Chapman, 21-Mar-2011.)
|- ( ( M e. ZZ /\ N e. ZZ ) -> N || ( M x. N ) )
Theorem	iddvdsexp 11842	An integer divides a positive integer power of itself. (Contributed by Paul Chapman, 26-Oct-2012.)
|- ( ( M e. ZZ /\ N e. NN ) -> M || ( M ^ N ) )
Theorem	muldvds1 11843	If a product divides an integer, so does one of its factors. (Contributed by Paul Chapman, 21-Mar-2011.)
|- ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( K x. M ) || N -> K || N ) )
Theorem	muldvds2 11844	If a product divides an integer, so does one of its factors. (Contributed by Paul Chapman, 21-Mar-2011.)
|- ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( K x. M ) || N -> M || N ) )
Theorem	dvdscmul 11845	Multiplication by a constant maintains the divides relation. Theorem 1.1(d) in [ApostolNT] p. 14 (multiplication property of the divides relation). (Contributed by Paul Chapman, 21-Mar-2011.)
|- ( ( M e. ZZ /\ N e. ZZ /\ K e. ZZ ) -> ( M || N -> ( K x. M ) || ( K x. N ) ) )
Theorem	dvdsmulc 11846	Multiplication by a constant maintains the divides relation. (Contributed by Paul Chapman, 21-Mar-2011.)
|- ( ( M e. ZZ /\ N e. ZZ /\ K e. ZZ ) -> ( M || N -> ( M x. K ) || ( N x. K ) ) )
Theorem	dvdscmulr 11847	Cancellation law for the divides relation. Theorem 1.1(e) in [ApostolNT] p. 14. (Contributed by Paul Chapman, 21-Mar-2011.)
|- ( ( M e. ZZ /\ N e. ZZ /\ ( K e. ZZ /\ K =/= 0 ) ) -> ( ( K x. M ) || ( K x. N ) <-> M || N ) )
Theorem	dvdsmulcr 11848	Cancellation law for the divides relation. (Contributed by Paul Chapman, 21-Mar-2011.)
|- ( ( M e. ZZ /\ N e. ZZ /\ ( K e. ZZ /\ K =/= 0 ) ) -> ( ( M x. K ) || ( N x. K ) <-> M || N ) )
Theorem	summodnegmod 11849	The sum of two integers modulo a positive integer equals zero iff the first of the two integers equals the negative of the other integer modulo the positive integer. (Contributed by AV, 25-Jul-2021.)
|- ( ( A e. ZZ /\ B e. ZZ /\ N e. NN ) -> ( ( ( A + B ) mod N ) = 0 <-> ( A mod N ) = ( -u B mod N ) ) )
Theorem	modmulconst 11850	Constant multiplication in a modulo operation, see theorem 5.3 in [ApostolNT] p. 108. (Contributed by AV, 21-Jul-2021.)
|- ( ( ( A e. ZZ /\ B e. ZZ /\ C e. NN ) /\ M e. NN ) -> ( ( A mod M ) = ( B mod M ) <-> ( ( C x. A ) mod ( C x. M ) ) = ( ( C x. B ) mod ( C x. M ) ) ) )
Theorem	dvds2ln 11851	If an integer divides each of two other integers, it divides any linear combination of them. Theorem 1.1(c) in [ApostolNT] p. 14 (linearity property of the divides relation). (Contributed by Paul Chapman, 21-Mar-2011.)
|- ( ( ( I e. ZZ /\ J e. ZZ ) /\ ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) ) -> ( ( K || M /\ K || N ) -> K || ( ( I x. M ) + ( J x. N ) ) ) )
Theorem	dvds2add 11852	If an integer divides each of two other integers, it divides their sum. (Contributed by Paul Chapman, 21-Mar-2011.)
|- ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( K || M /\ K || N ) -> K || ( M + N ) ) )
Theorem	dvds2sub 11853	If an integer divides each of two other integers, it divides their difference. (Contributed by Paul Chapman, 21-Mar-2011.)
|- ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( K || M /\ K || N ) -> K || ( M - N ) ) )
Theorem	dvds2subd 11854	Deduction form of dvds2sub 11853. (Contributed by Stanislas Polu, 9-Mar-2020.)
|- ( ph -> K e. ZZ )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> N e. ZZ )   &    |- ( ph -> K || M )   &    |- ( ph -> K || N )   =>    |- ( ph -> K || ( M - N ) )
Theorem	dvdstr 11855	The divides relation is transitive. Theorem 1.1(b) in [ApostolNT] p. 14 (transitive property of the divides relation). (Contributed by Paul Chapman, 21-Mar-2011.)
|- ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( K || M /\ M || N ) -> K || N ) )
Theorem	dvds2addd 11856	Deduction form of dvds2add 11852. (Contributed by SN, 21-Aug-2024.)
|- ( ph -> K e. ZZ )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> N e. ZZ )   &    |- ( ph -> K || M )   &    |- ( ph -> K || N )   =>    |- ( ph -> K || ( M + N ) )
Theorem	dvdstrd 11857	The divides relation is transitive, a deduction version of dvdstr 11855. (Contributed by metakunt, 12-May-2024.)
|- ( ph -> K e. ZZ )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> N e. ZZ )   &    |- ( ph -> K || M )   &    |- ( ph -> M || N )   =>    |- ( ph -> K || N )
Theorem	dvdsmultr1 11858	If an integer divides another, it divides a multiple of it. (Contributed by Paul Chapman, 17-Nov-2012.)
|- ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( K || M -> K || ( M x. N ) ) )
Theorem	dvdsmultr1d 11859	Natural deduction form of dvdsmultr1 11858. (Contributed by Stanislas Polu, 9-Mar-2020.)
|- ( ph -> K e. ZZ )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> N e. ZZ )   &    |- ( ph -> K || M )   =>    |- ( ph -> K || ( M x. N ) )
Theorem	dvdsmultr2 11860	If an integer divides another, it divides a multiple of it. (Contributed by Paul Chapman, 17-Nov-2012.)
|- ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( K || N -> K || ( M x. N ) ) )
Theorem	ordvdsmul 11861	If an integer divides either of two others, it divides their product. (Contributed by Paul Chapman, 17-Nov-2012.) (Proof shortened by Mario Carneiro, 17-Jul-2014.)
|- ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( K || M \/ K || N ) -> K || ( M x. N ) ) )
Theorem	dvdssub2 11862	If an integer divides a difference, then it divides one term iff it divides the other. (Contributed by Mario Carneiro, 13-Jul-2014.)
|- ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ K || ( M - N ) ) -> ( K || M <-> K || N ) )
Theorem	dvdsadd 11863	An integer divides another iff it divides their sum. (Contributed by Paul Chapman, 31-Mar-2011.) (Revised by Mario Carneiro, 13-Jul-2014.)
|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M || N <-> M || ( M + N ) ) )
Theorem	dvdsaddr 11864	An integer divides another iff it divides their sum. (Contributed by Paul Chapman, 31-Mar-2011.)
|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M || N <-> M || ( N + M ) ) )
Theorem	dvdssub 11865	An integer divides another iff it divides their difference. (Contributed by Paul Chapman, 31-Mar-2011.)
|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M || N <-> M || ( M - N ) ) )
Theorem	dvdssubr 11866	An integer divides another iff it divides their difference. (Contributed by Paul Chapman, 31-Mar-2011.)
|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M || N <-> M || ( N - M ) ) )
Theorem	dvdsadd2b 11867	Adding a multiple of the base does not affect divisibility. (Contributed by Stefan O'Rear, 23-Sep-2014.)
|- ( ( A e. ZZ /\ B e. ZZ /\ ( C e. ZZ /\ A || C ) ) -> ( A || B <-> A || ( C + B ) ) )
Theorem	dvdsaddre2b 11868	Adding a multiple of the base does not affect divisibility. Variant of dvdsadd2b 11867 only requiring B to be a real number (not necessarily an integer). (Contributed by AV, 19-Jul-2021.)
|- ( ( A e. ZZ /\ B e. RR /\ ( C e. ZZ /\ A || C ) ) -> ( A || B <-> A || ( C + B ) ) )
Theorem	dvdslelemd 11869	Lemma for dvdsle 11870. (Contributed by Jim Kingdon, 8-Nov-2021.)
|- ( ph -> M e. ZZ )   &    |- ( ph -> N e. NN )   &    |- ( ph -> K e. ZZ )   &    |- ( ph -> N < M )   =>    |- ( ph -> ( K x. M ) =/= N )
Theorem	dvdsle 11870	The divisors of a positive integer are bounded by it. The proof does not use /. (Contributed by Paul Chapman, 21-Mar-2011.)
|- ( ( M e. ZZ /\ N e. NN ) -> ( M || N -> M <_ N ) )
Theorem	dvdsleabs 11871	The divisors of a nonzero integer are bounded by its absolute value. Theorem 1.1(i) in [ApostolNT] p. 14 (comparison property of the divides relation). (Contributed by Paul Chapman, 21-Mar-2011.) (Proof shortened by Fan Zheng, 3-Jul-2016.)
|- ( ( M e. ZZ /\ N e. ZZ /\ N =/= 0 ) -> ( M || N -> M <_ ( abs ` N ) ) )
Theorem	dvdsleabs2 11872	Transfer divisibility to an order constraint on absolute values. (Contributed by Stefan O'Rear, 24-Sep-2014.)
|- ( ( M e. ZZ /\ N e. ZZ /\ N =/= 0 ) -> ( M || N -> ( abs ` M ) <_ ( abs ` N ) ) )
Theorem	dvdsabseq 11873	If two integers divide each other, they must be equal, up to a difference in sign. Theorem 1.1(j) in [ApostolNT] p. 14. (Contributed by Mario Carneiro, 30-May-2014.) (Revised by AV, 7-Aug-2021.)
|- ( ( M || N /\ N || M ) -> ( abs ` M ) = ( abs ` N ) )
Theorem	dvdseq 11874	If two nonnegative integers divide each other, they must be equal. (Contributed by Mario Carneiro, 30-May-2014.) (Proof shortened by AV, 7-Aug-2021.)
|- ( ( ( M e. NN0 /\ N e. NN0 ) /\ ( M || N /\ N || M ) ) -> M = N )
Theorem	divconjdvds 11875	If a nonzero integer M divides another integer N, the other integer N divided by the nonzero integer M (i.e. the divisor conjugate of N to M) divides the other integer N. Theorem 1.1(k) in [ApostolNT] p. 14. (Contributed by AV, 7-Aug-2021.)
|- ( ( M || N /\ M =/= 0 ) -> ( N / M ) || N )
Theorem	dvdsdivcl 11876*	The complement of a divisor of N is also a divisor of N. (Contributed by Mario Carneiro, 2-Jul-2015.) (Proof shortened by AV, 9-Aug-2021.)
|- ( ( N e. NN /\ A e. { x e. NN | x || N } ) -> ( N / A ) e. { x e. NN | x || N } )
Theorem	dvdsflip 11877*	An involution of the divisors of a number. (Contributed by Stefan O'Rear, 12-Sep-2015.) (Proof shortened by Mario Carneiro, 13-May-2016.)
|- A = { x e. NN | x || N }   &    |- F = ( y e. A |-> ( N / y ) )   =>    |- ( N e. NN -> F : A -1-1-onto-> A )
Theorem	dvdsssfz1 11878*	The set of divisors of a number is a subset of a finite set. (Contributed by Mario Carneiro, 22-Sep-2014.)
|- ( A e. NN -> { p e. NN | p || A } C_ ( 1 ... A ) )
Theorem	dvds1 11879	The only nonnegative integer that divides 1 is 1. (Contributed by Mario Carneiro, 2-Jul-2015.)
|- ( M e. NN0 -> ( M || 1 <-> M = 1 ) )
Theorem	alzdvds 11880*	Only 0 is divisible by all integers. (Contributed by Paul Chapman, 21-Mar-2011.)
|- ( N e. ZZ -> ( A. x e. ZZ x || N <-> N = 0 ) )
Theorem	dvdsext 11881*	Poset extensionality for division. (Contributed by Stefan O'Rear, 6-Sep-2015.)
|- ( ( A e. NN0 /\ B e. NN0 ) -> ( A = B <-> A. x e. NN0 ( A || x <-> B || x ) ) )
Theorem	fzm1ndvds 11882	No number between 1 and M - 1 divides M. (Contributed by Mario Carneiro, 24-Jan-2015.)
|- ( ( M e. NN /\ N e. ( 1 ... ( M - 1 ) ) ) -> -. M || N )
Theorem	fzo0dvdseq 11883	Zero is the only one of the first A nonnegative integers that is divisible by A. (Contributed by Stefan O'Rear, 6-Sep-2015.)
|- ( B e. ( 0..^ A ) -> ( A || B <-> B = 0 ) )
Theorem	fzocongeq 11884	Two different elements of a half-open range are not congruent mod its length. (Contributed by Stefan O'Rear, 6-Sep-2015.)
|- ( ( A e. ( C..^ D ) /\ B e. ( C..^ D ) ) -> ( ( D - C ) || ( A - B ) <-> A = B ) )
Theorem	addmodlteqALT 11885	Two nonnegative integers less than the modulus are equal iff the sums of these integer with another integer are equal modulo the modulus. Shorter proof of addmodlteq 10418 based on the "divides" relation. (Contributed by AV, 14-Mar-2021.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( ( I e. ( 0..^ N ) /\ J e. ( 0..^ N ) /\ S e. ZZ ) -> ( ( ( I + S ) mod N ) = ( ( J + S ) mod N ) <-> I = J ) )
Theorem	dvdsfac 11886	A positive integer divides any greater factorial. (Contributed by Paul Chapman, 28-Nov-2012.)
|- ( ( K e. NN /\ N e. ( ZZ>= ` K ) ) -> K || ( ! ` N ) )
Theorem	dvdsexp 11887	A power divides a power with a greater exponent. (Contributed by Mario Carneiro, 23-Feb-2014.)
|- ( ( A e. ZZ /\ M e. NN0 /\ N e. ( ZZ>= ` M ) ) -> ( A ^ M ) || ( A ^ N ) )
Theorem	dvdsmod 11888	Any number K whose mod base N is divisible by a divisor P of the base is also divisible by P. This means that primes will also be relatively prime to the base when reduced mod N for any base. (Contributed by Mario Carneiro, 13-Mar-2014.)
|- ( ( ( P e. NN /\ N e. NN /\ K e. ZZ ) /\ P || N ) -> ( P || ( K mod N ) <-> P || K ) )
Theorem	mulmoddvds 11889	If an integer is divisible by a positive integer, the product of this integer with another integer modulo the positive integer is 0. (Contributed by Alexander van der Vekens, 30-Aug-2018.)
|- ( ( N e. NN /\ A e. ZZ /\ B e. ZZ ) -> ( N || A -> ( ( A x. B ) mod N ) = 0 ) )
Theorem	3dvdsdec 11890	A decimal number is divisible by three iff the sum of its two "digits" is divisible by three. The term "digits" in its narrow sense is only correct if A and B actually are digits (i.e. nonnegative integers less than 10). However, this theorem holds for arbitrary nonnegative integers A and B, especially if A is itself a decimal number, e.g., A = ; C D. (Contributed by AV, 14-Jun-2021.) (Revised by AV, 8-Sep-2021.)
|- A e. NN0   &    |- B e. NN0   =>    |- ( 3 || ; A B <-> 3 || ( A + B ) )
Theorem	3dvds2dec 11891	A decimal number is divisible by three iff the sum of its three "digits" is divisible by three. The term "digits" in its narrow sense is only correct if A, B and C actually are digits (i.e. nonnegative integers less than 10). However, this theorem holds for arbitrary nonnegative integers A, B and C. (Contributed by AV, 14-Jun-2021.) (Revised by AV, 1-Aug-2021.)
|- A e. NN0   &    |- B e. NN0   &    |- C e. NN0   =>    |- ( 3 || ;; A B C <-> 3 || ( ( A + B ) + C ) )
5.1.2  Even and odd numbers The set ZZ of integers can be partitioned into the set of even numbers and the set of odd numbers, see zeo4 11895. Instead of defining new class variables Even and Odd to represent these sets, we use the idiom 2 || N to say that " N is even" (which implies N e. ZZ, see evenelz 11892) and -. 2 || N to say that " N is odd" (under the assumption that N e. ZZ). The previously proven theorems about even and odd numbers, like zneo 9374, zeo 9378, zeo2 9379, etc. use different representations, which are equivalent with the representations using the divides relation, see evend2 11914 and oddp1d2 11915. The corresponding theorems are zeneo 11896, zeo3 11893 and zeo4 11895.
Theorem	evenelz 11892	An even number is an integer. This follows immediately from the reverse closure of the divides relation, see dvdszrcl 11819. (Contributed by AV, 22-Jun-2021.)
|- ( 2 || N -> N e. ZZ )
Theorem	zeo3 11893	An integer is even or odd. (Contributed by AV, 17-Jun-2021.)
|- ( N e. ZZ -> ( 2 || N \/ -. 2 || N ) )
Theorem	zeoxor 11894	An integer is even or odd but not both. (Contributed by Jim Kingdon, 10-Nov-2021.)
|- ( N e. ZZ -> ( 2 || N \/_ -. 2 || N ) )
Theorem	zeo4 11895	An integer is even or odd but not both. (Contributed by AV, 17-Jun-2021.)
|- ( N e. ZZ -> ( 2 || N <-> -. -. 2 || N ) )
Theorem	zeneo 11896	No even integer equals an odd integer (i.e. no integer can be both even and odd). Exercise 10(a) of [Apostol] p. 28. This variant of zneo 9374 follows immediately from the fact that a contradiction implies anything, see pm2.21i 647. (Contributed by AV, 22-Jun-2021.)
|- ( ( A e. ZZ /\ B e. ZZ ) -> ( ( 2 || A /\ -. 2 || B ) -> A =/= B ) )
Theorem	odd2np1lem 11897*	Lemma for odd2np1 11898. (Contributed by Scott Fenton, 3-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
|- ( N e. NN0 -> ( E. n e. ZZ ( ( 2 x. n ) + 1 ) = N \/ E. k e. ZZ ( k x. 2 ) = N ) )
Theorem	odd2np1 11898*	An integer is odd iff it is one plus twice another integer. (Contributed by Scott Fenton, 3-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
|- ( N e. ZZ -> ( -. 2 || N <-> E. n e. ZZ ( ( 2 x. n ) + 1 ) = N ) )
Theorem	even2n 11899*	An integer is even iff it is twice another integer. (Contributed by AV, 25-Jun-2020.)
|- ( 2 || N <-> E. n e. ZZ ( 2 x. n ) = N )
Theorem	oddm1even 11900	An integer is odd iff its predecessor is even. (Contributed by Mario Carneiro, 5-Sep-2016.)
|- ( N e. ZZ -> ( -. 2 || N <-> 2 || ( N - 1 ) ) )