P. 330 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 32901-33000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	prodpr 32901*	A product over a pair is the product of the elements. (Contributed by Thierry Arnoux, 1-Jan-2022.)
⊢ (𝑘 = 𝐴 → 𝐷 = 𝐸)    &   ⊢ (𝑘 = 𝐵 → 𝐷 = 𝐹)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐸 ∈ ℂ)    &   ⊢ (𝜑 → 𝐹 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    ⇒   ⊢ (𝜑 → ∏𝑘 ∈ {𝐴, 𝐵}𝐷 = (𝐸 · 𝐹))
Theorem	prodtp 32902*	A product over a triple is the product of the elements. (Contributed by Thierry Arnoux, 1-Jan-2022.)
⊢ (𝑘 = 𝐴 → 𝐷 = 𝐸)    &   ⊢ (𝑘 = 𝐵 → 𝐷 = 𝐹)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐸 ∈ ℂ)    &   ⊢ (𝜑 → 𝐹 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ (𝑘 = 𝐶 → 𝐷 = 𝐺)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐺 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐶)    &   ⊢ (𝜑 → 𝐵 ≠ 𝐶)    ⇒   ⊢ (𝜑 → ∏𝑘 ∈ {𝐴, 𝐵, 𝐶}𝐷 = ((𝐸 · 𝐹) · 𝐺))
Theorem	fsumub 32903*	An upper bound for a term of a positive finite sum. (Contributed by Thierry Arnoux, 27-Dec-2021.)
⊢ (𝑘 = 𝐾 → 𝐵 = 𝐷)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 = 𝐶)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐾 ∈ 𝐴)    ⇒   ⊢ (𝜑 → 𝐷 ≤ 𝐶)
Theorem	fsumiunle 32904*	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 32905	Split the hundreds from a decimal value. (Contributed by Thierry Arnoux, 25-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℝ    ⇒   ⊢ ;;𝐴𝐵𝐶 = ((;;100 · 𝐴) + ;𝐵𝐶)
21.3.6  Real and complex functions
21.3.6.1  Signum (sgn or sign) function - misc. additions
Theorem	sgncl 32906	Closure of the signum. (Contributed by Thierry Arnoux, 28-Sep-2018.)
⊢ (𝐴 ∈ ℝ* → (sgn‘𝐴) ∈ {-1, 0, 1})
Theorem	sgnclre 32907	Closure of the signum. (Contributed by Thierry Arnoux, 28-Sep-2018.)
⊢ (𝐴 ∈ ℝ → (sgn‘𝐴) ∈ ℝ)
Theorem	sgnneg 32908	Negation of the signum. (Contributed by Thierry Arnoux, 1-Oct-2018.)
⊢ (𝐴 ∈ ℝ → (sgn‘-𝐴) = -(sgn‘𝐴))
Theorem	sgn3da 32909	A conditional containing a signum is true if it is true in all three possible cases. (Contributed by Thierry Arnoux, 1-Oct-2018.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ ((sgn‘𝐴) = 0 → (𝜓 ↔ 𝜒))    &   ⊢ ((sgn‘𝐴) = 1 → (𝜓 ↔ 𝜃))    &   ⊢ ((sgn‘𝐴) = -1 → (𝜓 ↔ 𝜏))    &   ⊢ ((𝜑 ∧ 𝐴 = 0) → 𝜒)    &   ⊢ ((𝜑 ∧ 0 < 𝐴) → 𝜃)    &   ⊢ ((𝜑 ∧ 𝐴 < 0) → 𝜏)    ⇒   ⊢ (𝜑 → 𝜓)
Theorem	sgnmul 32910	Signum of a product. (Contributed by Thierry Arnoux, 2-Oct-2018.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (sgn‘(𝐴 · 𝐵)) = ((sgn‘𝐴) · (sgn‘𝐵)))
Theorem	sgnmulrp2 32911	Multiplication by a positive number does not affect signum. (Contributed by Thierry Arnoux, 2-Oct-2018.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → (sgn‘(𝐴 · 𝐵)) = (sgn‘𝐴))
Theorem	sgnsub 32912	Subtraction of a number of opposite sign. (Contributed by Thierry Arnoux, 2-Oct-2018.)
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 · 𝐵) < 0) → (sgn‘(𝐴 − 𝐵)) = (sgn‘𝐴))
Theorem	sgnnbi 32913	Negative signum. (Contributed by Thierry Arnoux, 2-Oct-2018.)
⊢ (𝐴 ∈ ℝ* → ((sgn‘𝐴) = -1 ↔ 𝐴 < 0))
Theorem	sgnpbi 32914	Positive signum. (Contributed by Thierry Arnoux, 2-Oct-2018.)
⊢ (𝐴 ∈ ℝ* → ((sgn‘𝐴) = 1 ↔ 0 < 𝐴))
Theorem	sgn0bi 32915	Zero signum. (Contributed by Thierry Arnoux, 10-Oct-2018.)
⊢ (𝐴 ∈ ℝ* → ((sgn‘𝐴) = 0 ↔ 𝐴 = 0))
Theorem	sgnsgn 32916	Signum is idempotent. (Contributed by Thierry Arnoux, 2-Oct-2018.)
⊢ (𝐴 ∈ ℝ* → (sgn‘(sgn‘𝐴)) = (sgn‘𝐴))
Theorem	sgnmulsgn 32917	If two real numbers are of different signs, so are their signs. (Contributed by Thierry Arnoux, 12-Oct-2018.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 · 𝐵) < 0 ↔ ((sgn‘𝐴) · (sgn‘𝐵)) < 0))
Theorem	sgnmulsgp 32918	If two real numbers are of same signs, so are their signs. (Contributed by Thierry Arnoux, 12-Oct-2018.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (0 < (𝐴 · 𝐵) ↔ 0 < ((sgn‘𝐴) · (sgn‘𝐵))))
21.3.6.2  Integer powers - misc. additions
Theorem	nexple 32919	A lower bound for an exponentiation. (Contributed by Thierry Arnoux, 19-Aug-2017.)
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℝ ∧ 2 ≤ 𝐵) → 𝐴 ≤ (𝐵↑𝐴))
Theorem	2exple2exp 32920*	If a nonnegative integer 𝑋 is a multiple of a power of two, but less than the next power of two, it is itself a power of two. (Contributed by Thierry Arnoux, 19-Oct-2025.)
⊢ (𝜑 → 𝑋 ∈ ℕ)    &   ⊢ (𝜑 → 𝐾 ∈ ℕ0)    &   ⊢ (𝜑 → (2↑𝐾) ∥ 𝑋)    &   ⊢ (𝜑 → 𝑋 ≤ (2↑(𝐾 + 1)))    ⇒   ⊢ (𝜑 → ∃𝑛 ∈ ℕ0 𝑋 = (2↑𝑛))
Theorem	expevenpos 32921	Even powers are positive. (Contributed by Thierry Arnoux, 9-Nov-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 2 ∥ 𝑁)    ⇒   ⊢ (𝜑 → 0 ≤ (𝐴↑𝑁))
Theorem	oexpled 32922	Odd power monomials are monotonic. (Contributed by Thierry Arnoux, 9-Nov-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → ¬ 2 ∥ 𝑁)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    ⇒   ⊢ (𝜑 → (𝐴↑𝑁) ≤ (𝐵↑𝑁))
21.3.6.3  Indicator Functions (continued)
Theorem	indsumin 32923*	Finite sum of a product with the indicator function / Cartesian product with the indicator function. (Contributed by Thierry Arnoux, 11-Dec-2021.)
⊢ (𝜑 → 𝑂 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑂)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝑂)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ ℂ)    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 ((((𝟭‘𝑂)‘𝐵)‘𝑘) · 𝐶) = Σ𝑘 ∈ (𝐴 ∩ 𝐵)𝐶)
Theorem	prodindf 32924*	The product of indicators is one if and only if all values are in the set. (Contributed by Thierry Arnoux, 11-Dec-2021.)
⊢ (𝜑 → 𝑂 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝑂)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝑂)    ⇒   ⊢ (𝜑 → ∏𝑘 ∈ 𝐴 (((𝟭‘𝑂)‘𝐵)‘(𝐹‘𝑘)) = if(ran 𝐹 ⊆ 𝐵, 1, 0))
Theorem	indsn 32925*	The indicator function of a singleton. (Contributed by Thierry Arnoux, 15-Feb-2026.)
⊢ ((𝑂 ∈ 𝑉 ∧ 𝑋 ∈ 𝑂) → ((𝟭‘𝑂)‘{𝑋}) = (𝑥 ∈ 𝑂 ↦ if(𝑥 = 𝑋, 1, 0)))
Theorem	indf1o 32926	The bijection between a power set and the set of indicator functions. (Contributed by Thierry Arnoux, 14-Aug-2017.)
⊢ (𝑂 ∈ 𝑉 → (𝟭‘𝑂):𝒫 𝑂–1-1-onto→({0, 1} ↑m 𝑂))
Theorem	indpreima 32927	A function with range {0, 1} as an indicator of the preimage of {1}. (Contributed by Thierry Arnoux, 23-Aug-2017.)
⊢ ((𝑂 ∈ 𝑉 ∧ 𝐹:𝑂⟶{0, 1}) → 𝐹 = ((𝟭‘𝑂)‘(◡𝐹 “ {1})))
Theorem	indf1ofs 32928*	The bijection between finite subsets and the indicator functions with finite support. (Contributed by Thierry Arnoux, 22-Aug-2017.)
⊢ (𝑂 ∈ 𝑉 → ((𝟭‘𝑂) ↾ Fin):(𝒫 𝑂 ∩ Fin)–1-1-onto→{𝑓 ∈ ({0, 1} ↑m 𝑂) ∣ (◡𝑓 “ {1}) ∈ Fin})
Theorem	indsupp 32929	The support of the indicator function. (Contributed by Thierry Arnoux, 13-Oct-2025.)
⊢ ((𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂) → (((𝟭‘𝑂)‘𝐴) supp 0) = 𝐴)
Theorem	indfsd 32930	The indicator function of a finite set has finite support. (Contributed by Thierry Arnoux, 18-Jan-2026.)
⊢ (𝜑 → 𝑂 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑂)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    ⇒   ⊢ (𝜑 → ((𝟭‘𝑂)‘𝐴) finSupp 0)
Theorem	indfsid 32931	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 32932	Constant used for decimal fraction constructor. See df-dp2 32933.
class _𝐴𝐵
Definition	df-dp2 32933	Define the "decimal fraction constructor", which is used to build up "decimal fractions" in base 10. This is intentionally similar to df-dec 12647. (Contributed by David A. Wheeler, 15-May-2015.) (Revised by AV, 9-Sep-2021.)
⊢ _𝐴𝐵 = (𝐴 + (𝐵 / ;10))
Theorem	dp2eq1 32934	Equality theorem for the decimal expansion constructor. (Contributed by David A. Wheeler, 15-May-2015.)
⊢ (𝐴 = 𝐵 → _𝐴𝐶 = _𝐵𝐶)
Theorem	dp2eq2 32935	Equality theorem for the decimal expansion constructor. (Contributed by David A. Wheeler, 15-May-2015.)
⊢ (𝐴 = 𝐵 → _𝐶𝐴 = _𝐶𝐵)
Theorem	dp2eq1i 32936	Equality theorem for the decimal expansion constructor. (Contributed by David A. Wheeler, 15-May-2015.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ _𝐴𝐶 = _𝐵𝐶
Theorem	dp2eq2i 32937	Equality theorem for the decimal expansion constructor. (Contributed by David A. Wheeler, 15-May-2015.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ _𝐶𝐴 = _𝐶𝐵
Theorem	dp2eq12i 32938	Equality theorem for the decimal expansion constructor. (Contributed by David A. Wheeler, 15-May-2015.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ _𝐴𝐶 = _𝐵𝐷
Theorem	dp20u 32939	Add a zero in the tenths (lower) place. (Contributed by Thierry Arnoux, 16-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    ⇒   ⊢ _𝐴0 = 𝐴
Theorem	dp20h 32940	Add a zero in the unit places. (Contributed by Thierry Arnoux, 16-Dec-2021.)
⊢ 𝐴 ∈ ℝ+    ⇒   ⊢ _0𝐴 = (𝐴 / ;10)
Theorem	dp2cl 32941	Closure for the decimal fraction constructor if both values are reals. (Contributed by David A. Wheeler, 15-May-2015.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → _𝐴𝐵 ∈ ℝ)
Theorem	dp2clq 32942	Closure for a decimal fraction. (Contributed by Thierry Arnoux, 16-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℚ    ⇒   ⊢ _𝐴𝐵 ∈ ℚ
Theorem	rpdp2cl 32943	Closure for a decimal fraction in the positive real numbers. (Contributed by Thierry Arnoux, 16-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℝ+    ⇒   ⊢ _𝐴𝐵 ∈ ℝ+
Theorem	rpdp2cl2 32944	Closure for a decimal fraction with no decimal expansion in the positive real numbers. (Contributed by Thierry Arnoux, 25-Dec-2021.)
⊢ 𝐴 ∈ ℕ    ⇒   ⊢ _𝐴0 ∈ ℝ+
Theorem	dp2lt10 32945	Decimal fraction builds real numbers less than 10. (Contributed by Thierry Arnoux, 16-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℝ+    &   ⊢ 𝐴 < ;10    &   ⊢ 𝐵 < ;10    ⇒   ⊢ _𝐴𝐵 < ;10
Theorem	dp2lt 32946	Comparing two decimal fractions (equal unit places). (Contributed by Thierry Arnoux, 16-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℝ+    &   ⊢ 𝐶 ∈ ℝ+    &   ⊢ 𝐵 < 𝐶    ⇒   ⊢ _𝐴𝐵 < _𝐴𝐶
Theorem	dp2ltsuc 32947	Comparing a decimal fraction with the next integer. (Contributed by Thierry Arnoux, 25-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℝ+    &   ⊢ 𝐵 < ;10    &   ⊢ (𝐴 + 1) = 𝐶    ⇒   ⊢ _𝐴𝐵 < 𝐶
Theorem	dp2ltc 32948	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 32950 and df-dp2 32933 for more information; dpval2 32954 and dpfrac1 32953 provide a more convenient way to obtain a value. This is intentionally similar to df-dec 12647.
Syntax	cdp 32949	Decimal point operator. See df-dp 32950.
class .
Definition	df-dp 32950*	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 32951	Define the value of the decimal point operator. See df-dp 32950. (Contributed by David A. Wheeler, 15-May-2015.)
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℝ) → (𝐴.𝐵) = _𝐴𝐵)
Theorem	dpcl 32952	Prove that the closure of the decimal point is ℝ as we have defined it. See df-dp 32950. (Contributed by David A. Wheeler, 15-May-2015.)
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℝ) → (𝐴.𝐵) ∈ ℝ)
Theorem	dpfrac1 32953	Prove a simple equivalence involving the decimal point. See df-dp 32950 and dpcl 32952. (Contributed by David A. Wheeler, 15-May-2015.) (Revised by AV, 9-Sep-2021.)
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℝ) → (𝐴.𝐵) = (;𝐴𝐵 / ;10))
Theorem	dpval2 32954	Value of the decimal point construct. (Contributed by Thierry Arnoux, 16-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ (𝐴.𝐵) = (𝐴 + (𝐵 / ;10))
Theorem	dpval3 32955	Value of the decimal point construct. (Contributed by Thierry Arnoux, 16-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ (𝐴.𝐵) = _𝐴𝐵
Theorem	dpmul10 32956	Multiply by 10 a decimal expansion. (Contributed by Thierry Arnoux, 25-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ ((𝐴.𝐵) · ;10) = ;𝐴𝐵
Theorem	decdiv10 32957	Divide a decimal number by 10. (Contributed by Thierry Arnoux, 25-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ (;𝐴𝐵 / ;10) = (𝐴.𝐵)
Theorem	dpmul100 32958	Multiply by 100 a decimal expansion. (Contributed by Thierry Arnoux, 25-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℝ    ⇒   ⊢ ((𝐴._𝐵𝐶) · ;;100) = ;;𝐴𝐵𝐶
Theorem	dp3mul10 32959	Multiply by 10 a decimal expansion with 3 digits. (Contributed by Thierry Arnoux, 25-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℝ    ⇒   ⊢ ((𝐴._𝐵𝐶) · ;10) = (;𝐴𝐵.𝐶)
Theorem	dpmul1000 32960	Multiply by 1000 a decimal expansion. (Contributed by Thierry Arnoux, 25-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℝ    ⇒   ⊢ ((𝐴._𝐵_𝐶𝐷) · ;;;1000) = ;;;𝐴𝐵𝐶𝐷
Theorem	dpval3rp 32961	Value of the decimal point construct. (Contributed by Thierry Arnoux, 16-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℝ+    ⇒   ⊢ (𝐴.𝐵) = _𝐴𝐵
Theorem	dp0u 32962	Add a zero in the tenths place. (Contributed by Thierry Arnoux, 16-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    ⇒   ⊢ (𝐴.0) = 𝐴
Theorem	dp0h 32963	Remove a zero in the units places. (Contributed by Thierry Arnoux, 16-Dec-2021.)
⊢ 𝐴 ∈ ℝ+    ⇒   ⊢ (0.𝐴) = (𝐴 / ;10)
Theorem	rpdpcl 32964	Closure of the decimal point in the positive real numbers. (Contributed by Thierry Arnoux, 16-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℝ+    ⇒   ⊢ (𝐴.𝐵) ∈ ℝ+
Theorem	dplt 32965	Comparing two decimal expansions (equal higher places). (Contributed by Thierry Arnoux, 16-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℝ+    &   ⊢ 𝐶 ∈ ℝ+    &   ⊢ 𝐵 < 𝐶    ⇒   ⊢ (𝐴.𝐵) < (𝐴.𝐶)
Theorem	dplti 32966	Comparing a decimal expansions with the next higher integer. (Contributed by Thierry Arnoux, 16-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℝ+    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐵 < ;10    &   ⊢ (𝐴 + 1) = 𝐶    ⇒   ⊢ (𝐴.𝐵) < 𝐶
Theorem	dpgti 32967	Comparing a decimal expansions with the next lower integer. (Contributed by Thierry Arnoux, 16-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℝ+    ⇒   ⊢ 𝐴 < (𝐴.𝐵)
Theorem	dpltc 32968	Comparing two decimal integers (unequal higher places). (Contributed by Thierry Arnoux, 16-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℝ+    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℝ+    &   ⊢ 𝐴 < 𝐶    &   ⊢ 𝐵 < ;10    ⇒   ⊢ (𝐴.𝐵) < (𝐶.𝐷)
Theorem	dpexpp1 32969	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 32970	Multiply by 10 a decimal expansion which starts with a zero. (Contributed by Thierry Arnoux, 16-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℝ+    ⇒   ⊢ ((0._𝐴𝐵) · ;10) = (𝐴.𝐵)
Theorem	dpadd2 32971	Addition with one decimal, no carry. (Contributed by Thierry Arnoux, 29-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℝ+    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℝ+    &   ⊢ 𝐸 ∈ ℕ0    &   ⊢ 𝐹 ∈ ℝ+    &   ⊢ 𝐺 ∈ ℕ0    &   ⊢ 𝐻 ∈ ℕ0    &   ⊢ (𝐺 + 𝐻) = 𝐼    &   ⊢ ((𝐴.𝐵) + (𝐶.𝐷)) = (𝐸.𝐹)    ⇒   ⊢ ((𝐺._𝐴𝐵) + (𝐻._𝐶𝐷)) = (𝐼._𝐸𝐹)
Theorem	dpadd 32972	Addition with one decimal. (Contributed by Thierry Arnoux, 27-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℕ0    &   ⊢ 𝐸 ∈ ℕ0    &   ⊢ 𝐹 ∈ ℕ0    &   ⊢ (;𝐴𝐵 + ;𝐶𝐷) = ;𝐸𝐹    ⇒   ⊢ ((𝐴.𝐵) + (𝐶.𝐷)) = (𝐸.𝐹)
Theorem	dpadd3 32973	Addition with two decimals. (Contributed by Thierry Arnoux, 27-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℕ0    &   ⊢ 𝐸 ∈ ℕ0    &   ⊢ 𝐺 ∈ ℕ0    &   ⊢ 𝐹 ∈ ℕ0    &   ⊢ 𝐻 ∈ ℕ0    &   ⊢ 𝐼 ∈ ℕ0    &   ⊢ (;;𝐴𝐵𝐶 + ;;𝐷𝐸𝐹) = ;;𝐺𝐻𝐼    ⇒   ⊢ ((𝐴._𝐵𝐶) + (𝐷._𝐸𝐹)) = (𝐺._𝐻𝐼)
Theorem	dpmul 32974	Multiplication with one decimal point. (Contributed by Thierry Arnoux, 26-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℕ0    &   ⊢ 𝐸 ∈ ℕ0    &   ⊢ 𝐺 ∈ ℕ0    &   ⊢ 𝐽 ∈ ℕ0    &   ⊢ 𝐾 ∈ ℕ0    &   ⊢ (𝐴 · 𝐶) = 𝐹    &   ⊢ (𝐴 · 𝐷) = 𝑀    &   ⊢ (𝐵 · 𝐶) = 𝐿    &   ⊢ (𝐵 · 𝐷) = ;𝐸𝐾    &   ⊢ ((𝐿 + 𝑀) + 𝐸) = ;𝐺𝐽    &   ⊢ (𝐹 + 𝐺) = 𝐼    ⇒   ⊢ ((𝐴.𝐵) · (𝐶.𝐷)) = (𝐼._𝐽𝐾)
Theorem	dpmul4 32975	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 32976	Example theorem demonstrating decimal expansions. (Contributed by Thierry Arnoux, 27-Dec-2021.)
⊢ (3 / 2) = (1.5)
Theorem	1mhdrd 32977	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 32978	Extend class notation to include division of extended reals.
class /𝑒
Definition	df-xdiv 32979*	Define division over extended real numbers. (Contributed by Thierry Arnoux, 17-Dec-2016.)
⊢ /𝑒 = (𝑥 ∈ ℝ*, 𝑦 ∈ (ℝ ∖ {0}) ↦ (℩𝑧 ∈ ℝ* (𝑦 ·e 𝑧) = 𝑥))
Theorem	xdivval 32980*	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 32981*	Existence of reciprocal of nonzero real number. (Contributed by Thierry Arnoux, 17-Dec-2016.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) → ∃𝑥 ∈ ℝ (𝐴 ·e 𝑥) = 1)
Theorem	xmulcand 32982	Cancellation law for extended multiplication. (Contributed by Thierry Arnoux, 17-Dec-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ≠ 0)    ⇒   ⊢ (𝜑 → ((𝐶 ·e 𝐴) = (𝐶 ·e 𝐵) ↔ 𝐴 = 𝐵))
Theorem	xreceu 32983*	Existential uniqueness of reciprocals. Theorem I.8 of [Apostol] p. 18. (Contributed by Thierry Arnoux, 17-Dec-2016.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → ∃!𝑥 ∈ ℝ* (𝐵 ·e 𝑥) = 𝐴)
Theorem	xdivcld 32984	Closure law for the extended division. (Contributed by Thierry Arnoux, 15-Mar-2017.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    ⇒   ⊢ (𝜑 → (𝐴 /𝑒 𝐵) ∈ ℝ*)
Theorem	xdivcl 32985	Closure law for the extended division. (Contributed by Thierry Arnoux, 15-Mar-2017.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → (𝐴 /𝑒 𝐵) ∈ ℝ*)
Theorem	xdivmul 32986	Relationship between division and multiplication. (Contributed by Thierry Arnoux, 24-Dec-2016.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ (𝐶 ∈ ℝ ∧ 𝐶 ≠ 0)) → ((𝐴 /𝑒 𝐶) = 𝐵 ↔ (𝐶 ·e 𝐵) = 𝐴))
Theorem	rexdiv 32987	The extended real division operation when both arguments are real. (Contributed by Thierry Arnoux, 18-Dec-2016.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → (𝐴 /𝑒 𝐵) = (𝐴 / 𝐵))
Theorem	xdivrec 32988	Relationship between division and reciprocal. (Contributed by Thierry Arnoux, 5-Jul-2017.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → (𝐴 /𝑒 𝐵) = (𝐴 ·e (1 /𝑒 𝐵)))
Theorem	xdivid 32989	A number divided by itself is one. (Contributed by Thierry Arnoux, 18-Dec-2016.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) → (𝐴 /𝑒 𝐴) = 1)
Theorem	xdiv0 32990	Division into zero is zero. (Contributed by Thierry Arnoux, 18-Dec-2016.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) → (0 /𝑒 𝐴) = 0)
Theorem	xdiv0rp 32991	Division into zero is zero. (Contributed by Thierry Arnoux, 18-Dec-2016.)
⊢ (𝐴 ∈ ℝ+ → (0 /𝑒 𝐴) = 0)
Theorem	eliccioo 32992	Membership in a closed interval of extended reals versus the same open interval. (Contributed by Thierry Arnoux, 18-Dec-2016.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵) → (𝐶 ∈ (𝐴[,]𝐵) ↔ (𝐶 = 𝐴 ∨ 𝐶 ∈ (𝐴(,)𝐵) ∨ 𝐶 = 𝐵)))
Theorem	elxrge02 32993	Elementhood in the set of nonnegative extended reals. (Contributed by Thierry Arnoux, 18-Dec-2016.)
⊢ (𝐴 ∈ (0[,]+∞) ↔ (𝐴 = 0 ∨ 𝐴 ∈ ℝ+ ∨ 𝐴 = +∞))
Theorem	xdivpnfrp 32994	Plus infinity divided by a positive real number is plus infinity. (Contributed by Thierry Arnoux, 18-Dec-2016.)
⊢ (𝐴 ∈ ℝ+ → (+∞ /𝑒 𝐴) = +∞)
Theorem	rpxdivcld 32995	Closure law for extended division of positive reals. (Contributed by Thierry Arnoux, 18-Dec-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    ⇒   ⊢ (𝜑 → (𝐴 /𝑒 𝐵) ∈ ℝ+)
Theorem	xrpxdivcld 32996	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 32997	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 32998*	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 32999	A word has finite support. (Contributed by Thierry Arnoux, 27-May-2025.)
⊢ (𝜑 → 𝑍 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑊 ∈ Word 𝑆)    ⇒   ⊢ (𝜑 → 𝑊 finSupp 𝑍)
Theorem	wrdpmcl 33000	Closure of a word with permuted symbols. (Contributed by Thierry Arnoux, 27-May-2025.)
⊢ 𝐽 = (0..^(♯‘𝑊))    &   ⊢ (𝜑 → 𝐸:𝐽–1-1-onto→𝐽)    &   ⊢ (𝜑 → 𝑊 ∈ Word 𝑆)    ⇒   ⊢ (𝜑 → (𝑊 ∘ 𝐸) ∈ Word 𝑆)