P. 326 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 32501-32600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	fsumub 32501*	An upper bound for a term of a positive finite sum. (Contributed by Thierry Arnoux, 27-Dec-2021.)
⊢ (𝑘 = 𝐾 → 𝐵 = 𝐷)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 = 𝐶)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐾 ∈ 𝐴)    ⇒   ⊢ (𝜑 → 𝐷 ≤ 𝐶)
Theorem	fsumiunle 32502*	Upper bound for a sum of nonnegative terms over an indexed union. The inequality may be strict if the indexed union is non-disjoint, since in the right hand side, a summand may be counted several times. (Contributed by Thierry Arnoux, 1-Jan-2021.)
⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ Fin)    &   ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ ℝ)    &   ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑘 ∈ 𝐵) → 0 ≤ 𝐶)    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵𝐶 ≤ Σ𝑥 ∈ 𝐴 Σ𝑘 ∈ 𝐵 𝐶)
21.3.5.11  Decimal numbers
Theorem	dfdec100 32503	Split the hundreds from a decimal value. (Contributed by Thierry Arnoux, 25-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℝ    ⇒   ⊢ ;;𝐴𝐵𝐶 = ((;;100 · 𝐴) + ;𝐵𝐶)
21.3.6  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 32504	Constant used for decimal fraction constructor. See df-dp2 32505.
class _𝐴𝐵
Definition	df-dp2 32505	Define the "decimal fraction constructor", which is used to build up "decimal fractions" in base 10. This is intentionally similar to df-dec 12675. (Contributed by David A. Wheeler, 15-May-2015.) (Revised by AV, 9-Sep-2021.)
⊢ _𝐴𝐵 = (𝐴 + (𝐵 / ;10))
Theorem	dp2eq1 32506	Equality theorem for the decimal expansion constructor. (Contributed by David A. Wheeler, 15-May-2015.)
⊢ (𝐴 = 𝐵 → _𝐴𝐶 = _𝐵𝐶)
Theorem	dp2eq2 32507	Equality theorem for the decimal expansion constructor. (Contributed by David A. Wheeler, 15-May-2015.)
⊢ (𝐴 = 𝐵 → _𝐶𝐴 = _𝐶𝐵)
Theorem	dp2eq1i 32508	Equality theorem for the decimal expansion constructor. (Contributed by David A. Wheeler, 15-May-2015.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ _𝐴𝐶 = _𝐵𝐶
Theorem	dp2eq2i 32509	Equality theorem for the decimal expansion constructor. (Contributed by David A. Wheeler, 15-May-2015.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ _𝐶𝐴 = _𝐶𝐵
Theorem	dp2eq12i 32510	Equality theorem for the decimal expansion constructor. (Contributed by David A. Wheeler, 15-May-2015.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ _𝐴𝐶 = _𝐵𝐷
Theorem	dp20u 32511	Add a zero in the tenths (lower) place. (Contributed by Thierry Arnoux, 16-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    ⇒   ⊢ _𝐴0 = 𝐴
Theorem	dp20h 32512	Add a zero in the unit places. (Contributed by Thierry Arnoux, 16-Dec-2021.)
⊢ 𝐴 ∈ ℝ+    ⇒   ⊢ _0𝐴 = (𝐴 / ;10)
Theorem	dp2cl 32513	Closure for the decimal fraction constructor if both values are reals. (Contributed by David A. Wheeler, 15-May-2015.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → _𝐴𝐵 ∈ ℝ)
Theorem	dp2clq 32514	Closure for a decimal fraction. (Contributed by Thierry Arnoux, 16-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℚ    ⇒   ⊢ _𝐴𝐵 ∈ ℚ
Theorem	rpdp2cl 32515	Closure for a decimal fraction in the positive real numbers. (Contributed by Thierry Arnoux, 16-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℝ+    ⇒   ⊢ _𝐴𝐵 ∈ ℝ+
Theorem	rpdp2cl2 32516	Closure for a decimal fraction with no decimal expansion in the positive real numbers. (Contributed by Thierry Arnoux, 25-Dec-2021.)
⊢ 𝐴 ∈ ℕ    ⇒   ⊢ _𝐴0 ∈ ℝ+
Theorem	dp2lt10 32517	Decimal fraction builds real numbers less than 10. (Contributed by Thierry Arnoux, 16-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℝ+    &   ⊢ 𝐴 < ;10    &   ⊢ 𝐵 < ;10    ⇒   ⊢ _𝐴𝐵 < ;10
Theorem	dp2lt 32518	Comparing two decimal fractions (equal unit places). (Contributed by Thierry Arnoux, 16-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℝ+    &   ⊢ 𝐶 ∈ ℝ+    &   ⊢ 𝐵 < 𝐶    ⇒   ⊢ _𝐴𝐵 < _𝐴𝐶
Theorem	dp2ltsuc 32519	Comparing a decimal fraction with the next integer. (Contributed by Thierry Arnoux, 25-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℝ+    &   ⊢ 𝐵 < ;10    &   ⊢ (𝐴 + 1) = 𝐶    ⇒   ⊢ _𝐴𝐵 < 𝐶
Theorem	dp2ltc 32520	Comparing two decimal expansions (unequal higher places). (Contributed by Thierry Arnoux, 16-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℝ+    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℝ+    &   ⊢ 𝐵 < ;10    &   ⊢ 𝐴 < 𝐶    ⇒   ⊢ _𝐴𝐵 < _𝐶𝐷
21.3.6.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 32522 and df-dp2 32505 for more information; dpval2 32526 and dpfrac1 32525 provide a more convenient way to obtain a value. This is intentionally similar to df-dec 12675.
Syntax	cdp 32521	Decimal point operator. See df-dp 32522.
class .
Definition	df-dp 32522*	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 32523	Define the value of the decimal point operator. See df-dp 32522. (Contributed by David A. Wheeler, 15-May-2015.)
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℝ) → (𝐴.𝐵) = _𝐴𝐵)
Theorem	dpcl 32524	Prove that the closure of the decimal point is ℝ as we have defined it. See df-dp 32522. (Contributed by David A. Wheeler, 15-May-2015.)
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℝ) → (𝐴.𝐵) ∈ ℝ)
Theorem	dpfrac1 32525	Prove a simple equivalence involving the decimal point. See df-dp 32522 and dpcl 32524. (Contributed by David A. Wheeler, 15-May-2015.) (Revised by AV, 9-Sep-2021.)
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℝ) → (𝐴.𝐵) = (;𝐴𝐵 / ;10))
Theorem	dpval2 32526	Value of the decimal point construct. (Contributed by Thierry Arnoux, 16-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ (𝐴.𝐵) = (𝐴 + (𝐵 / ;10))
Theorem	dpval3 32527	Value of the decimal point construct. (Contributed by Thierry Arnoux, 16-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ (𝐴.𝐵) = _𝐴𝐵
Theorem	dpmul10 32528	Multiply by 10 a decimal expansion. (Contributed by Thierry Arnoux, 25-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ ((𝐴.𝐵) · ;10) = ;𝐴𝐵
Theorem	decdiv10 32529	Divide a decimal number by 10. (Contributed by Thierry Arnoux, 25-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ (;𝐴𝐵 / ;10) = (𝐴.𝐵)
Theorem	dpmul100 32530	Multiply by 100 a decimal expansion. (Contributed by Thierry Arnoux, 25-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℝ    ⇒   ⊢ ((𝐴._𝐵𝐶) · ;;100) = ;;𝐴𝐵𝐶
Theorem	dp3mul10 32531	Multiply by 10 a decimal expansion with 3 digits. (Contributed by Thierry Arnoux, 25-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℝ    ⇒   ⊢ ((𝐴._𝐵𝐶) · ;10) = (;𝐴𝐵.𝐶)
Theorem	dpmul1000 32532	Multiply by 1000 a decimal expansion. (Contributed by Thierry Arnoux, 25-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℝ    ⇒   ⊢ ((𝐴._𝐵_𝐶𝐷) · ;;;1000) = ;;;𝐴𝐵𝐶𝐷
Theorem	dpval3rp 32533	Value of the decimal point construct. (Contributed by Thierry Arnoux, 16-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℝ+    ⇒   ⊢ (𝐴.𝐵) = _𝐴𝐵
Theorem	dp0u 32534	Add a zero in the tenths place. (Contributed by Thierry Arnoux, 16-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    ⇒   ⊢ (𝐴.0) = 𝐴
Theorem	dp0h 32535	Remove a zero in the units places. (Contributed by Thierry Arnoux, 16-Dec-2021.)
⊢ 𝐴 ∈ ℝ+    ⇒   ⊢ (0.𝐴) = (𝐴 / ;10)
Theorem	rpdpcl 32536	Closure of the decimal point in the positive real numbers. (Contributed by Thierry Arnoux, 16-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℝ+    ⇒   ⊢ (𝐴.𝐵) ∈ ℝ+
Theorem	dplt 32537	Comparing two decimal expansions (equal higher places). (Contributed by Thierry Arnoux, 16-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℝ+    &   ⊢ 𝐶 ∈ ℝ+    &   ⊢ 𝐵 < 𝐶    ⇒   ⊢ (𝐴.𝐵) < (𝐴.𝐶)
Theorem	dplti 32538	Comparing a decimal expansions with the next higher integer. (Contributed by Thierry Arnoux, 16-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℝ+    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐵 < ;10    &   ⊢ (𝐴 + 1) = 𝐶    ⇒   ⊢ (𝐴.𝐵) < 𝐶
Theorem	dpgti 32539	Comparing a decimal expansions with the next lower integer. (Contributed by Thierry Arnoux, 16-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℝ+    ⇒   ⊢ 𝐴 < (𝐴.𝐵)
Theorem	dpltc 32540	Comparing two decimal integers (unequal higher places). (Contributed by Thierry Arnoux, 16-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℝ+    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℝ+    &   ⊢ 𝐴 < 𝐶    &   ⊢ 𝐵 < ;10    ⇒   ⊢ (𝐴.𝐵) < (𝐶.𝐷)
Theorem	dpexpp1 32541	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 32542	Multiply by 10 a decimal expansion which starts with a zero. (Contributed by Thierry Arnoux, 16-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℝ+    ⇒   ⊢ ((0._𝐴𝐵) · ;10) = (𝐴.𝐵)
Theorem	dpadd2 32543	Addition with one decimal, no carry. (Contributed by Thierry Arnoux, 29-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℝ+    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℝ+    &   ⊢ 𝐸 ∈ ℕ0    &   ⊢ 𝐹 ∈ ℝ+    &   ⊢ 𝐺 ∈ ℕ0    &   ⊢ 𝐻 ∈ ℕ0    &   ⊢ (𝐺 + 𝐻) = 𝐼    &   ⊢ ((𝐴.𝐵) + (𝐶.𝐷)) = (𝐸.𝐹)    ⇒   ⊢ ((𝐺._𝐴𝐵) + (𝐻._𝐶𝐷)) = (𝐼._𝐸𝐹)
Theorem	dpadd 32544	Addition with one decimal. (Contributed by Thierry Arnoux, 27-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℕ0    &   ⊢ 𝐸 ∈ ℕ0    &   ⊢ 𝐹 ∈ ℕ0    &   ⊢ (;𝐴𝐵 + ;𝐶𝐷) = ;𝐸𝐹    ⇒   ⊢ ((𝐴.𝐵) + (𝐶.𝐷)) = (𝐸.𝐹)
Theorem	dpadd3 32545	Addition with two decimals. (Contributed by Thierry Arnoux, 27-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℕ0    &   ⊢ 𝐸 ∈ ℕ0    &   ⊢ 𝐺 ∈ ℕ0    &   ⊢ 𝐹 ∈ ℕ0    &   ⊢ 𝐻 ∈ ℕ0    &   ⊢ 𝐼 ∈ ℕ0    &   ⊢ (;;𝐴𝐵𝐶 + ;;𝐷𝐸𝐹) = ;;𝐺𝐻𝐼    ⇒   ⊢ ((𝐴._𝐵𝐶) + (𝐷._𝐸𝐹)) = (𝐺._𝐻𝐼)
Theorem	dpmul 32546	Multiplication with one decimal point. (Contributed by Thierry Arnoux, 26-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℕ0    &   ⊢ 𝐸 ∈ ℕ0    &   ⊢ 𝐺 ∈ ℕ0    &   ⊢ 𝐽 ∈ ℕ0    &   ⊢ 𝐾 ∈ ℕ0    &   ⊢ (𝐴 · 𝐶) = 𝐹    &   ⊢ (𝐴 · 𝐷) = 𝑀    &   ⊢ (𝐵 · 𝐶) = 𝐿    &   ⊢ (𝐵 · 𝐷) = ;𝐸𝐾    &   ⊢ ((𝐿 + 𝑀) + 𝐸) = ;𝐺𝐽    &   ⊢ (𝐹 + 𝐺) = 𝐼    ⇒   ⊢ ((𝐴.𝐵) · (𝐶.𝐷)) = (𝐼._𝐽𝐾)
Theorem	dpmul4 32547	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 32548	Example theorem demonstrating decimal expansions. (Contributed by Thierry Arnoux, 27-Dec-2021.)
⊢ (3 / 2) = (1.5)
Theorem	1mhdrd 32549	Example theorem demonstrating decimal expansions. (Contributed by Thierry Arnoux, 27-Dec-2021.)
⊢ ((0._99) + (0._01)) = 1
21.3.6.2  Division in the extended real number system
Syntax	cxdiv 32550	Extend class notation to include division of extended reals.
class /𝑒
Definition	df-xdiv 32551*	Define division over extended real numbers. (Contributed by Thierry Arnoux, 17-Dec-2016.)
⊢ /𝑒 = (𝑥 ∈ ℝ*, 𝑦 ∈ (ℝ ∖ {0}) ↦ (℩𝑧 ∈ ℝ* (𝑦 ·e 𝑧) = 𝑥))
Theorem	xdivval 32552*	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 32553*	Existence of reciprocal of nonzero real number. (Contributed by Thierry Arnoux, 17-Dec-2016.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) → ∃𝑥 ∈ ℝ (𝐴 ·e 𝑥) = 1)
Theorem	xmulcand 32554	Cancellation law for extended multiplication. (Contributed by Thierry Arnoux, 17-Dec-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ≠ 0)    ⇒   ⊢ (𝜑 → ((𝐶 ·e 𝐴) = (𝐶 ·e 𝐵) ↔ 𝐴 = 𝐵))
Theorem	xreceu 32555*	Existential uniqueness of reciprocals. Theorem I.8 of [Apostol] p. 18. (Contributed by Thierry Arnoux, 17-Dec-2016.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → ∃!𝑥 ∈ ℝ* (𝐵 ·e 𝑥) = 𝐴)
Theorem	xdivcld 32556	Closure law for the extended division. (Contributed by Thierry Arnoux, 15-Mar-2017.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    ⇒   ⊢ (𝜑 → (𝐴 /𝑒 𝐵) ∈ ℝ*)
Theorem	xdivcl 32557	Closure law for the extended division. (Contributed by Thierry Arnoux, 15-Mar-2017.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → (𝐴 /𝑒 𝐵) ∈ ℝ*)
Theorem	xdivmul 32558	Relationship between division and multiplication. (Contributed by Thierry Arnoux, 24-Dec-2016.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ (𝐶 ∈ ℝ ∧ 𝐶 ≠ 0)) → ((𝐴 /𝑒 𝐶) = 𝐵 ↔ (𝐶 ·e 𝐵) = 𝐴))
Theorem	rexdiv 32559	The extended real division operation when both arguments are real. (Contributed by Thierry Arnoux, 18-Dec-2016.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → (𝐴 /𝑒 𝐵) = (𝐴 / 𝐵))
Theorem	xdivrec 32560	Relationship between division and reciprocal. (Contributed by Thierry Arnoux, 5-Jul-2017.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → (𝐴 /𝑒 𝐵) = (𝐴 ·e (1 /𝑒 𝐵)))
Theorem	xdivid 32561	A number divided by itself is one. (Contributed by Thierry Arnoux, 18-Dec-2016.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) → (𝐴 /𝑒 𝐴) = 1)
Theorem	xdiv0 32562	Division into zero is zero. (Contributed by Thierry Arnoux, 18-Dec-2016.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) → (0 /𝑒 𝐴) = 0)
Theorem	xdiv0rp 32563	Division into zero is zero. (Contributed by Thierry Arnoux, 18-Dec-2016.)
⊢ (𝐴 ∈ ℝ+ → (0 /𝑒 𝐴) = 0)
Theorem	eliccioo 32564	Membership in a closed interval of extended reals versus the same open interval. (Contributed by Thierry Arnoux, 18-Dec-2016.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵) → (𝐶 ∈ (𝐴[,]𝐵) ↔ (𝐶 = 𝐴 ∨ 𝐶 ∈ (𝐴(,)𝐵) ∨ 𝐶 = 𝐵)))
Theorem	elxrge02 32565	Elementhood in the set of nonnegative extended reals. (Contributed by Thierry Arnoux, 18-Dec-2016.)
⊢ (𝐴 ∈ (0[,]+∞) ↔ (𝐴 = 0 ∨ 𝐴 ∈ ℝ+ ∨ 𝐴 = +∞))
Theorem	xdivpnfrp 32566	Plus infinity divided by a positive real number is plus infinity. (Contributed by Thierry Arnoux, 18-Dec-2016.)
⊢ (𝐴 ∈ ℝ+ → (+∞ /𝑒 𝐴) = +∞)
Theorem	rpxdivcld 32567	Closure law for extended division of positive reals. (Contributed by Thierry Arnoux, 18-Dec-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    ⇒   ⊢ (𝜑 → (𝐴 /𝑒 𝐵) ∈ ℝ+)
Theorem	xrpxdivcld 32568	Closure law for extended division of positive extended reals. (Contributed by Thierry Arnoux, 18-Dec-2016.)
⊢ (𝜑 → 𝐴 ∈ (0[,]+∞))    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    ⇒   ⊢ (𝜑 → (𝐴 /𝑒 𝐵) ∈ (0[,]+∞))
21.3.7  Words over a set - misc additions
Theorem	wrdfd 32569	A word is a zero-based sequence with a recoverable upper limit, deduction version. (Contributed by Thierry Arnoux, 22-Dec-2021.)
⊢ (𝜑 → 𝑁 = (♯‘𝑊))    &   ⊢ (𝜑 → 𝑊 ∈ Word 𝑆)    ⇒   ⊢ (𝜑 → 𝑊:(0..^𝑁)⟶𝑆)
Theorem	wrdres 32570	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 32571*	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	pfx1s2 32572	The prefix of length 1 of a length 2 word. (Contributed by Thierry Arnoux, 19-Sep-2023.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (⟨“𝐴𝐵”⟩ prefix 1) = ⟨“𝐴”⟩)
Theorem	pfxrn2 32573	The range of a prefix of a word is a subset of the range of that word. Stronger version of pfxrn 14632. (Contributed by Thierry Arnoux, 12-Dec-2023.)
⊢ ((𝑊 ∈ Word 𝑆 ∧ 𝐿 ∈ (0...(♯‘𝑊))) → ran (𝑊 prefix 𝐿) ⊆ ran 𝑊)
Theorem	pfxrn3 32574	Express the range of a prefix of a word. Stronger version of pfxrn2 32573. (Contributed by Thierry Arnoux, 13-Dec-2023.)
⊢ ((𝑊 ∈ Word 𝑆 ∧ 𝐿 ∈ (0...(♯‘𝑊))) → ran (𝑊 prefix 𝐿) = (𝑊 “ (0..^𝐿)))
Theorem	pfxf1 32575	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 32576	Conditions for a length 1 string to be a one-to-one function. (Contributed by Thierry Arnoux, 11-Dec-2023.)
⊢ (𝜑 → 𝐼 ∈ 𝐷)    ⇒   ⊢ (𝜑 → ⟨“𝐼”⟩:dom ⟨“𝐼”⟩–1-1→𝐷)
Theorem	s2rn 32577	Range of a length 2 string. (Contributed by Thierry Arnoux, 19-Sep-2023.)
⊢ (𝜑 → 𝐼 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐽 ∈ 𝐷)    ⇒   ⊢ (𝜑 → ran ⟨“𝐼𝐽”⟩ = {𝐼, 𝐽})
Theorem	s2f1 32578	Conditions for a length 2 string to be a one-to-one function. (Contributed by Thierry Arnoux, 19-Sep-2023.)
⊢ (𝜑 → 𝐼 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐽 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐼 ≠ 𝐽)    ⇒   ⊢ (𝜑 → ⟨“𝐼𝐽”⟩:dom ⟨“𝐼𝐽”⟩–1-1→𝐷)
Theorem	s3rn 32579	Range of a length 3 string. (Contributed by Thierry Arnoux, 19-Sep-2023.)
⊢ (𝜑 → 𝐼 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐽 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐾 ∈ 𝐷)    ⇒   ⊢ (𝜑 → ran ⟨“𝐼𝐽𝐾”⟩ = {𝐼, 𝐽, 𝐾})
Theorem	s3f1 32580	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 32581	Closure of the words of length 3 in a preimage using the hash function. (Contributed by Thierry Arnoux, 27-Sep-2023.)
⊢ ⟨“𝐼𝐽𝐾”⟩ ∈ (◡♯ “ {3})
Theorem	ccatf1 32582	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 32583	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	wrdt2ind 32584*	Perform an induction over the structure of a word of even length. (Contributed by Thierry Arnoux, 26-Sep-2023.)
⊢ (𝑥 = ∅ → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑥 = (𝑦 ++ ⟨“𝑖𝑗”⟩) → (𝜑 ↔ 𝜃))    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏))    &   ⊢ 𝜓    &   ⊢ ((𝑦 ∈ Word 𝐵 ∧ 𝑖 ∈ 𝐵 ∧ 𝑗 ∈ 𝐵) → (𝜒 → 𝜃))    ⇒   ⊢ ((𝐴 ∈ Word 𝐵 ∧ 2 ∥ (♯‘𝐴)) → 𝜏)
Theorem	swrdrn2 32585	The range of a subword is a subset of the range of that word. Stronger version of swrdrn 14599. (Contributed by Thierry Arnoux, 12-Dec-2023.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) → ran (𝑊 substr ⟨𝑀, 𝑁⟩) ⊆ ran 𝑊)
Theorem	swrdrn3 32586	Express the range of a subword. Stronger version of swrdrn2 32585. (Contributed by Thierry Arnoux, 13-Dec-2023.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) → ran (𝑊 substr ⟨𝑀, 𝑁⟩) = (𝑊 “ (𝑀..^𝑁)))
Theorem	swrdf1 32587	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 32588	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.7.1  Splicing words (substring replacement)
Theorem	splfv3 32589	Symbols to the right of a splice are unaffected. (Contributed by Thierry Arnoux, 14-Dec-2023.)
⊢ (𝜑 → 𝑆 ∈ Word 𝐴)    &   ⊢ (𝜑 → 𝐹 ∈ (0...𝑇))    &   ⊢ (𝜑 → 𝑇 ∈ (0...(♯‘𝑆)))    &   ⊢ (𝜑 → 𝑅 ∈ Word 𝐴)    &   ⊢ (𝜑 → 𝑋 ∈ (0..^((♯‘𝑆) − 𝑇)))    &   ⊢ (𝜑 → 𝐾 = (𝐹 + (♯‘𝑅)))    ⇒   ⊢ (𝜑 → ((𝑆 splice ⟨𝐹, 𝑇, 𝑅⟩)‘(𝑋 + 𝐾)) = (𝑆‘(𝑋 + 𝑇)))
21.3.7.2  Cyclic shift of words
Theorem	1cshid 32590	Cyclically shifting a single letter word keeps it unchanged. (Contributed by Thierry Arnoux, 21-Nov-2023.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ∧ (♯‘𝑊) = 1) → (𝑊 cyclShift 𝑁) = 𝑊)
Theorem	cshw1s2 32591	Cyclically shifting a length 2 word swaps its symbols. (Contributed by Thierry Arnoux, 19-Sep-2023.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (⟨“𝐴𝐵”⟩ cyclShift 1) = ⟨“𝐵𝐴”⟩)
Theorem	cshwrnid 32592	Cyclically shifting a word preserves its range. (Contributed by Thierry Arnoux, 19-Sep-2023.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ) → ran (𝑊 cyclShift 𝑁) = ran 𝑊)
Theorem	cshf1o 32593	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.8  Extensible Structures
21.3.8.1  Structure restriction operator
Theorem	ressplusf 32594	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 32595	The norm in a restricted structure. (Contributed by Thierry Arnoux, 8-Oct-2017.)
⊢ 𝐻 = (𝐺 ↾s 𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ 𝑁 = (norm‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Mnd ∧ 0 ∈ 𝐴 ∧ 𝐴 ⊆ 𝐵) → (𝑁 ↾ 𝐴) = (norm‘𝐻))
Theorem	abvpropd2 32596	Weaker version of abvpropd 20675. (Contributed by Thierry Arnoux, 8-Nov-2017.)
⊢ (𝜑 → (Base‘𝐾) = (Base‘𝐿))    &   ⊢ (𝜑 → (+g‘𝐾) = (+g‘𝐿))    &   ⊢ (𝜑 → (.r‘𝐾) = (.r‘𝐿))    ⇒   ⊢ (𝜑 → (AbsVal‘𝐾) = (AbsVal‘𝐿))
21.3.8.2  The opposite group
Theorem	oppgle 32597	less-than relation of an opposite group. (Contributed by Thierry Arnoux, 13-Apr-2018.)
⊢ 𝑂 = (oppg‘𝑅)    &   ⊢ ≤ = (le‘𝑅)    ⇒   ⊢ ≤ = (le‘𝑂)
Theorem	oppgleOLD 32598	Obsolete version of oppgle 32597 as of 27-Oct-2024. less-than relation of an opposite group. (Contributed by Thierry Arnoux, 13-Apr-2018.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝑂 = (oppg‘𝑅)    &   ⊢ ≤ = (le‘𝑅)    ⇒   ⊢ ≤ = (le‘𝑂)
Theorem	oppglt 32599	less-than relation of an opposite group. (Contributed by Thierry Arnoux, 13-Apr-2018.)
⊢ 𝑂 = (oppg‘𝑅)    &   ⊢ < = (lt‘𝑅)    ⇒   ⊢ (𝑅 ∈ 𝑉 → < = (lt‘𝑂))
21.3.8.3  Posets
Theorem	ressprs 32600	The restriction of a proset is a proset. (Contributed by Thierry Arnoux, 11-Sep-2015.)
⊢ 𝐵 = (Base‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵) → (𝐾 ↾s 𝐴) ∈ Proset )