P. 162 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 16101-16200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	dvdscmulr 16101	Cancellation law for the divides relation. Theorem 1.1(e) in [ApostolNT] p. 14. (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝐾 ∈ ℤ ∧ 𝐾 ≠ 0)) → ((𝐾 · 𝑀) ∥ (𝐾 · 𝑁) ↔ 𝑀 ∥ 𝑁))
Theorem	dvdsmulcr 16102	Cancellation law for the divides relation. (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝐾 ∈ ℤ ∧ 𝐾 ≠ 0)) → ((𝑀 · 𝐾) ∥ (𝑁 · 𝐾) ↔ 𝑀 ∥ 𝑁))
Theorem	summodnegmod 16103	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 16104	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 16105	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 16106	If an integer divides each of two other integers, it divides their sum. (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁) → 𝐾 ∥ (𝑀 + 𝑁)))
Theorem	dvds2sub 16107	If an integer divides each of two other integers, it divides their difference. (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁) → 𝐾 ∥ (𝑀 − 𝑁)))
Theorem	dvds2addd 16108	Deduction form of dvds2add 16106. (Contributed by SN, 21-Aug-2024.)
⊢ (𝜑 → 𝐾 ∈ ℤ)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ (𝜑 → 𝐾 ∥ 𝑀)    &   ⊢ (𝜑 → 𝐾 ∥ 𝑁)    ⇒   ⊢ (𝜑 → 𝐾 ∥ (𝑀 + 𝑁))
Theorem	dvds2subd 16109	Deduction form of dvds2sub 16107. (Contributed by Stanislas Polu, 9-Mar-2020.)
⊢ (𝜑 → 𝐾 ∈ ℤ)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ (𝜑 → 𝐾 ∥ 𝑀)    &   ⊢ (𝜑 → 𝐾 ∥ 𝑁)    ⇒   ⊢ (𝜑 → 𝐾 ∥ (𝑀 − 𝑁))
Theorem	dvdstr 16110	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	dvdstrd 16111	The divides relation is transitive, a deduction version of dvdstr 16110. (Contributed by metakunt, 12-May-2024.)
⊢ (𝜑 → 𝐾 ∈ ℤ)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ (𝜑 → 𝐾 ∥ 𝑀)    &   ⊢ (𝜑 → 𝑀 ∥ 𝑁)    ⇒   ⊢ (𝜑 → 𝐾 ∥ 𝑁)
Theorem	dvdsmultr1 16112	If an integer divides another, it divides a multiple of it. (Contributed by Paul Chapman, 17-Nov-2012.)
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 ∥ 𝑀 → 𝐾 ∥ (𝑀 · 𝑁)))
Theorem	dvdsmultr1d 16113	Deduction form of dvdsmultr1 16112. (Contributed by Stanislas Polu, 9-Mar-2020.)
⊢ (𝜑 → 𝐾 ∈ ℤ)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ (𝜑 → 𝐾 ∥ 𝑀)    ⇒   ⊢ (𝜑 → 𝐾 ∥ (𝑀 · 𝑁))
Theorem	dvdsmultr2 16114	If an integer divides another, it divides a multiple of it. (Contributed by Paul Chapman, 17-Nov-2012.)
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 ∥ 𝑁 → 𝐾 ∥ (𝑀 · 𝑁)))
Theorem	dvdsmultr2d 16115	Deduction form of dvdsmultr2 16114. (Contributed by SN, 23-Aug-2024.)
⊢ (𝜑 → 𝐾 ∈ ℤ)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ (𝜑 → 𝐾 ∥ 𝑁)    ⇒   ⊢ (𝜑 → 𝐾 ∥ (𝑀 · 𝑁))
Theorem	ordvdsmul 16116	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 16117	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 16118	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 16119	An integer divides another iff it divides their sum. (Contributed by Paul Chapman, 31-Mar-2011.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ∥ 𝑁 ↔ 𝑀 ∥ (𝑁 + 𝑀)))
Theorem	dvdssub 16120	An integer divides another iff it divides their difference. (Contributed by Paul Chapman, 31-Mar-2011.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ∥ 𝑁 ↔ 𝑀 ∥ (𝑀 − 𝑁)))
Theorem	dvdssubr 16121	An integer divides another iff it divides their difference. (Contributed by Paul Chapman, 31-Mar-2011.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ∥ 𝑁 ↔ 𝑀 ∥ (𝑁 − 𝑀)))
Theorem	dvdsadd2b 16122	Adding a multiple of the base does not affect divisibility. (Contributed by Stefan O'Rear, 23-Sep-2014.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ (𝐶 ∈ ℤ ∧ 𝐴 ∥ 𝐶)) → (𝐴 ∥ 𝐵 ↔ 𝐴 ∥ (𝐶 + 𝐵)))
Theorem	dvdsaddre2b 16123	Adding a multiple of the base does not affect divisibility. Variant of dvdsadd2b 16122 only requiring 𝐵 to be a real number (not necessarily an integer). (Contributed by AV, 19-Jul-2021.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℤ ∧ 𝐴 ∥ 𝐶)) → (𝐴 ∥ 𝐵 ↔ 𝐴 ∥ (𝐶 + 𝐵)))
Theorem	fsumdvds 16124*	If every term in a sum is divisible by 𝑁, then so is the sum. (Contributed by Mario Carneiro, 17-Jan-2015.)
⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℤ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑁 ∥ 𝐵)    ⇒   ⊢ (𝜑 → 𝑁 ∥ Σ𝑘 ∈ 𝐴 𝐵)
Theorem	dvdslelem 16125	Lemma for dvdsle 16126. (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ 𝑀 ∈ ℤ    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝐾 ∈ ℤ    ⇒   ⊢ (𝑁 < 𝑀 → (𝐾 · 𝑀) ≠ 𝑁)
Theorem	dvdsle 16126	The divisors of a positive integer are bounded by it. The proof does not use /. (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑀 ∥ 𝑁 → 𝑀 ≤ 𝑁))
Theorem	dvdsleabs 16127	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 16128	Transfer divisibility to an order constraint on absolute values. (Contributed by Stefan O'Rear, 24-Sep-2014.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (𝑀 ∥ 𝑁 → (abs‘𝑀) ≤ (abs‘𝑁)))
Theorem	dvdsabseq 16129	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 16130	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 16131	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 16132*	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 16133*	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 16134*	The set of divisors of a number is a subset of a finite set. (Contributed by Mario Carneiro, 22-Sep-2014.)
⊢ (𝐴 ∈ ℕ → {𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐴} ⊆ (1...𝐴))
Theorem	dvds1 16135	The only nonnegative integer that divides 1 is 1. (Contributed by Mario Carneiro, 2-Jul-2015.)
⊢ (𝑀 ∈ ℕ0 → (𝑀 ∥ 1 ↔ 𝑀 = 1))
Theorem	alzdvds 16136*	Only 0 is divisible by all integers. (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ (𝑁 ∈ ℤ → (∀𝑥 ∈ ℤ 𝑥 ∥ 𝑁 ↔ 𝑁 = 0))
Theorem	dvdsext 16137*	Poset extensionality for division. (Contributed by Stefan O'Rear, 6-Sep-2015.)
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0) → (𝐴 = 𝐵 ↔ ∀𝑥 ∈ ℕ0 (𝐴 ∥ 𝑥 ↔ 𝐵 ∥ 𝑥)))
Theorem	fzm1ndvds 16138	No number between 1 and 𝑀 − 1 divides 𝑀. (Contributed by Mario Carneiro, 24-Jan-2015.)
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ (1...(𝑀 − 1))) → ¬ 𝑀 ∥ 𝑁)
Theorem	fzo0dvdseq 16139	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 16140	Two different elements of a half-open range are not congruent mod its length. (Contributed by Stefan O'Rear, 6-Sep-2015.)
⊢ ((𝐴 ∈ (𝐶..^𝐷) ∧ 𝐵 ∈ (𝐶..^𝐷)) → ((𝐷 − 𝐶) ∥ (𝐴 − 𝐵) ↔ 𝐴 = 𝐵))
Theorem	addmodlteqALT 16141	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 13779 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 16142	A positive integer divides any greater factorial. (Contributed by Paul Chapman, 28-Nov-2012.)
⊢ ((𝐾 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘𝐾)) → 𝐾 ∥ (!‘𝑁))
Theorem	dvdsexp2im 16143	If an integer divides another integer, then it also divides any of its powers. (Contributed by Scott Fenton, 7-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝐾 ∥ 𝑀 → 𝐾 ∥ (𝑀↑𝑁)))
Theorem	dvdsexp 16144	A power divides a power with a greater exponent. (Contributed by Mario Carneiro, 23-Feb-2014.)
⊢ ((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ (ℤ≥‘𝑀)) → (𝐴↑𝑀) ∥ (𝐴↑𝑁))
Theorem	dvdsmod 16145	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 16146	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.) (Proof shortened by AV, 18-Mar-2022.)
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝑁 ∥ 𝐴 → ((𝐴 · 𝐵) mod 𝑁) = 0))
Theorem	3dvds 16147*	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.)
⊢ ((𝑁 ∈ ℕ0 ∧ 𝐹:(0...𝑁)⟶ℤ) → (3 ∥ Σ𝑘 ∈ (0...𝑁)((𝐹‘𝑘) · (;10↑𝑘)) ↔ 3 ∥ Σ𝑘 ∈ (0...𝑁)(𝐹‘𝑘)))
Theorem	3dvdsdec 16148	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 16149	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 ∥ ((𝐴 + 𝐵) + 𝐶))
Theorem	fprodfvdvdsd 16150*	A finite product of integers is divisible by any of its factors being function values. (Contributed by AV, 1-Aug-2021.)
⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐵)    &   ⊢ (𝜑 → 𝐹:𝐵⟶ℤ)    ⇒   ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∥ ∏𝑘 ∈ 𝐴 (𝐹‘𝑘))
Theorem	fproddvdsd 16151*	A finite product of integers is divisible by any of its factors. (Contributed by AV, 14-Aug-2020.) (Proof shortened by AV, 2-Aug-2021.)
⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐴 ⊆ ℤ)    ⇒   ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝑥 ∥ ∏𝑘 ∈ 𝐴 𝑘)
6.1.4  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 16154. 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 16152) and ¬ 2 ∥ 𝑁 to say that "𝑁 is odd" (under the assumption that 𝑁 ∈ ℤ). The previously proven theorems about even and odd numbers, like zneo 12516, zeo 12519, zeo2 12520, etc. use different representations, which are equivalent to the representations using the divides relation, see evend2 16173 and oddp1d2 16174. The corresponding theorems are zeneo 16155, zeo3 16153 and zeo4 16154.
Theorem	evenelz 16152	An even number is an integer. This follows immediately from the reverse closure of the divides relation, see dvdszrcl 16075. (Contributed by AV, 22-Jun-2021.)
⊢ (2 ∥ 𝑁 → 𝑁 ∈ ℤ)
Theorem	zeo3 16153	An integer is even or odd. With this representation of even and odd integers, this variant of zeo 12519 follows immediately from the law of excluded middle, see exmidd 894. (Contributed by AV, 17-Jun-2021.)
⊢ (𝑁 ∈ ℤ → (2 ∥ 𝑁 ∨ ¬ 2 ∥ 𝑁))
Theorem	zeo4 16154	An integer is even or odd but not both. With this representation of even and odd integers, this variant of zeo2 12520 follows immediately from the principle of double negation, see notnotb 315. (Contributed by AV, 17-Jun-2021.)
⊢ (𝑁 ∈ ℤ → (2 ∥ 𝑁 ↔ ¬ ¬ 2 ∥ 𝑁))
Theorem	zeneo 16155	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 12516 follows immediately from the fact that a contradiction implies anything, see pm2.21i 119. (Contributed by AV, 22-Jun-2021.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((2 ∥ 𝐴 ∧ ¬ 2 ∥ 𝐵) → 𝐴 ≠ 𝐵))
Theorem	odd2np1lem 16156*	Lemma for odd2np1 16157. (Contributed by Scott Fenton, 3-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ (𝑁 ∈ ℕ0 → (∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁 ∨ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁))
Theorem	odd2np1 16157*	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 16158*	An integer is even iff it is twice another integer. (Contributed by AV, 25-Jun-2020.)
⊢ (2 ∥ 𝑁 ↔ ∃𝑛 ∈ ℤ (2 · 𝑛) = 𝑁)
Theorem	oddm1even 16159	An integer is odd iff its predecessor is even. (Contributed by Mario Carneiro, 5-Sep-2016.)
⊢ (𝑁 ∈ ℤ → (¬ 2 ∥ 𝑁 ↔ 2 ∥ (𝑁 − 1)))
Theorem	oddp1even 16160	An integer is odd iff its successor is even. (Contributed by Mario Carneiro, 5-Sep-2016.)
⊢ (𝑁 ∈ ℤ → (¬ 2 ∥ 𝑁 ↔ 2 ∥ (𝑁 + 1)))
Theorem	oexpneg 16161	The exponential of the negative of a number, when the exponent is odd. (Contributed by Mario Carneiro, 25-Apr-2015.) (Proof shortened by AV, 10-Jul-2022.)
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁) → (-𝐴↑𝑁) = -(𝐴↑𝑁))
Theorem	mod2eq0even 16162	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 16163	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.) (Proof shortened by AV, 5-Jul-2020.)
⊢ (𝑁 ∈ ℤ → ((𝑁 mod 2) = 1 ↔ ¬ 2 ∥ 𝑁))
Theorem	oddnn02np1 16164*	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 16165*	An integer greater than one is odd iff it is one plus twice a positive integer. (Contributed by AV, 16-Aug-2021.) (Proof shortened by AV, 9-Jul-2022.)
⊢ (𝑁 ∈ (ℤ≥‘2) → (¬ 2 ∥ 𝑁 ↔ ∃𝑛 ∈ ℕ ((2 · 𝑛) + 1) = 𝑁))
Theorem	evennn02n 16166*	A nonnegative integer is even iff it is twice another nonnegative integer. (Contributed by AV, 12-Aug-2021.) (Proof shortened by AV, 10-Jul-2022.)
⊢ (𝑁 ∈ ℕ0 → (2 ∥ 𝑁 ↔ ∃𝑛 ∈ ℕ0 (2 · 𝑛) = 𝑁))
Theorem	evennn2n 16167*	A positive integer is even iff it is twice another positive integer. (Contributed by AV, 12-Aug-2021.)
⊢ (𝑁 ∈ ℕ → (2 ∥ 𝑁 ↔ ∃𝑛 ∈ ℕ (2 · 𝑛) = 𝑁))
Theorem	2tp1odd 16168	A number which is twice an integer increased by 1 is odd. (Contributed by AV, 16-Jul-2021.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 = ((2 · 𝐴) + 1)) → ¬ 2 ∥ 𝐵)
Theorem	mulsucdiv2z 16169	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 16170	A squared odd number minus 1 divided by 8 is an integer. (Contributed by AV, 19-Jul-2021.)
⊢ ((𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁) → (((𝑁↑2) − 1) / 8) ∈ ℤ)
Theorem	2teven 16171	A number which is twice an integer is even. (Contributed by AV, 16-Jul-2021.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 = (2 · 𝐴)) → 2 ∥ 𝐵)
Theorem	zeo5 16172	An integer is either even or odd, version of zeo3 16153 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 16173	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 12519 and zeo2 12520. (Contributed by AV, 22-Jun-2021.)
⊢ (𝑁 ∈ ℤ → (2 ∥ 𝑁 ↔ (𝑁 / 2) ∈ ℤ))
Theorem	oddp1d2 16174	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 12519 and zeo2 12520. (Contributed by AV, 22-Jun-2021.)
⊢ (𝑁 ∈ ℤ → (¬ 2 ∥ 𝑁 ↔ ((𝑁 + 1) / 2) ∈ ℤ))
Theorem	zob 16175	Alternate characterizations of an odd number. (Contributed by AV, 7-Jun-2020.)
⊢ (𝑁 ∈ ℤ → (((𝑁 + 1) / 2) ∈ ℤ ↔ ((𝑁 − 1) / 2) ∈ ℤ))
Theorem	oddm1d2 16176	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 16177	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 16178	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 16179	The sum of two odds is even. (Contributed by Scott Fenton, 7-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ (((𝐴 ∈ ℤ ∧ ¬ 2 ∥ 𝐴) ∧ (𝐵 ∈ ℤ ∧ ¬ 2 ∥ 𝐵)) → 2 ∥ (𝐴 + 𝐵))
Theorem	omoe 16180	The difference of two odds is even. (Contributed by Scott Fenton, 7-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ (((𝐴 ∈ ℤ ∧ ¬ 2 ∥ 𝐴) ∧ (𝐵 ∈ ℤ ∧ ¬ 2 ∥ 𝐵)) → 2 ∥ (𝐴 − 𝐵))
Theorem	opeo 16181	The sum of an odd and an even is odd. (Contributed by Scott Fenton, 7-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ (((𝐴 ∈ ℤ ∧ ¬ 2 ∥ 𝐴) ∧ (𝐵 ∈ ℤ ∧ 2 ∥ 𝐵)) → ¬ 2 ∥ (𝐴 + 𝐵))
Theorem	omeo 16182	The difference of an odd and an even is odd. (Contributed by Scott Fenton, 7-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ (((𝐴 ∈ ℤ ∧ ¬ 2 ∥ 𝐴) ∧ (𝐵 ∈ ℤ ∧ 2 ∥ 𝐵)) → ¬ 2 ∥ (𝐴 − 𝐵))
Theorem	z0even 16183	2 divides 0. That means 0 is even. (Contributed by AV, 11-Feb-2020.) (Revised by AV, 23-Jun-2021.)
⊢ 2 ∥ 0
Theorem	n2dvds1 16184	2 does not divide 1. That means 1 is odd. (Contributed by David A. Wheeler, 8-Dec-2018.) (Proof shortened by Steven Nguyen, 3-May-2023.)
⊢ ¬ 2 ∥ 1
Theorem	n2dvdsm1 16185	2 does not divide -1. That means -1 is odd. (Contributed by AV, 15-Aug-2021.)
⊢ ¬ 2 ∥ -1
Theorem	z2even 16186	2 divides 2. That means 2 is even. (Contributed by AV, 12-Feb-2020.) (Revised by AV, 23-Jun-2021.)
⊢ 2 ∥ 2
Theorem	n2dvds3 16187	2 does not divide 3. That means 3 is odd. (Contributed by AV, 28-Feb-2021.) (Proof shortened by Steven Nguyen, 3-May-2023.)
⊢ ¬ 2 ∥ 3
Theorem	z4even 16188	2 divides 4. That means 4 is even. (Contributed by AV, 23-Jul-2020.) (Revised by AV, 4-Jul-2021.)
⊢ 2 ∥ 4
Theorem	4dvdseven 16189	An integer which is divisible by 4 is divisible by 2, that is, is even. (Contributed by AV, 4-Jul-2021.)
⊢ (4 ∥ 𝑁 → 2 ∥ 𝑁)
Theorem	m1expe 16190	Exponentiation of -1 by an even power. Variant of m1expeven 13943. (Contributed by AV, 25-Jun-2021.)
⊢ (2 ∥ 𝑁 → (-1↑𝑁) = 1)
Theorem	m1expo 16191	Exponentiation of -1 by an odd power. (Contributed by AV, 26-Jun-2021.)
⊢ ((𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁) → (-1↑𝑁) = -1)
Theorem	m1exp1 16192	Exponentiation of negative one is one iff the exponent is even. (Contributed by AV, 20-Jun-2021.)
⊢ (𝑁 ∈ ℤ → ((-1↑𝑁) = 1 ↔ 2 ∥ 𝑁))
Theorem	nn0enne 16193	A positive integer is an even nonnegative integer iff it is an even positive integer. (Contributed by AV, 30-May-2020.)
⊢ (𝑁 ∈ ℕ → ((𝑁 / 2) ∈ ℕ0 ↔ (𝑁 / 2) ∈ ℕ))
Theorem	nn0ehalf 16194	The half of an even nonnegative integer is a nonnegative integer. (Contributed by AV, 22-Jun-2020.) (Revised by AV, 28-Jun-2021.) (Proof shortened by AV, 10-Jul-2022.)
⊢ ((𝑁 ∈ ℕ0 ∧ 2 ∥ 𝑁) → (𝑁 / 2) ∈ ℕ0)
Theorem	nnehalf 16195	The half of an even positive integer is a positive integer. (Contributed by AV, 28-Jun-2021.)
⊢ ((𝑁 ∈ ℕ ∧ 2 ∥ 𝑁) → (𝑁 / 2) ∈ ℕ)
Theorem	nn0onn 16196	An odd nonnegative integer is positive. (Contributed by Steven Nguyen, 25-Mar-2023.)
⊢ ((𝑁 ∈ ℕ0 ∧ ¬ 2 ∥ 𝑁) → 𝑁 ∈ ℕ)
Theorem	nn0o1gt2 16197	An odd nonnegative integer is either 1 or greater than 2. (Contributed by AV, 2-Jun-2020.)
⊢ ((𝑁 ∈ ℕ0 ∧ ((𝑁 + 1) / 2) ∈ ℕ0) → (𝑁 = 1 ∨ 2 < 𝑁))
Theorem	nno 16198	An alternate characterization of an odd integer greater than 1. (Contributed by AV, 2-Jun-2020.) (Proof shortened by AV, 10-Jul-2022.)
⊢ ((𝑁 ∈ (ℤ≥‘2) ∧ ((𝑁 + 1) / 2) ∈ ℕ0) → ((𝑁 − 1) / 2) ∈ ℕ)
Theorem	nn0o 16199	An alternate characterization of an odd nonnegative integer. (Contributed by AV, 28-May-2020.) (Proof shortened by AV, 2-Jun-2020.)
⊢ ((𝑁 ∈ ℕ0 ∧ ((𝑁 + 1) / 2) ∈ ℕ0) → ((𝑁 − 1) / 2) ∈ ℕ0)
Theorem	nn0ob 16200	Alternate characterizations of an odd nonnegative integer. (Contributed by AV, 4-Jun-2020.)
⊢ (𝑁 ∈ ℕ0 → (((𝑁 + 1) / 2) ∈ ℕ0 ↔ ((𝑁 − 1) / 2) ∈ ℕ0))