P. 329 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 32801-32900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	fsumub 32801*	An upper bound for a term of a positive finite sum. (Contributed by Thierry Arnoux, 27-Dec-2021.)
⊢ (𝑘 = 𝐾 → 𝐵 = 𝐷)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 = 𝐶)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐾 ∈ 𝐴)    ⇒   ⊢ (𝜑 → 𝐷 ≤ 𝐶)
Theorem	fsumiunle 32802*	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 32803	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 32804	Closure of the signum. (Contributed by Thierry Arnoux, 28-Sep-2018.)
⊢ (𝐴 ∈ ℝ* → (sgn‘𝐴) ∈ {-1, 0, 1})
Theorem	sgnclre 32805	Closure of the signum. (Contributed by Thierry Arnoux, 28-Sep-2018.)
⊢ (𝐴 ∈ ℝ → (sgn‘𝐴) ∈ ℝ)
Theorem	sgnneg 32806	Negation of the signum. (Contributed by Thierry Arnoux, 1-Oct-2018.)
⊢ (𝐴 ∈ ℝ → (sgn‘-𝐴) = -(sgn‘𝐴))
Theorem	sgn3da 32807	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 32808	Signum of a product. (Contributed by Thierry Arnoux, 2-Oct-2018.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (sgn‘(𝐴 · 𝐵)) = ((sgn‘𝐴) · (sgn‘𝐵)))
Theorem	sgnmulrp2 32809	Multiplication by a positive number does not affect signum. (Contributed by Thierry Arnoux, 2-Oct-2018.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+) → (sgn‘(𝐴 · 𝐵)) = (sgn‘𝐴))
Theorem	sgnsub 32810	Subtraction of a number of opposite sign. (Contributed by Thierry Arnoux, 2-Oct-2018.)
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐴 · 𝐵) < 0) → (sgn‘(𝐴 − 𝐵)) = (sgn‘𝐴))
Theorem	sgnnbi 32811	Negative signum. (Contributed by Thierry Arnoux, 2-Oct-2018.)
⊢ (𝐴 ∈ ℝ* → ((sgn‘𝐴) = -1 ↔ 𝐴 < 0))
Theorem	sgnpbi 32812	Positive signum. (Contributed by Thierry Arnoux, 2-Oct-2018.)
⊢ (𝐴 ∈ ℝ* → ((sgn‘𝐴) = 1 ↔ 0 < 𝐴))
Theorem	sgn0bi 32813	Zero signum. (Contributed by Thierry Arnoux, 10-Oct-2018.)
⊢ (𝐴 ∈ ℝ* → ((sgn‘𝐴) = 0 ↔ 𝐴 = 0))
Theorem	sgnsgn 32814	Signum is idempotent. (Contributed by Thierry Arnoux, 2-Oct-2018.)
⊢ (𝐴 ∈ ℝ* → (sgn‘(sgn‘𝐴)) = (sgn‘𝐴))
Theorem	sgnmulsgn 32815	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 32816	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 32817	A lower bound for an exponentiation. (Contributed by Thierry Arnoux, 19-Aug-2017.)
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℝ ∧ 2 ≤ 𝐵) → 𝐴 ≤ (𝐵↑𝐴))
Theorem	2exple2exp 32818*	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 32819	Even powers are positive. (Contributed by Thierry Arnoux, 9-Nov-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 2 ∥ 𝑁)    ⇒   ⊢ (𝜑 → 0 ≤ (𝐴↑𝑁))
Theorem	oexpled 32820	Odd power monomials are monotonic. (Contributed by Thierry Arnoux, 9-Nov-2025.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → ¬ 2 ∥ 𝑁)    &   ⊢ (𝜑 → 𝐴 ≤ 𝐵)    ⇒   ⊢ (𝜑 → (𝐴↑𝑁) ≤ (𝐵↑𝑁))
21.3.6.3  Indicator Functions
Syntax	cind 32821	Extend class notation with the indicator function generator.
class 𝟭
Definition	df-ind 32822*	Define the indicator function generator. (Contributed by Thierry Arnoux, 20-Jan-2017.)
⊢ 𝟭 = (𝑜 ∈ V ↦ (𝑎 ∈ 𝒫 𝑜 ↦ (𝑥 ∈ 𝑜 ↦ if(𝑥 ∈ 𝑎, 1, 0))))
Theorem	indv 32823*	Value of the indicator function generator with domain 𝑂. (Contributed by Thierry Arnoux, 23-Aug-2017.)
⊢ (𝑂 ∈ 𝑉 → (𝟭‘𝑂) = (𝑎 ∈ 𝒫 𝑂 ↦ (𝑥 ∈ 𝑂 ↦ if(𝑥 ∈ 𝑎, 1, 0))))
Theorem	indval 32824*	Value of the indicator function generator for a set 𝐴 and a domain 𝑂. (Contributed by Thierry Arnoux, 2-Feb-2017.)
⊢ ((𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂) → ((𝟭‘𝑂)‘𝐴) = (𝑥 ∈ 𝑂 ↦ if(𝑥 ∈ 𝐴, 1, 0)))
Theorem	indval2 32825	Alternate value of the indicator function generator. (Contributed by Thierry Arnoux, 2-Feb-2017.)
⊢ ((𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂) → ((𝟭‘𝑂)‘𝐴) = ((𝐴 × {1}) ∪ ((𝑂 ∖ 𝐴) × {0})))
Theorem	indf 32826	An indicator function as a function with domain and codomain. (Contributed by Thierry Arnoux, 13-Aug-2017.)
⊢ ((𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂) → ((𝟭‘𝑂)‘𝐴):𝑂⟶{0, 1})
Theorem	indfval 32827	Value of the indicator function. (Contributed by Thierry Arnoux, 13-Aug-2017.)
⊢ ((𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ∧ 𝑋 ∈ 𝑂) → (((𝟭‘𝑂)‘𝐴)‘𝑋) = if(𝑋 ∈ 𝐴, 1, 0))
Theorem	ind1 32828	Value of the indicator function where it is 1. (Contributed by Thierry Arnoux, 14-Aug-2017.)
⊢ ((𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ∧ 𝑋 ∈ 𝐴) → (((𝟭‘𝑂)‘𝐴)‘𝑋) = 1)
Theorem	ind0 32829	Value of the indicator function where it is 0. (Contributed by Thierry Arnoux, 14-Aug-2017.)
⊢ ((𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ∧ 𝑋 ∈ (𝑂 ∖ 𝐴)) → (((𝟭‘𝑂)‘𝐴)‘𝑋) = 0)
Theorem	ind1a 32830	Value of the indicator function where it is 1. (Contributed by Thierry Arnoux, 22-Aug-2017.)
⊢ ((𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ∧ 𝑋 ∈ 𝑂) → ((((𝟭‘𝑂)‘𝐴)‘𝑋) = 1 ↔ 𝑋 ∈ 𝐴))
Theorem	indpi1 32831	Preimage of the singleton {1} by the indicator function. See i1f1lem 25610. (Contributed by Thierry Arnoux, 21-Aug-2017.)
⊢ ((𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂) → (◡((𝟭‘𝑂)‘𝐴) “ {1}) = 𝐴)
Theorem	indsum 32832*	Finite sum of a product with the indicator function / Cartesian product with the indicator function. (Contributed by Thierry Arnoux, 14-Aug-2017.)
⊢ (𝜑 → 𝑂 ∈ Fin)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑂)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑂) → 𝐵 ∈ ℂ)    ⇒   ⊢ (𝜑 → Σ𝑥 ∈ 𝑂 ((((𝟭‘𝑂)‘𝐴)‘𝑥) · 𝐵) = Σ𝑥 ∈ 𝐴 𝐵)
Theorem	indsumin 32833*	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 32834*	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	indf1o 32835	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 32836	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 32837*	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 32838	The support of the indicator function. (Contributed by Thierry Arnoux, 13-Oct-2025.)
⊢ ((𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂) → (((𝟭‘𝑂)‘𝐴) supp 0) = 𝐴)
Theorem	indfsd 32839	The indicator function of a finite set has finite support. (Contributed by Thierry Arnoux, 18-Jan-2026.)
⊢ (𝜑 → 𝑂 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝑂)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    ⇒   ⊢ (𝜑 → ((𝟭‘𝑂)‘𝐴) finSupp 0)
Theorem	indfsid 32840	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 32841	Constant used for decimal fraction constructor. See df-dp2 32842.
class _𝐴𝐵
Definition	df-dp2 32842	Define the "decimal fraction constructor", which is used to build up "decimal fractions" in base 10. This is intentionally similar to df-dec 12581. (Contributed by David A. Wheeler, 15-May-2015.) (Revised by AV, 9-Sep-2021.)
⊢ _𝐴𝐵 = (𝐴 + (𝐵 / ;10))
Theorem	dp2eq1 32843	Equality theorem for the decimal expansion constructor. (Contributed by David A. Wheeler, 15-May-2015.)
⊢ (𝐴 = 𝐵 → _𝐴𝐶 = _𝐵𝐶)
Theorem	dp2eq2 32844	Equality theorem for the decimal expansion constructor. (Contributed by David A. Wheeler, 15-May-2015.)
⊢ (𝐴 = 𝐵 → _𝐶𝐴 = _𝐶𝐵)
Theorem	dp2eq1i 32845	Equality theorem for the decimal expansion constructor. (Contributed by David A. Wheeler, 15-May-2015.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ _𝐴𝐶 = _𝐵𝐶
Theorem	dp2eq2i 32846	Equality theorem for the decimal expansion constructor. (Contributed by David A. Wheeler, 15-May-2015.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ _𝐶𝐴 = _𝐶𝐵
Theorem	dp2eq12i 32847	Equality theorem for the decimal expansion constructor. (Contributed by David A. Wheeler, 15-May-2015.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ _𝐴𝐶 = _𝐵𝐷
Theorem	dp20u 32848	Add a zero in the tenths (lower) place. (Contributed by Thierry Arnoux, 16-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    ⇒   ⊢ _𝐴0 = 𝐴
Theorem	dp20h 32849	Add a zero in the unit places. (Contributed by Thierry Arnoux, 16-Dec-2021.)
⊢ 𝐴 ∈ ℝ+    ⇒   ⊢ _0𝐴 = (𝐴 / ;10)
Theorem	dp2cl 32850	Closure for the decimal fraction constructor if both values are reals. (Contributed by David A. Wheeler, 15-May-2015.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → _𝐴𝐵 ∈ ℝ)
Theorem	dp2clq 32851	Closure for a decimal fraction. (Contributed by Thierry Arnoux, 16-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℚ    ⇒   ⊢ _𝐴𝐵 ∈ ℚ
Theorem	rpdp2cl 32852	Closure for a decimal fraction in the positive real numbers. (Contributed by Thierry Arnoux, 16-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℝ+    ⇒   ⊢ _𝐴𝐵 ∈ ℝ+
Theorem	rpdp2cl2 32853	Closure for a decimal fraction with no decimal expansion in the positive real numbers. (Contributed by Thierry Arnoux, 25-Dec-2021.)
⊢ 𝐴 ∈ ℕ    ⇒   ⊢ _𝐴0 ∈ ℝ+
Theorem	dp2lt10 32854	Decimal fraction builds real numbers less than 10. (Contributed by Thierry Arnoux, 16-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℝ+    &   ⊢ 𝐴 < ;10    &   ⊢ 𝐵 < ;10    ⇒   ⊢ _𝐴𝐵 < ;10
Theorem	dp2lt 32855	Comparing two decimal fractions (equal unit places). (Contributed by Thierry Arnoux, 16-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℝ+    &   ⊢ 𝐶 ∈ ℝ+    &   ⊢ 𝐵 < 𝐶    ⇒   ⊢ _𝐴𝐵 < _𝐴𝐶
Theorem	dp2ltsuc 32856	Comparing a decimal fraction with the next integer. (Contributed by Thierry Arnoux, 25-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℝ+    &   ⊢ 𝐵 < ;10    &   ⊢ (𝐴 + 1) = 𝐶    ⇒   ⊢ _𝐴𝐵 < 𝐶
Theorem	dp2ltc 32857	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 32859 and df-dp2 32842 for more information; dpval2 32863 and dpfrac1 32862 provide a more convenient way to obtain a value. This is intentionally similar to df-dec 12581.
Syntax	cdp 32858	Decimal point operator. See df-dp 32859.
class .
Definition	df-dp 32859*	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 32860	Define the value of the decimal point operator. See df-dp 32859. (Contributed by David A. Wheeler, 15-May-2015.)
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℝ) → (𝐴.𝐵) = _𝐴𝐵)
Theorem	dpcl 32861	Prove that the closure of the decimal point is ℝ as we have defined it. See df-dp 32859. (Contributed by David A. Wheeler, 15-May-2015.)
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℝ) → (𝐴.𝐵) ∈ ℝ)
Theorem	dpfrac1 32862	Prove a simple equivalence involving the decimal point. See df-dp 32859 and dpcl 32861. (Contributed by David A. Wheeler, 15-May-2015.) (Revised by AV, 9-Sep-2021.)
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℝ) → (𝐴.𝐵) = (;𝐴𝐵 / ;10))
Theorem	dpval2 32863	Value of the decimal point construct. (Contributed by Thierry Arnoux, 16-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ (𝐴.𝐵) = (𝐴 + (𝐵 / ;10))
Theorem	dpval3 32864	Value of the decimal point construct. (Contributed by Thierry Arnoux, 16-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ (𝐴.𝐵) = _𝐴𝐵
Theorem	dpmul10 32865	Multiply by 10 a decimal expansion. (Contributed by Thierry Arnoux, 25-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ ((𝐴.𝐵) · ;10) = ;𝐴𝐵
Theorem	decdiv10 32866	Divide a decimal number by 10. (Contributed by Thierry Arnoux, 25-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ (;𝐴𝐵 / ;10) = (𝐴.𝐵)
Theorem	dpmul100 32867	Multiply by 100 a decimal expansion. (Contributed by Thierry Arnoux, 25-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℝ    ⇒   ⊢ ((𝐴._𝐵𝐶) · ;;100) = ;;𝐴𝐵𝐶
Theorem	dp3mul10 32868	Multiply by 10 a decimal expansion with 3 digits. (Contributed by Thierry Arnoux, 25-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℝ    ⇒   ⊢ ((𝐴._𝐵𝐶) · ;10) = (;𝐴𝐵.𝐶)
Theorem	dpmul1000 32869	Multiply by 1000 a decimal expansion. (Contributed by Thierry Arnoux, 25-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℝ    ⇒   ⊢ ((𝐴._𝐵_𝐶𝐷) · ;;;1000) = ;;;𝐴𝐵𝐶𝐷
Theorem	dpval3rp 32870	Value of the decimal point construct. (Contributed by Thierry Arnoux, 16-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℝ+    ⇒   ⊢ (𝐴.𝐵) = _𝐴𝐵
Theorem	dp0u 32871	Add a zero in the tenths place. (Contributed by Thierry Arnoux, 16-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    ⇒   ⊢ (𝐴.0) = 𝐴
Theorem	dp0h 32872	Remove a zero in the units places. (Contributed by Thierry Arnoux, 16-Dec-2021.)
⊢ 𝐴 ∈ ℝ+    ⇒   ⊢ (0.𝐴) = (𝐴 / ;10)
Theorem	rpdpcl 32873	Closure of the decimal point in the positive real numbers. (Contributed by Thierry Arnoux, 16-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℝ+    ⇒   ⊢ (𝐴.𝐵) ∈ ℝ+
Theorem	dplt 32874	Comparing two decimal expansions (equal higher places). (Contributed by Thierry Arnoux, 16-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℝ+    &   ⊢ 𝐶 ∈ ℝ+    &   ⊢ 𝐵 < 𝐶    ⇒   ⊢ (𝐴.𝐵) < (𝐴.𝐶)
Theorem	dplti 32875	Comparing a decimal expansions with the next higher integer. (Contributed by Thierry Arnoux, 16-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℝ+    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐵 < ;10    &   ⊢ (𝐴 + 1) = 𝐶    ⇒   ⊢ (𝐴.𝐵) < 𝐶
Theorem	dpgti 32876	Comparing a decimal expansions with the next lower integer. (Contributed by Thierry Arnoux, 16-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℝ+    ⇒   ⊢ 𝐴 < (𝐴.𝐵)
Theorem	dpltc 32877	Comparing two decimal integers (unequal higher places). (Contributed by Thierry Arnoux, 16-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℝ+    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℝ+    &   ⊢ 𝐴 < 𝐶    &   ⊢ 𝐵 < ;10    ⇒   ⊢ (𝐴.𝐵) < (𝐶.𝐷)
Theorem	dpexpp1 32878	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 32879	Multiply by 10 a decimal expansion which starts with a zero. (Contributed by Thierry Arnoux, 16-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℝ+    ⇒   ⊢ ((0._𝐴𝐵) · ;10) = (𝐴.𝐵)
Theorem	dpadd2 32880	Addition with one decimal, no carry. (Contributed by Thierry Arnoux, 29-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℝ+    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℝ+    &   ⊢ 𝐸 ∈ ℕ0    &   ⊢ 𝐹 ∈ ℝ+    &   ⊢ 𝐺 ∈ ℕ0    &   ⊢ 𝐻 ∈ ℕ0    &   ⊢ (𝐺 + 𝐻) = 𝐼    &   ⊢ ((𝐴.𝐵) + (𝐶.𝐷)) = (𝐸.𝐹)    ⇒   ⊢ ((𝐺._𝐴𝐵) + (𝐻._𝐶𝐷)) = (𝐼._𝐸𝐹)
Theorem	dpadd 32881	Addition with one decimal. (Contributed by Thierry Arnoux, 27-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℕ0    &   ⊢ 𝐸 ∈ ℕ0    &   ⊢ 𝐹 ∈ ℕ0    &   ⊢ (;𝐴𝐵 + ;𝐶𝐷) = ;𝐸𝐹    ⇒   ⊢ ((𝐴.𝐵) + (𝐶.𝐷)) = (𝐸.𝐹)
Theorem	dpadd3 32882	Addition with two decimals. (Contributed by Thierry Arnoux, 27-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℕ0    &   ⊢ 𝐸 ∈ ℕ0    &   ⊢ 𝐺 ∈ ℕ0    &   ⊢ 𝐹 ∈ ℕ0    &   ⊢ 𝐻 ∈ ℕ0    &   ⊢ 𝐼 ∈ ℕ0    &   ⊢ (;;𝐴𝐵𝐶 + ;;𝐷𝐸𝐹) = ;;𝐺𝐻𝐼    ⇒   ⊢ ((𝐴._𝐵𝐶) + (𝐷._𝐸𝐹)) = (𝐺._𝐻𝐼)
Theorem	dpmul 32883	Multiplication with one decimal point. (Contributed by Thierry Arnoux, 26-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℕ0    &   ⊢ 𝐸 ∈ ℕ0    &   ⊢ 𝐺 ∈ ℕ0    &   ⊢ 𝐽 ∈ ℕ0    &   ⊢ 𝐾 ∈ ℕ0    &   ⊢ (𝐴 · 𝐶) = 𝐹    &   ⊢ (𝐴 · 𝐷) = 𝑀    &   ⊢ (𝐵 · 𝐶) = 𝐿    &   ⊢ (𝐵 · 𝐷) = ;𝐸𝐾    &   ⊢ ((𝐿 + 𝑀) + 𝐸) = ;𝐺𝐽    &   ⊢ (𝐹 + 𝐺) = 𝐼    ⇒   ⊢ ((𝐴.𝐵) · (𝐶.𝐷)) = (𝐼._𝐽𝐾)
Theorem	dpmul4 32884	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 32885	Example theorem demonstrating decimal expansions. (Contributed by Thierry Arnoux, 27-Dec-2021.)
⊢ (3 / 2) = (1.5)
Theorem	1mhdrd 32886	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 32887	Extend class notation to include division of extended reals.
class /𝑒
Definition	df-xdiv 32888*	Define division over extended real numbers. (Contributed by Thierry Arnoux, 17-Dec-2016.)
⊢ /𝑒 = (𝑥 ∈ ℝ*, 𝑦 ∈ (ℝ ∖ {0}) ↦ (℩𝑧 ∈ ℝ* (𝑦 ·e 𝑧) = 𝑥))
Theorem	xdivval 32889*	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 32890*	Existence of reciprocal of nonzero real number. (Contributed by Thierry Arnoux, 17-Dec-2016.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) → ∃𝑥 ∈ ℝ (𝐴 ·e 𝑥) = 1)
Theorem	xmulcand 32891	Cancellation law for extended multiplication. (Contributed by Thierry Arnoux, 17-Dec-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ≠ 0)    ⇒   ⊢ (𝜑 → ((𝐶 ·e 𝐴) = (𝐶 ·e 𝐵) ↔ 𝐴 = 𝐵))
Theorem	xreceu 32892*	Existential uniqueness of reciprocals. Theorem I.8 of [Apostol] p. 18. (Contributed by Thierry Arnoux, 17-Dec-2016.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → ∃!𝑥 ∈ ℝ* (𝐵 ·e 𝑥) = 𝐴)
Theorem	xdivcld 32893	Closure law for the extended division. (Contributed by Thierry Arnoux, 15-Mar-2017.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    ⇒   ⊢ (𝜑 → (𝐴 /𝑒 𝐵) ∈ ℝ*)
Theorem	xdivcl 32894	Closure law for the extended division. (Contributed by Thierry Arnoux, 15-Mar-2017.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → (𝐴 /𝑒 𝐵) ∈ ℝ*)
Theorem	xdivmul 32895	Relationship between division and multiplication. (Contributed by Thierry Arnoux, 24-Dec-2016.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ (𝐶 ∈ ℝ ∧ 𝐶 ≠ 0)) → ((𝐴 /𝑒 𝐶) = 𝐵 ↔ (𝐶 ·e 𝐵) = 𝐴))
Theorem	rexdiv 32896	The extended real division operation when both arguments are real. (Contributed by Thierry Arnoux, 18-Dec-2016.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → (𝐴 /𝑒 𝐵) = (𝐴 / 𝐵))
Theorem	xdivrec 32897	Relationship between division and reciprocal. (Contributed by Thierry Arnoux, 5-Jul-2017.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → (𝐴 /𝑒 𝐵) = (𝐴 ·e (1 /𝑒 𝐵)))
Theorem	xdivid 32898	A number divided by itself is one. (Contributed by Thierry Arnoux, 18-Dec-2016.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) → (𝐴 /𝑒 𝐴) = 1)
Theorem	xdiv0 32899	Division into zero is zero. (Contributed by Thierry Arnoux, 18-Dec-2016.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) → (0 /𝑒 𝐴) = 0)
Theorem	xdiv0rp 32900	Division into zero is zero. (Contributed by Thierry Arnoux, 18-Dec-2016.)
⊢ (𝐴 ∈ ℝ+ → (0 /𝑒 𝐴) = 0)