P. 328 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 32701-32800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ffsrn 32701	The range of a finitely supported function is finite. (Contributed by Thierry Arnoux, 27-Aug-2017.)
⊢ (𝜑 → 𝑍 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑉)    &   ⊢ (𝜑 → Fun 𝐹)    &   ⊢ (𝜑 → (𝐹 supp 𝑍) ∈ Fin)    ⇒   ⊢ (𝜑 → ran 𝐹 ∈ Fin)
Theorem	cocnvf1o 32702	Composing with the inverse of a bijection. (Contributed by Thierry Arnoux, 15-Jan-2026.)
⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝐺:𝐴⟶𝐵)    &   ⊢ (𝜑 → 𝐻:𝐴–1-1-onto→𝐴)    ⇒   ⊢ (𝜑 → (𝐹 = (𝐺 ∘ 𝐻) ↔ 𝐺 = (𝐹 ∘ ◡𝐻)))
Theorem	resf1o 32703*	Restriction of functions to a superset of their support creates a bijection. (Contributed by Thierry Arnoux, 12-Sep-2017.)
⊢ 𝑋 = {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ (◡𝑓 “ (𝐵 ∖ {𝑍})) ⊆ 𝐶}    &   ⊢ 𝐹 = (𝑓 ∈ 𝑋 ↦ (𝑓 ↾ 𝐶))    ⇒   ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ⊆ 𝐴) ∧ 𝑍 ∈ 𝐵) → 𝐹:𝑋–1-1-onto→(𝐵 ↑m 𝐶))
Theorem	maprnin 32704*	Restricting the range of the mapping operator. (Contributed by Thierry Arnoux, 30-Aug-2017.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ ((𝐵 ∩ 𝐶) ↑m 𝐴) = {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ ran 𝑓 ⊆ 𝐶}
Theorem	fpwrelmapffslem 32705*	Lemma for fpwrelmapffs 32707. For this theorem, the sets 𝐴 and 𝐵 could be infinite, but the relation 𝑅 itself is finite. (Contributed by Thierry Arnoux, 1-Sep-2017.) (Revised by Thierry Arnoux, 1-Sep-2019.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝒫 𝐵)    &   ⊢ (𝜑 → 𝑅 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))})    ⇒   ⊢ (𝜑 → (𝑅 ∈ Fin ↔ (ran 𝐹 ⊆ Fin ∧ (𝐹 supp ∅) ∈ Fin)))
Theorem	fpwrelmap 32706*	Define a canonical mapping between functions from 𝐴 into subsets of 𝐵 and the relations with domain 𝐴 and range within 𝐵. Note that the same relation is used in axdc2lem 10331 and marypha2lem1 9314. (Contributed by Thierry Arnoux, 28-Aug-2017.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝑀 = (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))})    ⇒   ⊢ 𝑀:(𝒫 𝐵 ↑m 𝐴)–1-1-onto→𝒫 (𝐴 × 𝐵)
Theorem	fpwrelmapffs 32707*	Define a canonical mapping between finite relations (finite subsets of a cartesian product) and functions with finite support into finite subsets. (Contributed by Thierry Arnoux, 28-Aug-2017.) (Revised by Thierry Arnoux, 1-Sep-2019.)
⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    &   ⊢ 𝑀 = (𝑓 ∈ (𝒫 𝐵 ↑m 𝐴) ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝑓‘𝑥))})    &   ⊢ 𝑆 = {𝑓 ∈ ((𝒫 𝐵 ∩ Fin) ↑m 𝐴) ∣ (𝑓 supp ∅) ∈ Fin}    ⇒   ⊢ (𝑀 ↾ 𝑆):𝑆–1-1-onto→(𝒫 (𝐴 × 𝐵) ∩ Fin)
21.3.5  Real and Complex Numbers
Theorem	sgnval2 32708	Value of the signum of a real number, expresssed using absolute value. (Contributed by Thierry Arnoux, 9-Nov-2025.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) → (sgn‘𝐴) = (𝐴 / (abs‘𝐴)))
21.3.5.1  Complex operations - misc. additions
Theorem	creq0 32709	The real representation of complex numbers is zero iff both its terms are zero. Cf. crne0 12110. (Contributed by Thierry Arnoux, 20-Aug-2023.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 = 0 ∧ 𝐵 = 0) ↔ (𝐴 + (i · 𝐵)) = 0))
Theorem	1nei 32710	The imaginary unit i is not one. (Contributed by Thierry Arnoux, 20-Aug-2023.)
⊢ 1 ≠ i
Theorem	1neg1t1neg1 32711	An integer unit times itself. (Contributed by Thierry Arnoux, 23-Aug-2020.)
⊢ (𝑁 ∈ {-1, 1} → (𝑁 · 𝑁) = 1)
Theorem	nnmulge 32712	Multiplying by a positive integer 𝑀 yields greater than or equal nonnegative integers. (Contributed by Thierry Arnoux, 13-Dec-2021.)
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ0) → 𝑁 ≤ (𝑀 · 𝑁))
Theorem	submuladdd 32713	The product of a difference and a sum. Cf. addmulsub 11571. (Contributed by Thierry Arnoux, 6-Jul-2025.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐷 ∈ ℂ)    ⇒   ⊢ (𝜑 → ((𝐴 − 𝐵) · (𝐶 + 𝐷)) = (((𝐴 · 𝐶) + (𝐴 · 𝐷)) − ((𝐵 · 𝐶) + (𝐵 · 𝐷))))
Theorem	muldivdid 32714	Distribution of division over addition with a multiplication. (Contributed by Thierry Arnoux, 6-Jul-2025.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    ⇒   ⊢ (𝜑 → (((𝐴 · 𝐵) + 𝐶) / 𝐵) = (𝐴 + (𝐶 / 𝐵)))
Theorem	binom2subadd 32715	The difference of the squares of the sum and difference of two complex numbers 𝐴 and 𝐵. (Contributed by Thierry Arnoux, 5-Nov-2025.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (((𝐴 + 𝐵)↑2) − ((𝐴 − 𝐵)↑2)) = (4 · (𝐴 · 𝐵)))
Theorem	cjsubd 32716	Complex conjugate distributes over subtraction. (Contributed by Thierry Arnoux, 1-Jul-2025.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → (∗‘(𝐴 − 𝐵)) = ((∗‘𝐴) − (∗‘𝐵)))
Theorem	re0cj 32717	The conjugate of a pure imaginary number is its negative. (Contributed by Thierry Arnoux, 25-Jun-2025.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → (ℜ‘𝐴) = 0)    ⇒   ⊢ (𝜑 → (∗‘𝐴) = -𝐴)
Theorem	receqid 32718	Real numbers equal to their own reciprocal have absolute value 1. (Contributed by Thierry Arnoux, 9-Nov-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    ⇒   ⊢ (𝜑 → ((1 / 𝐴) = 𝐴 ↔ (abs‘𝐴) = 1))
Theorem	pythagreim 32719	A simplified version of the Pythagorean theorem, where the points 𝐴 and 𝐵 respectively lie on the imaginary and real axes, and the right angle is at the origin. (Contributed by Thierry Arnoux, 2-Nov-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    ⇒   ⊢ (𝜑 → ((abs‘(𝐵 − (i · 𝐴)))↑2) = ((𝐴↑2) + (𝐵↑2)))
Theorem	efiargd 32720	The exponential of the "arg" function ℑ ∘ log, deduction version. (Contributed by Thierry Arnoux, 5-Nov-2025.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    ⇒   ⊢ (𝜑 → (exp‘(i · (ℑ‘(log‘𝐴)))) = (𝐴 / (abs‘𝐴)))
Theorem	arginv 32721	The argument of the inverse of a complex number 𝐴. (Contributed by Thierry Arnoux, 5-Nov-2025.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    &   ⊢ (𝜑 → ¬ -𝐴 ∈ ℝ+)    ⇒   ⊢ (𝜑 → (ℑ‘(log‘(1 / 𝐴))) = -(ℑ‘(log‘𝐴)))
Theorem	argcj 32722	The argument of the conjugate of a complex number 𝐴. (Contributed by Thierry Arnoux, 5-Nov-2025.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    &   ⊢ (𝜑 → ¬ -𝐴 ∈ ℝ+)    ⇒   ⊢ (𝜑 → (ℑ‘(log‘(∗‘𝐴))) = -(ℑ‘(log‘𝐴)))
Theorem	quad3d 32723	Variant of quadratic equation with discriminant expanded. (Contributed by Filip Cernatescu, 19-Oct-2019.) Deduction version. (Revised by Thierry Arnoux, 6-Jul-2025.)
⊢ (𝜑 → 𝑋 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → ((𝐴 · (𝑋↑2)) + ((𝐵 · 𝑋) + 𝐶)) = 0)    ⇒   ⊢ (𝜑 → (𝑋 = ((-𝐵 + (√‘((𝐵↑2) − (4 · (𝐴 · 𝐶))))) / (2 · 𝐴)) ∨ 𝑋 = ((-𝐵 − (√‘((𝐵↑2) − (4 · (𝐴 · 𝐶))))) / (2 · 𝐴))))
21.3.5.2  Ordering on reals - misc additions
Theorem	lt2addrd 32724*	If the right-hand side of a 'less than' relationship is an addition, then we can express the left-hand side as an addition, too, where each term is respectively less than each term of the original right side. (Contributed by Thierry Arnoux, 15-Mar-2017.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < (𝐵 + 𝐶))    ⇒   ⊢ (𝜑 → ∃𝑏 ∈ ℝ ∃𝑐 ∈ ℝ (𝐴 = (𝑏 + 𝑐) ∧ 𝑏 < 𝐵 ∧ 𝑐 < 𝐶))
21.3.5.3  Extended reals - misc additions
Theorem	xrlelttric 32725	Trichotomy law for extended reals. (Contributed by Thierry Arnoux, 12-Sep-2017.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 ≤ 𝐵 ∨ 𝐵 < 𝐴))
Theorem	xaddeq0 32726	Two extended reals which add up to zero are each other's negatives. (Contributed by Thierry Arnoux, 13-Jun-2017.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → ((𝐴 +𝑒 𝐵) = 0 ↔ 𝐴 = -𝑒𝐵))
Theorem	rexmul2 32727	If the result 𝐴 of an extended real multiplication is real, then its first factor 𝐵 is also real. See also rexmul 13162. (Contributed by Thierry Arnoux, 26-Oct-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ*)    &   ⊢ (𝜑 → 0 < 𝐶)    &   ⊢ (𝜑 → 𝐴 = (𝐵 ·e 𝐶))    ⇒   ⊢ (𝜑 → 𝐵 ∈ ℝ)
Theorem	xrinfm 32728	The extended real numbers are unbounded below. (Contributed by Thierry Arnoux, 18-Feb-2018.) (Revised by AV, 28-Sep-2020.)
⊢ inf(ℝ*, ℝ*, < ) = -∞
Theorem	le2halvesd 32729	A sum is less than the whole if each term is less than half. (Contributed by Thierry Arnoux, 29-Nov-2017.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≤ (𝐶 / 2))    &   ⊢ (𝜑 → 𝐵 ≤ (𝐶 / 2))    ⇒   ⊢ (𝜑 → (𝐴 + 𝐵) ≤ 𝐶)
Theorem	xraddge02 32730	A number is less than or equal to itself plus a nonnegative number. (Contributed by Thierry Arnoux, 28-Dec-2016.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (0 ≤ 𝐵 → 𝐴 ≤ (𝐴 +𝑒 𝐵)))
Theorem	xrge0addge 32731	A number is less than or equal to itself plus a nonnegative number. (Contributed by Thierry Arnoux, 19-Jul-2020.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ (0[,]+∞)) → 𝐴 ≤ (𝐴 +𝑒 𝐵))
Theorem	xlt2addrd 32732*	If the right-hand side of a 'less than' relationship is an addition, then we can express the left-hand side as an addition, too, where each term is respectively less than each term of the original right side. (Contributed by Thierry Arnoux, 15-Mar-2017.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ≠ -∞)    &   ⊢ (𝜑 → 𝐶 ≠ -∞)    &   ⊢ (𝜑 → 𝐴 < (𝐵 +𝑒 𝐶))    ⇒   ⊢ (𝜑 → ∃𝑏 ∈ ℝ* ∃𝑐 ∈ ℝ* (𝐴 = (𝑏 +𝑒 𝑐) ∧ 𝑏 < 𝐵 ∧ 𝑐 < 𝐶))
Theorem	xrge0infss 32733*	Any subset of nonnegative extended reals has an infimum. (Contributed by Thierry Arnoux, 16-Sep-2019.) (Revised by AV, 4-Oct-2020.)
⊢ (𝐴 ⊆ (0[,]+∞) → ∃𝑥 ∈ (0[,]+∞)(∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ (0[,]+∞)(𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)))
Theorem	xrge0infssd 32734	Inequality deduction for infimum of a nonnegative extended real subset. (Contributed by Thierry Arnoux, 16-Sep-2019.) (Revised by AV, 4-Oct-2020.)
⊢ (𝜑 → 𝐶 ⊆ 𝐵)    &   ⊢ (𝜑 → 𝐵 ⊆ (0[,]+∞))    ⇒   ⊢ (𝜑 → inf(𝐵, (0[,]+∞), < ) ≤ inf(𝐶, (0[,]+∞), < ))
Theorem	xrge0addcld 32735	Nonnegative extended reals are closed under addition. (Contributed by Thierry Arnoux, 16-Sep-2019.)
⊢ (𝜑 → 𝐴 ∈ (0[,]+∞))    &   ⊢ (𝜑 → 𝐵 ∈ (0[,]+∞))    ⇒   ⊢ (𝜑 → (𝐴 +𝑒 𝐵) ∈ (0[,]+∞))
Theorem	xrge0subcld 32736	Condition for closure of nonnegative extended reals under subtraction. (Contributed by Thierry Arnoux, 27-May-2020.)
⊢ (𝜑 → 𝐴 ∈ (0[,]+∞))    &   ⊢ (𝜑 → 𝐵 ∈ (0[,]+∞))    &   ⊢ (𝜑 → 𝐵 ≤ 𝐴)    ⇒   ⊢ (𝜑 → (𝐴 +𝑒 -𝑒𝐵) ∈ (0[,]+∞))
Theorem	infxrge0lb 32737	A member of a set of nonnegative extended reals is greater than or equal to the set's infimum. (Contributed by Thierry Arnoux, 19-Jul-2020.) (Revised by AV, 4-Oct-2020.)
⊢ (𝜑 → 𝐴 ⊆ (0[,]+∞))    &   ⊢ (𝜑 → 𝐵 ∈ 𝐴)    ⇒   ⊢ (𝜑 → inf(𝐴, (0[,]+∞), < ) ≤ 𝐵)
Theorem	infxrge0glb 32738*	The infimum of a set of nonnegative extended reals is the greatest lower bound. (Contributed by Thierry Arnoux, 19-Jul-2020.) (Revised by AV, 4-Oct-2020.)
⊢ (𝜑 → 𝐴 ⊆ (0[,]+∞))    &   ⊢ (𝜑 → 𝐵 ∈ (0[,]+∞))    ⇒   ⊢ (𝜑 → (inf(𝐴, (0[,]+∞), < ) < 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑥 < 𝐵))
Theorem	infxrge0gelb 32739*	The infimum of a set of nonnegative extended reals is greater than or equal to a lower bound. (Contributed by Thierry Arnoux, 19-Jul-2020.) (Revised by AV, 4-Oct-2020.)
⊢ (𝜑 → 𝐴 ⊆ (0[,]+∞))    &   ⊢ (𝜑 → 𝐵 ∈ (0[,]+∞))    ⇒   ⊢ (𝜑 → (𝐵 ≤ inf(𝐴, (0[,]+∞), < ) ↔ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑥))
Theorem	xrofsup 32740	The supremum is preserved by extended addition set operation. (Provided minus infinity is not involved as it does not behave well with addition.) (Contributed by Thierry Arnoux, 20-Mar-2017.)
⊢ (𝜑 → 𝑋 ⊆ ℝ*)    &   ⊢ (𝜑 → 𝑌 ⊆ ℝ*)    &   ⊢ (𝜑 → sup(𝑋, ℝ*, < ) ≠ -∞)    &   ⊢ (𝜑 → sup(𝑌, ℝ*, < ) ≠ -∞)    &   ⊢ (𝜑 → 𝑍 = ( +𝑒 “ (𝑋 × 𝑌)))    ⇒   ⊢ (𝜑 → sup(𝑍, ℝ*, < ) = (sup(𝑋, ℝ*, < ) +𝑒 sup(𝑌, ℝ*, < )))
Theorem	supxrnemnf 32741	The supremum of a nonempty set of extended reals which does not contain minus infinity is not minus infinity. (Contributed by Thierry Arnoux, 21-Mar-2017.)
⊢ ((𝐴 ⊆ ℝ* ∧ 𝐴 ≠ ∅ ∧ ¬ -∞ ∈ 𝐴) → sup(𝐴, ℝ*, < ) ≠ -∞)
21.3.5.4  Extended nonnegative integers - misc additions
Theorem	xnn0gt0 32742	Nonzero extended nonnegative integers are strictly greater than zero. (Contributed by Thierry Arnoux, 30-Jul-2023.)
⊢ ((𝑁 ∈ ℕ0* ∧ 𝑁 ≠ 0) → 0 < 𝑁)
Theorem	xnn01gt 32743	An extended nonnegative integer is neither 0 nor 1 if and only if it is greater than 1. (Contributed by Thierry Arnoux, 21-Nov-2023.)
⊢ (𝑁 ∈ ℕ0* → (¬ 𝑁 ∈ {0, 1} ↔ 1 < 𝑁))
Theorem	nn0xmulclb 32744	Finite multiplication in the extended nonnegative integers. (Contributed by Thierry Arnoux, 30-Jul-2023.)
⊢ (((𝐴 ∈ ℕ0* ∧ 𝐵 ∈ ℕ0*) ∧ (𝐴 ≠ 0 ∧ 𝐵 ≠ 0)) → ((𝐴 ·e 𝐵) ∈ ℕ0 ↔ (𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0)))
Theorem	xnn0nn0d 32745	Conditions for an extended nonnegative integer to be a nonnegative integer. (Contributed by Thierry Arnoux, 26-Oct-2025.)
⊢ (𝜑 → 𝑁 ∈ ℕ0*)    &   ⊢ (𝜑 → 𝑁 ∈ ℝ)    ⇒   ⊢ (𝜑 → 𝑁 ∈ ℕ0)
Theorem	xnn0nnd 32746	Conditions for an extended nonnegative integer to be a positive integer. (Contributed by Thierry Arnoux, 26-Oct-2025.)
⊢ (𝜑 → 𝑁 ∈ ℕ0*)    &   ⊢ (𝜑 → 𝑁 ∈ ℝ)    &   ⊢ (𝜑 → 0 < 𝑁)    ⇒   ⊢ (𝜑 → 𝑁 ∈ ℕ)
21.3.5.5  Real number intervals - misc additions
Theorem	joiniooico 32747	Disjoint joining an open interval with a closed-below, open-above interval to form a closed-below, open-above interval. (Contributed by Thierry Arnoux, 26-Sep-2017.)
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (𝐴 < 𝐵 ∧ 𝐵 ≤ 𝐶)) → (((𝐴(,)𝐵) ∩ (𝐵[,)𝐶)) = ∅ ∧ ((𝐴(,)𝐵) ∪ (𝐵[,)𝐶)) = (𝐴(,)𝐶)))
Theorem	ubico 32748	A right-open interval does not contain its right endpoint. (Contributed by Thierry Arnoux, 5-Apr-2017.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*) → ¬ 𝐵 ∈ (𝐴[,)𝐵))
Theorem	xeqlelt 32749	Equality in terms of 'less than or equal to', 'less than'. (Contributed by Thierry Arnoux, 5-Jul-2017.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (𝐴 = 𝐵 ↔ (𝐴 ≤ 𝐵 ∧ ¬ 𝐴 < 𝐵)))
Theorem	eliccelico 32750	Relate elementhood to a closed interval with elementhood to the same closed-below, open-above interval or to its upper bound. (Contributed by Thierry Arnoux, 3-Jul-2017.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵) → (𝐶 ∈ (𝐴[,]𝐵) ↔ (𝐶 ∈ (𝐴[,)𝐵) ∨ 𝐶 = 𝐵)))
Theorem	elicoelioo 32751	Relate elementhood to a closed-below, open-above interval with elementhood to the same open interval or to its lower bound. (Contributed by Thierry Arnoux, 6-Jul-2017.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 < 𝐵) → (𝐶 ∈ (𝐴[,)𝐵) ↔ (𝐶 = 𝐴 ∨ 𝐶 ∈ (𝐴(,)𝐵))))
Theorem	iocinioc2 32752	Intersection between two open-below, closed-above intervals sharing the same upper bound. (Contributed by Thierry Arnoux, 7-Aug-2017.)
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 ≤ 𝐵) → ((𝐴(,]𝐶) ∩ (𝐵(,]𝐶)) = (𝐵(,]𝐶))
Theorem	xrdifh 32753	Class difference of a half-open interval in the extended reals. (Contributed by Thierry Arnoux, 1-Aug-2017.)
⊢ 𝐴 ∈ ℝ*    ⇒   ⊢ (ℝ* ∖ (𝐴[,]+∞)) = (-∞[,)𝐴)
Theorem	iocinif 32754	Relate intersection of two open-below, closed-above intervals with the same upper bound with a conditional construct. (Contributed by Thierry Arnoux, 7-Aug-2017.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → ((𝐴(,]𝐶) ∩ (𝐵(,]𝐶)) = if(𝐴 < 𝐵, (𝐵(,]𝐶), (𝐴(,]𝐶)))
Theorem	difioo 32755	The difference between two open intervals sharing the same lower bound. (Contributed by Thierry Arnoux, 26-Sep-2017.)
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ 𝐴 < 𝐵) → ((𝐴(,)𝐶) ∖ (𝐴(,)𝐵)) = (𝐵[,)𝐶))
Theorem	difico 32756	The difference between two closed-below, open-above intervals sharing the same upper bound. (Contributed by Thierry Arnoux, 13-Oct-2017.)
⊢ (((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) ∧ (𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶)) → ((𝐴[,)𝐶) ∖ (𝐵[,)𝐶)) = (𝐴[,)𝐵))
21.3.5.6  Finite intervals of integers - misc additions
Theorem	uzssico 32757	Upper integer sets are a subset of the corresponding closed-below, open-above intervals. (Contributed by Thierry Arnoux, 29-Dec-2021.)
⊢ (𝑀 ∈ ℤ → (ℤ≥‘𝑀) ⊆ (𝑀[,)+∞))
Theorem	fz2ssnn0 32758	A finite set of sequential integers that is a subset of ℕ0. (Contributed by Thierry Arnoux, 8-Dec-2021.)
⊢ (𝑀 ∈ ℕ0 → (𝑀...𝑁) ⊆ ℕ0)
Theorem	nndiffz1 32759	Upper set of the positive integers. (Contributed by Thierry Arnoux, 22-Aug-2017.)
⊢ (𝑁 ∈ ℕ0 → (ℕ ∖ (1...𝑁)) = (ℤ≥‘(𝑁 + 1)))
Theorem	ssnnssfz 32760*	For any finite subset of ℕ, find a superset in the form of a set of sequential integers. (Contributed by Thierry Arnoux, 13-Sep-2017.)
⊢ (𝐴 ∈ (𝒫 ℕ ∩ Fin) → ∃𝑛 ∈ ℕ 𝐴 ⊆ (1...𝑛))
Theorem	fzm1ne1 32761	Elementhood of an integer and its predecessor in finite intervals of integers. (Contributed by Thierry Arnoux, 1-Jan-2024.)
⊢ ((𝐾 ∈ (𝑀...𝑁) ∧ 𝐾 ≠ 𝑀) → (𝐾 − 1) ∈ (𝑀...(𝑁 − 1)))
Theorem	fzspl 32762	Split the last element of a finite set of sequential integers. More generic than fzsuc 13463. (Contributed by Thierry Arnoux, 7-Nov-2016.)
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑀...𝑁) = ((𝑀...(𝑁 − 1)) ∪ {𝑁}))
Theorem	fzdif2 32763	Split the last element of a finite set of sequential integers. More generic than fzsuc 13463. (Contributed by Thierry Arnoux, 22-Aug-2020.)
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → ((𝑀...𝑁) ∖ {𝑁}) = (𝑀...(𝑁 − 1)))
Theorem	fzodif2 32764	Split the last element of a half-open range of sequential integers. (Contributed by Thierry Arnoux, 5-Dec-2021.)
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → ((𝑀..^(𝑁 + 1)) ∖ {𝑁}) = (𝑀..^𝑁))
Theorem	fzodif1 32765	Set difference of two half-open range of sequential integers sharing the same starting value. (Contributed by Thierry Arnoux, 2-Oct-2023.)
⊢ (𝐾 ∈ (𝑀...𝑁) → ((𝑀..^𝑁) ∖ (𝑀..^𝐾)) = (𝐾..^𝑁))
Theorem	fzsplit3 32766	Split a finite interval of integers into two parts. (Contributed by Thierry Arnoux, 2-May-2017.)
⊢ (𝐾 ∈ (𝑀...𝑁) → (𝑀...𝑁) = ((𝑀...(𝐾 − 1)) ∪ (𝐾...𝑁)))
Theorem	bcm1n 32767	The proportion of one binomial coefficient to another with 𝑁 decreased by 1. (Contributed by Thierry Arnoux, 9-Nov-2016.)
⊢ ((𝐾 ∈ (0...(𝑁 − 1)) ∧ 𝑁 ∈ ℕ) → (((𝑁 − 1)C𝐾) / (𝑁C𝐾)) = ((𝑁 − 𝐾) / 𝑁))
21.3.5.7  Half-open integer ranges - misc additions
Theorem	iundisjfi 32768*	Rewrite a countable union as a disjoint union, finite version. Cf. iundisj 25469. (Contributed by Thierry Arnoux, 15-Feb-2017.)
⊢ Ⅎ𝑛𝐵    &   ⊢ (𝑛 = 𝑘 → 𝐴 = 𝐵)    ⇒   ⊢ ∪ 𝑛 ∈ (1..^𝑁)𝐴 = ∪ 𝑛 ∈ (1..^𝑁)(𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵)
Theorem	iundisj2fi 32769*	A disjoint union is disjoint, finite version. Cf. iundisj2 25470. (Contributed by Thierry Arnoux, 16-Feb-2017.)
⊢ Ⅎ𝑛𝐵    &   ⊢ (𝑛 = 𝑘 → 𝐴 = 𝐵)    ⇒   ⊢ Disj 𝑛 ∈ (1..^𝑁)(𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵)
Theorem	iundisjcnt 32770*	Rewrite a countable union as a disjoint union. (Contributed by Thierry Arnoux, 16-Feb-2017.)
⊢ Ⅎ𝑛𝐵    &   ⊢ (𝑛 = 𝑘 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → (𝑁 = ℕ ∨ 𝑁 = (1..^𝑀)))    ⇒   ⊢ (𝜑 → ∪ 𝑛 ∈ 𝑁 𝐴 = ∪ 𝑛 ∈ 𝑁 (𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵))
Theorem	iundisj2cnt 32771*	A countable disjoint union is disjoint. Cf. iundisj2 25470. (Contributed by Thierry Arnoux, 16-Feb-2017.)
⊢ Ⅎ𝑛𝐵    &   ⊢ (𝑛 = 𝑘 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → (𝑁 = ℕ ∨ 𝑁 = (1..^𝑀)))    ⇒   ⊢ (𝜑 → Disj 𝑛 ∈ 𝑁 (𝐴 ∖ ∪ 𝑘 ∈ (1..^𝑛)𝐵))
Theorem	f1ocnt 32772*	Given a countable set 𝐴, number its elements by providing a one-to-one mapping either with ℕ or an integer range starting from 1. The domain of the function can then be used with iundisjcnt 32770 or iundisj2cnt 32771. (Contributed by Thierry Arnoux, 25-Jul-2020.)
⊢ (𝐴 ≼ ω → ∃𝑓(𝑓:dom 𝑓–1-1-onto→𝐴 ∧ (dom 𝑓 = ℕ ∨ dom 𝑓 = (1..^((♯‘𝐴) + 1)))))
Theorem	fz1nnct 32773	NN and integer ranges starting from 1 are countable. (Contributed by Thierry Arnoux, 25-Jul-2020.)
⊢ ((𝐴 = ℕ ∨ 𝐴 = (1..^𝑀)) → 𝐴 ≼ ω)
Theorem	fz1nntr 32774	NN and integer ranges starting from 1 are a transitive family of set. (Contributed by Thierry Arnoux, 25-Jul-2020.)
⊢ (((𝐴 = ℕ ∨ 𝐴 = (1..^𝑀)) ∧ 𝑁 ∈ 𝐴) → (1..^𝑁) ⊆ 𝐴)
Theorem	fzo0opth 32775	Equality for a half open integer range starting at zero is the same as equality of its upper bound, analogous to fzopth 13453 and fzoopth 13654. (Contributed by Thierry Arnoux, 27-May-2025.)
⊢ (𝜑 → 𝑀 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → ((0..^𝑀) = (0..^𝑁) ↔ 𝑀 = 𝑁))
Theorem	nn0difffzod 32776	A nonnegative integer that is not in the half-open range from 0 to 𝑁 is at least 𝑁. (Contributed by Thierry Arnoux, 20-Feb-2025.)
⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ (𝜑 → 𝑀 ∈ (ℕ0 ∖ (0..^𝑁)))    ⇒   ⊢ (𝜑 → ¬ 𝑀 < 𝑁)
Theorem	suppssnn0 32777*	Show that the support of a function is contained in an half-open nonnegative integer range. (Contributed by Thierry Arnoux, 20-Feb-2025.)
⊢ (𝜑 → 𝐹 Fn ℕ0)    &   ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ 𝑁 ≤ 𝑘) → (𝐹‘𝑘) = 𝑍)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    ⇒   ⊢ (𝜑 → (𝐹 supp 𝑍) ⊆ (0..^𝑁))
21.3.5.8  The ` # ` (set size) function - misc additions
Theorem	hashunif 32778*	The cardinality of a disjoint finite union of finite sets. Cf. hashuni 15725. (Contributed by Thierry Arnoux, 17-Feb-2017.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐴 ⊆ Fin)    &   ⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 𝑥)    ⇒   ⊢ (𝜑 → (♯‘∪ 𝐴) = Σ𝑥 ∈ 𝐴 (♯‘𝑥))
Theorem	hashxpe 32779	The size of the Cartesian product of two finite sets is the product of their sizes. This is a version of hashxp 14333 valid for infinite sets, which uses extended real numbers. (Contributed by Thierry Arnoux, 27-May-2023.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (♯‘(𝐴 × 𝐵)) = ((♯‘𝐴) ·e (♯‘𝐵)))
Theorem	hashgt1 32780	Restate "set contains at least two elements" in terms of elementhood. (Contributed by Thierry Arnoux, 21-Nov-2023.)
⊢ (𝐴 ∈ 𝑉 → (¬ 𝐴 ∈ (◡♯ “ {0, 1}) ↔ 1 < (♯‘𝐴)))
Theorem	hashpss 32781	The size of a proper subset is less than the size of its finite superset. (Contributed by Thierry Arnoux, 13-Oct-2025.)
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ⊊ 𝐴) → (♯‘𝐵) < (♯‘𝐴))
Theorem	hashne0 32782	Deduce that the size of a set is not zero. (Contributed by Thierry Arnoux, 26-Oct-2025.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐴 ≠ ∅)    ⇒   ⊢ (𝜑 → 0 < (♯‘𝐴))
Theorem	hashimaf1 32783	Taking the image of a set by a one-to-one function does not affect size. (Contributed by Thierry Arnoux, 18-Jan-2026.)
⊢ (𝜑 → 𝐹:𝐴–1-1→𝐵)    &   ⊢ (𝜑 → 𝐶 ⊆ 𝐴)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (♯‘(𝐹 “ 𝐶)) = (♯‘𝐶))
21.3.5.9  The greatest common divisor operator - misc. additions
Theorem	elq2 32784*	Elementhood in the rational numbers, providing the canonical representation. (Contributed by Thierry Arnoux, 9-Nov-2025.)
⊢ (𝑄 ∈ ℚ → ∃𝑝 ∈ ℤ ∃𝑞 ∈ ℕ (𝑄 = (𝑝 / 𝑞) ∧ (𝑝 gcd 𝑞) = 1))
Theorem	znumd 32785	Numerator of an integer. (Contributed by Thierry Arnoux, 4-May-2025.)
⊢ (𝜑 → 𝑍 ∈ ℤ)    ⇒   ⊢ (𝜑 → (numer‘𝑍) = 𝑍)
Theorem	zdend 32786	Denominator of an integer. (Contributed by Thierry Arnoux, 4-May-2025.)
⊢ (𝜑 → 𝑍 ∈ ℤ)    ⇒   ⊢ (𝜑 → (denom‘𝑍) = 1)
Theorem	numdenneg 32787	Numerator and denominator of the negative. (Contributed by Thierry Arnoux, 27-Oct-2017.)
⊢ (𝑄 ∈ ℚ → ((numer‘-𝑄) = -(numer‘𝑄) ∧ (denom‘-𝑄) = (denom‘𝑄)))
Theorem	divnumden2 32788	Calculate the reduced form of a quotient using gcd. This version extends divnumden 16651 for the negative integers. (Contributed by Thierry Arnoux, 25-Oct-2017.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ -𝐵 ∈ ℕ) → ((numer‘(𝐴 / 𝐵)) = -(𝐴 / (𝐴 gcd 𝐵)) ∧ (denom‘(𝐴 / 𝐵)) = -(𝐵 / (𝐴 gcd 𝐵))))
Theorem	expgt0b 32789	A real number 𝐴 raised to an odd integer power is positive iff it is positive. (Contributed by SN, 4-Mar-2023.) Use the more standard ¬ 2 ∥ 𝑁 (Revised by Thierry Arnoux, 14-Jun-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → ¬ 2 ∥ 𝑁)    ⇒   ⊢ (𝜑 → (0 < 𝐴 ↔ 0 < (𝐴↑𝑁)))
21.3.5.10  Integers
Theorem	nn0split01 32790	Split 0 and 1 from the nonnegative integers. (Contributed by Thierry Arnoux, 8-Jun-2025.)
⊢ ℕ0 = ({0, 1} ∪ (ℤ≥‘2))
Theorem	nn0disj01 32791	The pair {0, 1} does not overlap the rest of the nonnegative integers. (Contributed by Thierry Arnoux, 8-Jun-2025.)
⊢ ({0, 1} ∩ (ℤ≥‘2)) = ∅
Theorem	nnindf 32792*	Principle of Mathematical Induction, using a bound-variable hypothesis instead of distinct variables. (Contributed by Thierry Arnoux, 6-May-2018.)
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝑥 = 1 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑥 = (𝑦 + 1) → (𝜑 ↔ 𝜃))    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏))    &   ⊢ 𝜓    &   ⊢ (𝑦 ∈ ℕ → (𝜒 → 𝜃))    ⇒   ⊢ (𝐴 ∈ ℕ → 𝜏)
Theorem	nn0min 32793*	Extracting the minimum positive integer for which a property 𝜒 does not hold. This uses substitutions similar to nn0ind 12560. (Contributed by Thierry Arnoux, 6-May-2018.)
⊢ (𝑛 = 0 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑛 = 𝑚 → (𝜓 ↔ 𝜃))    &   ⊢ (𝑛 = (𝑚 + 1) → (𝜓 ↔ 𝜏))    &   ⊢ (𝜑 → ¬ 𝜒)    &   ⊢ (𝜑 → ∃𝑛 ∈ ℕ 𝜓)    ⇒   ⊢ (𝜑 → ∃𝑚 ∈ ℕ0 (¬ 𝜃 ∧ 𝜏))
Theorem	subne0nn 32794	A nonnegative difference is positive if the two numbers are not equal. (Contributed by Thierry Arnoux, 17-Dec-2023.)
⊢ (𝜑 → 𝑀 ∈ ℂ)    &   ⊢ (𝜑 → 𝑁 ∈ ℂ)    &   ⊢ (𝜑 → (𝑀 − 𝑁) ∈ ℕ0)    &   ⊢ (𝜑 → 𝑀 ≠ 𝑁)    ⇒   ⊢ (𝜑 → (𝑀 − 𝑁) ∈ ℕ)
Theorem	ltesubnnd 32795	Subtracting an integer number from another number decreases it. See ltsubrpd 12958. (Contributed by Thierry Arnoux, 18-Apr-2017.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    ⇒   ⊢ (𝜑 → ((𝑀 + 1) − 𝑁) ≤ 𝑀)
Theorem	fprodeq02 32796*	If one of the factors is zero the product is zero. (Contributed by Thierry Arnoux, 11-Dec-2021.)
⊢ (𝑘 = 𝐾 → 𝐵 = 𝐶)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐾 ∈ 𝐴)    &   ⊢ (𝜑 → 𝐶 = 0)    ⇒   ⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐵 = 0)
Theorem	pr01ssre 32797	The range of the indicator function is a subset of ℝ. (Contributed by Thierry Arnoux, 14-Aug-2017.)
⊢ {0, 1} ⊆ ℝ
Theorem	fprodex01 32798*	A product of factors equal to zero or one is zero exactly when one of the factors is zero. (Contributed by Thierry Arnoux, 11-Dec-2021.)
⊢ (𝑘 = 𝑙 → 𝐵 = 𝐶)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ {0, 1})    ⇒   ⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐵 = if(∀𝑙 ∈ 𝐴 𝐶 = 1, 1, 0))
Theorem	prodpr 32799*	A product over a pair is the product of the elements. (Contributed by Thierry Arnoux, 1-Jan-2022.)
⊢ (𝑘 = 𝐴 → 𝐷 = 𝐸)    &   ⊢ (𝑘 = 𝐵 → 𝐷 = 𝐹)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐸 ∈ ℂ)    &   ⊢ (𝜑 → 𝐹 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    ⇒   ⊢ (𝜑 → ∏𝑘 ∈ {𝐴, 𝐵}𝐷 = (𝐸 · 𝐹))
Theorem	prodtp 32800*	A product over a triple is the product of the elements. (Contributed by Thierry Arnoux, 1-Jan-2022.)
⊢ (𝑘 = 𝐴 → 𝐷 = 𝐸)    &   ⊢ (𝑘 = 𝐵 → 𝐷 = 𝐹)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐸 ∈ ℂ)    &   ⊢ (𝜑 → 𝐹 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ (𝑘 = 𝐶 → 𝐷 = 𝐺)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐺 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐶)    &   ⊢ (𝜑 → 𝐵 ≠ 𝐶)    ⇒   ⊢ (𝜑 → ∏𝑘 ∈ {𝐴, 𝐵, 𝐶}𝐷 = ((𝐸 · 𝐹) · 𝐺))