Home | Metamath
Proof Explorer Theorem List (p. 122 of 450) | < 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-28697) |
Hilbert Space Explorer
(28698-30220) |
Users' Mathboxes
(30221-44913) |
Type | Label | Description |
---|---|---|
Statement | ||
Syntax | cdc 12101 | Constant used for decimal constructor. |
class ;𝐴𝐵 | ||
Definition | df-dec 12102 | Define the "decimal constructor", which is used to build up "decimal integers" or "numeric terms" in base 10. For example, (;;;1000 + ;;;2000) = ;;;3000 1kp2ke3k 28227. (Contributed by Mario Carneiro, 17-Apr-2015.) (Revised by AV, 1-Aug-2021.) |
⊢ ;𝐴𝐵 = (((9 + 1) · 𝐴) + 𝐵) | ||
Theorem | 9p1e10 12103 | 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 12104 | 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 12105 | A decimal number is a set. (Contributed by Mario Carneiro, 17-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
⊢ ;𝐴𝐵 ∈ V | ||
Theorem | deceq1 12106 | Equality theorem for the decimal constructor. (Contributed by Mario Carneiro, 17-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
⊢ (𝐴 = 𝐵 → ;𝐴𝐶 = ;𝐵𝐶) | ||
Theorem | deceq2 12107 | Equality theorem for the decimal constructor. (Contributed by Mario Carneiro, 17-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
⊢ (𝐴 = 𝐵 → ;𝐶𝐴 = ;𝐶𝐵) | ||
Theorem | deceq1i 12108 | Equality theorem for the decimal constructor. (Contributed by Mario Carneiro, 17-Apr-2015.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ ;𝐴𝐶 = ;𝐵𝐶 | ||
Theorem | deceq2i 12109 | Equality theorem for the decimal constructor. (Contributed by Mario Carneiro, 17-Apr-2015.) |
⊢ 𝐴 = 𝐵 ⇒ ⊢ ;𝐶𝐴 = ;𝐶𝐵 | ||
Theorem | deceq12i 12110 | Equality theorem for the decimal constructor. (Contributed by Mario Carneiro, 17-Apr-2015.) |
⊢ 𝐴 = 𝐵 & ⊢ 𝐶 = 𝐷 ⇒ ⊢ ;𝐴𝐶 = ;𝐵𝐷 | ||
Theorem | numnncl 12111 | Closure for a numeral (with units place). (Contributed by Mario Carneiro, 18-Feb-2014.) |
⊢ 𝑇 ∈ ℕ0 & ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ ⇒ ⊢ ((𝑇 · 𝐴) + 𝐵) ∈ ℕ | ||
Theorem | num0u 12112 | Add a zero in the units place. (Contributed by Mario Carneiro, 18-Feb-2014.) |
⊢ 𝑇 ∈ ℕ0 & ⊢ 𝐴 ∈ ℕ0 ⇒ ⊢ (𝑇 · 𝐴) = ((𝑇 · 𝐴) + 0) | ||
Theorem | num0h 12113 | Add a zero in the higher places. (Contributed by Mario Carneiro, 18-Feb-2014.) |
⊢ 𝑇 ∈ ℕ0 & ⊢ 𝐴 ∈ ℕ0 ⇒ ⊢ 𝐴 = ((𝑇 · 0) + 𝐴) | ||
Theorem | numcl 12114 | Closure for a decimal integer (with units place). (Contributed by Mario Carneiro, 18-Feb-2014.) |
⊢ 𝑇 ∈ ℕ0 & ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 ⇒ ⊢ ((𝑇 · 𝐴) + 𝐵) ∈ ℕ0 | ||
Theorem | numsuc 12115 | The successor of a decimal integer (no carry). (Contributed by Mario Carneiro, 18-Feb-2014.) |
⊢ 𝑇 ∈ ℕ0 & ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ (𝐵 + 1) = 𝐶 & ⊢ 𝑁 = ((𝑇 · 𝐴) + 𝐵) ⇒ ⊢ (𝑁 + 1) = ((𝑇 · 𝐴) + 𝐶) | ||
Theorem | deccl 12116 | Closure for a numeral. (Contributed by Mario Carneiro, 17-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 ⇒ ⊢ ;𝐴𝐵 ∈ ℕ0 | ||
Theorem | 10nn 12117 | 10 is a positive integer. (Contributed by NM, 8-Nov-2012.) (Revised by AV, 6-Sep-2021.) |
⊢ ;10 ∈ ℕ | ||
Theorem | 10pos 12118 | The number 10 is positive. (Contributed by NM, 5-Feb-2007.) (Revised by AV, 8-Sep-2021.) |
⊢ 0 < ;10 | ||
Theorem | 10nn0 12119 | 10 is a nonnegative integer. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
⊢ ;10 ∈ ℕ0 | ||
Theorem | 10re 12120 | 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 12121 | Closure for a numeral. (Contributed by Mario Carneiro, 17-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ ⇒ ⊢ ;𝐴𝐵 ∈ ℕ | ||
Theorem | dec0u 12122 | 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 12123 | Add a zero in the higher places. (Contributed by Mario Carneiro, 17-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
⊢ 𝐴 ∈ ℕ0 ⇒ ⊢ 𝐴 = ;0𝐴 | ||
Theorem | numnncl2 12124 | Closure for a decimal integer (zero units place). (Contributed by Mario Carneiro, 9-Mar-2015.) |
⊢ 𝑇 ∈ ℕ & ⊢ 𝐴 ∈ ℕ ⇒ ⊢ ((𝑇 · 𝐴) + 0) ∈ ℕ | ||
Theorem | decnncl2 12125 | Closure for a decimal integer (zero units place). (Contributed by Mario Carneiro, 17-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
⊢ 𝐴 ∈ ℕ ⇒ ⊢ ;𝐴0 ∈ ℕ | ||
Theorem | numlt 12126 | Comparing two decimal integers (equal higher places). (Contributed by Mario Carneiro, 18-Feb-2014.) |
⊢ 𝑇 ∈ ℕ & ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ & ⊢ 𝐵 < 𝐶 ⇒ ⊢ ((𝑇 · 𝐴) + 𝐵) < ((𝑇 · 𝐴) + 𝐶) | ||
Theorem | numltc 12127 | Comparing two decimal integers (unequal higher places). (Contributed by Mario Carneiro, 18-Feb-2014.) |
⊢ 𝑇 ∈ ℕ & ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ0 & ⊢ 𝐷 ∈ ℕ0 & ⊢ 𝐶 < 𝑇 & ⊢ 𝐴 < 𝐵 ⇒ ⊢ ((𝑇 · 𝐴) + 𝐶) < ((𝑇 · 𝐵) + 𝐷) | ||
Theorem | le9lt10 12128 | 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 12129 | Comparing two decimal integers (equal higher places). (Contributed by Mario Carneiro, 17-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ & ⊢ 𝐵 < 𝐶 ⇒ ⊢ ;𝐴𝐵 < ;𝐴𝐶 | ||
Theorem | decltc 12130 | 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 12131 | Comparing two decimal integers (unequal higher places). (Contributed by AV, 8-Sep-2021.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ0 & ⊢ 𝐷 ∈ ℕ0 & ⊢ 𝐶 ≤ 9 & ⊢ 𝐴 < 𝐵 ⇒ ⊢ ;𝐴𝐶 < ;𝐵𝐷 | ||
Theorem | decsuc 12132 | 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 12133 | 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 12134 | 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 12135 | Comparing two decimal integers (equal higher places). (Contributed by AV, 17-Aug-2021.) (Revised by AV, 8-Sep-2021.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ0 & ⊢ 𝐵 ≤ 𝐶 ⇒ ⊢ ;𝐴𝐵 ≤ ;𝐴𝐶 | ||
Theorem | decleh 12136 | 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 12137 | Comparing a digit to a decimal integer. (Contributed by AV, 17-Aug-2021.) |
⊢ 𝐴 ∈ ℕ & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ0 & ⊢ 𝐶 ≤ 9 ⇒ ⊢ 𝐶 ≤ ;𝐴𝐵 | ||
Theorem | numlti 12138 | Comparing a digit to a decimal integer. (Contributed by Mario Carneiro, 18-Feb-2014.) |
⊢ 𝑇 ∈ ℕ & ⊢ 𝐴 ∈ ℕ & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ0 & ⊢ 𝐶 < 𝑇 ⇒ ⊢ 𝐶 < ((𝑇 · 𝐴) + 𝐵) | ||
Theorem | declti 12139 | 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 12140 | Comparing a digit to a decimal integer. (Contributed by AV, 8-Sep-2021.) |
⊢ 𝐴 ∈ ℕ & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ0 & ⊢ 𝐶 ≤ 9 ⇒ ⊢ 𝐶 < ;𝐴𝐵 | ||
Theorem | numsucc 12141 | The successor of a decimal integer (with carry). (Contributed by Mario Carneiro, 18-Feb-2014.) |
⊢ 𝑌 ∈ ℕ0 & ⊢ 𝑇 = (𝑌 + 1) & ⊢ 𝐴 ∈ ℕ0 & ⊢ (𝐴 + 1) = 𝐵 & ⊢ 𝑁 = ((𝑇 · 𝐴) + 𝑌) ⇒ ⊢ (𝑁 + 1) = ((𝑇 · 𝐵) + 0) | ||
Theorem | decsucc 12142 | 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 12143 | The successor of zero. (Contributed by Mario Carneiro, 18-Feb-2014.) |
⊢ 1 = (0 + 1) | ||
Theorem | dec10p 12144 | Ten plus an integer. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
⊢ (;10 + 𝐴) = ;1𝐴 | ||
Theorem | numma 12145 | 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 12146 | 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 12147 | 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 12148 | Add two decimal integers 𝑀 and 𝑁 (no carry). (Contributed by Mario Carneiro, 18-Feb-2014.) |
⊢ 𝑇 ∈ ℕ0 & ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ0 & ⊢ 𝐷 ∈ ℕ0 & ⊢ 𝑀 = ((𝑇 · 𝐴) + 𝐵) & ⊢ 𝑁 = ((𝑇 · 𝐶) + 𝐷) & ⊢ (𝐴 + 𝐶) = 𝐸 & ⊢ (𝐵 + 𝐷) = 𝐹 ⇒ ⊢ (𝑀 + 𝑁) = ((𝑇 · 𝐸) + 𝐹) | ||
Theorem | numaddc 12149 | Add two decimal integers 𝑀 and 𝑁 (with carry). (Contributed by Mario Carneiro, 18-Feb-2014.) |
⊢ 𝑇 ∈ ℕ0 & ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ0 & ⊢ 𝐷 ∈ ℕ0 & ⊢ 𝑀 = ((𝑇 · 𝐴) + 𝐵) & ⊢ 𝑁 = ((𝑇 · 𝐶) + 𝐷) & ⊢ 𝐹 ∈ ℕ0 & ⊢ ((𝐴 + 𝐶) + 1) = 𝐸 & ⊢ (𝐵 + 𝐷) = ((𝑇 · 1) + 𝐹) ⇒ ⊢ (𝑀 + 𝑁) = ((𝑇 · 𝐸) + 𝐹) | ||
Theorem | nummul1c 12150 | The product of a decimal integer with a number. (Contributed by Mario Carneiro, 18-Feb-2014.) |
⊢ 𝑇 ∈ ℕ0 & ⊢ 𝑃 ∈ ℕ0 & ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝑁 = ((𝑇 · 𝐴) + 𝐵) & ⊢ 𝐷 ∈ ℕ0 & ⊢ 𝐸 ∈ ℕ0 & ⊢ ((𝐴 · 𝑃) + 𝐸) = 𝐶 & ⊢ (𝐵 · 𝑃) = ((𝑇 · 𝐸) + 𝐷) ⇒ ⊢ (𝑁 · 𝑃) = ((𝑇 · 𝐶) + 𝐷) | ||
Theorem | nummul2c 12151 | 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 12152 | 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 12153 | 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 12154 | 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 12155 | 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 12156 | 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 | decaddc2 12157 | 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 12158 | 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 12159 | 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 12160 | 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 12161 | Add two numerals 𝑀 and 𝑁 (no carry). (Contributed by Mario Carneiro, 18-Feb-2014.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝑁 ∈ ℕ0 & ⊢ 𝑀 = ;𝐴𝐵 & ⊢ (𝐵 + 𝑁) = 𝐶 ⇒ ⊢ (𝑀 + 𝑁) = ;𝐴𝐶 | ||
Theorem | decaddci 12162 | Add two numerals 𝑀 and 𝑁 (no carry). (Contributed by Mario Carneiro, 18-Feb-2014.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝑁 ∈ ℕ0 & ⊢ 𝑀 = ;𝐴𝐵 & ⊢ (𝐴 + 1) = 𝐷 & ⊢ 𝐶 ∈ ℕ0 & ⊢ (𝐵 + 𝑁) = ;1𝐶 ⇒ ⊢ (𝑀 + 𝑁) = ;𝐷𝐶 | ||
Theorem | decaddci2 12163 | 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 | decsubi 12164 | 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 | decmul1 12165 | The product of a numeral with a number (no carry). (Contributed by AV, 22-Jul-2021.) (Revised by AV, 6-Sep-2021.) Remove hypothesis 𝐷 ∈ ℕ0. (Revised by Steven Nguyen, 7-Dec-2022.) |
⊢ 𝑃 ∈ ℕ0 & ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝑁 = ;𝐴𝐵 & ⊢ (𝐴 · 𝑃) = 𝐶 & ⊢ (𝐵 · 𝑃) = 𝐷 ⇒ ⊢ (𝑁 · 𝑃) = ;𝐶𝐷 | ||
Theorem | decmul1c 12166 | 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 | decmul2c 12167 | 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 | decmulnc 12168 | The product of a numeral with a number (no carry). (Contributed by AV, 15-Jun-2021.) |
⊢ 𝑁 ∈ ℕ0 & ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 ⇒ ⊢ (𝑁 · ;𝐴𝐵) = ;(𝑁 · 𝐴)(𝑁 · 𝐵) | ||
Theorem | 11multnc 12169 | The product of 11 (as numeral) with a number (no carry). (Contributed by AV, 15-Jun-2021.) |
⊢ 𝑁 ∈ ℕ0 ⇒ ⊢ (𝑁 · ;11) = ;𝑁𝑁 | ||
Theorem | decmul10add 12170 | 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 | 6p5lem 12171 | Lemma for 6p5e11 12174 and related theorems. (Contributed by Mario Carneiro, 19-Apr-2015.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐷 ∈ ℕ0 & ⊢ 𝐸 ∈ ℕ0 & ⊢ 𝐵 = (𝐷 + 1) & ⊢ 𝐶 = (𝐸 + 1) & ⊢ (𝐴 + 𝐷) = ;1𝐸 ⇒ ⊢ (𝐴 + 𝐵) = ;1𝐶 | ||
Theorem | 5p5e10 12172 | 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 | 6p4e10 12173 | 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 | 6p5e11 12174 | 6 + 5 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
⊢ (6 + 5) = ;11 | ||
Theorem | 6p6e12 12175 | 6 + 6 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.) |
⊢ (6 + 6) = ;12 | ||
Theorem | 7p3e10 12176 | 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 | 7p4e11 12177 | 7 + 4 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
⊢ (7 + 4) = ;11 | ||
Theorem | 7p5e12 12178 | 7 + 5 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.) |
⊢ (7 + 5) = ;12 | ||
Theorem | 7p6e13 12179 | 7 + 6 = 13. (Contributed by Mario Carneiro, 19-Apr-2015.) |
⊢ (7 + 6) = ;13 | ||
Theorem | 7p7e14 12180 | 7 + 7 = 14. (Contributed by Mario Carneiro, 19-Apr-2015.) |
⊢ (7 + 7) = ;14 | ||
Theorem | 8p2e10 12181 | 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 | 8p3e11 12182 | 8 + 3 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
⊢ (8 + 3) = ;11 | ||
Theorem | 8p4e12 12183 | 8 + 4 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.) |
⊢ (8 + 4) = ;12 | ||
Theorem | 8p5e13 12184 | 8 + 5 = 13. (Contributed by Mario Carneiro, 19-Apr-2015.) |
⊢ (8 + 5) = ;13 | ||
Theorem | 8p6e14 12185 | 8 + 6 = 14. (Contributed by Mario Carneiro, 19-Apr-2015.) |
⊢ (8 + 6) = ;14 | ||
Theorem | 8p7e15 12186 | 8 + 7 = 15. (Contributed by Mario Carneiro, 19-Apr-2015.) |
⊢ (8 + 7) = ;15 | ||
Theorem | 8p8e16 12187 | 8 + 8 = 16. (Contributed by Mario Carneiro, 19-Apr-2015.) |
⊢ (8 + 8) = ;16 | ||
Theorem | 9p2e11 12188 | 9 + 2 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
⊢ (9 + 2) = ;11 | ||
Theorem | 9p3e12 12189 | 9 + 3 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.) |
⊢ (9 + 3) = ;12 | ||
Theorem | 9p4e13 12190 | 9 + 4 = 13. (Contributed by Mario Carneiro, 19-Apr-2015.) |
⊢ (9 + 4) = ;13 | ||
Theorem | 9p5e14 12191 | 9 + 5 = 14. (Contributed by Mario Carneiro, 19-Apr-2015.) |
⊢ (9 + 5) = ;14 | ||
Theorem | 9p6e15 12192 | 9 + 6 = 15. (Contributed by Mario Carneiro, 19-Apr-2015.) |
⊢ (9 + 6) = ;15 | ||
Theorem | 9p7e16 12193 | 9 + 7 = 16. (Contributed by Mario Carneiro, 19-Apr-2015.) |
⊢ (9 + 7) = ;16 | ||
Theorem | 9p8e17 12194 | 9 + 8 = 17. (Contributed by Mario Carneiro, 19-Apr-2015.) |
⊢ (9 + 8) = ;17 | ||
Theorem | 9p9e18 12195 | 9 + 9 = 18. (Contributed by Mario Carneiro, 19-Apr-2015.) |
⊢ (9 + 9) = ;18 | ||
Theorem | 10p10e20 12196 | 10 + 10 = 20. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
⊢ (;10 + ;10) = ;20 | ||
Theorem | 10m1e9 12197 | 10 - 1 = 9. (Contributed by AV, 6-Sep-2021.) |
⊢ (;10 − 1) = 9 | ||
Theorem | 4t3lem 12198 | Lemma for 4t3e12 12199 and related theorems. (Contributed by Mario Carneiro, 19-Apr-2015.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 = (𝐵 + 1) & ⊢ (𝐴 · 𝐵) = 𝐷 & ⊢ (𝐷 + 𝐴) = 𝐸 ⇒ ⊢ (𝐴 · 𝐶) = 𝐸 | ||
Theorem | 4t3e12 12199 | 4 times 3 equals 12. (Contributed by Mario Carneiro, 19-Apr-2015.) |
⊢ (4 · 3) = ;12 | ||
Theorem | 4t4e16 12200 | 4 times 4 equals 16. (Contributed by Mario Carneiro, 19-Apr-2015.) |
⊢ (4 · 4) = ;16 |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |