P. 120 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 11901-12000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	recos4p 11901*	Separate out the first four terms of the infinite series expansion of the cosine of a real number. (Contributed by Paul Chapman, 19-Jan-2008.) (Revised by Mario Carneiro, 30-Apr-2014.)
|- F = ( n e. NN0 |-> ( ( ( _i x. A ) ^ n ) / ( ! ` n ) ) )   =>    |- ( A e. RR -> ( cos ` A ) = ( ( 1 - ( ( A ^ 2 ) / 2 ) ) + ( Re ` sum_ k e. ( ZZ>= ` 4 ) ( F ` k ) ) ) )
Theorem	resincl 11902	The sine of a real number is real. (Contributed by NM, 30-Apr-2005.)
|- ( A e. RR -> ( sin ` A ) e. RR )
Theorem	recoscl 11903	The cosine of a real number is real. (Contributed by NM, 30-Apr-2005.)
|- ( A e. RR -> ( cos ` A ) e. RR )
Theorem	retanclap 11904	The closure of the tangent function with a real argument. (Contributed by David A. Wheeler, 15-Mar-2014.)
|- ( ( A e. RR /\ ( cos ` A ) # 0 ) -> ( tan ` A ) e. RR )
Theorem	resincld 11905	Closure of the sine function. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR )   =>    |- ( ph -> ( sin ` A ) e. RR )
Theorem	recoscld 11906	Closure of the cosine function. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR )   =>    |- ( ph -> ( cos ` A ) e. RR )
Theorem	retanclapd 11907	Closure of the tangent function. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> ( cos ` A ) # 0 )   =>    |- ( ph -> ( tan ` A ) e. RR )
Theorem	sinneg 11908	The sine of a negative is the negative of the sine. (Contributed by NM, 30-Apr-2005.)
|- ( A e. CC -> ( sin ` -u A ) = -u ( sin ` A ) )
Theorem	cosneg 11909	The cosines of a number and its negative are the same. (Contributed by NM, 30-Apr-2005.)
|- ( A e. CC -> ( cos ` -u A ) = ( cos ` A ) )
Theorem	tannegap 11910	The tangent of a negative is the negative of the tangent. (Contributed by David A. Wheeler, 23-Mar-2014.)
|- ( ( A e. CC /\ ( cos ` A ) # 0 ) -> ( tan ` -u A ) = -u ( tan ` A ) )
Theorem	sin0 11911	Value of the sine function at 0. (Contributed by Steve Rodriguez, 14-Mar-2005.)
|- ( sin ` 0 ) = 0
Theorem	cos0 11912	Value of the cosine function at 0. (Contributed by NM, 30-Apr-2005.)
|- ( cos ` 0 ) = 1
Theorem	tan0 11913	The value of the tangent function at zero is zero. (Contributed by David A. Wheeler, 16-Mar-2014.)
|- ( tan ` 0 ) = 0
Theorem	efival 11914	The exponential function in terms of sine and cosine. (Contributed by NM, 30-Apr-2005.)
|- ( A e. CC -> ( exp ` ( _i x. A ) ) = ( ( cos ` A ) + ( _i x. ( sin ` A ) ) ) )
Theorem	efmival 11915	The exponential function in terms of sine and cosine. (Contributed by NM, 14-Jan-2006.)
|- ( A e. CC -> ( exp ` ( -u _i x. A ) ) = ( ( cos ` A ) - ( _i x. ( sin ` A ) ) ) )
Theorem	efeul 11916	Eulerian representation of the complex exponential. (Suggested by Jeff Hankins, 3-Jul-2006.) (Contributed by NM, 4-Jul-2006.)
|- ( A e. CC -> ( exp ` A ) = ( ( exp ` ( Re ` A ) ) x. ( ( cos ` ( Im ` A ) ) + ( _i x. ( sin ` ( Im ` A ) ) ) ) ) )
Theorem	efieq 11917	The exponentials of two imaginary numbers are equal iff their sine and cosine components are equal. (Contributed by Paul Chapman, 15-Mar-2008.)
|- ( ( A e. RR /\ B e. RR ) -> ( ( exp ` ( _i x. A ) ) = ( exp ` ( _i x. B ) ) <-> ( ( cos ` A ) = ( cos ` B ) /\ ( sin ` A ) = ( sin ` B ) ) ) )
Theorem	sinadd 11918	Addition formula for sine. Equation 14 of [Gleason] p. 310. (Contributed by Steve Rodriguez, 10-Nov-2006.) (Revised by Mario Carneiro, 30-Apr-2014.)
|- ( ( A e. CC /\ B e. CC ) -> ( sin ` ( A + B ) ) = ( ( ( sin ` A ) x. ( cos ` B ) ) + ( ( cos ` A ) x. ( sin ` B ) ) ) )
Theorem	cosadd 11919	Addition formula for cosine. Equation 15 of [Gleason] p. 310. (Contributed by NM, 15-Jan-2006.) (Revised by Mario Carneiro, 30-Apr-2014.)
|- ( ( A e. CC /\ B e. CC ) -> ( cos ` ( A + B ) ) = ( ( ( cos ` A ) x. ( cos ` B ) ) - ( ( sin ` A ) x. ( sin ` B ) ) ) )
Theorem	tanaddaplem 11920	A useful intermediate step in tanaddap 11921 when showing that the addition of tangents is well-defined. (Contributed by Mario Carneiro, 4-Apr-2015.) (Revised by Jim Kingdon, 25-Dec-2022.)
|- ( ( ( A e. CC /\ B e. CC ) /\ ( ( cos ` A ) # 0 /\ ( cos ` B ) # 0 ) ) -> ( ( cos ` ( A + B ) ) # 0 <-> ( ( tan ` A ) x. ( tan ` B ) ) # 1 ) )
Theorem	tanaddap 11921	Addition formula for tangent. (Contributed by Mario Carneiro, 4-Apr-2015.)
|- ( ( ( A e. CC /\ B e. CC ) /\ ( ( cos ` A ) # 0 /\ ( cos ` B ) # 0 /\ ( cos ` ( A + B ) ) # 0 ) ) -> ( tan ` ( A + B ) ) = ( ( ( tan ` A ) + ( tan ` B ) ) / ( 1 - ( ( tan ` A ) x. ( tan ` B ) ) ) ) )
Theorem	sinsub 11922	Sine of difference. (Contributed by Paul Chapman, 12-Oct-2007.)
|- ( ( A e. CC /\ B e. CC ) -> ( sin ` ( A - B ) ) = ( ( ( sin ` A ) x. ( cos ` B ) ) - ( ( cos ` A ) x. ( sin ` B ) ) ) )
Theorem	cossub 11923	Cosine of difference. (Contributed by Paul Chapman, 12-Oct-2007.)
|- ( ( A e. CC /\ B e. CC ) -> ( cos ` ( A - B ) ) = ( ( ( cos ` A ) x. ( cos ` B ) ) + ( ( sin ` A ) x. ( sin ` B ) ) ) )
Theorem	addsin 11924	Sum of sines. (Contributed by Paul Chapman, 12-Oct-2007.)
|- ( ( A e. CC /\ B e. CC ) -> ( ( sin ` A ) + ( sin ` B ) ) = ( 2 x. ( ( sin ` ( ( A + B ) / 2 ) ) x. ( cos ` ( ( A - B ) / 2 ) ) ) ) )
Theorem	subsin 11925	Difference of sines. (Contributed by Paul Chapman, 12-Oct-2007.)
|- ( ( A e. CC /\ B e. CC ) -> ( ( sin ` A ) - ( sin ` B ) ) = ( 2 x. ( ( cos ` ( ( A + B ) / 2 ) ) x. ( sin ` ( ( A - B ) / 2 ) ) ) ) )
Theorem	sinmul 11926	Product of sines can be rewritten as half the difference of certain cosines. This follows from cosadd 11919 and cossub 11923. (Contributed by David A. Wheeler, 26-May-2015.)
|- ( ( A e. CC /\ B e. CC ) -> ( ( sin ` A ) x. ( sin ` B ) ) = ( ( ( cos ` ( A - B ) ) - ( cos ` ( A + B ) ) ) / 2 ) )
Theorem	cosmul 11927	Product of cosines can be rewritten as half the sum of certain cosines. This follows from cosadd 11919 and cossub 11923. (Contributed by David A. Wheeler, 26-May-2015.)
|- ( ( A e. CC /\ B e. CC ) -> ( ( cos ` A ) x. ( cos ` B ) ) = ( ( ( cos ` ( A - B ) ) + ( cos ` ( A + B ) ) ) / 2 ) )
Theorem	addcos 11928	Sum of cosines. (Contributed by Paul Chapman, 12-Oct-2007.)
|- ( ( A e. CC /\ B e. CC ) -> ( ( cos ` A ) + ( cos ` B ) ) = ( 2 x. ( ( cos ` ( ( A + B ) / 2 ) ) x. ( cos ` ( ( A - B ) / 2 ) ) ) ) )
Theorem	subcos 11929	Difference of cosines. (Contributed by Paul Chapman, 12-Oct-2007.) (Revised by Mario Carneiro, 10-May-2014.)
|- ( ( A e. CC /\ B e. CC ) -> ( ( cos ` B ) - ( cos ` A ) ) = ( 2 x. ( ( sin ` ( ( A + B ) / 2 ) ) x. ( sin ` ( ( A - B ) / 2 ) ) ) ) )
Theorem	sincossq 11930	Sine squared plus cosine squared is 1. Equation 17 of [Gleason] p. 311. Note that this holds for non-real arguments, even though individually each term is unbounded. (Contributed by NM, 15-Jan-2006.)
|- ( A e. CC -> ( ( ( sin ` A ) ^ 2 ) + ( ( cos ` A ) ^ 2 ) ) = 1 )
Theorem	sin2t 11931	Double-angle formula for sine. (Contributed by Paul Chapman, 17-Jan-2008.)
|- ( A e. CC -> ( sin ` ( 2 x. A ) ) = ( 2 x. ( ( sin ` A ) x. ( cos ` A ) ) ) )
Theorem	cos2t 11932	Double-angle formula for cosine. (Contributed by Paul Chapman, 24-Jan-2008.)
|- ( A e. CC -> ( cos ` ( 2 x. A ) ) = ( ( 2 x. ( ( cos ` A ) ^ 2 ) ) - 1 ) )
Theorem	cos2tsin 11933	Double-angle formula for cosine in terms of sine. (Contributed by NM, 12-Sep-2008.)
|- ( A e. CC -> ( cos ` ( 2 x. A ) ) = ( 1 - ( 2 x. ( ( sin ` A ) ^ 2 ) ) ) )
Theorem	sinbnd 11934	The sine of a real number lies between -1 and 1. Equation 18 of [Gleason] p. 311. (Contributed by NM, 16-Jan-2006.)
|- ( A e. RR -> ( -u 1 <_ ( sin ` A ) /\ ( sin ` A ) <_ 1 ) )
Theorem	cosbnd 11935	The cosine of a real number lies between -1 and 1. Equation 18 of [Gleason] p. 311. (Contributed by NM, 16-Jan-2006.)
|- ( A e. RR -> ( -u 1 <_ ( cos ` A ) /\ ( cos ` A ) <_ 1 ) )
Theorem	sinbnd2 11936	The sine of a real number is in the closed interval from -1 to 1. (Contributed by Mario Carneiro, 12-May-2014.)
|- ( A e. RR -> ( sin ` A ) e. ( -u 1 [,] 1 ) )
Theorem	cosbnd2 11937	The cosine of a real number is in the closed interval from -1 to 1. (Contributed by Mario Carneiro, 12-May-2014.)
|- ( A e. RR -> ( cos ` A ) e. ( -u 1 [,] 1 ) )
Theorem	ef01bndlem 11938*	Lemma for sin01bnd 11939 and cos01bnd 11940. (Contributed by Paul Chapman, 19-Jan-2008.)
|- F = ( n e. NN0 |-> ( ( ( _i x. A ) ^ n ) / ( ! ` n ) ) )   =>    |- ( A e. ( 0 (,] 1 ) -> ( abs ` sum_ k e. ( ZZ>= ` 4 ) ( F ` k ) ) < ( ( A ^ 4 ) / 6 ) )
Theorem	sin01bnd 11939	Bounds on the sine of a positive real number less than or equal to 1. (Contributed by Paul Chapman, 19-Jan-2008.) (Revised by Mario Carneiro, 30-Apr-2014.)
|- ( A e. ( 0 (,] 1 ) -> ( ( A - ( ( A ^ 3 ) / 3 ) ) < ( sin ` A ) /\ ( sin ` A ) < A ) )
Theorem	cos01bnd 11940	Bounds on the cosine of a positive real number less than or equal to 1. (Contributed by Paul Chapman, 19-Jan-2008.) (Revised by Mario Carneiro, 30-Apr-2014.)
|- ( A e. ( 0 (,] 1 ) -> ( ( 1 - ( 2 x. ( ( A ^ 2 ) / 3 ) ) ) < ( cos ` A ) /\ ( cos ` A ) < ( 1 - ( ( A ^ 2 ) / 3 ) ) ) )
Theorem	cos1bnd 11941	Bounds on the cosine of 1. (Contributed by Paul Chapman, 19-Jan-2008.)
|- ( ( 1 / 3 ) < ( cos ` 1 ) /\ ( cos ` 1 ) < ( 2 / 3 ) )
Theorem	cos2bnd 11942	Bounds on the cosine of 2. (Contributed by Paul Chapman, 19-Jan-2008.)
|- ( -u ( 7 / 9 ) < ( cos ` 2 ) /\ ( cos ` 2 ) < -u ( 1 / 9 ) )
Theorem	sinltxirr 11943*	The sine of a positive irrational number is less than its argument. Here irrational means apart from any rational number. (Contributed by Mario Carneiro, 29-Jul-2014.)
|- ( ( A e. RR+ /\ A. q e. QQ A # q ) -> ( sin ` A ) < A )
Theorem	sin01gt0 11944	The sine of a positive real number less than or equal to 1 is positive. (Contributed by Paul Chapman, 19-Jan-2008.) (Revised by Wolf Lammen, 25-Sep-2020.)
|- ( A e. ( 0 (,] 1 ) -> 0 < ( sin ` A ) )
Theorem	cos01gt0 11945	The cosine of a positive real number less than or equal to 1 is positive. (Contributed by Paul Chapman, 19-Jan-2008.)
|- ( A e. ( 0 (,] 1 ) -> 0 < ( cos ` A ) )
Theorem	sin02gt0 11946	The sine of a positive real number less than or equal to 2 is positive. (Contributed by Paul Chapman, 19-Jan-2008.)
|- ( A e. ( 0 (,] 2 ) -> 0 < ( sin ` A ) )
Theorem	sincos1sgn 11947	The signs of the sine and cosine of 1. (Contributed by Paul Chapman, 19-Jan-2008.)
|- ( 0 < ( sin ` 1 ) /\ 0 < ( cos ` 1 ) )
Theorem	sincos2sgn 11948	The signs of the sine and cosine of 2. (Contributed by Paul Chapman, 19-Jan-2008.)
|- ( 0 < ( sin ` 2 ) /\ ( cos ` 2 ) < 0 )
Theorem	sin4lt0 11949	The sine of 4 is negative. (Contributed by Paul Chapman, 19-Jan-2008.)
|- ( sin ` 4 ) < 0
Theorem	cos12dec 11950	Cosine is decreasing from one to two. (Contributed by Mario Carneiro and Jim Kingdon, 6-Mar-2024.)
|- ( ( A e. ( 1 [,] 2 ) /\ B e. ( 1 [,] 2 ) /\ A < B ) -> ( cos ` B ) < ( cos ` A ) )
Theorem	absefi 11951	The absolute value of the exponential of an imaginary number is one. Equation 48 of [Rudin] p. 167. (Contributed by Jason Orendorff, 9-Feb-2007.)
|- ( A e. RR -> ( abs ` ( exp ` ( _i x. A ) ) ) = 1 )
Theorem	absef 11952	The absolute value of the exponential is the exponential of the real part. (Contributed by Paul Chapman, 13-Sep-2007.)
|- ( A e. CC -> ( abs ` ( exp ` A ) ) = ( exp ` ( Re ` A ) ) )
Theorem	absefib 11953	A complex number is real iff the exponential of its product with _i has absolute value one. (Contributed by NM, 21-Aug-2008.)
|- ( A e. CC -> ( A e. RR <-> ( abs ` ( exp ` ( _i x. A ) ) ) = 1 ) )
Theorem	efieq1re 11954	A number whose imaginary exponential is one is real. (Contributed by NM, 21-Aug-2008.)
|- ( ( A e. CC /\ ( exp ` ( _i x. A ) ) = 1 ) -> A e. RR )
Theorem	demoivre 11955	De Moivre's Formula. Proof by induction given at http://en.wikipedia.org/wiki/De_Moivre's_formula, but restricted to nonnegative integer powers. See also demoivreALT 11956 for an alternate longer proof not using the exponential function. (Contributed by NM, 24-Jul-2007.)
|- ( ( A e. CC /\ N e. ZZ ) -> ( ( ( cos ` A ) + ( _i x. ( sin ` A ) ) ) ^ N ) = ( ( cos ` ( N x. A ) ) + ( _i x. ( sin ` ( N x. A ) ) ) ) )
Theorem	demoivreALT 11956	Alternate proof of demoivre 11955. 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.10.1.1  The circle constant (tau = 2 pi)
Syntax	ctau 11957	Extend class notation to include the constant tau, tau = 6.28318....
class tau
Definition	df-tau 11958	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.10.2  _e is irrational
Theorem	eirraplem 11959*	Lemma for eirrap 11960. (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 11960	_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 11961. (Contributed by Jim Kingdon, 6-Jan-2023.)
|- ( Q e. QQ -> _e # Q )
Theorem	eirr 11961	_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 11960. (Contributed by Paul Chapman, 9-Feb-2008.) (Revised by Jim Kingdon, 6-Jan-2023.)
|- _e e/ QQ
Theorem	egt2lt3 11962	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 11963	Euler's constant _e is greater than 0. (Contributed by Jeff Hankins, 22-Nov-2008.)
|- 0 < _e
Theorem	epr 11964	Euler's constant _e is a positive real. (Contributed by Jeff Hankins, 22-Nov-2008.)
|- _e e. RR+
Theorem	ene0 11965	_e is not 0. (Contributed by David A. Wheeler, 17-Oct-2017.)
|- _e =/= 0
Theorem	eap0 11966	_e is apart from 0. (Contributed by Jim Kingdon, 7-Jan-2023.)
|- _e # 0
Theorem	ene1 11967	_e is not 1. (Contributed by David A. Wheeler, 17-Oct-2017.)
|- _e =/= 1
Theorem	eap1 11968	_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 11969	Extend the definition of a class to include the divides relation. See df-dvds 11970.
class ||
Definition	df-dvds 11970*	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 11971*	Define the divides relation. M || N means M divides into N with no remainder. For example, 3 || 6 (ex-dvds 15460). As proven in dvdsval3 11973, M || N <-> ( N mod M ) = 0. See divides 11971 and dvdsval2 11972 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 11972	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 11973	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 11974	Reverse closure for the divisibility relation. (Contributed by Stefan O'Rear, 5-Sep-2015.)
|- ( X || Y -> ( X e. ZZ /\ Y e. ZZ ) )
Theorem	dvdsmod0 11975	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 11976	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 11977	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 12427). (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 11978	Strong form of dvdsval2 11972 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 11979*	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 11980	Divisibility is decidable. (Contributed by Jim Kingdon, 14-Nov-2021.)
|- ( ( M e. NN /\ N e. ZZ ) -> DECID M || N )
Theorem	moddvds 11981	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 11982	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 11983	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 11984*	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 11985*	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 11986	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 11987	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 11988	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 11989	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 11990	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 11991	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 11992	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 11993	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 11994	Divisibility of integers is decidable. (Contributed by Jim Kingdon, 17-Jan-2022.)
|- ( ( M e. ZZ /\ N e. ZZ ) -> DECID M || N )
Theorem	dvdsmul1 11995	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 11996	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 11997	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 11998	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 11999	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 12000	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 ) ) )