HomeTheorem List (p. 115 of 424)
GIF version.
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Metamath
Proof Explorer Theorem List (p. 115 of 424) | < Previous Next > |
| Bad symbols? Try the
GIF version. |
||
|
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
||
| Color key: | Metamath Proof Explorer
(1-27159) |
Hilbert Space Explorer
(27160-28684) |
Users' Mathboxes
(28685-42360) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | decnncl2 11401 | Closure for a decimal integer (zero units place). (Contributed by Mario Carneiro, 17-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
| ⊢ 𝐴 ∈ ℕ ⇒ ⊢ ;𝐴0 ∈ ℕ | ||
| Theorem | decnncl2OLD 11402 | Obsolete proof of decnncl2 11401 as of 6-Sep-2021. (Contributed by Mario Carneiro, 17-Apr-2015.) (New usage is discouraged.) (Proof modification is discouraged.) |
| ⊢ 𝐴 ∈ ℕ ⇒ ⊢ ;𝐴0 ∈ ℕ | ||
| Theorem | numlt 11403 | Comparing two decimal integers (equal higher places). (Contributed by Mario Carneiro, 18-Feb-2014.) |
| ⊢ 𝑇 ∈ ℕ & ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ & ⊢ 𝐵 < 𝐶 ⇒ ⊢ ((𝑇 · 𝐴) + 𝐵) < ((𝑇 · 𝐴) + 𝐶) | ||
| Theorem | numltc 11404 | Comparing two decimal integers (unequal higher places). (Contributed by Mario Carneiro, 18-Feb-2014.) |
| ⊢ 𝑇 ∈ ℕ & ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ0 & ⊢ 𝐷 ∈ ℕ0 & ⊢ 𝐶 < 𝑇 & ⊢ 𝐴 < 𝐵 ⇒ ⊢ ((𝑇 · 𝐴) + 𝐶) < ((𝑇 · 𝐵) + 𝐷) | ||
| Theorem | le9lt10 11405 | A "decimal digit" (i.e. a nonnegative integer less than or equal to 9) is less then 10. (Contributed by AV, 8-Sep-2021.) |
| ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐴 ≤ 9 ⇒ ⊢ 𝐴 < ;10 | ||
| Theorem | declt 11406 | Comparing two decimal integers (equal higher places). (Contributed by Mario Carneiro, 17-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
| ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ & ⊢ 𝐵 < 𝐶 ⇒ ⊢ ;𝐴𝐵 < ;𝐴𝐶 | ||
| Theorem | decltOLD 11407 | Obsolete proof of declt 11406 as of 6-Sep-2021. (Contributed by Mario Carneiro, 17-Apr-2015.) (New usage is discouraged.) (Proof modification is discouraged.) |
| ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ & ⊢ 𝐵 < 𝐶 ⇒ ⊢ ;𝐴𝐵 < ;𝐴𝐶 | ||
| Theorem | decltc 11408 | 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 | decltcOLD 11409 | Obsolete version of decltc 11408 as of 6-Sep-2021. (Contributed by Mario Carneiro, 17-Apr-2015.) (New usage is discouraged.) (Proof modification is discouraged.) |
| ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ0 & ⊢ 𝐷 ∈ ℕ0 & ⊢ 𝐶 < 10 & ⊢ 𝐴 < 𝐵 ⇒ ⊢ ;𝐴𝐶 < ;𝐵𝐷 | ||
| Theorem | declth 11410 | Comparing two decimal integers (unequal higher places). (Contributed by AV, 8-Sep-2021.) |
| ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ0 & ⊢ 𝐷 ∈ ℕ0 & ⊢ 𝐶 ≤ 9 & ⊢ 𝐴 < 𝐵 ⇒ ⊢ ;𝐴𝐶 < ;𝐵𝐷 | ||
| Theorem | decsuc 11411 | 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 | decsucOLD 11412 | Obsolete proof of decsuc 11411 as of 6-Sep-2021. (Contributed by Mario Carneiro, 17-Apr-2015.) (New usage is discouraged.) (Proof modification is discouraged.) |
| ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ (𝐵 + 1) = 𝐶 & ⊢ 𝑁 = ;𝐴𝐵 ⇒ ⊢ (𝑁 + 1) = ;𝐴𝐶 | ||
| Theorem | 3declth 11413 | 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 11414 | 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 | 3decltcOLD 11415 | Obsolete version of 3decltc 11414 as of 6-Sep-2021. (Contributed by AV, 15-Jun-2021.) (New usage is discouraged.) (Proof modification is discouraged.) |
| ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ0 & ⊢ 𝐷 ∈ ℕ0 & ⊢ 𝐸 ∈ ℕ0 & ⊢ 𝐹 ∈ ℕ0 & ⊢ 𝐶 < 10 & ⊢ 𝐸 < 10 & ⊢ 𝐴 < 𝐵 ⇒ ⊢ ;;𝐴𝐶𝐸 < ;;𝐵𝐷𝐹 | ||
| Theorem | decle 11416 | Comparing two decimal integers (equal higher places). (Contributed by AV, 17-Aug-2021.) (Revised by AV, 8-Sep-2021.) |
| ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ0 & ⊢ 𝐵 ≤ 𝐶 ⇒ ⊢ ;𝐴𝐵 ≤ ;𝐴𝐶 | ||
| Theorem | decleh 11417 | 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 11418 | Comparing a digit to a decimal integer. (Contributed by AV, 17-Aug-2021.) |
| ⊢ 𝐴 ∈ ℕ & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ0 & ⊢ 𝐶 ≤ 9 ⇒ ⊢ 𝐶 ≤ ;𝐴𝐵 | ||
| Theorem | decleOLD 11419 | Obsolete version of decle 11416 as of 8-Sep-2021. (Contributed by AV, 17-Aug-2021.) (New usage is discouraged.) (Proof modification is discouraged.) |
| ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ0 & ⊢ 𝐵 ≤ 𝐶 ⇒ ⊢ ;𝐴𝐵 ≤ ;𝐴𝐶 | ||
| Theorem | declecOLD 11420 | Obsolete version of decleh 11417 as of 8-Sep-2021. (Contributed by AV, 17-Aug-2021.) (New usage is discouraged.) (Proof modification is discouraged.) |
| ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ0 & ⊢ 𝐷 ∈ ℕ0 & ⊢ 𝐶 ≤ 9 & ⊢ 𝐴 < 𝐵 ⇒ ⊢ ;𝐴𝐶 ≤ ;𝐵𝐷 | ||
| Theorem | numlti 11421 | Comparing a digit to a decimal integer. (Contributed by Mario Carneiro, 18-Feb-2014.) |
| ⊢ 𝑇 ∈ ℕ & ⊢ 𝐴 ∈ ℕ & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ0 & ⊢ 𝐶 < 𝑇 ⇒ ⊢ 𝐶 < ((𝑇 · 𝐴) + 𝐵) | ||
| Theorem | declti 11422 | 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 11423 | Comparing a digit to a decimal integer. (Contributed by AV, 8-Sep-2021.) |
| ⊢ 𝐴 ∈ ℕ & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ0 & ⊢ 𝐶 ≤ 9 ⇒ ⊢ 𝐶 < ;𝐴𝐵 | ||
| Theorem | decltiOLD 11424 | Obsolete version of declti 11422 as of 6-Sep-2021. (Contributed by Mario Carneiro, 18-Feb-2014.) (New usage is discouraged.) (Proof modification is discouraged.) |
| ⊢ 𝐴 ∈ ℕ & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ0 & ⊢ 𝐶 < 10 ⇒ ⊢ 𝐶 < ;𝐴𝐵 | ||
| Theorem | numsucc 11425 | The successor of a decimal integer (with carry). (Contributed by Mario Carneiro, 18-Feb-2014.) |
| ⊢ 𝑌 ∈ ℕ0 & ⊢ 𝑇 = (𝑌 + 1) & ⊢ 𝐴 ∈ ℕ0 & ⊢ (𝐴 + 1) = 𝐵 & ⊢ 𝑁 = ((𝑇 · 𝐴) + 𝑌) ⇒ ⊢ (𝑁 + 1) = ((𝑇 · 𝐵) + 0) | ||
| Theorem | decsucc 11426 | 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 | decsuccOLD 11427 | Obsolete version of decsucc 11426 as of 6-Sep-2021. (Contributed by Mario Carneiro, 18-Feb-2014.) (New usage is discouraged.) (Proof modification is discouraged.) |
| ⊢ 𝐴 ∈ ℕ0 & ⊢ (𝐴 + 1) = 𝐵 & ⊢ 𝑁 = ;𝐴9 ⇒ ⊢ (𝑁 + 1) = ;𝐵0 | ||
| Theorem | 1e0p1 11428 | The successor of zero. (Contributed by Mario Carneiro, 18-Feb-2014.) |
| ⊢ 1 = (0 + 1) | ||
| Theorem | dec10p 11429 | Ten plus an integer. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
| ⊢ (;10 + 𝐴) = ;1𝐴 | ||
| Theorem | dec10pOLD 11430 | Obsolete version of dec10p 11429 as of 6-Sep-2021. (Contributed by Mario Carneiro, 19-Apr-2015.) (New usage is discouraged.) (Proof modification is discouraged.) |
| ⊢ (10 + 𝐴) = ;1𝐴 | ||
| Theorem | dec10OLD 11431 | 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.) Obsolete as of 6-Sep-2021, because the symbol 10 will be removed, and ;10 will be used instead in general. (New usage is discouraged.) (Proof modification is discouraged.) |
| ⊢ 10 = ;10 | ||
| Theorem | 9p1e10bOLD 11432 | Obsolete proof of 9p1e10 11372 as of 1-Aug-2021. (Contributed by Stanislas Polu, 7-Apr-2020.) (New usage is discouraged.) (Proof modification is discouraged.) |
| ⊢ (9 + 1) = ;10 | ||
| Theorem | numma 11433 | 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 11434 | 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 11435 | 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 11436 | Add two decimal integers 𝑀 and 𝑁 (no carry). (Contributed by Mario Carneiro, 18-Feb-2014.) |
| ⊢ 𝑇 ∈ ℕ0 & ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ0 & ⊢ 𝐷 ∈ ℕ0 & ⊢ 𝑀 = ((𝑇 · 𝐴) + 𝐵) & ⊢ 𝑁 = ((𝑇 · 𝐶) + 𝐷) & ⊢ (𝐴 + 𝐶) = 𝐸 & ⊢ (𝐵 + 𝐷) = 𝐹 ⇒ ⊢ (𝑀 + 𝑁) = ((𝑇 · 𝐸) + 𝐹) | ||
| Theorem | numaddc 11437 | Add two decimal integers 𝑀 and 𝑁 (with carry). (Contributed by Mario Carneiro, 18-Feb-2014.) |
| ⊢ 𝑇 ∈ ℕ0 & ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ0 & ⊢ 𝐷 ∈ ℕ0 & ⊢ 𝑀 = ((𝑇 · 𝐴) + 𝐵) & ⊢ 𝑁 = ((𝑇 · 𝐶) + 𝐷) & ⊢ 𝐹 ∈ ℕ0 & ⊢ ((𝐴 + 𝐶) + 1) = 𝐸 & ⊢ (𝐵 + 𝐷) = ((𝑇 · 1) + 𝐹) ⇒ ⊢ (𝑀 + 𝑁) = ((𝑇 · 𝐸) + 𝐹) | ||
| Theorem | nummul1c 11438 | The product of a decimal integer with a number. (Contributed by Mario Carneiro, 18-Feb-2014.) |
| ⊢ 𝑇 ∈ ℕ0 & ⊢ 𝑃 ∈ ℕ0 & ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝑁 = ((𝑇 · 𝐴) + 𝐵) & ⊢ 𝐷 ∈ ℕ0 & ⊢ 𝐸 ∈ ℕ0 & ⊢ ((𝐴 · 𝑃) + 𝐸) = 𝐶 & ⊢ (𝐵 · 𝑃) = ((𝑇 · 𝐸) + 𝐷) ⇒ ⊢ (𝑁 · 𝑃) = ((𝑇 · 𝐶) + 𝐷) | ||
| Theorem | nummul2c 11439 | 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 11440 | 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 | decmaOLD 11441 | Obsolete proof of decma 11440 as of 6-Sep-2021. (Contributed by Mario Carneiro, 18-Feb-2014.) (New usage is discouraged.) (Proof modification is discouraged.) |
| ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ0 & ⊢ 𝐷 ∈ ℕ0 & ⊢ 𝑀 = ;𝐴𝐵 & ⊢ 𝑁 = ;𝐶𝐷 & ⊢ 𝑃 ∈ ℕ0 & ⊢ ((𝐴 · 𝑃) + 𝐶) = 𝐸 & ⊢ ((𝐵 · 𝑃) + 𝐷) = 𝐹 ⇒ ⊢ ((𝑀 · 𝑃) + 𝑁) = ;𝐸𝐹 | ||
| Theorem | decmac 11442 | 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 | decmacOLD 11443 | Obsolete proof of decmac 11442 as of 6-Sep-2021. (Contributed by Mario Carneiro, 18-Feb-2014.) (New usage is discouraged.) (Proof modification is discouraged.) |
| ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ0 & ⊢ 𝐷 ∈ ℕ0 & ⊢ 𝑀 = ;𝐴𝐵 & ⊢ 𝑁 = ;𝐶𝐷 & ⊢ 𝑃 ∈ ℕ0 & ⊢ 𝐹 ∈ ℕ0 & ⊢ 𝐺 ∈ ℕ0 & ⊢ ((𝐴 · 𝑃) + (𝐶 + 𝐺)) = 𝐸 & ⊢ ((𝐵 · 𝑃) + 𝐷) = ;𝐺𝐹 ⇒ ⊢ ((𝑀 · 𝑃) + 𝑁) = ;𝐸𝐹 | ||
| Theorem | decma2c 11444 | 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 | decma2cOLD 11445 | Obsolete proof of decma2c 11444 as of 6-Sep-2021. (Contributed by Mario Carneiro, 18-Feb-2014.) (New usage is discouraged.) (Proof modification is discouraged.) |
| ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ0 & ⊢ 𝐷 ∈ ℕ0 & ⊢ 𝑀 = ;𝐴𝐵 & ⊢ 𝑁 = ;𝐶𝐷 & ⊢ 𝑃 ∈ ℕ0 & ⊢ 𝐹 ∈ ℕ0 & ⊢ 𝐺 ∈ ℕ0 & ⊢ ((𝑃 · 𝐴) + (𝐶 + 𝐺)) = 𝐸 & ⊢ ((𝑃 · 𝐵) + 𝐷) = ;𝐺𝐹 ⇒ ⊢ ((𝑃 · 𝑀) + 𝑁) = ;𝐸𝐹 | ||
| Theorem | decadd 11446 | Add two numerals 𝑀 and 𝑁 (no carry). (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by AV, 6-Sep-2021.) |
| ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ0 & ⊢ 𝐷 ∈ ℕ0 & ⊢ 𝑀 = ;𝐴𝐵 & ⊢ 𝑁 = ;𝐶𝐷 & ⊢ (𝐴 + 𝐶) = 𝐸 & ⊢ (𝐵 + 𝐷) = 𝐹 ⇒ ⊢ (𝑀 + 𝑁) = ;𝐸𝐹 | ||
| Theorem | decaddOLD 11447 | Obsolete proof of decadd 11446 as of 6-Sep-2021. (Contributed by Mario Carneiro, 18-Feb-2014.) (New usage is discouraged.) (Proof modification is discouraged.) |
| ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ0 & ⊢ 𝐷 ∈ ℕ0 & ⊢ 𝑀 = ;𝐴𝐵 & ⊢ 𝑁 = ;𝐶𝐷 & ⊢ (𝐴 + 𝐶) = 𝐸 & ⊢ (𝐵 + 𝐷) = 𝐹 ⇒ ⊢ (𝑀 + 𝑁) = ;𝐸𝐹 | ||
| Theorem | decaddc 11448 | 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𝐹 ⇒ ⊢ (𝑀 + 𝑁) = ;𝐸𝐹 | ||
| Theorem | decaddcOLD 11449 | Obsolete proof of decaddc 11448 as of 6-Sep-2021. (Contributed by Mario Carneiro, 18-Feb-2014.) (New usage is discouraged.) (Proof modification is discouraged.) |
| ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ0 & ⊢ 𝐷 ∈ ℕ0 & ⊢ 𝑀 = ;𝐴𝐵 & ⊢ 𝑁 = ;𝐶𝐷 & ⊢ ((𝐴 + 𝐶) + 1) = 𝐸 & ⊢ 𝐹 ∈ ℕ0 & ⊢ (𝐵 + 𝐷) = ;1𝐹 ⇒ ⊢ (𝑀 + 𝑁) = ;𝐸𝐹 | ||
| Theorem | decaddc2OLD 11450 | Obsolete version of decaddc2 11451 as of 6-Sep-2021. (Contributed by Mario Carneiro, 18-Feb-2014.) (New usage is discouraged.) (Proof modification is discouraged.) |
| ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ0 & ⊢ 𝐷 ∈ ℕ0 & ⊢ 𝑀 = ;𝐴𝐵 & ⊢ 𝑁 = ;𝐶𝐷 & ⊢ ((𝐴 + 𝐶) + 1) = 𝐸 & ⊢ (𝐵 + 𝐷) = 10 ⇒ ⊢ (𝑀 + 𝑁) = ;𝐸0 | ||
| Theorem | decaddc2 11451 | Add two numerals 𝑀 and 𝑁 (with carry). (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by AV, 6-Sep-2021.) |
| ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ0 & ⊢ 𝐷 ∈ ℕ0 & ⊢ 𝑀 = ;𝐴𝐵 & ⊢ 𝑁 = ;𝐶𝐷 & ⊢ ((𝐴 + 𝐶) + 1) = 𝐸 & ⊢ (𝐵 + 𝐷) = ;10 ⇒ ⊢ (𝑀 + 𝑁) = ;𝐸0 | ||
| Theorem | decrmanc 11452 | Perform a multiply-add of two numerals 𝑀 and 𝑁 against a fixed multiplicand 𝑃 (no carry). (Contributed by AV, 16-Sep-2021.) |
| ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝑁 ∈ ℕ0 & ⊢ 𝑀 = ;𝐴𝐵 & ⊢ 𝑃 ∈ ℕ0 & ⊢ (𝐴 · 𝑃) = 𝐸 & ⊢ ((𝐵 · 𝑃) + 𝑁) = 𝐹 ⇒ ⊢ ((𝑀 · 𝑃) + 𝑁) = ;𝐸𝐹 | ||
| Theorem | decrmac 11453 | Perform a multiply-add of two numerals 𝑀 and 𝑁 against a fixed multiplicand 𝑃 (with carry). (Contributed by AV, 16-Sep-2021.) |
| ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝑁 ∈ ℕ0 & ⊢ 𝑀 = ;𝐴𝐵 & ⊢ 𝑃 ∈ ℕ0 & ⊢ 𝐹 ∈ ℕ0 & ⊢ 𝐺 ∈ ℕ0 & ⊢ ((𝐴 · 𝑃) + 𝐺) = 𝐸 & ⊢ ((𝐵 · 𝑃) + 𝑁) = ;𝐺𝐹 ⇒ ⊢ ((𝑀 · 𝑃) + 𝑁) = ;𝐸𝐹 | ||
| Theorem | decaddm10 11454 | The sum of two multiples of 10 is a multiple of 10. (Contributed by AV, 30-Jul-2021.) |
| ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 ⇒ ⊢ (;𝐴0 + ;𝐵0) = ;(𝐴 + 𝐵)0 | ||
| Theorem | decaddi 11455 | Add two numerals 𝑀 and 𝑁 (no carry). (Contributed by Mario Carneiro, 18-Feb-2014.) |
| ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝑁 ∈ ℕ0 & ⊢ 𝑀 = ;𝐴𝐵 & ⊢ (𝐵 + 𝑁) = 𝐶 ⇒ ⊢ (𝑀 + 𝑁) = ;𝐴𝐶 | ||
| Theorem | decaddci 11456 | Add two numerals 𝑀 and 𝑁 (no carry). (Contributed by Mario Carneiro, 18-Feb-2014.) |
| ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝑁 ∈ ℕ0 & ⊢ 𝑀 = ;𝐴𝐵 & ⊢ (𝐴 + 1) = 𝐷 & ⊢ 𝐶 ∈ ℕ0 & ⊢ (𝐵 + 𝑁) = ;1𝐶 ⇒ ⊢ (𝑀 + 𝑁) = ;𝐷𝐶 | ||
| Theorem | decaddci2 11457 | Add two numerals 𝑀 and 𝑁 (no carry). (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by AV, 6-Sep-2021.) |
| ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝑁 ∈ ℕ0 & ⊢ 𝑀 = ;𝐴𝐵 & ⊢ (𝐴 + 1) = 𝐷 & ⊢ (𝐵 + 𝑁) = ;10 ⇒ ⊢ (𝑀 + 𝑁) = ;𝐷0 | ||
| Theorem | decaddci2OLD 11458 | Obsolete version of decaddci2 11457 as of 6-Sep-2021. (Contributed by Mario Carneiro, 18-Feb-2014.) (New usage is discouraged.) (Proof modification is discouraged.) |
| ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝑁 ∈ ℕ0 & ⊢ 𝑀 = ;𝐴𝐵 & ⊢ (𝐴 + 1) = 𝐷 & ⊢ (𝐵 + 𝑁) = 10 ⇒ ⊢ (𝑀 + 𝑁) = ;𝐷0 | ||
| Theorem | decsubi 11459 | Difference between a numeral 𝑀 and a nonnegative integer 𝑁 (no underflow). (Contributed by AV, 22-Jul-2021.) (Revised by AV, 6-Sep-2021.) |
| ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝑁 ∈ ℕ0 & ⊢ 𝑀 = ;𝐴𝐵 & ⊢ (𝐴 + 1) = 𝐷 & ⊢ (𝐵 − 𝑁) = 𝐶 ⇒ ⊢ (𝑀 − 𝑁) = ;𝐴𝐶 | ||
| Theorem | decsubiOLD 11460 | Obsolete proof of decsubi 11459 as of 6-Sep-2021. (Contributed by AV, 22-Jul-2021.) (New usage is discouraged.) (Proof modification is discouraged.) |
| ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝑁 ∈ ℕ0 & ⊢ 𝑀 = ;𝐴𝐵 & ⊢ (𝐴 + 1) = 𝐷 & ⊢ (𝐵 − 𝑁) = 𝐶 ⇒ ⊢ (𝑀 − 𝑁) = ;𝐴𝐶 | ||
| Theorem | decmul1 11461 | The product of a numeral with a number (no carry). (Contributed by AV, 22-Jul-2021.) (Revised by AV, 6-Sep-2021.) |
| ⊢ 𝑃 ∈ ℕ0 & ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝑁 = ;𝐴𝐵 & ⊢ 𝐷 ∈ ℕ0 & ⊢ (𝐴 · 𝑃) = 𝐶 & ⊢ (𝐵 · 𝑃) = 𝐷 ⇒ ⊢ (𝑁 · 𝑃) = ;𝐶𝐷 | ||
| Theorem | decmul1OLD 11462 | Obsolete proof of decmul1 11461 as of 6-Sep-2021. (Contributed by AV, 22-Jul-2021.) (New usage is discouraged.) (Proof modification is discouraged.) |
| ⊢ 𝑃 ∈ ℕ0 & ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝑁 = ;𝐴𝐵 & ⊢ 𝐷 ∈ ℕ0 & ⊢ (𝐴 · 𝑃) = 𝐶 & ⊢ (𝐵 · 𝑃) = 𝐷 ⇒ ⊢ (𝑁 · 𝑃) = ;𝐶𝐷 | ||
| Theorem | decmul1c 11463 | The product of a numeral with a number (with carry). (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by AV, 6-Sep-2021.) |
| ⊢ 𝑃 ∈ ℕ0 & ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝑁 = ;𝐴𝐵 & ⊢ 𝐷 ∈ ℕ0 & ⊢ 𝐸 ∈ ℕ0 & ⊢ ((𝐴 · 𝑃) + 𝐸) = 𝐶 & ⊢ (𝐵 · 𝑃) = ;𝐸𝐷 ⇒ ⊢ (𝑁 · 𝑃) = ;𝐶𝐷 | ||
| Theorem | decmul1cOLD 11464 | Obsolete proof of decmul1c 11463 as of 6-Sep-2021. (Contributed by Mario Carneiro, 18-Feb-2014.) (New usage is discouraged.) (Proof modification is discouraged.) |
| ⊢ 𝑃 ∈ ℕ0 & ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝑁 = ;𝐴𝐵 & ⊢ 𝐷 ∈ ℕ0 & ⊢ 𝐸 ∈ ℕ0 & ⊢ ((𝐴 · 𝑃) + 𝐸) = 𝐶 & ⊢ (𝐵 · 𝑃) = ;𝐸𝐷 ⇒ ⊢ (𝑁 · 𝑃) = ;𝐶𝐷 | ||
| Theorem | decmul2c 11465 | The product of a numeral with a number (with carry). (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by AV, 6-Sep-2021.) |
| ⊢ 𝑃 ∈ ℕ0 & ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝑁 = ;𝐴𝐵 & ⊢ 𝐷 ∈ ℕ0 & ⊢ 𝐸 ∈ ℕ0 & ⊢ ((𝑃 · 𝐴) + 𝐸) = 𝐶 & ⊢ (𝑃 · 𝐵) = ;𝐸𝐷 ⇒ ⊢ (𝑃 · 𝑁) = ;𝐶𝐷 | ||
| Theorem | decmul2cOLD 11466 | Obsolete proof of decmul2c 11465 as of 6-Sep-2021. (Contributed by Mario Carneiro, 18-Feb-2014.) (New usage is discouraged.) (Proof modification is discouraged.) |
| ⊢ 𝑃 ∈ ℕ0 & ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝑁 = ;𝐴𝐵 & ⊢ 𝐷 ∈ ℕ0 & ⊢ 𝐸 ∈ ℕ0 & ⊢ ((𝑃 · 𝐴) + 𝐸) = 𝐶 & ⊢ (𝑃 · 𝐵) = ;𝐸𝐷 ⇒ ⊢ (𝑃 · 𝑁) = ;𝐶𝐷 | ||
| Theorem | decmulnc 11467 | The product of a numeral with a number (no carry). (Contributed by AV, 15-Jun-2021.) |
| ⊢ 𝑁 ∈ ℕ0 & ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 ⇒ ⊢ (𝑁 · ;𝐴𝐵) = ;(𝑁 · 𝐴)(𝑁 · 𝐵) | ||
| Theorem | 11multnc 11468 | The product of 11 (as numeral) with a number (no carry). (Contributed by AV, 15-Jun-2021.) |
| ⊢ 𝑁 ∈ ℕ0 ⇒ ⊢ (𝑁 · ;11) = ;𝑁𝑁 | ||
| Theorem | decmul10add 11469 | A multiplication of a number and a numeral expressed as addition with first summand as multiple of 10. (Contributed by AV, 22-Jul-2021.) (Revised by AV, 6-Sep-2021.) |
| ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝑀 ∈ ℕ0 & ⊢ 𝐸 = (𝑀 · 𝐴) & ⊢ 𝐹 = (𝑀 · 𝐵) ⇒ ⊢ (𝑀 · ;𝐴𝐵) = (;𝐸0 + 𝐹) | ||
| Theorem | decmul10addOLD 11470 | Obsolete proof of decmul10add 11469 as of 6-Sep-2021. (Contributed by AV, 22-Jul-2021.) (New usage is discouraged.) (Proof modification is discouraged.) |
| ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝑀 ∈ ℕ0 & ⊢ 𝐸 = (𝑀 · 𝐴) & ⊢ 𝐹 = (𝑀 · 𝐵) ⇒ ⊢ (𝑀 · ;𝐴𝐵) = (;𝐸0 + 𝐹) | ||
| Theorem | 6p5lem 11471 | Lemma for 6p5e11 11476 and related theorems. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐷 ∈ ℕ0 & ⊢ 𝐸 ∈ ℕ0 & ⊢ 𝐵 = (𝐷 + 1) & ⊢ 𝐶 = (𝐸 + 1) & ⊢ (𝐴 + 𝐷) = ;1𝐸 ⇒ ⊢ (𝐴 + 𝐵) = ;1𝐶 | ||
| Theorem | 5p5e10 11472 | 5 + 5 = 10. (Contributed by NM, 5-Feb-2007.) (Revised by Stanislas Polu, 7-Apr-2020.) (Revised by AV, 6-Sep-2021.) |
| ⊢ (5 + 5) = ;10 | ||
| Theorem | 5p5e10bOLD 11473 | Obsolete proof of 5p5e10 11472 as of 6-Sep-2021. (Contributed by Stanislas Polu, 7-Apr-2020.) (New usage is discouraged.) (Proof modification is discouraged.) |
| ⊢ (5 + 5) = ;10 | ||
| Theorem | 6p4e10 11474 | 6 + 4 = 10. (Contributed by NM, 5-Feb-2007.) (Revised by Stanislas Polu, 7-Apr-2020.) (Revised by AV, 6-Sep-2021.) |
| ⊢ (6 + 4) = ;10 | ||
| Theorem | 6p4e10bOLD 11475 | Obsolete proof of 6p4e10 11474 as of 6-Sep-2021. (Contributed by Stanislas Polu, 7-Apr-2020.) (New usage is discouraged.) (Proof modification is discouraged.) |
| ⊢ (6 + 4) = ;10 | ||
| Theorem | 6p5e11 11476 | 6 + 5 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
| ⊢ (6 + 5) = ;11 | ||
| Theorem | 6p5e11OLD 11477 | Obsolete proof of 6p5e11 11476 as of 6-Sep-2021. (Contributed by Mario Carneiro, 19-Apr-2015.) (New usage is discouraged.) (Proof modification is discouraged.) |
| ⊢ (6 + 5) = ;11 | ||
| Theorem | 6p6e12 11478 | 6 + 6 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (6 + 6) = ;12 | ||
| Theorem | 7p3e10 11479 | 7 + 3 = 10. (Contributed by NM, 5-Feb-2007.) (Revised by Stanislas Polu, 7-Apr-2020.) (Revised by AV, 6-Sep-2021.) |
| ⊢ (7 + 3) = ;10 | ||
| Theorem | 7p3e10bOLD 11480 | Obsolete proof of 7p3e10 11479 as of 6-Sep-2021. (Contributed by Stanislas Polu, 7-Apr-2020.) (New usage is discouraged.) (Proof modification is discouraged.) |
| ⊢ (7 + 3) = ;10 | ||
| Theorem | 7p4e11 11481 | 7 + 4 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
| ⊢ (7 + 4) = ;11 | ||
| Theorem | 7p4e11OLD 11482 | Obsolete proof of 7p4e11 11481 as of 6-Sep-2021. (Contributed by Mario Carneiro, 19-Apr-2015.) (New usage is discouraged.) (Proof modification is discouraged.) |
| ⊢ (7 + 4) = ;11 | ||
| Theorem | 7p5e12 11483 | 7 + 5 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (7 + 5) = ;12 | ||
| Theorem | 7p6e13 11484 | 7 + 6 = 13. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (7 + 6) = ;13 | ||
| Theorem | 7p7e14 11485 | 7 + 7 = 14. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (7 + 7) = ;14 | ||
| Theorem | 8p2e10 11486 | 8 + 2 = 10. (Contributed by NM, 5-Feb-2007.) (Revised by Stanislas Polu, 7-Apr-2020.) (Revised by AV, 6-Sep-2021.) |
| ⊢ (8 + 2) = ;10 | ||
| Theorem | 8p2e10bOLD 11487 | Obsolete proof of 8p2e10 11486 as of 6-Sep-2021. (Contributed by Stanislas Polu, 7-Apr-2020.) (New usage is discouraged.) (Proof modification is discouraged.) |
| ⊢ (8 + 2) = ;10 | ||
| Theorem | 8p3e11 11488 | 8 + 3 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
| ⊢ (8 + 3) = ;11 | ||
| Theorem | 8p3e11OLD 11489 | Obsolete proof of 8p3e11 11488 as of 6-Sep-2021. (Contributed by Mario Carneiro, 19-Apr-2015.) (New usage is discouraged.) (Proof modification is discouraged.) |
| ⊢ (8 + 3) = ;11 | ||
| Theorem | 8p4e12 11490 | 8 + 4 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (8 + 4) = ;12 | ||
| Theorem | 8p5e13 11491 | 8 + 5 = 13. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (8 + 5) = ;13 | ||
| Theorem | 8p6e14 11492 | 8 + 6 = 14. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (8 + 6) = ;14 | ||
| Theorem | 8p7e15 11493 | 8 + 7 = 15. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (8 + 7) = ;15 | ||
| Theorem | 8p8e16 11494 | 8 + 8 = 16. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (8 + 8) = ;16 | ||
| Theorem | 9p2e11 11495 | 9 + 2 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
| ⊢ (9 + 2) = ;11 | ||
| Theorem | 9p2e11OLD 11496 | Obsolete proof of 9p2e11 11495 as of 6-Sep-2021. (Contributed by Mario Carneiro, 19-Apr-2015.) (New usage is discouraged.) (Proof modification is discouraged.) |
| ⊢ (9 + 2) = ;11 | ||
| Theorem | 9p3e12 11497 | 9 + 3 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (9 + 3) = ;12 | ||
| Theorem | 9p4e13 11498 | 9 + 4 = 13. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (9 + 4) = ;13 | ||
| Theorem | 9p5e14 11499 | 9 + 5 = 14. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (9 + 5) = ;14 | ||
| Theorem | 9p6e15 11500 | 9 + 6 = 15. (Contributed by Mario Carneiro, 19-Apr-2015.) |
| ⊢ (9 + 6) = ;15 | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |