P. 128 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 12701-12800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	btwnnz 12701	A number between an integer and its successor is not an integer. (Contributed by NM, 3-May-2005.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐴 < 𝐵 ∧ 𝐵 < (𝐴 + 1)) → ¬ 𝐵 ∈ ℤ)
Theorem	gtndiv 12702	A larger number does not divide a smaller positive integer. (Contributed by NM, 3-May-2005.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℕ ∧ 𝐵 < 𝐴) → ¬ (𝐵 / 𝐴) ∈ ℤ)
Theorem	halfnz 12703	One-half is not an integer. (Contributed by NM, 31-Jul-2004.)
⊢ ¬ (1 / 2) ∈ ℤ
Theorem	3halfnz 12704	Three halves is not an integer. (Contributed by AV, 2-Jun-2020.)
⊢ ¬ (3 / 2) ∈ ℤ
Theorem	suprzcl 12705*	The supremum of a bounded-above set of integers is a member of the set. (Contributed by Paul Chapman, 21-Mar-2011.) (Revised by Mario Carneiro, 26-Jun-2015.)
⊢ ((𝐴 ⊆ ℤ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) → sup(𝐴, ℝ, < ) ∈ 𝐴)
Theorem	prime 12706*	Two ways to express "𝐴 is a prime number (or 1)". See also isprm 16769. (Contributed by NM, 4-May-2005.)
⊢ (𝐴 ∈ ℕ → (∀𝑥 ∈ ℕ ((𝐴 / 𝑥) ∈ ℕ → (𝑥 = 1 ∨ 𝑥 = 𝐴)) ↔ ∀𝑥 ∈ ℕ ((1 < 𝑥 ∧ 𝑥 ≤ 𝐴 ∧ (𝐴 / 𝑥) ∈ ℕ) → 𝑥 = 𝐴)))
Theorem	msqznn 12707	The square of a nonzero integer is a positive integer. (Contributed by NM, 2-Aug-2004.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐴 ≠ 0) → (𝐴 · 𝐴) ∈ ℕ)
Theorem	zneo 12708	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.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (2 · 𝐴) ≠ ((2 · 𝐵) + 1))
Theorem	nneo 12709	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 12710	A positive integer is even or odd but not both. (Contributed by NM, 20-Aug-2001.)
⊢ 𝑁 ∈ ℕ    ⇒   ⊢ ((𝑁 / 2) ∈ ℕ ↔ ¬ ((𝑁 + 1) / 2) ∈ ℕ)
Theorem	zeo 12711	An integer is even or odd. (Contributed by NM, 1-Jan-2006.)
⊢ (𝑁 ∈ ℤ → ((𝑁 / 2) ∈ ℤ ∨ ((𝑁 + 1) / 2) ∈ ℤ))
Theorem	zeo2 12712	An integer is even or odd but not both. (Contributed by Mario Carneiro, 12-Sep-2015.)
⊢ (𝑁 ∈ ℤ → ((𝑁 / 2) ∈ ℤ ↔ ¬ ((𝑁 + 1) / 2) ∈ ℤ))
Theorem	peano2uz2 12713*	Second Peano postulate for upper integers. (Contributed by NM, 3-Oct-2004.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ {𝑥 ∈ ℤ ∣ 𝐴 ≤ 𝑥}) → (𝐵 + 1) ∈ {𝑥 ∈ ℤ ∣ 𝐴 ≤ 𝑥})
Theorem	peano5uzi 12714*	Peano's inductive postulate for upper integers. (Contributed by NM, 6-Jul-2005.) (Revised by Mario Carneiro, 3-May-2014.)
⊢ 𝑁 ∈ ℤ    ⇒   ⊢ ((𝑁 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 + 1) ∈ 𝐴) → {𝑘 ∈ ℤ ∣ 𝑁 ≤ 𝑘} ⊆ 𝐴)
Theorem	peano5uzti 12715*	Peano's inductive postulate for upper integers. (Contributed by NM, 6-Jul-2005.) (Revised by Mario Carneiro, 25-Jul-2013.)
⊢ (𝑁 ∈ ℤ → ((𝑁 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 + 1) ∈ 𝐴) → {𝑘 ∈ ℤ ∣ 𝑁 ≤ 𝑘} ⊆ 𝐴))
Theorem	dfuzi 12716*	An expression for the upper integers that start at 𝑁 that is analogous to dfnn2 12274 for positive integers. (Contributed by NM, 6-Jul-2005.) (Proof shortened by Mario Carneiro, 3-May-2014.)
⊢ 𝑁 ∈ ℤ    ⇒   ⊢ {𝑧 ∈ ℤ ∣ 𝑁 ≤ 𝑧} = ∩ {𝑥 ∣ (𝑁 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}
Theorem	uzind 12717*	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 12718*	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 12719*	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 12720*	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.)
⊢ (𝑥 = 0 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑥 = (𝑦 + 1) → (𝜑 ↔ 𝜃))    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏))    &   ⊢ 𝜓    &   ⊢ (𝑦 ∈ ℕ0 → (𝜒 → 𝜃))    ⇒   ⊢ (𝐴 ∈ ℕ0 → 𝜏)
Theorem	nn0indALT 12721*	Principle of Mathematical Induction (inference schema) on nonnegative integers. The last four hypotheses give us the substitution instances we need; the first two are the basis and the induction step. Either nn0ind 12720 or nn0indALT 12721 may be used; see comment for nnind 12279. (Contributed by NM, 28-Nov-2005.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (𝑦 ∈ ℕ0 → (𝜒 → 𝜃))    &   ⊢ 𝜓    &   ⊢ (𝑥 = 0 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑥 = (𝑦 + 1) → (𝜑 ↔ 𝜃))    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏))    ⇒   ⊢ (𝐴 ∈ ℕ0 → 𝜏)
Theorem	nn0indd 12722*	Principle of Mathematical Induction (inference schema) on nonnegative integers, a deduction version. (Contributed by Thierry Arnoux, 23-Mar-2018.)
⊢ (𝑥 = 0 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑥 = 𝑦 → (𝜓 ↔ 𝜃))    &   ⊢ (𝑥 = (𝑦 + 1) → (𝜓 ↔ 𝜏))    &   ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜂))    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ 𝜃) → 𝜏)    ⇒   ⊢ ((𝜑 ∧ 𝐴 ∈ ℕ0) → 𝜂)
Theorem	fzind 12723*	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.)
⊢ (𝑥 = 𝑀 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑥 = (𝑦 + 1) → (𝜑 ↔ 𝜃))    &   ⊢ (𝑥 = 𝐾 → (𝜑 ↔ 𝜏))    &   ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) → 𝜓)    &   ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑦 ∈ ℤ ∧ 𝑀 ≤ 𝑦 ∧ 𝑦 < 𝑁)) → (𝜒 → 𝜃))    ⇒   ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ 𝑀 ≤ 𝐾 ∧ 𝐾 ≤ 𝑁)) → 𝜏)
Theorem	fnn0ind 12724*	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.)
⊢ (𝑥 = 0 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑥 = (𝑦 + 1) → (𝜑 ↔ 𝜃))    &   ⊢ (𝑥 = 𝐾 → (𝜑 ↔ 𝜏))    &   ⊢ (𝑁 ∈ ℕ0 → 𝜓)    &   ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑦 ∈ ℕ0 ∧ 𝑦 < 𝑁) → (𝜒 → 𝜃))    ⇒   ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℕ0 ∧ 𝐾 ≤ 𝑁) → 𝜏)
Theorem	nn0ind-raph 12725*	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 12726*	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	fzindd 12727*	Induction on the integers from M to N inclusive, a deduction version. (Contributed by metakunt, 12-May-2024.)
⊢ (𝑥 = 𝑀 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑥 = 𝑦 → (𝜓 ↔ 𝜃))    &   ⊢ (𝑥 = (𝑦 + 1) → (𝜓 ↔ 𝜏))    &   ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜂))    &   ⊢ (𝜑 → 𝜒)    &   ⊢ ((𝜑 ∧ (𝑦 ∈ ℤ ∧ 𝑀 ≤ 𝑦 ∧ 𝑦 < 𝑁) ∧ 𝜃) → 𝜏)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ (𝜑 → 𝑀 ≤ 𝑁)    ⇒   ⊢ ((𝜑 ∧ (𝐴 ∈ ℤ ∧ 𝑀 ≤ 𝐴 ∧ 𝐴 ≤ 𝑁)) → 𝜂)
Theorem	btwnz 12728*	Any real number can be sandwiched between two integers. Exercise 2 of [Apostol] p. 28. (Contributed by NM, 10-Nov-2004.)
⊢ (𝐴 ∈ ℝ → (∃𝑥 ∈ ℤ 𝑥 < 𝐴 ∧ ∃𝑦 ∈ ℤ 𝐴 < 𝑦))
Theorem	zred 12729	An integer is a real number. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℤ)    ⇒   ⊢ (𝜑 → 𝐴 ∈ ℝ)
Theorem	zcnd 12730	An integer is a complex number. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℤ)    ⇒   ⊢ (𝜑 → 𝐴 ∈ ℂ)
Theorem	znegcld 12731	Closure law for negative integers. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℤ)    ⇒   ⊢ (𝜑 → -𝐴 ∈ ℤ)
Theorem	peano2zd 12732	Deduction from second Peano postulate generalized to integers. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℤ)    ⇒   ⊢ (𝜑 → (𝐴 + 1) ∈ ℤ)
Theorem	zaddcld 12733	Closure of addition of integers. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℤ)    &   ⊢ (𝜑 → 𝐵 ∈ ℤ)    ⇒   ⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℤ)
Theorem	zsubcld 12734	Closure of subtraction of integers. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℤ)    &   ⊢ (𝜑 → 𝐵 ∈ ℤ)    ⇒   ⊢ (𝜑 → (𝐴 − 𝐵) ∈ ℤ)
Theorem	zmulcld 12735	Closure of multiplication of integers. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℤ)    &   ⊢ (𝜑 → 𝐵 ∈ ℤ)    ⇒   ⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℤ)
Theorem	znnn0nn 12736	The negative of a negative integer, is a natural number. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ ((𝑁 ∈ ℤ ∧ ¬ 𝑁 ∈ ℕ0) → -𝑁 ∈ ℕ)
Theorem	zadd2cl 12737	Increasing an integer by 2 results in an integer. (Contributed by Alexander van der Vekens, 16-Sep-2018.)
⊢ (𝑁 ∈ ℤ → (𝑁 + 2) ∈ ℤ)
Theorem	zriotaneg 12738*	The negative of the unique integer such that 𝜑. (Contributed by AV, 1-Dec-2018.)
⊢ (𝑥 = -𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃!𝑥 ∈ ℤ 𝜑 → (℩𝑥 ∈ ℤ 𝜑) = -(℩𝑦 ∈ ℤ 𝜓))
Theorem	suprfinzcl 12739	The supremum of a nonempty finite set of integers is a member of the set. (Contributed by AV, 1-Oct-2019.)
⊢ ((𝐴 ⊆ ℤ ∧ 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin) → sup(𝐴, ℝ, < ) ∈ 𝐴)
5.4.10  Decimal arithmetic
Syntax	cdc 12740	Constant used for decimal constructor.
class ;𝐴𝐵
Definition	df-dec 12741	Define the "decimal constructor", which is used to build up "decimal integers" or "numeric terms" in base 10. For example, (;;;1000 + ;;;2000) = ;;;3000 1kp2ke3k 30934. (Contributed by Mario Carneiro, 17-Apr-2015.) (Revised by AV, 1-Aug-2021.)
⊢ ;𝐴𝐵 = (((9 + 1) · 𝐴) + 𝐵)
Theorem	9p1e10 12742	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 12743	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	decex 12744	A decimal number is a set. (Contributed by Mario Carneiro, 17-Apr-2015.) (Revised by AV, 6-Sep-2021.)
⊢ ;𝐴𝐵 ∈ V
Theorem	deceq1 12745	Equality theorem for the decimal constructor. (Contributed by Mario Carneiro, 17-Apr-2015.) (Revised by AV, 6-Sep-2021.)
⊢ (𝐴 = 𝐵 → ;𝐴𝐶 = ;𝐵𝐶)
Theorem	deceq2 12746	Equality theorem for the decimal constructor. (Contributed by Mario Carneiro, 17-Apr-2015.) (Revised by AV, 6-Sep-2021.)
⊢ (𝐴 = 𝐵 → ;𝐶𝐴 = ;𝐶𝐵)
Theorem	deceq1i 12747	Equality theorem for the decimal constructor. (Contributed by Mario Carneiro, 17-Apr-2015.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ ;𝐴𝐶 = ;𝐵𝐶
Theorem	deceq2i 12748	Equality theorem for the decimal constructor. (Contributed by Mario Carneiro, 17-Apr-2015.)
⊢ 𝐴 = 𝐵    ⇒   ⊢ ;𝐶𝐴 = ;𝐶𝐵
Theorem	deceq12i 12749	Equality theorem for the decimal constructor. (Contributed by Mario Carneiro, 17-Apr-2015.)
⊢ 𝐴 = 𝐵    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ ;𝐴𝐶 = ;𝐵𝐷
Theorem	numnncl 12750	Closure for a numeral (with units place). (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝑇 ∈ ℕ0    &   ⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ    ⇒   ⊢ ((𝑇 · 𝐴) + 𝐵) ∈ ℕ
Theorem	num0u 12751	Add a zero in the units place. (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝑇 ∈ ℕ0    &   ⊢ 𝐴 ∈ ℕ0    ⇒   ⊢ (𝑇 · 𝐴) = ((𝑇 · 𝐴) + 0)
Theorem	num0h 12752	Add a zero in the higher places. (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝑇 ∈ ℕ0    &   ⊢ 𝐴 ∈ ℕ0    ⇒   ⊢ 𝐴 = ((𝑇 · 0) + 𝐴)
Theorem	numcl 12753	Closure for a decimal integer (with units place). (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝑇 ∈ ℕ0    &   ⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    ⇒   ⊢ ((𝑇 · 𝐴) + 𝐵) ∈ ℕ0
Theorem	numsuc 12754	The successor of a decimal integer (no carry). (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝑇 ∈ ℕ0    &   ⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ (𝐵 + 1) = 𝐶    &   ⊢ 𝑁 = ((𝑇 · 𝐴) + 𝐵)    ⇒   ⊢ (𝑁 + 1) = ((𝑇 · 𝐴) + 𝐶)
Theorem	deccl 12755	Closure for a numeral. (Contributed by Mario Carneiro, 17-Apr-2015.) (Revised by AV, 6-Sep-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    ⇒   ⊢ ;𝐴𝐵 ∈ ℕ0
Theorem	11nn0 12756	11 is a nonnegative integer. (Contributed by Umit Teoman Dogan, 10-Jun-2026.)
⊢ ;11 ∈ ℕ0
Theorem	12nn0 12757	12 is a nonnegative integer. (Contributed by Umit Teoman Dogan, 10-Jun-2026.)
⊢ ;12 ∈ ℕ0
Theorem	16nn0 12758	16 is a nonnegative integer. (Contributed by Umit Teoman Dogan, 10-Jun-2026.)
⊢ ;16 ∈ ℕ0
Theorem	25nn0 12759	25 is a nonnegative integer. (Contributed by Umit Teoman Dogan, 10-Jun-2026.)
⊢ ;25 ∈ ℕ0
Theorem	10nn 12760	10 is a positive integer. (Contributed by NM, 8-Nov-2012.) (Revised by AV, 6-Sep-2021.)
⊢ ;10 ∈ ℕ
Theorem	10pos 12761	The number 10 is positive. (Contributed by NM, 5-Feb-2007.) (Revised by AV, 8-Sep-2021.)
⊢ 0 < ;10
Theorem	10nn0 12762	10 is a nonnegative integer. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.)
⊢ ;10 ∈ ℕ0
Theorem	10re 12763	The number 10 is real. (Contributed by NM, 5-Feb-2007.) (Revised by AV, 8-Sep-2021.) Reduce dependencies on axioms. (Revised by Steven Nguyen, 8-Oct-2022.)
⊢ ;10 ∈ ℝ
Theorem	decnncl 12764	Closure for a numeral. (Contributed by Mario Carneiro, 17-Apr-2015.) (Revised by AV, 6-Sep-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ    ⇒   ⊢ ;𝐴𝐵 ∈ ℕ
Theorem	11nn 12765	11 is a positive integer. (Contributed by Umit Teoman Dogan, 10-Jun-2026.)
⊢ ;11 ∈ ℕ
Theorem	dec0u 12766	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 12767	Add a zero in the higher places. (Contributed by Mario Carneiro, 17-Apr-2015.) (Revised by AV, 6-Sep-2021.)
⊢ 𝐴 ∈ ℕ0    ⇒   ⊢ 𝐴 = ;0𝐴
Theorem	numnncl2 12768	Closure for a decimal integer (zero units place). (Contributed by Mario Carneiro, 9-Mar-2015.)
⊢ 𝑇 ∈ ℕ    &   ⊢ 𝐴 ∈ ℕ    ⇒   ⊢ ((𝑇 · 𝐴) + 0) ∈ ℕ
Theorem	decnncl2 12769	Closure for a decimal integer (zero units place). (Contributed by Mario Carneiro, 17-Apr-2015.) (Revised by AV, 6-Sep-2021.)
⊢ 𝐴 ∈ ℕ    ⇒   ⊢ ;𝐴0 ∈ ℕ
Theorem	numlt 12770	Comparing two decimal integers (equal higher places). (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝑇 ∈ ℕ    &   ⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ    &   ⊢ 𝐵 < 𝐶    ⇒   ⊢ ((𝑇 · 𝐴) + 𝐵) < ((𝑇 · 𝐴) + 𝐶)
Theorem	numltc 12771	Comparing two decimal integers (unequal higher places). (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝑇 ∈ ℕ    &   ⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℕ0    &   ⊢ 𝐶 < 𝑇    &   ⊢ 𝐴 < 𝐵    ⇒   ⊢ ((𝑇 · 𝐴) + 𝐶) < ((𝑇 · 𝐵) + 𝐷)
Theorem	le9lt10 12772	A "decimal digit" (i.e. a nonnegative integer less than or equal to 9) is less than 10. (Contributed by AV, 8-Sep-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐴 ≤ 9    ⇒   ⊢ 𝐴 < ;10
Theorem	declt 12773	Comparing two decimal integers (equal higher places). (Contributed by Mario Carneiro, 17-Apr-2015.) (Revised by AV, 6-Sep-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ    &   ⊢ 𝐵 < 𝐶    ⇒   ⊢ ;𝐴𝐵 < ;𝐴𝐶
Theorem	decltc 12774	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 12775	Comparing two decimal integers (unequal higher places). (Contributed by AV, 8-Sep-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℕ0    &   ⊢ 𝐶 ≤ 9    &   ⊢ 𝐴 < 𝐵    ⇒   ⊢ ;𝐴𝐶 < ;𝐵𝐷
Theorem	decsuc 12776	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 12777	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 12778	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 12779	Comparing two decimal integers (equal higher places). (Contributed by AV, 17-Aug-2021.) (Revised by AV, 8-Sep-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐵 ≤ 𝐶    ⇒   ⊢ ;𝐴𝐵 ≤ ;𝐴𝐶
Theorem	decleh 12780	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 12781	Comparing a digit to a decimal integer. (Contributed by AV, 17-Aug-2021.)
⊢ 𝐴 ∈ ℕ    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐶 ≤ 9    ⇒   ⊢ 𝐶 ≤ ;𝐴𝐵
Theorem	numlti 12782	Comparing a digit to a decimal integer. (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝑇 ∈ ℕ    &   ⊢ 𝐴 ∈ ℕ    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐶 < 𝑇    ⇒   ⊢ 𝐶 < ((𝑇 · 𝐴) + 𝐵)
Theorem	declti 12783	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 12784	Comparing a digit to a decimal integer. (Contributed by AV, 8-Sep-2021.)
⊢ 𝐴 ∈ ℕ    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐶 ≤ 9    ⇒   ⊢ 𝐶 < ;𝐴𝐵
Theorem	numsucc 12785	The successor of a decimal integer (with carry). (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝑌 ∈ ℕ0    &   ⊢ 𝑇 = (𝑌 + 1)    &   ⊢ 𝐴 ∈ ℕ0    &   ⊢ (𝐴 + 1) = 𝐵    &   ⊢ 𝑁 = ((𝑇 · 𝐴) + 𝑌)    ⇒   ⊢ (𝑁 + 1) = ((𝑇 · 𝐵) + 0)
Theorem	decsucc 12786	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 12787	The successor of zero. (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 1 = (0 + 1)
Theorem	dec10p 12788	Ten plus an integer. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.)
⊢ (;10 + 𝐴) = ;1𝐴
Theorem	numma 12789	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 12790	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 12791	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 12792	Add two decimal integers 𝑀 and 𝑁 (no carry). (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝑇 ∈ ℕ0    &   ⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℕ0    &   ⊢ 𝑀 = ((𝑇 · 𝐴) + 𝐵)    &   ⊢ 𝑁 = ((𝑇 · 𝐶) + 𝐷)    &   ⊢ (𝐴 + 𝐶) = 𝐸    &   ⊢ (𝐵 + 𝐷) = 𝐹    ⇒   ⊢ (𝑀 + 𝑁) = ((𝑇 · 𝐸) + 𝐹)
Theorem	numaddc 12793	Add two decimal integers 𝑀 and 𝑁 (with carry). (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝑇 ∈ ℕ0    &   ⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℕ0    &   ⊢ 𝑀 = ((𝑇 · 𝐴) + 𝐵)    &   ⊢ 𝑁 = ((𝑇 · 𝐶) + 𝐷)    &   ⊢ 𝐹 ∈ ℕ0    &   ⊢ ((𝐴 + 𝐶) + 1) = 𝐸    &   ⊢ (𝐵 + 𝐷) = ((𝑇 · 1) + 𝐹)    ⇒   ⊢ (𝑀 + 𝑁) = ((𝑇 · 𝐸) + 𝐹)
Theorem	nummul1c 12794	The product of a decimal integer with a number. (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝑇 ∈ ℕ0    &   ⊢ 𝑃 ∈ ℕ0    &   ⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝑁 = ((𝑇 · 𝐴) + 𝐵)    &   ⊢ 𝐷 ∈ ℕ0    &   ⊢ 𝐸 ∈ ℕ0    &   ⊢ ((𝐴 · 𝑃) + 𝐸) = 𝐶    &   ⊢ (𝐵 · 𝑃) = ((𝑇 · 𝐸) + 𝐷)    ⇒   ⊢ (𝑁 · 𝑃) = ((𝑇 · 𝐶) + 𝐷)
Theorem	nummul2c 12795	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 12796	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 12797	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 12798	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 12799	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 12800	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𝐹    ⇒   ⊢ (𝑀 + 𝑁) = ;𝐸𝐹