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	nnltlem1 8101	Positive integer ordering relation. (Contributed by NM, 21-Jun-2005.)
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 < 𝑁 ↔ 𝑀 ≤ (𝑁 − 1)))
Theorem	nnm1ge0 8102	A positive integer decreased by 1 is greater than or equal to 0. (Contributed by AV, 30-Oct-2018.)
⊢ (𝑁 ∈ ℕ → 0 ≤ (𝑁 − 1))
Theorem	nn0ge0div 8103	Division of a nonnegative integer by a positive number is not negative. (Contributed by Alexander van der Vekens, 14-Apr-2018.)
⊢ ((𝐾 ∈ ℕ0 ∧ 𝐿 ∈ ℕ) → 0 ≤ (𝐾 / 𝐿))
Theorem	zdiv 8104*	Two ways to express "𝑀 divides 𝑁. (Contributed by NM, 3-Oct-2008.)
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℤ) → (∃𝑘 ∈ ℤ (𝑀 · 𝑘) = 𝑁 ↔ (𝑁 / 𝑀) ∈ ℤ))
Theorem	zdivadd 8105	Property of divisibility: if 𝐷 divides A and B then it divides A + B. (Contributed by NM, 3-Oct-2008.)
⊢ (((𝐷 ∈ ℕ ∧ A ∈ ℤ ∧ B ∈ ℤ) ∧ ((A / 𝐷) ∈ ℤ ∧ (B / 𝐷) ∈ ℤ)) → ((A + B) / 𝐷) ∈ ℤ)
Theorem	zdivmul 8106	Property of divisibility: if 𝐷 divides A then it divides B · A. (Contributed by NM, 3-Oct-2008.)
⊢ (((𝐷 ∈ ℕ ∧ A ∈ ℤ ∧ B ∈ ℤ) ∧ (A / 𝐷) ∈ ℤ) → ((B · A) / 𝐷) ∈ ℤ)
Theorem	zextle 8107*	An extensionality-like property for integer ordering. (Contributed by NM, 29-Oct-2005.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ∀𝑘 ∈ ℤ (𝑘 ≤ 𝑀 ↔ 𝑘 ≤ 𝑁)) → 𝑀 = 𝑁)
Theorem	zextlt 8108*	An extensionality-like property for integer ordering. (Contributed by NM, 29-Oct-2005.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ∀𝑘 ∈ ℤ (𝑘 < 𝑀 ↔ 𝑘 < 𝑁)) → 𝑀 = 𝑁)
Theorem	recnz 8109	The reciprocal of a number greater than 1 is not an integer. (Contributed by NM, 3-May-2005.)
⊢ ((A ∈ ℝ ∧ 1 < A) → ¬ (1 / A) ∈ ℤ)
Theorem	btwnnz 8110	A number between an integer and its successor is not an integer. (Contributed by NM, 3-May-2005.)
⊢ ((A ∈ ℤ ∧ A < B ∧ B < (A + 1)) → ¬ B ∈ ℤ)
Theorem	gtndiv 8111	A larger number does not divide a smaller positive integer. (Contributed by NM, 3-May-2005.)
⊢ ((A ∈ ℝ ∧ B ∈ ℕ ∧ B < A) → ¬ (B / A) ∈ ℤ)
Theorem	halfnz 8112	One-half is not an integer. (Contributed by NM, 31-Jul-2004.)
⊢ ¬ (1 / 2) ∈ ℤ
Theorem	prime 8113*	Two ways to express "A is a prime number (or 1)." (Contributed by NM, 4-May-2005.)
⊢ (A ∈ ℕ → (∀x ∈ ℕ ((A / x) ∈ ℕ → (x = 1 ∨ x = A)) ↔ ∀x ∈ ℕ ((1 < x ∧ x ≤ A ∧ (A / x) ∈ ℕ) → x = A)))
Theorem	msqznn 8114	The square of a nonzero integer is a positive integer. (Contributed by NM, 2-Aug-2004.)
⊢ ((A ∈ ℤ ∧ A ≠ 0) → (A · A) ∈ ℕ)
Theorem	zneo 8115	No even integer equals an odd integer (i.e. no integer can be both even and odd). Exercise 10(a) of [Apostol] p. 28. (Contributed by NM, 31-Jul-2004.) (Proof shortened by Mario Carneiro, 18-May-2014.)
⊢ ((A ∈ ℤ ∧ B ∈ ℤ) → (2 · A) ≠ ((2 · B) + 1))
Theorem	nneoor 8116	A positive integer is even or odd. (Contributed by Jim Kingdon, 15-Mar-2020.)
⊢ (𝑁 ∈ ℕ → ((𝑁 / 2) ∈ ℕ ∨ ((𝑁 + 1) / 2) ∈ ℕ))
Theorem	nneo 8117	A positive integer is even or odd but not both. (Contributed by NM, 1-Jan-2006.) (Proof shortened by Mario Carneiro, 18-May-2014.)
⊢ (𝑁 ∈ ℕ → ((𝑁 / 2) ∈ ℕ ↔ ¬ ((𝑁 + 1) / 2) ∈ ℕ))
Theorem	nneoi 8118	A positive integer is even or odd but not both. (Contributed by NM, 20-Aug-2001.)
⊢ 𝑁 ∈ ℕ    ⇒   ⊢ ((𝑁 / 2) ∈ ℕ ↔ ¬ ((𝑁 + 1) / 2) ∈ ℕ)
Theorem	zeo 8119	An integer is even or odd. (Contributed by NM, 1-Jan-2006.)
⊢ (𝑁 ∈ ℤ → ((𝑁 / 2) ∈ ℤ ∨ ((𝑁 + 1) / 2) ∈ ℤ))
Theorem	zeo2 8120	An integer is even or odd but not both. (Contributed by Mario Carneiro, 12-Sep-2015.)
⊢ (𝑁 ∈ ℤ → ((𝑁 / 2) ∈ ℤ ↔ ¬ ((𝑁 + 1) / 2) ∈ ℤ))
Theorem	peano2uz2 8121*	Second Peano postulate for upper integers. (Contributed by NM, 3-Oct-2004.)
⊢ ((A ∈ ℤ ∧ B ∈ {x ∈ ℤ ∣ A ≤ x}) → (B + 1) ∈ {x ∈ ℤ ∣ A ≤ x})
Theorem	peano5uzti 8122*	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 8123*	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 8124*	An expression for the upper integers that start at 𝑁 that is analogous to dfnn2 7697 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 8125*	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 8126*	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 8127*	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 8128*	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 8129*	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 8130*	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 8131*	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 8132*	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 8133*	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 8134	A positive integer is an integer. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℕ0)    ⇒   ⊢ (φ → A ∈ ℤ)
Theorem	nnzd 8135	A nonnegative integer is an integer. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℕ)    ⇒   ⊢ (φ → A ∈ ℤ)
Theorem	zred 8136	An integer is a real number. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℤ)    ⇒   ⊢ (φ → A ∈ ℝ)
Theorem	zcnd 8137	An integer is a complex number. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℤ)    ⇒   ⊢ (φ → A ∈ ℂ)
Theorem	znegcld 8138	Closure law for negative integers. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℤ)    ⇒   ⊢ (φ → -A ∈ ℤ)
Theorem	peano2zd 8139	Deduction from second Peano postulate generalized to integers. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℤ)    ⇒   ⊢ (φ → (A + 1) ∈ ℤ)
Theorem	zaddcld 8140	Closure of addition of integers. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℤ)    &   ⊢ (φ → B ∈ ℤ)    ⇒   ⊢ (φ → (A + B) ∈ ℤ)
Theorem	zsubcld 8141	Closure of subtraction of integers. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℤ)    &   ⊢ (φ → B ∈ ℤ)    ⇒   ⊢ (φ → (A − B) ∈ ℤ)
Theorem	zmulcld 8142	Closure of multiplication of integers. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℤ)    &   ⊢ (φ → B ∈ ℤ)    ⇒   ⊢ (φ → (A · B) ∈ ℤ)
Theorem	zadd2cl 8143	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 8144	Constant used for decimal constructor.
class ;AB
Definition	df-dec 8145	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 8146	Equality theorem for the decimal constructor. (Contributed by Mario Carneiro, 17-Apr-2015.)
⊢ (A = B → ;A𝐶 = ;B𝐶)
Theorem	deceq2 8147	Equality theorem for the decimal constructor. (Contributed by Mario Carneiro, 17-Apr-2015.)
⊢ (A = B → ;𝐶A = ;𝐶B)
Theorem	deceq1i 8148	Equality theorem for the decimal constructor. (Contributed by Mario Carneiro, 17-Apr-2015.)
⊢ A = B    ⇒   ⊢ ;A𝐶 = ;B𝐶
Theorem	deceq2i 8149	Equality theorem for the decimal constructor. (Contributed by Mario Carneiro, 17-Apr-2015.)
⊢ A = B    ⇒   ⊢ ;𝐶A = ;𝐶B
Theorem	deceq12i 8150	Equality theorem for the decimal constructor. (Contributed by Mario Carneiro, 17-Apr-2015.)
⊢ A = B    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ ;A𝐶 = ;B𝐷
Theorem	numnncl 8151	Closure for a numeral (with units place). (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝑇 ∈ ℕ0    &   ⊢ A ∈ ℕ0    &   ⊢ B ∈ ℕ    ⇒   ⊢ ((𝑇 · A) + B) ∈ ℕ
Theorem	num0u 8152	Add a zero in the units place. (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝑇 ∈ ℕ0    &   ⊢ A ∈ ℕ0    ⇒   ⊢ (𝑇 · A) = ((𝑇 · A) + 0)
Theorem	num0h 8153	Add a zero in the higher places. (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝑇 ∈ ℕ0    &   ⊢ A ∈ ℕ0    ⇒   ⊢ A = ((𝑇 · 0) + A)
Theorem	numcl 8154	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 8155	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 8156	Closure for a numeral. (Contributed by Mario Carneiro, 17-Apr-2015.)
⊢ A ∈ ℕ0    &   ⊢ B ∈ ℕ    ⇒   ⊢ ;AB ∈ ℕ
Theorem	deccl 8157	Closure for a numeral. (Contributed by Mario Carneiro, 17-Apr-2015.)
⊢ A ∈ ℕ0    &   ⊢ B ∈ ℕ0    ⇒   ⊢ ;AB ∈ ℕ0
Theorem	dec0u 8158	Add a zero in the units place. (Contributed by Mario Carneiro, 17-Apr-2015.)
⊢ A ∈ ℕ0    ⇒   ⊢ (10 · A) = ;A0
Theorem	dec0h 8159	Add a zero in the higher places. (Contributed by Mario Carneiro, 17-Apr-2015.)
⊢ A ∈ ℕ0    ⇒   ⊢ A = ;0A
Theorem	numnncl2 8160	Closure for a decimal integer (zero units place). (Contributed by Mario Carneiro, 9-Mar-2015.)
⊢ 𝑇 ∈ ℕ    &   ⊢ A ∈ ℕ    ⇒   ⊢ ((𝑇 · A) + 0) ∈ ℕ
Theorem	decnncl2 8161	Closure for a decimal integer (zero units place). (Contributed by Mario Carneiro, 17-Apr-2015.)
⊢ A ∈ ℕ    ⇒   ⊢ ;A0 ∈ ℕ
Theorem	numlt 8162	Comparing two decimal integers (equal higher places). (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝑇 ∈ ℕ    &   ⊢ A ∈ ℕ0    &   ⊢ B ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ    &   ⊢ B < 𝐶    ⇒   ⊢ ((𝑇 · A) + B) < ((𝑇 · A) + 𝐶)
Theorem	numltc 8163	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 8164	Comparing two decimal integers (equal higher places). (Contributed by Mario Carneiro, 17-Apr-2015.)
⊢ A ∈ ℕ0    &   ⊢ B ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ    &   ⊢ B < 𝐶    ⇒   ⊢ ;AB < ;A𝐶
Theorem	decltc 8165	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 8166	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 8167	Comparing a digit to a decimal integer. (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝑇 ∈ ℕ    &   ⊢ A ∈ ℕ    &   ⊢ B ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐶 < 𝑇    ⇒   ⊢ 𝐶 < ((𝑇 · A) + B)
Theorem	declti 8168	Comparing a digit to a decimal integer. (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ A ∈ ℕ    &   ⊢ B ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐶 < 10    ⇒   ⊢ 𝐶 < ;AB
Theorem	numsucc 8169	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 8170	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 8171	The successor of zero. (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 1 = (0 + 1)
Theorem	dec10p 8172	Ten plus an integer. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (10 + A) = ;1A
Theorem	dec10 8173	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 8174	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 8175	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 8176	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 8177	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 8178	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 8179	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 8180	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 8181	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 8182	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 8183	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 8184	Add two numerals 𝑀 and 𝑁 (no carry). (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ A ∈ ℕ0    &   ⊢ B ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℕ0    &   ⊢ 𝑀 = ;AB    &   ⊢ 𝑁 = ;𝐶𝐷    &   ⊢ (A + 𝐶) = 𝐸    &   ⊢ (B + 𝐷) = 𝐹    ⇒   ⊢ (𝑀 + 𝑁) = ;𝐸𝐹
Theorem	decaddc 8185	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 8186	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 8187	Add two numerals 𝑀 and 𝑁 (no carry). (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ A ∈ ℕ0    &   ⊢ B ∈ ℕ0    &   ⊢ 𝑁 ∈ ℕ0    &   ⊢ 𝑀 = ;AB    &   ⊢ (B + 𝑁) = 𝐶    ⇒   ⊢ (𝑀 + 𝑁) = ;A𝐶
Theorem	decaddci 8188	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 8189	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 8190	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 8191	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 8192	Lemma for 6p5e11 8193 and related theorems. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ A ∈ ℕ0    &   ⊢ 𝐷 ∈ ℕ0    &   ⊢ 𝐸 ∈ ℕ0    &   ⊢ B = (𝐷 + 1)    &   ⊢ 𝐶 = (𝐸 + 1)    &   ⊢ (A + 𝐷) = ;1𝐸    ⇒   ⊢ (A + B) = ;1𝐶
Theorem	6p5e11 8193	6 + 5 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (6 + 5) = ;11
Theorem	6p6e12 8194	6 + 6 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (6 + 6) = ;12
Theorem	7p4e11 8195	7 + 4 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (7 + 4) = ;11
Theorem	7p5e12 8196	7 + 5 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (7 + 5) = ;12
Theorem	7p6e13 8197	7 + 6 = 13. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (7 + 6) = ;13
Theorem	7p7e14 8198	7 + 7 = 14. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (7 + 7) = ;14
Theorem	8p3e11 8199	8 + 3 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (8 + 3) = ;11
Theorem	8p4e12 8200	8 + 4 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (8 + 4) = ;12