P. 477 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 47601-47700   *Has distinct variable group(s)

Type	Label	Description
Statement
21.48.6.4  The empty set - extension
Theorem	ralralimp 47601*	Selecting one of two alternatives within a restricted generalization if one of the alternatives is false. (Contributed by AV, 6-Sep-2018.) (Proof shortened by AV, 13-Oct-2018.)
⊢ ((𝜑 ∧ 𝐴 ≠ ∅) → (∀𝑥 ∈ 𝐴 ((𝜑 → (𝜃 ∨ 𝜏)) ∧ ¬ 𝜃) → 𝜏))
21.48.6.5  Indexed union and intersection - extension
Theorem	otiunsndisjX 47602*	The union of singletons consisting of ordered triples which have distinct first and third components are disjunct. (Contributed by Alexander van der Vekens, 10-Mar-2018.)
⊢ (𝐵 ∈ 𝑋 → Disj 𝑎 ∈ 𝑉 ∪ 𝑐 ∈ 𝑊 {⟨𝑎, 𝐵, 𝑐⟩})
21.48.6.6  Functions - extension
Theorem	fvifeq 47603	Equality of function values with conditional arguments, see also fvif 6851. (Contributed by Alexander van der Vekens, 21-May-2018.)
⊢ (𝐴 = if(𝜑, 𝐵, 𝐶) → (𝐹‘𝐴) = if(𝜑, (𝐹‘𝐵), (𝐹‘𝐶)))
Theorem	rnfdmpr 47604	The range of a one-to-one function 𝐹 of an unordered pair into a set is the unordered pair of the function values. (Contributed by Alexander van der Vekens, 2-Feb-2018.)
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) → (𝐹 Fn {𝑋, 𝑌} → ran 𝐹 = {(𝐹‘𝑋), (𝐹‘𝑌)}))
Theorem	imarnf1pr 47605	The image of the range of a function 𝐹 under a function 𝐸 if 𝐹 is a function from a pair into the domain of 𝐸. (Contributed by Alexander van der Vekens, 2-Feb-2018.)
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) → (((𝐹:{𝑋, 𝑌}⟶dom 𝐸 ∧ 𝐸:dom 𝐸⟶𝑅) ∧ ((𝐸‘(𝐹‘𝑋)) = 𝐴 ∧ (𝐸‘(𝐹‘𝑌)) = 𝐵)) → (𝐸 “ ran 𝐹) = {𝐴, 𝐵}))
Theorem	funop1 47606*	A function is an ordered pair iff it is a singleton of an ordered pair. (Contributed by AV, 20-Sep-2020.) (Avoid depending on this detail.)
⊢ (∃𝑥∃𝑦 𝐹 = ⟨𝑥, 𝑦⟩ → (Fun 𝐹 ↔ ∃𝑥∃𝑦 𝐹 = {⟨𝑥, 𝑦⟩}))
Theorem	fun2dmnopgexmpl 47607	A function with a domain containing (at least) two different elements is not an ordered pair. (Contributed by AV, 21-Sep-2020.) (Avoid depending on this detail.)
⊢ (𝐺 = {⟨0, 1⟩, ⟨1, 1⟩} → ¬ 𝐺 ∈ (V × V))
Theorem	opabresex0d 47608*	A collection of ordered pairs, the class of all possible second components being a set, with a restriction of a binary relation is a set. (Contributed by Alexander van der Vekens, 1-Nov-2017.) (Revised by AV, 1-Jan-2021.)
⊢ ((𝜑 ∧ 𝑥𝑅𝑦) → 𝑥 ∈ 𝐶)    &   ⊢ ((𝜑 ∧ 𝑥𝑅𝑦) → 𝜃)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → {𝑦 ∣ 𝜃} ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑊)    ⇒   ⊢ (𝜑 → {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑅𝑦 ∧ 𝜓)} ∈ V)
Theorem	opabbrfex0d 47609*	A collection of ordered pairs, the class of all possible second components being a set, is a set. (Contributed by AV, 15-Jan-2021.)
⊢ ((𝜑 ∧ 𝑥𝑅𝑦) → 𝑥 ∈ 𝐶)    &   ⊢ ((𝜑 ∧ 𝑥𝑅𝑦) → 𝜃)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → {𝑦 ∣ 𝜃} ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑊)    ⇒   ⊢ (𝜑 → {⟨𝑥, 𝑦⟩ ∣ 𝑥𝑅𝑦} ∈ V)
Theorem	opabresexd 47610*	A collection of ordered pairs, the second component being a function, with a restriction of a binary relation is a set. (Contributed by Alexander van der Vekens, 1-Nov-2017.) (Revised by AV, 15-Jan-2021.)
⊢ ((𝜑 ∧ 𝑥𝑅𝑦) → 𝑥 ∈ 𝐶)    &   ⊢ ((𝜑 ∧ 𝑥𝑅𝑦) → 𝑦:𝐴⟶𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝐴 ∈ 𝑈)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑊)    ⇒   ⊢ (𝜑 → {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑅𝑦 ∧ 𝜓)} ∈ V)
Theorem	opabbrfexd 47611*	A collection of ordered pairs, the second component being a function, is a set. (Contributed by AV, 15-Jan-2021.)
⊢ ((𝜑 ∧ 𝑥𝑅𝑦) → 𝑥 ∈ 𝐶)    &   ⊢ ((𝜑 ∧ 𝑥𝑅𝑦) → 𝑦:𝐴⟶𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝐴 ∈ 𝑈)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑊)    ⇒   ⊢ (𝜑 → {⟨𝑥, 𝑦⟩ ∣ 𝑥𝑅𝑦} ∈ V)
Theorem	f1oresf1orab 47612*	Build a bijection by restricting the domain of a bijection. (Contributed by AV, 1-Aug-2022.)
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐶)    &   ⊢ (𝜑 → 𝐹:𝐴–1-1-onto→𝐵)    &   ⊢ (𝜑 → 𝐷 ⊆ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶) → (𝜒 ↔ 𝑥 ∈ 𝐷))    ⇒   ⊢ (𝜑 → (𝐹 ↾ 𝐷):𝐷–1-1-onto→{𝑦 ∈ 𝐵 ∣ 𝜒})
Theorem	f1oresf1o 47613*	Build a bijection by restricting the domain of a bijection. (Contributed by AV, 31-Jul-2022.)
⊢ (𝜑 → 𝐹:𝐴–1-1-onto→𝐵)    &   ⊢ (𝜑 → 𝐷 ⊆ 𝐴)    &   ⊢ (𝜑 → (∃𝑥 ∈ 𝐷 (𝐹‘𝑥) = 𝑦 ↔ (𝑦 ∈ 𝐵 ∧ 𝜒)))    ⇒   ⊢ (𝜑 → (𝐹 ↾ 𝐷):𝐷–1-1-onto→{𝑦 ∈ 𝐵 ∣ 𝜒})
Theorem	f1oresf1o2 47614*	Build a bijection by restricting the domain of a bijection. (Contributed by AV, 31-Jul-2022.)
⊢ (𝜑 → 𝐹:𝐴–1-1-onto→𝐵)    &   ⊢ (𝜑 → 𝐷 ⊆ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑦 = (𝐹‘𝑥)) → (𝑥 ∈ 𝐷 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (𝐹 ↾ 𝐷):𝐷–1-1-onto→{𝑦 ∈ 𝐵 ∣ 𝜒})
21.48.6.7  Maps-to notation - extension
Theorem	fvmptrab 47615*	Value of a function mapping a set to a class abstraction restricting a class depending on the argument of the function. More general version of fvmptrabfv 6975, but relying on the fact that out-of-domain arguments evaluate to the empty set, which relies on set.mm's particular encoding. (Contributed by AV, 14-Feb-2022.)
⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ {𝑦 ∈ 𝑀 ∣ 𝜑})    &   ⊢ (𝑥 = 𝑋 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝑋 → 𝑀 = 𝑁)    &   ⊢ (𝑋 ∈ 𝑉 → 𝑁 ∈ V)    &   ⊢ (𝑋 ∉ 𝑉 → 𝑁 = ∅)    ⇒   ⊢ (𝐹‘𝑋) = {𝑦 ∈ 𝑁 ∣ 𝜓}
Theorem	fvmptrabdm 47616*	Value of a function mapping a set to a class abstraction restricting the value of another function. See also fvmptrabfv 6975. (Suggested by BJ, 18-Feb-2022.) (Contributed by AV, 18-Feb-2022.)
⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ {𝑦 ∈ (𝐺‘𝑌) ∣ 𝜑})    &   ⊢ (𝑥 = 𝑋 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑌 ∈ dom 𝐺 → 𝑋 ∈ dom 𝐹)    ⇒   ⊢ (𝐹‘𝑋) = {𝑦 ∈ (𝐺‘𝑌) ∣ 𝜓}
21.48.6.8  Subtraction - extension
Theorem	cnambpcma 47617	((a-b)+c)-a = c-a holds for complex numbers a,b,c. (Contributed by Alexander van der Vekens, 23-Mar-2018.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (((𝐴 − 𝐵) + 𝐶) − 𝐴) = (𝐶 − 𝐵))
Theorem	cnapbmcpd 47618	((a+b)-c)+d = ((a+d)+b)-c holds for complex numbers a,b,c,d. (Contributed by Alexander van der Vekens, 23-Mar-2018.)
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) → (((𝐴 + 𝐵) − 𝐶) + 𝐷) = (((𝐴 + 𝐷) + 𝐵) − 𝐶))
Theorem	addsubeq0 47619	The sum of two complex numbers is equal to the difference of these two complex numbers iff the subtrahend is 0. (Contributed by AV, 8-May-2023.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐴 + 𝐵) = (𝐴 − 𝐵) ↔ 𝐵 = 0))
21.48.6.9  Ordering on reals (cont.) - extension
Theorem	leaddsuble 47620	Addition and subtraction on one side of "less than or equal to". (Contributed by Alexander van der Vekens, 18-Mar-2018.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 ≤ 𝐶 ↔ ((𝐴 + 𝐵) − 𝐶) ≤ 𝐴))
Theorem	2leaddle2 47621	If two real numbers are less than a third real number, the sum of the real numbers is less than twice the third real number. (Contributed by Alexander van der Vekens, 21-May-2018.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐶 ∧ 𝐵 < 𝐶) → (𝐴 + 𝐵) < (2 · 𝐶)))
Theorem	ltnltne 47622	Variant of trichotomy law for 'less than'. (Contributed by Alexander van der Vekens, 8-Jun-2018.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ (¬ 𝐵 < 𝐴 ∧ ¬ 𝐵 = 𝐴)))
Theorem	p1lep2 47623	A real number increasd by 1 is less than or equal to the number increased by 2. (Contributed by Alexander van der Vekens, 17-Sep-2018.)
⊢ (𝑁 ∈ ℝ → (𝑁 + 1) ≤ (𝑁 + 2))
Theorem	ltsubsubaddltsub 47624	If the result of subtracting two numbers is greater than a number, the result of adding one of these subtracted numbers to the number is less than the result of subtracting the other subtracted number only. (Contributed by Alexander van der Vekens, 9-Jun-2018.)
⊢ ((𝐽 ∈ ℝ ∧ (𝐿 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ)) → (𝐽 < ((𝐿 − 𝑀) − 𝑁) ↔ (𝐽 + 𝑀) < (𝐿 − 𝑁)))
Theorem	zm1nn 47625	An integer minus 1 is positive under certain circumstances. (Contributed by Alexander van der Vekens, 9-Jun-2018.)
⊢ ((𝑁 ∈ ℕ0 ∧ 𝐿 ∈ ℤ) → ((𝐽 ∈ ℝ ∧ 0 ≤ 𝐽 ∧ 𝐽 < ((𝐿 − 𝑁) − 1)) → (𝐿 − 1) ∈ ℕ))
21.48.6.10  Imaginary and complex number properties - extension
Theorem	readdcnnred 47626	The sum of a real number and an imaginary number is not a real number. (Contributed by AV, 23-Jan-2023.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ (ℂ ∖ ℝ))    ⇒   ⊢ (𝜑 → (𝐴 + 𝐵) ∉ ℝ)
Theorem	resubcnnred 47627	The difference of a real number and an imaginary number is not a real number. (Contributed by AV, 23-Jan-2023.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ (ℂ ∖ ℝ))    ⇒   ⊢ (𝜑 → (𝐴 − 𝐵) ∉ ℝ)
Theorem	recnmulnred 47628	The product of a real number and an imaginary number is not a real number. (Contributed by AV, 23-Jan-2023.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ (ℂ ∖ ℝ))    &   ⊢ (𝜑 → 𝐴 ≠ 0)    ⇒   ⊢ (𝜑 → (𝐴 · 𝐵) ∉ ℝ)
Theorem	cndivrenred 47629	The quotient of an imaginary number and a real number is not a real number. (Contributed by AV, 23-Jan-2023.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ (ℂ ∖ ℝ))    &   ⊢ (𝜑 → 𝐴 ≠ 0)    ⇒   ⊢ (𝜑 → (𝐵 / 𝐴) ∉ ℝ)
Theorem	sqrtnegnre 47630	The square root of a negative number is not a real number. (Contributed by AV, 28-Feb-2023.)
⊢ ((𝑋 ∈ ℝ ∧ 𝑋 < 0) → (√‘𝑋) ∉ ℝ)
21.48.6.11  Nonnegative integers (as a subset of complex numbers) - extension
Theorem	nn0resubcl 47631	Closure law for subtraction of reals, restricted to nonnegative integers. (Contributed by Alexander van der Vekens, 6-Apr-2018.)
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0) → (𝐴 − 𝐵) ∈ ℝ)
21.48.6.12  Integers (as a subset of complex numbers) - extension
Theorem	zgeltp1eq 47632	If an integer is between another integer and its successor, the integer is equal to the other integer. (Contributed by AV, 30-May-2020.)
⊢ ((𝐼 ∈ ℤ ∧ 𝐴 ∈ ℤ) → ((𝐴 ≤ 𝐼 ∧ 𝐼 < (𝐴 + 1)) → 𝐼 = 𝐴))
21.48.6.13  Decimal arithmetic - extension
Theorem	1t10e1p1e11 47633	11 is 1 times 10 to the power of 1, plus 1. (Contributed by AV, 4-Aug-2020.) (Revised by AV, 9-Sep-2021.)
⊢ ;11 = ((1 · (;10↑1)) + 1)
Theorem	deccarry 47634	Add 1 to a 2 digit number with carry. This is a special case of decsucc 12653, but in closed form. As observed by ML, this theorem allows for carrying the 1 down multiple decimal constructors, so we can carry the 1 multiple times down a multi-digit number, e.g., by applying this theorem three times we get (;;999 + 1) = ;;;1000. (Contributed by AV, 4-Aug-2020.) (Revised by ML, 8-Aug-2020.) (Proof shortened by AV, 10-Sep-2021.)
⊢ (𝐴 ∈ ℕ → (;𝐴9 + 1) = ;(𝐴 + 1)0)
21.48.6.14  Upper sets of integers - extension
Theorem	eluzge0nn0 47635	If an integer is greater than or equal to a nonnegative integer, then it is a nonnegative integer. (Contributed by Alexander van der Vekens, 27-Aug-2018.)
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (0 ≤ 𝑀 → 𝑁 ∈ ℕ0))
21.48.6.15  Infinity and the extended real number system (cont.) - extension
Theorem	nltle2tri 47636	Negated extended trichotomy law for 'less than' and 'less than or equal to'. (Contributed by AV, 18-Jul-2020.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → ¬ (𝐴 < 𝐵 ∧ 𝐵 ≤ 𝐶 ∧ 𝐶 ≤ 𝐴))
21.48.6.16  Finite intervals of integers - extension
Theorem	ssfz12 47637	Subset relationship for finite sets of sequential integers. (Contributed by Alexander van der Vekens, 16-Mar-2018.)
⊢ ((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝐾 ≤ 𝐿) → ((𝐾...𝐿) ⊆ (𝑀...𝑁) → (𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁)))
Theorem	elfz2z 47638	Membership of an integer in a finite set of sequential integers starting at 0. (Contributed by Alexander van der Vekens, 25-May-2018.)
⊢ ((𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 ∈ (0...𝑁) ↔ (0 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁)))
Theorem	2elfz3nn0 47639	If there are two elements in a finite set of sequential integers starting at 0, these two elements as well as the upper bound are nonnegative integers. (Contributed by Alexander van der Vekens, 7-Apr-2018.)
⊢ ((𝐴 ∈ (0...𝑁) ∧ 𝐵 ∈ (0...𝑁)) → (𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0))
Theorem	fz0addcom 47640	The addition of two members of a finite set of sequential integers starting at 0 is commutative. (Contributed by Alexander van der Vekens, 22-May-2018.) (Revised by Alexander van der Vekens, 9-Jun-2018.)
⊢ ((𝐴 ∈ (0...𝑁) ∧ 𝐵 ∈ (0...𝑁)) → (𝐴 + 𝐵) = (𝐵 + 𝐴))
Theorem	2elfz2melfz 47641	If the sum of two integers of a 0-based finite set of sequential integers is greater than the upper bound, the difference between one of the integers and the difference between the upper bound and the other integer is in the 0-based finite set of sequential integers with the first integer as upper bound. (Contributed by Alexander van der Vekens, 7-Apr-2018.) (Revised by Alexander van der Vekens, 31-May-2018.)
⊢ ((𝐴 ∈ (0...𝑁) ∧ 𝐵 ∈ (0...𝑁)) → (𝑁 < (𝐴 + 𝐵) → (𝐵 − (𝑁 − 𝐴)) ∈ (0...𝐴)))
Theorem	fz0addge0 47642	The sum of two integers in 0-based finite sets of sequential integers is greater than or equal to zero. (Contributed by Alexander van der Vekens, 8-Jun-2018.)
⊢ ((𝐴 ∈ (0...𝑀) ∧ 𝐵 ∈ (0...𝑁)) → 0 ≤ (𝐴 + 𝐵))
Theorem	elfzlble 47643	Membership of an integer in a finite set of sequential integers with the integer as upper bound and a lower bound less than or equal to the integer. (Contributed by AV, 21-Oct-2018.)
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → 𝑁 ∈ ((𝑁 − 𝑀)...𝑁))
Theorem	elfzelfzlble 47644	Membership of an element of a finite set of sequential integers in a finite set of sequential integers with the same upper bound and a lower bound less than the upper bound. (Contributed by AV, 21-Oct-2018.)
⊢ ((𝑀 ∈ ℤ ∧ 𝐾 ∈ (0...𝑁) ∧ 𝑁 < (𝑀 + 𝐾)) → 𝐾 ∈ ((𝑁 − 𝑀)...𝑁))
21.48.6.17  Half-open integer ranges - extension
Theorem	fzopred 47645	Join a predecessor to the beginning of an open integer interval. Generalization of fzo0sn0fzo1 13676. (Contributed by AV, 14-Jul-2020.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 < 𝑁) → (𝑀..^𝑁) = ({𝑀} ∪ ((𝑀 + 1)..^𝑁)))
Theorem	fzopredsuc 47646	Join a predecessor and a successor to the beginning and the end of an open integer interval. This theorem holds even if 𝑁 = 𝑀 (then (𝑀...𝑁) = {𝑀} = ({𝑀} ∪ ∅) ∪ {𝑀}). (Contributed by AV, 14-Jul-2020.)
⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑀...𝑁) = (({𝑀} ∪ ((𝑀 + 1)..^𝑁)) ∪ {𝑁}))
Theorem	1fzopredsuc 47647	Join 0 and a successor to the beginning and the end of an open integer interval starting at 1. (Contributed by AV, 14-Jul-2020.)
⊢ (𝑁 ∈ ℕ0 → (0...𝑁) = (({0} ∪ (1..^𝑁)) ∪ {𝑁}))
Theorem	el1fzopredsuc 47648	An element of an open integer interval starting at 1 joined by 0 and a successor at the beginning and the end is either 0 or an element of the open integer interval or the successor. (Contributed by AV, 14-Jul-2020.)
⊢ (𝑁 ∈ ℕ0 → (𝐼 ∈ (0...𝑁) ↔ (𝐼 = 0 ∨ 𝐼 ∈ (1..^𝑁) ∨ 𝐼 = 𝑁)))
Theorem	subsubelfzo0 47649	Subtracting a difference from a number which is not less than the difference results in a bounded nonnegative integer. (Contributed by Alexander van der Vekens, 21-May-2018.)
⊢ ((𝐴 ∈ (0..^𝑁) ∧ 𝐼 ∈ (0..^𝑁) ∧ ¬ 𝐼 < (𝑁 − 𝐴)) → (𝐼 − (𝑁 − 𝐴)) ∈ (0..^𝐴))
Theorem	2ffzoeq 47650*	Two functions over a half-open range of nonnegative integers are equal if and only if their domains have the same length and the function values are the same at each position. (Contributed by Alexander van der Vekens, 1-Jul-2018.)
⊢ (((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ (𝐹:(0..^𝑀)⟶𝑋 ∧ 𝑃:(0..^𝑁)⟶𝑌)) → (𝐹 = 𝑃 ↔ (𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑀)(𝐹‘𝑖) = (𝑃‘𝑖))))
21.48.6.18  The floor and ceiling functions - extension
Theorem	2ltceilhalf 47651	The ceiling of half of an integer greater than 2 is greater than or equal to 2. (Contributed by AV, 4-Sep-2025.)
⊢ (𝑁 ∈ (ℤ≥‘3) → 2 ≤ (⌈‘(𝑁 / 2)))
Theorem	ceilhalfgt1 47652	The ceiling of half of an integer greater than two is greater than one. (Contributed by AV, 2-Nov-2025.)
⊢ (𝑁 ∈ (ℤ≥‘3) → 1 < (⌈‘(𝑁 / 2)))
Theorem	ceilhalfelfzo1 47653	A positive integer less than (the ceiling of) half of another integer is in the half-open range of positive integers up to the other integer. (Contributed by AV, 7-Sep-2025.)
⊢ 𝐽 = (1..^(⌈‘(𝑁 / 2)))    ⇒   ⊢ (𝑁 ∈ ℕ → (𝐾 ∈ 𝐽 → 𝐾 ∈ (1..^𝑁)))
Theorem	gpgedgvtx1lem 47654	Lemma for gpgedgvtx1 48385. (Contributed by AV, 1-Sep-2025.) (Proof shortened by AV, 8-Sep-2025.)
⊢ 𝐽 = (1..^(⌈‘(𝑁 / 2)))    &   ⊢ 𝐼 = (0..^𝑁)    ⇒   ⊢ ((𝑁 ∈ (ℤ≥‘3) ∧ 𝑋 ∈ 𝐽) → 𝑋 ∈ 𝐼)
Theorem	2tceilhalfelfzo1 47655	Two times a positive integer less than (the ceiling of) half of another integer is less than the other integer. This theorem would hold even for integers less than 3, but then a corresponding 𝐾 would not exist. (Contributed by AV, 9-Sep-2025.)
⊢ ((𝑁 ∈ (ℤ≥‘3) ∧ 𝐾 ∈ (1..^(⌈‘(𝑁 / 2)))) → (2 · 𝐾) < 𝑁)
Theorem	ceilbi 47656	A condition equivalent to ceiling. Analogous to flbi 13741. (Contributed by AV, 2-Nov-2025.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℤ) → ((⌈‘𝐴) = 𝐵 ↔ (𝐴 ≤ 𝐵 ∧ 𝐵 < (𝐴 + 1))))
Theorem	ceilhalf1 47657	The ceiling of one half is one. (Contributed by AV, 2-Nov-2025.)
⊢ (⌈‘(1 / 2)) = 1
Theorem	rehalfge1 47658	Half of a real number greater than or equal to two is greater than or equal to one. (Contributed by AV, 2-Nov-2025.)
⊢ (𝑋 ∈ (2[,)+∞) → 1 ≤ (𝑋 / 2))
Theorem	ceilhalfnn 47659	The ceiling of half of a positive integer is a positive integer. (Contributed by AV, 2-Nov-2025.)
⊢ (𝑁 ∈ ℕ → (⌈‘(𝑁 / 2)) ∈ ℕ)
Theorem	1elfzo1ceilhalf1 47660	1 is in the half-open integer range from 1 to the ceiling of half of an integer greater than two is greater than one. (Contributed by AV, 2-Nov-2025.)
⊢ (𝑁 ∈ (ℤ≥‘3) → 1 ∈ (1..^(⌈‘(𝑁 / 2))))
21.48.6.19  The modulo (remainder) operation - extension
Theorem	fldivmod 47661	Expressing the floor of a division by the modulo operator. (Contributed by AV, 6-Jun-2020.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → (⌊‘(𝐴 / 𝐵)) = ((𝐴 − (𝐴 mod 𝐵)) / 𝐵))
Theorem	ceildivmod 47662	Expressing the ceiling of a division by the modulo operator. (Contributed by AV, 7-Sep-2025.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → (⌈‘(𝐴 / 𝐵)) = ((𝐴 + ((𝐵 − 𝐴) mod 𝐵)) / 𝐵))
Theorem	ceil5half3 47663	The ceiling of half of 5 is 3. (Contributed by AV, 7-Sep-2025.)
⊢ (⌈‘(5 / 2)) = 3
Theorem	submodaddmod 47664	Subtraction and addition modulo a positive integer. (Contributed by AV, 7-Sep-2025.)
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ)) → (((𝐴 + 𝐵) mod 𝑁) = ((𝐴 − 𝐶) mod 𝑁) ↔ ((𝐴 + (𝐵 + 𝐶)) mod 𝑁) = (𝐴 mod 𝑁)))
Theorem	difltmodne 47665	Two nonnegative integers are not equal modulo a positive modulus if their difference is greater than 0 and less than the modulus. (Contributed by AV, 6-Sep-2025.)
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (1 ≤ (𝐴 − 𝐵) ∧ (𝐴 − 𝐵) < 𝑁)) → (𝐴 mod 𝑁) ≠ (𝐵 mod 𝑁))
Theorem	zplusmodne 47666	A nonnegative integer is not itself plus a positive integer modulo an integer greater than 1 and the positive integer. (Contributed by AV, 6-Sep-2025.)
⊢ ((𝑁 ∈ (ℤ≥‘2) ∧ 𝐴 ∈ ℤ ∧ 𝐾 ∈ (1..^𝑁)) → ((𝐴 + 𝐾) mod 𝑁) ≠ (𝐴 mod 𝑁))
Theorem	addmodne 47667	The sum of a nonnegative integer and a positive integer modulo a number greater than both integers is not equal to the nonnegative integer. (Contributed by AV, 27-Aug-2025.) (Proof shortened by AV, 6-Sep-2025.)
⊢ ((𝑀 ∈ ℕ ∧ (𝐴 ∈ ℕ0 ∧ 𝐴 < 𝑀) ∧ (𝐵 ∈ ℕ ∧ 𝐵 < 𝑀)) → ((𝐴 + 𝐵) mod 𝑀) ≠ 𝐴)
Theorem	plusmod5ne 47668	A nonnegative integer is not itself plus a positive integer less than 5 modulo 5. (Contributed by AV, 6-Sep-2025.)
⊢ ((𝐴 ∈ (0..^5) ∧ 𝐾 ∈ (1..^5)) → ((𝐴 + 𝐾) mod 5) ≠ 𝐴)
Theorem	zp1modne 47669	An integer is not itself plus 1 modulo an integer greater than 1. (Contributed by AV, 6-Sep-2025.)
⊢ ((𝑁 ∈ (ℤ≥‘2) ∧ 𝐴 ∈ ℤ) → ((𝐴 + 1) mod 𝑁) ≠ (𝐴 mod 𝑁))
Theorem	p1modne 47670	A nonnegative integer is not itself plus 1 modulo an integer greater than 1 and the nonnegative integer. (Contributed by AV, 6-Sep-2025.)
⊢ ((𝑁 ∈ (ℤ≥‘2) ∧ 𝐴 ∈ (0..^𝑁)) → ((𝐴 + 1) mod 𝑁) ≠ 𝐴)
Theorem	m1modne 47671	A nonnegative integer is not itself minus 1 modulo an integer greater than 1 and the nonnegative integer. (Contributed by AV, 6-Sep-2025.)
⊢ ((𝑁 ∈ (ℤ≥‘2) ∧ 𝐴 ∈ (0..^𝑁)) → ((𝐴 − 1) mod 𝑁) ≠ 𝐴)
Theorem	minusmod5ne 47672	A nonnegative integer is not itself minus a positive integer less than 5 modulo 5. (Contributed by AV, 7-Sep-2025.)
⊢ ((𝐴 ∈ (0..^5) ∧ 𝐾 ∈ (1..^5)) → ((𝐴 − 𝐾) mod 5) ≠ 𝐴)
Theorem	submodlt 47673	The difference of an element of a half-open range of nonnegative integers and the upper bound of this range modulo an integer greater than the upper bound. (Contributed by AV, 1-Sep-2025.)
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ (0..^𝐵) ∧ 𝐵 < 𝑁) → ((𝐴 − 𝐵) mod 𝑁) = ((𝑁 + 𝐴) − 𝐵))
Theorem	submodneaddmod 47674	An integer minus 𝐵 is not itself plus 𝐶 modulo an integer greater than the sum of 𝐵 and 𝐶. (Contributed by AV, 6-Sep-2025.)
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (1 ≤ (𝐵 + 𝐶) ∧ (𝐵 + 𝐶) < 𝑁)) → ((𝐴 + 𝐵) mod 𝑁) ≠ ((𝐴 − 𝐶) mod 𝑁))
Theorem	m1modnep2mod 47675	A nonnegative integer minus 1 is not itself plus 2 modulo an integer greater than 3 and the nonnegative integer. (Contributed by AV, 6-Sep-2025.)
⊢ ((𝑁 ∈ (ℤ≥‘4) ∧ 𝐴 ∈ ℤ) → ((𝐴 − 1) mod 𝑁) ≠ ((𝐴 + 2) mod 𝑁))
Theorem	minusmodnep2tmod 47676	A nonnegative integer minus a positive integer 1 or 2 is not itself plus 2 times the positive integer modulo 5. (Contributed by AV, 8-Sep-2025.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ (1..^3)) → ((𝐴 − 𝐵) mod 5) ≠ ((𝐴 + (2 · 𝐵)) mod 5))
Theorem	m1mod0mod1 47677	An integer decreased by 1 is 0 modulo a positive integer iff the integer is 1 modulo the same modulus. (Contributed by AV, 6-Jun-2020.)
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 1 < 𝑁) → (((𝐴 − 1) mod 𝑁) = 0 ↔ (𝐴 mod 𝑁) = 1))
Theorem	elmod2 47678	An integer modulo 2 is either 0 or 1. (Contributed by AV, 24-May-2020.) (Proof shortened by OpenAI, 3-Jul-2020.)
⊢ (𝑁 ∈ ℤ → (𝑁 mod 2) ∈ {0, 1})
Theorem	mod0mul 47679*	If an integer is 0 modulo a positive integer, this integer must be a multiple of the modulus. (Contributed by AV, 7-Jun-2020.)
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝐴 mod 𝑁) = 0 → ∃𝑥 ∈ ℤ 𝐴 = (𝑥 · 𝑁)))
Theorem	modn0mul 47680*	If an integer is not 0 modulo a positive integer, this integer must be the sum of a multiple of the modulus and a positive integer less than the modulus. (Contributed by AV, 7-Jun-2020.)
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝐴 mod 𝑁) ≠ 0 → ∃𝑥 ∈ ℤ ∃𝑦 ∈ (1..^𝑁)𝐴 = ((𝑥 · 𝑁) + 𝑦)))
Theorem	m1modmmod 47681	An integer decreased by 1 modulo a positive integer minus the integer modulo the same modulus is either -1 or the modulus minus 1. (Contributed by AV, 7-Jun-2020.)
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((𝐴 − 1) mod 𝑁) − (𝐴 mod 𝑁)) = if((𝐴 mod 𝑁) = 0, (𝑁 − 1), -1))
Theorem	difmodm1lt 47682	The difference between an integer modulo a positive integer and the integer decreased by 1 modulo the same modulus is less than the modulus decreased by 1 (if the modulus is greater than 2). This theorem would not be valid for an odd 𝐴 and 𝑁 = 2, since ((𝐴 mod 𝑁) − ((𝐴 − 1) mod 𝑁)) would be (1 − 0) = 1 which is not less than (𝑁 − 1) = 1. (Contributed by AV, 6-Jun-2012.) (Proof shortened by SN, 27-Nov-2025.)
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ 2 < 𝑁) → ((𝐴 mod 𝑁) − ((𝐴 − 1) mod 𝑁)) < (𝑁 − 1))
Theorem	8mod5e3 47683	8 modulo 5 is 3. (Contributed by AV, 20-Nov-2025.)
⊢ (8 mod 5) = 3
Theorem	modmkpkne 47684	If an integer minus a constant equals another integer plus the constant modulo 𝑁, then the first integer plus the constant equals the second integer minus the constant modulo 𝑁 iff the fourfold of the constant is a multiple of 𝑁. (Contributed by AV, 15-Nov-2025.)
⊢ ((𝑁 ∈ ℕ ∧ (𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ∧ 𝐾 ∈ ℤ)) → (((𝑌 − 𝐾) mod 𝑁) = ((𝑋 + 𝐾) mod 𝑁) → (((𝑌 + 𝐾) mod 𝑁) = ((𝑋 − 𝐾) mod 𝑁) ↔ ((4 · 𝐾) mod 𝑁) = 0)))
Theorem	modmknepk 47685	A nonnegative integer less than the modulus plus/minus a positive integer less than (the ceiling of) half of the modulus are not equal modulo the modulus. For this theorem, it is essential that 𝐾 < (𝑁 / 2)! (Contributed by AV, 3-Sep-2025.) (Revised by AV, 15-Nov-2025.)
⊢ 𝐽 = (1..^(⌈‘(𝑁 / 2)))    &   ⊢ 𝐼 = (0..^𝑁)    ⇒   ⊢ ((𝑁 ∈ (ℤ≥‘3) ∧ 𝑌 ∈ 𝐼 ∧ 𝐾 ∈ 𝐽) → ((𝑌 − 𝐾) mod 𝑁) ≠ ((𝑌 + 𝐾) mod 𝑁))
Theorem	modlt0b 47686	An integer with an absolute value less than a positive integer is 0 modulo the positive integer iff it is 0. (Contributed by AV, 21-Nov-2025.)
⊢ ((𝑁 ∈ ℕ ∧ 𝑋 ∈ ℤ ∧ (abs‘𝑋) < 𝑁) → ((𝑋 mod 𝑁) = 0 ↔ 𝑋 = 0))
Theorem	mod2addne 47687	The sums of a nonnegative integer less than the modulus and two integers whose difference is less than the modulus are not equal modulo the modulus. (Contributed by AV, 15-Nov-2025.)
⊢ 𝐼 = (0..^𝑁)    ⇒   ⊢ ((𝑁 ∈ ℕ ∧ (𝑋 ∈ 𝐼 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (abs‘(𝐴 − 𝐵)) ∈ (1..^𝑁)) → ((𝑋 + 𝐴) mod 𝑁) ≠ ((𝑋 + 𝐵) mod 𝑁))
Theorem	modm1nep1 47688	A nonnegative integer less than a modulus greater than 2 plus/minus one are not equal modulo the modulus. (Contributed by AV, 15-Nov-2025.)
⊢ 𝐼 = (0..^𝑁)    ⇒   ⊢ ((𝑁 ∈ (ℤ≥‘3) ∧ 𝑌 ∈ 𝐼) → ((𝑌 − 1) mod 𝑁) ≠ ((𝑌 + 1) mod 𝑁))
Theorem	modm2nep1 47689	A nonnegative integer less than a modulus greater than 4 plus one/minus two are not equal modulo the modulus. (Contributed by AV, 22-Nov-2025.)
⊢ 𝐼 = (0..^𝑁)    ⇒   ⊢ ((𝑁 ∈ (ℤ≥‘5) ∧ 𝑌 ∈ 𝐼) → ((𝑌 − 2) mod 𝑁) ≠ ((𝑌 + 1) mod 𝑁))
Theorem	modp2nep1 47690	A nonnegative integer less than a modulus greater than 4 plus one/plus two are not equal modulo the modulus. (Contributed by AV, 22-Nov-2025.)
⊢ 𝐼 = (0..^𝑁)    ⇒   ⊢ ((𝑁 ∈ (ℤ≥‘5) ∧ 𝑌 ∈ 𝐼) → ((𝑌 + 2) mod 𝑁) ≠ ((𝑌 + 1) mod 𝑁))
Theorem	modm1nep2 47691	A nonnegative integer less than a modulus greater than 4 plus one/minus two are not equal modulo the modulus. (Contributed by AV, 22-Nov-2025.)
⊢ 𝐼 = (0..^𝑁)    ⇒   ⊢ ((𝑁 ∈ (ℤ≥‘5) ∧ 𝑌 ∈ 𝐼) → ((𝑌 − 1) mod 𝑁) ≠ ((𝑌 + 2) mod 𝑁))
Theorem	modm1nem2 47692	A nonnegative integer less than a modulus greater than 4 minus one/minus two are not equal modulo the modulus. (Contributed by AV, 22-Nov-2025.)
⊢ 𝐼 = (0..^𝑁)    ⇒   ⊢ ((𝑁 ∈ (ℤ≥‘5) ∧ 𝑌 ∈ 𝐼) → ((𝑌 − 1) mod 𝑁) ≠ ((𝑌 − 2) mod 𝑁))
Theorem	modm1p1ne 47693	If an integer minus one equals another integer plus one modulo an integer greater than 4, then the first integer plus one is not equal to the second integer minus one modulo the same modulus. (Contributed by AV, 15-Nov-2025.)
⊢ 𝐼 = (0..^𝑁)    ⇒   ⊢ ((𝑁 ∈ (ℤ≥‘5) ∧ 𝑋 ∈ 𝐼 ∧ 𝑌 ∈ 𝐼) → (((𝑌 − 1) mod 𝑁) = ((𝑋 + 1) mod 𝑁) → ((𝑌 + 1) mod 𝑁) ≠ ((𝑋 − 1) mod 𝑁)))
21.48.6.20  The infinite sequence builder "seq"
Theorem	smonoord 47694*	Ordering relation for a strictly monotonic sequence, increasing case. Analogous to monoord 13960 (except that the case 𝑀 = 𝑁 must be excluded). Duplicate of monoords 45622? (Contributed by AV, 12-Jul-2020.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(𝑁 − 1))) → (𝐹‘𝑘) < (𝐹‘(𝑘 + 1)))    ⇒   ⊢ (𝜑 → (𝐹‘𝑀) < (𝐹‘𝑁))
21.48.6.21  Finite and infinite sums - extension
Theorem	fsummsndifre 47695*	A finite sum with one of its integer summands removed is a real number. (Contributed by Alexander van der Vekens, 31-Aug-2018.)
⊢ ((𝐴 ∈ Fin ∧ ∀𝑘 ∈ 𝐴 𝐵 ∈ ℤ) → Σ𝑘 ∈ (𝐴 ∖ {𝑋})𝐵 ∈ ℝ)
Theorem	fsumsplitsndif 47696*	Separate out a term in a finite sum by splitting the sum into two parts. (Contributed by Alexander van der Vekens, 31-Aug-2018.)
⊢ ((𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐴 ∧ ∀𝑘 ∈ 𝐴 𝐵 ∈ ℤ) → Σ𝑘 ∈ 𝐴 𝐵 = (Σ𝑘 ∈ (𝐴 ∖ {𝑋})𝐵 + ⦋𝑋 / 𝑘⦌𝐵))
Theorem	fsummmodsndifre 47697*	A finite sum of summands modulo a positive number with one of its summands removed is a real number. (Contributed by Alexander van der Vekens, 31-Aug-2018.)
⊢ ((𝐴 ∈ Fin ∧ 𝑁 ∈ ℕ ∧ ∀𝑘 ∈ 𝐴 𝐵 ∈ ℤ) → Σ𝑘 ∈ (𝐴 ∖ {𝑋})(𝐵 mod 𝑁) ∈ ℝ)
Theorem	fsummmodsnunz 47698*	A finite sum of summands modulo a positive number with an additional summand is an integer. (Contributed by Alexander van der Vekens, 1-Sep-2018.)
⊢ ((𝐴 ∈ Fin ∧ 𝑁 ∈ ℕ ∧ ∀𝑘 ∈ (𝐴 ∪ {𝑧})𝐵 ∈ ℤ) → Σ𝑘 ∈ (𝐴 ∪ {𝑧})(𝐵 mod 𝑁) ∈ ℤ)
21.48.6.22  Extensible structures - extension
Theorem	setsidel 47699	The injected slot is an element of the structure with replacement. (Contributed by AV, 10-Nov-2021.)
⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ 𝑅 = (𝑆 sSet ⟨𝐴, 𝐵⟩)    ⇒   ⊢ (𝜑 → ⟨𝐴, 𝐵⟩ ∈ 𝑅)
Theorem	setsnidel 47700	The injected slot is an element of the structure with replacement. (Contributed by AV, 10-Nov-2021.)
⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ 𝑅 = (𝑆 sSet ⟨𝐴, 𝐵⟩)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑌)    &   ⊢ (𝜑 → ⟨𝐶, 𝐷⟩ ∈ 𝑆)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐶)    ⇒   ⊢ (𝜑 → ⟨𝐶, 𝐷⟩ ∈ 𝑅)