P. 126 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 12501-12600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	eap0 12501	_e is apart from 0. (Contributed by Jim Kingdon, 7-Jan-2023.)
|- _e # 0
Theorem	ene1 12502	_e is not 1. (Contributed by David A. Wheeler, 17-Oct-2017.)
|- _e =/= 1
Theorem	eap1 12503	_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 12504	Extend the definition of a class to include the divides relation. See df-dvds 12505.
class ||
Definition	df-dvds 12505*	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 12506*	Define the divides relation. M || N means M divides into N with no remainder. For example, 3 || 6 (ex-dvds 16629). As proven in dvdsval3 12508, M || N <-> ( N mod M ) = 0. See divides 12506 and dvdsval2 12507 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 12507	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 12508	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 12509	Reverse closure for the divisibility relation. (Contributed by Stefan O'Rear, 5-Sep-2015.)
|- ( X || Y -> ( X e. ZZ /\ Y e. ZZ ) )
Theorem	dvdsmod0 12510	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 12511	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 12512	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 12962). (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 12513	Strong form of dvdsval2 12507 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 12514*	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 12515	Divisibility is decidable. (Contributed by Jim Kingdon, 14-Nov-2021.)
|- ( ( M e. NN /\ N e. ZZ ) -> DECID M || N )
Theorem	moddvds 12516	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 12517	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 12518	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 12519*	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 12520*	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 12521	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 12522	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 12523	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 12524	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 12525	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 12526	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 12527	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 12528	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 12529	Divisibility of integers is decidable. (Contributed by Jim Kingdon, 17-Jan-2022.)
|- ( ( M e. ZZ /\ N e. ZZ ) -> DECID M || N )
Theorem	dvdsmul1 12530	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 12531	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 12532	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 12533	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 12534	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 12535	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 12536	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 12537	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 12538	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 12539	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 12540	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 12541	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 12542	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 12543	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 12544	Deduction form of dvds2sub 12543. (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 12545	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 12546	Deduction form of dvds2add 12542. (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 12547	The divides relation is transitive, a deduction version of dvdstr 12545. (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 12548	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 12549	Natural deduction form of dvdsmultr1 12548. (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 12550	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 12551	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 12552	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 12553	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 12554	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 12555	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 12556	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 12557	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 12558	Adding a multiple of the base does not affect divisibility. Variant of dvdsadd2b 12557 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	fsumdvds 12559*	If every term in a sum is divisible by N, then so is the sum. (Contributed by Mario Carneiro, 17-Jan-2015.)
|- ( ph -> A e. Fin )   &    |- ( ph -> N e. ZZ )   &    |- ( ( ph /\ k e. A ) -> B e. ZZ )   &    |- ( ( ph /\ k e. A ) -> N || B )   =>    |- ( ph -> N || sum_ k e. A B )
Theorem	dvdslelemd 12560	Lemma for dvdsle 12561. (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 12561	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 12562	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 12563	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 12564	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 12565	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 12566	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 12567*	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 12568*	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 12569*	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 12570	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 12571*	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 12572*	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 12573	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 12574	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 12575	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 12576	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 10789 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 12577	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 12578	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 12579	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 12580	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	3dvds 12581*	A rule for divisibility by 3 of a number written in base 10. This is Metamath 100 proof #85. (Contributed by Mario Carneiro, 14-Jul-2014.) (Revised by Mario Carneiro, 17-Jan-2015.) (Revised by AV, 8-Sep-2021.)
|- ( ( N e. NN0 /\ F : ( 0 ... N ) --> ZZ ) -> ( 3 || sum_ k e. ( 0 ... N ) ( ( F ` k ) x. (; 1 0 ^ k ) ) <-> 3 || sum_ k e. ( 0 ... N ) ( F ` k ) ) )
Theorem	3dvdsdec 12582	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 12583	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 12587. 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 12584) 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 9702, zeo 9706, zeo2 9707, etc. use different representations, which are equivalent with the representations using the divides relation, see evend2 12606 and oddp1d2 12607. The corresponding theorems are zeneo 12588, zeo3 12585 and zeo4 12587.
Theorem	evenelz 12584	An even number is an integer. This follows immediately from the reverse closure of the divides relation, see dvdszrcl 12509. (Contributed by AV, 22-Jun-2021.)
|- ( 2 || N -> N e. ZZ )
Theorem	zeo3 12585	An integer is even or odd. (Contributed by AV, 17-Jun-2021.)
|- ( N e. ZZ -> ( 2 || N \/ -. 2 || N ) )
Theorem	zeoxor 12586	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 12587	An integer is even or odd but not both. (Contributed by AV, 17-Jun-2021.)
|- ( N e. ZZ -> ( 2 || N <-> -. -. 2 || N ) )
Theorem	zeneo 12588	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 9702 follows immediately from the fact that a contradiction implies anything, see pm2.21i 651. (Contributed by AV, 22-Jun-2021.)
|- ( ( A e. ZZ /\ B e. ZZ ) -> ( ( 2 || A /\ -. 2 || B ) -> A =/= B ) )
Theorem	odd2np1lem 12589*	Lemma for odd2np1 12590. (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 12590*	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 12591*	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 12592	An integer is odd iff its predecessor is even. (Contributed by Mario Carneiro, 5-Sep-2016.)
|- ( N e. ZZ -> ( -. 2 || N <-> 2 || ( N - 1 ) ) )
Theorem	oddp1even 12593	An integer is odd iff its successor is even. (Contributed by Mario Carneiro, 5-Sep-2016.)
|- ( N e. ZZ -> ( -. 2 || N <-> 2 || ( N + 1 ) ) )
Theorem	oexpneg 12594	The exponential of the negative of a number, when the exponent is odd. (Contributed by Mario Carneiro, 25-Apr-2015.)
|- ( ( A e. CC /\ N e. NN /\ -. 2 || N ) -> ( -u A ^ N ) = -u ( A ^ N ) )
Theorem	mod2eq0even 12595	An integer is 0 modulo 2 iff it is even (i.e. divisible by 2), see example 2 in [ApostolNT] p. 107. (Contributed by AV, 21-Jul-2021.)
|- ( N e. ZZ -> ( ( N mod 2 ) = 0 <-> 2 || N ) )
Theorem	mod2eq1n2dvds 12596	An integer is 1 modulo 2 iff it is odd (i.e. not divisible by 2), see example 3 in [ApostolNT] p. 107. (Contributed by AV, 24-May-2020.)
|- ( N e. ZZ -> ( ( N mod 2 ) = 1 <-> -. 2 || N ) )
Theorem	oddnn02np1 12597*	A nonnegative integer is odd iff it is one plus twice another nonnegative integer. (Contributed by AV, 19-Jun-2021.)
|- ( N e. NN0 -> ( -. 2 || N <-> E. n e. NN0 ( ( 2 x. n ) + 1 ) = N ) )
Theorem	oddge22np1 12598*	An integer greater than one is odd iff it is one plus twice a positive integer. (Contributed by AV, 16-Aug-2021.)
|- ( N e. ( ZZ>= ` 2 ) -> ( -. 2 || N <-> E. n e. NN ( ( 2 x. n ) + 1 ) = N ) )
Theorem	evennn02n 12599*	A nonnegative integer is even iff it is twice another nonnegative integer. (Contributed by AV, 12-Aug-2021.)
|- ( N e. NN0 -> ( 2 || N <-> E. n e. NN0 ( 2 x. n ) = N ) )
Theorem	evennn2n 12600*	A positive integer is even iff it is twice another positive integer. (Contributed by AV, 12-Aug-2021.)
|- ( N e. NN -> ( 2 || N <-> E. n e. NN ( 2 x. n ) = N ) )