P. 332 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 33101-33200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	indfsd 33101	The indicator function of a finite set has finite support. (Contributed by Thierry Arnoux, 18-Jan-2026.)
⊢ (𝜑 → 𝑂 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑂)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    ⇒   ⊢ (𝜑 → ((𝟭‘𝑂)‘𝐴) finSupp 0)
Theorem	indfsid 33102	Conditions for a function to be an indicator function. (Contributed by Thierry Arnoux, 18-Jan-2026.)
⊢ (𝜑 → 𝑂 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝑂⟶{0, 1})    ⇒   ⊢ (𝜑 → 𝐹 = ((𝟭‘𝑂)‘(𝐹 supp 0)))
21.3.7  Decimal expansion Define a decimal expansion constructor. The decimal expansions built with this constructor are not meant to be used alone outside of this chapter. Rather, they are meant to be used exclusively as part of a decimal number with a decimal fraction, for example (3._1_4_1_59). That decimal point operator is defined in the next section. The bulk of these constructions have originally been proposed by David A. Wheeler on 12-May-2015, and discussed with Mario Carneiro in this thread: https://groups.google.com/g/metamath/c/2AW7T3d2YiQ.
Syntax	cdp2 33103	Constant used for decimal fraction constructor. See df-dp2 33104.
class _𝐴𝐵
Definition	df-dp2 33104	Define the "decimal fraction constructor", which is used to build up "decimal fractions" in base 10. This is intentionally similar to df-dec 12703. (Contributed by David A. Wheeler, 15-May-2015.) (Revised by AV, 9-Sep-2021.)
⊢ _𝐴𝐵 = (𝐴 + (𝐵 / ;10))
Theorem	dp2eq1 33105	Equality theorem for the decimal expansion constructor. (Contributed by David A. Wheeler, 15-May-2015.)
⊢ (𝐴 = 𝐵 → _𝐴𝐶 = _𝐵𝐶)
Theorem	dp2eq2 33106	Equality theorem for the decimal expansion constructor. (Contributed by David A. Wheeler, 15-May-2015.)
⊢ (𝐴 = 𝐵 → _𝐶𝐴 = _𝐶𝐵)
Theorem	dp2eq1i 33107	Equality theorem for the decimal expansion constructor. (Contributed by David A. Wheeler, 15-May-2015.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ _𝐴𝐶 = _𝐵𝐶
Theorem	dp2eq2i 33108	Equality theorem for the decimal expansion constructor. (Contributed by David A. Wheeler, 15-May-2015.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ _𝐶𝐴 = _𝐶𝐵
Theorem	dp2eq12i 33109	Equality theorem for the decimal expansion constructor. (Contributed by David A. Wheeler, 15-May-2015.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ _𝐴𝐶 = _𝐵𝐷
Theorem	dp20u 33110	Add a zero in the tenths (lower) place. (Contributed by Thierry Arnoux, 16-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    ⇒   ⊢ _𝐴0 = 𝐴
Theorem	dp20h 33111	Add a zero in the unit places. (Contributed by Thierry Arnoux, 16-Dec-2021.)
⊢ 𝐴 ∈ ℝ+    ⇒   ⊢ _0𝐴 = (𝐴 / ;10)
Theorem	dp2cl 33112	Closure for the decimal fraction constructor if both values are reals. (Contributed by David A. Wheeler, 15-May-2015.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → _𝐴𝐵 ∈ ℝ)
Theorem	dp2clq 33113	Closure for a decimal fraction. (Contributed by Thierry Arnoux, 16-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℚ    ⇒   ⊢ _𝐴𝐵 ∈ ℚ
Theorem	rpdp2cl 33114	Closure for a decimal fraction in the positive real numbers. (Contributed by Thierry Arnoux, 16-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℝ+    ⇒   ⊢ _𝐴𝐵 ∈ ℝ+
Theorem	rpdp2cl2 33115	Closure for a decimal fraction with no decimal expansion in the positive real numbers. (Contributed by Thierry Arnoux, 25-Dec-2021.)
⊢ 𝐴 ∈ ℕ    ⇒   ⊢ _𝐴0 ∈ ℝ+
Theorem	dp2lt10 33116	Decimal fraction builds real numbers less than 10. (Contributed by Thierry Arnoux, 16-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℝ+    &   ⊢ 𝐴 < ;10    &   ⊢ 𝐵 < ;10    ⇒   ⊢ _𝐴𝐵 < ;10
Theorem	dp2lt 33117	Comparing two decimal fractions (equal unit places). (Contributed by Thierry Arnoux, 16-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℝ+    &   ⊢ 𝐶 ∈ ℝ+    &   ⊢ 𝐵 < 𝐶    ⇒   ⊢ _𝐴𝐵 < _𝐴𝐶
Theorem	dp2ltsuc 33118	Comparing a decimal fraction with the next integer. (Contributed by Thierry Arnoux, 25-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℝ+    &   ⊢ 𝐵 < ;10    &   ⊢ (𝐴 + 1) = 𝐶    ⇒   ⊢ _𝐴𝐵 < 𝐶
Theorem	dp2ltc 33119	Comparing two decimal expansions (unequal higher places). (Contributed by Thierry Arnoux, 16-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℝ+    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℝ+    &   ⊢ 𝐵 < ;10    &   ⊢ 𝐴 < 𝐶    ⇒   ⊢ _𝐴𝐵 < _𝐶𝐷
21.3.7.1  Decimal point Define the decimal point operator and the decimal fraction constructor. This can model traditional decimal point notation, and serve as a convenient way to write some fractional numbers. See df-dp 33121 and df-dp2 33104 for more information; dpval2 33125 and dpfrac1 33124 provide a more convenient way to obtain a value. This is intentionally similar to df-dec 12703.
Syntax	cdp 33120	Decimal point operator. See df-dp 33121.
class .
Definition	df-dp 33121*	Define the . (decimal point) operator. For example, (1.5) = (3 / 2), and -(;32._7_18) = -(;;;;32718 / ;;;1000) Unary minus, if applied, should normally be applied in front of the parentheses. Metamath intentionally does not have a built-in construct for numbers, so it can show that numbers are something you can build based on set theory. However, that means that Metamath has no built-in way to parse and handle decimal numbers as traditionally written, e.g., "2.54". Here we create a system for modeling traditional decimal point notation; it is not syntactically identical, but it is sufficiently similar so it is a reasonable model of decimal point notation. It should also serve as a convenient way to write some fractional numbers. The RHS is ℝ, not ℚ; this should simplify some proofs. The LHS is ℕ0, since that is what is used in practice. The definition intentionally does not allow negative numbers on the LHS; if it did, nonzero fractions would produce the wrong results. (It would be possible to define the decimal point to do this, but using it would be more complicated, and the expression -(𝐴.𝐵) is just as convenient.) (Contributed by David A. Wheeler, 15-May-2015.)
⊢ . = (𝑥 ∈ ℕ0, 𝑦 ∈ ℝ ↦ _𝑥𝑦)
Theorem	dpval 33122	Define the value of the decimal point operator. See df-dp 33121. (Contributed by David A. Wheeler, 15-May-2015.)
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℝ) → (𝐴.𝐵) = _𝐴𝐵)
Theorem	dpcl 33123	Prove that the closure of the decimal point is ℝ as we have defined it. See df-dp 33121. (Contributed by David A. Wheeler, 15-May-2015.)
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℝ) → (𝐴.𝐵) ∈ ℝ)
Theorem	dpfrac1 33124	Prove a simple equivalence involving the decimal point. See df-dp 33121 and dpcl 33123. (Contributed by David A. Wheeler, 15-May-2015.) (Revised by AV, 9-Sep-2021.)
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℝ) → (𝐴.𝐵) = (;𝐴𝐵 / ;10))
Theorem	dpval2 33125	Value of the decimal point construct. (Contributed by Thierry Arnoux, 16-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ (𝐴.𝐵) = (𝐴 + (𝐵 / ;10))
Theorem	dpval3 33126	Value of the decimal point construct. (Contributed by Thierry Arnoux, 16-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ (𝐴.𝐵) = _𝐴𝐵
Theorem	dpmul10 33127	Multiply by 10 a decimal expansion. (Contributed by Thierry Arnoux, 25-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ ((𝐴.𝐵) · ;10) = ;𝐴𝐵
Theorem	decdiv10 33128	Divide a decimal number by 10. (Contributed by Thierry Arnoux, 25-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ (;𝐴𝐵 / ;10) = (𝐴.𝐵)
Theorem	dpmul100 33129	Multiply by 100 a decimal expansion. (Contributed by Thierry Arnoux, 25-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℝ    ⇒   ⊢ ((𝐴._𝐵𝐶) · ;;100) = ;;𝐴𝐵𝐶
Theorem	dp3mul10 33130	Multiply by 10 a decimal expansion with 3 digits. (Contributed by Thierry Arnoux, 25-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℝ    ⇒   ⊢ ((𝐴._𝐵𝐶) · ;10) = (;𝐴𝐵.𝐶)
Theorem	dpmul1000 33131	Multiply by 1000 a decimal expansion. (Contributed by Thierry Arnoux, 25-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℝ    ⇒   ⊢ ((𝐴._𝐵_𝐶𝐷) · ;;;1000) = ;;;𝐴𝐵𝐶𝐷
Theorem	dpval3rp 33132	Value of the decimal point construct. (Contributed by Thierry Arnoux, 16-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℝ+    ⇒   ⊢ (𝐴.𝐵) = _𝐴𝐵
Theorem	dp0u 33133	Add a zero in the tenths place. (Contributed by Thierry Arnoux, 16-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    ⇒   ⊢ (𝐴.0) = 𝐴
Theorem	dp0h 33134	Remove a zero in the units places. (Contributed by Thierry Arnoux, 16-Dec-2021.)
⊢ 𝐴 ∈ ℝ+    ⇒   ⊢ (0.𝐴) = (𝐴 / ;10)
Theorem	rpdpcl 33135	Closure of the decimal point in the positive real numbers. (Contributed by Thierry Arnoux, 16-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℝ+    ⇒   ⊢ (𝐴.𝐵) ∈ ℝ+
Theorem	dplt 33136	Comparing two decimal expansions (equal higher places). (Contributed by Thierry Arnoux, 16-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℝ+    &   ⊢ 𝐶 ∈ ℝ+    &   ⊢ 𝐵 < 𝐶    ⇒   ⊢ (𝐴.𝐵) < (𝐴.𝐶)
Theorem	dplti 33137	Comparing a decimal expansions with the next higher integer. (Contributed by Thierry Arnoux, 16-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℝ+    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐵 < ;10    &   ⊢ (𝐴 + 1) = 𝐶    ⇒   ⊢ (𝐴.𝐵) < 𝐶
Theorem	dpgti 33138	Comparing a decimal expansions with the next lower integer. (Contributed by Thierry Arnoux, 16-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℝ+    ⇒   ⊢ 𝐴 < (𝐴.𝐵)
Theorem	dpltc 33139	Comparing two decimal integers (unequal higher places). (Contributed by Thierry Arnoux, 16-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℝ+    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℝ+    &   ⊢ 𝐴 < 𝐶    &   ⊢ 𝐵 < ;10    ⇒   ⊢ (𝐴.𝐵) < (𝐶.𝐷)
Theorem	dpexpp1 33140	Add one zero to the mantisse, and a one to the exponent in a scientific notation. (Contributed by Thierry Arnoux, 16-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℝ+    &   ⊢ (𝑃 + 1) = 𝑄    &   ⊢ 𝑃 ∈ ℤ    &   ⊢ 𝑄 ∈ ℤ    ⇒   ⊢ ((𝐴.𝐵) · (;10↑𝑃)) = ((0._𝐴𝐵) · (;10↑𝑄))
Theorem	0dp2dp 33141	Multiply by 10 a decimal expansion which starts with a zero. (Contributed by Thierry Arnoux, 16-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℝ+    ⇒   ⊢ ((0._𝐴𝐵) · ;10) = (𝐴.𝐵)
Theorem	dpadd2 33142	Addition with one decimal, no carry. (Contributed by Thierry Arnoux, 29-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℝ+    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℝ+    &   ⊢ 𝐸 ∈ ℕ0    &   ⊢ 𝐹 ∈ ℝ+    &   ⊢ 𝐺 ∈ ℕ0    &   ⊢ 𝐻 ∈ ℕ0    &   ⊢ (𝐺 + 𝐻) = 𝐼    &   ⊢ ((𝐴.𝐵) + (𝐶.𝐷)) = (𝐸.𝐹)    ⇒   ⊢ ((𝐺._𝐴𝐵) + (𝐻._𝐶𝐷)) = (𝐼._𝐸𝐹)
Theorem	dpadd 33143	Addition with one decimal. (Contributed by Thierry Arnoux, 27-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℕ0    &   ⊢ 𝐸 ∈ ℕ0    &   ⊢ 𝐹 ∈ ℕ0    &   ⊢ (;𝐴𝐵 + ;𝐶𝐷) = ;𝐸𝐹    ⇒   ⊢ ((𝐴.𝐵) + (𝐶.𝐷)) = (𝐸.𝐹)
Theorem	dpadd3 33144	Addition with two decimals. (Contributed by Thierry Arnoux, 27-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℕ0    &   ⊢ 𝐸 ∈ ℕ0    &   ⊢ 𝐺 ∈ ℕ0    &   ⊢ 𝐹 ∈ ℕ0    &   ⊢ 𝐻 ∈ ℕ0    &   ⊢ 𝐼 ∈ ℕ0    &   ⊢ (;;𝐴𝐵𝐶 + ;;𝐷𝐸𝐹) = ;;𝐺𝐻𝐼    ⇒   ⊢ ((𝐴._𝐵𝐶) + (𝐷._𝐸𝐹)) = (𝐺._𝐻𝐼)
Theorem	dpmul 33145	Multiplication with one decimal point. (Contributed by Thierry Arnoux, 26-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℕ0    &   ⊢ 𝐸 ∈ ℕ0    &   ⊢ 𝐺 ∈ ℕ0    &   ⊢ 𝐽 ∈ ℕ0    &   ⊢ 𝐾 ∈ ℕ0    &   ⊢ (𝐴 · 𝐶) = 𝐹    &   ⊢ (𝐴 · 𝐷) = 𝑀    &   ⊢ (𝐵 · 𝐶) = 𝐿    &   ⊢ (𝐵 · 𝐷) = ;𝐸𝐾    &   ⊢ ((𝐿 + 𝑀) + 𝐸) = ;𝐺𝐽    &   ⊢ (𝐹 + 𝐺) = 𝐼    ⇒   ⊢ ((𝐴.𝐵) · (𝐶.𝐷)) = (𝐼._𝐽𝐾)
Theorem	dpmul4 33146	An upper bound to multiplication of decimal numbers with 4 digits. (Contributed by Thierry Arnoux, 25-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℕ0    &   ⊢ 𝐸 ∈ ℕ0    &   ⊢ 𝐺 ∈ ℕ0    &   ⊢ 𝐽 ∈ ℕ0    &   ⊢ 𝐾 ∈ ℕ0    &   ⊢ 𝐹 ∈ ℕ0    &   ⊢ 𝐻 ∈ ℕ0    &   ⊢ 𝐼 ∈ ℕ0    &   ⊢ 𝐿 ∈ ℕ0    &   ⊢ 𝑀 ∈ ℕ0    &   ⊢ 𝑁 ∈ ℕ0    &   ⊢ 𝑂 ∈ ℕ0    &   ⊢ 𝑃 ∈ ℕ0    &   ⊢ 𝑄 ∈ ℕ0    &   ⊢ 𝑅 ∈ ℕ0    &   ⊢ 𝑆 ∈ ℕ0    &   ⊢ 𝑇 ∈ ℕ0    &   ⊢ 𝑈 ∈ ℕ0    &   ⊢ 𝑊 ∈ ℕ0    &   ⊢ 𝑋 ∈ ℕ0    &   ⊢ 𝑌 ∈ ℕ0    &   ⊢ 𝑍 ∈ ℕ0    &   ⊢ 𝑈 < ;10    &   ⊢ 𝑃 < ;10    &   ⊢ 𝑄 < ;10    &   ⊢ (;;𝐿𝑀𝑁 + 𝑂) = ;;;𝑅𝑆𝑇𝑈    &   ⊢ ((𝐴.𝐵) · (𝐸.𝐹)) = (𝐼._𝐽𝐾)    &   ⊢ ((𝐶.𝐷) · (𝐺.𝐻)) = (𝑂._𝑃𝑄)    &   ⊢ (;;;𝐼𝐽𝐾1 + ;;𝑅𝑆𝑇) = ;;;𝑊𝑋𝑌𝑍    &   ⊢ (((𝐴.𝐵) + (𝐶.𝐷)) · ((𝐸.𝐹) + (𝐺.𝐻))) = (((𝐼._𝐽𝐾) + (𝐿._𝑀𝑁)) + (𝑂._𝑃𝑄))    ⇒   ⊢ ((𝐴._𝐵_𝐶𝐷) · (𝐸._𝐹_𝐺𝐻)) < (𝑊._𝑋_𝑌𝑍)
Theorem	threehalves 33147	Example theorem demonstrating decimal expansions. (Contributed by Thierry Arnoux, 27-Dec-2021.)
⊢ (3 / 2) = (1.5)
Theorem	1mhdrd 33148	Example theorem demonstrating decimal expansions. (Contributed by Thierry Arnoux, 27-Dec-2021.)
⊢ ((0._99) + (0._01)) = 1
21.3.7.2  Division in the extended real number system
Syntax	cxdiv 33149	Extend class notation to include division of extended reals.
class /𝑒
Definition	df-xdiv 33150*	Define division over extended real numbers. (Contributed by Thierry Arnoux, 17-Dec-2016.)
⊢ /𝑒 = (𝑥 ∈ ℝ*, 𝑦 ∈ (ℝ ∖ {0}) ↦ (℩𝑧 ∈ ℝ* (𝑦 ·e 𝑧) = 𝑥))
Theorem	xdivval 33151*	Value of division: the (unique) element 𝑥 such that (𝐵 · 𝑥) = 𝐴. This is meaningful only when 𝐵 is nonzero. (Contributed by Thierry Arnoux, 17-Dec-2016.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → (𝐴 /𝑒 𝐵) = (℩𝑥 ∈ ℝ* (𝐵 ·e 𝑥) = 𝐴))
Theorem	xrecex 33152*	Existence of reciprocal of nonzero real number. (Contributed by Thierry Arnoux, 17-Dec-2016.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) → ∃𝑥 ∈ ℝ (𝐴 ·e 𝑥) = 1)
Theorem	xmulcand 33153	Cancellation law for extended multiplication. (Contributed by Thierry Arnoux, 17-Dec-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ≠ 0)    ⇒   ⊢ (𝜑 → ((𝐶 ·e 𝐴) = (𝐶 ·e 𝐵) ↔ 𝐴 = 𝐵))
Theorem	xreceu 33154*	Existential uniqueness of reciprocals. Theorem I.8 of [Apostol] p. 18. (Contributed by Thierry Arnoux, 17-Dec-2016.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → ∃!𝑥 ∈ ℝ* (𝐵 ·e 𝑥) = 𝐴)
Theorem	xdivcld 33155	Closure law for the extended division. (Contributed by Thierry Arnoux, 15-Mar-2017.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    ⇒   ⊢ (𝜑 → (𝐴 /𝑒 𝐵) ∈ ℝ*)
Theorem	xdivcl 33156	Closure law for the extended division. (Contributed by Thierry Arnoux, 15-Mar-2017.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → (𝐴 /𝑒 𝐵) ∈ ℝ*)
Theorem	xdivmul 33157	Relationship between division and multiplication. (Contributed by Thierry Arnoux, 24-Dec-2016.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ (𝐶 ∈ ℝ ∧ 𝐶 ≠ 0)) → ((𝐴 /𝑒 𝐶) = 𝐵 ↔ (𝐶 ·e 𝐵) = 𝐴))
Theorem	rexdiv 33158	The extended real division operation when both arguments are real. (Contributed by Thierry Arnoux, 18-Dec-2016.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → (𝐴 /𝑒 𝐵) = (𝐴 / 𝐵))
Theorem	xdivrec 33159	Relationship between division and reciprocal. (Contributed by Thierry Arnoux, 5-Jul-2017.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → (𝐴 /𝑒 𝐵) = (𝐴 ·e (1 /𝑒 𝐵)))
Theorem	xdivid 33160	A number divided by itself is one. (Contributed by Thierry Arnoux, 18-Dec-2016.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) → (𝐴 /𝑒 𝐴) = 1)
Theorem	xdiv0 33161	Division into zero is zero. (Contributed by Thierry Arnoux, 18-Dec-2016.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) → (0 /𝑒 𝐴) = 0)
Theorem	xdiv0rp 33162	Division into zero is zero. (Contributed by Thierry Arnoux, 18-Dec-2016.)
⊢ (𝐴 ∈ ℝ+ → (0 /𝑒 𝐴) = 0)
Theorem	eliccioo 33163	Membership in a closed interval of extended reals versus the same open interval. (Contributed by Thierry Arnoux, 18-Dec-2016.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵) → (𝐶 ∈ (𝐴[,]𝐵) ↔ (𝐶 = 𝐴 ∨ 𝐶 ∈ (𝐴(,)𝐵) ∨ 𝐶 = 𝐵)))
Theorem	elxrge02 33164	Elementhood in the set of nonnegative extended reals. (Contributed by Thierry Arnoux, 18-Dec-2016.)
⊢ (𝐴 ∈ (0[,]+∞) ↔ (𝐴 = 0 ∨ 𝐴 ∈ ℝ+ ∨ 𝐴 = +∞))
Theorem	xdivpnfrp 33165	Plus infinity divided by a positive real number is plus infinity. (Contributed by Thierry Arnoux, 18-Dec-2016.)
⊢ (𝐴 ∈ ℝ+ → (+∞ /𝑒 𝐴) = +∞)
Theorem	rpxdivcld 33166	Closure law for extended division of positive reals. (Contributed by Thierry Arnoux, 18-Dec-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    ⇒   ⊢ (𝜑 → (𝐴 /𝑒 𝐵) ∈ ℝ+)
Theorem	xrpxdivcld 33167	Closure law for extended division of positive extended reals. (Contributed by Thierry Arnoux, 18-Dec-2016.)
⊢ (𝜑 → 𝐴 ∈ (0[,]+∞))    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    ⇒   ⊢ (𝜑 → (𝐴 /𝑒 𝐵) ∈ (0[,]+∞))
21.3.8  Words over a set - misc additions
Theorem	wrdres 33168	Condition for the restriction of a word to be a word itself. (Contributed by Thierry Arnoux, 5-Oct-2018.)
⊢ ((𝑊 ∈ Word 𝑆 ∧ 𝑁 ∈ (0...(♯‘𝑊))) → (𝑊 ↾ (0..^𝑁)) ∈ Word 𝑆)
Theorem	wrdsplex 33169*	Existence of a split of a word at a given index. (Contributed by Thierry Arnoux, 11-Oct-2018.) (Proof shortened by AV, 3-Nov-2022.)
⊢ ((𝑊 ∈ Word 𝑆 ∧ 𝑁 ∈ (0...(♯‘𝑊))) → ∃𝑣 ∈ Word 𝑆𝑊 = ((𝑊 ↾ (0..^𝑁)) ++ 𝑣))
Theorem	wrdfsupp 33170	A word has finite support. (Contributed by Thierry Arnoux, 27-May-2025.)
⊢ (𝜑 → 𝑍 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑊 ∈ Word 𝑆)    ⇒   ⊢ (𝜑 → 𝑊 finSupp 𝑍)
Theorem	wrdpmcl 33171	Closure of a word with permuted symbols. (Contributed by Thierry Arnoux, 27-May-2025.)
⊢ 𝐽 = (0..^(♯‘𝑊))    &   ⊢ (𝜑 → 𝐸:𝐽–1-1-onto→𝐽)    &   ⊢ (𝜑 → 𝑊 ∈ Word 𝑆)    ⇒   ⊢ (𝜑 → (𝑊 ∘ 𝐸) ∈ Word 𝑆)
Theorem	pfx1s2 33172	The prefix of length 1 of a length 2 word. (Contributed by Thierry Arnoux, 19-Sep-2023.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (⟨“𝐴𝐵”⟩ prefix 1) = ⟨“𝐴”⟩)
Theorem	pfxrn2 33173	The range of a prefix of a word is a subset of the range of that word. Stronger version of pfxrn 14713. (Contributed by Thierry Arnoux, 12-Dec-2023.)
⊢ ((𝑊 ∈ Word 𝑆 ∧ 𝐿 ∈ (0...(♯‘𝑊))) → ran (𝑊 prefix 𝐿) ⊆ ran 𝑊)
Theorem	pfxrn3 33174	Express the range of a prefix of a word. Stronger version of pfxrn2 33173. (Contributed by Thierry Arnoux, 13-Dec-2023.)
⊢ ((𝑊 ∈ Word 𝑆 ∧ 𝐿 ∈ (0...(♯‘𝑊))) → ran (𝑊 prefix 𝐿) = (𝑊 “ (0..^𝐿)))
Theorem	pfxf1 33175	Condition for a prefix to be injective. (Contributed by Thierry Arnoux, 13-Dec-2023.)
⊢ (𝜑 → 𝑊 ∈ Word 𝑆)    &   ⊢ (𝜑 → 𝑊:dom 𝑊–1-1→𝑆)    &   ⊢ (𝜑 → 𝐿 ∈ (0...(♯‘𝑊)))    ⇒   ⊢ (𝜑 → (𝑊 prefix 𝐿):dom (𝑊 prefix 𝐿)–1-1→𝑆)
Theorem	s1f1 33176	Conditions for a length 1 string to be a one-to-one function. (Contributed by Thierry Arnoux, 11-Dec-2023.)
⊢ (𝜑 → 𝐼 ∈ 𝐷)    ⇒   ⊢ (𝜑 → ⟨“𝐼”⟩:dom ⟨“𝐼”⟩–1-1→𝐷)
Theorem	s2rnOLD 33177	Obsolete version of s2rn 14990 as of 1-Aug-2025. Range of a length 2 string. (Contributed by Thierry Arnoux, 19-Sep-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝐼 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐽 ∈ 𝐷)    ⇒   ⊢ (𝜑 → ran ⟨“𝐼𝐽”⟩ = {𝐼, 𝐽})
Theorem	s2f1 33178	Conditions for a length 2 string to be a one-to-one function. (Contributed by Thierry Arnoux, 19-Sep-2023.)
⊢ (𝜑 → 𝐼 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐽 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐼 ≠ 𝐽)    ⇒   ⊢ (𝜑 → ⟨“𝐼𝐽”⟩:dom ⟨“𝐼𝐽”⟩–1-1→𝐷)
Theorem	s3rnOLD 33179	Obsolete version of s2rn 14990 as of 1-Aug-2025. Range of a length 3 string. (Contributed by Thierry Arnoux, 19-Sep-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝐼 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐽 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐾 ∈ 𝐷)    ⇒   ⊢ (𝜑 → ran ⟨“𝐼𝐽𝐾”⟩ = {𝐼, 𝐽, 𝐾})
Theorem	s3f1 33180	Conditions for a length 3 string to be a one-to-one function. (Contributed by Thierry Arnoux, 19-Sep-2023.)
⊢ (𝜑 → 𝐼 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐽 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐾 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐼 ≠ 𝐽)    &   ⊢ (𝜑 → 𝐽 ≠ 𝐾)    &   ⊢ (𝜑 → 𝐾 ≠ 𝐼)    ⇒   ⊢ (𝜑 → ⟨“𝐼𝐽𝐾”⟩:dom ⟨“𝐼𝐽𝐾”⟩–1-1→𝐷)
Theorem	s3clhash 33181	Closure of the words of length 3 in a preimage using the hash function. (Contributed by Thierry Arnoux, 27-Sep-2023.)
⊢ ⟨“𝐼𝐽𝐾”⟩ ∈ (◡♯ “ {3})
Theorem	ccatf1 33182	Conditions for a concatenation to be injective. (Contributed by Thierry Arnoux, 11-Dec-2023.)
⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐴 ∈ Word 𝑆)    &   ⊢ (𝜑 → 𝐵 ∈ Word 𝑆)    &   ⊢ (𝜑 → 𝐴:dom 𝐴–1-1→𝑆)    &   ⊢ (𝜑 → 𝐵:dom 𝐵–1-1→𝑆)    &   ⊢ (𝜑 → (ran 𝐴 ∩ ran 𝐵) = ∅)    ⇒   ⊢ (𝜑 → (𝐴 ++ 𝐵):dom (𝐴 ++ 𝐵)–1-1→𝑆)
Theorem	pfxlsw2ccat 33183	Reconstruct a word from its prefix and its last two symbols. (Contributed by Thierry Arnoux, 26-Sep-2023.)
⊢ 𝑁 = (♯‘𝑊)    ⇒   ⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁) → 𝑊 = ((𝑊 prefix (𝑁 − 2)) ++ ⟨“(𝑊‘(𝑁 − 2))(𝑊‘(𝑁 − 1))”⟩))
Theorem	ccatws1f1o 33184	Conditions for the concatenation of a word and a singleton word to be bijective. (Contributed by Thierry Arnoux, 27-May-2025.)
⊢ 𝑁 = (♯‘𝑇)    &   ⊢ 𝐽 = (0..^(𝑁 + 1))    &   ⊢ (𝜑 → 𝑇:(0..^𝑁)–1-1-onto→(0..^𝑁))    ⇒   ⊢ (𝜑 → (𝑇 ++ ⟨“𝑁”⟩):𝐽–1-1-onto→𝐽)
Theorem	ccatws1f1olast 33185	Two ways to reorder symbols in a word 𝑊 according to permutation 𝑇, and add a last symbol 𝑋. (Contributed by Thierry Arnoux, 27-May-2025.)
⊢ 𝑁 = (♯‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ Word 𝑆)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑆)    &   ⊢ (𝜑 → 𝑇:(0..^𝑁)–1-1-onto→(0..^𝑁))    ⇒   ⊢ (𝜑 → ((𝑊 ++ ⟨“𝑋”⟩) ∘ (𝑇 ++ ⟨“𝑁”⟩)) = ((𝑊 ∘ 𝑇) ++ ⟨“𝑋”⟩))
Theorem	wrdt2ind 33186*	Perform an induction over the structure of a word of even length. (Contributed by Thierry Arnoux, 26-Sep-2023.)
⊢ (𝑥 = ∅ → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑥 = (𝑦 ++ ⟨“𝑖𝑗”⟩) → (𝜑 ↔ 𝜃))    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏))    &   ⊢ 𝜓    &   ⊢ ((𝑦 ∈ Word 𝐵 ∧ 𝑖 ∈ 𝐵 ∧ 𝑗 ∈ 𝐵) → (𝜒 → 𝜃))    ⇒   ⊢ ((𝐴 ∈ Word 𝐵 ∧ 2 ∥ (♯‘𝐴)) → 𝜏)
Theorem	swrdrn2 33187	The range of a subword is a subset of the range of that word. Stronger version of swrdrn 14680. (Contributed by Thierry Arnoux, 12-Dec-2023.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) → ran (𝑊 substr ⟨𝑀, 𝑁⟩) ⊆ ran 𝑊)
Theorem	swrdrn3 33188	Express the range of a subword. Stronger version of swrdrn2 33187. (Contributed by Thierry Arnoux, 13-Dec-2023.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) → ran (𝑊 substr ⟨𝑀, 𝑁⟩) = (𝑊 “ (𝑀..^𝑁)))
Theorem	swrdf1 33189	Condition for a subword to be injective. (Contributed by Thierry Arnoux, 12-Dec-2023.)
⊢ (𝜑 → 𝑊 ∈ Word 𝐷)    &   ⊢ (𝜑 → 𝑀 ∈ (0...𝑁))    &   ⊢ (𝜑 → 𝑁 ∈ (0...(♯‘𝑊)))    &   ⊢ (𝜑 → 𝑊:dom 𝑊–1-1→𝐷)    ⇒   ⊢ (𝜑 → (𝑊 substr ⟨𝑀, 𝑁⟩):dom (𝑊 substr ⟨𝑀, 𝑁⟩)–1-1→𝐷)
Theorem	swrdrndisj 33190	Condition for the range of two subwords of an injective word to be disjoint. (Contributed by Thierry Arnoux, 13-Dec-2023.)
⊢ (𝜑 → 𝑊 ∈ Word 𝐷)    &   ⊢ (𝜑 → 𝑀 ∈ (0...𝑁))    &   ⊢ (𝜑 → 𝑁 ∈ (0...(♯‘𝑊)))    &   ⊢ (𝜑 → 𝑊:dom 𝑊–1-1→𝐷)    &   ⊢ (𝜑 → 𝑂 ∈ (𝑁...𝑃))    &   ⊢ (𝜑 → 𝑃 ∈ (𝑁...(♯‘𝑊)))    ⇒   ⊢ (𝜑 → (ran (𝑊 substr ⟨𝑀, 𝑁⟩) ∩ ran (𝑊 substr ⟨𝑂, 𝑃⟩)) = ∅)
21.3.8.1  Splicing words (substring replacement)
Theorem	splfv3 33191	Symbols to the right of a splice are unaffected. (Contributed by Thierry Arnoux, 14-Dec-2023.)
⊢ (𝜑 → 𝑆 ∈ Word 𝐴)    &   ⊢ (𝜑 → 𝐹 ∈ (0...𝑇))    &   ⊢ (𝜑 → 𝑇 ∈ (0...(♯‘𝑆)))    &   ⊢ (𝜑 → 𝑅 ∈ Word 𝐴)    &   ⊢ (𝜑 → 𝑋 ∈ (0..^((♯‘𝑆) − 𝑇)))    &   ⊢ (𝜑 → 𝐾 = (𝐹 + (♯‘𝑅)))    ⇒   ⊢ (𝜑 → ((𝑆 splice ⟨𝐹, 𝑇, 𝑅⟩)‘(𝑋 + 𝐾)) = (𝑆‘(𝑋 + 𝑇)))
21.3.8.2  Cyclic shift of words
Theorem	1cshid 33192	Cyclically shifting a single letter word keeps it unchanged. (Contributed by Thierry Arnoux, 21-Nov-2023.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ∧ (♯‘𝑊) = 1) → (𝑊 cyclShift 𝑁) = 𝑊)
Theorem	cshw1s2 33193	Cyclically shifting a length 2 word swaps its symbols. (Contributed by Thierry Arnoux, 19-Sep-2023.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (⟨“𝐴𝐵”⟩ cyclShift 1) = ⟨“𝐵𝐴”⟩)
Theorem	cshwrnid 33194	Cyclically shifting a word preserves its range. (Contributed by Thierry Arnoux, 19-Sep-2023.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ) → ran (𝑊 cyclShift 𝑁) = ran 𝑊)
Theorem	cshf1o 33195	Condition for the cyclic shift to be a bijection. (Contributed by Thierry Arnoux, 4-Oct-2023.)
⊢ ((𝑊 ∈ Word 𝐷 ∧ 𝑊:dom 𝑊–1-1→𝐷 ∧ 𝑁 ∈ ℤ) → (𝑊 cyclShift 𝑁):dom 𝑊–1-1-onto→ran 𝑊)
21.3.9  Extensible Structures
21.3.9.1  Structure restriction operator
Theorem	ressplusf 33196	The group operation function +𝑓 of a structure's restriction is the operation function's restriction to the new base. (Contributed by Thierry Arnoux, 26-Mar-2017.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝐻 = (𝐺 ↾s 𝐴)    &   ⊢ ⨣ = (+g‘𝐺)    &   ⊢ ⨣ Fn (𝐵 × 𝐵)    &   ⊢ 𝐴 ⊆ 𝐵    ⇒   ⊢ (+𝑓‘𝐻) = ( ⨣ ↾ (𝐴 × 𝐴))
Theorem	ressnm 33197	The norm in a restricted structure. (Contributed by Thierry Arnoux, 8-Oct-2017.)
⊢ 𝐻 = (𝐺 ↾s 𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ 𝑁 = (norm‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Mnd ∧ 0 ∈ 𝐴 ∧ 𝐴 ⊆ 𝐵) → (𝑁 ↾ 𝐴) = (norm‘𝐻))
Theorem	abvpropd2 33198	Weaker version of abvpropd 20907. (Contributed by Thierry Arnoux, 8-Nov-2017.)
⊢ (𝜑 → (Base‘𝐾) = (Base‘𝐿))    &   ⊢ (𝜑 → (+g‘𝐾) = (+g‘𝐿))    &   ⊢ (𝜑 → (.r‘𝐾) = (.r‘𝐿))    ⇒   ⊢ (𝜑 → (AbsVal‘𝐾) = (AbsVal‘𝐿))
21.3.9.2  Posets
Theorem	ressprs 33199	The restriction of a proset is a proset. (Contributed by Thierry Arnoux, 11-Sep-2015.)
⊢ 𝐵 = (Base‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵) → (𝐾 ↾s 𝐴) ∈ Proset )
Theorem	posrasymb 33200	A poset ordering is asymmetric. (Contributed by Thierry Arnoux, 13-Sep-2018.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵))    ⇒   ⊢ ((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑋) ↔ 𝑋 = 𝑌))