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	p1modz1 11801	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.)
⊢ ((𝑀 ∥ 𝐴 ∧ 1 < 𝑀) → ((𝐴 + 1) mod 𝑀) = 1)
Theorem	dvdsmodexp 11802	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 12234). (Contributed by Mario Carneiro, 28-Feb-2014.) (Revised by AV, 19-Mar-2022.)
⊢ ((𝑁 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∥ 𝐴) → ((𝐴↑𝐵) mod 𝑁) = (𝐴 mod 𝑁))
Theorem	nndivdvds 11803	Strong form of dvdsval2 11797 for positive integers. (Contributed by Stefan O'Rear, 13-Sep-2014.)
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐵 ∥ 𝐴 ↔ (𝐴 / 𝐵) ∈ ℕ))
Theorem	nndivides 11804*	Definition of the divides relation for positive integers. (Contributed by AV, 26-Jul-2021.)
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 ∥ 𝑁 ↔ ∃𝑛 ∈ ℕ (𝑛 · 𝑀) = 𝑁))
Theorem	dvdsdc 11805	Divisibility is decidable. (Contributed by Jim Kingdon, 14-Nov-2021.)
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℤ) → DECID 𝑀 ∥ 𝑁)
Theorem	moddvds 11806	Two ways to say 𝐴≡𝐵 (mod 𝑁), see also definition in [ApostolNT] p. 106. (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐴 mod 𝑁) = (𝐵 mod 𝑁) ↔ 𝑁 ∥ (𝐴 − 𝐵)))
Theorem	modm1div 11807	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.)
⊢ ((𝑁 ∈ (ℤ≥‘2) ∧ 𝐴 ∈ ℤ) → ((𝐴 mod 𝑁) = 1 ↔ 𝑁 ∥ (𝐴 − 1)))
Theorem	dvds0lem 11808	A lemma to assist theorems of ∥ with no antecedents. (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ (((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 · 𝑀) = 𝑁) → 𝑀 ∥ 𝑁)
Theorem	dvds1lem 11809*	A lemma to assist theorems of ∥ with one antecedent. (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ (𝜑 → (𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ))    &   ⊢ (𝜑 → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ ℤ) → 𝑍 ∈ ℤ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ ℤ) → ((𝑥 · 𝐽) = 𝐾 → (𝑍 · 𝑀) = 𝑁))    ⇒   ⊢ (𝜑 → (𝐽 ∥ 𝐾 → 𝑀 ∥ 𝑁))
Theorem	dvds2lem 11810*	A lemma to assist theorems of ∥ with two antecedents. (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ (𝜑 → (𝐼 ∈ ℤ ∧ 𝐽 ∈ ℤ))    &   ⊢ (𝜑 → (𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ))    &   ⊢ (𝜑 → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → 𝑍 ∈ ℤ)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (((𝑥 · 𝐼) = 𝐽 ∧ (𝑦 · 𝐾) = 𝐿) → (𝑍 · 𝑀) = 𝑁))    ⇒   ⊢ (𝜑 → ((𝐼 ∥ 𝐽 ∧ 𝐾 ∥ 𝐿) → 𝑀 ∥ 𝑁))
Theorem	iddvds 11811	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.)
⊢ (𝑁 ∈ ℤ → 𝑁 ∥ 𝑁)
Theorem	1dvds 11812	1 divides any integer. Theorem 1.1(f) in [ApostolNT] p. 14. (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ (𝑁 ∈ ℤ → 1 ∥ 𝑁)
Theorem	dvds0 11813	Any integer divides 0. Theorem 1.1(g) in [ApostolNT] p. 14. (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ (𝑁 ∈ ℤ → 𝑁 ∥ 0)
Theorem	negdvdsb 11814	An integer divides another iff its negation does. (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ∥ 𝑁 ↔ -𝑀 ∥ 𝑁))
Theorem	dvdsnegb 11815	An integer divides another iff it divides its negation. (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ∥ 𝑁 ↔ 𝑀 ∥ -𝑁))
Theorem	absdvdsb 11816	An integer divides another iff its absolute value does. (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ∥ 𝑁 ↔ (abs‘𝑀) ∥ 𝑁))
Theorem	dvdsabsb 11817	An integer divides another iff it divides its absolute value. (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ∥ 𝑁 ↔ 𝑀 ∥ (abs‘𝑁)))
Theorem	0dvds 11818	Only 0 is divisible by 0. Theorem 1.1(h) in [ApostolNT] p. 14. (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ (𝑁 ∈ ℤ → (0 ∥ 𝑁 ↔ 𝑁 = 0))
Theorem	zdvdsdc 11819	Divisibility of integers is decidable. (Contributed by Jim Kingdon, 17-Jan-2022.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → DECID 𝑀 ∥ 𝑁)
Theorem	dvdsmul1 11820	An integer divides a multiple of itself. (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑀 ∥ (𝑀 · 𝑁))
Theorem	dvdsmul2 11821	An integer divides a multiple of itself. (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑁 ∥ (𝑀 · 𝑁))
Theorem	iddvdsexp 11822	An integer divides a positive integer power of itself. (Contributed by Paul Chapman, 26-Oct-2012.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 𝑀 ∥ (𝑀↑𝑁))
Theorem	muldvds1 11823	If a product divides an integer, so does one of its factors. (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐾 · 𝑀) ∥ 𝑁 → 𝐾 ∥ 𝑁))
Theorem	muldvds2 11824	If a product divides an integer, so does one of its factors. (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐾 · 𝑀) ∥ 𝑁 → 𝑀 ∥ 𝑁))
Theorem	dvdscmul 11825	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.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑀 ∥ 𝑁 → (𝐾 · 𝑀) ∥ (𝐾 · 𝑁)))
Theorem	dvdsmulc 11826	Multiplication by a constant maintains the divides relation. (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑀 ∥ 𝑁 → (𝑀 · 𝐾) ∥ (𝑁 · 𝐾)))
Theorem	dvdscmulr 11827	Cancellation law for the divides relation. Theorem 1.1(e) in [ApostolNT] p. 14. (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝐾 ∈ ℤ ∧ 𝐾 ≠ 0)) → ((𝐾 · 𝑀) ∥ (𝐾 · 𝑁) ↔ 𝑀 ∥ 𝑁))
Theorem	dvdsmulcr 11828	Cancellation law for the divides relation. (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝐾 ∈ ℤ ∧ 𝐾 ≠ 0)) → ((𝑀 · 𝐾) ∥ (𝑁 · 𝐾) ↔ 𝑀 ∥ 𝑁))
Theorem	summodnegmod 11829	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.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((𝐴 + 𝐵) mod 𝑁) = 0 ↔ (𝐴 mod 𝑁) = (-𝐵 mod 𝑁)))
Theorem	modmulconst 11830	Constant multiplication in a modulo operation, see theorem 5.3 in [ApostolNT] p. 108. (Contributed by AV, 21-Jul-2021.)
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ) ∧ 𝑀 ∈ ℕ) → ((𝐴 mod 𝑀) = (𝐵 mod 𝑀) ↔ ((𝐶 · 𝐴) mod (𝐶 · 𝑀)) = ((𝐶 · 𝐵) mod (𝐶 · 𝑀))))
Theorem	dvds2ln 11831	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.)
⊢ (((𝐼 ∈ ℤ ∧ 𝐽 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → ((𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁) → 𝐾 ∥ ((𝐼 · 𝑀) + (𝐽 · 𝑁))))
Theorem	dvds2add 11832	If an integer divides each of two other integers, it divides their sum. (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁) → 𝐾 ∥ (𝑀 + 𝑁)))
Theorem	dvds2sub 11833	If an integer divides each of two other integers, it divides their difference. (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁) → 𝐾 ∥ (𝑀 − 𝑁)))
Theorem	dvds2subd 11834	Deduction form of dvds2sub 11833. (Contributed by Stanislas Polu, 9-Mar-2020.)
⊢ (𝜑 → 𝐾 ∈ ℤ)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ (𝜑 → 𝐾 ∥ 𝑀)    &   ⊢ (𝜑 → 𝐾 ∥ 𝑁)    ⇒   ⊢ (𝜑 → 𝐾 ∥ (𝑀 − 𝑁))
Theorem	dvdstr 11835	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.)
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐾 ∥ 𝑀 ∧ 𝑀 ∥ 𝑁) → 𝐾 ∥ 𝑁))
Theorem	dvds2addd 11836	Deduction form of dvds2add 11832. (Contributed by SN, 21-Aug-2024.)
⊢ (𝜑 → 𝐾 ∈ ℤ)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ (𝜑 → 𝐾 ∥ 𝑀)    &   ⊢ (𝜑 → 𝐾 ∥ 𝑁)    ⇒   ⊢ (𝜑 → 𝐾 ∥ (𝑀 + 𝑁))
Theorem	dvdstrd 11837	The divides relation is transitive, a deduction version of dvdstr 11835. (Contributed by metakunt, 12-May-2024.)
⊢ (𝜑 → 𝐾 ∈ ℤ)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ (𝜑 → 𝐾 ∥ 𝑀)    &   ⊢ (𝜑 → 𝑀 ∥ 𝑁)    ⇒   ⊢ (𝜑 → 𝐾 ∥ 𝑁)
Theorem	dvdsmultr1 11838	If an integer divides another, it divides a multiple of it. (Contributed by Paul Chapman, 17-Nov-2012.)
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 ∥ 𝑀 → 𝐾 ∥ (𝑀 · 𝑁)))
Theorem	dvdsmultr1d 11839	Natural deduction form of dvdsmultr1 11838. (Contributed by Stanislas Polu, 9-Mar-2020.)
⊢ (𝜑 → 𝐾 ∈ ℤ)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ (𝜑 → 𝐾 ∥ 𝑀)    ⇒   ⊢ (𝜑 → 𝐾 ∥ (𝑀 · 𝑁))
Theorem	dvdsmultr2 11840	If an integer divides another, it divides a multiple of it. (Contributed by Paul Chapman, 17-Nov-2012.)
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 ∥ 𝑁 → 𝐾 ∥ (𝑀 · 𝑁)))
Theorem	ordvdsmul 11841	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.)
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐾 ∥ 𝑀 ∨ 𝐾 ∥ 𝑁) → 𝐾 ∥ (𝑀 · 𝑁)))
Theorem	dvdssub2 11842	If an integer divides a difference, then it divides one term iff it divides the other. (Contributed by Mario Carneiro, 13-Jul-2014.)
⊢ (((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐾 ∥ (𝑀 − 𝑁)) → (𝐾 ∥ 𝑀 ↔ 𝐾 ∥ 𝑁))
Theorem	dvdsadd 11843	An integer divides another iff it divides their sum. (Contributed by Paul Chapman, 31-Mar-2011.) (Revised by Mario Carneiro, 13-Jul-2014.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ∥ 𝑁 ↔ 𝑀 ∥ (𝑀 + 𝑁)))
Theorem	dvdsaddr 11844	An integer divides another iff it divides their sum. (Contributed by Paul Chapman, 31-Mar-2011.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ∥ 𝑁 ↔ 𝑀 ∥ (𝑁 + 𝑀)))
Theorem	dvdssub 11845	An integer divides another iff it divides their difference. (Contributed by Paul Chapman, 31-Mar-2011.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ∥ 𝑁 ↔ 𝑀 ∥ (𝑀 − 𝑁)))
Theorem	dvdssubr 11846	An integer divides another iff it divides their difference. (Contributed by Paul Chapman, 31-Mar-2011.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ∥ 𝑁 ↔ 𝑀 ∥ (𝑁 − 𝑀)))
Theorem	dvdsadd2b 11847	Adding a multiple of the base does not affect divisibility. (Contributed by Stefan O'Rear, 23-Sep-2014.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ (𝐶 ∈ ℤ ∧ 𝐴 ∥ 𝐶)) → (𝐴 ∥ 𝐵 ↔ 𝐴 ∥ (𝐶 + 𝐵)))
Theorem	dvdsaddre2b 11848	Adding a multiple of the base does not affect divisibility. Variant of dvdsadd2b 11847 only requiring 𝐵 to be a real number (not necessarily an integer). (Contributed by AV, 19-Jul-2021.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℤ ∧ 𝐴 ∥ 𝐶)) → (𝐴 ∥ 𝐵 ↔ 𝐴 ∥ (𝐶 + 𝐵)))
Theorem	dvdslelemd 11849	Lemma for dvdsle 11850. (Contributed by Jim Kingdon, 8-Nov-2021.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐾 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 < 𝑀)    ⇒   ⊢ (𝜑 → (𝐾 · 𝑀) ≠ 𝑁)
Theorem	dvdsle 11850	The divisors of a positive integer are bounded by it. The proof does not use /. (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑀 ∥ 𝑁 → 𝑀 ≤ 𝑁))
Theorem	dvdsleabs 11851	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.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (𝑀 ∥ 𝑁 → 𝑀 ≤ (abs‘𝑁)))
Theorem	dvdsleabs2 11852	Transfer divisibility to an order constraint on absolute values. (Contributed by Stefan O'Rear, 24-Sep-2014.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (𝑀 ∥ 𝑁 → (abs‘𝑀) ≤ (abs‘𝑁)))
Theorem	dvdsabseq 11853	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.)
⊢ ((𝑀 ∥ 𝑁 ∧ 𝑁 ∥ 𝑀) → (abs‘𝑀) = (abs‘𝑁))
Theorem	dvdseq 11854	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.)
⊢ (((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ (𝑀 ∥ 𝑁 ∧ 𝑁 ∥ 𝑀)) → 𝑀 = 𝑁)
Theorem	divconjdvds 11855	If a nonzero integer 𝑀 divides another integer 𝑁, the other integer 𝑁 divided by the nonzero integer 𝑀 (i.e. the divisor conjugate of 𝑁 to 𝑀) divides the other integer 𝑁. Theorem 1.1(k) in [ApostolNT] p. 14. (Contributed by AV, 7-Aug-2021.)
⊢ ((𝑀 ∥ 𝑁 ∧ 𝑀 ≠ 0) → (𝑁 / 𝑀) ∥ 𝑁)
Theorem	dvdsdivcl 11856*	The complement of a divisor of 𝑁 is also a divisor of 𝑁. (Contributed by Mario Carneiro, 2-Jul-2015.) (Proof shortened by AV, 9-Aug-2021.)
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → (𝑁 / 𝐴) ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁})
Theorem	dvdsflip 11857*	An involution of the divisors of a number. (Contributed by Stefan O'Rear, 12-Sep-2015.) (Proof shortened by Mario Carneiro, 13-May-2016.)
⊢ 𝐴 = {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}    &   ⊢ 𝐹 = (𝑦 ∈ 𝐴 ↦ (𝑁 / 𝑦))    ⇒   ⊢ (𝑁 ∈ ℕ → 𝐹:𝐴–1-1-onto→𝐴)
Theorem	dvdsssfz1 11858*	The set of divisors of a number is a subset of a finite set. (Contributed by Mario Carneiro, 22-Sep-2014.)
⊢ (𝐴 ∈ ℕ → {𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐴} ⊆ (1...𝐴))
Theorem	dvds1 11859	The only nonnegative integer that divides 1 is 1. (Contributed by Mario Carneiro, 2-Jul-2015.)
⊢ (𝑀 ∈ ℕ0 → (𝑀 ∥ 1 ↔ 𝑀 = 1))
Theorem	alzdvds 11860*	Only 0 is divisible by all integers. (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ (𝑁 ∈ ℤ → (∀𝑥 ∈ ℤ 𝑥 ∥ 𝑁 ↔ 𝑁 = 0))
Theorem	dvdsext 11861*	Poset extensionality for division. (Contributed by Stefan O'Rear, 6-Sep-2015.)
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0) → (𝐴 = 𝐵 ↔ ∀𝑥 ∈ ℕ0 (𝐴 ∥ 𝑥 ↔ 𝐵 ∥ 𝑥)))
Theorem	fzm1ndvds 11862	No number between 1 and 𝑀 − 1 divides 𝑀. (Contributed by Mario Carneiro, 24-Jan-2015.)
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ (1...(𝑀 − 1))) → ¬ 𝑀 ∥ 𝑁)
Theorem	fzo0dvdseq 11863	Zero is the only one of the first 𝐴 nonnegative integers that is divisible by 𝐴. (Contributed by Stefan O'Rear, 6-Sep-2015.)
⊢ (𝐵 ∈ (0..^𝐴) → (𝐴 ∥ 𝐵 ↔ 𝐵 = 0))
Theorem	fzocongeq 11864	Two different elements of a half-open range are not congruent mod its length. (Contributed by Stefan O'Rear, 6-Sep-2015.)
⊢ ((𝐴 ∈ (𝐶..^𝐷) ∧ 𝐵 ∈ (𝐶..^𝐷)) → ((𝐷 − 𝐶) ∥ (𝐴 − 𝐵) ↔ 𝐴 = 𝐵))
Theorem	addmodlteqALT 11865	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 10398 based on the "divides" relation. (Contributed by AV, 14-Mar-2021.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ ((𝐼 ∈ (0..^𝑁) ∧ 𝐽 ∈ (0..^𝑁) ∧ 𝑆 ∈ ℤ) → (((𝐼 + 𝑆) mod 𝑁) = ((𝐽 + 𝑆) mod 𝑁) ↔ 𝐼 = 𝐽))
Theorem	dvdsfac 11866	A positive integer divides any greater factorial. (Contributed by Paul Chapman, 28-Nov-2012.)
⊢ ((𝐾 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘𝐾)) → 𝐾 ∥ (!‘𝑁))
Theorem	dvdsexp 11867	A power divides a power with a greater exponent. (Contributed by Mario Carneiro, 23-Feb-2014.)
⊢ ((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ (ℤ≥‘𝑀)) → (𝐴↑𝑀) ∥ (𝐴↑𝑁))
Theorem	dvdsmod 11868	Any number 𝐾 whose mod base 𝑁 is divisible by a divisor 𝑃 of the base is also divisible by 𝑃. This means that primes will also be relatively prime to the base when reduced mod 𝑁 for any base. (Contributed by Mario Carneiro, 13-Mar-2014.)
⊢ (((𝑃 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝐾 ∈ ℤ) ∧ 𝑃 ∥ 𝑁) → (𝑃 ∥ (𝐾 mod 𝑁) ↔ 𝑃 ∥ 𝐾))
Theorem	mulmoddvds 11869	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.)
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝑁 ∥ 𝐴 → ((𝐴 · 𝐵) mod 𝑁) = 0))
Theorem	3dvdsdec 11870	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 𝐴 and 𝐵 actually are digits (i.e. nonnegative integers less than 10). However, this theorem holds for arbitrary nonnegative integers 𝐴 and 𝐵, especially if 𝐴 is itself a decimal number, e.g., 𝐴 = ;𝐶𝐷. (Contributed by AV, 14-Jun-2021.) (Revised by AV, 8-Sep-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    ⇒   ⊢ (3 ∥ ;𝐴𝐵 ↔ 3 ∥ (𝐴 + 𝐵))
Theorem	3dvds2dec 11871	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 𝐴, 𝐵 and 𝐶 actually are digits (i.e. nonnegative integers less than 10). However, this theorem holds for arbitrary nonnegative integers 𝐴, 𝐵 and 𝐶. (Contributed by AV, 14-Jun-2021.) (Revised by AV, 1-Aug-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    ⇒   ⊢ (3 ∥ ;;𝐴𝐵𝐶 ↔ 3 ∥ ((𝐴 + 𝐵) + 𝐶))
5.1.2  Even and odd numbers The set ℤ of integers can be partitioned into the set of even numbers and the set of odd numbers, see zeo4 11875. Instead of defining new class variables Even and Odd to represent these sets, we use the idiom 2 ∥ 𝑁 to say that "𝑁 is even" (which implies 𝑁 ∈ ℤ, see evenelz 11872) and ¬ 2 ∥ 𝑁 to say that "𝑁 is odd" (under the assumption that 𝑁 ∈ ℤ). The previously proven theorems about even and odd numbers, like zneo 9354, zeo 9358, zeo2 9359, etc. use different representations, which are equivalent with the representations using the divides relation, see evend2 11894 and oddp1d2 11895. The corresponding theorems are zeneo 11876, zeo3 11873 and zeo4 11875.
Theorem	evenelz 11872	An even number is an integer. This follows immediately from the reverse closure of the divides relation, see dvdszrcl 11799. (Contributed by AV, 22-Jun-2021.)
⊢ (2 ∥ 𝑁 → 𝑁 ∈ ℤ)
Theorem	zeo3 11873	An integer is even or odd. (Contributed by AV, 17-Jun-2021.)
⊢ (𝑁 ∈ ℤ → (2 ∥ 𝑁 ∨ ¬ 2 ∥ 𝑁))
Theorem	zeoxor 11874	An integer is even or odd but not both. (Contributed by Jim Kingdon, 10-Nov-2021.)
⊢ (𝑁 ∈ ℤ → (2 ∥ 𝑁 ⊻ ¬ 2 ∥ 𝑁))
Theorem	zeo4 11875	An integer is even or odd but not both. (Contributed by AV, 17-Jun-2021.)
⊢ (𝑁 ∈ ℤ → (2 ∥ 𝑁 ↔ ¬ ¬ 2 ∥ 𝑁))
Theorem	zeneo 11876	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 9354 follows immediately from the fact that a contradiction implies anything, see pm2.21i 646. (Contributed by AV, 22-Jun-2021.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((2 ∥ 𝐴 ∧ ¬ 2 ∥ 𝐵) → 𝐴 ≠ 𝐵))
Theorem	odd2np1lem 11877*	Lemma for odd2np1 11878. (Contributed by Scott Fenton, 3-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ (𝑁 ∈ ℕ0 → (∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁 ∨ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁))
Theorem	odd2np1 11878*	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.)
⊢ (𝑁 ∈ ℤ → (¬ 2 ∥ 𝑁 ↔ ∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁))
Theorem	even2n 11879*	An integer is even iff it is twice another integer. (Contributed by AV, 25-Jun-2020.)
⊢ (2 ∥ 𝑁 ↔ ∃𝑛 ∈ ℤ (2 · 𝑛) = 𝑁)
Theorem	oddm1even 11880	An integer is odd iff its predecessor is even. (Contributed by Mario Carneiro, 5-Sep-2016.)
⊢ (𝑁 ∈ ℤ → (¬ 2 ∥ 𝑁 ↔ 2 ∥ (𝑁 − 1)))
Theorem	oddp1even 11881	An integer is odd iff its successor is even. (Contributed by Mario Carneiro, 5-Sep-2016.)
⊢ (𝑁 ∈ ℤ → (¬ 2 ∥ 𝑁 ↔ 2 ∥ (𝑁 + 1)))
Theorem	oexpneg 11882	The exponential of the negative of a number, when the exponent is odd. (Contributed by Mario Carneiro, 25-Apr-2015.)
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁) → (-𝐴↑𝑁) = -(𝐴↑𝑁))
Theorem	mod2eq0even 11883	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.)
⊢ (𝑁 ∈ ℤ → ((𝑁 mod 2) = 0 ↔ 2 ∥ 𝑁))
Theorem	mod2eq1n2dvds 11884	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.)
⊢ (𝑁 ∈ ℤ → ((𝑁 mod 2) = 1 ↔ ¬ 2 ∥ 𝑁))
Theorem	oddnn02np1 11885*	A nonnegative integer is odd iff it is one plus twice another nonnegative integer. (Contributed by AV, 19-Jun-2021.)
⊢ (𝑁 ∈ ℕ0 → (¬ 2 ∥ 𝑁 ↔ ∃𝑛 ∈ ℕ0 ((2 · 𝑛) + 1) = 𝑁))
Theorem	oddge22np1 11886*	An integer greater than one is odd iff it is one plus twice a positive integer. (Contributed by AV, 16-Aug-2021.)
⊢ (𝑁 ∈ (ℤ≥‘2) → (¬ 2 ∥ 𝑁 ↔ ∃𝑛 ∈ ℕ ((2 · 𝑛) + 1) = 𝑁))
Theorem	evennn02n 11887*	A nonnegative integer is even iff it is twice another nonnegative integer. (Contributed by AV, 12-Aug-2021.)
⊢ (𝑁 ∈ ℕ0 → (2 ∥ 𝑁 ↔ ∃𝑛 ∈ ℕ0 (2 · 𝑛) = 𝑁))
Theorem	evennn2n 11888*	A positive integer is even iff it is twice another positive integer. (Contributed by AV, 12-Aug-2021.)
⊢ (𝑁 ∈ ℕ → (2 ∥ 𝑁 ↔ ∃𝑛 ∈ ℕ (2 · 𝑛) = 𝑁))
Theorem	2tp1odd 11889	A number which is twice an integer increased by 1 is odd. (Contributed by AV, 16-Jul-2021.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 = ((2 · 𝐴) + 1)) → ¬ 2 ∥ 𝐵)
Theorem	mulsucdiv2z 11890	An integer multiplied with its successor divided by 2 yields an integer, i.e. an integer multiplied with its successor is even. (Contributed by AV, 19-Jul-2021.)
⊢ (𝑁 ∈ ℤ → ((𝑁 · (𝑁 + 1)) / 2) ∈ ℤ)
Theorem	sqoddm1div8z 11891	A squared odd number minus 1 divided by 8 is an integer. (Contributed by AV, 19-Jul-2021.)
⊢ ((𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁) → (((𝑁↑2) − 1) / 8) ∈ ℤ)
Theorem	2teven 11892	A number which is twice an integer is even. (Contributed by AV, 16-Jul-2021.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 = (2 · 𝐴)) → 2 ∥ 𝐵)
Theorem	zeo5 11893	An integer is either even or odd, version of zeo3 11873 avoiding the negation of the representation of an odd number. (Proposed by BJ, 21-Jun-2021.) (Contributed by AV, 26-Jun-2020.)
⊢ (𝑁 ∈ ℤ → (2 ∥ 𝑁 ∨ 2 ∥ (𝑁 + 1)))
Theorem	evend2 11894	An integer is even iff its quotient with 2 is an integer. This is a representation of even numbers without using the divides relation, see zeo 9358 and zeo2 9359. (Contributed by AV, 22-Jun-2021.)
⊢ (𝑁 ∈ ℤ → (2 ∥ 𝑁 ↔ (𝑁 / 2) ∈ ℤ))
Theorem	oddp1d2 11895	An integer is odd iff its successor divided by 2 is an integer. This is a representation of odd numbers without using the divides relation, see zeo 9358 and zeo2 9359. (Contributed by AV, 22-Jun-2021.)
⊢ (𝑁 ∈ ℤ → (¬ 2 ∥ 𝑁 ↔ ((𝑁 + 1) / 2) ∈ ℤ))
Theorem	zob 11896	Alternate characterizations of an odd number. (Contributed by AV, 7-Jun-2020.)
⊢ (𝑁 ∈ ℤ → (((𝑁 + 1) / 2) ∈ ℤ ↔ ((𝑁 − 1) / 2) ∈ ℤ))
Theorem	oddm1d2 11897	An integer is odd iff its predecessor divided by 2 is an integer. This is another representation of odd numbers without using the divides relation. (Contributed by AV, 18-Jun-2021.) (Proof shortened by AV, 22-Jun-2021.)
⊢ (𝑁 ∈ ℤ → (¬ 2 ∥ 𝑁 ↔ ((𝑁 − 1) / 2) ∈ ℤ))
Theorem	ltoddhalfle 11898	An integer is less than half of an odd number iff it is less than or equal to the half of the predecessor of the odd number (which is an even number). (Contributed by AV, 29-Jun-2021.)
⊢ ((𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ∧ 𝑀 ∈ ℤ) → (𝑀 < (𝑁 / 2) ↔ 𝑀 ≤ ((𝑁 − 1) / 2)))
Theorem	halfleoddlt 11899	An integer is greater than half of an odd number iff it is greater than or equal to the half of the odd number. (Contributed by AV, 1-Jul-2021.)
⊢ ((𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ∧ 𝑀 ∈ ℤ) → ((𝑁 / 2) ≤ 𝑀 ↔ (𝑁 / 2) < 𝑀))
Theorem	opoe 11900	The sum of two odds is even. (Contributed by Scott Fenton, 7-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ (((𝐴 ∈ ℤ ∧ ¬ 2 ∥ 𝐴) ∧ (𝐵 ∈ ℤ ∧ ¬ 2 ∥ 𝐵)) → 2 ∥ (𝐴 + 𝐵))