P. 469 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 46801-46900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	smflimsupmpt 46801*	The superior limit of a sequence of sigma-measurable functions is sigma-measurable. Proposition 121F (d) of [Fremlin1] p. 39 . 𝐴 can contain 𝑚 as a free variable, in other words it can be thought of as an indexed collection 𝐴(𝑚). 𝐵 can be thought of as a collection with two indices 𝐵(𝑚, 𝑥). (Contributed by Glauco Siliprandi, 23-Oct-2021.)
⊢ Ⅎ𝑚𝜑    &   ⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑛𝜑    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑊)    &   ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ (SMblFn‘𝑆))    &   ⊢ 𝐷 = {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ≥‘𝑛)𝐴 ∣ (lim sup‘(𝑚 ∈ 𝑍 ↦ 𝐵)) ∈ ℝ}    &   ⊢ 𝐺 = (𝑥 ∈ 𝐷 ↦ (lim sup‘(𝑚 ∈ 𝑍 ↦ 𝐵)))    ⇒   ⊢ (𝜑 → 𝐺 ∈ (SMblFn‘𝑆))
Theorem	smfliminflem 46802*	The inferior limit of a countable set of sigma-measurable functions is sigma-measurable. Proposition 121F (e) of [Fremlin1] p. 39 . (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐹:𝑍⟶(SMblFn‘𝑆))    &   ⊢ 𝐷 = {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim inf‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ}    &   ⊢ 𝐺 = (𝑥 ∈ 𝐷 ↦ (lim inf‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))))    ⇒   ⊢ (𝜑 → 𝐺 ∈ (SMblFn‘𝑆))
Theorem	smfliminf 46803*	The inferior limit of a countable set of sigma-measurable functions is sigma-measurable. Proposition 121F (e) of [Fremlin1] p. 39 . (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ Ⅎ𝑚𝐹    &   ⊢ Ⅎ𝑥𝐹    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐹:𝑍⟶(SMblFn‘𝑆))    &   ⊢ 𝐷 = {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ≥‘𝑛)dom (𝐹‘𝑚) ∣ (lim inf‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))) ∈ ℝ}    &   ⊢ 𝐺 = (𝑥 ∈ 𝐷 ↦ (lim inf‘(𝑚 ∈ 𝑍 ↦ ((𝐹‘𝑚)‘𝑥))))    ⇒   ⊢ (𝜑 → 𝐺 ∈ (SMblFn‘𝑆))
Theorem	smfliminfmpt 46804*	The inferior limit of a countable set of sigma-measurable functions is sigma-measurable. Proposition 121F (e) of [Fremlin1] p. 39 . 𝐴 can contain 𝑚 as a free variable, in other words it can be thought of as an indexed collection 𝐴(𝑚). 𝐵 can be thought of as a collection with two indices 𝐵(𝑚, 𝑥). (Contributed by Glauco Siliprandi, 2-Jan-2022.)
⊢ Ⅎ𝑚𝜑    &   ⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑛𝜑    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ (SMblFn‘𝑆))    &   ⊢ 𝐷 = {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈ (ℤ≥‘𝑛)𝐴 ∣ (lim inf‘(𝑚 ∈ 𝑍 ↦ 𝐵)) ∈ ℝ}    &   ⊢ 𝐺 = (𝑥 ∈ 𝐷 ↦ (lim inf‘(𝑚 ∈ 𝑍 ↦ 𝐵)))    ⇒   ⊢ (𝜑 → 𝐺 ∈ (SMblFn‘𝑆))
Theorem	adddmmbl 46805	If two functions have domains in the sigma-algebra, the domain of their addition also belongs to the sigma-algebra. This is the first statement of Proposition 121H of [Fremlin1], p. 39. Note: While the theorem in the book assumes the functions are sigma-measurable, this assumption is unnecessary for the part concerning their addition. (Contributed by Glauco Siliprandi, 30-Dec-2024.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑆)    ⇒   ⊢ (𝜑 → dom (𝑥 ∈ (𝐴 ∩ 𝐵) ↦ (𝐶 + 𝐷)) ∈ 𝑆)
Theorem	adddmmbl2 46806	If two functions have domains in the sigma-algebra, the domain of their addition also belongs to the sigma-algebra. This is the first statement of Proposition 121H of [Fremlin1], p. 39. Note: While the theorem in the book assumes the functions are sigma-measurable, this assumption is unnecessary for the part concerning their addition. (Contributed by Glauco Siliprandi, 30-Dec-2024.)
⊢ Ⅎ𝑥𝐹    &   ⊢ Ⅎ𝑥𝐺    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → dom 𝐹 ∈ 𝑆)    &   ⊢ (𝜑 → dom 𝐺 ∈ 𝑆)    &   ⊢ 𝐻 = (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹‘𝑥) + (𝐺‘𝑥)))    ⇒   ⊢ (𝜑 → dom 𝐻 ∈ 𝑆)
Theorem	muldmmbl 46807	If two functions have domains in the sigma-algebra, the domain of their multiplication also belongs to the sigma-algebra. This is the second statement of Proposition 121H of [Fremlin1], p. 39. Note: While the theorem in the book assumes the functions are sigma-measurable, this assumption is unnecessary for the part concerning their multiplication. (Contributed by Glauco Siliprandi, 30-Dec-2024.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑆)    ⇒   ⊢ (𝜑 → dom (𝑥 ∈ (𝐴 ∩ 𝐵) ↦ (𝐶 · 𝐷)) ∈ 𝑆)
Theorem	muldmmbl2 46808	If two functions have domains in the sigma-algebra, the domain of their multiplication also belongs to the sigma-algebra. This is the second statement of Proposition 121H of [Fremlin1], p. 39. Note: While the theorem in the book assumes the functions are sigma-measurable, this assumption is unnecessary for the part concerning their multiplication. (Contributed by Glauco Siliprandi, 30-Dec-2024.)
⊢ Ⅎ𝑥𝐹    &   ⊢ Ⅎ𝑥𝐺    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → dom 𝐹 ∈ 𝑆)    &   ⊢ (𝜑 → dom 𝐺 ∈ 𝑆)    &   ⊢ 𝐻 = (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹‘𝑥) · (𝐺‘𝑥)))    ⇒   ⊢ (𝜑 → dom 𝐻 ∈ 𝑆)
Theorem	smfdmmblpimne 46809*	If a measurable function w.r.t. to a sigma-algebra has domain in the sigma-algebra, the set of elements that are not mapped to a given real, is in the sigma-algebra (Contributed by Glauco Siliprandi, 5-Jan-2025.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝐴    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑆)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ (SMblFn‘𝑆))    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ 𝐷 = {𝑥 ∈ 𝐴 ∣ 𝐵 ≠ 𝐶}    ⇒   ⊢ (𝜑 → 𝐷 ∈ 𝑆)
Theorem	smfdivdmmbl 46810	If a functions and a sigma-measurable function have domains in the sigma-algebra, the domain of the division of the two functions is in the sigma-algebra. This is the third statement of Proposition 121H of [Fremlin1] p. 39 . Note: While the theorem in the book assumes both functions are sigma-measurable, this assumption is unnecessary for the part concerning their division, for the function at the numerator (it is needed only for the function at the denominator). (Contributed by Glauco Siliprandi, 5-Jan-2025.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝐵    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑆)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐷 ∈ 𝑊)    &   ⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ 𝐷) ∈ (SMblFn‘𝑆))    &   ⊢ 𝐸 = {𝑥 ∈ 𝐵 ∣ 𝐷 ≠ 0}    ⇒   ⊢ (𝜑 → (𝐴 ∩ 𝐸) ∈ 𝑆)
Theorem	smfpimne 46811*	Given a function measurable w.r.t. to a sigma-algebra, the preimage of reals that are different from a value in the extended reals is in the subspace of sigma-algebra induced by its domain. (Contributed by Glauco Siliprandi, 5-Jan-2025.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝐹    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐹 ∈ (SMblFn‘𝑆))    &   ⊢ 𝐷 = dom 𝐹    &   ⊢ (𝜑 → 𝐴 ∈ ℝ*)    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) ≠ 𝐴} ∈ (𝑆 ↾t 𝐷))
Theorem	smfpimne2 46812*	Given a function measurable w.r.t. to a sigma-algebra, the preimage of reals that are different from a value is in the subspace sigma-algebra induced by its domain. Notice that 𝐴 is not assumed to be an extended real. (Contributed by Glauco Siliprandi, 5-Jan-2025.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝐹    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐹 ∈ (SMblFn‘𝑆))    &   ⊢ 𝐷 = dom 𝐹    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝐷 ∣ (𝐹‘𝑥) ≠ 𝐴} ∈ (𝑆 ↾t 𝐷))
Theorem	smfdivdmmbl2 46813	If a functions and a sigma-measurable function have domains in the sigma-algebra, the domain of the division of the two functions is in the sigma-algebra. This is the third statement of Proposition 121H of [Fremlin1] p. 39 . Note: While the theorem in the book assumes both functions are sigma-measurable, this assumption is unnecessary for the part concerning their division, for the function at the numerator. It is required only for the function at the denominator. (Contributed by Glauco Siliprandi, 5-Jan-2025.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝐹    &   ⊢ Ⅎ𝑥𝐺    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝑉)    &   ⊢ (𝜑 → 𝐺 ∈ (SMblFn‘𝑆))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑆)    &   ⊢ (𝜑 → dom 𝐺 ∈ 𝑆)    &   ⊢ 𝐷 = {𝑥 ∈ dom 𝐺 ∣ (𝐺‘𝑥) ≠ 0}    &   ⊢ 𝐻 = (𝑥 ∈ (dom 𝐹 ∩ 𝐷) ↦ ((𝐹‘𝑥) / (𝐺‘𝑥)))    ⇒   ⊢ (𝜑 → dom 𝐻 ∈ 𝑆)
Theorem	fsupdm 46814*	The domain of the sup function is defined in Proposition 121F (b) of [Fremlin1], p. 38. Note that this definition of the sup function is quite general, as it does not require the original functions to be sigma-measurable, and it could be applied to uncountable sets of functions. The equality proved here is part of the proof of the fourth statement of Proposition 121H in [Fremlin1], p. 39. (Contributed by Glauco Siliprandi, 24-Jan-2025.)
⊢ Ⅎ𝑛𝜑    &   ⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑚𝜑    &   ⊢ Ⅎ𝑥𝐹    &   ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛):dom (𝐹‘𝑛)⟶ℝ*)    &   ⊢ 𝐷 = {𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛) ∣ ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 ((𝐹‘𝑛)‘𝑥) ≤ 𝑦}    &   ⊢ 𝐻 = (𝑛 ∈ 𝑍 ↦ (𝑚 ∈ ℕ ↦ {𝑥 ∈ dom (𝐹‘𝑛) ∣ ((𝐹‘𝑛)‘𝑥) < 𝑚}))    ⇒   ⊢ (𝜑 → 𝐷 = ∪ 𝑚 ∈ ℕ ∩ 𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚))
Theorem	fsupdm2 46815*	The domain of the sup function is defined in Proposition 121F (b) of [Fremlin1], p. 38. Note that this definition of the sup function is quite general, as it does not require the original functions to be sigma-measurable, and it could be applied to uncountable sets of functions. The equality proved here is part of the proof of the fourth statement of Proposition 121H in [Fremlin1], p. 39. (Contributed by Glauco Siliprandi, 24-Jan-2025.)
⊢ Ⅎ𝑛𝜑    &   ⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑚𝜑    &   ⊢ Ⅎ𝑥𝐹    &   ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛):dom (𝐹‘𝑛)⟶ℝ*)    &   ⊢ 𝐷 = {𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛) ∣ ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 ((𝐹‘𝑛)‘𝑥) ≤ 𝑦}    &   ⊢ 𝐺 = (𝑥 ∈ 𝐷 ↦ sup(ran (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < ))    &   ⊢ 𝐻 = (𝑛 ∈ 𝑍 ↦ (𝑚 ∈ ℕ ↦ {𝑥 ∈ dom (𝐹‘𝑛) ∣ ((𝐹‘𝑛)‘𝑥) < 𝑚}))    ⇒   ⊢ (𝜑 → dom 𝐺 = ∪ 𝑚 ∈ ℕ ∩ 𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚))
Theorem	smfsupdmmbllem 46816*	If a countable set of sigma-measurable functions have domains in the sigma-algebra, then their supremum function has the domain in the sigma-algebra. This is the fourth statement of Proposition 121H of [Fremlin1] p. 39 . (Contributed by Glauco Siliprandi, 24-Jan-2025.)
⊢ Ⅎ𝑛𝜑    &   ⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑚𝜑    &   ⊢ Ⅎ𝑥𝐹    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐹:𝑍⟶(SMblFn‘𝑆))    &   ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → dom (𝐹‘𝑛) ∈ 𝑆)    &   ⊢ 𝐷 = {𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛) ∣ ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 ((𝐹‘𝑛)‘𝑥) ≤ 𝑦}    &   ⊢ 𝐻 = (𝑛 ∈ 𝑍 ↦ (𝑚 ∈ ℕ ↦ {𝑥 ∈ dom (𝐹‘𝑛) ∣ ((𝐹‘𝑛)‘𝑥) < 𝑚}))    &   ⊢ 𝐺 = (𝑥 ∈ 𝐷 ↦ sup(ran (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < ))    ⇒   ⊢ (𝜑 → dom 𝐺 ∈ 𝑆)
Theorem	smfsupdmmbl 46817*	If a countable set of sigma-measurable functions have domains in the sigma-algebra, then their supremum function has the domain in the sigma-algebra. This is the fourth statement of Proposition 121H of [Fremlin1] p. 39 . (Contributed by Glauco Siliprandi, 24-Jan-2025.)
⊢ Ⅎ𝑛𝜑    &   ⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝐹    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐹:𝑍⟶(SMblFn‘𝑆))    &   ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → dom (𝐹‘𝑛) ∈ 𝑆)    &   ⊢ 𝐷 = {𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛) ∣ ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 ((𝐹‘𝑛)‘𝑥) ≤ 𝑦}    &   ⊢ 𝐺 = (𝑥 ∈ 𝐷 ↦ sup(ran (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < ))    ⇒   ⊢ (𝜑 → dom 𝐺 ∈ 𝑆)
Theorem	finfdm 46818*	The domain of the inf function is defined in Proposition 121F (c) of [Fremlin1], p. 39. See smfinf 46790. Note that this definition of the inf function is quite general, as it does not require the original functions to be sigma-measurable, and it could be applied to uncountable sets of functions. The equality proved here is part of the proof of the fifth statement of Proposition 121H in [Fremlin1], p. 39. (Contributed by Glauco Siliprandi, 1-Feb-2025.)
⊢ Ⅎ𝑛𝜑    &   ⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑚𝜑    &   ⊢ Ⅎ𝑥𝐹    &   ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛):dom (𝐹‘𝑛)⟶ℝ*)    &   ⊢ 𝐷 = {𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛) ∣ ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)}    &   ⊢ 𝐻 = (𝑛 ∈ 𝑍 ↦ (𝑚 ∈ ℕ ↦ {𝑥 ∈ dom (𝐹‘𝑛) ∣ -𝑚 < ((𝐹‘𝑛)‘𝑥)}))    ⇒   ⊢ (𝜑 → 𝐷 = ∪ 𝑚 ∈ ℕ ∩ 𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚))
Theorem	finfdm2 46819*	The domain of the inf function is defined in Proposition 121F (c) of [Fremlin1], p. 39. See smfinf 46790. Note that this definition of the inf function is quite general, as it does not require the original functions to be sigma-measurable, and it could be applied to uncountable sets of functions. The equality proved here is part of the proof of the fifth statement of Proposition 121H in [Fremlin1], p. 39. (Contributed by Glauco Siliprandi, 1-Feb-2025.)
⊢ Ⅎ𝑛𝜑    &   ⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑚𝜑    &   ⊢ Ⅎ𝑥𝐹    &   ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐹‘𝑛):dom (𝐹‘𝑛)⟶ℝ*)    &   ⊢ 𝐷 = {𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛) ∣ ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)}    &   ⊢ 𝐺 = (𝑥 ∈ 𝐷 ↦ inf(ran (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < ))    &   ⊢ 𝐻 = (𝑛 ∈ 𝑍 ↦ (𝑚 ∈ ℕ ↦ {𝑥 ∈ dom (𝐹‘𝑛) ∣ -𝑚 < ((𝐹‘𝑛)‘𝑥)}))    ⇒   ⊢ (𝜑 → dom 𝐺 = ∪ 𝑚 ∈ ℕ ∩ 𝑛 ∈ 𝑍 ((𝐻‘𝑛)‘𝑚))
Theorem	smfinfdmmbllem 46820*	If a countable set of sigma-measurable functions have domains in the sigma-algebra, then their infimum function has the domain in the sigma-algebra. This is the fifth statement of Proposition 121H of [Fremlin1] p. 39 . (Contributed by Glauco Siliprandi, 1-Feb-2025.)
⊢ Ⅎ𝑛𝜑    &   ⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑚𝜑    &   ⊢ Ⅎ𝑥𝐹    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐹:𝑍⟶(SMblFn‘𝑆))    &   ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → dom (𝐹‘𝑛) ∈ 𝑆)    &   ⊢ 𝐷 = {𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛) ∣ ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)}    &   ⊢ 𝐺 = (𝑥 ∈ 𝐷 ↦ inf(ran (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < ))    &   ⊢ 𝐻 = (𝑛 ∈ 𝑍 ↦ (𝑚 ∈ ℕ ↦ {𝑥 ∈ dom (𝐹‘𝑛) ∣ -𝑚 < ((𝐹‘𝑛)‘𝑥)}))    ⇒   ⊢ (𝜑 → dom 𝐺 ∈ 𝑆)
Theorem	smfinfdmmbl 46821*	If a countable set of sigma-measurable functions have domains in the sigma-algebra, then their infimum function has the domain in the sigma-algebra. This is the fifth statement of Proposition 121H of [Fremlin1] p. 39 . (Contributed by Glauco Siliprandi, 1-Feb-2025.)
⊢ Ⅎ𝑛𝜑    &   ⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑥𝐹    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑆 ∈ SAlg)    &   ⊢ (𝜑 → 𝐹:𝑍⟶(SMblFn‘𝑆))    &   ⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → dom (𝐹‘𝑛) ∈ 𝑆)    &   ⊢ 𝐷 = {𝑥 ∈ ∩ 𝑛 ∈ 𝑍 dom (𝐹‘𝑛) ∣ ∃𝑦 ∈ ℝ ∀𝑛 ∈ 𝑍 𝑦 ≤ ((𝐹‘𝑛)‘𝑥)}    &   ⊢ 𝐺 = (𝑥 ∈ 𝐷 ↦ inf(ran (𝑛 ∈ 𝑍 ↦ ((𝐹‘𝑛)‘𝑥)), ℝ, < ))    ⇒   ⊢ (𝜑 → dom 𝐺 ∈ 𝑆)
21.44  Mathbox for Saveliy Skresanov
21.44.1  Ceva's theorem
Theorem	sigarval 46822*	Define the signed area by treating complex numbers as vectors with two components. (Contributed by Saveliy Skresanov, 19-Sep-2017.)
⊢ 𝐺 = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (ℑ‘((∗‘𝑥) · 𝑦)))    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴𝐺𝐵) = (ℑ‘((∗‘𝐴) · 𝐵)))
Theorem	sigarim 46823*	Signed area takes value in reals. (Contributed by Saveliy Skresanov, 19-Sep-2017.)
⊢ 𝐺 = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (ℑ‘((∗‘𝑥) · 𝑦)))    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴𝐺𝐵) ∈ ℝ)
Theorem	sigarac 46824*	Signed area is anticommutative. (Contributed by Saveliy Skresanov, 19-Sep-2017.)
⊢ 𝐺 = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (ℑ‘((∗‘𝑥) · 𝑦)))    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴𝐺𝐵) = -(𝐵𝐺𝐴))
Theorem	sigaraf 46825*	Signed area is additive by the first argument. (Contributed by Saveliy Skresanov, 19-Sep-2017.)
⊢ 𝐺 = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (ℑ‘((∗‘𝑥) · 𝑦)))    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐶)𝐺𝐵) = ((𝐴𝐺𝐵) + (𝐶𝐺𝐵)))
Theorem	sigarmf 46826*	Signed area is additive (with respect to subtraction) by the first argument. (Contributed by Saveliy Skresanov, 19-Sep-2017.)
⊢ 𝐺 = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (ℑ‘((∗‘𝑥) · 𝑦)))    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐶)𝐺𝐵) = ((𝐴𝐺𝐵) − (𝐶𝐺𝐵)))
Theorem	sigaras 46827*	Signed area is additive by the second argument. (Contributed by Saveliy Skresanov, 19-Sep-2017.)
⊢ 𝐺 = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (ℑ‘((∗‘𝑥) · 𝑦)))    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴𝐺(𝐵 + 𝐶)) = ((𝐴𝐺𝐵) + (𝐴𝐺𝐶)))
Theorem	sigarms 46828*	Signed area is additive (with respect to subtraction) by the second argument. (Contributed by Saveliy Skresanov, 19-Sep-2017.)
⊢ 𝐺 = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (ℑ‘((∗‘𝑥) · 𝑦)))    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴𝐺(𝐵 − 𝐶)) = ((𝐴𝐺𝐵) − (𝐴𝐺𝐶)))
Theorem	sigarls 46829*	Signed area is linear by the second argument. (Contributed by Saveliy Skresanov, 19-Sep-2017.)
⊢ 𝐺 = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (ℑ‘((∗‘𝑥) · 𝑦)))    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℝ) → (𝐴𝐺(𝐵 · 𝐶)) = ((𝐴𝐺𝐵) · 𝐶))
Theorem	sigarid 46830*	Signed area of a flat parallelogram is zero. (Contributed by Saveliy Skresanov, 20-Sep-2017.)
⊢ 𝐺 = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (ℑ‘((∗‘𝑥) · 𝑦)))    ⇒   ⊢ (𝐴 ∈ ℂ → (𝐴𝐺𝐴) = 0)
Theorem	sigarexp 46831*	Expand the signed area formula by linearity. (Contributed by Saveliy Skresanov, 20-Sep-2017.)
⊢ 𝐺 = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (ℑ‘((∗‘𝑥) · 𝑦)))    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐶)𝐺(𝐵 − 𝐶)) = (((𝐴𝐺𝐵) − (𝐴𝐺𝐶)) − (𝐶𝐺𝐵)))
Theorem	sigarperm 46832*	Signed area (𝐴 − 𝐶)𝐺(𝐵 − 𝐶) acts as a double area of a triangle 𝐴𝐵𝐶. Here we prove that cyclically permuting the vertices doesn't change the area. (Contributed by Saveliy Skresanov, 20-Sep-2017.)
⊢ 𝐺 = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (ℑ‘((∗‘𝑥) · 𝑦)))    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐶)𝐺(𝐵 − 𝐶)) = ((𝐵 − 𝐴)𝐺(𝐶 − 𝐴)))
Theorem	sigardiv 46833*	If signed area between vectors 𝐵 − 𝐴 and 𝐶 − 𝐴 is zero, then those vectors lie on the same line. (Contributed by Saveliy Skresanov, 22-Sep-2017.)
⊢ 𝐺 = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (ℑ‘((∗‘𝑥) · 𝑦)))    &   ⊢ (𝜑 → (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ))    &   ⊢ (𝜑 → ¬ 𝐶 = 𝐴)    &   ⊢ (𝜑 → ((𝐵 − 𝐴)𝐺(𝐶 − 𝐴)) = 0)    ⇒   ⊢ (𝜑 → ((𝐵 − 𝐴) / (𝐶 − 𝐴)) ∈ ℝ)
Theorem	sigarimcd 46834*	Signed area takes value in complex numbers. Deduction version. (Contributed by Saveliy Skresanov, 23-Sep-2017.)
⊢ 𝐺 = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (ℑ‘((∗‘𝑥) · 𝑦)))    &   ⊢ (𝜑 → (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ))    ⇒   ⊢ (𝜑 → (𝐴𝐺𝐵) ∈ ℂ)
Theorem	sigariz 46835*	If signed area is zero, the signed area with swapped arguments is also zero. Deduction version. (Contributed by Saveliy Skresanov, 23-Sep-2017.)
⊢ 𝐺 = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (ℑ‘((∗‘𝑥) · 𝑦)))    &   ⊢ (𝜑 → (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ))    &   ⊢ (𝜑 → (𝐴𝐺𝐵) = 0)    ⇒   ⊢ (𝜑 → (𝐵𝐺𝐴) = 0)
Theorem	sigarcol 46836*	Given three points 𝐴, 𝐵 and 𝐶 such that ¬ 𝐴 = 𝐵, the point 𝐶 lies on the line going through 𝐴 and 𝐵 iff the corresponding signed area is zero. That justifies the usage of signed area as a collinearity indicator. (Contributed by Saveliy Skresanov, 22-Sep-2017.)
⊢ 𝐺 = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (ℑ‘((∗‘𝑥) · 𝑦)))    &   ⊢ (𝜑 → (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ))    &   ⊢ (𝜑 → ¬ 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (((𝐴 − 𝐶)𝐺(𝐵 − 𝐶)) = 0 ↔ ∃𝑡 ∈ ℝ 𝐶 = (𝐵 + (𝑡 · (𝐴 − 𝐵)))))
Theorem	sharhght 46837*	Let 𝐴𝐵𝐶 be a triangle, and let 𝐷 lie on the line 𝐴𝐵. Then (doubled) areas of triangles 𝐴𝐷𝐶 and 𝐶𝐷𝐵 relate as lengths of corresponding bases 𝐴𝐷 and 𝐷𝐵. (Contributed by Saveliy Skresanov, 23-Sep-2017.)
⊢ 𝐺 = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (ℑ‘((∗‘𝑥) · 𝑦)))    &   ⊢ (𝜑 → (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ))    &   ⊢ (𝜑 → (𝐷 ∈ ℂ ∧ ((𝐴 − 𝐷)𝐺(𝐵 − 𝐷)) = 0))    ⇒   ⊢ (𝜑 → (((𝐶 − 𝐴)𝐺(𝐷 − 𝐴)) · (𝐵 − 𝐷)) = (((𝐶 − 𝐵)𝐺(𝐷 − 𝐵)) · (𝐴 − 𝐷)))
Theorem	sigaradd 46838*	Subtracting (double) area of 𝐴𝐷𝐶 from 𝐴𝐵𝐶 yields the (double) area of 𝐷𝐵𝐶. (Contributed by Saveliy Skresanov, 23-Sep-2017.)
⊢ 𝐺 = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (ℑ‘((∗‘𝑥) · 𝑦)))    &   ⊢ (𝜑 → (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ))    &   ⊢ (𝜑 → (𝐷 ∈ ℂ ∧ ((𝐴 − 𝐷)𝐺(𝐵 − 𝐷)) = 0))    ⇒   ⊢ (𝜑 → (((𝐵 − 𝐶)𝐺(𝐴 − 𝐶)) − ((𝐷 − 𝐶)𝐺(𝐴 − 𝐶))) = ((𝐵 − 𝐶)𝐺(𝐷 − 𝐶)))
Theorem	cevathlem1 46839	Ceva's theorem first lemma. Multiplies three identities and divides by the common factors. (Contributed by Saveliy Skresanov, 24-Sep-2017.)
⊢ (𝜑 → (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ))    &   ⊢ (𝜑 → (𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ ∧ 𝐹 ∈ ℂ))    &   ⊢ (𝜑 → (𝐺 ∈ ℂ ∧ 𝐻 ∈ ℂ ∧ 𝐾 ∈ ℂ))    &   ⊢ (𝜑 → (𝐴 ≠ 0 ∧ 𝐸 ≠ 0 ∧ 𝐶 ≠ 0))    &   ⊢ (𝜑 → ((𝐴 · 𝐵) = (𝐶 · 𝐷) ∧ (𝐸 · 𝐹) = (𝐴 · 𝐺) ∧ (𝐶 · 𝐻) = (𝐸 · 𝐾)))    ⇒   ⊢ (𝜑 → ((𝐵 · 𝐹) · 𝐻) = ((𝐷 · 𝐺) · 𝐾))
Theorem	cevathlem2 46840*	Ceva's theorem second lemma. Relate (doubled) areas of triangles 𝐶𝐴𝑂 and 𝐴𝐵𝑂 with of segments 𝐵𝐷 and 𝐷𝐶. (Contributed by Saveliy Skresanov, 24-Sep-2017.)
⊢ 𝐺 = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (ℑ‘((∗‘𝑥) · 𝑦)))    &   ⊢ (𝜑 → (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ))    &   ⊢ (𝜑 → (𝐹 ∈ ℂ ∧ 𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ))    &   ⊢ (𝜑 → 𝑂 ∈ ℂ)    &   ⊢ (𝜑 → (((𝐴 − 𝑂)𝐺(𝐷 − 𝑂)) = 0 ∧ ((𝐵 − 𝑂)𝐺(𝐸 − 𝑂)) = 0 ∧ ((𝐶 − 𝑂)𝐺(𝐹 − 𝑂)) = 0))    &   ⊢ (𝜑 → (((𝐴 − 𝐹)𝐺(𝐵 − 𝐹)) = 0 ∧ ((𝐵 − 𝐷)𝐺(𝐶 − 𝐷)) = 0 ∧ ((𝐶 − 𝐸)𝐺(𝐴 − 𝐸)) = 0))    &   ⊢ (𝜑 → (((𝐴 − 𝑂)𝐺(𝐵 − 𝑂)) ≠ 0 ∧ ((𝐵 − 𝑂)𝐺(𝐶 − 𝑂)) ≠ 0 ∧ ((𝐶 − 𝑂)𝐺(𝐴 − 𝑂)) ≠ 0))    ⇒   ⊢ (𝜑 → (((𝐶 − 𝑂)𝐺(𝐴 − 𝑂)) · (𝐵 − 𝐷)) = (((𝐴 − 𝑂)𝐺(𝐵 − 𝑂)) · (𝐷 − 𝐶)))
Theorem	cevath 46841*	Ceva's theorem. Let 𝐴𝐵𝐶 be a triangle and let points 𝐹, 𝐷 and 𝐸 lie on sides 𝐴𝐵, 𝐵𝐶, 𝐶𝐴 correspondingly. Suppose that cevians 𝐴𝐷, 𝐵𝐸 and 𝐶𝐹 intersect at one point 𝑂. Then triangle's sides are partitioned into segments and their lengths satisfy a certain identity. Here we obtain a bit stronger version by using complex numbers themselves instead of their absolute values. The proof goes by applying cevathlem2 46840 three times and then using cevathlem1 46839 to multiply obtained identities and prove the theorem. In the theorem statement we are using function 𝐺 as a collinearity indicator. For justification of that use, see sigarcol 46836. This is Metamath 100 proof #61. (Contributed by Saveliy Skresanov, 24-Sep-2017.)
⊢ 𝐺 = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (ℑ‘((∗‘𝑥) · 𝑦)))    &   ⊢ (𝜑 → (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ))    &   ⊢ (𝜑 → (𝐹 ∈ ℂ ∧ 𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ))    &   ⊢ (𝜑 → 𝑂 ∈ ℂ)    &   ⊢ (𝜑 → (((𝐴 − 𝑂)𝐺(𝐷 − 𝑂)) = 0 ∧ ((𝐵 − 𝑂)𝐺(𝐸 − 𝑂)) = 0 ∧ ((𝐶 − 𝑂)𝐺(𝐹 − 𝑂)) = 0))    &   ⊢ (𝜑 → (((𝐴 − 𝐹)𝐺(𝐵 − 𝐹)) = 0 ∧ ((𝐵 − 𝐷)𝐺(𝐶 − 𝐷)) = 0 ∧ ((𝐶 − 𝐸)𝐺(𝐴 − 𝐸)) = 0))    &   ⊢ (𝜑 → (((𝐴 − 𝑂)𝐺(𝐵 − 𝑂)) ≠ 0 ∧ ((𝐵 − 𝑂)𝐺(𝐶 − 𝑂)) ≠ 0 ∧ ((𝐶 − 𝑂)𝐺(𝐴 − 𝑂)) ≠ 0))    ⇒   ⊢ (𝜑 → (((𝐴 − 𝐹) · (𝐶 − 𝐸)) · (𝐵 − 𝐷)) = (((𝐹 − 𝐵) · (𝐸 − 𝐴)) · (𝐷 − 𝐶)))
21.44.2  Simple groups
Theorem	simpcntrab 46842	The center of a simple group is trivial or the group is abelian. (Contributed by SS, 3-Jan-2024.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ 𝑍 = (Cntr‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ SimpGrp)    ⇒   ⊢ (𝜑 → (𝑍 = { 0 } ∨ 𝐺 ∈ Abel))
21.45  Mathbox for Ender Ting
21.45.1  Increasing sequences and subsequences
Theorem	et-ltneverrefl 46843	Less-than class is never reflexive. (Contributed by Ender Ting, 22-Nov-2024.) Prefer to specify theorem domain and then apply ltnri 11352. (New usage is discouraged.)
⊢ ¬ 𝐴 < 𝐴
Theorem	et-equeucl 46844	Alternative proof that equality is left-Euclidean, using ax7 2014 directly instead of utility theorems; done for practice. (Contributed by Ender Ting, 21-Dec-2024.)
⊢ (𝑥 = 𝑧 → (𝑦 = 𝑧 → 𝑥 = 𝑦))
Theorem	et-sqrtnegnre 46845	The square root of a negative number is not a real number. (Contributed by Ender Ting, 5-Jan-2025.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 < 0) → ¬ (√‘𝐴) ∈ ℝ)
Theorem	ormklocald 46846*	If elements of a certain sequence are ordered with respect to a certain relation, then its consecutive elements satisfy that relation (so-called "local monotonicity"). (Contributed by Ender Ting, 30-Apr-2025.)
⊢ (𝜑 → 𝑅 Or 𝑆)    &   ⊢ (𝜑 → ∀𝑘 ∈ (0..^(𝑇 + 1))(𝐵‘𝑘) ∈ 𝑆)    &   ⊢ (𝜑 → ∀𝑘 ∈ (0..^𝑇)∀𝑡 ∈ (1..^(𝑇 + 1))(𝑘 < 𝑡 → (𝐵‘𝑘)𝑅(𝐵‘𝑡)))    ⇒   ⊢ (𝜑 → ∀𝑘 ∈ (0..^𝑇)(𝐵‘𝑘)𝑅(𝐵‘(𝑘 + 1)))
Theorem	ormkglobd 46847*	If all adjacent elements of a certain sequence are ordered according to a relation which is a total order on S, then any element is so related to anything to right of it (so-called "global monotonicity"). Deduction form. (Contributed by Ender Ting, 30-Apr-2025.)
⊢ (𝜑 → 𝑅 Or 𝑆)    &   ⊢ (𝜑 → ∀𝑘 ∈ (0..^(𝑇 + 1))(𝐵‘𝑘) ∈ 𝑆)    &   ⊢ (𝜑 → ∀𝑘 ∈ (0..^𝑇)(𝐵‘𝑘)𝑅(𝐵‘(𝑘 + 1)))    ⇒   ⊢ (𝜑 → ∀𝑘 ∈ (0..^𝑇)∀𝑡 ∈ (1..^(𝑇 + 1))(𝑘 < 𝑡 → (𝐵‘𝑘)𝑅(𝐵‘𝑡)))
Theorem	natlocalincr 46848*	Global monotonicity on half-open range implies local monotonicity. Inference form. (Contributed by Ender Ting, 22-Nov-2024.)
⊢ ∀𝑘 ∈ (0..^𝑇)∀𝑡 ∈ (1..^(𝑇 + 1))(𝑘 < 𝑡 → (𝐵‘𝑘) < (𝐵‘𝑡))    ⇒   ⊢ ∀𝑘 ∈ (0..^𝑇)(𝐵‘𝑘) < (𝐵‘(𝑘 + 1))
Theorem	natglobalincr 46849*	Local monotonicity on half-open integer range implies global monotonicity. Inference form. (Contributed by Ender Ting, 23-Nov-2024.)
⊢ ∀𝑘 ∈ (0..^𝑇)(𝐵‘𝑘) < (𝐵‘(𝑘 + 1))    &   ⊢ 𝑇 ∈ ℤ    ⇒   ⊢ ∀𝑘 ∈ (0..^𝑇)∀𝑡 ∈ ((𝑘 + 1)...𝑇)(𝐵‘𝑘) < (𝐵‘𝑡)
Syntax	cupword 46850	Extend class notation to include the set of strictly increasing sequences.
class UpWord 𝑆
Definition	df-upword 46851*	Strictly increasing sequence is a sequence, adjacent elements of which increase. (Contributed by Ender Ting, 19-Nov-2024.)
⊢ UpWord 𝑆 = {𝑤 ∣ (𝑤 ∈ Word 𝑆 ∧ ∀𝑘 ∈ (0..^((♯‘𝑤) − 1))(𝑤‘𝑘) < (𝑤‘(𝑘 + 1)))}
Theorem	upwordnul 46852	Empty set is an increasing sequence for every range. (Contributed by Ender Ting, 19-Nov-2024.)
⊢ ∅ ∈ UpWord 𝑆
Theorem	upwordisword 46853	Any increasing sequence is a sequence. (Contributed by Ender Ting, 19-Nov-2024.)
⊢ (𝐴 ∈ UpWord 𝑆 → 𝐴 ∈ Word 𝑆)
Theorem	singoutnword 46854	Singleton with character out of range 𝑉 is not a word for that range. (Contributed by Ender Ting, 21-Nov-2024.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (¬ 𝐴 ∈ 𝑉 → ¬ ⟨“𝐴”⟩ ∈ Word 𝑉)
Theorem	singoutnupword 46855	Singleton with character out of range 𝑆 is not an increasing sequence for that range. (Contributed by Ender Ting, 22-Nov-2024.)
⊢ 𝐴 ∈ V    ⇒   ⊢ (¬ 𝐴 ∈ 𝑆 → ¬ ⟨“𝐴”⟩ ∈ UpWord 𝑆)
Theorem	upwordsing 46856	Singleton is an increasing sequence for any compatible range. (Contributed by Ender Ting, 21-Nov-2024.)
⊢ 𝐴 ∈ 𝑆    ⇒   ⊢ ⟨“𝐴”⟩ ∈ UpWord 𝑆
Theorem	upwordsseti 46857	Strictly increasing sequences with a set given for range form a set. (Contributed by Ender Ting, 21-Nov-2024.)
⊢ 𝑆 ∈ V    ⇒   ⊢ UpWord 𝑆 ∈ V
Theorem	tworepnotupword 46858	Concatenation of identical singletons is never an increasing sequence. (Contributed by Ender Ting, 22-Nov-2024.)
⊢ 𝐴 ∈ V    ⇒   ⊢ ¬ (⟨“𝐴”⟩ ++ ⟨“𝐴”⟩) ∈ UpWord 𝑆
Theorem	upwrdfi 46859*	There is a finite number of strictly increasing sequences of a given length over finite alphabet. Trivially holds for invalid lengths where there're zero matching sequences. (Contributed by Ender Ting, 5-Jan-2024.)
⊢ (𝑆 ∈ Fin → {𝑎 ∈ UpWord 𝑆 ∣ (♯‘𝑎) = 𝑇} ∈ Fin)
21.45.2  Scratchpad for number theory
Theorem	evenwodadd 46860	If an integer is multiplied by its sum with an odd number (thus changing its parity), the result is even. (Contributed by Ender Ting, 30-Apr-2025.)
⊢ (𝜑 → 𝑖 ∈ ℤ)    &   ⊢ (𝜑 → 𝑗 ∈ ℤ)    &   ⊢ (𝜑 → ¬ 2 ∥ 𝑗)    ⇒   ⊢ (𝜑 → 2 ∥ (𝑖 · (𝑖 + 𝑗)))
21.45.3  Scratchpad for math on real numbers
Theorem	squeezedltsq 46861	If a real value is squeezed between two others, its square is less than square of at least one of them. Deduction form. (Contributed by Ender Ting, 31-Oct-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    &   ⊢ (𝜑 → 𝐵 < 𝐶)    ⇒   ⊢ (𝜑 → ((𝐵 · 𝐵) < (𝐴 · 𝐴) ∨ (𝐵 · 𝐵) < (𝐶 · 𝐶)))
21.46  Mathbox for Jarvin Udandy
Theorem	hirstL-ax3 46862	The third axiom of a system called "L" but proven to be a theorem since set.mm uses a different third axiom. This is named hirst after Holly P. Hirst and Jeffry L. Hirst. Axiom A3 of [Mendelson] p. 35. (Contributed by Jarvin Udandy, 7-Feb-2015.) (Proof modification is discouraged.)
⊢ ((¬ 𝜑 → ¬ 𝜓) → ((¬ 𝜑 → 𝜓) → 𝜑))
Theorem	ax3h 46863	Recover ax-3 8 from hirstL-ax3 46862. (Contributed by Jarvin Udandy, 3-Jul-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((¬ 𝜑 → ¬ 𝜓) → (𝜓 → 𝜑))
Theorem	aibandbiaiffaiffb 46864	A closed form showing (a implies b and b implies a) same-as (a same-as b). (Contributed by Jarvin Udandy, 3-Sep-2016.)
⊢ (((𝜑 → 𝜓) ∧ (𝜓 → 𝜑)) ↔ (𝜑 ↔ 𝜓))
Theorem	aibandbiaiaiffb 46865	A closed form showing (a implies b and b implies a) implies (a same-as b). (Contributed by Jarvin Udandy, 3-Sep-2016.)
⊢ (((𝜑 → 𝜓) ∧ (𝜓 → 𝜑)) → (𝜑 ↔ 𝜓))
Theorem	notatnand 46866	Do not use. Use intnanr instead. Given not a, there exists a proof for not (a and b). (Contributed by Jarvin Udandy, 31-Aug-2016.)
⊢ ¬ 𝜑    ⇒   ⊢ ¬ (𝜑 ∧ 𝜓)
Theorem	aistia 46867	Given a is equivalent to ⊤, there exists a proof for a. (Contributed by Jarvin Udandy, 30-Aug-2016.)
⊢ (𝜑 ↔ ⊤)    ⇒   ⊢ 𝜑
Theorem	aisfina 46868	Given a is equivalent to ⊥, there exists a proof for not a. (Contributed by Jarvin Udandy, 30-Aug-2016.)
⊢ (𝜑 ↔ ⊥)    ⇒   ⊢ ¬ 𝜑
Theorem	bothtbothsame 46869	Given both a, b are equivalent to ⊤, there exists a proof for a is the same as b. (Contributed by Jarvin Udandy, 31-Aug-2016.)
⊢ (𝜑 ↔ ⊤)    &   ⊢ (𝜓 ↔ ⊤)    ⇒   ⊢ (𝜑 ↔ 𝜓)
Theorem	bothfbothsame 46870	Given both a, b are equivalent to ⊥, there exists a proof for a is the same as b. (Contributed by Jarvin Udandy, 31-Aug-2016.)
⊢ (𝜑 ↔ ⊥)    &   ⊢ (𝜓 ↔ ⊥)    ⇒   ⊢ (𝜑 ↔ 𝜓)
Theorem	aiffbbtat 46871	Given a is equivalent to b, b is equivalent to ⊤ there exists a proof for a is equivalent to T. (Contributed by Jarvin Udandy, 29-Aug-2016.)
⊢ (𝜑 ↔ 𝜓)    &   ⊢ (𝜓 ↔ ⊤)    ⇒   ⊢ (𝜑 ↔ ⊤)
Theorem	aisbbisfaisf 46872	Given a is equivalent to b, b is equivalent to ⊥ there exists a proof for a is equivalent to F. (Contributed by Jarvin Udandy, 30-Aug-2016.)
⊢ (𝜑 ↔ 𝜓)    &   ⊢ (𝜓 ↔ ⊥)    ⇒   ⊢ (𝜑 ↔ ⊥)
Theorem	axorbtnotaiffb 46873	Given a is exclusive to b, there exists a proof for (not (a if-and-only-if b)); df-xor 1511 is a closed form of this. (Contributed by Jarvin Udandy, 7-Sep-2016.)
⊢ (𝜑 ⊻ 𝜓)    ⇒   ⊢ ¬ (𝜑 ↔ 𝜓)
Theorem	aiffnbandciffatnotciffb 46874	Given a is equivalent to (not b), c is equivalent to a, there exists a proof for ( not ( c iff b ) ). (Contributed by Jarvin Udandy, 7-Sep-2016.)
⊢ (𝜑 ↔ ¬ 𝜓)    &   ⊢ (𝜒 ↔ 𝜑)    ⇒   ⊢ ¬ (𝜒 ↔ 𝜓)
Theorem	axorbciffatcxorb 46875	Given a is equivalent to (not b), c is equivalent to a. there exists a proof for ( c xor b ). (Contributed by Jarvin Udandy, 7-Sep-2016.)
⊢ (𝜑 ⊻ 𝜓)    &   ⊢ (𝜒 ↔ 𝜑)    ⇒   ⊢ (𝜒 ⊻ 𝜓)
Theorem	aibnbna 46876	Given a implies b, (not b), there exists a proof for (not a). (Contributed by Jarvin Udandy, 1-Sep-2016.)
⊢ (𝜑 → 𝜓)    &   ⊢ ¬ 𝜓    ⇒   ⊢ ¬ 𝜑
Theorem	aibnbaif 46877	Given a implies b, not b, there exists a proof for a is F. (Contributed by Jarvin Udandy, 1-Sep-2016.)
⊢ (𝜑 → 𝜓)    &   ⊢ ¬ 𝜓    ⇒   ⊢ (𝜑 ↔ ⊥)
Theorem	aiffbtbat 46878	Given a is equivalent to b, T. is equivalent to b. there exists a proof for a is equivalent to T. (Contributed by Jarvin Udandy, 29-Aug-2016.)
⊢ (𝜑 ↔ 𝜓)    &   ⊢ (⊤ ↔ 𝜓)    ⇒   ⊢ (𝜑 ↔ ⊤)
Theorem	astbstanbst 46879	Given a is equivalent to T., also given that b is equivalent to T, there exists a proof for a and b is equivalent to T. (Contributed by Jarvin Udandy, 29-Aug-2016.)
⊢ (𝜑 ↔ ⊤)    &   ⊢ (𝜓 ↔ ⊤)    ⇒   ⊢ ((𝜑 ∧ 𝜓) ↔ ⊤)
Theorem	aistbistaandb 46880	Given a is equivalent to T., also given that b is equivalent to T, there exists a proof for (a and b). (Contributed by Jarvin Udandy, 9-Sep-2016.)
⊢ (𝜑 ↔ ⊤)    &   ⊢ (𝜓 ↔ ⊤)    ⇒   ⊢ (𝜑 ∧ 𝜓)
Theorem	aisbnaxb 46881	Given a is equivalent to b, there exists a proof for (not (a xor b)). (Contributed by Jarvin Udandy, 28-Aug-2016.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ ¬ (𝜑 ⊻ 𝜓)
Theorem	atbiffatnnb 46882	If a implies b, then a implies not not b. (Contributed by Jarvin Udandy, 28-Aug-2016.)
⊢ ((𝜑 → 𝜓) → (𝜑 → ¬ ¬ 𝜓))
Theorem	bisaiaisb 46883	Application of bicom1 with a, b swapped. (Contributed by Jarvin Udandy, 31-Aug-2016.)
⊢ ((𝜓 ↔ 𝜑) → (𝜑 ↔ 𝜓))
Theorem	atbiffatnnbalt 46884	If a implies b, then a implies not not b. (Contributed by Jarvin Udandy, 29-Aug-2016.)
⊢ ((𝜑 → 𝜓) → (𝜑 → ¬ ¬ 𝜓))
Theorem	abnotbtaxb 46885	Assuming a, not b, there exists a proof a-xor-b.) (Contributed by Jarvin Udandy, 31-Aug-2016.)
⊢ 𝜑    &   ⊢ ¬ 𝜓    ⇒   ⊢ (𝜑 ⊻ 𝜓)
Theorem	abnotataxb 46886	Assuming not a, b, there exists a proof a-xor-b.) (Contributed by Jarvin Udandy, 31-Aug-2016.)
⊢ ¬ 𝜑    &   ⊢ 𝜓    ⇒   ⊢ (𝜑 ⊻ 𝜓)
Theorem	conimpf 46887	Assuming a, not b, and a implies b, there exists a proof that a is false.) (Contributed by Jarvin Udandy, 28-Aug-2016.)
⊢ 𝜑    &   ⊢ ¬ 𝜓    &   ⊢ (𝜑 → 𝜓)    ⇒   ⊢ (𝜑 ↔ ⊥)
Theorem	conimpfalt 46888	Assuming a, not b, and a implies b, there exists a proof that a is false.) (Contributed by Jarvin Udandy, 29-Aug-2016.)
⊢ 𝜑    &   ⊢ ¬ 𝜓    &   ⊢ (𝜑 → 𝜓)    ⇒   ⊢ (𝜑 ↔ ⊥)
Theorem	aistbisfiaxb 46889	Given a is equivalent to T., Given b is equivalent to F. there exists a proof for a-xor-b. (Contributed by Jarvin Udandy, 31-Aug-2016.)
⊢ (𝜑 ↔ ⊤)    &   ⊢ (𝜓 ↔ ⊥)    ⇒   ⊢ (𝜑 ⊻ 𝜓)
Theorem	aisfbistiaxb 46890	Given a is equivalent to F., Given b is equivalent to T., there exists a proof for a-xor-b. (Contributed by Jarvin Udandy, 31-Aug-2016.)
⊢ (𝜑 ↔ ⊥)    &   ⊢ (𝜓 ↔ ⊤)    ⇒   ⊢ (𝜑 ⊻ 𝜓)
Theorem	aifftbifffaibif 46891	Given a is equivalent to T., Given b is equivalent to F., there exists a proof for that a implies b is false. (Contributed by Jarvin Udandy, 7-Sep-2020.)
⊢ (𝜑 ↔ ⊤)    &   ⊢ (𝜓 ↔ ⊥)    ⇒   ⊢ ((𝜑 → 𝜓) ↔ ⊥)
Theorem	aifftbifffaibifff 46892	Given a is equivalent to T., Given b is equivalent to F., there exists a proof for that a iff b is false. (Contributed by Jarvin Udandy, 7-Sep-2020.)
⊢ (𝜑 ↔ ⊤)    &   ⊢ (𝜓 ↔ ⊥)    ⇒   ⊢ ((𝜑 ↔ 𝜓) ↔ ⊥)
Theorem	atnaiana 46893	Given a, it is not the case a implies a self contradiction. (Contributed by Jarvin Udandy, 7-Sep-2020.)
⊢ 𝜑    ⇒   ⊢ ¬ (𝜑 → (𝜑 ∧ ¬ 𝜑))
Theorem	ainaiaandna 46894	Given a, a implies it is not the case a implies a self contradiction. (Contributed by Jarvin Udandy, 7-Sep-2020.)
⊢ 𝜑    ⇒   ⊢ (𝜑 → ¬ (𝜑 → (𝜑 ∧ ¬ 𝜑)))
Theorem	abcdta 46895	Given (((a and b) and c) and d), there exists a proof for a. (Contributed by Jarvin Udandy, 3-Sep-2016.)
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃)    ⇒   ⊢ 𝜑
Theorem	abcdtb 46896	Given (((a and b) and c) and d), there exists a proof for b. (Contributed by Jarvin Udandy, 3-Sep-2016.)
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃)    ⇒   ⊢ 𝜓
Theorem	abcdtc 46897	Given (((a and b) and c) and d), there exists a proof for c. (Contributed by Jarvin Udandy, 3-Sep-2016.)
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃)    ⇒   ⊢ 𝜒
Theorem	abcdtd 46898	Given (((a and b) and c) and d), there exists a proof for d. (Contributed by Jarvin Udandy, 3-Sep-2016.)
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃)    ⇒   ⊢ 𝜃
Theorem	abciffcbatnabciffncba 46899	Operands in a biconditional expression converted negated. Additionally biconditional converted to show antecedent implies sequent. Closed form. (Contributed by Jarvin Udandy, 7-Sep-2020.)
⊢ (¬ ((𝜑 ∧ 𝜓) ∧ 𝜒) → ¬ ((𝜒 ∧ 𝜓) ∧ 𝜑))
Theorem	abciffcbatnabciffncbai 46900	Operands in a biconditional expression converted negated. Additionally biconditional converted to show antecedent implies sequent. (Contributed by Jarvin Udandy, 7-Sep-2020.)
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ ((𝜒 ∧ 𝜓) ∧ 𝜑))    ⇒   ⊢ (¬ ((𝜑 ∧ 𝜓) ∧ 𝜒) → ¬ ((𝜒 ∧ 𝜓) ∧ 𝜑))