P. 308 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 30701-30800   *Has distinct variable group(s)

Type	Label	Description
Statement
20.3.5.8  The ` # ` (set size) function - misc additions
Theorem	hashunif 30701*	The cardinality of a disjoint finite union of finite sets. Cf. hashuni 15274. (Contributed by Thierry Arnoux, 17-Feb-2017.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝐴 ⊆ Fin)    &   ⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 𝑥)    ⇒   ⊢ (𝜑 → (♯‘∪ 𝐴) = Σ𝑥 ∈ 𝐴 (♯‘𝑥))
Theorem	hashxpe 30702	The size of the Cartesian product of two finite sets is the product of their sizes. This is a version of hashxp 13887 valid for infinite sets, which uses extended real numbers. (Contributed by Thierry Arnoux, 27-May-2023.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (♯‘(𝐴 × 𝐵)) = ((♯‘𝐴) ·e (♯‘𝐵)))
Theorem	hashgt1 30703	Restate "set contains at least two elements" in terms of elementhood. (Contributed by Thierry Arnoux, 21-Nov-2023.)
⊢ (𝐴 ∈ 𝑉 → (¬ 𝐴 ∈ (◡♯ “ {0, 1}) ↔ 1 < (♯‘𝐴)))
20.3.5.9  The greatest common divisor operator - misc. add
Theorem	dvdszzq 30704	Divisibility for an integer quotient. (Contributed by Thierry Arnoux, 17-Sep-2023.)
⊢ 𝑁 = (𝐴 / 𝐵)    &   ⊢ (𝜑 → 𝑃 ∈ ℙ)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ (𝜑 → 𝐵 ∈ ℤ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    &   ⊢ (𝜑 → 𝑃 ∥ 𝐴)    &   ⊢ (𝜑 → ¬ 𝑃 ∥ 𝐵)    ⇒   ⊢ (𝜑 → 𝑃 ∥ 𝑁)
Theorem	prmdvdsbc 30705	Condition for a prime number to divide a binomial coefficient. (Contributed by Thierry Arnoux, 17-Sep-2023.)
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → 𝑃 ∥ (𝑃C𝑁))
Theorem	numdenneg 30706	Numerator and denominator of the negative. (Contributed by Thierry Arnoux, 27-Oct-2017.)
⊢ (𝑄 ∈ ℚ → ((numer‘-𝑄) = -(numer‘𝑄) ∧ (denom‘-𝑄) = (denom‘𝑄)))
Theorem	divnumden2 30707	Calculate the reduced form of a quotient using gcd. This version extends divnumden 16188 for the negative integers. (Contributed by Thierry Arnoux, 25-Oct-2017.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ -𝐵 ∈ ℕ) → ((numer‘(𝐴 / 𝐵)) = -(𝐴 / (𝐴 gcd 𝐵)) ∧ (denom‘(𝐴 / 𝐵)) = -(𝐵 / (𝐴 gcd 𝐵))))
20.3.5.10  Integers
Theorem	nnindf 30708*	Principle of Mathematical Induction, using a bound-variable hypothesis instead of distinct variables. (Contributed by Thierry Arnoux, 6-May-2018.)
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝑥 = 1 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑥 = (𝑦 + 1) → (𝜑 ↔ 𝜃))    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏))    &   ⊢ 𝜓    &   ⊢ (𝑦 ∈ ℕ → (𝜒 → 𝜃))    ⇒   ⊢ (𝐴 ∈ ℕ → 𝜏)
Theorem	nn0min 30709*	Extracting the minimum positive integer for which a property 𝜒 does not hold. This uses substitutions similar to nn0ind 12158. (Contributed by Thierry Arnoux, 6-May-2018.)
⊢ (𝑛 = 0 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑛 = 𝑚 → (𝜓 ↔ 𝜃))    &   ⊢ (𝑛 = (𝑚 + 1) → (𝜓 ↔ 𝜏))    &   ⊢ (𝜑 → ¬ 𝜒)    &   ⊢ (𝜑 → ∃𝑛 ∈ ℕ 𝜓)    ⇒   ⊢ (𝜑 → ∃𝑚 ∈ ℕ0 (¬ 𝜃 ∧ 𝜏))
Theorem	subne0nn 30710	A nonnegative difference is positive if the two numbers are not equal. (Contributed by Thierry Arnoux, 17-Dec-2023.)
⊢ (𝜑 → 𝑀 ∈ ℂ)    &   ⊢ (𝜑 → 𝑁 ∈ ℂ)    &   ⊢ (𝜑 → (𝑀 − 𝑁) ∈ ℕ0)    &   ⊢ (𝜑 → 𝑀 ≠ 𝑁)    ⇒   ⊢ (𝜑 → (𝑀 − 𝑁) ∈ ℕ)
Theorem	ltesubnnd 30711	Subtracting an integer number from another number decreases it. See ltsubrpd 12546. (Contributed by Thierry Arnoux, 18-Apr-2017.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    ⇒   ⊢ (𝜑 → ((𝑀 + 1) − 𝑁) ≤ 𝑀)
Theorem	fprodeq02 30712*	If one of the factors is zero the product is zero. (Contributed by Thierry Arnoux, 11-Dec-2021.)
⊢ (𝑘 = 𝐾 → 𝐵 = 𝐶)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐾 ∈ 𝐴)    &   ⊢ (𝜑 → 𝐶 = 0)    ⇒   ⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐵 = 0)
Theorem	pr01ssre 30713	The range of the indicator function is a subset of ℝ. (Contributed by Thierry Arnoux, 14-Aug-2017.)
⊢ {0, 1} ⊆ ℝ
Theorem	fprodex01 30714*	A product of factors equal to zero or one is zero exactly when one of the factors is zero. (Contributed by Thierry Arnoux, 11-Dec-2021.)
⊢ (𝑘 = 𝑙 → 𝐵 = 𝐶)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ {0, 1})    ⇒   ⊢ (𝜑 → ∏𝑘 ∈ 𝐴 𝐵 = if(∀𝑙 ∈ 𝐴 𝐶 = 1, 1, 0))
Theorem	prodpr 30715*	A product over a pair is the product of the elements. (Contributed by Thierry Arnoux, 1-Jan-2022.)
⊢ (𝑘 = 𝐴 → 𝐷 = 𝐸)    &   ⊢ (𝑘 = 𝐵 → 𝐷 = 𝐹)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐸 ∈ ℂ)    &   ⊢ (𝜑 → 𝐹 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    ⇒   ⊢ (𝜑 → ∏𝑘 ∈ {𝐴, 𝐵}𝐷 = (𝐸 · 𝐹))
Theorem	prodtp 30716*	A product over a triple is the product of the elements. (Contributed by Thierry Arnoux, 1-Jan-2022.)
⊢ (𝑘 = 𝐴 → 𝐷 = 𝐸)    &   ⊢ (𝑘 = 𝐵 → 𝐷 = 𝐹)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐸 ∈ ℂ)    &   ⊢ (𝜑 → 𝐹 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐵)    &   ⊢ (𝑘 = 𝐶 → 𝐷 = 𝐺)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐺 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 𝐶)    &   ⊢ (𝜑 → 𝐵 ≠ 𝐶)    ⇒   ⊢ (𝜑 → ∏𝑘 ∈ {𝐴, 𝐵, 𝐶}𝐷 = ((𝐸 · 𝐹) · 𝐺))
Theorem	fsumub 30717*	An upper bound for a term of a positive finite sum. (Contributed by Thierry Arnoux, 27-Dec-2021.)
⊢ (𝑘 = 𝐾 → 𝐵 = 𝐷)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 = 𝐶)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐾 ∈ 𝐴)    ⇒   ⊢ (𝜑 → 𝐷 ≤ 𝐶)
Theorem	fsumiunle 30718*	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 ≤ 𝐶)    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵𝐶 ≤ Σ𝑥 ∈ 𝐴 Σ𝑘 ∈ 𝐵 𝐶)
20.3.5.11  Decimal numbers
Theorem	dfdec100 30719	Split the hundreds from a decimal value. (Contributed by Thierry Arnoux, 25-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℝ    ⇒   ⊢ ;;𝐴𝐵𝐶 = ((;;100 · 𝐴) + ;𝐵𝐶)
20.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 30720	Constant used for decimal fraction constructor. See df-dp2 30721.
class _𝐴𝐵
Definition	df-dp2 30721	Define the "decimal fraction constructor", which is used to build up "decimal fractions" in base 10. This is intentionally similar to df-dec 12180. (Contributed by David A. Wheeler, 15-May-2015.) (Revised by AV, 9-Sep-2021.)
⊢ _𝐴𝐵 = (𝐴 + (𝐵 / ;10))
Theorem	dp2eq1 30722	Equality theorem for the decimal expansion constructor. (Contributed by David A. Wheeler, 15-May-2015.)
⊢ (𝐴 = 𝐵 → _𝐴𝐶 = _𝐵𝐶)
Theorem	dp2eq2 30723	Equality theorem for the decimal expansion constructor. (Contributed by David A. Wheeler, 15-May-2015.)
⊢ (𝐴 = 𝐵 → _𝐶𝐴 = _𝐶𝐵)
Theorem	dp2eq1i 30724	Equality theorem for the decimal expansion constructor. (Contributed by David A. Wheeler, 15-May-2015.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ _𝐴𝐶 = _𝐵𝐶
Theorem	dp2eq2i 30725	Equality theorem for the decimal expansion constructor. (Contributed by David A. Wheeler, 15-May-2015.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ _𝐶𝐴 = _𝐶𝐵
Theorem	dp2eq12i 30726	Equality theorem for the decimal expansion constructor. (Contributed by David A. Wheeler, 15-May-2015.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ _𝐴𝐶 = _𝐵𝐷
Theorem	dp20u 30727	Add a zero in the tenths (lower) place. (Contributed by Thierry Arnoux, 16-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    ⇒   ⊢ _𝐴0 = 𝐴
Theorem	dp20h 30728	Add a zero in the unit places. (Contributed by Thierry Arnoux, 16-Dec-2021.)
⊢ 𝐴 ∈ ℝ+    ⇒   ⊢ _0𝐴 = (𝐴 / ;10)
Theorem	dp2cl 30729	Closure for the decimal fraction constructor if both values are reals. (Contributed by David A. Wheeler, 15-May-2015.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → _𝐴𝐵 ∈ ℝ)
Theorem	dp2clq 30730	Closure for a decimal fraction. (Contributed by Thierry Arnoux, 16-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℚ    ⇒   ⊢ _𝐴𝐵 ∈ ℚ
Theorem	rpdp2cl 30731	Closure for a decimal fraction in the positive real numbers. (Contributed by Thierry Arnoux, 16-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℝ+    ⇒   ⊢ _𝐴𝐵 ∈ ℝ+
Theorem	rpdp2cl2 30732	Closure for a decimal fraction with no decimal expansion in the positive real numbers. (Contributed by Thierry Arnoux, 25-Dec-2021.)
⊢ 𝐴 ∈ ℕ    ⇒   ⊢ _𝐴0 ∈ ℝ+
Theorem	dp2lt10 30733	Decimal fraction builds real numbers less than 10. (Contributed by Thierry Arnoux, 16-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℝ+    &   ⊢ 𝐴 < ;10    &   ⊢ 𝐵 < ;10    ⇒   ⊢ _𝐴𝐵 < ;10
Theorem	dp2lt 30734	Comparing two decimal fractions (equal unit places). (Contributed by Thierry Arnoux, 16-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℝ+    &   ⊢ 𝐶 ∈ ℝ+    &   ⊢ 𝐵 < 𝐶    ⇒   ⊢ _𝐴𝐵 < _𝐴𝐶
Theorem	dp2ltsuc 30735	Comparing a decimal fraction with the next integer. (Contributed by Thierry Arnoux, 25-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℝ+    &   ⊢ 𝐵 < ;10    &   ⊢ (𝐴 + 1) = 𝐶    ⇒   ⊢ _𝐴𝐵 < 𝐶
Theorem	dp2ltc 30736	Comparing two decimal expansions (unequal higher places). (Contributed by Thierry Arnoux, 16-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℝ+    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℝ+    &   ⊢ 𝐵 < ;10    &   ⊢ 𝐴 < 𝐶    ⇒   ⊢ _𝐴𝐵 < _𝐶𝐷
20.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 30738 and df-dp2 30721 for more information; dpval2 30742 and dpfrac1 30741 provide a more convenient way to obtain a value. This is intentionally similar to df-dec 12180.
Syntax	cdp 30737	Decimal point operator. See df-dp 30738.
class .
Definition	df-dp 30738*	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 30739	Define the value of the decimal point operator. See df-dp 30738. (Contributed by David A. Wheeler, 15-May-2015.)
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℝ) → (𝐴.𝐵) = _𝐴𝐵)
Theorem	dpcl 30740	Prove that the closure of the decimal point is ℝ as we have defined it. See df-dp 30738. (Contributed by David A. Wheeler, 15-May-2015.)
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℝ) → (𝐴.𝐵) ∈ ℝ)
Theorem	dpfrac1 30741	Prove a simple equivalence involving the decimal point. See df-dp 30738 and dpcl 30740. (Contributed by David A. Wheeler, 15-May-2015.) (Revised by AV, 9-Sep-2021.)
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℝ) → (𝐴.𝐵) = (;𝐴𝐵 / ;10))
Theorem	dpval2 30742	Value of the decimal point construct. (Contributed by Thierry Arnoux, 16-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ (𝐴.𝐵) = (𝐴 + (𝐵 / ;10))
Theorem	dpval3 30743	Value of the decimal point construct. (Contributed by Thierry Arnoux, 16-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ (𝐴.𝐵) = _𝐴𝐵
Theorem	dpmul10 30744	Multiply by 10 a decimal expansion. (Contributed by Thierry Arnoux, 25-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ ((𝐴.𝐵) · ;10) = ;𝐴𝐵
Theorem	decdiv10 30745	Divide a decimal number by 10. (Contributed by Thierry Arnoux, 25-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℝ    ⇒   ⊢ (;𝐴𝐵 / ;10) = (𝐴.𝐵)
Theorem	dpmul100 30746	Multiply by 100 a decimal expansion. (Contributed by Thierry Arnoux, 25-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℝ    ⇒   ⊢ ((𝐴._𝐵𝐶) · ;;100) = ;;𝐴𝐵𝐶
Theorem	dp3mul10 30747	Multiply by 10 a decimal expansion with 3 digits. (Contributed by Thierry Arnoux, 25-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℝ    ⇒   ⊢ ((𝐴._𝐵𝐶) · ;10) = (;𝐴𝐵.𝐶)
Theorem	dpmul1000 30748	Multiply by 1000 a decimal expansion. (Contributed by Thierry Arnoux, 25-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℝ    ⇒   ⊢ ((𝐴._𝐵_𝐶𝐷) · ;;;1000) = ;;;𝐴𝐵𝐶𝐷
Theorem	dpval3rp 30749	Value of the decimal point construct. (Contributed by Thierry Arnoux, 16-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℝ+    ⇒   ⊢ (𝐴.𝐵) = _𝐴𝐵
Theorem	dp0u 30750	Add a zero in the tenths place. (Contributed by Thierry Arnoux, 16-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    ⇒   ⊢ (𝐴.0) = 𝐴
Theorem	dp0h 30751	Remove a zero in the units places. (Contributed by Thierry Arnoux, 16-Dec-2021.)
⊢ 𝐴 ∈ ℝ+    ⇒   ⊢ (0.𝐴) = (𝐴 / ;10)
Theorem	rpdpcl 30752	Closure of the decimal point in the positive real numbers. (Contributed by Thierry Arnoux, 16-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℝ+    ⇒   ⊢ (𝐴.𝐵) ∈ ℝ+
Theorem	dplt 30753	Comparing two decimal expansions (equal higher places). (Contributed by Thierry Arnoux, 16-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℝ+    &   ⊢ 𝐶 ∈ ℝ+    &   ⊢ 𝐵 < 𝐶    ⇒   ⊢ (𝐴.𝐵) < (𝐴.𝐶)
Theorem	dplti 30754	Comparing a decimal expansions with the next higher integer. (Contributed by Thierry Arnoux, 16-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℝ+    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐵 < ;10    &   ⊢ (𝐴 + 1) = 𝐶    ⇒   ⊢ (𝐴.𝐵) < 𝐶
Theorem	dpgti 30755	Comparing a decimal expansions with the next lower integer. (Contributed by Thierry Arnoux, 16-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℝ+    ⇒   ⊢ 𝐴 < (𝐴.𝐵)
Theorem	dpltc 30756	Comparing two decimal integers (unequal higher places). (Contributed by Thierry Arnoux, 16-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℝ+    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℝ+    &   ⊢ 𝐴 < 𝐶    &   ⊢ 𝐵 < ;10    ⇒   ⊢ (𝐴.𝐵) < (𝐶.𝐷)
Theorem	dpexpp1 30757	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 30758	Multiply by 10 a decimal expansion which starts with a zero. (Contributed by Thierry Arnoux, 16-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℝ+    ⇒   ⊢ ((0._𝐴𝐵) · ;10) = (𝐴.𝐵)
Theorem	dpadd2 30759	Addition with one decimal, no carry. (Contributed by Thierry Arnoux, 29-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℝ+    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℝ+    &   ⊢ 𝐸 ∈ ℕ0    &   ⊢ 𝐹 ∈ ℝ+    &   ⊢ 𝐺 ∈ ℕ0    &   ⊢ 𝐻 ∈ ℕ0    &   ⊢ (𝐺 + 𝐻) = 𝐼    &   ⊢ ((𝐴.𝐵) + (𝐶.𝐷)) = (𝐸.𝐹)    ⇒   ⊢ ((𝐺._𝐴𝐵) + (𝐻._𝐶𝐷)) = (𝐼._𝐸𝐹)
Theorem	dpadd 30760	Addition with one decimal. (Contributed by Thierry Arnoux, 27-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℕ0    &   ⊢ 𝐸 ∈ ℕ0    &   ⊢ 𝐹 ∈ ℕ0    &   ⊢ (;𝐴𝐵 + ;𝐶𝐷) = ;𝐸𝐹    ⇒   ⊢ ((𝐴.𝐵) + (𝐶.𝐷)) = (𝐸.𝐹)
Theorem	dpadd3 30761	Addition with two decimals. (Contributed by Thierry Arnoux, 27-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℕ0    &   ⊢ 𝐸 ∈ ℕ0    &   ⊢ 𝐺 ∈ ℕ0    &   ⊢ 𝐹 ∈ ℕ0    &   ⊢ 𝐻 ∈ ℕ0    &   ⊢ 𝐼 ∈ ℕ0    &   ⊢ (;;𝐴𝐵𝐶 + ;;𝐷𝐸𝐹) = ;;𝐺𝐻𝐼    ⇒   ⊢ ((𝐴._𝐵𝐶) + (𝐷._𝐸𝐹)) = (𝐺._𝐻𝐼)
Theorem	dpmul 30762	Multiplication with one decimal point. (Contributed by Thierry Arnoux, 26-Dec-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℕ0    &   ⊢ 𝐸 ∈ ℕ0    &   ⊢ 𝐺 ∈ ℕ0    &   ⊢ 𝐽 ∈ ℕ0    &   ⊢ 𝐾 ∈ ℕ0    &   ⊢ (𝐴 · 𝐶) = 𝐹    &   ⊢ (𝐴 · 𝐷) = 𝑀    &   ⊢ (𝐵 · 𝐶) = 𝐿    &   ⊢ (𝐵 · 𝐷) = ;𝐸𝐾    &   ⊢ ((𝐿 + 𝑀) + 𝐸) = ;𝐺𝐽    &   ⊢ (𝐹 + 𝐺) = 𝐼    ⇒   ⊢ ((𝐴.𝐵) · (𝐶.𝐷)) = (𝐼._𝐽𝐾)
Theorem	dpmul4 30763	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 30764	Example theorem demonstrating decimal expansions. (Contributed by Thierry Arnoux, 27-Dec-2021.)
⊢ (3 / 2) = (1.5)
Theorem	1mhdrd 30765	Example theorem demonstrating decimal expansions. (Contributed by Thierry Arnoux, 27-Dec-2021.)
⊢ ((0._99) + (0._01)) = 1
20.3.6.2  Division in the extended real number system
Syntax	cxdiv 30766	Extend class notation to include division of extended reals.
class /𝑒
Definition	df-xdiv 30767*	Define division over extended real numbers. (Contributed by Thierry Arnoux, 17-Dec-2016.)
⊢ /𝑒 = (𝑥 ∈ ℝ*, 𝑦 ∈ (ℝ ∖ {0}) ↦ (℩𝑧 ∈ ℝ* (𝑦 ·e 𝑧) = 𝑥))
Theorem	xdivval 30768*	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 30769*	Existence of reciprocal of nonzero real number. (Contributed by Thierry Arnoux, 17-Dec-2016.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) → ∃𝑥 ∈ ℝ (𝐴 ·e 𝑥) = 1)
Theorem	xmulcand 30770	Cancellation law for extended multiplication. (Contributed by Thierry Arnoux, 17-Dec-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ≠ 0)    ⇒   ⊢ (𝜑 → ((𝐶 ·e 𝐴) = (𝐶 ·e 𝐵) ↔ 𝐴 = 𝐵))
Theorem	xreceu 30771*	Existential uniqueness of reciprocals. Theorem I.8 of [Apostol] p. 18. (Contributed by Thierry Arnoux, 17-Dec-2016.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → ∃!𝑥 ∈ ℝ* (𝐵 ·e 𝑥) = 𝐴)
Theorem	xdivcld 30772	Closure law for the extended division. (Contributed by Thierry Arnoux, 15-Mar-2017.)
⊢ (𝜑 → 𝐴 ∈ ℝ*)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    ⇒   ⊢ (𝜑 → (𝐴 /𝑒 𝐵) ∈ ℝ*)
Theorem	xdivcl 30773	Closure law for the extended division. (Contributed by Thierry Arnoux, 15-Mar-2017.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → (𝐴 /𝑒 𝐵) ∈ ℝ*)
Theorem	xdivmul 30774	Relationship between division and multiplication. (Contributed by Thierry Arnoux, 24-Dec-2016.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ (𝐶 ∈ ℝ ∧ 𝐶 ≠ 0)) → ((𝐴 /𝑒 𝐶) = 𝐵 ↔ (𝐶 ·e 𝐵) = 𝐴))
Theorem	rexdiv 30775	The extended real division operation when both arguments are real. (Contributed by Thierry Arnoux, 18-Dec-2016.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → (𝐴 /𝑒 𝐵) = (𝐴 / 𝐵))
Theorem	xdivrec 30776	Relationship between division and reciprocal. (Contributed by Thierry Arnoux, 5-Jul-2017.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0) → (𝐴 /𝑒 𝐵) = (𝐴 ·e (1 /𝑒 𝐵)))
Theorem	xdivid 30777	A number divided by itself is one. (Contributed by Thierry Arnoux, 18-Dec-2016.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) → (𝐴 /𝑒 𝐴) = 1)
Theorem	xdiv0 30778	Division into zero is zero. (Contributed by Thierry Arnoux, 18-Dec-2016.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) → (0 /𝑒 𝐴) = 0)
Theorem	xdiv0rp 30779	Division into zero is zero. (Contributed by Thierry Arnoux, 18-Dec-2016.)
⊢ (𝐴 ∈ ℝ+ → (0 /𝑒 𝐴) = 0)
Theorem	eliccioo 30780	Membership in a closed interval of extended reals versus the same open interval. (Contributed by Thierry Arnoux, 18-Dec-2016.)
⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵) → (𝐶 ∈ (𝐴[,]𝐵) ↔ (𝐶 = 𝐴 ∨ 𝐶 ∈ (𝐴(,)𝐵) ∨ 𝐶 = 𝐵)))
Theorem	elxrge02 30781	Elementhood in the set of nonnegative extended reals. (Contributed by Thierry Arnoux, 18-Dec-2016.)
⊢ (𝐴 ∈ (0[,]+∞) ↔ (𝐴 = 0 ∨ 𝐴 ∈ ℝ+ ∨ 𝐴 = +∞))
Theorem	xdivpnfrp 30782	Plus infinity divided by a positive real number is plus infinity. (Contributed by Thierry Arnoux, 18-Dec-2016.)
⊢ (𝐴 ∈ ℝ+ → (+∞ /𝑒 𝐴) = +∞)
Theorem	rpxdivcld 30783	Closure law for extended division of positive reals. (Contributed by Thierry Arnoux, 18-Dec-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    ⇒   ⊢ (𝜑 → (𝐴 /𝑒 𝐵) ∈ ℝ+)
Theorem	xrpxdivcld 30784	Closure law for extended division of positive extended reals. (Contributed by Thierry Arnoux, 18-Dec-2016.)
⊢ (𝜑 → 𝐴 ∈ (0[,]+∞))    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    ⇒   ⊢ (𝜑 → (𝐴 /𝑒 𝐵) ∈ (0[,]+∞))
20.3.7  Words over a set - misc additions
Theorem	wrdfd 30785	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 30786	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 30787*	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 30788	The prefix of length 1 of a length 2 word. (Contributed by Thierry Arnoux, 19-Sep-2023.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (⟨“𝐴𝐵”⟩ prefix 1) = ⟨“𝐴”⟩)
Theorem	pfxrn2 30789	The range of a prefix of a word is a subset of the range of that word. Stronger version of pfxrn 14136. (Contributed by Thierry Arnoux, 12-Dec-2023.)
⊢ ((𝑊 ∈ Word 𝑆 ∧ 𝐿 ∈ (0...(♯‘𝑊))) → ran (𝑊 prefix 𝐿) ⊆ ran 𝑊)
Theorem	pfxrn3 30790	Express the range of a prefix of a word. Stronger version of pfxrn2 30789. (Contributed by Thierry Arnoux, 13-Dec-2023.)
⊢ ((𝑊 ∈ Word 𝑆 ∧ 𝐿 ∈ (0...(♯‘𝑊))) → ran (𝑊 prefix 𝐿) = (𝑊 “ (0..^𝐿)))
Theorem	pfxf1 30791	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 30792	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 30793	Range of a length 2 string. (Contributed by Thierry Arnoux, 19-Sep-2023.)
⊢ (𝜑 → 𝐼 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐽 ∈ 𝐷)    ⇒   ⊢ (𝜑 → ran ⟨“𝐼𝐽”⟩ = {𝐼, 𝐽})
Theorem	s2f1 30794	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 30795	Range of a length 3 string. (Contributed by Thierry Arnoux, 19-Sep-2023.)
⊢ (𝜑 → 𝐼 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐽 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐾 ∈ 𝐷)    ⇒   ⊢ (𝜑 → ran ⟨“𝐼𝐽𝐾”⟩ = {𝐼, 𝐽, 𝐾})
Theorem	s3f1 30796	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 30797	Closure of the words of length 3 in a preimage using the hash function. (Contributed by Thierry Arnoux, 27-Sep-2023.)
⊢ ⟨“𝐼𝐽𝐾”⟩ ∈ (◡♯ “ {3})
Theorem	ccatf1 30798	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 30799	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 30800*	Perform an induction over the structure of a word of even length. (Contributed by Thierry Arnoux, 26-Sep-2023.)
⊢ (𝑥 = ∅ → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑥 = (𝑦 ++ ⟨“𝑖𝑗”⟩) → (𝜑 ↔ 𝜃))    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏))    &   ⊢ 𝜓    &   ⊢ ((𝑦 ∈ Word 𝐵 ∧ 𝑖 ∈ 𝐵 ∧ 𝑗 ∈ 𝐵) → (𝜒 → 𝜃))    ⇒   ⊢ ((𝐴 ∈ Word 𝐵 ∧ 2 ∥ (♯‘𝐴)) → 𝜏)