P. 98 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 9701-9800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	nn0ind-raph 9701*	Principle of Mathematical Induction (inference schema) on nonnegative integers. The first four hypotheses give us the substitution instances we need; the last two are the basis and the induction step. Raph Levien remarks: "This seems a bit painful. I wonder if an explicit substitution version would be easier." (Contributed by Raph Levien, 10-Apr-2004.)
⊢ (𝑥 = 0 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑥 = (𝑦 + 1) → (𝜑 ↔ 𝜃))    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏))    &   ⊢ 𝜓    &   ⊢ (𝑦 ∈ ℕ0 → (𝜒 → 𝜃))    ⇒   ⊢ (𝐴 ∈ ℕ0 → 𝜏)
Theorem	zindd 9702*	Principle of Mathematical Induction on all integers, deduction version. The first five hypotheses give the substitutions; the last three are the basis, the induction, and the extension to negative numbers. (Contributed by Paul Chapman, 17-Apr-2009.) (Proof shortened by Mario Carneiro, 4-Jan-2017.)
⊢ (𝑥 = 0 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑥 = (𝑦 + 1) → (𝜑 ↔ 𝜏))    &   ⊢ (𝑥 = -𝑦 → (𝜑 ↔ 𝜃))    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜂))    &   ⊢ (𝜁 → 𝜓)    &   ⊢ (𝜁 → (𝑦 ∈ ℕ0 → (𝜒 → 𝜏)))    &   ⊢ (𝜁 → (𝑦 ∈ ℕ → (𝜒 → 𝜃)))    ⇒   ⊢ (𝜁 → (𝐴 ∈ ℤ → 𝜂))
Theorem	btwnz 9703*	Any real number can be sandwiched between two integers. Exercise 2 of [Apostol] p. 28. (Contributed by NM, 10-Nov-2004.)
⊢ (𝐴 ∈ ℝ → (∃𝑥 ∈ ℤ 𝑥 < 𝐴 ∧ ∃𝑦 ∈ ℤ 𝐴 < 𝑦))
Theorem	nn0zd 9704	A positive integer is an integer. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℕ0)    ⇒   ⊢ (𝜑 → 𝐴 ∈ ℤ)
Theorem	nnzd 9705	A nonnegative integer is an integer. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    ⇒   ⊢ (𝜑 → 𝐴 ∈ ℤ)
Theorem	zred 9706	An integer is a real number. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℤ)    ⇒   ⊢ (𝜑 → 𝐴 ∈ ℝ)
Theorem	zcnd 9707	An integer is a complex number. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℤ)    ⇒   ⊢ (𝜑 → 𝐴 ∈ ℂ)
Theorem	znegcld 9708	Closure law for negative integers. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℤ)    ⇒   ⊢ (𝜑 → -𝐴 ∈ ℤ)
Theorem	peano2zd 9709	Deduction from second Peano postulate generalized to integers. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℤ)    ⇒   ⊢ (𝜑 → (𝐴 + 1) ∈ ℤ)
Theorem	zaddcld 9710	Closure of addition of integers. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℤ)    &   ⊢ (𝜑 → 𝐵 ∈ ℤ)    ⇒   ⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℤ)
Theorem	zsubcld 9711	Closure of subtraction of integers. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℤ)    &   ⊢ (𝜑 → 𝐵 ∈ ℤ)    ⇒   ⊢ (𝜑 → (𝐴 − 𝐵) ∈ ℤ)
Theorem	zmulcld 9712	Closure of multiplication of integers. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℤ)    &   ⊢ (𝜑 → 𝐵 ∈ ℤ)    ⇒   ⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℤ)
Theorem	zadd2cl 9713	Increasing an integer by 2 results in an integer. (Contributed by Alexander van der Vekens, 16-Sep-2018.)
⊢ (𝑁 ∈ ℤ → (𝑁 + 2) ∈ ℤ)
Theorem	btwnapz 9714	A number between an integer and its successor is apart from any integer. (Contributed by Jim Kingdon, 6-Jan-2023.)
⊢ (𝜑 → 𝐴 ∈ ℤ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℤ)    &   ⊢ (𝜑 → 𝐴 < 𝐵)    &   ⊢ (𝜑 → 𝐵 < (𝐴 + 1))    ⇒   ⊢ (𝜑 → 𝐵 # 𝐶)
4.4.10  Decimal arithmetic
Syntax	cdc 9715	Constant used for decimal constructor.
class ;𝐴𝐵
Definition	df-dec 9716	Define the "decimal constructor", which is used to build up "decimal integers" or "numeric terms" in base 10. For example, (;;;1000 + ;;;2000) = ;;;3000 1kp2ke3k 16541. (Contributed by Mario Carneiro, 17-Apr-2015.) (Revised by AV, 1-Aug-2021.)
⊢ ;𝐴𝐵 = (((9 + 1) · 𝐴) + 𝐵)
Theorem	9p1e10 9717	9 + 1 = 10. (Contributed by Mario Carneiro, 18-Apr-2015.) (Revised by Stanislas Polu, 7-Apr-2020.) (Revised by AV, 1-Aug-2021.)
⊢ (9 + 1) = ;10
Theorem	dfdec10 9718	Version of the definition of the "decimal constructor" using ;10 instead of the symbol 10. Of course, this statement cannot be used as definition, because it uses the "decimal constructor". (Contributed by AV, 1-Aug-2021.)
⊢ ;𝐴𝐵 = ((;10 · 𝐴) + 𝐵)
Theorem	deceq1 9719	Equality theorem for the decimal constructor. (Contributed by Mario Carneiro, 17-Apr-2015.) (Revised by AV, 6-Sep-2021.)
⊢ (𝐴 = 𝐵 → ;𝐴𝐶 = ;𝐵𝐶)
Theorem	deceq2 9720	Equality theorem for the decimal constructor. (Contributed by Mario Carneiro, 17-Apr-2015.) (Revised by AV, 6-Sep-2021.)
⊢ (𝐴 = 𝐵 → ;𝐶𝐴 = ;𝐶𝐵)
Theorem	deceq1i 9721	Equality theorem for the decimal constructor. (Contributed by Mario Carneiro, 17-Apr-2015.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ ;𝐴𝐶 = ;𝐵𝐶
Theorem	deceq2i 9722	Equality theorem for the decimal constructor. (Contributed by Mario Carneiro, 17-Apr-2015.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ ;𝐶𝐴 = ;𝐶𝐵
Theorem	deceq12i 9723	Equality theorem for the decimal constructor. (Contributed by Mario Carneiro, 17-Apr-2015.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ ;𝐴𝐶 = ;𝐵𝐷
Theorem	numnncl 9724	Closure for a numeral (with units place). (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝑇 ∈ ℕ0    &   ⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ    ⇒   ⊢ ((𝑇 · 𝐴) + 𝐵) ∈ ℕ
Theorem	num0u 9725	Add a zero in the units place. (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝑇 ∈ ℕ0    &   ⊢ 𝐴 ∈ ℕ0    ⇒   ⊢ (𝑇 · 𝐴) = ((𝑇 · 𝐴) + 0)
Theorem	num0h 9726	Add a zero in the higher places. (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝑇 ∈ ℕ0    &   ⊢ 𝐴 ∈ ℕ0    ⇒   ⊢ 𝐴 = ((𝑇 · 0) + 𝐴)
Theorem	numcl 9727	Closure for a decimal integer (with units place). (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝑇 ∈ ℕ0    &   ⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    ⇒   ⊢ ((𝑇 · 𝐴) + 𝐵) ∈ ℕ0
Theorem	numsuc 9728	The successor of a decimal integer (no carry). (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝑇 ∈ ℕ0    &   ⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ (𝐵 + 1) = 𝐶    &   ⊢ 𝑁 = ((𝑇 · 𝐴) + 𝐵)    ⇒   ⊢ (𝑁 + 1) = ((𝑇 · 𝐴) + 𝐶)
Theorem	deccl 9729	Closure for a numeral. (Contributed by Mario Carneiro, 17-Apr-2015.) (Revised by AV, 6-Sep-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    ⇒   ⊢ ;𝐴𝐵 ∈ ℕ0
Theorem	10nn 9730	10 is a positive integer. (Contributed by NM, 8-Nov-2012.) (Revised by AV, 6-Sep-2021.)
⊢ ;10 ∈ ℕ
Theorem	10pos 9731	The number 10 is positive. (Contributed by NM, 5-Feb-2007.) (Revised by AV, 8-Sep-2021.)
⊢ 0 < ;10
Theorem	10nn0 9732	10 is a nonnegative integer. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.)
⊢ ;10 ∈ ℕ0
Theorem	10re 9733	The number 10 is real. (Contributed by NM, 5-Feb-2007.) (Revised by AV, 8-Sep-2021.)
⊢ ;10 ∈ ℝ
Theorem	decnncl 9734	Closure for a numeral. (Contributed by Mario Carneiro, 17-Apr-2015.) (Revised by AV, 6-Sep-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ    ⇒   ⊢ ;𝐴𝐵 ∈ ℕ
Theorem	dec0u 9735	Add a zero in the units place. (Contributed by Mario Carneiro, 17-Apr-2015.) (Revised by AV, 6-Sep-2021.)
⊢ 𝐴 ∈ ℕ0    ⇒   ⊢ (;10 · 𝐴) = ;𝐴0
Theorem	dec0h 9736	Add a zero in the higher places. (Contributed by Mario Carneiro, 17-Apr-2015.) (Revised by AV, 6-Sep-2021.)
⊢ 𝐴 ∈ ℕ0    ⇒   ⊢ 𝐴 = ;0𝐴
Theorem	numnncl2 9737	Closure for a decimal integer (zero units place). (Contributed by Mario Carneiro, 9-Mar-2015.)
⊢ 𝑇 ∈ ℕ    &   ⊢ 𝐴 ∈ ℕ    ⇒   ⊢ ((𝑇 · 𝐴) + 0) ∈ ℕ
Theorem	decnncl2 9738	Closure for a decimal integer (zero units place). (Contributed by Mario Carneiro, 17-Apr-2015.) (Revised by AV, 6-Sep-2021.)
⊢ 𝐴 ∈ ℕ    ⇒   ⊢ ;𝐴0 ∈ ℕ
Theorem	numlt 9739	Comparing two decimal integers (equal higher places). (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝑇 ∈ ℕ    &   ⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ    &   ⊢ 𝐵 < 𝐶    ⇒   ⊢ ((𝑇 · 𝐴) + 𝐵) < ((𝑇 · 𝐴) + 𝐶)
Theorem	numltc 9740	Comparing two decimal integers (unequal higher places). (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝑇 ∈ ℕ    &   ⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℕ0    &   ⊢ 𝐶 < 𝑇    &   ⊢ 𝐴 < 𝐵    ⇒   ⊢ ((𝑇 · 𝐴) + 𝐶) < ((𝑇 · 𝐵) + 𝐷)
Theorem	le9lt10 9741	A "decimal digit" (i.e. a nonnegative integer less than or equal to 9) is less then 10. (Contributed by AV, 8-Sep-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐴 ≤ 9    ⇒   ⊢ 𝐴 < ;10
Theorem	declt 9742	Comparing two decimal integers (equal higher places). (Contributed by Mario Carneiro, 17-Apr-2015.) (Revised by AV, 6-Sep-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ    &   ⊢ 𝐵 < 𝐶    ⇒   ⊢ ;𝐴𝐵 < ;𝐴𝐶
Theorem	decltc 9743	Comparing two decimal integers (unequal higher places). (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by AV, 6-Sep-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℕ0    &   ⊢ 𝐶 < ;10    &   ⊢ 𝐴 < 𝐵    ⇒   ⊢ ;𝐴𝐶 < ;𝐵𝐷
Theorem	declth 9744	Comparing two decimal integers (unequal higher places). (Contributed by AV, 8-Sep-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℕ0    &   ⊢ 𝐶 ≤ 9    &   ⊢ 𝐴 < 𝐵    ⇒   ⊢ ;𝐴𝐶 < ;𝐵𝐷
Theorem	decsuc 9745	The successor of a decimal integer (no carry). (Contributed by Mario Carneiro, 17-Apr-2015.) (Revised by AV, 6-Sep-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ (𝐵 + 1) = 𝐶    &   ⊢ 𝑁 = ;𝐴𝐵    ⇒   ⊢ (𝑁 + 1) = ;𝐴𝐶
Theorem	3declth 9746	Comparing two decimal integers with three "digits" (unequal higher places). (Contributed by AV, 8-Sep-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℕ0    &   ⊢ 𝐸 ∈ ℕ0    &   ⊢ 𝐹 ∈ ℕ0    &   ⊢ 𝐴 < 𝐵    &   ⊢ 𝐶 ≤ 9    &   ⊢ 𝐸 ≤ 9    ⇒   ⊢ ;;𝐴𝐶𝐸 < ;;𝐵𝐷𝐹
Theorem	3decltc 9747	Comparing two decimal integers with three "digits" (unequal higher places). (Contributed by AV, 15-Jun-2021.) (Revised by AV, 6-Sep-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℕ0    &   ⊢ 𝐸 ∈ ℕ0    &   ⊢ 𝐹 ∈ ℕ0    &   ⊢ 𝐴 < 𝐵    &   ⊢ 𝐶 < ;10    &   ⊢ 𝐸 < ;10    ⇒   ⊢ ;;𝐴𝐶𝐸 < ;;𝐵𝐷𝐹
Theorem	decle 9748	Comparing two decimal integers (equal higher places). (Contributed by AV, 17-Aug-2021.) (Revised by AV, 8-Sep-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐵 ≤ 𝐶    ⇒   ⊢ ;𝐴𝐵 ≤ ;𝐴𝐶
Theorem	decleh 9749	Comparing two decimal integers (unequal higher places). (Contributed by AV, 17-Aug-2021.) (Revised by AV, 8-Sep-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℕ0    &   ⊢ 𝐶 ≤ 9    &   ⊢ 𝐴 < 𝐵    ⇒   ⊢ ;𝐴𝐶 ≤ ;𝐵𝐷
Theorem	declei 9750	Comparing a digit to a decimal integer. (Contributed by AV, 17-Aug-2021.)
⊢ 𝐴 ∈ ℕ    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐶 ≤ 9    ⇒   ⊢ 𝐶 ≤ ;𝐴𝐵
Theorem	numlti 9751	Comparing a digit to a decimal integer. (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝑇 ∈ ℕ    &   ⊢ 𝐴 ∈ ℕ    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐶 < 𝑇    ⇒   ⊢ 𝐶 < ((𝑇 · 𝐴) + 𝐵)
Theorem	declti 9752	Comparing a digit to a decimal integer. (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by AV, 6-Sep-2021.)
⊢ 𝐴 ∈ ℕ    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐶 < ;10    ⇒   ⊢ 𝐶 < ;𝐴𝐵
Theorem	decltdi 9753	Comparing a digit to a decimal integer. (Contributed by AV, 8-Sep-2021.)
⊢ 𝐴 ∈ ℕ    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐶 ≤ 9    ⇒   ⊢ 𝐶 < ;𝐴𝐵
Theorem	numsucc 9754	The successor of a decimal integer (with carry). (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝑌 ∈ ℕ0    &   ⊢ 𝑇 = (𝑌 + 1)    &   ⊢ 𝐴 ∈ ℕ0    &   ⊢ (𝐴 + 1) = 𝐵    &   ⊢ 𝑁 = ((𝑇 · 𝐴) + 𝑌)    ⇒   ⊢ (𝑁 + 1) = ((𝑇 · 𝐵) + 0)
Theorem	decsucc 9755	The successor of a decimal integer (with carry). (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by AV, 6-Sep-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ (𝐴 + 1) = 𝐵    &   ⊢ 𝑁 = ;𝐴9    ⇒   ⊢ (𝑁 + 1) = ;𝐵0
Theorem	1e0p1 9756	The successor of zero. (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 1 = (0 + 1)
Theorem	dec10p 9757	Ten plus an integer. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.)
⊢ (;10 + 𝐴) = ;1𝐴
Theorem	numma 9758	Perform a multiply-add of two decimal integers 𝑀 and 𝑁 against a fixed multiplicand 𝑃 (no carry). (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝑇 ∈ ℕ0    &   ⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℕ0    &   ⊢ 𝑀 = ((𝑇 · 𝐴) + 𝐵)    &   ⊢ 𝑁 = ((𝑇 · 𝐶) + 𝐷)    &   ⊢ 𝑃 ∈ ℕ0    &   ⊢ ((𝐴 · 𝑃) + 𝐶) = 𝐸    &   ⊢ ((𝐵 · 𝑃) + 𝐷) = 𝐹    ⇒   ⊢ ((𝑀 · 𝑃) + 𝑁) = ((𝑇 · 𝐸) + 𝐹)
Theorem	nummac 9759	Perform a multiply-add of two decimal integers 𝑀 and 𝑁 against a fixed multiplicand 𝑃 (with carry). (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝑇 ∈ ℕ0    &   ⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℕ0    &   ⊢ 𝑀 = ((𝑇 · 𝐴) + 𝐵)    &   ⊢ 𝑁 = ((𝑇 · 𝐶) + 𝐷)    &   ⊢ 𝑃 ∈ ℕ0    &   ⊢ 𝐹 ∈ ℕ0    &   ⊢ 𝐺 ∈ ℕ0    &   ⊢ ((𝐴 · 𝑃) + (𝐶 + 𝐺)) = 𝐸    &   ⊢ ((𝐵 · 𝑃) + 𝐷) = ((𝑇 · 𝐺) + 𝐹)    ⇒   ⊢ ((𝑀 · 𝑃) + 𝑁) = ((𝑇 · 𝐸) + 𝐹)
Theorem	numma2c 9760	Perform a multiply-add of two decimal integers 𝑀 and 𝑁 against a fixed multiplicand 𝑃 (with carry). (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝑇 ∈ ℕ0    &   ⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℕ0    &   ⊢ 𝑀 = ((𝑇 · 𝐴) + 𝐵)    &   ⊢ 𝑁 = ((𝑇 · 𝐶) + 𝐷)    &   ⊢ 𝑃 ∈ ℕ0    &   ⊢ 𝐹 ∈ ℕ0    &   ⊢ 𝐺 ∈ ℕ0    &   ⊢ ((𝑃 · 𝐴) + (𝐶 + 𝐺)) = 𝐸    &   ⊢ ((𝑃 · 𝐵) + 𝐷) = ((𝑇 · 𝐺) + 𝐹)    ⇒   ⊢ ((𝑃 · 𝑀) + 𝑁) = ((𝑇 · 𝐸) + 𝐹)
Theorem	numadd 9761	Add two decimal integers 𝑀 and 𝑁 (no carry). (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝑇 ∈ ℕ0    &   ⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℕ0    &   ⊢ 𝑀 = ((𝑇 · 𝐴) + 𝐵)    &   ⊢ 𝑁 = ((𝑇 · 𝐶) + 𝐷)    &   ⊢ (𝐴 + 𝐶) = 𝐸    &   ⊢ (𝐵 + 𝐷) = 𝐹    ⇒   ⊢ (𝑀 + 𝑁) = ((𝑇 · 𝐸) + 𝐹)
Theorem	numaddc 9762	Add two decimal integers 𝑀 and 𝑁 (with carry). (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝑇 ∈ ℕ0    &   ⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℕ0    &   ⊢ 𝑀 = ((𝑇 · 𝐴) + 𝐵)    &   ⊢ 𝑁 = ((𝑇 · 𝐶) + 𝐷)    &   ⊢ 𝐹 ∈ ℕ0    &   ⊢ ((𝐴 + 𝐶) + 1) = 𝐸    &   ⊢ (𝐵 + 𝐷) = ((𝑇 · 1) + 𝐹)    ⇒   ⊢ (𝑀 + 𝑁) = ((𝑇 · 𝐸) + 𝐹)
Theorem	nummul1c 9763	The product of a decimal integer with a number. (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝑇 ∈ ℕ0    &   ⊢ 𝑃 ∈ ℕ0    &   ⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝑁 = ((𝑇 · 𝐴) + 𝐵)    &   ⊢ 𝐷 ∈ ℕ0    &   ⊢ 𝐸 ∈ ℕ0    &   ⊢ ((𝐴 · 𝑃) + 𝐸) = 𝐶    &   ⊢ (𝐵 · 𝑃) = ((𝑇 · 𝐸) + 𝐷)    ⇒   ⊢ (𝑁 · 𝑃) = ((𝑇 · 𝐶) + 𝐷)
Theorem	nummul2c 9764	The product of a decimal integer with a number (with carry). (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝑇 ∈ ℕ0    &   ⊢ 𝑃 ∈ ℕ0    &   ⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝑁 = ((𝑇 · 𝐴) + 𝐵)    &   ⊢ 𝐷 ∈ ℕ0    &   ⊢ 𝐸 ∈ ℕ0    &   ⊢ ((𝑃 · 𝐴) + 𝐸) = 𝐶    &   ⊢ (𝑃 · 𝐵) = ((𝑇 · 𝐸) + 𝐷)    ⇒   ⊢ (𝑃 · 𝑁) = ((𝑇 · 𝐶) + 𝐷)
Theorem	decma 9765	Perform a multiply-add of two numerals 𝑀 and 𝑁 against a fixed multiplicand 𝑃 (no carry). (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by AV, 6-Sep-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℕ0    &   ⊢ 𝑀 = ;𝐴𝐵    &   ⊢ 𝑁 = ;𝐶𝐷    &   ⊢ 𝑃 ∈ ℕ0    &   ⊢ ((𝐴 · 𝑃) + 𝐶) = 𝐸    &   ⊢ ((𝐵 · 𝑃) + 𝐷) = 𝐹    ⇒   ⊢ ((𝑀 · 𝑃) + 𝑁) = ;𝐸𝐹
Theorem	decmac 9766	Perform a multiply-add of two numerals 𝑀 and 𝑁 against a fixed multiplicand 𝑃 (with carry). (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by AV, 6-Sep-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℕ0    &   ⊢ 𝑀 = ;𝐴𝐵    &   ⊢ 𝑁 = ;𝐶𝐷    &   ⊢ 𝑃 ∈ ℕ0    &   ⊢ 𝐹 ∈ ℕ0    &   ⊢ 𝐺 ∈ ℕ0    &   ⊢ ((𝐴 · 𝑃) + (𝐶 + 𝐺)) = 𝐸    &   ⊢ ((𝐵 · 𝑃) + 𝐷) = ;𝐺𝐹    ⇒   ⊢ ((𝑀 · 𝑃) + 𝑁) = ;𝐸𝐹
Theorem	decma2c 9767	Perform a multiply-add of two numerals 𝑀 and 𝑁 against a fixed multiplier 𝑃 (with carry). (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by AV, 6-Sep-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℕ0    &   ⊢ 𝑀 = ;𝐴𝐵    &   ⊢ 𝑁 = ;𝐶𝐷    &   ⊢ 𝑃 ∈ ℕ0    &   ⊢ 𝐹 ∈ ℕ0    &   ⊢ 𝐺 ∈ ℕ0    &   ⊢ ((𝑃 · 𝐴) + (𝐶 + 𝐺)) = 𝐸    &   ⊢ ((𝑃 · 𝐵) + 𝐷) = ;𝐺𝐹    ⇒   ⊢ ((𝑃 · 𝑀) + 𝑁) = ;𝐸𝐹
Theorem	decadd 9768	Add two numerals 𝑀 and 𝑁 (no carry). (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by AV, 6-Sep-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℕ0    &   ⊢ 𝑀 = ;𝐴𝐵    &   ⊢ 𝑁 = ;𝐶𝐷    &   ⊢ (𝐴 + 𝐶) = 𝐸    &   ⊢ (𝐵 + 𝐷) = 𝐹    ⇒   ⊢ (𝑀 + 𝑁) = ;𝐸𝐹
Theorem	decaddc 9769	Add two numerals 𝑀 and 𝑁 (with carry). (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by AV, 6-Sep-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℕ0    &   ⊢ 𝑀 = ;𝐴𝐵    &   ⊢ 𝑁 = ;𝐶𝐷    &   ⊢ ((𝐴 + 𝐶) + 1) = 𝐸    &   ⊢ 𝐹 ∈ ℕ0    &   ⊢ (𝐵 + 𝐷) = ;1𝐹    ⇒   ⊢ (𝑀 + 𝑁) = ;𝐸𝐹
Theorem	decaddc2 9770	Add two numerals 𝑀 and 𝑁 (with carry). (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by AV, 6-Sep-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℕ0    &   ⊢ 𝑀 = ;𝐴𝐵    &   ⊢ 𝑁 = ;𝐶𝐷    &   ⊢ ((𝐴 + 𝐶) + 1) = 𝐸    &   ⊢ (𝐵 + 𝐷) = ;10    ⇒   ⊢ (𝑀 + 𝑁) = ;𝐸0
Theorem	decrmanc 9771	Perform a multiply-add of two numerals 𝑀 and 𝑁 against a fixed multiplicand 𝑃 (no carry). (Contributed by AV, 16-Sep-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝑁 ∈ ℕ0    &   ⊢ 𝑀 = ;𝐴𝐵    &   ⊢ 𝑃 ∈ ℕ0    &   ⊢ (𝐴 · 𝑃) = 𝐸    &   ⊢ ((𝐵 · 𝑃) + 𝑁) = 𝐹    ⇒   ⊢ ((𝑀 · 𝑃) + 𝑁) = ;𝐸𝐹
Theorem	decrmac 9772	Perform a multiply-add of two numerals 𝑀 and 𝑁 against a fixed multiplicand 𝑃 (with carry). (Contributed by AV, 16-Sep-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝑁 ∈ ℕ0    &   ⊢ 𝑀 = ;𝐴𝐵    &   ⊢ 𝑃 ∈ ℕ0    &   ⊢ 𝐹 ∈ ℕ0    &   ⊢ 𝐺 ∈ ℕ0    &   ⊢ ((𝐴 · 𝑃) + 𝐺) = 𝐸    &   ⊢ ((𝐵 · 𝑃) + 𝑁) = ;𝐺𝐹    ⇒   ⊢ ((𝑀 · 𝑃) + 𝑁) = ;𝐸𝐹
Theorem	decaddm10 9773	The sum of two multiples of 10 is a multiple of 10. (Contributed by AV, 30-Jul-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    ⇒   ⊢ (;𝐴0 + ;𝐵0) = ;(𝐴 + 𝐵)0
Theorem	decaddi 9774	Add two numerals 𝑀 and 𝑁 (no carry). (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝑁 ∈ ℕ0    &   ⊢ 𝑀 = ;𝐴𝐵    &   ⊢ (𝐵 + 𝑁) = 𝐶    ⇒   ⊢ (𝑀 + 𝑁) = ;𝐴𝐶
Theorem	decaddci 9775	Add two numerals 𝑀 and 𝑁 (no carry). (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝑁 ∈ ℕ0    &   ⊢ 𝑀 = ;𝐴𝐵    &   ⊢ (𝐴 + 1) = 𝐷    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ (𝐵 + 𝑁) = ;1𝐶    ⇒   ⊢ (𝑀 + 𝑁) = ;𝐷𝐶
Theorem	decaddci2 9776	Add two numerals 𝑀 and 𝑁 (no carry). (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by AV, 6-Sep-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝑁 ∈ ℕ0    &   ⊢ 𝑀 = ;𝐴𝐵    &   ⊢ (𝐴 + 1) = 𝐷    &   ⊢ (𝐵 + 𝑁) = ;10    ⇒   ⊢ (𝑀 + 𝑁) = ;𝐷0
Theorem	decsubi 9777	Difference between a numeral 𝑀 and a nonnegative integer 𝑁 (no underflow). (Contributed by AV, 22-Jul-2021.) (Revised by AV, 6-Sep-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝑁 ∈ ℕ0    &   ⊢ 𝑀 = ;𝐴𝐵    &   ⊢ (𝐴 + 1) = 𝐷    &   ⊢ (𝐵 − 𝑁) = 𝐶    ⇒   ⊢ (𝑀 − 𝑁) = ;𝐴𝐶
Theorem	decmul1 9778	The product of a numeral with a number (no carry). (Contributed by AV, 22-Jul-2021.) (Revised by AV, 6-Sep-2021.)
⊢ 𝑃 ∈ ℕ0    &   ⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝑁 = ;𝐴𝐵    &   ⊢ 𝐷 ∈ ℕ0    &   ⊢ (𝐴 · 𝑃) = 𝐶    &   ⊢ (𝐵 · 𝑃) = 𝐷    ⇒   ⊢ (𝑁 · 𝑃) = ;𝐶𝐷
Theorem	decmul1c 9779	The product of a numeral with a number (with carry). (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by AV, 6-Sep-2021.)
⊢ 𝑃 ∈ ℕ0    &   ⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝑁 = ;𝐴𝐵    &   ⊢ 𝐷 ∈ ℕ0    &   ⊢ 𝐸 ∈ ℕ0    &   ⊢ ((𝐴 · 𝑃) + 𝐸) = 𝐶    &   ⊢ (𝐵 · 𝑃) = ;𝐸𝐷    ⇒   ⊢ (𝑁 · 𝑃) = ;𝐶𝐷
Theorem	decmul2c 9780	The product of a numeral with a number (with carry). (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by AV, 6-Sep-2021.)
⊢ 𝑃 ∈ ℕ0    &   ⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝑁 = ;𝐴𝐵    &   ⊢ 𝐷 ∈ ℕ0    &   ⊢ 𝐸 ∈ ℕ0    &   ⊢ ((𝑃 · 𝐴) + 𝐸) = 𝐶    &   ⊢ (𝑃 · 𝐵) = ;𝐸𝐷    ⇒   ⊢ (𝑃 · 𝑁) = ;𝐶𝐷
Theorem	decmulnc 9781	The product of a numeral with a number (no carry). (Contributed by AV, 15-Jun-2021.)
⊢ 𝑁 ∈ ℕ0    &   ⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    ⇒   ⊢ (𝑁 · ;𝐴𝐵) = ;(𝑁 · 𝐴)(𝑁 · 𝐵)
Theorem	11multnc 9782	The product of 11 (as numeral) with a number (no carry). (Contributed by AV, 15-Jun-2021.)
⊢ 𝑁 ∈ ℕ0    ⇒   ⊢ (𝑁 · ;11) = ;𝑁𝑁
Theorem	decmul10add 9783	A multiplication of a number and a numeral expressed as addition with first summand as multiple of 10. (Contributed by AV, 22-Jul-2021.) (Revised by AV, 6-Sep-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝑀 ∈ ℕ0    &   ⊢ 𝐸 = (𝑀 · 𝐴)    &   ⊢ 𝐹 = (𝑀 · 𝐵)    ⇒   ⊢ (𝑀 · ;𝐴𝐵) = (;𝐸0 + 𝐹)
Theorem	6p5lem 9784	Lemma for 6p5e11 9787 and related theorems. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℕ0    &   ⊢ 𝐸 ∈ ℕ0    &   ⊢ 𝐵 = (𝐷 + 1)    &   ⊢ 𝐶 = (𝐸 + 1)    &   ⊢ (𝐴 + 𝐷) = ;1𝐸    ⇒   ⊢ (𝐴 + 𝐵) = ;1𝐶
Theorem	5p5e10 9785	5 + 5 = 10. (Contributed by NM, 5-Feb-2007.) (Revised by Stanislas Polu, 7-Apr-2020.) (Revised by AV, 6-Sep-2021.)
⊢ (5 + 5) = ;10
Theorem	6p4e10 9786	6 + 4 = 10. (Contributed by NM, 5-Feb-2007.) (Revised by Stanislas Polu, 7-Apr-2020.) (Revised by AV, 6-Sep-2021.)
⊢ (6 + 4) = ;10
Theorem	6p5e11 9787	6 + 5 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.)
⊢ (6 + 5) = ;11
Theorem	6p6e12 9788	6 + 6 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (6 + 6) = ;12
Theorem	7p3e10 9789	7 + 3 = 10. (Contributed by NM, 5-Feb-2007.) (Revised by Stanislas Polu, 7-Apr-2020.) (Revised by AV, 6-Sep-2021.)
⊢ (7 + 3) = ;10
Theorem	7p4e11 9790	7 + 4 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.)
⊢ (7 + 4) = ;11
Theorem	7p5e12 9791	7 + 5 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (7 + 5) = ;12
Theorem	7p6e13 9792	7 + 6 = 13. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (7 + 6) = ;13
Theorem	7p7e14 9793	7 + 7 = 14. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (7 + 7) = ;14
Theorem	8p2e10 9794	8 + 2 = 10. (Contributed by NM, 5-Feb-2007.) (Revised by Stanislas Polu, 7-Apr-2020.) (Revised by AV, 6-Sep-2021.)
⊢ (8 + 2) = ;10
Theorem	8p3e11 9795	8 + 3 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.)
⊢ (8 + 3) = ;11
Theorem	8p4e12 9796	8 + 4 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (8 + 4) = ;12
Theorem	8p5e13 9797	8 + 5 = 13. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (8 + 5) = ;13
Theorem	8p6e14 9798	8 + 6 = 14. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (8 + 6) = ;14
Theorem	8p7e15 9799	8 + 7 = 15. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (8 + 7) = ;15
Theorem	8p8e16 9800	8 + 8 = 16. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (8 + 8) = ;16