P. 479 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 47801-47900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	finfdm2 47801*	The domain of the inf function is defined in Proposition 121F (c) of [Fremlin1], p. 39. See smfinf 47772. 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 47802*	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 47803*	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.46  Mathbox for Saveliy Skresanov
21.46.1  Ceva's theorem
Theorem	sigarval 47804*	Define the signed area by treating complex numbers as vectors with two components. (Contributed by Saveliy Skresanov, 19-Sep-2017.)
⊢ 𝐺 = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (ℑ‘((∗‘𝑥) · 𝑦)))    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴𝐺𝐵) = (ℑ‘((∗‘𝐴) · 𝐵)))
Theorem	sigarim 47805*	Signed area takes value in reals. (Contributed by Saveliy Skresanov, 19-Sep-2017.)
⊢ 𝐺 = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (ℑ‘((∗‘𝑥) · 𝑦)))    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴𝐺𝐵) ∈ ℝ)
Theorem	sigarac 47806*	Signed area is anticommutative. (Contributed by Saveliy Skresanov, 19-Sep-2017.)
⊢ 𝐺 = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (ℑ‘((∗‘𝑥) · 𝑦)))    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴𝐺𝐵) = -(𝐵𝐺𝐴))
Theorem	sigaraf 47807*	Signed area is additive by the first argument. (Contributed by Saveliy Skresanov, 19-Sep-2017.)
⊢ 𝐺 = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (ℑ‘((∗‘𝑥) · 𝑦)))    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐶)𝐺𝐵) = ((𝐴𝐺𝐵) + (𝐶𝐺𝐵)))
Theorem	sigarmf 47808*	Signed area is additive (with respect to subtraction) by the first argument. (Contributed by Saveliy Skresanov, 19-Sep-2017.)
⊢ 𝐺 = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (ℑ‘((∗‘𝑥) · 𝑦)))    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐶)𝐺𝐵) = ((𝐴𝐺𝐵) − (𝐶𝐺𝐵)))
Theorem	sigaras 47809*	Signed area is additive by the second argument. (Contributed by Saveliy Skresanov, 19-Sep-2017.)
⊢ 𝐺 = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (ℑ‘((∗‘𝑥) · 𝑦)))    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴𝐺(𝐵 + 𝐶)) = ((𝐴𝐺𝐵) + (𝐴𝐺𝐶)))
Theorem	sigarms 47810*	Signed area is additive (with respect to subtraction) by the second argument. (Contributed by Saveliy Skresanov, 19-Sep-2017.)
⊢ 𝐺 = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (ℑ‘((∗‘𝑥) · 𝑦)))    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴𝐺(𝐵 − 𝐶)) = ((𝐴𝐺𝐵) − (𝐴𝐺𝐶)))
Theorem	sigarls 47811*	Signed area is linear by the second argument. (Contributed by Saveliy Skresanov, 19-Sep-2017.)
⊢ 𝐺 = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (ℑ‘((∗‘𝑥) · 𝑦)))    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℝ) → (𝐴𝐺(𝐵 · 𝐶)) = ((𝐴𝐺𝐵) · 𝐶))
Theorem	sigarid 47812*	Signed area of a flat parallelogram is zero. (Contributed by Saveliy Skresanov, 20-Sep-2017.)
⊢ 𝐺 = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (ℑ‘((∗‘𝑥) · 𝑦)))    ⇒   ⊢ (𝐴 ∈ ℂ → (𝐴𝐺𝐴) = 0)
Theorem	sigarexp 47813*	Expand the signed area formula by linearity. (Contributed by Saveliy Skresanov, 20-Sep-2017.)
⊢ 𝐺 = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (ℑ‘((∗‘𝑥) · 𝑦)))    ⇒   ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 − 𝐶)𝐺(𝐵 − 𝐶)) = (((𝐴𝐺𝐵) − (𝐴𝐺𝐶)) − (𝐶𝐺𝐵)))
Theorem	sigarperm 47814*	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 47815*	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 47816*	Signed area takes value in complex numbers. Deduction version. (Contributed by Saveliy Skresanov, 23-Sep-2017.)
⊢ 𝐺 = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (ℑ‘((∗‘𝑥) · 𝑦)))    &   ⊢ (𝜑 → (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ))    ⇒   ⊢ (𝜑 → (𝐴𝐺𝐵) ∈ ℂ)
Theorem	sigariz 47817*	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 47818*	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 47819*	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 47820*	Subtracting (double) area of 𝐴𝐷𝐶 from 𝐴𝐵𝐶 yields the (double) area of 𝐷𝐵𝐶. (Contributed by Saveliy Skresanov, 23-Sep-2017.)
⊢ 𝐺 = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (ℑ‘((∗‘𝑥) · 𝑦)))    &   ⊢ (𝜑 → (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ))    &   ⊢ (𝜑 → (𝐷 ∈ ℂ ∧ ((𝐴 − 𝐷)𝐺(𝐵 − 𝐷)) = 0))    ⇒   ⊢ (𝜑 → (((𝐵 − 𝐶)𝐺(𝐴 − 𝐶)) − ((𝐷 − 𝐶)𝐺(𝐴 − 𝐶))) = ((𝐵 − 𝐶)𝐺(𝐷 − 𝐶)))
Theorem	cevathlem1 47821	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 47822*	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 47823*	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 47822 three times and then using cevathlem1 47821 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 47818. This is Metamath 100 proof #61. (Contributed by Saveliy Skresanov, 24-Sep-2017.)
⊢ 𝐺 = (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (ℑ‘((∗‘𝑥) · 𝑦)))    &   ⊢ (𝜑 → (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ))    &   ⊢ (𝜑 → (𝐹 ∈ ℂ ∧ 𝐷 ∈ ℂ ∧ 𝐸 ∈ ℂ))    &   ⊢ (𝜑 → 𝑂 ∈ ℂ)    &   ⊢ (𝜑 → (((𝐴 − 𝑂)𝐺(𝐷 − 𝑂)) = 0 ∧ ((𝐵 − 𝑂)𝐺(𝐸 − 𝑂)) = 0 ∧ ((𝐶 − 𝑂)𝐺(𝐹 − 𝑂)) = 0))    &   ⊢ (𝜑 → (((𝐴 − 𝐹)𝐺(𝐵 − 𝐹)) = 0 ∧ ((𝐵 − 𝐷)𝐺(𝐶 − 𝐷)) = 0 ∧ ((𝐶 − 𝐸)𝐺(𝐴 − 𝐸)) = 0))    &   ⊢ (𝜑 → (((𝐴 − 𝑂)𝐺(𝐵 − 𝑂)) ≠ 0 ∧ ((𝐵 − 𝑂)𝐺(𝐶 − 𝑂)) ≠ 0 ∧ ((𝐶 − 𝑂)𝐺(𝐴 − 𝑂)) ≠ 0))    ⇒   ⊢ (𝜑 → (((𝐴 − 𝐹) · (𝐶 − 𝐸)) · (𝐵 − 𝐷)) = (((𝐹 − 𝐵) · (𝐸 − 𝐴)) · (𝐷 − 𝐶)))
21.46.2  Simple groups
Theorem	simpcntrab 47824	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.47  Mathbox for Ender Ting
21.47.1  Interesting facts
Theorem	et-ltneverrefl 47825	Less-than class is never reflexive. (Contributed by Ender Ting, 22-Nov-2024.) Prefer to specify theorem domain and then apply ltnri 11400. (New usage is discouraged.)
⊢ ¬ 𝐴 < 𝐴
Theorem	et-equeucl 47826	Alternative proof that equality is left-Euclidean, using ax7 2049 directly instead of utility theorems; done for practice. (Contributed by Ender Ting, 21-Dec-2024.)
⊢ (𝑥 = 𝑧 → (𝑦 = 𝑧 → 𝑥 = 𝑦))
Theorem	et-sqrtnegnre 47827	The square root of a negative number is not a real number. (Contributed by Ender Ting, 5-Jan-2025.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 < 0) → ¬ (√‘𝐴) ∈ ℝ)
Theorem	quantgodel 47828	There can be no formula asserting its own non-universality, in parallel to bj-babygodel 37443; proof path is shorter but relying on a property of specialization which provability predicates do not have. For a matching proof, see quantgodelALT 47829. (Contributed by Ender Ting, 9-May-2026.)
⊢ (𝜑 ↔ ¬ ∀𝑥𝜑)    ⇒   ⊢ ⊥
Theorem	quantgodelALT 47829	There can be no formula asserting its own non-universality; follows the steps of bj-babygodel 37443. (Contributed by Ender Ting, 7-May-2026.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (𝜑 ↔ ¬ ∀𝑥𝜑)    ⇒   ⊢ ⊥
21.47.2  Increasing sequences and subsequences
Theorem	ormklocald 47830*	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 47831*	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	chnsubseqword 47832	A subsequence of a chain is a word. (Contributed by Ender Ting, 22-Jan-2026.)
⊢ (𝜑 → 𝑊 ∈ ( < Chain 𝐴))    &   ⊢ (𝜑 → 𝐼 ∈ ( < Chain (0..^(♯‘𝑊))))    ⇒   ⊢ (𝜑 → (𝑊 ∘ 𝐼) ∈ Word 𝐴)
Theorem	chnsubseqwl 47833	A subsequence of a chain has the same length as its indexing sequence. (Contributed by Ender Ting, 22-Jan-2026.)
⊢ (𝜑 → 𝑊 ∈ ( < Chain 𝐴))    &   ⊢ (𝜑 → 𝐼 ∈ ( < Chain (0..^(♯‘𝑊))))    ⇒   ⊢ (𝜑 → (♯‘(𝑊 ∘ 𝐼)) = (♯‘𝐼))
Theorem	chnsubseq 47834	An order-preserving subsequence of an ordered chain is itself a chain. (Contributed by Ender Ting, 22-Jan-2026.)
⊢ (𝜑 → 𝑊 ∈ ( < Chain 𝐴))    &   ⊢ (𝜑 → 𝐼 ∈ ( < Chain (0..^(♯‘𝑊))))    &   ⊢ (𝜑 → < Po 𝐴)    ⇒   ⊢ (𝜑 → (𝑊 ∘ 𝐼) ∈ ( < Chain 𝐴))
Theorem	chnsuslle 47835	Length of a subsequence is bounded by the length of original chain. (Contributed by Ender Ting, 30-Jan-2026.)
⊢ (𝜑 → 𝑊 ∈ ( < Chain 𝐴))    &   ⊢ (𝜑 → 𝐼 ∈ ( < Chain (0..^(♯‘𝑊))))    &   ⊢ (𝜑 → < Po 𝐴)    ⇒   ⊢ (𝜑 → (♯‘(𝑊 ∘ 𝐼)) ≤ (♯‘𝑊))
Theorem	chnerlem1 47836	In a chain constructed on an equivalence relation, the last element is equivalent to any. This theorem is a translation of chnub 18776 to equivalence relations. (Contributed by Ender Ting, 29-Jan-2026.)
⊢ (𝜑 → ∼ Er 𝐴)    &   ⊢ (𝜑 → 𝐶 ∈ ( ∼ Chain 𝐴))    &   ⊢ (𝜑 → 𝐽 ∈ (0..^(♯‘𝐶)))    ⇒   ⊢ (𝜑 → (𝐶‘𝐽) ∼ (lastS‘𝐶))
Theorem	chnerlem2 47837	Lemma for chner 47839 where the I-th element comes before the J-th. (Contributed by Ender Ting, 29-Jan-2026.)
⊢ (𝜑 → ∼ Er 𝐴)    &   ⊢ (𝜑 → 𝐶 ∈ ( ∼ Chain 𝐴))    &   ⊢ (𝜑 → 𝐽 ∈ (0..^(♯‘𝐶)))    ⇒   ⊢ ((𝜑 ∧ 𝐼 ∈ (0..^𝐽)) → (𝐶‘𝐼) ∼ (𝐶‘𝐽))
Theorem	chnerlem3 47838	Lemma for chner 47839- trichotomy of integers within the word's domain. (Contributed by Ender Ting, 29-Jan-2026.)
⊢ (𝜑 → ∼ Er 𝐴)    &   ⊢ (𝜑 → 𝐶 ∈ ( ∼ Chain 𝐴))    &   ⊢ (𝜑 → 𝐽 ∈ (0..^(♯‘𝐶)))    &   ⊢ (𝜑 → 𝐼 ∈ (0..^(♯‘𝐶)))    ⇒   ⊢ (𝜑 → (𝐼 ∈ (0..^𝐽) ∨ 𝐽 ∈ (0..^𝐼) ∨ 𝐼 = 𝐽))
Theorem	chner 47839	Any two elements are equivalent in a chain constructed on an equivalence relation. (Contributed by Ender Ting, 29-Jan-2026.)
⊢ (𝜑 → ∼ Er 𝐴)    &   ⊢ (𝜑 → 𝐶 ∈ ( ∼ Chain 𝐴))    &   ⊢ (𝜑 → 𝐽 ∈ (0..^(♯‘𝐶)))    &   ⊢ (𝜑 → 𝐼 ∈ (0..^(♯‘𝐶)))    ⇒   ⊢ (𝜑 → (𝐶‘𝐼) ∼ (𝐶‘𝐽))
Theorem	wrddin 47840	A word in two alphabets is also a word under their intersection. (Contributed by Ender Ting, 24-Jul-2026.)
⊢ ((𝐴 ∈ Word 𝐵 ∧ 𝐴 ∈ Word 𝐶) → 𝐴 ∈ Word (𝐵 ∩ 𝐶))
Theorem	wrddrin 47841	A word whose alphabet is intersection of two classes is also a word in each of those alphabets. (Contributed by Ender Ting, 24-Jul-2026.)
⊢ (𝐴 ∈ Word (𝐵 ∩ 𝐶) → (𝐴 ∈ Word 𝐵 ∧ 𝐴 ∈ Word 𝐶))
Theorem	wrddin2 47842	Distribution of word class constructor over class intersection. (Contributed by Ender Ting, 24-Jul-2026.)
⊢ Word (𝐵 ∩ 𝐶) = (Word 𝐵 ∩ Word 𝐶)
Theorem	wrddun 47843	Words in either of two alphabets are words in their union. (Contributed by Ender Ting, 24-Jul-2026.)
⊢ ((𝐴 ∈ Word 𝐵 ∨ 𝐴 ∈ Word 𝐶) → 𝐴 ∈ Word (𝐵 ∪ 𝐶))
Theorem	wrddun2 47844	Superadditivity of word constructor. Class of words over union alphabet includes all words over either alphabet in the union; if 𝐵 and 𝐶 are non-empty and different, then this subclass relation is strict because of the words which have symbols both from 𝐵 and from 𝐶. (Contributed by Ender Ting, 24-Jul-2026.)
⊢ (Word 𝐵 ∪ Word 𝐶) ⊆ Word (𝐵 ∪ 𝐶)
Theorem	chndin 47845	A chain in two alphabets at once is also a chain in their intersection. (Contributed by Ender Ting, 24-Jul-2026.)
⊢ ((𝐴 ∈ (𝑅 Chain 𝐵) ∧ 𝐴 ∈ (𝑅 Chain 𝐶)) → 𝐴 ∈ (𝑅 Chain (𝐵 ∩ 𝐶)))
Theorem	chndrin 47846	A chain whose alphabet is intersection of two classes is also a chain in each of those alphabets. (Contributed by Ender Ting, 24-Jul-2026.)
⊢ (𝐴 ∈ (𝑅 Chain (𝐵 ∩ 𝐶)) → (𝐴 ∈ (𝑅 Chain 𝐵) ∧ 𝐴 ∈ (𝑅 Chain 𝐶)))
Theorem	chndin2 47847	Distribution of chain class constructor over alphabet intersection. (Contributed by Ender Ting, 24-Jul-2026.)
⊢ (𝑅 Chain (𝐵 ∩ 𝐶)) = ((𝑅 Chain 𝐵) ∩ (𝑅 Chain 𝐶))
Theorem	chndun 47848	Chains in either of two alphabets are chains in their union. (Contributed by Ender Ting, 24-Jul-2026.)
⊢ ((𝐴 ∈ (𝑅 Chain 𝐵) ∨ 𝐴 ∈ (𝑅 Chain 𝐶)) → 𝐴 ∈ (𝑅 Chain (𝐵 ∪ 𝐶)))
Theorem	chndun2 47849	Superaddivity of chain constructor over alphabet parameter. (Contributed by Ender Ting, 24-Jul-2026.)
⊢ ((𝑅 Chain 𝐵) ∪ (𝑅 Chain 𝐶)) ⊆ (𝑅 Chain (𝐵 ∪ 𝐶))
Theorem	chnrin 47850	Satisfying two chain relations makes a chain under their intersection. (Contributed by Ender Ting, 24-Jul-2026.)
⊢ ((𝐴 ∈ (𝑅 Chain 𝐵) ∧ 𝐴 ∈ ( < Chain 𝐵)) → 𝐴 ∈ ((𝑅 ∩ < ) Chain 𝐵))
Theorem	chnrrin 47851	A chain of elements satisfying two relations at once is a chain under either of them. (Contributed by Ender Ting, 24-Jul-2026.)
⊢ (𝐴 ∈ ((𝑅 ∩ < ) Chain 𝐵) → (𝐴 ∈ (𝑅 Chain 𝐵) ∧ 𝐴 ∈ ( < Chain 𝐵)))
Theorem	chnrin2 47852	Distribution of chain class constructor over relation intersection. (Contributed by Ender Ting, 24-Jul-2026.)
⊢ ((𝑅 ∩ < ) Chain 𝐵) = ((𝑅 Chain 𝐵) ∩ ( < Chain 𝐵))
Theorem	chnrun 47853	Satisfying either of two chain relations is sufficient to make a chain under their union. (Contributed by Ender Ting, 24-Jul-2026.)
⊢ ((𝐴 ∈ (𝑅 Chain 𝐵) ∨ 𝐴 ∈ ( < Chain 𝐵)) → 𝐴 ∈ ((𝑅 ∪ < ) Chain 𝐵))
Theorem	chnrun2 47854	Superadditivity of chain constructor over relation parameter. (Contributed by Ender Ting, 24-Jul-2026.)
⊢ ((𝑅 Chain 𝐵) ∪ ( < Chain 𝐵)) ⊆ ((𝑅 ∪ < ) Chain 𝐵)
21.47.3  Scratchpad for number theory
Theorem	evenwodadd 47855	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.47.4  Scratchpad for math on real numbers
Theorem	squeezedltsq 47856	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.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    &   ⊢ (𝜑 → 𝐵 < 𝐶)    ⇒   ⊢ (𝜑 → ((𝐵 · 𝐵) < (𝐴 · 𝐴) ∨ (𝐵 · 𝐵) < (𝐶 · 𝐶)))
Theorem	sqrtnnaa 47857	Square root of a natural number is algebraic. (Contributed by Ender Ting, 21-Jul-2026.)
⊢ (𝐴 ∈ ℕ → (√‘𝐴) ∈ 𝔸)
Theorem	sqrtnzqaa 47858	Square root of a nonzero rational is algebraic. (Contributed by Ender Ting, 22-Jul-2026.)
⊢ ((𝐴 ∈ ℚ ∧ 𝐴 ≠ 0) → (√‘𝐴) ∈ 𝔸)
Theorem	sqrtqaa 47859	Square root of a rational number is algebraic. (Contributed by Ender Ting, 22-Jul-2026.)
⊢ (𝐴 ∈ ℚ → (√‘𝐴) ∈ 𝔸)
Theorem	numtowerdt 47860	Certain number sets and fields form a tower. In particular, singleton 1, natural numbers, natural numbers with zero, integers, rationals, algebraic reals (notice that current definition allows algebraic numbers to be complex thus the restriction), reals and complex number sets are a tower of proper subsets. (Contributed by Ender Ting, 31-Jul-2026.)
⊢ ⟨“{1}ℕℕ0ℤℚ(𝔸 ∩ ℝ)ℝℂ”⟩ ∈ ( [⊊] Chain V)
Theorem	sin3t 47861	Triple-angle formula for sine, in pure sine form. (Contributed by Ender Ting, 16-Mar-2026.)
⊢ (𝐴 ∈ ℂ → (sin‘(3 · 𝐴)) = ((3 · (sin‘𝐴)) − (4 · ((sin‘𝐴)↑3))))
Theorem	cos3t 47862	Triple-angle formula for cosine, in pure cosine form. (Contributed by Ender Ting, 16-Mar-2026.)
⊢ (𝐴 ∈ ℂ → (cos‘(3 · 𝐴)) = ((4 · ((cos‘𝐴)↑3)) − (3 · (cos‘𝐴))))
Theorem	sin5tlem1 47863	Lemma 1 for quintupled angle sine calculation, expanding triple-angle sine times double-angle cosine. (Contributed by Ender Ting, 16-Mar-2026.)
⊢ (𝑁 ∈ ℂ → (((3 · 𝑁) − (4 · (𝑁↑3))) · (1 − (2 · (𝑁↑2)))) = (((8 · (𝑁↑5)) − (;10 · (𝑁↑3))) + (3 · 𝑁)))
Theorem	sin5tlem2 47864	Lemma 2 for quintupled angle sine calculation, multiplicating triple angle cosine by cosine straight and converting into sine. (Contributed by Ender Ting, 16-Apr-2026.)
⊢ ((𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ (𝑁↑2) = (1 − (𝑀↑2))) → (((4 · (𝑁↑3)) − (3 · 𝑁)) · 𝑁) = ((4 · ((1 − (2 · (𝑀↑2))) + (𝑀↑4))) − (3 · (1 − (𝑀↑2)))))
Theorem	sin5tlem3 47865	Lemma 3 for quintupled angle sine calculation, multiplicating triple angle cosine by double angle sine. (Contributed by Ender Ting, 16-Apr-2026.)
⊢ ((𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ (𝑁↑2) = (1 − (𝑀↑2))) → (((4 · (𝑁↑3)) − (3 · 𝑁)) · (2 · (𝑀 · 𝑁))) = (((4 · ((1 − (2 · (𝑀↑2))) + (𝑀↑4))) − (3 · (1 − (𝑀↑2)))) · (2 · 𝑀)))
Theorem	sin5tlem4 47866	Lemma 4 for quintupled angle sine calculation: expanding lemma 3 result to difference of polynomials. (Contributed by Ender Ting, 17-Apr-2026.)
⊢ ((𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ (𝑁↑2) = (1 − (𝑀↑2))) → (((4 · (𝑁↑3)) − (3 · 𝑁)) · (2 · (𝑀 · 𝑁))) = ((((8 · (𝑀↑5)) − (;16 · (𝑀↑3))) + (8 · 𝑀)) − ((6 · 𝑀) − (6 · (𝑀↑3)))))
Theorem	sin5tlem5 47867	Lemma 5 for quintupled angle sine calculation: sine of triple-angle and double-angle sum, as a polynomial in sine straight. (Contributed by Ender Ting, 17-Apr-2026.)
⊢ ((𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ (𝑁↑2) = (1 − (𝑀↑2))) → ((((3 · 𝑀) − (4 · (𝑀↑3))) · (1 − (2 · (𝑀↑2)))) + (((4 · (𝑁↑3)) − (3 · 𝑁)) · (2 · (𝑀 · 𝑁)))) = (((;16 · (𝑀↑5)) − (;20 · (𝑀↑3))) + (5 · 𝑀)))
Theorem	sin5t 47868	Five-times-angle formula for sine, in pure sine form. (Contributed by Ender Ting, 17-Apr-2026.)
⊢ (𝐴 ∈ ℂ → (sin‘(5 · 𝐴)) = (((;16 · ((sin‘𝐴)↑5)) − (;20 · ((sin‘𝐴)↑3))) + (5 · (sin‘𝐴))))
Theorem	cos5t 47869	Five-times-angle formula for cosine, in pure cosine form. (Contributed by Ender Ting, 20-Apr-2026.)
⊢ (𝐴 ∈ ℂ → (cos‘(5 · 𝐴)) = (((;16 · ((cos‘𝐴)↑5)) − (;20 · ((cos‘𝐴)↑3))) + (5 · (cos‘𝐴))))
Theorem	cos5teq 47870	Five-times-angle formula for cosine, substitution helper. (Contributed by Ender Ting, 9-May-2026.)
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 = (5 · 𝐴) ∧ 𝐶 = (cos‘𝐴)) → (cos‘𝐵) = (((;16 · (𝐶↑5)) − (;20 · (𝐶↑3))) + (5 · 𝐶)))
Theorem	goldpolyfactor 47871	Factorization of a polynomial which has golden ratio among its roots, done by term-by-term-by-term multiplying and summing a few shorter polynomials. (Contributed by Ender Ting, 24-Jul-2026.)
⊢ 𝐹 ∈ ℂ    ⇒   ⊢ (((((𝐹↑2) − 𝐹) − 1) · (((𝐹↑2) − 𝐹) − 1)) · (𝐹 + 2)) = ((((𝐹↑5) − (5 · (𝐹↑3))) + (5 · 𝐹)) + 2)
Theorem	goldrarr 47872	The golden ratio is a real value. (Contributed by Ender Ting, 15-Mar-2026.)
⊢ 𝐹 = (2 · (cos‘(π / 5)))    ⇒   ⊢ 𝐹 ∈ ℝ
Theorem	goldrasin 47873	Alternative trigonometric formula for the golden ratio. (Contributed by Ender Ting, 15-Mar-2026.)
⊢ 𝐹 = (2 · (cos‘(π / 5)))    ⇒   ⊢ 𝐹 = (2 · (sin‘(π · (3 / ;10))))
Theorem	goldrapos 47874	Golden ratio is positive. (Contributed by Ender Ting, 16-Apr-2026.)
⊢ 𝐹 = (2 · (cos‘(π / 5)))    ⇒   ⊢ 0 < 𝐹
Theorem	goldrarp 47875	The golden ratio is a positive real. (Contributed by Ender Ting, 16-Apr-2026.)
⊢ 𝐹 = (2 · (cos‘(π / 5)))    ⇒   ⊢ 𝐹 ∈ ℝ+
Theorem	goldracos5teq 47876	Lemma 1 for determining the value of golden ratio. (Contributed by Ender Ting, 9-May-2026.)
⊢ 𝐹 = (2 · (cos‘(π / 5)))    ⇒   ⊢ (cos‘π) = (((;16 · ((𝐹 / 2)↑5)) − (;20 · ((𝐹 / 2)↑3))) + (5 · (𝐹 / 2)))
Theorem	goldratmolem2 47877	Lemma 2 for determining the value of golden ratio. (Contributed by Ender Ting, 9-May-2026.)
⊢ 𝐹 = (2 · (cos‘(π / 5)))    ⇒   ⊢ -1 = ((((𝐹↑5) / 2) − (5 · ((𝐹↑3) / 2))) + (5 · (𝐹 / 2)))
Theorem	goldratmolem3 47878	Lemma 3 for determining the value of golden ratio. (Contributed by Ender Ting, 23-Jul-2026.)
⊢ 𝐹 = (2 · (cos‘(π / 5)))    ⇒   ⊢ ((((𝐹↑5) − (5 · (𝐹↑3))) + (5 · 𝐹)) + 2) = 0
Theorem	goldratmolem4 47879	Lemma 4 for determining the value of golden ratio. (Contributed by Ender Ting, 24-Jul-2026.)
⊢ 𝐹 = (2 · (cos‘(π / 5)))    ⇒   ⊢ (((𝐹↑2) − 𝐹) − 1) = 0
Theorem	goldratval 47880	Value of the golden ratio. (Contributed by Ender Ting, 24-Jul-2026.)
⊢ 𝐹 = (2 · (cos‘(π / 5)))    ⇒   ⊢ 𝐹 = ((1 + (√‘5)) / 2)
Theorem	lambert0 47881	A value of Lambert W (product logarithm) function at zero. (Contributed by Ender Ting, 13-Nov-2025.)
⊢ 𝑅 = ◡(𝑥 ∈ ℂ ↦ (𝑥 · (exp‘𝑥)))    ⇒   ⊢ 0𝑅0
Theorem	lamberte 47882	A value of Lambert W (product logarithm) function at e. (Contributed by Ender Ting, 13-Nov-2025.)
⊢ 𝑅 = ◡(𝑥 ∈ ℂ ↦ (𝑥 · (exp‘𝑥)))    ⇒   ⊢ e𝑅1
Theorem	cjnpoly 47883	Complex conjugation operator is not a polynomial with complex coefficients. Indeed; if it was, then multiplying 𝑥 conjugate by 𝑥 itself and adding 1 would yield a nowhere-zero non-constant polynomial, contrary to the fta 27389. (Contributed by Ender Ting, 8-Dec-2025.)
⊢ ¬ ∗ ∈ (Poly‘ℂ)
Theorem	tannpoly 47884	The tangent function is not a polynomial with complex coefficients, as it is not defined on the whole complex plane. (Contributed by Ender Ting, 10-Dec-2025.)
⊢ ¬ tan ∈ (Poly‘ℂ)
Theorem	sinnpoly 47885	Sine function is not a polynomial with complex coefficients. Indeed, it has infinitely many zeros but is not constant zero, contrary to fta1 26611. (Contributed by Ender Ting, 10-Dec-2025.)
⊢ ¬ sin ∈ (Poly‘ℂ)
Theorem	sqrtrrnpoly 47886	Real square root is not a polynomial with real coefficients, because its value is imaginary for negative arguments. (Contributed by Ender Ting, 22-Jul-2026.)
⊢ ¬ √ ∈ (Poly‘ℝ)
Theorem	sqrtnpoly 47887	Square root function is not polynomial with complex coefficients either. Otherwise, its composition with a square monomial - the identity - would have to be of even degree. (Contributed by Ender Ting, 22-Jul-2026.)
⊢ ¬ √ ∈ (Poly‘ℂ)
21.47.5  Turing Machine Finite Reach theorem
Theorem	tmachlem-extapes 47888*	The class of all tapes is a set. (Contributed by Ender Ting, 27-Jul-2026.)
⊢ (𝜑 → 𝑈 ∈ Fin)    &   ⊢ (𝜑 → 𝐼 ∈ V)    &   ⊢ (𝜑 → 𝑇 = (𝑈 ↑m 𝐼))    &   ⊢ (𝜑 → 𝑆:𝑇⟶(𝒫 𝐼 ∩ Fin))    &   ⊢ (𝜑 → 𝐴 = (𝑧 ∈ 𝑇 ↦ {𝑦 ∈ 𝑇 ∣ (𝑦 ↾ (𝑆‘𝑧)) = (𝑧 ↾ (𝑆‘𝑧))}))    &   ⊢ (𝜑 → ∀𝑧 ∈ 𝑇 ∀𝑦 ∈ (𝐴‘𝑧)(𝑆‘𝑦) = (𝑆‘𝑧))    ⇒   ⊢ (𝜑 → 𝑇 ∈ V)
Theorem	tmachlem-finscan 47889*	Execution on any tape only scanned a finite number of cells. (Contributed by Ender Ting, 27-Jul-2026.)
⊢ (𝜑 → 𝑈 ∈ Fin)    &   ⊢ (𝜑 → 𝐼 ∈ V)    &   ⊢ (𝜑 → 𝑇 = (𝑈 ↑m 𝐼))    &   ⊢ (𝜑 → 𝑆:𝑇⟶(𝒫 𝐼 ∩ Fin))    &   ⊢ (𝜑 → 𝐴 = (𝑧 ∈ 𝑇 ↦ {𝑦 ∈ 𝑇 ∣ (𝑦 ↾ (𝑆‘𝑧)) = (𝑧 ↾ (𝑆‘𝑧))}))    &   ⊢ (𝜑 → ∀𝑧 ∈ 𝑇 ∀𝑦 ∈ (𝐴‘𝑧)(𝑆‘𝑦) = (𝑆‘𝑧))    ⇒   ⊢ ((𝜑 ∧ 𝑎 ∈ 𝑇) → (𝑆‘𝑎) ∈ Fin)
Theorem	tmachlem-agreeself 47890*	Any tape belongs to its own agreement set. (Contributed by Ender Ting, 27-Jul-2026.)
⊢ (𝜑 → 𝑈 ∈ Fin)    &   ⊢ (𝜑 → 𝐼 ∈ V)    &   ⊢ (𝜑 → 𝑇 = (𝑈 ↑m 𝐼))    &   ⊢ (𝜑 → 𝑆:𝑇⟶(𝒫 𝐼 ∩ Fin))    &   ⊢ (𝜑 → 𝐴 = (𝑧 ∈ 𝑇 ↦ {𝑦 ∈ 𝑇 ∣ (𝑦 ↾ (𝑆‘𝑧)) = (𝑧 ↾ (𝑆‘𝑧))}))    &   ⊢ (𝜑 → ∀𝑧 ∈ 𝑇 ∀𝑦 ∈ (𝐴‘𝑧)(𝑆‘𝑦) = (𝑆‘𝑧))    ⇒   ⊢ ((𝜑 ∧ 𝑎 ∈ 𝑇) → 𝑎 ∈ (𝐴‘𝑎))
Theorem	tmachlem-agreeprod 47891*	Agreement set can be written as infinite product of acceptable values for tape's cells. (Contributed by Ender Ting, 27-Jul-2026.)
⊢ (𝜑 → 𝑈 ∈ Fin)    &   ⊢ (𝜑 → 𝐼 ∈ V)    &   ⊢ (𝜑 → 𝑇 = (𝑈 ↑m 𝐼))    &   ⊢ (𝜑 → 𝑆:𝑇⟶(𝒫 𝐼 ∩ Fin))    &   ⊢ (𝜑 → 𝐴 = (𝑧 ∈ 𝑇 ↦ {𝑦 ∈ 𝑇 ∣ (𝑦 ↾ (𝑆‘𝑧)) = (𝑧 ↾ (𝑆‘𝑧))}))    &   ⊢ (𝜑 → ∀𝑧 ∈ 𝑇 ∀𝑦 ∈ (𝐴‘𝑧)(𝑆‘𝑦) = (𝑆‘𝑧))    ⇒   ⊢ ((𝜑 ∧ 𝑎 ∈ 𝑇) → (𝐴‘𝑎) = X𝑖 ∈ 𝐼 if(𝑖 ∈ (𝑆‘𝑎), {(𝑎‘𝑖)}, 𝑈))
Theorem	tmachlem-tpcomp 47892*	Product (discrete) topology of tapes is compact by Tychonoff's theorem. To work for infinite index sets (such as ℤ for 𝐼 which is the main interpretation), it requires Choice. (Contributed by Ender Ting, 27-Jul-2026.)
⊢ (𝜑 → 𝑈 ∈ Fin)    &   ⊢ (𝜑 → 𝐼 ∈ V)    &   ⊢ (𝜑 → 𝑇 = (𝑈 ↑m 𝐼))    &   ⊢ (𝜑 → 𝑆:𝑇⟶(𝒫 𝐼 ∩ Fin))    &   ⊢ (𝜑 → 𝐴 = (𝑧 ∈ 𝑇 ↦ {𝑦 ∈ 𝑇 ∣ (𝑦 ↾ (𝑆‘𝑧)) = (𝑧 ↾ (𝑆‘𝑧))}))    &   ⊢ (𝜑 → ∀𝑧 ∈ 𝑇 ∀𝑦 ∈ (𝐴‘𝑧)(𝑆‘𝑦) = (𝑆‘𝑧))    ⇒   ⊢ (𝜑 → (∏t‘(𝑖 ∈ 𝐼 ↦ 𝒫 𝑈)) ∈ Comp)
Theorem	tmachlem-tpbase 47893*	The base set of product topology of tapes is the set of tapes. (Contributed by Ender Ting, 28-Jul-2026.)
⊢ (𝜑 → 𝑈 ∈ Fin)    &   ⊢ (𝜑 → 𝐼 ∈ V)    &   ⊢ (𝜑 → 𝑇 = (𝑈 ↑m 𝐼))    &   ⊢ (𝜑 → 𝑆:𝑇⟶(𝒫 𝐼 ∩ Fin))    &   ⊢ (𝜑 → 𝐴 = (𝑧 ∈ 𝑇 ↦ {𝑦 ∈ 𝑇 ∣ (𝑦 ↾ (𝑆‘𝑧)) = (𝑧 ↾ (𝑆‘𝑧))}))    &   ⊢ (𝜑 → ∀𝑧 ∈ 𝑇 ∀𝑦 ∈ (𝐴‘𝑧)(𝑆‘𝑦) = (𝑆‘𝑧))    ⇒   ⊢ (𝜑 → ∪ (∏t‘(𝑖 ∈ 𝐼 ↦ 𝒫 𝑈)) = 𝑇)
Theorem	tmachlem-tpitem 47894*	Topology lemma. (Contributed by Ender Ting, 27-Jul-2026.)
⊢ (𝜑 → 𝑈 ∈ Fin)    &   ⊢ (𝜑 → 𝐼 ∈ V)    &   ⊢ (𝜑 → 𝑇 = (𝑈 ↑m 𝐼))    &   ⊢ (𝜑 → 𝑆:𝑇⟶(𝒫 𝐼 ∩ Fin))    &   ⊢ (𝜑 → 𝐴 = (𝑧 ∈ 𝑇 ↦ {𝑦 ∈ 𝑇 ∣ (𝑦 ↾ (𝑆‘𝑧)) = (𝑧 ↾ (𝑆‘𝑧))}))    &   ⊢ (𝜑 → ∀𝑧 ∈ 𝑇 ∀𝑦 ∈ (𝐴‘𝑧)(𝑆‘𝑦) = (𝑆‘𝑧))    ⇒   ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐼) → ((𝑖 ∈ 𝐼 ↦ 𝒫 𝑈)‘𝑎) = 𝒫 𝑈)
Theorem	tmachlem-tpopen 47895*	Agreement sets are open in the product topology of tapes. (Contributed by Ender Ting, 27-Jul-2026.)
⊢ (𝜑 → 𝑈 ∈ Fin)    &   ⊢ (𝜑 → 𝐼 ∈ V)    &   ⊢ (𝜑 → 𝑇 = (𝑈 ↑m 𝐼))    &   ⊢ (𝜑 → 𝑆:𝑇⟶(𝒫 𝐼 ∩ Fin))    &   ⊢ (𝜑 → 𝐴 = (𝑧 ∈ 𝑇 ↦ {𝑦 ∈ 𝑇 ∣ (𝑦 ↾ (𝑆‘𝑧)) = (𝑧 ↾ (𝑆‘𝑧))}))    &   ⊢ (𝜑 → ∀𝑧 ∈ 𝑇 ∀𝑦 ∈ (𝐴‘𝑧)(𝑆‘𝑦) = (𝑆‘𝑧))    ⇒   ⊢ ((𝜑 ∧ 𝑎 ∈ 𝑇) → X𝑏 ∈ 𝐼 if(𝑏 ∈ (𝑆‘𝑎), {(𝑎‘𝑏)}, 𝑈) ∈ (∏t‘(𝑖 ∈ 𝐼 ↦ 𝒫 𝑈)))
Theorem	tmachlem-tpopen2 47896*	Variable-renaming lemma connecting tmachlem-agreeprod 47891 and tmachlem-tpopen 47895. (Contributed by Ender Ting, 27-Jul-2026.)
⊢ (𝜑 → 𝑈 ∈ Fin)    &   ⊢ (𝜑 → 𝐼 ∈ V)    &   ⊢ (𝜑 → 𝑇 = (𝑈 ↑m 𝐼))    &   ⊢ (𝜑 → 𝑆:𝑇⟶(𝒫 𝐼 ∩ Fin))    &   ⊢ (𝜑 → 𝐴 = (𝑧 ∈ 𝑇 ↦ {𝑦 ∈ 𝑇 ∣ (𝑦 ↾ (𝑆‘𝑧)) = (𝑧 ↾ (𝑆‘𝑧))}))    &   ⊢ (𝜑 → ∀𝑧 ∈ 𝑇 ∀𝑦 ∈ (𝐴‘𝑧)(𝑆‘𝑦) = (𝑆‘𝑧))    ⇒   ⊢ ((𝜑 ∧ 𝑎 ∈ 𝑇) → (𝐴‘𝑎) ∈ (∏t‘(𝑏 ∈ 𝐼 ↦ 𝒫 𝑈)))
Theorem	tmachlem-uassst 47897*	Union of all agreement sets only includes tapes. (Contributed by Ender Ting, 28-Jul-2026.)
⊢ (𝜑 → 𝑈 ∈ Fin)    &   ⊢ (𝜑 → 𝐼 ∈ V)    &   ⊢ (𝜑 → 𝑇 = (𝑈 ↑m 𝐼))    &   ⊢ (𝜑 → 𝑆:𝑇⟶(𝒫 𝐼 ∩ Fin))    &   ⊢ (𝜑 → 𝐴 = (𝑧 ∈ 𝑇 ↦ {𝑦 ∈ 𝑇 ∣ (𝑦 ↾ (𝑆‘𝑧)) = (𝑧 ↾ (𝑆‘𝑧))}))    &   ⊢ (𝜑 → ∀𝑧 ∈ 𝑇 ∀𝑦 ∈ (𝐴‘𝑧)(𝑆‘𝑦) = (𝑆‘𝑧))    ⇒   ⊢ (𝜑 → ∪ ran 𝐴 ⊆ 𝑇)
Theorem	tmachlem-exlargecover 47898*	Product topology of tapes has an open cover. (Contributed by Ender Ting, 28-Jul-2026.)
⊢ (𝜑 → 𝑈 ∈ Fin)    &   ⊢ (𝜑 → 𝐼 ∈ V)    &   ⊢ (𝜑 → 𝑇 = (𝑈 ↑m 𝐼))    &   ⊢ (𝜑 → 𝑆:𝑇⟶(𝒫 𝐼 ∩ Fin))    &   ⊢ (𝜑 → 𝐴 = (𝑧 ∈ 𝑇 ↦ {𝑦 ∈ 𝑇 ∣ (𝑦 ↾ (𝑆‘𝑧)) = (𝑧 ↾ (𝑆‘𝑧))}))    &   ⊢ (𝜑 → ∀𝑧 ∈ 𝑇 ∀𝑦 ∈ (𝐴‘𝑧)(𝑆‘𝑦) = (𝑆‘𝑧))    ⇒   ⊢ (𝜑 → ∪ ran 𝐴 = 𝑇)
Theorem	tmachlem-extpcover 47899*	Product topology of tapes admits finite cover. (Contributed by Ender Ting, 28-Jul-2026.)
⊢ (𝜑 → 𝑈 ∈ Fin)    &   ⊢ (𝜑 → 𝐼 ∈ V)    &   ⊢ (𝜑 → 𝑇 = (𝑈 ↑m 𝐼))    &   ⊢ (𝜑 → 𝑆:𝑇⟶(𝒫 𝐼 ∩ Fin))    &   ⊢ (𝜑 → 𝐴 = (𝑧 ∈ 𝑇 ↦ {𝑦 ∈ 𝑇 ∣ (𝑦 ↾ (𝑆‘𝑧)) = (𝑧 ↾ (𝑆‘𝑧))}))    &   ⊢ (𝜑 → ∀𝑧 ∈ 𝑇 ∀𝑦 ∈ (𝐴‘𝑧)(𝑆‘𝑦) = (𝑆‘𝑧))    ⇒   ⊢ (𝜑 → ∃𝑎 ∈ (𝒫 ran 𝐴 ∩ Fin)∪ (∏t‘(𝑖 ∈ 𝐼 ↦ 𝒫 𝑈)) = ∪ 𝑎)
Theorem	tmachlem-exagreecover 47900*	Particular properties of the finite cover of agreesets. (Contributed by Ender Ting, 28-Jul-2026.)
⊢ (𝜑 → 𝑈 ∈ Fin)    &   ⊢ (𝜑 → 𝐼 ∈ V)    &   ⊢ (𝜑 → 𝑇 = (𝑈 ↑m 𝐼))    &   ⊢ (𝜑 → 𝑆:𝑇⟶(𝒫 𝐼 ∩ Fin))    &   ⊢ (𝜑 → 𝐴 = (𝑧 ∈ 𝑇 ↦ {𝑦 ∈ 𝑇 ∣ (𝑦 ↾ (𝑆‘𝑧)) = (𝑧 ↾ (𝑆‘𝑧))}))    &   ⊢ (𝜑 → ∀𝑧 ∈ 𝑇 ∀𝑦 ∈ (𝐴‘𝑧)(𝑆‘𝑦) = (𝑆‘𝑧))    ⇒   ⊢ (𝜑 → ∃𝑎(𝑎 ⊆ ran 𝐴 ∧ 𝑎 ∈ Fin ∧ 𝑇 = ∪ 𝑎))