HomeHome Intuitionistic Logic Explorer
Theorem List (p. 82 of 95)
< Previous  Next >
Bad symbols? Try the
GIF version.

Mirrors  >  Metamath Home Page  >  ILE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Theorem List for Intuitionistic Logic Explorer - 8101-8200   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theorempeano2uz2 8101* Second Peano postulate for upper integers. (Contributed by NM, 3-Oct-2004.)
((A B {x ℤ ∣ Ax}) → (B + 1) {x ℤ ∣ Ax})
 
Theorempeano5uzti 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))
 
Theorempeano5uzi 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)
 
Theoremdfuzi 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)}
 
Theoremuzind 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) → (φθ))    &   (𝑗 = 𝑁 → (φτ))    &   (𝑀 ℤ → ψ)    &   ((𝑀 𝑘 𝑀𝑘) → (χθ))       ((𝑀 𝑁 𝑀𝑁) → τ)
 
Theoremuzind2 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) → (φθ))    &   (𝑗 = 𝑁 → (φτ))    &   (𝑀 ℤ → ψ)    &   ((𝑀 𝑘 𝑀 < 𝑘) → (χθ))       ((𝑀 𝑁 𝑀 < 𝑁) → τ)
 
Theoremuzind3 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) → (φθ))    &   (𝑗 = 𝑁 → (φτ))    &   (𝑀 ℤ → ψ)    &   ((𝑀 𝑚 {𝑘 ℤ ∣ 𝑀𝑘}) → (χθ))       ((𝑀 𝑁 {𝑘 ℤ ∣ 𝑀𝑘}) → τ)
 
Theoremnn0ind 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τ)
 
Theoremfzind 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 < 𝑁)) → (χθ))       (((𝑀 𝑁 ℤ) (𝐾 𝑀𝐾 𝐾𝑁)) → τ)
 
Theoremfnn0ind 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 𝐾𝑁) → τ)
 
Theoremnn0ind-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τ)
 
Theoremzindd 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 ℤ → η))
 
Theorembtwnz 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))
 
Theoremnn0zd 8114 A positive integer is an integer. (Contributed by Mario Carneiro, 28-May-2016.)
(φA 0)       (φA ℤ)
 
Theoremnnzd 8115 A nonnegative integer is an integer. (Contributed by Mario Carneiro, 28-May-2016.)
(φA ℕ)       (φA ℤ)
 
Theoremzred 8116 An integer is a real number. (Contributed by Mario Carneiro, 28-May-2016.)
(φA ℤ)       (φA ℝ)
 
Theoremzcnd 8117 An integer is a complex number. (Contributed by Mario Carneiro, 28-May-2016.)
(φA ℤ)       (φA ℂ)
 
Theoremznegcld 8118 Closure law for negative integers. (Contributed by Mario Carneiro, 28-May-2016.)
(φA ℤ)       (φ → -A ℤ)
 
Theorempeano2zd 8119 Deduction from second Peano postulate generalized to integers. (Contributed by Mario Carneiro, 28-May-2016.)
(φA ℤ)       (φ → (A + 1) ℤ)
 
Theoremzaddcld 8120 Closure of addition of integers. (Contributed by Mario Carneiro, 28-May-2016.)
(φA ℤ)    &   (φB ℤ)       (φ → (A + B) ℤ)
 
Theoremzsubcld 8121 Closure of subtraction of integers. (Contributed by Mario Carneiro, 28-May-2016.)
(φA ℤ)    &   (φB ℤ)       (φ → (AB) ℤ)
 
Theoremzmulcld 8122 Closure of multiplication of integers. (Contributed by Mario Carneiro, 28-May-2016.)
(φA ℤ)    &   (φB ℤ)       (φ → (A · B) ℤ)
 
Theoremzadd2cl 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
 
Syntaxcdc 8124 Constant used for decimal constructor.
class AB
 
Definitiondf-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)
 
Theoremdeceq1 8126 Equality theorem for the decimal constructor. (Contributed by Mario Carneiro, 17-Apr-2015.)
(A = BA𝐶 = B𝐶)
 
Theoremdeceq2 8127 Equality theorem for the decimal constructor. (Contributed by Mario Carneiro, 17-Apr-2015.)
(A = B𝐶A = 𝐶B)
 
Theoremdeceq1i 8128 Equality theorem for the decimal constructor. (Contributed by Mario Carneiro, 17-Apr-2015.)
A = B       A𝐶 = B𝐶
 
Theoremdeceq2i 8129 Equality theorem for the decimal constructor. (Contributed by Mario Carneiro, 17-Apr-2015.)
A = B       𝐶A = 𝐶B
 
Theoremdeceq12i 8130 Equality theorem for the decimal constructor. (Contributed by Mario Carneiro, 17-Apr-2015.)
A = B    &   𝐶 = 𝐷       A𝐶 = B𝐷
 
Theoremnumnncl 8131 Closure for a numeral (with units place). (Contributed by Mario Carneiro, 18-Feb-2014.)
𝑇 0    &   A 0    &   B        ((𝑇 · A) + B)
 
Theoremnum0u 8132 Add a zero in the units place. (Contributed by Mario Carneiro, 18-Feb-2014.)
𝑇 0    &   A 0       (𝑇 · A) = ((𝑇 · A) + 0)
 
Theoremnum0h 8133 Add a zero in the higher places. (Contributed by Mario Carneiro, 18-Feb-2014.)
𝑇 0    &   A 0       A = ((𝑇 · 0) + A)
 
Theoremnumcl 8134 Closure for a decimal integer (with units place). (Contributed by Mario Carneiro, 18-Feb-2014.)
𝑇 0    &   A 0    &   B 0       ((𝑇 · A) + B) 0
 
Theoremnumsuc 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) + 𝐶)
 
Theoremdecnncl 8136 Closure for a numeral. (Contributed by Mario Carneiro, 17-Apr-2015.)
A 0    &   B        AB
 
Theoremdeccl 8137 Closure for a numeral. (Contributed by Mario Carneiro, 17-Apr-2015.)
A 0    &   B 0       AB 0
 
Theoremdec0u 8138 Add a zero in the units place. (Contributed by Mario Carneiro, 17-Apr-2015.)
A 0       (10 · A) = A0
 
Theoremdec0h 8139 Add a zero in the higher places. (Contributed by Mario Carneiro, 17-Apr-2015.)
A 0       A = 0A
 
Theoremnumnncl2 8140 Closure for a decimal integer (zero units place). (Contributed by Mario Carneiro, 9-Mar-2015.)
𝑇     &   A        ((𝑇 · A) + 0)
 
Theoremdecnncl2 8141 Closure for a decimal integer (zero units place). (Contributed by Mario Carneiro, 17-Apr-2015.)
A        A0
 
Theoremnumlt 8142 Comparing two decimal integers (equal higher places). (Contributed by Mario Carneiro, 18-Feb-2014.)
𝑇     &   A 0    &   B 0    &   𝐶     &   B < 𝐶       ((𝑇 · A) + B) < ((𝑇 · A) + 𝐶)
 
Theoremnumltc 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) + 𝐷)
 
Theoremdeclt 8144 Comparing two decimal integers (equal higher places). (Contributed by Mario Carneiro, 17-Apr-2015.)
A 0    &   B 0    &   𝐶     &   B < 𝐶       AB < A𝐶
 
Theoremdecltc 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𝐷
 
Theoremdecsuc 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𝐶
 
Theoremnumlti 8147 Comparing a digit to a decimal integer. (Contributed by Mario Carneiro, 18-Feb-2014.)
𝑇     &   A     &   B 0    &   𝐶 0    &   𝐶 < 𝑇       𝐶 < ((𝑇 · A) + B)
 
Theoremdeclti 8148 Comparing a digit to a decimal integer. (Contributed by Mario Carneiro, 18-Feb-2014.)
A     &   B 0    &   𝐶 0    &   𝐶 < 10       𝐶 < AB
 
Theoremnumsucc 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)
 
Theoremdecsucc 8150 The successor of a decimal integer (with carry). (Contributed by Mario Carneiro, 18-Feb-2014.)
A 0    &   (A + 1) = B    &   𝑁 = A9       (𝑁 + 1) = B0
 
Theorem1e0p1 8151 The successor of zero. (Contributed by Mario Carneiro, 18-Feb-2014.)
1 = (0 + 1)
 
Theoremdec10p 8152 Ten plus an integer. (Contributed by Mario Carneiro, 19-Apr-2015.)
(10 + A) = 1A
 
Theoremdec10 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
 
Theoremnumma 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 · 𝑃) + 𝐷) = 𝐹       ((𝑀 · 𝑃) + 𝑁) = ((𝑇 · 𝐸) + 𝐹)
 
Theoremnummac 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 · 𝑃) + 𝐷) = ((𝑇 · 𝐺) + 𝐹)       ((𝑀 · 𝑃) + 𝑁) = ((𝑇 · 𝐸) + 𝐹)
 
Theoremnumma2c 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) + 𝐷) = ((𝑇 · 𝐺) + 𝐹)       ((𝑃 · 𝑀) + 𝑁) = ((𝑇 · 𝐸) + 𝐹)
 
Theoremnumadd 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 + 𝐷) = 𝐹       (𝑀 + 𝑁) = ((𝑇 · 𝐸) + 𝐹)
 
Theoremnumaddc 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) + 𝐹)       (𝑀 + 𝑁) = ((𝑇 · 𝐸) + 𝐹)
 
Theoremnummul1c 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 · 𝑃) = ((𝑇 · 𝐸) + 𝐷)       (𝑁 · 𝑃) = ((𝑇 · 𝐶) + 𝐷)
 
Theoremnummul2c 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) = ((𝑇 · 𝐸) + 𝐷)       (𝑃 · 𝑁) = ((𝑇 · 𝐶) + 𝐷)
 
Theoremdecma 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 · 𝑃) + 𝐷) = 𝐹       ((𝑀 · 𝑃) + 𝑁) = 𝐸𝐹
 
Theoremdecmac 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 · 𝑃) + 𝐷) = 𝐺𝐹       ((𝑀 · 𝑃) + 𝑁) = 𝐸𝐹
 
Theoremdecma2c 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) + 𝐷) = 𝐺𝐹       ((𝑃 · 𝑀) + 𝑁) = 𝐸𝐹
 
Theoremdecadd 8164 Add two numerals 𝑀 and 𝑁 (no carry). (Contributed by Mario Carneiro, 18-Feb-2014.)
A 0    &   B 0    &   𝐶 0    &   𝐷 0    &   𝑀 = AB    &   𝑁 = 𝐶𝐷    &   (A + 𝐶) = 𝐸    &   (B + 𝐷) = 𝐹       (𝑀 + 𝑁) = 𝐸𝐹
 
Theoremdecaddc 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𝐹       (𝑀 + 𝑁) = 𝐸𝐹
 
Theoremdecaddc2 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
 
Theoremdecaddi 8167 Add two numerals 𝑀 and 𝑁 (no carry). (Contributed by Mario Carneiro, 18-Feb-2014.)
A 0    &   B 0    &   𝑁 0    &   𝑀 = AB    &   (B + 𝑁) = 𝐶       (𝑀 + 𝑁) = A𝐶
 
Theoremdecaddci 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𝐶       (𝑀 + 𝑁) = 𝐷𝐶
 
Theoremdecaddci2 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
 
Theoremdecmul1c 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 · 𝑃) = 𝐸𝐷       (𝑁 · 𝑃) = 𝐶𝐷
 
Theoremdecmul2c 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) = 𝐸𝐷       (𝑃 · 𝑁) = 𝐶𝐷
 
Theorem6p5lem 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𝐶
 
Theorem6p5e11 8173 6 + 5 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.)
(6 + 5) = 11
 
Theorem6p6e12 8174 6 + 6 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
(6 + 6) = 12
 
Theorem7p4e11 8175 7 + 4 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.)
(7 + 4) = 11
 
Theorem7p5e12 8176 7 + 5 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
(7 + 5) = 12
 
Theorem7p6e13 8177 7 + 6 = 13. (Contributed by Mario Carneiro, 19-Apr-2015.)
(7 + 6) = 13
 
Theorem7p7e14 8178 7 + 7 = 14. (Contributed by Mario Carneiro, 19-Apr-2015.)
(7 + 7) = 14
 
Theorem8p3e11 8179 8 + 3 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.)
(8 + 3) = 11
 
Theorem8p4e12 8180 8 + 4 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
(8 + 4) = 12
 
Theorem8p5e13 8181 8 + 5 = 13. (Contributed by Mario Carneiro, 19-Apr-2015.)
(8 + 5) = 13
 
Theorem8p6e14 8182 8 + 6 = 14. (Contributed by Mario Carneiro, 19-Apr-2015.)
(8 + 6) = 14
 
Theorem8p7e15 8183 8 + 7 = 15. (Contributed by Mario Carneiro, 19-Apr-2015.)
(8 + 7) = 15
 
Theorem8p8e16 8184 8 + 8 = 16. (Contributed by Mario Carneiro, 19-Apr-2015.)
(8 + 8) = 16
 
Theorem9p2e11 8185 9 + 2 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.)
(9 + 2) = 11
 
Theorem9p3e12 8186 9 + 3 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
(9 + 3) = 12
 
Theorem9p4e13 8187 9 + 4 = 13. (Contributed by Mario Carneiro, 19-Apr-2015.)
(9 + 4) = 13
 
Theorem9p5e14 8188 9 + 5 = 14. (Contributed by Mario Carneiro, 19-Apr-2015.)
(9 + 5) = 14
 
Theorem9p6e15 8189 9 + 6 = 15. (Contributed by Mario Carneiro, 19-Apr-2015.)
(9 + 6) = 15
 
Theorem9p7e16 8190 9 + 7 = 16. (Contributed by Mario Carneiro, 19-Apr-2015.)
(9 + 7) = 16
 
Theorem9p8e17 8191 9 + 8 = 17. (Contributed by Mario Carneiro, 19-Apr-2015.)
(9 + 8) = 17
 
Theorem9p9e18 8192 9 + 9 = 18. (Contributed by Mario Carneiro, 19-Apr-2015.)
(9 + 9) = 18
 
Theorem10p10e20 8193 10 + 10 = 20. (Contributed by Mario Carneiro, 19-Apr-2015.)
(10 + 10) = 20
 
Theorem4t3lem 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 · 𝐶) = 𝐸
 
Theorem4t3e12 8195 4 times 3 equals 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
(4 · 3) = 12
 
Theorem4t4e16 8196 4 times 4 equals 16. (Contributed by Mario Carneiro, 19-Apr-2015.)
(4 · 4) = 16
 
Theorem5t3e15 8197 5 times 3 equals 15. (Contributed by Mario Carneiro, 19-Apr-2015.)
(5 · 3) = 15
 
Theorem5t4e20 8198 5 times 4 equals 20. (Contributed by Mario Carneiro, 19-Apr-2015.)
(5 · 4) = 20
 
Theorem5t5e25 8199 5 times 5 equals 25. (Contributed by Mario Carneiro, 19-Apr-2015.)
(5 · 5) = 25
 
Theorem6t2e12 8200 6 times 2 equals 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
(6 · 2) = 12
    < Previous  Next >

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9427
  Copyright terms: Public domain < Previous  Next >