P. 461 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 46001-46100   *Has distinct variable group(s)

Type	Label	Description
Statement
21.45.6.10  Imaginary and complex number properties - extension
Theorem	readdcnnred 46001	The sum of a real number and an imaginary number is not a real number. (Contributed by AV, 23-Jan-2023.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ (ℂ ∖ ℝ))    ⇒   ⊢ (𝜑 → (𝐴 + 𝐵) ∉ ℝ)
Theorem	resubcnnred 46002	The difference of a real number and an imaginary number is not a real number. (Contributed by AV, 23-Jan-2023.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ (ℂ ∖ ℝ))    ⇒   ⊢ (𝜑 → (𝐴 − 𝐵) ∉ ℝ)
Theorem	recnmulnred 46003	The product of a real number and an imaginary number is not a real number. (Contributed by AV, 23-Jan-2023.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ (ℂ ∖ ℝ))    &   ⊢ (𝜑 → 𝐴 ≠ 0)    ⇒   ⊢ (𝜑 → (𝐴 · 𝐵) ∉ ℝ)
Theorem	cndivrenred 46004	The quotient of an imaginary number and a real number is not a real number. (Contributed by AV, 23-Jan-2023.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ (ℂ ∖ ℝ))    &   ⊢ (𝜑 → 𝐴 ≠ 0)    ⇒   ⊢ (𝜑 → (𝐵 / 𝐴) ∉ ℝ)
Theorem	sqrtnegnre 46005	The square root of a negative number is not a real number. (Contributed by AV, 28-Feb-2023.)
⊢ ((𝑋 ∈ ℝ ∧ 𝑋 < 0) → (√‘𝑋) ∉ ℝ)
21.45.6.11  Nonnegative integers (as a subset of complex numbers) - extension
Theorem	nn0resubcl 46006	Closure law for subtraction of reals, restricted to nonnegative integers. (Contributed by Alexander van der Vekens, 6-Apr-2018.)
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0) → (𝐴 − 𝐵) ∈ ℝ)
21.45.6.12  Integers (as a subset of complex numbers) - extension
Theorem	zgeltp1eq 46007	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.45.6.13  Decimal arithmetic - extension
Theorem	1t10e1p1e11 46008	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 46009	Add 1 to a 2 digit number with carry. This is a special case of decsucc 12717, 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.45.6.14  Upper sets of integers - extension
Theorem	eluzge0nn0 46010	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.45.6.15  Infinity and the extended real number system (cont.) - extension
Theorem	nltle2tri 46011	Negated extended trichotomy law for 'less than' and 'less than or equal to'. (Contributed by AV, 18-Jul-2020.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → ¬ (𝐴 < 𝐵 ∧ 𝐵 ≤ 𝐶 ∧ 𝐶 ≤ 𝐴))
21.45.6.16  Finite intervals of integers - extension
Theorem	ssfz12 46012	Subset relationship for finite sets of sequential integers. (Contributed by Alexander van der Vekens, 16-Mar-2018.)
⊢ ((𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝐾 ≤ 𝐿) → ((𝐾...𝐿) ⊆ (𝑀...𝑁) → (𝑀 ≤ 𝐾 ∧ 𝐿 ≤ 𝑁)))
Theorem	elfz2z 46013	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 46014	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 46015	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 46016	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 46017	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 46018	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 46019	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.45.6.17  Half-open integer ranges - extension
Theorem	fzopred 46020	Join a predecessor to the beginning of an open integer interval. Generalization of fzo0sn0fzo1 13720. (Contributed by AV, 14-Jul-2020.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 < 𝑁) → (𝑀..^𝑁) = ({𝑀} ∪ ((𝑀 + 1)..^𝑁)))
Theorem	fzopredsuc 46021	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 46022	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 46023	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 46024	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	fzoopth 46025	A half-open integer range can represent an ordered pair, analogous to fzopth 13537. (Contributed by Alexander van der Vekens, 1-Jul-2018.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 < 𝑁) → ((𝑀..^𝑁) = (𝐽..^𝐾) ↔ (𝑀 = 𝐽 ∧ 𝑁 = 𝐾)))
Theorem	2ffzoeq 46026*	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.45.6.18  The modulo (remainder) operation - extension
Theorem	m1mod0mod1 46027	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 46028	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})
21.45.6.19  The infinite sequence builder "seq"
Theorem	smonoord 46029*	Ordering relation for a strictly monotonic sequence, increasing case. Analogous to monoord 13997 (except that the case 𝑀 = 𝑁 must be excluded). Duplicate of monoords 43997? (Contributed by AV, 12-Jul-2020.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘(𝑀 + 1)))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...(𝑁 − 1))) → (𝐹‘𝑘) < (𝐹‘(𝑘 + 1)))    ⇒   ⊢ (𝜑 → (𝐹‘𝑀) < (𝐹‘𝑁))
21.45.6.20  Finite and infinite sums - extension
Theorem	fsummsndifre 46030*	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 46031*	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 46032*	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 46033*	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.45.6.21  Extensible structures - extension
Theorem	setsidel 46034	The injected slot is an element of the structure with replacement. (Contributed by AV, 10-Nov-2021.)
⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ 𝑅 = (𝑆 sSet ⟨𝐴, 𝐵⟩)    ⇒   ⊢ (𝜑 → ⟨𝐴, 𝐵⟩ ∈ 𝑅)
Theorem	setsnidel 46035	The injected slot is an element of the structure with replacement. (Contributed by AV, 10-Nov-2021.)
⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ 𝑅 = (𝑆 sSet ⟨𝐴, 𝐵⟩)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑌)    &   ⊢ (𝜑 → ⟨𝐶, 𝐷⟩ ∈ 𝑆)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐶)    ⇒   ⊢ (𝜑 → ⟨𝐶, 𝐷⟩ ∈ 𝑅)
Theorem	setsv 46036	The value of the structure replacement function is a set. (Contributed by AV, 10-Nov-2021.)
⊢ ((𝑆 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝑆 sSet ⟨𝐴, 𝐵⟩) ∈ V)
21.45.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 6237) for theorems about preimages (sometimes, also "imacnv" is used as in fvimacnvi 7053), and "preimafv" (as in preimafvn0 46038) 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 46043): 𝑆 = (◡𝐹 “ {(𝐹‘𝑥)}). 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 46067) by constructing a surjective function 𝑔:𝐴–onto→𝑃 and an injective function ℎ:𝑃–1-1→𝐵 so that 𝐹 = (ℎ ∘ 𝑔) ( see fundcmpsurinjpreimafv 46066). See also Wikipedia ("Surjective function", 17-Mar-2024, https://en.wikipedia.org/wiki/Surjective_function 46066 (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 46069), see also Wikipedia ("Bijection, injection and surjection", 17-Mar-2024, https://en.wikipedia.org/wiki/Bijection,_injection_and_surjection 46069 (section "Properties"). Finally, it is shown that every function 𝐹:𝐴⟶𝐵 can be decomposed into a surjective, a bijective and an injective function (see fundcmpsurbijinj 46068), 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 46064). 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 46067, and 𝐹 = (𝐼 ∘ 𝑂) with 𝑂 = (𝐵 ∘ 𝑆) (a surjective function) is a decomposition into a surjective and an injective function corresponding to fundcmpsurinjimaid 46069.
Theorem	preimafvsnel 46037	The preimage of a function value at 𝑋 contains 𝑋. (Contributed by AV, 7-Mar-2024.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → 𝑋 ∈ (◡𝐹 “ {(𝐹‘𝑋)}))
Theorem	preimafvn0 46038	The preimage of a function value is not empty. (Contributed by AV, 7-Mar-2024.)
⊢ ((𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → (◡𝐹 “ {(𝐹‘𝑋)}) ≠ ∅)
Theorem	uniimafveqt 46039*	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 46040	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 46041*	The class 𝑃 of all preimages of function values is a set. (Contributed by AV, 10-Mar-2024.)
⊢ 𝑃 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (◡𝐹 “ {(𝐹‘𝑥)})}    ⇒   ⊢ (𝐴 ∈ 𝑉 → 𝑃 ∈ V)
Theorem	elsetpreimafvb 46042*	The characterization of an element of the class 𝑃 of all preimages of function values. (Contributed by AV, 10-Mar-2024.)
⊢ 𝑃 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (◡𝐹 “ {(𝐹‘𝑥)})}    ⇒   ⊢ (𝑆 ∈ 𝑉 → (𝑆 ∈ 𝑃 ↔ ∃𝑥 ∈ 𝐴 𝑆 = (◡𝐹 “ {(𝐹‘𝑥)})))
Theorem	elsetpreimafv 46043*	An element of the class 𝑃 of all preimages of function values. (Contributed by AV, 8-Mar-2024.)
⊢ 𝑃 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (◡𝐹 “ {(𝐹‘𝑥)})}    ⇒   ⊢ (𝑆 ∈ 𝑃 → ∃𝑥 ∈ 𝐴 𝑆 = (◡𝐹 “ {(𝐹‘𝑥)}))
Theorem	elsetpreimafvssdm 46044*	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 46045*	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 46046*	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 46047*	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 46048*	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 46049*	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 46050*	The elements of the preimage of a function value have the same function values. (Contributed by AV, 5-Mar-2024.)
⊢ 𝑃 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (◡𝐹 “ {(𝐹‘𝑥)})}    ⇒   ⊢ ((𝐹 Fn 𝐴 ∧ (𝑆 ∈ 𝑃 ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆)) → (𝐹‘𝑋) = (𝐹‘𝑌))
Theorem	eqfvelsetpreimafv 46051*	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 46052*	An element of the preimage of a function value expressed as a restricted class abstraction. (Contributed by AV, 9-Mar-2024.)
⊢ 𝑃 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (◡𝐹 “ {(𝐹‘𝑥)})}    ⇒   ⊢ ((𝐹 Fn 𝐴 ∧ 𝑆 ∈ 𝑃 ∧ 𝑋 ∈ 𝑆) → 𝑆 = {𝑥 ∈ 𝐴 ∣ (𝐹‘𝑥) = (𝐹‘𝑋)})
Theorem	imaelsetpreimafv 46053*	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 46054*	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 46055*	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 46056*	Lemma 1 for fundcmpsurinj 46067. (Contributed by AV, 4-Mar-2024.)
⊢ 𝑃 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (◡𝐹 “ {(𝐹‘𝑥)})}    &   ⊢ 𝐺 = (𝑥 ∈ 𝐴 ↦ (◡𝐹 “ {(𝐹‘𝑥)}))    ⇒   ⊢ ran 𝐺 = 𝑃
Theorem	fundcmpsurinjlem2 46057*	Lemma 2 for fundcmpsurinj 46067. (Contributed by AV, 4-Mar-2024.)
⊢ 𝑃 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (◡𝐹 “ {(𝐹‘𝑥)})}    &   ⊢ 𝐺 = (𝑥 ∈ 𝐴 ↦ (◡𝐹 “ {(𝐹‘𝑥)}))    ⇒   ⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝑉) → 𝐺:𝐴–onto→𝑃)
Theorem	fundcmpsurinjlem3 46058*	Lemma 3 for fundcmpsurinj 46067. (Contributed by AV, 3-Mar-2024.)
⊢ 𝑃 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (◡𝐹 “ {(𝐹‘𝑥)})}    &   ⊢ 𝐻 = (𝑝 ∈ 𝑃 ↦ ∪ (𝐹 “ 𝑝))    ⇒   ⊢ ((Fun 𝐹 ∧ 𝑋 ∈ 𝑃) → (𝐻‘𝑋) = ∪ (𝐹 “ 𝑋))
Theorem	imasetpreimafvbijlemf 46059*	Lemma for imasetpreimafvbij 46064: the mapping 𝐻 is a function into the range of function 𝐹. (Contributed by AV, 22-Mar-2024.)
⊢ 𝑃 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (◡𝐹 “ {(𝐹‘𝑥)})}    &   ⊢ 𝐻 = (𝑝 ∈ 𝑃 ↦ ∪ (𝐹 “ 𝑝))    ⇒   ⊢ (𝐹 Fn 𝐴 → 𝐻:𝑃⟶(𝐹 “ 𝐴))
Theorem	imasetpreimafvbijlemfv 46060*	Lemma for imasetpreimafvbij 46064: the value of the mapping 𝐻 at a preimage of a value of function 𝐹. (Contributed by AV, 5-Mar-2024.)
⊢ 𝑃 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (◡𝐹 “ {(𝐹‘𝑥)})}    &   ⊢ 𝐻 = (𝑝 ∈ 𝑃 ↦ ∪ (𝐹 “ 𝑝))    ⇒   ⊢ ((𝐹 Fn 𝐴 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ∈ 𝑌) → (𝐻‘𝑌) = (𝐹‘𝑋))
Theorem	imasetpreimafvbijlemfv1 46061*	Lemma for imasetpreimafvbij 46064: 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 46062*	Lemma for imasetpreimafvbij 46064: 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 46063*	Lemma for imasetpreimafvbij 46064: the mapping 𝐻 is a function onto the range of function 𝐹. (Contributed by AV, 22-Mar-2024.)
⊢ 𝑃 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (◡𝐹 “ {(𝐹‘𝑥)})}    &   ⊢ 𝐻 = (𝑝 ∈ 𝑃 ↦ ∪ (𝐹 “ 𝑝))    ⇒   ⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝑉) → 𝐻:𝑃–onto→(𝐹 “ 𝐴))
Theorem	imasetpreimafvbij 46064*	The mapping 𝐻 is a bijective function betwen 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 46065*	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 46066*	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 46067*	Every function 𝐹:𝐴⟶𝐵 can be decomposed into a surjective and an injective function. (Contributed by AV, 13-Mar-2024.)
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝑉) → ∃𝑔∃ℎ∃𝑝(𝑔:𝐴–onto→𝑝 ∧ ℎ:𝑝–1-1→𝐵 ∧ 𝐹 = (ℎ ∘ 𝑔)))
Theorem	fundcmpsurbijinj 46068*	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 46069*	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 46070*	Alternate proof of fundcmpsurinj 46067, based on fundcmpsurinjimaid 46069: 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.45.8  Partitions of real intervals Based on the theorems of the fourierdlem* series of GS's mathbox.
Syntax	ciccp 46071	Extend class notation with the partitions of a closed interval of extended reals.
class RePart
Definition	df-iccp 46072*	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 46073*	Partition consisting of a fixed number 𝑀 of parts. (Contributed by AV, 9-Jul-2020.)
⊢ (𝑀 ∈ ℕ → (RePart‘𝑀) = {𝑝 ∈ (ℝ* ↑m (0...𝑀)) ∣ ∀𝑖 ∈ (0..^𝑀)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1))})
Theorem	iccpart 46074*	A special partition. Corresponds to fourierdlem2 44815 in GS's mathbox. (Contributed by AV, 9-Jul-2020.)
⊢ (𝑀 ∈ ℕ → (𝑃 ∈ (RePart‘𝑀) ↔ (𝑃 ∈ (ℝ* ↑m (0...𝑀)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑃‘𝑖) < (𝑃‘(𝑖 + 1)))))
Theorem	iccpartimp 46075	Implications for a class being a partition. (Contributed by AV, 11-Jul-2020.)
⊢ ((𝑀 ∈ ℕ ∧ 𝑃 ∈ (RePart‘𝑀) ∧ 𝐼 ∈ (0..^𝑀)) → (𝑃 ∈ (ℝ* ↑m (0...𝑀)) ∧ (𝑃‘𝐼) < (𝑃‘(𝐼 + 1))))
Theorem	iccpartres 46076	The restriction of a partition is a partition. (Contributed by AV, 16-Jul-2020.)
⊢ ((𝑀 ∈ ℕ ∧ 𝑃 ∈ (RePart‘(𝑀 + 1))) → (𝑃 ↾ (0...𝑀)) ∈ (RePart‘𝑀))
Theorem	iccpartxr 46077	If there is a partition, then all intermediate points and bounds are extended real numbers. (Contributed by AV, 11-Jul-2020.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑃 ∈ (RePart‘𝑀))    &   ⊢ (𝜑 → 𝐼 ∈ (0...𝑀))    ⇒   ⊢ (𝜑 → (𝑃‘𝐼) ∈ ℝ*)
Theorem	iccpartgtprec 46078	If there is a partition, then all intermediate points and the upper bound are strictly greater than the preceeding intermediate points or lower bound. (Contributed by AV, 11-Jul-2020.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑃 ∈ (RePart‘𝑀))    &   ⊢ (𝜑 → 𝐼 ∈ (1...𝑀))    ⇒   ⊢ (𝜑 → (𝑃‘(𝐼 − 1)) < (𝑃‘𝐼))
Theorem	iccpartipre 46079	If there is a partition, then all intermediate points are real numbers. (Contributed by AV, 11-Jul-2020.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑃 ∈ (RePart‘𝑀))    &   ⊢ (𝜑 → 𝐼 ∈ (1..^𝑀))    ⇒   ⊢ (𝜑 → (𝑃‘𝐼) ∈ ℝ)
Theorem	iccpartiltu 46080*	If there is a partition, then all intermediate points are strictly less than the upper bound. (Contributed by AV, 12-Jul-2020.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑃 ∈ (RePart‘𝑀))    ⇒   ⊢ (𝜑 → ∀𝑖 ∈ (1..^𝑀)(𝑃‘𝑖) < (𝑃‘𝑀))
Theorem	iccpartigtl 46081*	If there is a partition, then all intermediate points are strictly greater than the lower bound. (Contributed by AV, 12-Jul-2020.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑃 ∈ (RePart‘𝑀))    ⇒   ⊢ (𝜑 → ∀𝑖 ∈ (1..^𝑀)(𝑃‘0) < (𝑃‘𝑖))
Theorem	iccpartlt 46082	If there is a partition, then the lower bound is strictly less than the upper bound. Corresponds to fourierdlem11 44824 in GS's mathbox. (Contributed by AV, 12-Jul-2020.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑃 ∈ (RePart‘𝑀))    ⇒   ⊢ (𝜑 → (𝑃‘0) < (𝑃‘𝑀))
Theorem	iccpartltu 46083*	If there is a partition, then all intermediate points and the lower bound are strictly less than the upper bound. (Contributed by AV, 14-Jul-2020.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑃 ∈ (RePart‘𝑀))    ⇒   ⊢ (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑃‘𝑖) < (𝑃‘𝑀))
Theorem	iccpartgtl 46084*	If there is a partition, then all intermediate points and the upper bound are strictly greater than the lower bound. (Contributed by AV, 14-Jul-2020.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑃 ∈ (RePart‘𝑀))    ⇒   ⊢ (𝜑 → ∀𝑖 ∈ (1...𝑀)(𝑃‘0) < (𝑃‘𝑖))
Theorem	iccpartgt 46085*	If there is a partition, then all intermediate points and the bounds are strictly ordered. (Contributed by AV, 18-Jul-2020.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑃 ∈ (RePart‘𝑀))    ⇒   ⊢ (𝜑 → ∀𝑖 ∈ (0...𝑀)∀𝑗 ∈ (0...𝑀)(𝑖 < 𝑗 → (𝑃‘𝑖) < (𝑃‘𝑗)))
Theorem	iccpartleu 46086*	If there is a partition, then all intermediate points and the lower and the upper bound are less than or equal to the upper bound. (Contributed by AV, 14-Jul-2020.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑃 ∈ (RePart‘𝑀))    ⇒   ⊢ (𝜑 → ∀𝑖 ∈ (0...𝑀)(𝑃‘𝑖) ≤ (𝑃‘𝑀))
Theorem	iccpartgel 46087*	If there is a partition, then all intermediate points and the upper and the lower bound are greater than or equal to the lower bound. (Contributed by AV, 14-Jul-2020.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑃 ∈ (RePart‘𝑀))    ⇒   ⊢ (𝜑 → ∀𝑖 ∈ (0...𝑀)(𝑃‘0) ≤ (𝑃‘𝑖))
Theorem	iccpartrn 46088	If there is a partition, then all intermediate points and bounds are contained in a closed interval of extended reals. (Contributed by AV, 14-Jul-2020.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑃 ∈ (RePart‘𝑀))    ⇒   ⊢ (𝜑 → ran 𝑃 ⊆ ((𝑃‘0)[,](𝑃‘𝑀)))
Theorem	iccpartf 46089	The range of the partition is between its starting point and its ending point. Corresponds to fourierdlem15 44828 in GS's mathbox. (Contributed by Glauco Siliprandi, 11-Dec-2019.) (Revised by AV, 14-Jul-2020.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑃 ∈ (RePart‘𝑀))    ⇒   ⊢ (𝜑 → 𝑃:(0...𝑀)⟶((𝑃‘0)[,](𝑃‘𝑀)))
Theorem	iccpartel 46090	If there is a partition, then all intermediate points and bounds are contained in a closed interval of extended reals. (Contributed by AV, 14-Jul-2020.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑃 ∈ (RePart‘𝑀))    ⇒   ⊢ ((𝜑 ∧ 𝐼 ∈ (0...𝑀)) → (𝑃‘𝐼) ∈ ((𝑃‘0)[,](𝑃‘𝑀)))
Theorem	iccelpart 46091*	An element of any partitioned half-open interval of extended reals is an element of a part of this partition. (Contributed by AV, 18-Jul-2020.)
⊢ (𝑀 ∈ ℕ → ∀𝑝 ∈ (RePart‘𝑀)(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑀)) → ∃𝑖 ∈ (0..^𝑀)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))))
Theorem	iccpartiun 46092*	A half-open interval of extended reals is the union of the parts of its partition. (Contributed by AV, 18-Jul-2020.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑃 ∈ (RePart‘𝑀))    ⇒   ⊢ (𝜑 → ((𝑃‘0)[,)(𝑃‘𝑀)) = ∪ 𝑖 ∈ (0..^𝑀)((𝑃‘𝑖)[,)(𝑃‘(𝑖 + 1))))
Theorem	icceuelpartlem 46093	Lemma for icceuelpart 46094. (Contributed by AV, 19-Jul-2020.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑃 ∈ (RePart‘𝑀))    ⇒   ⊢ (𝜑 → ((𝐼 ∈ (0..^𝑀) ∧ 𝐽 ∈ (0..^𝑀)) → (𝐼 < 𝐽 → (𝑃‘(𝐼 + 1)) ≤ (𝑃‘𝐽))))
Theorem	icceuelpart 46094*	An element of a partitioned half-open interval of extended reals is an element of exactly one part of the partition. (Contributed by AV, 19-Jul-2020.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑃 ∈ (RePart‘𝑀))    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ ((𝑃‘0)[,)(𝑃‘𝑀))) → ∃!𝑖 ∈ (0..^𝑀)𝑋 ∈ ((𝑃‘𝑖)[,)(𝑃‘(𝑖 + 1))))
Theorem	iccpartdisj 46095*	The segments of a partitioned half-open interval of extended reals are a disjoint collection. (Contributed by AV, 19-Jul-2020.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑃 ∈ (RePart‘𝑀))    ⇒   ⊢ (𝜑 → Disj 𝑖 ∈ (0..^𝑀)((𝑃‘𝑖)[,)(𝑃‘(𝑖 + 1))))
Theorem	iccpartnel 46096	A point of a partition is not an element of any open interval determined by the partition. Corresponds to fourierdlem12 44825 in GS's mathbox. (Contributed by Glauco Siliprandi, 11-Dec-2019.) (Revised by AV, 8-Jul-2020.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑃 ∈ (RePart‘𝑀))    &   ⊢ (𝜑 → 𝑋 ∈ ran 𝑃)    ⇒   ⊢ ((𝜑 ∧ 𝐼 ∈ (0..^𝑀)) → ¬ 𝑋 ∈ ((𝑃‘𝐼)(,)(𝑃‘(𝐼 + 1))))
21.45.9  Shifting functions with an integer range domain
Theorem	fargshiftfv 46097*	If a class is a function, then the values of the "shifted function" correspond to the function values of the class. (Contributed by Alexander van der Vekens, 23-Nov-2017.)
⊢ 𝐺 = (𝑥 ∈ (0..^(♯‘𝐹)) ↦ (𝐹‘(𝑥 + 1)))    ⇒   ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐹:(1...𝑁)⟶dom 𝐸) → (𝑋 ∈ (0..^𝑁) → (𝐺‘𝑋) = (𝐹‘(𝑋 + 1))))
Theorem	fargshiftf 46098*	If a class is a function, then also its "shifted function" is a function. (Contributed by Alexander van der Vekens, 23-Nov-2017.)
⊢ 𝐺 = (𝑥 ∈ (0..^(♯‘𝐹)) ↦ (𝐹‘(𝑥 + 1)))    ⇒   ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐹:(1...𝑁)⟶dom 𝐸) → 𝐺:(0..^(♯‘𝐹))⟶dom 𝐸)
Theorem	fargshiftf1 46099*	If a function is 1-1, then also the shifted function is 1-1. (Contributed by Alexander van der Vekens, 23-Nov-2017.)
⊢ 𝐺 = (𝑥 ∈ (0..^(♯‘𝐹)) ↦ (𝐹‘(𝑥 + 1)))    ⇒   ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐹:(1...𝑁)–1-1→dom 𝐸) → 𝐺:(0..^(♯‘𝐹))–1-1→dom 𝐸)
Theorem	fargshiftfo 46100*	If a function is onto, then also the shifted function is onto. (Contributed by Alexander van der Vekens, 24-Nov-2017.)
⊢ 𝐺 = (𝑥 ∈ (0..^(♯‘𝐹)) ↦ (𝐹‘(𝑥 + 1)))    ⇒   ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐹:(1...𝑁)–onto→dom 𝐸) → 𝐺:(0..^(♯‘𝐹))–onto→dom 𝐸)