P. 82 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 8101-8200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	peano2uz2 8101*	Second Peano postulate for upper integers. (Contributed by NM, 3-Oct-2004.)
⊢ ((A ∈ ℤ ∧ B ∈ {x ∈ ℤ ∣ A ≤ x}) → (B + 1) ∈ {x ∈ ℤ ∣ A ≤ x})
Theorem	peano5uzti 8102*	Peano's inductive postulate for upper integers. (Contributed by NM, 6-Jul-2005.) (Revised by Mario Carneiro, 25-Jul-2013.)
⊢ (𝑁 ∈ ℤ → ((𝑁 ∈ A ∧ ∀x ∈ A (x + 1) ∈ A) → {𝑘 ∈ ℤ ∣ 𝑁 ≤ 𝑘} ⊆ A))
Theorem	peano5uzi 8103*	Peano's inductive postulate for upper integers. (Contributed by NM, 6-Jul-2005.) (Revised by Mario Carneiro, 3-May-2014.)
⊢ 𝑁 ∈ ℤ    ⇒   ⊢ ((𝑁 ∈ A ∧ ∀x ∈ A (x + 1) ∈ A) → {𝑘 ∈ ℤ ∣ 𝑁 ≤ 𝑘} ⊆ A)
Theorem	dfuzi 8104*	An expression for the upper integers that start at 𝑁 that is analogous to dfnn2 7677 for positive integers. (Contributed by NM, 6-Jul-2005.) (Proof shortened by Mario Carneiro, 3-May-2014.)
⊢ 𝑁 ∈ ℤ    ⇒   ⊢ {z ∈ ℤ ∣ 𝑁 ≤ z} = ∩ {x ∣ (𝑁 ∈ x ∧ ∀y ∈ x (y + 1) ∈ x)}
Theorem	uzind 8105*	Induction on the upper integers that start at 𝑀. The first four hypotheses give us the substitution instances we need; the last two are the basis and the induction step. (Contributed by NM, 5-Jul-2005.)
⊢ (𝑗 = 𝑀 → (φ ↔ ψ))    &   ⊢ (𝑗 = 𝑘 → (φ ↔ χ))    &   ⊢ (𝑗 = (𝑘 + 1) → (φ ↔ θ))    &   ⊢ (𝑗 = 𝑁 → (φ ↔ τ))    &   ⊢ (𝑀 ∈ ℤ → ψ)    &   ⊢ ((𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ ∧ 𝑀 ≤ 𝑘) → (χ → θ))    ⇒   ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) → τ)
Theorem	uzind2 8106*	Induction on the upper integers that start after an integer 𝑀. The first four hypotheses give us the substitution instances we need; the last two are the basis and the induction step. (Contributed by NM, 25-Jul-2005.)
⊢ (𝑗 = (𝑀 + 1) → (φ ↔ ψ))    &   ⊢ (𝑗 = 𝑘 → (φ ↔ χ))    &   ⊢ (𝑗 = (𝑘 + 1) → (φ ↔ θ))    &   ⊢ (𝑗 = 𝑁 → (φ ↔ τ))    &   ⊢ (𝑀 ∈ ℤ → ψ)    &   ⊢ ((𝑀 ∈ ℤ ∧ 𝑘 ∈ ℤ ∧ 𝑀 < 𝑘) → (χ → θ))    ⇒   ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 < 𝑁) → τ)
Theorem	uzind3 8107*	Induction on the upper integers that start at an integer 𝑀. The first four hypotheses give us the substitution instances we need, and the last two are the basis and the induction step. (Contributed by NM, 26-Jul-2005.)
⊢ (𝑗 = 𝑀 → (φ ↔ ψ))    &   ⊢ (𝑗 = 𝑚 → (φ ↔ χ))    &   ⊢ (𝑗 = (𝑚 + 1) → (φ ↔ θ))    &   ⊢ (𝑗 = 𝑁 → (φ ↔ τ))    &   ⊢ (𝑀 ∈ ℤ → ψ)    &   ⊢ ((𝑀 ∈ ℤ ∧ 𝑚 ∈ {𝑘 ∈ ℤ ∣ 𝑀 ≤ 𝑘}) → (χ → θ))    ⇒   ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ {𝑘 ∈ ℤ ∣ 𝑀 ≤ 𝑘}) → τ)
Theorem	nn0ind 8108*	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. (Contributed by NM, 13-May-2004.)
⊢ (x = 0 → (φ ↔ ψ))    &   ⊢ (x = y → (φ ↔ χ))    &   ⊢ (x = (y + 1) → (φ ↔ θ))    &   ⊢ (x = A → (φ ↔ τ))    &   ⊢ ψ    &   ⊢ (y ∈ ℕ0 → (χ → θ))    ⇒   ⊢ (A ∈ ℕ0 → τ)
Theorem	fzind 8109*	Induction on the integers from 𝑀 to 𝑁 inclusive . The first four hypotheses give us the substitution instances we need; the last two are the basis and the induction step. (Contributed by Paul Chapman, 31-Mar-2011.)
⊢ (x = 𝑀 → (φ ↔ ψ))    &   ⊢ (x = y → (φ ↔ χ))    &   ⊢ (x = (y + 1) → (φ ↔ θ))    &   ⊢ (x = 𝐾 → (φ ↔ τ))    &   ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) → ψ)    &   ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (y ∈ ℤ ∧ 𝑀 ≤ y ∧ y < 𝑁)) → (χ → θ))    ⇒   ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁)) → τ)
Theorem	fnn0ind 8110*	Induction on the integers from 0 to 𝑁 inclusive . The first four hypotheses give us the substitution instances we need; the last two are the basis and the induction step. (Contributed by Paul Chapman, 31-Mar-2011.)
⊢ (x = 0 → (φ ↔ ψ))    &   ⊢ (x = y → (φ ↔ χ))    &   ⊢ (x = (y + 1) → (φ ↔ θ))    &   ⊢ (x = 𝐾 → (φ ↔ τ))    &   ⊢ (𝑁 ∈ ℕ0 → ψ)    &   ⊢ ((𝑁 ∈ ℕ0 ∧ y ∈ ℕ0 ∧ y < 𝑁) → (χ → θ))    ⇒   ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0 ∧ 𝐾 ≤ 𝑁) → τ)
Theorem	nn0ind-raph 8111*	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.)
⊢ (x = 0 → (φ ↔ ψ))    &   ⊢ (x = y → (φ ↔ χ))    &   ⊢ (x = (y + 1) → (φ ↔ θ))    &   ⊢ (x = A → (φ ↔ τ))    &   ⊢ ψ    &   ⊢ (y ∈ ℕ0 → (χ → θ))    ⇒   ⊢ (A ∈ ℕ0 → τ)
Theorem	zindd 8112*	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.)
⊢ (x = 0 → (φ ↔ ψ))    &   ⊢ (x = y → (φ ↔ χ))    &   ⊢ (x = (y + 1) → (φ ↔ τ))    &   ⊢ (x = -y → (φ ↔ θ))    &   ⊢ (x = A → (φ ↔ η))    &   ⊢ (ζ → ψ)    &   ⊢ (ζ → (y ∈ ℕ0 → (χ → τ)))    &   ⊢ (ζ → (y ∈ ℕ → (χ → θ)))    ⇒   ⊢ (ζ → (A ∈ ℤ → η))
Theorem	btwnz 8113*	Any real number can be sandwiched between two integers. Exercise 2 of [Apostol] p. 28. (Contributed by NM, 10-Nov-2004.)
⊢ (A ∈ ℝ → (∃x ∈ ℤ x < A ∧ ∃y ∈ ℤ A < y))
Theorem	nn0zd 8114	A positive integer is an integer. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℕ0)    ⇒   ⊢ (φ → A ∈ ℤ)
Theorem	nnzd 8115	A nonnegative integer is an integer. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℕ)    ⇒   ⊢ (φ → A ∈ ℤ)
Theorem	zred 8116	An integer is a real number. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℤ)    ⇒   ⊢ (φ → A ∈ ℝ)
Theorem	zcnd 8117	An integer is a complex number. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℤ)    ⇒   ⊢ (φ → A ∈ ℂ)
Theorem	znegcld 8118	Closure law for negative integers. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℤ)    ⇒   ⊢ (φ → -A ∈ ℤ)
Theorem	peano2zd 8119	Deduction from second Peano postulate generalized to integers. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℤ)    ⇒   ⊢ (φ → (A + 1) ∈ ℤ)
Theorem	zaddcld 8120	Closure of addition of integers. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℤ)    &   ⊢ (φ → B ∈ ℤ)    ⇒   ⊢ (φ → (A + B) ∈ ℤ)
Theorem	zsubcld 8121	Closure of subtraction of integers. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℤ)    &   ⊢ (φ → B ∈ ℤ)    ⇒   ⊢ (φ → (A − B) ∈ ℤ)
Theorem	zmulcld 8122	Closure of multiplication of integers. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℤ)    &   ⊢ (φ → B ∈ ℤ)    ⇒   ⊢ (φ → (A · B) ∈ ℤ)
Theorem	zadd2cl 8123	Increasing an integer by 2 results in an integer. (Contributed by Alexander van der Vekens, 16-Sep-2018.)
⊢ (𝑁 ∈ ℤ → (𝑁 + 2) ∈ ℤ)
3.4.9  Decimal arithmetic
Syntax	cdc 8124	Constant used for decimal constructor.
class ;AB
Definition	df-dec 8125	Define the "decimal constructor", which is used to build up "decimal integers" or "numeric terms" in base 10. For example, (;;;1000 + ;;;2000) = ;;;3000. (Contributed by Mario Carneiro, 17-Apr-2015.)
⊢ ;AB = ((10 · A) + B)
Theorem	deceq1 8126	Equality theorem for the decimal constructor. (Contributed by Mario Carneiro, 17-Apr-2015.)
⊢ (A = B → ;A𝐶 = ;B𝐶)
Theorem	deceq2 8127	Equality theorem for the decimal constructor. (Contributed by Mario Carneiro, 17-Apr-2015.)
⊢ (A = B → ;𝐶A = ;𝐶B)
Theorem	deceq1i 8128	Equality theorem for the decimal constructor. (Contributed by Mario Carneiro, 17-Apr-2015.)
⊢ A = B    ⇒   ⊢ ;A𝐶 = ;B𝐶
Theorem	deceq2i 8129	Equality theorem for the decimal constructor. (Contributed by Mario Carneiro, 17-Apr-2015.)
⊢ A = B    ⇒   ⊢ ;𝐶A = ;𝐶B
Theorem	deceq12i 8130	Equality theorem for the decimal constructor. (Contributed by Mario Carneiro, 17-Apr-2015.)
⊢ A = B    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ ;A𝐶 = ;B𝐷
Theorem	numnncl 8131	Closure for a numeral (with units place). (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝑇 ∈ ℕ0    &   ⊢ A ∈ ℕ0    &   ⊢ B ∈ ℕ    ⇒   ⊢ ((𝑇 · A) + B) ∈ ℕ
Theorem	num0u 8132	Add a zero in the units place. (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝑇 ∈ ℕ0    &   ⊢ A ∈ ℕ0    ⇒   ⊢ (𝑇 · A) = ((𝑇 · A) + 0)
Theorem	num0h 8133	Add a zero in the higher places. (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝑇 ∈ ℕ0    &   ⊢ A ∈ ℕ0    ⇒   ⊢ A = ((𝑇 · 0) + A)
Theorem	numcl 8134	Closure for a decimal integer (with units place). (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝑇 ∈ ℕ0    &   ⊢ A ∈ ℕ0    &   ⊢ B ∈ ℕ0    ⇒   ⊢ ((𝑇 · A) + B) ∈ ℕ0
Theorem	numsuc 8135	The successor of a decimal integer (no carry). (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝑇 ∈ ℕ0    &   ⊢ A ∈ ℕ0    &   ⊢ B ∈ ℕ0    &   ⊢ (B + 1) = 𝐶    &   ⊢ 𝑁 = ((𝑇 · A) + B)    ⇒   ⊢ (𝑁 + 1) = ((𝑇 · A) + 𝐶)
Theorem	decnncl 8136	Closure for a numeral. (Contributed by Mario Carneiro, 17-Apr-2015.)
⊢ A ∈ ℕ0    &   ⊢ B ∈ ℕ    ⇒   ⊢ ;AB ∈ ℕ
Theorem	deccl 8137	Closure for a numeral. (Contributed by Mario Carneiro, 17-Apr-2015.)
⊢ A ∈ ℕ0    &   ⊢ B ∈ ℕ0    ⇒   ⊢ ;AB ∈ ℕ0
Theorem	dec0u 8138	Add a zero in the units place. (Contributed by Mario Carneiro, 17-Apr-2015.)
⊢ A ∈ ℕ0    ⇒   ⊢ (10 · A) = ;A0
Theorem	dec0h 8139	Add a zero in the higher places. (Contributed by Mario Carneiro, 17-Apr-2015.)
⊢ A ∈ ℕ0    ⇒   ⊢ A = ;0A
Theorem	numnncl2 8140	Closure for a decimal integer (zero units place). (Contributed by Mario Carneiro, 9-Mar-2015.)
⊢ 𝑇 ∈ ℕ    &   ⊢ A ∈ ℕ    ⇒   ⊢ ((𝑇 · A) + 0) ∈ ℕ
Theorem	decnncl2 8141	Closure for a decimal integer (zero units place). (Contributed by Mario Carneiro, 17-Apr-2015.)
⊢ A ∈ ℕ    ⇒   ⊢ ;A0 ∈ ℕ
Theorem	numlt 8142	Comparing two decimal integers (equal higher places). (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝑇 ∈ ℕ    &   ⊢ A ∈ ℕ0    &   ⊢ B ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ    &   ⊢ B < 𝐶    ⇒   ⊢ ((𝑇 · A) + B) < ((𝑇 · A) + 𝐶)
Theorem	numltc 8143	Comparing two decimal integers (unequal higher places). (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝑇 ∈ ℕ    &   ⊢ A ∈ ℕ0    &   ⊢ B ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℕ0    &   ⊢ 𝐶 < 𝑇    &   ⊢ A < B    ⇒   ⊢ ((𝑇 · A) + 𝐶) < ((𝑇 · B) + 𝐷)
Theorem	declt 8144	Comparing two decimal integers (equal higher places). (Contributed by Mario Carneiro, 17-Apr-2015.)
⊢ A ∈ ℕ0    &   ⊢ B ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ    &   ⊢ B < 𝐶    ⇒   ⊢ ;AB < ;A𝐶
Theorem	decltc 8145	Comparing two decimal integers (unequal higher places). (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ A ∈ ℕ0    &   ⊢ B ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℕ0    &   ⊢ 𝐶 < 10    &   ⊢ A < B    ⇒   ⊢ ;A𝐶 < ;B𝐷
Theorem	decsuc 8146	The successor of a decimal integer (no carry). (Contributed by Mario Carneiro, 17-Apr-2015.)
⊢ A ∈ ℕ0    &   ⊢ B ∈ ℕ0    &   ⊢ (B + 1) = 𝐶    &   ⊢ 𝑁 = ;AB    ⇒   ⊢ (𝑁 + 1) = ;A𝐶
Theorem	numlti 8147	Comparing a digit to a decimal integer. (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝑇 ∈ ℕ    &   ⊢ A ∈ ℕ    &   ⊢ B ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐶 < 𝑇    ⇒   ⊢ 𝐶 < ((𝑇 · A) + B)
Theorem	declti 8148	Comparing a digit to a decimal integer. (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ A ∈ ℕ    &   ⊢ B ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐶 < 10    ⇒   ⊢ 𝐶 < ;AB
Theorem	numsucc 8149	The successor of a decimal integer (with carry). (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝑌 ∈ ℕ0    &   ⊢ 𝑇 = (𝑌 + 1)    &   ⊢ A ∈ ℕ0    &   ⊢ (A + 1) = B    &   ⊢ 𝑁 = ((𝑇 · A) + 𝑌)    ⇒   ⊢ (𝑁 + 1) = ((𝑇 · B) + 0)
Theorem	decsucc 8150	The successor of a decimal integer (with carry). (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ A ∈ ℕ0    &   ⊢ (A + 1) = B    &   ⊢ 𝑁 = ;A9    ⇒   ⊢ (𝑁 + 1) = ;B0
Theorem	1e0p1 8151	The successor of zero. (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 1 = (0 + 1)
Theorem	dec10p 8152	Ten plus an integer. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (10 + A) = ;1A
Theorem	dec10 8153	The decimal form of 10. NB: In our presentations of large numbers later on, we will use our symbol for 10 at the highest digits when advantageous, because we can use this theorem to convert back to "long form" (where each digit is in the range 0-9) with no extra effort. However, we cannot do this for lower digits while maintaining the ease of use of the decimal system, since it requires nontrivial number knowledge (more than just equality theorems) to convert back. (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 10 = ;10
Theorem	numma 8154	Perform a multiply-add of two decimal integers 𝑀 and 𝑁 against a fixed multiplicand 𝑃 (no carry). (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝑇 ∈ ℕ0    &   ⊢ A ∈ ℕ0    &   ⊢ B ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℕ0    &   ⊢ 𝑀 = ((𝑇 · A) + B)    &   ⊢ 𝑁 = ((𝑇 · 𝐶) + 𝐷)    &   ⊢ 𝑃 ∈ ℕ0    &   ⊢ ((A · 𝑃) + 𝐶) = 𝐸    &   ⊢ ((B · 𝑃) + 𝐷) = 𝐹    ⇒   ⊢ ((𝑀 · 𝑃) + 𝑁) = ((𝑇 · 𝐸) + 𝐹)
Theorem	nummac 8155	Perform a multiply-add of two decimal integers 𝑀 and 𝑁 against a fixed multiplicand 𝑃 (with carry). (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝑇 ∈ ℕ0    &   ⊢ A ∈ ℕ0    &   ⊢ B ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℕ0    &   ⊢ 𝑀 = ((𝑇 · A) + B)    &   ⊢ 𝑁 = ((𝑇 · 𝐶) + 𝐷)    &   ⊢ 𝑃 ∈ ℕ0    &   ⊢ 𝐹 ∈ ℕ0    &   ⊢ 𝐺 ∈ ℕ0    &   ⊢ ((A · 𝑃) + (𝐶 + 𝐺)) = 𝐸    &   ⊢ ((B · 𝑃) + 𝐷) = ((𝑇 · 𝐺) + 𝐹)    ⇒   ⊢ ((𝑀 · 𝑃) + 𝑁) = ((𝑇 · 𝐸) + 𝐹)
Theorem	numma2c 8156	Perform a multiply-add of two decimal integers 𝑀 and 𝑁 against a fixed multiplicand 𝑃 (with carry). (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝑇 ∈ ℕ0    &   ⊢ A ∈ ℕ0    &   ⊢ B ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℕ0    &   ⊢ 𝑀 = ((𝑇 · A) + B)    &   ⊢ 𝑁 = ((𝑇 · 𝐶) + 𝐷)    &   ⊢ 𝑃 ∈ ℕ0    &   ⊢ 𝐹 ∈ ℕ0    &   ⊢ 𝐺 ∈ ℕ0    &   ⊢ ((𝑃 · A) + (𝐶 + 𝐺)) = 𝐸    &   ⊢ ((𝑃 · B) + 𝐷) = ((𝑇 · 𝐺) + 𝐹)    ⇒   ⊢ ((𝑃 · 𝑀) + 𝑁) = ((𝑇 · 𝐸) + 𝐹)
Theorem	numadd 8157	Add two decimal integers 𝑀 and 𝑁 (no carry). (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝑇 ∈ ℕ0    &   ⊢ A ∈ ℕ0    &   ⊢ B ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℕ0    &   ⊢ 𝑀 = ((𝑇 · A) + B)    &   ⊢ 𝑁 = ((𝑇 · 𝐶) + 𝐷)    &   ⊢ (A + 𝐶) = 𝐸    &   ⊢ (B + 𝐷) = 𝐹    ⇒   ⊢ (𝑀 + 𝑁) = ((𝑇 · 𝐸) + 𝐹)
Theorem	numaddc 8158	Add two decimal integers 𝑀 and 𝑁 (with carry). (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝑇 ∈ ℕ0    &   ⊢ A ∈ ℕ0    &   ⊢ B ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℕ0    &   ⊢ 𝑀 = ((𝑇 · A) + B)    &   ⊢ 𝑁 = ((𝑇 · 𝐶) + 𝐷)    &   ⊢ 𝐹 ∈ ℕ0    &   ⊢ ((A + 𝐶) + 1) = 𝐸    &   ⊢ (B + 𝐷) = ((𝑇 · 1) + 𝐹)    ⇒   ⊢ (𝑀 + 𝑁) = ((𝑇 · 𝐸) + 𝐹)
Theorem	nummul1c 8159	The product of a decimal integer with a number. (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝑇 ∈ ℕ0    &   ⊢ 𝑃 ∈ ℕ0    &   ⊢ A ∈ ℕ0    &   ⊢ B ∈ ℕ0    &   ⊢ 𝑁 = ((𝑇 · A) + B)    &   ⊢ 𝐷 ∈ ℕ0    &   ⊢ 𝐸 ∈ ℕ0    &   ⊢ ((A · 𝑃) + 𝐸) = 𝐶    &   ⊢ (B · 𝑃) = ((𝑇 · 𝐸) + 𝐷)    ⇒   ⊢ (𝑁 · 𝑃) = ((𝑇 · 𝐶) + 𝐷)
Theorem	nummul2c 8160	The product of a decimal integer with a number (with carry). (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝑇 ∈ ℕ0    &   ⊢ 𝑃 ∈ ℕ0    &   ⊢ A ∈ ℕ0    &   ⊢ B ∈ ℕ0    &   ⊢ 𝑁 = ((𝑇 · A) + B)    &   ⊢ 𝐷 ∈ ℕ0    &   ⊢ 𝐸 ∈ ℕ0    &   ⊢ ((𝑃 · A) + 𝐸) = 𝐶    &   ⊢ (𝑃 · B) = ((𝑇 · 𝐸) + 𝐷)    ⇒   ⊢ (𝑃 · 𝑁) = ((𝑇 · 𝐶) + 𝐷)
Theorem	decma 8161	Perform a multiply-add of two numerals 𝑀 and 𝑁 against a fixed multiplicand 𝑃 (no carry). (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ A ∈ ℕ0    &   ⊢ B ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℕ0    &   ⊢ 𝑀 = ;AB    &   ⊢ 𝑁 = ;𝐶𝐷    &   ⊢ 𝑃 ∈ ℕ0    &   ⊢ ((A · 𝑃) + 𝐶) = 𝐸    &   ⊢ ((B · 𝑃) + 𝐷) = 𝐹    ⇒   ⊢ ((𝑀 · 𝑃) + 𝑁) = ;𝐸𝐹
Theorem	decmac 8162	Perform a multiply-add of two numerals 𝑀 and 𝑁 against a fixed multiplicand 𝑃 (with carry). (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ A ∈ ℕ0    &   ⊢ B ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℕ0    &   ⊢ 𝑀 = ;AB    &   ⊢ 𝑁 = ;𝐶𝐷    &   ⊢ 𝑃 ∈ ℕ0    &   ⊢ 𝐹 ∈ ℕ0    &   ⊢ 𝐺 ∈ ℕ0    &   ⊢ ((A · 𝑃) + (𝐶 + 𝐺)) = 𝐸    &   ⊢ ((B · 𝑃) + 𝐷) = ;𝐺𝐹    ⇒   ⊢ ((𝑀 · 𝑃) + 𝑁) = ;𝐸𝐹
Theorem	decma2c 8163	Perform a multiply-add of two numerals 𝑀 and 𝑁 against a fixed multiplicand 𝑃 (with carry). (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ A ∈ ℕ0    &   ⊢ B ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℕ0    &   ⊢ 𝑀 = ;AB    &   ⊢ 𝑁 = ;𝐶𝐷    &   ⊢ 𝑃 ∈ ℕ0    &   ⊢ 𝐹 ∈ ℕ0    &   ⊢ 𝐺 ∈ ℕ0    &   ⊢ ((𝑃 · A) + (𝐶 + 𝐺)) = 𝐸    &   ⊢ ((𝑃 · B) + 𝐷) = ;𝐺𝐹    ⇒   ⊢ ((𝑃 · 𝑀) + 𝑁) = ;𝐸𝐹
Theorem	decadd 8164	Add two numerals 𝑀 and 𝑁 (no carry). (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ A ∈ ℕ0    &   ⊢ B ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℕ0    &   ⊢ 𝑀 = ;AB    &   ⊢ 𝑁 = ;𝐶𝐷    &   ⊢ (A + 𝐶) = 𝐸    &   ⊢ (B + 𝐷) = 𝐹    ⇒   ⊢ (𝑀 + 𝑁) = ;𝐸𝐹
Theorem	decaddc 8165	Add two numerals 𝑀 and 𝑁 (with carry). (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ A ∈ ℕ0    &   ⊢ B ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℕ0    &   ⊢ 𝑀 = ;AB    &   ⊢ 𝑁 = ;𝐶𝐷    &   ⊢ ((A + 𝐶) + 1) = 𝐸    &   ⊢ 𝐹 ∈ ℕ0    &   ⊢ (B + 𝐷) = ;1𝐹    ⇒   ⊢ (𝑀 + 𝑁) = ;𝐸𝐹
Theorem	decaddc2 8166	Add two numerals 𝑀 and 𝑁 (with carry). (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ A ∈ ℕ0    &   ⊢ B ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℕ0    &   ⊢ 𝑀 = ;AB    &   ⊢ 𝑁 = ;𝐶𝐷    &   ⊢ ((A + 𝐶) + 1) = 𝐸    &   ⊢ (B + 𝐷) = 10    ⇒   ⊢ (𝑀 + 𝑁) = ;𝐸0
Theorem	decaddi 8167	Add two numerals 𝑀 and 𝑁 (no carry). (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ A ∈ ℕ0    &   ⊢ B ∈ ℕ0    &   ⊢ 𝑁 ∈ ℕ0    &   ⊢ 𝑀 = ;AB    &   ⊢ (B + 𝑁) = 𝐶    ⇒   ⊢ (𝑀 + 𝑁) = ;A𝐶
Theorem	decaddci 8168	Add two numerals 𝑀 and 𝑁 (no carry). (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ A ∈ ℕ0    &   ⊢ B ∈ ℕ0    &   ⊢ 𝑁 ∈ ℕ0    &   ⊢ 𝑀 = ;AB    &   ⊢ (A + 1) = 𝐷    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ (B + 𝑁) = ;1𝐶    ⇒   ⊢ (𝑀 + 𝑁) = ;𝐷𝐶
Theorem	decaddci2 8169	Add two numerals 𝑀 and 𝑁 (no carry). (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ A ∈ ℕ0    &   ⊢ B ∈ ℕ0    &   ⊢ 𝑁 ∈ ℕ0    &   ⊢ 𝑀 = ;AB    &   ⊢ (A + 1) = 𝐷    &   ⊢ (B + 𝑁) = 10    ⇒   ⊢ (𝑀 + 𝑁) = ;𝐷0
Theorem	decmul1c 8170	The product of a numeral with a number. (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝑃 ∈ ℕ0    &   ⊢ A ∈ ℕ0    &   ⊢ B ∈ ℕ0    &   ⊢ 𝑁 = ;AB    &   ⊢ 𝐷 ∈ ℕ0    &   ⊢ 𝐸 ∈ ℕ0    &   ⊢ ((A · 𝑃) + 𝐸) = 𝐶    &   ⊢ (B · 𝑃) = ;𝐸𝐷    ⇒   ⊢ (𝑁 · 𝑃) = ;𝐶𝐷
Theorem	decmul2c 8171	The product of a numeral with a number (with carry). (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝑃 ∈ ℕ0    &   ⊢ A ∈ ℕ0    &   ⊢ B ∈ ℕ0    &   ⊢ 𝑁 = ;AB    &   ⊢ 𝐷 ∈ ℕ0    &   ⊢ 𝐸 ∈ ℕ0    &   ⊢ ((𝑃 · A) + 𝐸) = 𝐶    &   ⊢ (𝑃 · B) = ;𝐸𝐷    ⇒   ⊢ (𝑃 · 𝑁) = ;𝐶𝐷
Theorem	6p5lem 8172	Lemma for 6p5e11 8173 and related theorems. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ A ∈ ℕ0    &   ⊢ 𝐷 ∈ ℕ0    &   ⊢ 𝐸 ∈ ℕ0    &   ⊢ B = (𝐷 + 1)    &   ⊢ 𝐶 = (𝐸 + 1)    &   ⊢ (A + 𝐷) = ;1𝐸    ⇒   ⊢ (A + B) = ;1𝐶
Theorem	6p5e11 8173	6 + 5 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (6 + 5) = ;11
Theorem	6p6e12 8174	6 + 6 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (6 + 6) = ;12
Theorem	7p4e11 8175	7 + 4 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (7 + 4) = ;11
Theorem	7p5e12 8176	7 + 5 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (7 + 5) = ;12
Theorem	7p6e13 8177	7 + 6 = 13. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (7 + 6) = ;13
Theorem	7p7e14 8178	7 + 7 = 14. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (7 + 7) = ;14
Theorem	8p3e11 8179	8 + 3 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (8 + 3) = ;11
Theorem	8p4e12 8180	8 + 4 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (8 + 4) = ;12
Theorem	8p5e13 8181	8 + 5 = 13. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (8 + 5) = ;13
Theorem	8p6e14 8182	8 + 6 = 14. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (8 + 6) = ;14
Theorem	8p7e15 8183	8 + 7 = 15. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (8 + 7) = ;15
Theorem	8p8e16 8184	8 + 8 = 16. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (8 + 8) = ;16
Theorem	9p2e11 8185	9 + 2 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (9 + 2) = ;11
Theorem	9p3e12 8186	9 + 3 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (9 + 3) = ;12
Theorem	9p4e13 8187	9 + 4 = 13. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (9 + 4) = ;13
Theorem	9p5e14 8188	9 + 5 = 14. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (9 + 5) = ;14
Theorem	9p6e15 8189	9 + 6 = 15. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (9 + 6) = ;15
Theorem	9p7e16 8190	9 + 7 = 16. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (9 + 7) = ;16
Theorem	9p8e17 8191	9 + 8 = 17. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (9 + 8) = ;17
Theorem	9p9e18 8192	9 + 9 = 18. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (9 + 9) = ;18
Theorem	10p10e20 8193	10 + 10 = 20. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (10 + 10) = ;20
Theorem	4t3lem 8194	Lemma for 4t3e12 8195 and related theorems. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ A ∈ ℕ0    &   ⊢ B ∈ ℕ0    &   ⊢ 𝐶 = (B + 1)    &   ⊢ (A · B) = 𝐷    &   ⊢ (𝐷 + A) = 𝐸    ⇒   ⊢ (A · 𝐶) = 𝐸
Theorem	4t3e12 8195	4 times 3 equals 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (4 · 3) = ;12
Theorem	4t4e16 8196	4 times 4 equals 16. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (4 · 4) = ;16
Theorem	5t3e15 8197	5 times 3 equals 15. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (5 · 3) = ;15
Theorem	5t4e20 8198	5 times 4 equals 20. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (5 · 4) = ;20
Theorem	5t5e25 8199	5 times 5 equals 25. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (5 · 5) = ;25
Theorem	6t2e12 8200	6 times 2 equals 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (6 · 2) = ;12