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
Theorem	fz0addge0 47601	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 47602	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 47603	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 47604	Join a predecessor to the beginning of an open integer interval. Generalization of fzo0sn0fzo1 13675. (Contributed by AV, 14-Jul-2020.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 < 𝑁) → (𝑀..^𝑁) = ({𝑀} ∪ ((𝑀 + 1)..^𝑁)))
Theorem	fzopredsuc 47605	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 47606	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 47607	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 47608	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 47609*	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 47610	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 47611	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 47612	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 47613	Lemma for gpgedgvtx1 48344. (Contributed by AV, 1-Sep-2025.) (Proof shortened by AV, 8-Sep-2025.)
⊢ 𝐽 = (1..^(⌈‘(𝑁 / 2)))    &   ⊢ 𝐼 = (0..^𝑁)    ⇒   ⊢ ((𝑁 ∈ (ℤ≥‘3) ∧ 𝑋 ∈ 𝐽) → 𝑋 ∈ 𝐼)
Theorem	2tceilhalfelfzo1 47614	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 47615	A condition equivalent to ceiling. Analogous to flbi 13740. (Contributed by AV, 2-Nov-2025.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℤ) → ((⌈‘𝐴) = 𝐵 ↔ (𝐴 ≤ 𝐵 ∧ 𝐵 < (𝐴 + 1))))
Theorem	ceilhalf1 47616	The ceiling of one half is one. (Contributed by AV, 2-Nov-2025.)
⊢ (⌈‘(1 / 2)) = 1
Theorem	rehalfge1 47617	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 47618	The ceiling of half of a positive integer is a positive integer. (Contributed by AV, 2-Nov-2025.)
⊢ (𝑁 ∈ ℕ → (⌈‘(𝑁 / 2)) ∈ ℕ)
Theorem	1elfzo1ceilhalf1 47619	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 47620	Expressing the floor of a division by the modulo operator. (Contributed by AV, 6-Jun-2020.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → (⌊‘(𝐴 / 𝐵)) = ((𝐴 − (𝐴 mod 𝐵)) / 𝐵))
Theorem	ceildivmod 47621	Expressing the ceiling of a division by the modulo operator. (Contributed by AV, 7-Sep-2025.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → (⌈‘(𝐴 / 𝐵)) = ((𝐴 + ((𝐵 − 𝐴) mod 𝐵)) / 𝐵))
Theorem	ceil5half3 47622	The ceiling of half of 5 is 3. (Contributed by AV, 7-Sep-2025.)
⊢ (⌈‘(5 / 2)) = 3
Theorem	submodaddmod 47623	Subtraction and addition modulo a positive integer. (Contributed by AV, 7-Sep-2025.)
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ)) → (((𝐴 + 𝐵) mod 𝑁) = ((𝐴 − 𝐶) mod 𝑁) ↔ ((𝐴 + (𝐵 + 𝐶)) mod 𝑁) = (𝐴 mod 𝑁)))
Theorem	difltmodne 47624	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 47625	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 47626	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 47627	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 47628	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 47629	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 47630	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 47631	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 47632	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 47633	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 47634	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 47635	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 47636	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 47637	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 47638*	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 47639*	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 47640	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 47641	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 47642	8 modulo 5 is 3. (Contributed by AV, 20-Nov-2025.)
⊢ (8 mod 5) = 3
Theorem	modmkpkne 47643	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 47644	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 47645	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 47646	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 47647	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 47648	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 47649	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 47650	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 47651	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 47652	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 47653*	Ordering relation for a strictly monotonic sequence, increasing case. Analogous to monoord 13959 (except that the case 𝑀 = 𝑁 must be excluded). Duplicate of monoords 45581? (Contributed by AV, 12-Jul-2020.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(𝑁 − 1))) → (𝐹‘𝑘) < (𝐹‘(𝑘 + 1)))    ⇒   ⊢ (𝜑 → (𝐹‘𝑀) < (𝐹‘𝑁))
21.48.6.21  Finite and infinite sums - extension
Theorem	fsummsndifre 47654*	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 47655*	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 47656*	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 47657*	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 47658	The injected slot is an element of the structure with replacement. (Contributed by AV, 10-Nov-2021.)
⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ 𝑅 = (𝑆 sSet ⟨𝐴, 𝐵⟩)    ⇒   ⊢ (𝜑 → ⟨𝐴, 𝐵⟩ ∈ 𝑅)
Theorem	setsnidel 47659	The injected slot is an element of the structure with replacement. (Contributed by AV, 10-Nov-2021.)
⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ 𝑅 = (𝑆 sSet ⟨𝐴, 𝐵⟩)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑌)    &   ⊢ (𝜑 → ⟨𝐶, 𝐷⟩ ∈ 𝑆)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐶)    ⇒   ⊢ (𝜑 → ⟨𝐶, 𝐷⟩ ∈ 𝑅)
Theorem	setsv 47660	The value of the structure replacement function is a set. (Contributed by AV, 10-Nov-2021.)
⊢ ((𝑆 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝑆 sSet ⟨𝐴, 𝐵⟩) ∈ V)
21.48.7  Preimages of function values According to Wikipedia ("Image (mathematics)", 17-Mar-2024, https://en.wikipedia.org/wiki/ImageSupport_(mathematics)): "... evaluating a given function 𝑓 at each element of a given subset 𝐴 of its domain produces a set, called the "image of 𝐴 under (or through) 𝑓". Similarly, the inverse image (or preimage) of a given subset 𝐵 of the codomain of 𝑓 is the set of all elements of the domain that map to the members of 𝐵." The preimage of a set 𝐵 under a function 𝑓 is often denoted as "f^-1 (B)", but in set.mm, the idiom (◡𝑓 “ 𝐵) is used. As a special case, the idiom for the preimage of a function value at 𝑋 under a function 𝐹 is (◡𝐹 “ {(𝐹‘𝑋)}) (according to Wikipedia, the preimage of a singleton is also called a "fiber"). We use the label fragment "preima" (as in mptpreima 6197) for theorems about preimages (sometimes, also "imacnv" is used as in fvimacnvi 6999), and "preimafv" (as in preimafvn0 47662) for theorems about preimages of a function value. In this section, 𝑃 = {𝑧 ∣ ∃𝑥 ∈ 𝐴𝑧 = (◡𝐹 “ {(𝐹‘𝑥)})} will be the set of all preimages of function values of a function 𝐹, that means 𝑆 ∈ 𝑃 is a preimage of a function value (see, for example, elsetpreimafv 47667): 𝑆 = (◡𝐹 “ {(𝐹‘𝑥)}). With the help of such a set, it is shown that every function 𝐹:𝐴⟶𝐵 can be decomposed into a surjective and an injective function (see fundcmpsurinj 47691) by constructing a surjective function 𝑔:𝐴–onto→𝑃 and an injective function ℎ:𝑃–1-1→𝐵 so that 𝐹 = (ℎ ∘ 𝑔) ( see fundcmpsurinjpreimafv 47690). See also Wikipedia ("Surjective function", 17-Mar-2024, https://en.wikipedia.org/wiki/Surjective_function 47690 (section "Composition and decomposition"). This is different from the decomposition of 𝐹 into the surjective function 𝑔:𝐴–onto→(𝐹 “ 𝐴) (with (𝑔‘𝑥) = (𝐹‘𝑥) for 𝑥 ∈ 𝐴) and the injective function ℎ = ( I ↾ (𝐹 “ 𝐴)), ( see fundcmpsurinjimaid 47693), see also Wikipedia ("Bijection, injection and surjection", 17-Mar-2024, https://en.wikipedia.org/wiki/Bijection,_injection_and_surjection 47693 (section "Properties"). Finally, it is shown that every function 𝐹:𝐴⟶𝐵 can be decomposed into a surjective, a bijective and an injective function (see fundcmpsurbijinj 47692), by showing that there is a bijection between the set of all preimages of values of a function and the range of the function (see imasetpreimafvbij 47688). From this, both variants of decompositions of a function into a surjective and an injective function can be derived: Let 𝐹 = ((𝐼 ∘ 𝐵) ∘ 𝑆) be a decomposition of a function into a surjective, a bijective and an injective function, then 𝐹 = (𝐽 ∘ 𝑆) with 𝐽 = (𝐼 ∘ 𝐵) (an injective function) is a decomposition into a surjective and an injective function corresponding to fundcmpsurinj 47691, and 𝐹 = (𝐼 ∘ 𝑂) with 𝑂 = (𝐵 ∘ 𝑆) (a surjective function) is a decomposition into a surjective and an injective function corresponding to fundcmpsurinjimaid 47693.
Theorem	preimafvsnel 47661	The preimage of a function value at 𝑋 contains 𝑋. (Contributed by AV, 7-Mar-2024.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → 𝑋 ∈ (◡𝐹 “ {(𝐹‘𝑋)}))
Theorem	preimafvn0 47662	The preimage of a function value is not empty. (Contributed by AV, 7-Mar-2024.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → (◡𝐹 “ {(𝐹‘𝑋)}) ≠ ∅)
Theorem	uniimafveqt 47663*	The union of the image of a subset 𝑆 of the domain of a function with elements having the same function value is the function value at one of the elements of 𝑆. (Contributed by AV, 5-Mar-2024.)
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑆 ⊆ 𝐴 ∧ 𝑋 ∈ 𝑆) → (∀𝑥 ∈ 𝑆 (𝐹‘𝑥) = (𝐹‘𝑋) → ∪ (𝐹 “ 𝑆) = (𝐹‘𝑋)))
Theorem	uniimaprimaeqfv 47664	The union of the image of the preimage of a function value is the function value. (Contributed by AV, 12-Mar-2024.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → ∪ (𝐹 “ (◡𝐹 “ {(𝐹‘𝑋)})) = (𝐹‘𝑋))
Theorem	setpreimafvex 47665*	The class 𝑃 of all preimages of function values is a set. (Contributed by AV, 10-Mar-2024.)
⊢ 𝑃 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (◡𝐹 “ {(𝐹‘𝑥)})}    ⇒   ⊢ (𝐴 ∈ 𝑉 → 𝑃 ∈ V)
Theorem	elsetpreimafvb 47666*	The characterization of an element of the class 𝑃 of all preimages of function values. (Contributed by AV, 10-Mar-2024.)
⊢ 𝑃 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (◡𝐹 “ {(𝐹‘𝑥)})}    ⇒   ⊢ (𝑆 ∈ 𝑉 → (𝑆 ∈ 𝑃 ↔ ∃𝑥 ∈ 𝐴 𝑆 = (◡𝐹 “ {(𝐹‘𝑥)})))
Theorem	elsetpreimafv 47667*	An element of the class 𝑃 of all preimages of function values. (Contributed by AV, 8-Mar-2024.)
⊢ 𝑃 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (◡𝐹 “ {(𝐹‘𝑥)})}    ⇒   ⊢ (𝑆 ∈ 𝑃 → ∃𝑥 ∈ 𝐴 𝑆 = (◡𝐹 “ {(𝐹‘𝑥)}))
Theorem	elsetpreimafvssdm 47668*	An element of the class 𝑃 of all preimages of function values is a subset of the domain of the function. (Contributed by AV, 8-Mar-2024.)
⊢ 𝑃 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (◡𝐹 “ {(𝐹‘𝑥)})}    ⇒   ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ∈ 𝑃) → 𝑆 ⊆ 𝐴)
Theorem	fvelsetpreimafv 47669*	There is an element in a preimage 𝑆 of function values so that 𝑆 is the preimage of the function value at this element. (Contributed by AV, 8-Mar-2024.)
⊢ 𝑃 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (◡𝐹 “ {(𝐹‘𝑥)})}    ⇒   ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ∈ 𝑃) → ∃𝑥 ∈ 𝑆 𝑆 = (◡𝐹 “ {(𝐹‘𝑥)}))
Theorem	preimafvelsetpreimafv 47670*	The preimage of a function value is an element of the class 𝑃 of all preimages of function values. (Contributed by AV, 10-Mar-2024.)
⊢ 𝑃 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (◡𝐹 “ {(𝐹‘𝑥)})}    ⇒   ⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴) → (◡𝐹 “ {(𝐹‘𝑋)}) ∈ 𝑃)
Theorem	preimafvsspwdm 47671*	The class 𝑃 of all preimages of function values is a subset of the power set of the domain of the function. (Contributed by AV, 5-Mar-2024.)
⊢ 𝑃 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (◡𝐹 “ {(𝐹‘𝑥)})}    ⇒   ⊢ (𝐹 Fn 𝐴 → 𝑃 ⊆ 𝒫 𝐴)
Theorem	0nelsetpreimafv 47672*	The empty set is not an element of the class 𝑃 of all preimages of function values. (Contributed by AV, 6-Mar-2024.)
⊢ 𝑃 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (◡𝐹 “ {(𝐹‘𝑥)})}    ⇒   ⊢ (𝐹 Fn 𝐴 → ∅ ∉ 𝑃)
Theorem	elsetpreimafvbi 47673*	An element of the preimage of a function value is an element of the domain of the function with the same value as another element of the preimage. (Contributed by AV, 9-Mar-2024.)
⊢ 𝑃 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (◡𝐹 “ {(𝐹‘𝑥)})}    ⇒   ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ∈ 𝑃 ∧ 𝑋 ∈ 𝑆) → (𝑌 ∈ 𝑆 ↔ (𝑌 ∈ 𝐴 ∧ (𝐹‘𝑌) = (𝐹‘𝑋))))
Theorem	elsetpreimafveqfv 47674*	The elements of the preimage of a function value have the same function values. (Contributed by AV, 5-Mar-2024.)
⊢ 𝑃 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (◡𝐹 “ {(𝐹‘𝑥)})}    ⇒   ⊢ ((𝐹 Fn 𝐴 ∧ (𝑆 ∈ 𝑃 ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆)) → (𝐹‘𝑋) = (𝐹‘𝑌))
Theorem	eqfvelsetpreimafv 47675*	If an element of the domain of the function has the same function value as an element of the preimage of a function value, then it is an element of the same preimage. (Contributed by AV, 9-Mar-2024.)
⊢ 𝑃 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (◡𝐹 “ {(𝐹‘𝑥)})}    ⇒   ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ∈ 𝑃 ∧ 𝑋 ∈ 𝑆) → ((𝑌 ∈ 𝐴 ∧ (𝐹‘𝑌) = (𝐹‘𝑋)) → 𝑌 ∈ 𝑆))
Theorem	elsetpreimafvrab 47676*	An element of the preimage of a function value expressed as a restricted class abstraction. (Contributed by AV, 9-Mar-2024.)
⊢ 𝑃 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (◡𝐹 “ {(𝐹‘𝑥)})}    ⇒   ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ∈ 𝑃 ∧ 𝑋 ∈ 𝑆) → 𝑆 = {𝑥 ∈ 𝐴 ∣ (𝐹‘𝑥) = (𝐹‘𝑋)})
Theorem	imaelsetpreimafv 47677*	The image of an element of the preimage of a function value is the singleton consisting of the function value at one of its elements. (Contributed by AV, 5-Mar-2024.)
⊢ 𝑃 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (◡𝐹 “ {(𝐹‘𝑥)})}    ⇒   ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ∈ 𝑃 ∧ 𝑋 ∈ 𝑆) → (𝐹 “ 𝑆) = {(𝐹‘𝑋)})
Theorem	uniimaelsetpreimafv 47678*	The union of the image of an element of the preimage of a function value is an element of the range of the function. (Contributed by AV, 5-Mar-2024.) (Revised by AV, 22-Mar-2024.)
⊢ 𝑃 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (◡𝐹 “ {(𝐹‘𝑥)})}    ⇒   ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ∈ 𝑃) → ∪ (𝐹 “ 𝑆) ∈ ran 𝐹)
Theorem	elsetpreimafveq 47679*	If two preimages of function values contain elements with identical function values, then both preimages are equal. (Contributed by AV, 8-Mar-2024.)
⊢ 𝑃 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (◡𝐹 “ {(𝐹‘𝑥)})}    ⇒   ⊢ ((𝐹 Fn 𝐴 ∧ (𝑆 ∈ 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑅)) → ((𝐹‘𝑋) = (𝐹‘𝑌) → 𝑆 = 𝑅))
Theorem	fundcmpsurinjlem1 47680*	Lemma 1 for fundcmpsurinj 47691. (Contributed by AV, 4-Mar-2024.)
⊢ 𝑃 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (◡𝐹 “ {(𝐹‘𝑥)})}    &   ⊢ 𝐺 = (𝑥 ∈ 𝐴 ↦ (◡𝐹 “ {(𝐹‘𝑥)}))    ⇒   ⊢ ran 𝐺 = 𝑃
Theorem	fundcmpsurinjlem2 47681*	Lemma 2 for fundcmpsurinj 47691. (Contributed by AV, 4-Mar-2024.)
⊢ 𝑃 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (◡𝐹 “ {(𝐹‘𝑥)})}    &   ⊢ 𝐺 = (𝑥 ∈ 𝐴 ↦ (◡𝐹 “ {(𝐹‘𝑥)}))    ⇒   ⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝑉) → 𝐺:𝐴–onto→𝑃)
Theorem	fundcmpsurinjlem3 47682*	Lemma 3 for fundcmpsurinj 47691. (Contributed by AV, 3-Mar-2024.)
⊢ 𝑃 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (◡𝐹 “ {(𝐹‘𝑥)})}    &   ⊢ 𝐻 = (𝑝 ∈ 𝑃 ↦ ∪ (𝐹 “ 𝑝))    ⇒   ⊢ ((Fun 𝐹 ∧ 𝑋 ∈ 𝑃) → (𝐻‘𝑋) = ∪ (𝐹 “ 𝑋))
Theorem	imasetpreimafvbijlemf 47683*	Lemma for imasetpreimafvbij 47688: the mapping 𝐻 is a function into the range of function 𝐹. (Contributed by AV, 22-Mar-2024.)
⊢ 𝑃 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (◡𝐹 “ {(𝐹‘𝑥)})}    &   ⊢ 𝐻 = (𝑝 ∈ 𝑃 ↦ ∪ (𝐹 “ 𝑝))    ⇒   ⊢ (𝐹 Fn 𝐴 → 𝐻:𝑃⟶(𝐹 “ 𝐴))
Theorem	imasetpreimafvbijlemfv 47684*	Lemma for imasetpreimafvbij 47688: the value of the mapping 𝐻 at a preimage of a value of function 𝐹. (Contributed by AV, 5-Mar-2024.)
⊢ 𝑃 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (◡𝐹 “ {(𝐹‘𝑥)})}    &   ⊢ 𝐻 = (𝑝 ∈ 𝑃 ↦ ∪ (𝐹 “ 𝑝))    ⇒   ⊢ ((𝐹 Fn 𝐴 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ∈ 𝑌) → (𝐻‘𝑌) = (𝐹‘𝑋))
Theorem	imasetpreimafvbijlemfv1 47685*	Lemma for imasetpreimafvbij 47688: for a preimage of a value of function 𝐹 there is an element of the preimage so that the value of the mapping 𝐻 at this preimage is the function value at this element. (Contributed by AV, 5-Mar-2024.)
⊢ 𝑃 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (◡𝐹 “ {(𝐹‘𝑥)})}    &   ⊢ 𝐻 = (𝑝 ∈ 𝑃 ↦ ∪ (𝐹 “ 𝑝))    ⇒   ⊢ ((𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝑃) → ∃𝑦 ∈ 𝑋 (𝐻‘𝑋) = (𝐹‘𝑦))
Theorem	imasetpreimafvbijlemf1 47686*	Lemma for imasetpreimafvbij 47688: the mapping 𝐻 is an injective function into the range of function 𝐹. (Contributed by AV, 9-Mar-2024.) (Revised by AV, 22-Mar-2024.)
⊢ 𝑃 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (◡𝐹 “ {(𝐹‘𝑥)})}    &   ⊢ 𝐻 = (𝑝 ∈ 𝑃 ↦ ∪ (𝐹 “ 𝑝))    ⇒   ⊢ (𝐹 Fn 𝐴 → 𝐻:𝑃–1-1→(𝐹 “ 𝐴))
Theorem	imasetpreimafvbijlemfo 47687*	Lemma for imasetpreimafvbij 47688: the mapping 𝐻 is a function onto the range of function 𝐹. (Contributed by AV, 22-Mar-2024.)
⊢ 𝑃 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (◡𝐹 “ {(𝐹‘𝑥)})}    &   ⊢ 𝐻 = (𝑝 ∈ 𝑃 ↦ ∪ (𝐹 “ 𝑝))    ⇒   ⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝑉) → 𝐻:𝑃–onto→(𝐹 “ 𝐴))
Theorem	imasetpreimafvbij 47688*	The mapping 𝐻 is a bijective function between the set 𝑃 of all preimages of values of function 𝐹 and the range of 𝐹. (Contributed by AV, 22-Mar-2024.)
⊢ 𝑃 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (◡𝐹 “ {(𝐹‘𝑥)})}    &   ⊢ 𝐻 = (𝑝 ∈ 𝑃 ↦ ∪ (𝐹 “ 𝑝))    ⇒   ⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝑉) → 𝐻:𝑃–1-1-onto→(𝐹 “ 𝐴))
Theorem	fundcmpsurbijinjpreimafv 47689*	Every function 𝐹:𝐴⟶𝐵 can be decomposed into a surjective function onto 𝑃, a bijective function from 𝑃 and an injective function into the codomain of 𝐹. (Contributed by AV, 22-Mar-2024.)
⊢ 𝑃 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (◡𝐹 “ {(𝐹‘𝑥)})}    ⇒   ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝑉) → ∃𝑔∃ℎ∃𝑖((𝑔:𝐴–onto→𝑃 ∧ ℎ:𝑃–1-1-onto→(𝐹 “ 𝐴) ∧ 𝑖:(𝐹 “ 𝐴)–1-1→𝐵) ∧ 𝐹 = ((𝑖 ∘ ℎ) ∘ 𝑔)))
Theorem	fundcmpsurinjpreimafv 47690*	Every function 𝐹:𝐴⟶𝐵 can be decomposed into a surjective function onto 𝑃 and an injective function from 𝑃. (Contributed by AV, 12-Mar-2024.) (Proof shortened by AV, 22-Mar-2024.)
⊢ 𝑃 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (◡𝐹 “ {(𝐹‘𝑥)})}    ⇒   ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝑉) → ∃𝑔∃ℎ(𝑔:𝐴–onto→𝑃 ∧ ℎ:𝑃–1-1→𝐵 ∧ 𝐹 = (ℎ ∘ 𝑔)))
Theorem	fundcmpsurinj 47691*	Every function 𝐹:𝐴⟶𝐵 can be decomposed into a surjective and an injective function. (Contributed by AV, 13-Mar-2024.)
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝑉) → ∃𝑔∃ℎ∃𝑝(𝑔:𝐴–onto→𝑝 ∧ ℎ:𝑝–1-1→𝐵 ∧ 𝐹 = (ℎ ∘ 𝑔)))
Theorem	fundcmpsurbijinj 47692*	Every function 𝐹:𝐴⟶𝐵 can be decomposed into a surjective, a bijective and an injective function. (Contributed by AV, 23-Mar-2024.)
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝑉) → ∃𝑔∃ℎ∃𝑖∃𝑝∃𝑞((𝑔:𝐴–onto→𝑝 ∧ ℎ:𝑝–1-1-onto→𝑞 ∧ 𝑖:𝑞–1-1→𝐵) ∧ 𝐹 = ((𝑖 ∘ ℎ) ∘ 𝑔)))
Theorem	fundcmpsurinjimaid 47693*	Every function 𝐹:𝐴⟶𝐵 can be decomposed into a surjective function onto the image (𝐹 “ 𝐴) of the domain of 𝐹 and an injective function from the image (𝐹 “ 𝐴). (Contributed by AV, 17-Mar-2024.)
⊢ 𝐼 = (𝐹 “ 𝐴)    &   ⊢ 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥))    &   ⊢ 𝐻 = ( I ↾ 𝐼)    ⇒   ⊢ (𝐹:𝐴⟶𝐵 → (𝐺:𝐴–onto→𝐼 ∧ 𝐻:𝐼–1-1→𝐵 ∧ 𝐹 = (𝐻 ∘ 𝐺)))
Theorem	fundcmpsurinjALT 47694*	Alternate proof of fundcmpsurinj 47691, based on fundcmpsurinjimaid 47693: Every function 𝐹:𝐴⟶𝐵 can be decomposed into a surjective and an injective function. (Proof modification is discouraged.) (New usage is discouraged.) (Contributed by AV, 13-Mar-2024.)
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝑉) → ∃𝑔∃ℎ∃𝑝(𝑔:𝐴–onto→𝑝 ∧ ℎ:𝑝–1-1→𝐵 ∧ 𝐹 = (ℎ ∘ 𝑔)))
21.48.8  Partitions of real intervals Based on the theorems of the fourierdlem* series of GS's mathbox.
Syntax	ciccp 47695	Extend class notation with the partitions of a closed interval of extended reals.
class RePart
Definition	df-iccp 47696*	Define partitions of a closed interval of extended reals. Such partitions are finite increasing sequences of extended reals. (Contributed by AV, 8-Jul-2020.)
⊢ RePart = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ* ↑m (0...𝑚)) ∣ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1))})
Theorem	iccpval 47697*	Partition consisting of a fixed number 𝑀 of parts. (Contributed by AV, 9-Jul-2020.)
⊢ (𝑀 ∈ ℕ → (RePart‘𝑀) = {𝑝 ∈ (ℝ* ↑m (0...𝑀)) ∣ ∀𝑖 ∈ (0..^𝑀)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1))})
Theorem	iccpart 47698*	A special partition. Corresponds to fourierdlem2 46389 in GS's mathbox. (Contributed by AV, 9-Jul-2020.)
⊢ (𝑀 ∈ ℕ → (𝑃 ∈ (RePart‘𝑀) ↔ (𝑃 ∈ (ℝ* ↑m (0...𝑀)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑃‘𝑖) < (𝑃‘(𝑖 + 1)))))
Theorem	iccpartimp 47699	Implications for a class being a partition. (Contributed by AV, 11-Jul-2020.)
⊢ ((𝑀 ∈ ℕ ∧ 𝑃 ∈ (RePart‘𝑀) ∧ 𝐼 ∈ (0..^𝑀)) → (𝑃 ∈ (ℝ* ↑m (0...𝑀)) ∧ (𝑃‘𝐼) < (𝑃‘(𝐼 + 1))))
Theorem	iccpartres 47700	The restriction of a partition is a partition. (Contributed by AV, 16-Jul-2020.)
⊢ ((𝑀 ∈ ℕ ∧ 𝑃 ∈ (RePart‘(𝑀 + 1))) → (𝑃 ↾ (0...𝑀)) ∈ (RePart‘𝑀))