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	zsubcld 8101	Closure of subtraction of integers. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℤ)    &   ⊢ (φ → B ∈ ℤ)    ⇒   ⊢ (φ → (A − B) ∈ ℤ)
Theorem	zmulcld 8102	Closure of multiplication of integers. (Contributed by Mario Carneiro, 28-May-2016.)
⊢ (φ → A ∈ ℤ)    &   ⊢ (φ → B ∈ ℤ)    ⇒   ⊢ (φ → (A · B) ∈ ℤ)
Theorem	zadd2cl 8103	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 8104	Constant used for decimal constructor.
class ;AB
Definition	df-dec 8105	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 8106	Equality theorem for the decimal constructor. (Contributed by Mario Carneiro, 17-Apr-2015.)
⊢ (A = B → ;A𝐶 = ;B𝐶)
Theorem	deceq2 8107	Equality theorem for the decimal constructor. (Contributed by Mario Carneiro, 17-Apr-2015.)
⊢ (A = B → ;𝐶A = ;𝐶B)
Theorem	deceq1i 8108	Equality theorem for the decimal constructor. (Contributed by Mario Carneiro, 17-Apr-2015.)
⊢ A = B    ⇒   ⊢ ;A𝐶 = ;B𝐶
Theorem	deceq2i 8109	Equality theorem for the decimal constructor. (Contributed by Mario Carneiro, 17-Apr-2015.)
⊢ A = B    ⇒   ⊢ ;𝐶A = ;𝐶B
Theorem	deceq12i 8110	Equality theorem for the decimal constructor. (Contributed by Mario Carneiro, 17-Apr-2015.)
⊢ A = B    &   ⊢ 𝐶 = 𝐷    ⇒   ⊢ ;A𝐶 = ;B𝐷
Theorem	numnncl 8111	Closure for a numeral (with units place). (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝑇 ∈ ℕ0    &   ⊢ A ∈ ℕ0    &   ⊢ B ∈ ℕ    ⇒   ⊢ ((𝑇 · A) + B) ∈ ℕ
Theorem	num0u 8112	Add a zero in the units place. (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝑇 ∈ ℕ0    &   ⊢ A ∈ ℕ0    ⇒   ⊢ (𝑇 · A) = ((𝑇 · A) + 0)
Theorem	num0h 8113	Add a zero in the higher places. (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝑇 ∈ ℕ0    &   ⊢ A ∈ ℕ0    ⇒   ⊢ A = ((𝑇 · 0) + A)
Theorem	numcl 8114	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 8115	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 8116	Closure for a numeral. (Contributed by Mario Carneiro, 17-Apr-2015.)
⊢ A ∈ ℕ0    &   ⊢ B ∈ ℕ    ⇒   ⊢ ;AB ∈ ℕ
Theorem	deccl 8117	Closure for a numeral. (Contributed by Mario Carneiro, 17-Apr-2015.)
⊢ A ∈ ℕ0    &   ⊢ B ∈ ℕ0    ⇒   ⊢ ;AB ∈ ℕ0
Theorem	dec0u 8118	Add a zero in the units place. (Contributed by Mario Carneiro, 17-Apr-2015.)
⊢ A ∈ ℕ0    ⇒   ⊢ (10 · A) = ;A0
Theorem	dec0h 8119	Add a zero in the higher places. (Contributed by Mario Carneiro, 17-Apr-2015.)
⊢ A ∈ ℕ0    ⇒   ⊢ A = ;0A
Theorem	numnncl2 8120	Closure for a decimal integer (zero units place). (Contributed by Mario Carneiro, 9-Mar-2015.)
⊢ 𝑇 ∈ ℕ    &   ⊢ A ∈ ℕ    ⇒   ⊢ ((𝑇 · A) + 0) ∈ ℕ
Theorem	decnncl2 8121	Closure for a decimal integer (zero units place). (Contributed by Mario Carneiro, 17-Apr-2015.)
⊢ A ∈ ℕ    ⇒   ⊢ ;A0 ∈ ℕ
Theorem	numlt 8122	Comparing two decimal integers (equal higher places). (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝑇 ∈ ℕ    &   ⊢ A ∈ ℕ0    &   ⊢ B ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ    &   ⊢ B < 𝐶    ⇒   ⊢ ((𝑇 · A) + B) < ((𝑇 · A) + 𝐶)
Theorem	numltc 8123	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 8124	Comparing two decimal integers (equal higher places). (Contributed by Mario Carneiro, 17-Apr-2015.)
⊢ A ∈ ℕ0    &   ⊢ B ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ    &   ⊢ B < 𝐶    ⇒   ⊢ ;AB < ;A𝐶
Theorem	decltc 8125	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 8126	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 8127	Comparing a digit to a decimal integer. (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝑇 ∈ ℕ    &   ⊢ A ∈ ℕ    &   ⊢ B ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐶 < 𝑇    ⇒   ⊢ 𝐶 < ((𝑇 · A) + B)
Theorem	declti 8128	Comparing a digit to a decimal integer. (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ A ∈ ℕ    &   ⊢ B ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐶 < 10    ⇒   ⊢ 𝐶 < ;AB
Theorem	numsucc 8129	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 8130	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 8131	The successor of zero. (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 1 = (0 + 1)
Theorem	dec10p 8132	Ten plus an integer. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (10 + A) = ;1A
Theorem	dec10 8133	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 8134	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 8135	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 8136	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 8137	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 8138	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 8139	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 8140	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 8141	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 8142	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 8143	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 8144	Add two numerals 𝑀 and 𝑁 (no carry). (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ A ∈ ℕ0    &   ⊢ B ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℕ0    &   ⊢ 𝑀 = ;AB    &   ⊢ 𝑁 = ;𝐶𝐷    &   ⊢ (A + 𝐶) = 𝐸    &   ⊢ (B + 𝐷) = 𝐹    ⇒   ⊢ (𝑀 + 𝑁) = ;𝐸𝐹
Theorem	decaddc 8145	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 8146	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 8147	Add two numerals 𝑀 and 𝑁 (no carry). (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ A ∈ ℕ0    &   ⊢ B ∈ ℕ0    &   ⊢ 𝑁 ∈ ℕ0    &   ⊢ 𝑀 = ;AB    &   ⊢ (B + 𝑁) = 𝐶    ⇒   ⊢ (𝑀 + 𝑁) = ;A𝐶
Theorem	decaddci 8148	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 8149	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 8150	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 8151	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 8152	Lemma for 6p5e11 8153 and related theorems. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ A ∈ ℕ0    &   ⊢ 𝐷 ∈ ℕ0    &   ⊢ 𝐸 ∈ ℕ0    &   ⊢ B = (𝐷 + 1)    &   ⊢ 𝐶 = (𝐸 + 1)    &   ⊢ (A + 𝐷) = ;1𝐸    ⇒   ⊢ (A + B) = ;1𝐶
Theorem	6p5e11 8153	6 + 5 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (6 + 5) = ;11
Theorem	6p6e12 8154	6 + 6 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (6 + 6) = ;12
Theorem	7p4e11 8155	7 + 4 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (7 + 4) = ;11
Theorem	7p5e12 8156	7 + 5 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (7 + 5) = ;12
Theorem	7p6e13 8157	7 + 6 = 13. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (7 + 6) = ;13
Theorem	7p7e14 8158	7 + 7 = 14. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (7 + 7) = ;14
Theorem	8p3e11 8159	8 + 3 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (8 + 3) = ;11
Theorem	8p4e12 8160	8 + 4 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (8 + 4) = ;12
Theorem	8p5e13 8161	8 + 5 = 13. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (8 + 5) = ;13
Theorem	8p6e14 8162	8 + 6 = 14. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (8 + 6) = ;14
Theorem	8p7e15 8163	8 + 7 = 15. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (8 + 7) = ;15
Theorem	8p8e16 8164	8 + 8 = 16. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (8 + 8) = ;16
Theorem	9p2e11 8165	9 + 2 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (9 + 2) = ;11
Theorem	9p3e12 8166	9 + 3 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (9 + 3) = ;12
Theorem	9p4e13 8167	9 + 4 = 13. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (9 + 4) = ;13
Theorem	9p5e14 8168	9 + 5 = 14. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (9 + 5) = ;14
Theorem	9p6e15 8169	9 + 6 = 15. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (9 + 6) = ;15
Theorem	9p7e16 8170	9 + 7 = 16. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (9 + 7) = ;16
Theorem	9p8e17 8171	9 + 8 = 17. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (9 + 8) = ;17
Theorem	9p9e18 8172	9 + 9 = 18. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (9 + 9) = ;18
Theorem	10p10e20 8173	10 + 10 = 20. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (10 + 10) = ;20
Theorem	4t3lem 8174	Lemma for 4t3e12 8175 and related theorems. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ A ∈ ℕ0    &   ⊢ B ∈ ℕ0    &   ⊢ 𝐶 = (B + 1)    &   ⊢ (A · B) = 𝐷    &   ⊢ (𝐷 + A) = 𝐸    ⇒   ⊢ (A · 𝐶) = 𝐸
Theorem	4t3e12 8175	4 times 3 equals 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (4 · 3) = ;12
Theorem	4t4e16 8176	4 times 4 equals 16. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (4 · 4) = ;16
Theorem	5t3e15 8177	5 times 3 equals 15. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (5 · 3) = ;15
Theorem	5t4e20 8178	5 times 4 equals 20. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (5 · 4) = ;20
Theorem	5t5e25 8179	5 times 5 equals 25. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (5 · 5) = ;25
Theorem	6t2e12 8180	6 times 2 equals 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (6 · 2) = ;12
Theorem	6t3e18 8181	6 times 3 equals 18. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (6 · 3) = ;18
Theorem	6t4e24 8182	6 times 4 equals 24. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (6 · 4) = ;24
Theorem	6t5e30 8183	6 times 5 equals 30. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (6 · 5) = ;30
Theorem	6t6e36 8184	6 times 6 equals 36. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (6 · 6) = ;36
Theorem	7t2e14 8185	7 times 2 equals 14. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (7 · 2) = ;14
Theorem	7t3e21 8186	7 times 3 equals 21. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (7 · 3) = ;21
Theorem	7t4e28 8187	7 times 4 equals 28. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (7 · 4) = ;28
Theorem	7t5e35 8188	7 times 5 equals 35. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (7 · 5) = ;35
Theorem	7t6e42 8189	7 times 6 equals 42. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (7 · 6) = ;42
Theorem	7t7e49 8190	7 times 7 equals 49. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (7 · 7) = ;49
Theorem	8t2e16 8191	8 times 2 equals 16. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (8 · 2) = ;16
Theorem	8t3e24 8192	8 times 3 equals 24. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (8 · 3) = ;24
Theorem	8t4e32 8193	8 times 4 equals 32. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (8 · 4) = ;32
Theorem	8t5e40 8194	8 times 5 equals 40. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (8 · 5) = ;40
Theorem	8t6e48 8195	8 times 6 equals 48. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (8 · 6) = ;48
Theorem	8t7e56 8196	8 times 7 equals 56. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (8 · 7) = ;56
Theorem	8t8e64 8197	8 times 8 equals 64. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (8 · 8) = ;64
Theorem	9t2e18 8198	9 times 2 equals 18. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (9 · 2) = ;18
Theorem	9t3e27 8199	9 times 3 equals 27. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (9 · 3) = ;27
Theorem	9t4e36 8200	9 times 4 equals 36. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ (9 · 4) = ;36