Type | Label | Description |
Statement |
|
Theorem | 10nn0 9401 |
10 is a nonnegative integer. (Contributed by Mario Carneiro,
19-Apr-2015.) (Revised by AV, 6-Sep-2021.)
|
⊢ ;10 ∈ ℕ0 |
|
Theorem | 10re 9402 |
The number 10 is real. (Contributed by NM, 5-Feb-2007.) (Revised by AV,
8-Sep-2021.)
|
⊢ ;10 ∈ ℝ |
|
Theorem | decnncl 9403 |
Closure for a numeral. (Contributed by Mario Carneiro, 17-Apr-2015.)
(Revised by AV, 6-Sep-2021.)
|
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈
ℕ ⇒ ⊢ ;𝐴𝐵 ∈ ℕ |
|
Theorem | dec0u 9404 |
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 9405 |
Add a zero in the higher places. (Contributed by Mario Carneiro,
17-Apr-2015.) (Revised by AV, 6-Sep-2021.)
|
⊢ 𝐴 ∈
ℕ0 ⇒ ⊢ 𝐴 = ;0𝐴 |
|
Theorem | numnncl2 9406 |
Closure for a decimal integer (zero units place). (Contributed by Mario
Carneiro, 9-Mar-2015.)
|
⊢ 𝑇 ∈ ℕ & ⊢ 𝐴 ∈
ℕ ⇒ ⊢ ((𝑇 · 𝐴) + 0) ∈ ℕ |
|
Theorem | decnncl2 9407 |
Closure for a decimal integer (zero units place). (Contributed by Mario
Carneiro, 17-Apr-2015.) (Revised by AV, 6-Sep-2021.)
|
⊢ 𝐴 ∈ ℕ
⇒ ⊢ ;𝐴0 ∈ ℕ |
|
Theorem | numlt 9408 |
Comparing two decimal integers (equal higher places). (Contributed by
Mario Carneiro, 18-Feb-2014.)
|
⊢ 𝑇 ∈ ℕ & ⊢ 𝐴 ∈
ℕ0
& ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ & ⊢ 𝐵 < 𝐶 ⇒ ⊢ ((𝑇 · 𝐴) + 𝐵) < ((𝑇 · 𝐴) + 𝐶) |
|
Theorem | numltc 9409 |
Comparing two decimal integers (unequal higher places). (Contributed by
Mario Carneiro, 18-Feb-2014.)
|
⊢ 𝑇 ∈ ℕ & ⊢ 𝐴 ∈
ℕ0
& ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈
ℕ0
& ⊢ 𝐷 ∈ ℕ0 & ⊢ 𝐶 < 𝑇
& ⊢ 𝐴 < 𝐵 ⇒ ⊢ ((𝑇 · 𝐴) + 𝐶) < ((𝑇 · 𝐵) + 𝐷) |
|
Theorem | le9lt10 9410 |
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 9411 |
Comparing two decimal integers (equal higher places). (Contributed by
Mario Carneiro, 17-Apr-2015.) (Revised by AV, 6-Sep-2021.)
|
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈
ℕ0
& ⊢ 𝐶 ∈ ℕ & ⊢ 𝐵 < 𝐶 ⇒ ⊢ ;𝐴𝐵 < ;𝐴𝐶 |
|
Theorem | decltc 9412 |
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 9413 |
Comparing two decimal integers (unequal higher places). (Contributed
by AV, 8-Sep-2021.)
|
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈
ℕ0
& ⊢ 𝐶 ∈ ℕ0 & ⊢ 𝐷 ∈
ℕ0
& ⊢ 𝐶 ≤ 9 & ⊢ 𝐴 < 𝐵 ⇒ ⊢ ;𝐴𝐶 < ;𝐵𝐷 |
|
Theorem | decsuc 9414 |
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 9415 |
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 9416 |
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 9417 |
Comparing two decimal integers (equal higher places). (Contributed by
AV, 17-Aug-2021.) (Revised by AV, 8-Sep-2021.)
|
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈
ℕ0
& ⊢ 𝐶 ∈ ℕ0 & ⊢ 𝐵 ≤ 𝐶 ⇒ ⊢ ;𝐴𝐵 ≤ ;𝐴𝐶 |
|
Theorem | decleh 9418 |
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 9419 |
Comparing a digit to a decimal integer. (Contributed by AV,
17-Aug-2021.)
|
⊢ 𝐴 ∈ ℕ & ⊢ 𝐵 ∈
ℕ0
& ⊢ 𝐶 ∈ ℕ0 & ⊢ 𝐶 ≤
9 ⇒ ⊢ 𝐶 ≤ ;𝐴𝐵 |
|
Theorem | numlti 9420 |
Comparing a digit to a decimal integer. (Contributed by Mario Carneiro,
18-Feb-2014.)
|
⊢ 𝑇 ∈ ℕ & ⊢ 𝐴 ∈ ℕ & ⊢ 𝐵 ∈
ℕ0
& ⊢ 𝐶 ∈ ℕ0 & ⊢ 𝐶 < 𝑇 ⇒ ⊢ 𝐶 < ((𝑇 · 𝐴) + 𝐵) |
|
Theorem | declti 9421 |
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 9422 |
Comparing a digit to a decimal integer. (Contributed by AV,
8-Sep-2021.)
|
⊢ 𝐴 ∈ ℕ & ⊢ 𝐵 ∈
ℕ0
& ⊢ 𝐶 ∈ ℕ0 & ⊢ 𝐶 ≤
9 ⇒ ⊢ 𝐶 < ;𝐴𝐵 |
|
Theorem | numsucc 9423 |
The successor of a decimal integer (with carry). (Contributed by Mario
Carneiro, 18-Feb-2014.)
|
⊢ 𝑌 ∈ ℕ0 & ⊢ 𝑇 = (𝑌 + 1) & ⊢ 𝐴 ∈
ℕ0
& ⊢ (𝐴 + 1) = 𝐵
& ⊢ 𝑁 = ((𝑇 · 𝐴) + 𝑌) ⇒ ⊢ (𝑁 + 1) = ((𝑇 · 𝐵) + 0) |
|
Theorem | decsucc 9424 |
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 9425 |
The successor of zero. (Contributed by Mario Carneiro, 18-Feb-2014.)
|
⊢ 1 = (0 + 1) |
|
Theorem | dec10p 9426 |
Ten plus an integer. (Contributed by Mario Carneiro, 19-Apr-2015.)
(Revised by AV, 6-Sep-2021.)
|
⊢ (;10 + 𝐴) = ;1𝐴 |
|
Theorem | numma 9427 |
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 9428 |
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 9429 |
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 9430 |
Add two decimal integers 𝑀 and 𝑁 (no carry).
(Contributed by
Mario Carneiro, 18-Feb-2014.)
|
⊢ 𝑇 ∈ ℕ0 & ⊢ 𝐴 ∈
ℕ0
& ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈
ℕ0
& ⊢ 𝐷 ∈ ℕ0 & ⊢ 𝑀 = ((𝑇 · 𝐴) + 𝐵)
& ⊢ 𝑁 = ((𝑇 · 𝐶) + 𝐷)
& ⊢ (𝐴 + 𝐶) = 𝐸
& ⊢ (𝐵 + 𝐷) = 𝐹 ⇒ ⊢ (𝑀 + 𝑁) = ((𝑇 · 𝐸) + 𝐹) |
|
Theorem | numaddc 9431 |
Add two decimal integers 𝑀 and 𝑁 (with carry).
(Contributed
by Mario Carneiro, 18-Feb-2014.)
|
⊢ 𝑇 ∈ ℕ0 & ⊢ 𝐴 ∈
ℕ0
& ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈
ℕ0
& ⊢ 𝐷 ∈ ℕ0 & ⊢ 𝑀 = ((𝑇 · 𝐴) + 𝐵)
& ⊢ 𝑁 = ((𝑇 · 𝐶) + 𝐷)
& ⊢ 𝐹 ∈ ℕ0 & ⊢ ((𝐴 + 𝐶) + 1) = 𝐸
& ⊢ (𝐵 + 𝐷) = ((𝑇 · 1) + 𝐹) ⇒ ⊢ (𝑀 + 𝑁) = ((𝑇 · 𝐸) + 𝐹) |
|
Theorem | nummul1c 9432 |
The product of a decimal integer with a number. (Contributed by Mario
Carneiro, 18-Feb-2014.)
|
⊢ 𝑇 ∈ ℕ0 & ⊢ 𝑃 ∈
ℕ0
& ⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈
ℕ0
& ⊢ 𝑁 = ((𝑇 · 𝐴) + 𝐵)
& ⊢ 𝐷 ∈ ℕ0 & ⊢ 𝐸 ∈
ℕ0
& ⊢ ((𝐴 · 𝑃) + 𝐸) = 𝐶
& ⊢ (𝐵 · 𝑃) = ((𝑇 · 𝐸) + 𝐷) ⇒ ⊢ (𝑁 · 𝑃) = ((𝑇 · 𝐶) + 𝐷) |
|
Theorem | nummul2c 9433 |
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 9434 |
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 9435 |
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 9436 |
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 9437 |
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 9438 |
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 9439 |
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 9440 |
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 9441 |
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 9442 |
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 9443 |
Add two numerals 𝑀 and 𝑁 (no carry).
(Contributed by Mario
Carneiro, 18-Feb-2014.)
|
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈
ℕ0
& ⊢ 𝑁 ∈ ℕ0 & ⊢ 𝑀 = ;𝐴𝐵
& ⊢ (𝐵 + 𝑁) = 𝐶 ⇒ ⊢ (𝑀 + 𝑁) = ;𝐴𝐶 |
|
Theorem | decaddci 9444 |
Add two numerals 𝑀 and 𝑁 (no carry).
(Contributed by Mario
Carneiro, 18-Feb-2014.)
|
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈
ℕ0
& ⊢ 𝑁 ∈ ℕ0 & ⊢ 𝑀 = ;𝐴𝐵
& ⊢ (𝐴 + 1) = 𝐷
& ⊢ 𝐶 ∈ ℕ0 & ⊢ (𝐵 + 𝑁) = ;1𝐶 ⇒ ⊢ (𝑀 + 𝑁) = ;𝐷𝐶 |
|
Theorem | decaddci2 9445 |
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 9446 |
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 9447 |
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 | decmul1c 9448 |
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 9449 |
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 9450 |
The product of a numeral with a number (no carry). (Contributed by AV,
15-Jun-2021.)
|
⊢ 𝑁 ∈ ℕ0 & ⊢ 𝐴 ∈
ℕ0
& ⊢ 𝐵 ∈
ℕ0 ⇒ ⊢ (𝑁 · ;𝐴𝐵) = ;(𝑁 · 𝐴)(𝑁 · 𝐵) |
|
Theorem | 11multnc 9451 |
The product of 11 (as numeral) with a number (no carry). (Contributed
by AV, 15-Jun-2021.)
|
⊢ 𝑁 ∈
ℕ0 ⇒ ⊢ (𝑁 · ;11) = ;𝑁𝑁 |
|
Theorem | decmul10add 9452 |
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 9453 |
Lemma for 6p5e11 9456 and related theorems. (Contributed by Mario
Carneiro, 19-Apr-2015.)
|
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐷 ∈
ℕ0
& ⊢ 𝐸 ∈ ℕ0 & ⊢ 𝐵 = (𝐷 + 1) & ⊢ 𝐶 = (𝐸 + 1) & ⊢ (𝐴 + 𝐷) = ;1𝐸 ⇒ ⊢ (𝐴 + 𝐵) = ;1𝐶 |
|
Theorem | 5p5e10 9454 |
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 9455 |
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 9456 |
6 + 5 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by
AV, 6-Sep-2021.)
|
⊢ (6 + 5) = ;11 |
|
Theorem | 6p6e12 9457 |
6 + 6 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (6 + 6) = ;12 |
|
Theorem | 7p3e10 9458 |
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 9459 |
7 + 4 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by
AV, 6-Sep-2021.)
|
⊢ (7 + 4) = ;11 |
|
Theorem | 7p5e12 9460 |
7 + 5 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (7 + 5) = ;12 |
|
Theorem | 7p6e13 9461 |
7 + 6 = 13. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (7 + 6) = ;13 |
|
Theorem | 7p7e14 9462 |
7 + 7 = 14. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (7 + 7) = ;14 |
|
Theorem | 8p2e10 9463 |
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 9464 |
8 + 3 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by
AV, 6-Sep-2021.)
|
⊢ (8 + 3) = ;11 |
|
Theorem | 8p4e12 9465 |
8 + 4 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (8 + 4) = ;12 |
|
Theorem | 8p5e13 9466 |
8 + 5 = 13. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (8 + 5) = ;13 |
|
Theorem | 8p6e14 9467 |
8 + 6 = 14. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (8 + 6) = ;14 |
|
Theorem | 8p7e15 9468 |
8 + 7 = 15. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (8 + 7) = ;15 |
|
Theorem | 8p8e16 9469 |
8 + 8 = 16. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (8 + 8) = ;16 |
|
Theorem | 9p2e11 9470 |
9 + 2 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by
AV, 6-Sep-2021.)
|
⊢ (9 + 2) = ;11 |
|
Theorem | 9p3e12 9471 |
9 + 3 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (9 + 3) = ;12 |
|
Theorem | 9p4e13 9472 |
9 + 4 = 13. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (9 + 4) = ;13 |
|
Theorem | 9p5e14 9473 |
9 + 5 = 14. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (9 + 5) = ;14 |
|
Theorem | 9p6e15 9474 |
9 + 6 = 15. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (9 + 6) = ;15 |
|
Theorem | 9p7e16 9475 |
9 + 7 = 16. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (9 + 7) = ;16 |
|
Theorem | 9p8e17 9476 |
9 + 8 = 17. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (9 + 8) = ;17 |
|
Theorem | 9p9e18 9477 |
9 + 9 = 18. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (9 + 9) = ;18 |
|
Theorem | 10p10e20 9478 |
10 + 10 = 20. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by
AV, 6-Sep-2021.)
|
⊢ (;10 + ;10) = ;20 |
|
Theorem | 10m1e9 9479 |
10 - 1 = 9. (Contributed by AV, 6-Sep-2021.)
|
⊢ (;10 − 1) = 9 |
|
Theorem | 4t3lem 9480 |
Lemma for 4t3e12 9481 and related theorems. (Contributed by Mario
Carneiro, 19-Apr-2015.)
|
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈
ℕ0
& ⊢ 𝐶 = (𝐵 + 1) & ⊢ (𝐴 · 𝐵) = 𝐷
& ⊢ (𝐷 + 𝐴) = 𝐸 ⇒ ⊢ (𝐴 · 𝐶) = 𝐸 |
|
Theorem | 4t3e12 9481 |
4 times 3 equals 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (4 · 3) = ;12 |
|
Theorem | 4t4e16 9482 |
4 times 4 equals 16. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (4 · 4) = ;16 |
|
Theorem | 5t2e10 9483 |
5 times 2 equals 10. (Contributed by NM, 5-Feb-2007.) (Revised by AV,
4-Sep-2021.)
|
⊢ (5 · 2) = ;10 |
|
Theorem | 5t3e15 9484 |
5 times 3 equals 15. (Contributed by Mario Carneiro, 19-Apr-2015.)
(Revised by AV, 6-Sep-2021.)
|
⊢ (5 · 3) = ;15 |
|
Theorem | 5t4e20 9485 |
5 times 4 equals 20. (Contributed by Mario Carneiro, 19-Apr-2015.)
(Revised by AV, 6-Sep-2021.)
|
⊢ (5 · 4) = ;20 |
|
Theorem | 5t5e25 9486 |
5 times 5 equals 25. (Contributed by Mario Carneiro, 19-Apr-2015.)
(Revised by AV, 6-Sep-2021.)
|
⊢ (5 · 5) = ;25 |
|
Theorem | 6t2e12 9487 |
6 times 2 equals 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (6 · 2) = ;12 |
|
Theorem | 6t3e18 9488 |
6 times 3 equals 18. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (6 · 3) = ;18 |
|
Theorem | 6t4e24 9489 |
6 times 4 equals 24. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (6 · 4) = ;24 |
|
Theorem | 6t5e30 9490 |
6 times 5 equals 30. (Contributed by Mario Carneiro, 19-Apr-2015.)
(Revised by AV, 6-Sep-2021.)
|
⊢ (6 · 5) = ;30 |
|
Theorem | 6t6e36 9491 |
6 times 6 equals 36. (Contributed by Mario Carneiro, 19-Apr-2015.)
(Revised by AV, 6-Sep-2021.)
|
⊢ (6 · 6) = ;36 |
|
Theorem | 7t2e14 9492 |
7 times 2 equals 14. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (7 · 2) = ;14 |
|
Theorem | 7t3e21 9493 |
7 times 3 equals 21. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (7 · 3) = ;21 |
|
Theorem | 7t4e28 9494 |
7 times 4 equals 28. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (7 · 4) = ;28 |
|
Theorem | 7t5e35 9495 |
7 times 5 equals 35. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (7 · 5) = ;35 |
|
Theorem | 7t6e42 9496 |
7 times 6 equals 42. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (7 · 6) = ;42 |
|
Theorem | 7t7e49 9497 |
7 times 7 equals 49. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (7 · 7) = ;49 |
|
Theorem | 8t2e16 9498 |
8 times 2 equals 16. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (8 · 2) = ;16 |
|
Theorem | 8t3e24 9499 |
8 times 3 equals 24. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (8 · 3) = ;24 |
|
Theorem | 8t4e32 9500 |
8 times 4 equals 32. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
⊢ (8 · 4) = ;32 |