Theorem List for Intuitionistic Logic Explorer - 9201-9300 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | zaddcld 9201 |
Closure of addition of integers. (Contributed by Mario Carneiro,
28-May-2016.)
|
![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![ZZ ZZ](bbz.gif) ![) )](rp.gif) |
|
Theorem | zsubcld 9202 |
Closure of subtraction of integers. (Contributed by Mario Carneiro,
28-May-2016.)
|
![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![ZZ ZZ](bbz.gif) ![) )](rp.gif) |
|
Theorem | zmulcld 9203 |
Closure of multiplication of integers. (Contributed by Mario Carneiro,
28-May-2016.)
|
![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![ZZ ZZ](bbz.gif) ![) )](rp.gif) |
|
Theorem | zadd2cl 9204 |
Increasing an integer by 2 results in an integer. (Contributed by
Alexander van der Vekens, 16-Sep-2018.)
|
![( (](lp.gif) ![( (](lp.gif) ![2 2](2.gif) ![ZZ ZZ](bbz.gif) ![) )](rp.gif) |
|
Theorem | btwnapz 9205 |
A number between an integer and its successor is apart from any integer.
(Contributed by Jim Kingdon, 6-Jan-2023.)
|
![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif) ![RR RR](bbr.gif) ![( (](lp.gif) ![ZZ ZZ](bbz.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) ![( (](lp.gif) # ![C C](_cc.gif) ![) )](rp.gif) |
|
4.4.10 Decimal arithmetic
|
|
Syntax | cdc 9206 |
Constant used for decimal constructor.
|
;![A A](_ca.gif) ![B B](_cb.gif) |
|
Definition | df-dec 9207 |
Define the "decimal constructor", which is used to build up
"decimal
integers" or "numeric terms" in base ![1 1](1.gif) . For example,
;;;![1 1](1.gif) ![0 0](0.gif) ![0 0](0.gif) ;;;![2 2](2.gif) ![0 0](0.gif) ![0 0](0.gif) ![0 0](0.gif) ;;;![3 3](3.gif) ![0 0](0.gif) ![0 0](0.gif) 1kp2ke3k 13107.
(Contributed by Mario Carneiro, 17-Apr-2015.) (Revised by AV,
1-Aug-2021.)
|
;![A A](_ca.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | 9p1e10 9208 |
9 + 1 = 10. (Contributed by Mario Carneiro, 18-Apr-2015.) (Revised by
Stanislas Polu, 7-Apr-2020.) (Revised by AV, 1-Aug-2021.)
|
![( (](lp.gif) ![1 1](1.gif) ;![1 1](1.gif) ![0 0](0.gif) |
|
Theorem | dfdec10 9209 |
Version of the definition of the "decimal constructor" using ;![1 1](1.gif)
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.)
|
;![A A](_ca.gif) ![( (](lp.gif) ;![1 1](1.gif) ![A A](_ca.gif)
![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | deceq1 9210 |
Equality theorem for the decimal constructor. (Contributed by Mario
Carneiro, 17-Apr-2015.) (Revised by AV, 6-Sep-2021.)
|
![( (](lp.gif) ;![A A](_ca.gif)
;![B B](_cb.gif) ![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | deceq2 9211 |
Equality theorem for the decimal constructor. (Contributed by Mario
Carneiro, 17-Apr-2015.) (Revised by AV, 6-Sep-2021.)
|
![( (](lp.gif) ;![C C](_cc.gif)
;![C C](_cc.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | deceq1i 9212 |
Equality theorem for the decimal constructor. (Contributed by Mario
Carneiro, 17-Apr-2015.)
|
;![A A](_ca.gif) ;![B B](_cb.gif) ![C C](_cc.gif) |
|
Theorem | deceq2i 9213 |
Equality theorem for the decimal constructor. (Contributed by Mario
Carneiro, 17-Apr-2015.)
|
;![C C](_cc.gif) ;![C C](_cc.gif) ![B B](_cb.gif) |
|
Theorem | deceq12i 9214 |
Equality theorem for the decimal constructor. (Contributed by Mario
Carneiro, 17-Apr-2015.)
|
;![A A](_ca.gif) ;![B B](_cb.gif) ![D D](_cd.gif) |
|
Theorem | numnncl 9215 |
Closure for a numeral (with units place). (Contributed by Mario
Carneiro, 18-Feb-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![B B](_cb.gif)
![NN NN](bbn.gif) |
|
Theorem | num0u 9216 |
Add a zero in the units place. (Contributed by Mario Carneiro,
18-Feb-2014.)
|
![( (](lp.gif) ![A A](_ca.gif)
![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![0 0](0.gif) ![) )](rp.gif) |
|
Theorem | num0h 9217 |
Add a zero in the higher places. (Contributed by Mario Carneiro,
18-Feb-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![0 0](0.gif) ![A A](_ca.gif) ![) )](rp.gif) |
|
Theorem | numcl 9218 |
Closure for a decimal integer (with units place). (Contributed by Mario
Carneiro, 18-Feb-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif)
![B B](_cb.gif)
![NN0 NN0](_bbn0.gif) |
|
Theorem | numsuc 9219 |
The successor of a decimal integer (no carry). (Contributed by Mario
Carneiro, 18-Feb-2014.)
|
![( (](lp.gif) ![1 1](1.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif)
![B B](_cb.gif) ![( (](lp.gif) ![1 1](1.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | deccl 9220 |
Closure for a numeral. (Contributed by Mario Carneiro, 17-Apr-2015.)
(Revised by AV, 6-Sep-2021.)
|
;![A A](_ca.gif) ![NN0 NN0](_bbn0.gif) |
|
Theorem | 10nn 9221 |
10 is a positive integer. (Contributed by NM, 8-Nov-2012.) (Revised by
AV, 6-Sep-2021.)
|
;![1 1](1.gif) ![NN NN](bbn.gif) |
|
Theorem | 10pos 9222 |
The number 10 is positive. (Contributed by NM, 5-Feb-2007.) (Revised by
AV, 8-Sep-2021.)
|
;![1 1](1.gif) ![0 0](0.gif) |
|
Theorem | 10nn0 9223 |
10 is a nonnegative integer. (Contributed by Mario Carneiro,
19-Apr-2015.) (Revised by AV, 6-Sep-2021.)
|
;![1 1](1.gif) ![NN0 NN0](_bbn0.gif) |
|
Theorem | 10re 9224 |
The number 10 is real. (Contributed by NM, 5-Feb-2007.) (Revised by AV,
8-Sep-2021.)
|
;![1 1](1.gif) ![RR RR](bbr.gif) |
|
Theorem | decnncl 9225 |
Closure for a numeral. (Contributed by Mario Carneiro, 17-Apr-2015.)
(Revised by AV, 6-Sep-2021.)
|
;![A A](_ca.gif) ![NN NN](bbn.gif) |
|
Theorem | dec0u 9226 |
Add a zero in the units place. (Contributed by Mario Carneiro,
17-Apr-2015.) (Revised by AV, 6-Sep-2021.)
|
;![1 1](1.gif) ![A A](_ca.gif)
;![A A](_ca.gif) ![0 0](0.gif) |
|
Theorem | dec0h 9227 |
Add a zero in the higher places. (Contributed by Mario Carneiro,
17-Apr-2015.) (Revised by AV, 6-Sep-2021.)
|
;![0 0](0.gif) ![A A](_ca.gif) |
|
Theorem | numnncl2 9228 |
Closure for a decimal integer (zero units place). (Contributed by Mario
Carneiro, 9-Mar-2015.)
|
![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif)
![0 0](0.gif) ![NN NN](bbn.gif) |
|
Theorem | decnncl2 9229 |
Closure for a decimal integer (zero units place). (Contributed by Mario
Carneiro, 17-Apr-2015.) (Revised by AV, 6-Sep-2021.)
|
;![A A](_ca.gif) ![NN NN](bbn.gif) |
|
Theorem | numlt 9230 |
Comparing two decimal integers (equal higher places). (Contributed by
Mario Carneiro, 18-Feb-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif)
![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![C C](_cc.gif) ![) )](rp.gif) |
|
Theorem | numltc 9231 |
Comparing two decimal integers (unequal higher places). (Contributed by
Mario Carneiro, 18-Feb-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif)
![C C](_cc.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![D D](_cd.gif) ![) )](rp.gif) |
|
Theorem | le9lt10 9232 |
A "decimal digit" (i.e. a nonnegative integer less than or equal to
9)
is less then 10. (Contributed by AV, 8-Sep-2021.)
|
;![1 1](1.gif) ![0 0](0.gif) |
|
Theorem | declt 9233 |
Comparing two decimal integers (equal higher places). (Contributed by
Mario Carneiro, 17-Apr-2015.) (Revised by AV, 6-Sep-2021.)
|
;![A A](_ca.gif) ;![A A](_ca.gif) ![C C](_cc.gif) |
|
Theorem | decltc 9234 |
Comparing two decimal integers (unequal higher places). (Contributed
by Mario Carneiro, 18-Feb-2014.) (Revised by AV, 6-Sep-2021.)
|
;![1 1](1.gif) ;![A A](_ca.gif) ;![B B](_cb.gif) ![D D](_cd.gif) |
|
Theorem | declth 9235 |
Comparing two decimal integers (unequal higher places). (Contributed
by AV, 8-Sep-2021.)
|
;![A A](_ca.gif) ;![B B](_cb.gif) ![D D](_cd.gif) |
|
Theorem | decsuc 9236 |
The successor of a decimal integer (no carry). (Contributed by Mario
Carneiro, 17-Apr-2015.) (Revised by AV, 6-Sep-2021.)
|
![( (](lp.gif) ![1 1](1.gif) ;![A A](_ca.gif) ![( (](lp.gif) ![1 1](1.gif) ;![A A](_ca.gif) ![C C](_cc.gif) |
|
Theorem | 3declth 9237 |
Comparing two decimal integers with three "digits" (unequal higher
places). (Contributed by AV, 8-Sep-2021.)
|
;;![A A](_ca.gif) ![C C](_cc.gif)
;;![B B](_cb.gif) ![D D](_cd.gif) ![F F](_cf.gif) |
|
Theorem | 3decltc 9238 |
Comparing two decimal integers with three "digits" (unequal higher
places). (Contributed by AV, 15-Jun-2021.) (Revised by AV,
6-Sep-2021.)
|
;![1 1](1.gif)
;![1 1](1.gif) ;;![A A](_ca.gif) ![C C](_cc.gif) ;;![B B](_cb.gif) ![D D](_cd.gif) ![F F](_cf.gif) |
|
Theorem | decle 9239 |
Comparing two decimal integers (equal higher places). (Contributed by
AV, 17-Aug-2021.) (Revised by AV, 8-Sep-2021.)
|
;![A A](_ca.gif) ;![A A](_ca.gif) ![C C](_cc.gif) |
|
Theorem | decleh 9240 |
Comparing two decimal integers (unequal higher places). (Contributed by
AV, 17-Aug-2021.) (Revised by AV, 8-Sep-2021.)
|
;![A A](_ca.gif) ;![B B](_cb.gif) ![D D](_cd.gif) |
|
Theorem | declei 9241 |
Comparing a digit to a decimal integer. (Contributed by AV,
17-Aug-2021.)
|
;![A A](_ca.gif) ![B B](_cb.gif) |
|
Theorem | numlti 9242 |
Comparing a digit to a decimal integer. (Contributed by Mario Carneiro,
18-Feb-2014.)
|
![( (](lp.gif) ![(
(](lp.gif) ![A A](_ca.gif)
![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | declti 9243 |
Comparing a digit to a decimal integer. (Contributed by Mario
Carneiro, 18-Feb-2014.) (Revised by AV, 6-Sep-2021.)
|
;![1 1](1.gif)
;![A A](_ca.gif) ![B B](_cb.gif) |
|
Theorem | decltdi 9244 |
Comparing a digit to a decimal integer. (Contributed by AV,
8-Sep-2021.)
|
;![A A](_ca.gif) ![B B](_cb.gif) |
|
Theorem | numsucc 9245 |
The successor of a decimal integer (with carry). (Contributed by Mario
Carneiro, 18-Feb-2014.)
|
![( (](lp.gif) ![1 1](1.gif) ![( (](lp.gif) ![1 1](1.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif)
![Y Y](_cy.gif) ![( (](lp.gif) ![1 1](1.gif) ![( (](lp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![0 0](0.gif) ![) )](rp.gif) |
|
Theorem | decsucc 9246 |
The successor of a decimal integer (with carry). (Contributed by Mario
Carneiro, 18-Feb-2014.) (Revised by AV, 6-Sep-2021.)
|
![( (](lp.gif) ![1 1](1.gif) ;![A A](_ca.gif) ![( (](lp.gif) ![1 1](1.gif) ;![B B](_cb.gif) ![0 0](0.gif) |
|
Theorem | 1e0p1 9247 |
The successor of zero. (Contributed by Mario Carneiro, 18-Feb-2014.)
|
![( (](lp.gif) ![1 1](1.gif) ![) )](rp.gif) |
|
Theorem | dec10p 9248 |
Ten plus an integer. (Contributed by Mario Carneiro, 19-Apr-2015.)
(Revised by AV, 6-Sep-2021.)
|
;![1 1](1.gif) ![A A](_ca.gif)
;![1 1](1.gif) ![A A](_ca.gif) |
|
Theorem | numma 9249 |
Perform a multiply-add of two decimal integers and against
a fixed multiplicand (no carry). (Contributed by Mario
Carneiro, 18-Feb-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif)
![D D](_cd.gif) ![( (](lp.gif) ![( (](lp.gif) ![P P](_cp.gif)
![C C](_cc.gif)
![( (](lp.gif) ![( (](lp.gif) ![P P](_cp.gif) ![D D](_cd.gif)
![( (](lp.gif) ![(
(](lp.gif) ![P P](_cp.gif)
![N N](_cn.gif) ![( (](lp.gif) ![( (](lp.gif) ![E E](_ce.gif)
![F F](_cf.gif) ![) )](rp.gif) |
|
Theorem | nummac 9250 |
Perform a multiply-add of two decimal integers and against
a fixed multiplicand (with carry). (Contributed by Mario
Carneiro, 18-Feb-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif)
![D D](_cd.gif) ![( (](lp.gif) ![( (](lp.gif) ![P P](_cp.gif)
![( (](lp.gif)
![G G](_cg.gif) ![) )](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![P P](_cp.gif)
![D D](_cd.gif) ![( (](lp.gif) ![( (](lp.gif) ![G G](_cg.gif)
![F F](_cf.gif) ![( (](lp.gif) ![( (](lp.gif) ![P P](_cp.gif)
![N N](_cn.gif)
![( (](lp.gif) ![( (](lp.gif) ![E E](_ce.gif) ![F F](_cf.gif) ![) )](rp.gif) |
|
Theorem | numma2c 9251 |
Perform a multiply-add of two decimal integers and against
a fixed multiplicand (with carry). (Contributed by Mario
Carneiro, 18-Feb-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif)
![D D](_cd.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif)
![( (](lp.gif)
![G G](_cg.gif) ![) )](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![B B](_cb.gif)
![D D](_cd.gif) ![( (](lp.gif) ![( (](lp.gif) ![G G](_cg.gif)
![F F](_cf.gif) ![( (](lp.gif) ![( (](lp.gif) ![M M](_cm.gif)
![N N](_cn.gif)
![( (](lp.gif) ![( (](lp.gif) ![E E](_ce.gif) ![F F](_cf.gif) ![) )](rp.gif) |
|
Theorem | numadd 9252 |
Add two decimal integers and (no
carry). (Contributed by
Mario Carneiro, 18-Feb-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif)
![D D](_cd.gif) ![( (](lp.gif) ![C C](_cc.gif)
![( (](lp.gif) ![D D](_cd.gif)
![( (](lp.gif)
![N N](_cn.gif) ![( (](lp.gif) ![( (](lp.gif) ![E E](_ce.gif)
![F F](_cf.gif) ![) )](rp.gif) |
|
Theorem | numaddc 9253 |
Add two decimal integers and (with
carry). (Contributed
by Mario Carneiro, 18-Feb-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif)
![D D](_cd.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif)
![1 1](1.gif) ![( (](lp.gif)
![D D](_cd.gif) ![( (](lp.gif) ![( (](lp.gif) ![1 1](1.gif)
![F F](_cf.gif) ![( (](lp.gif) ![N N](_cn.gif)
![( (](lp.gif) ![( (](lp.gif) ![E E](_ce.gif) ![F F](_cf.gif) ![) )](rp.gif) |
|
Theorem | nummul1c 9254 |
The product of a decimal integer with a number. (Contributed by Mario
Carneiro, 18-Feb-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ![P P](_cp.gif)
![E E](_ce.gif)
![( (](lp.gif) ![P P](_cp.gif)
![( (](lp.gif) ![(
(](lp.gif) ![E E](_ce.gif)
![D D](_cd.gif) ![( (](lp.gif) ![P P](_cp.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif)
![D D](_cd.gif) ![) )](rp.gif) |
|
Theorem | nummul2c 9255 |
The product of a decimal integer with a number (with carry).
(Contributed by Mario Carneiro, 18-Feb-2014.)
|
![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif) ![B B](_cb.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif)
![E E](_ce.gif)
![( (](lp.gif) ![B B](_cb.gif)
![( (](lp.gif) ![(
(](lp.gif) ![E E](_ce.gif)
![D D](_cd.gif) ![( (](lp.gif) ![N N](_cn.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif)
![D D](_cd.gif) ![) )](rp.gif) |
|
Theorem | decma 9256 |
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.)
|
;![A A](_ca.gif) ;![C C](_cc.gif) ![( (](lp.gif) ![(
(](lp.gif) ![P P](_cp.gif)
![C C](_cc.gif) ![( (](lp.gif) ![( (](lp.gif) ![P P](_cp.gif) ![D D](_cd.gif)
![( (](lp.gif) ![(
(](lp.gif) ![P P](_cp.gif)
![N N](_cn.gif) ;![E E](_ce.gif) ![F F](_cf.gif) |
|
Theorem | decmac 9257 |
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.)
|
;![A A](_ca.gif) ;![C C](_cc.gif) ![( (](lp.gif) ![( (](lp.gif) ![P P](_cp.gif)
![( (](lp.gif)
![G G](_cg.gif) ![) )](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![P P](_cp.gif)
![D D](_cd.gif) ;![G G](_cg.gif) ![( (](lp.gif) ![( (](lp.gif) ![P P](_cp.gif)
![N N](_cn.gif)
;![E E](_ce.gif) ![F F](_cf.gif) |
|
Theorem | decma2c 9258 |
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.)
|
;![A A](_ca.gif) ;![C C](_cc.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif)
![( (](lp.gif)
![G G](_cg.gif) ![) )](rp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![B B](_cb.gif)
![D D](_cd.gif) ;![G G](_cg.gif) ![( (](lp.gif) ![( (](lp.gif) ![M M](_cm.gif)
![N N](_cn.gif)
;![E E](_ce.gif) ![F F](_cf.gif) |
|
Theorem | decadd 9259 |
Add two numerals and
(no carry).
(Contributed by Mario
Carneiro, 18-Feb-2014.) (Revised by AV, 6-Sep-2021.)
|
;![A A](_ca.gif) ;![C C](_cc.gif) ![( (](lp.gif) ![C C](_cc.gif)
![( (](lp.gif)
![D D](_cd.gif) ![( (](lp.gif) ![N N](_cn.gif)
;![E E](_ce.gif) ![F F](_cf.gif) |
|
Theorem | decaddc 9260 |
Add two numerals and
(with carry).
(Contributed by Mario
Carneiro, 18-Feb-2014.) (Revised by AV, 6-Sep-2021.)
|
;![A A](_ca.gif) ;![C C](_cc.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![1 1](1.gif)
![( (](lp.gif) ![D D](_cd.gif)
;![1 1](1.gif) ![( (](lp.gif) ![N N](_cn.gif)
;![E E](_ce.gif) ![F F](_cf.gif) |
|
Theorem | decaddc2 9261 |
Add two numerals and
(with carry).
(Contributed by Mario
Carneiro, 18-Feb-2014.) (Revised by AV, 6-Sep-2021.)
|
;![A A](_ca.gif) ;![C C](_cc.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![1 1](1.gif)
![( (](lp.gif)
![D D](_cd.gif) ;![1 1](1.gif) ![( (](lp.gif) ![N N](_cn.gif)
;![E E](_ce.gif) ![0 0](0.gif) |
|
Theorem | decrmanc 9262 |
Perform a multiply-add of two numerals and against a fixed
multiplicand
(no carry). (Contributed by AV, 16-Sep-2021.)
|
;![A A](_ca.gif) ![( (](lp.gif) ![P P](_cp.gif) ![( (](lp.gif) ![( (](lp.gif) ![P P](_cp.gif) ![N N](_cn.gif)
![( (](lp.gif) ![(
(](lp.gif) ![P P](_cp.gif)
![N N](_cn.gif) ;![E E](_ce.gif) ![F F](_cf.gif) |
|
Theorem | decrmac 9263 |
Perform a multiply-add of two numerals and against a fixed
multiplicand
(with carry). (Contributed by AV, 16-Sep-2021.)
|
;![A A](_ca.gif) ![( (](lp.gif) ![( (](lp.gif) ![P P](_cp.gif)
![G G](_cg.gif)
![( (](lp.gif) ![( (](lp.gif) ![P P](_cp.gif) ![N N](_cn.gif)
;![G G](_cg.gif) ![( (](lp.gif) ![( (](lp.gif) ![P P](_cp.gif)
![N N](_cn.gif)
;![E E](_ce.gif) ![F F](_cf.gif) |
|
Theorem | decaddm10 9264 |
The sum of two multiples of 10 is a multiple of 10. (Contributed by AV,
30-Jul-2021.)
|
;![A A](_ca.gif) ;![B B](_cb.gif) ![0 0](0.gif) ;![( (](lp.gif)
![B B](_cb.gif) ![) )](rp.gif) ![0
0](0.gif) |
|
Theorem | decaddi 9265 |
Add two numerals and
(no carry).
(Contributed by Mario
Carneiro, 18-Feb-2014.)
|
;![A A](_ca.gif) ![( (](lp.gif) ![N N](_cn.gif)
![( (](lp.gif)
![N N](_cn.gif) ;![A A](_ca.gif) ![C C](_cc.gif) |
|
Theorem | decaddci 9266 |
Add two numerals and
(no carry).
(Contributed by Mario
Carneiro, 18-Feb-2014.)
|
;![A A](_ca.gif) ![( (](lp.gif) ![1 1](1.gif)
![( (](lp.gif) ![N N](_cn.gif)
;![1 1](1.gif) ![( (](lp.gif) ![N N](_cn.gif)
;![D D](_cd.gif) ![C C](_cc.gif) |
|
Theorem | decaddci2 9267 |
Add two numerals and
(no carry).
(Contributed by Mario
Carneiro, 18-Feb-2014.) (Revised by AV, 6-Sep-2021.)
|
;![A A](_ca.gif) ![( (](lp.gif) ![1 1](1.gif)
![( (](lp.gif)
![N N](_cn.gif) ;![1 1](1.gif) ![( (](lp.gif) ![N N](_cn.gif)
;![D D](_cd.gif) ![0 0](0.gif) |
|
Theorem | decsubi 9268 |
Difference between a numeral and a nonnegative integer (no
underflow). (Contributed by AV, 22-Jul-2021.) (Revised by AV,
6-Sep-2021.)
|
;![A A](_ca.gif) ![( (](lp.gif) ![1 1](1.gif)
![( (](lp.gif) ![N N](_cn.gif) ![( (](lp.gif) ![N N](_cn.gif)
;![A A](_ca.gif) ![C C](_cc.gif) |
|
Theorem | decmul1 9269 |
The product of a numeral with a number (no carry). (Contributed by
AV, 22-Jul-2021.) (Revised by AV, 6-Sep-2021.)
|
;![A A](_ca.gif) ![( (](lp.gif) ![P P](_cp.gif) ![( (](lp.gif) ![P P](_cp.gif)
![( (](lp.gif) ![P P](_cp.gif) ;![C C](_cc.gif) ![D D](_cd.gif) |
|
Theorem | decmul1c 9270 |
The product of a numeral with a number (with carry). (Contributed by
Mario Carneiro, 18-Feb-2014.) (Revised by AV, 6-Sep-2021.)
|
;![A A](_ca.gif) ![( (](lp.gif) ![( (](lp.gif) ![P P](_cp.gif)
![E E](_ce.gif)
![( (](lp.gif) ![P P](_cp.gif)
;![E E](_ce.gif) ![( (](lp.gif) ![P P](_cp.gif)
;![C C](_cc.gif) ![D D](_cd.gif) |
|
Theorem | decmul2c 9271 |
The product of a numeral with a number (with carry). (Contributed by
Mario Carneiro, 18-Feb-2014.) (Revised by AV, 6-Sep-2021.)
|
;![A A](_ca.gif) ![( (](lp.gif) ![( (](lp.gif) ![A A](_ca.gif)
![E E](_ce.gif)
![( (](lp.gif) ![B B](_cb.gif)
;![E E](_ce.gif) ![( (](lp.gif) ![N N](_cn.gif)
;![C C](_cc.gif) ![D D](_cd.gif) |
|
Theorem | decmulnc 9272 |
The product of a numeral with a number (no carry). (Contributed by AV,
15-Jun-2021.)
|
![( (](lp.gif) ;![A A](_ca.gif) ![B B](_cb.gif) ;![( (](lp.gif) ![A A](_ca.gif) ![) )](rp.gif) ![( (](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) |
|
Theorem | 11multnc 9273 |
The product of 11 (as numeral) with a number (no carry). (Contributed
by AV, 15-Jun-2021.)
|
![( (](lp.gif) ;![1 1](1.gif) ![1 1](1.gif) ;![N N](_cn.gif) ![N N](_cn.gif) |
|
Theorem | decmul10add 9274 |
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.)
|
![( (](lp.gif) ![A A](_ca.gif) ![( (](lp.gif) ![B B](_cb.gif) ![( (](lp.gif) ;![A A](_ca.gif) ![B B](_cb.gif) ;![E E](_ce.gif) ![F F](_cf.gif) ![) )](rp.gif) |
|
Theorem | 6p5lem 9275 |
Lemma for 6p5e11 9278 and related theorems. (Contributed by Mario
Carneiro, 19-Apr-2015.)
|
![( (](lp.gif) ![1 1](1.gif) ![( (](lp.gif) ![1 1](1.gif) ![( (](lp.gif) ![D D](_cd.gif)
;![1 1](1.gif) ![( (](lp.gif) ![B B](_cb.gif)
;![1 1](1.gif) ![C C](_cc.gif) |
|
Theorem | 5p5e10 9276 |
5 + 5 = 10. (Contributed by NM, 5-Feb-2007.) (Revised by Stanislas Polu,
7-Apr-2020.) (Revised by AV, 6-Sep-2021.)
|
![( (](lp.gif) ![5 5](5.gif) ;![1 1](1.gif) ![0 0](0.gif) |
|
Theorem | 6p4e10 9277 |
6 + 4 = 10. (Contributed by NM, 5-Feb-2007.) (Revised by Stanislas Polu,
7-Apr-2020.) (Revised by AV, 6-Sep-2021.)
|
![( (](lp.gif) ![4 4](4.gif) ;![1 1](1.gif) ![0 0](0.gif) |
|
Theorem | 6p5e11 9278 |
6 + 5 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by
AV, 6-Sep-2021.)
|
![( (](lp.gif) ![5 5](5.gif) ;![1 1](1.gif) ![1 1](1.gif) |
|
Theorem | 6p6e12 9279 |
6 + 6 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
![( (](lp.gif) ![6 6](6.gif) ;![1 1](1.gif) ![2 2](2.gif) |
|
Theorem | 7p3e10 9280 |
7 + 3 = 10. (Contributed by NM, 5-Feb-2007.) (Revised by Stanislas Polu,
7-Apr-2020.) (Revised by AV, 6-Sep-2021.)
|
![( (](lp.gif) ![3 3](3.gif) ;![1 1](1.gif) ![0 0](0.gif) |
|
Theorem | 7p4e11 9281 |
7 + 4 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by
AV, 6-Sep-2021.)
|
![( (](lp.gif) ![4 4](4.gif) ;![1 1](1.gif) ![1 1](1.gif) |
|
Theorem | 7p5e12 9282 |
7 + 5 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
![( (](lp.gif) ![5 5](5.gif) ;![1 1](1.gif) ![2 2](2.gif) |
|
Theorem | 7p6e13 9283 |
7 + 6 = 13. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
![( (](lp.gif) ![6 6](6.gif) ;![1 1](1.gif) ![3 3](3.gif) |
|
Theorem | 7p7e14 9284 |
7 + 7 = 14. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
![( (](lp.gif) ![7 7](7.gif) ;![1 1](1.gif) ![4 4](4.gif) |
|
Theorem | 8p2e10 9285 |
8 + 2 = 10. (Contributed by NM, 5-Feb-2007.) (Revised by Stanislas Polu,
7-Apr-2020.) (Revised by AV, 6-Sep-2021.)
|
![( (](lp.gif) ![2 2](2.gif) ;![1 1](1.gif) ![0 0](0.gif) |
|
Theorem | 8p3e11 9286 |
8 + 3 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by
AV, 6-Sep-2021.)
|
![( (](lp.gif) ![3 3](3.gif) ;![1 1](1.gif) ![1 1](1.gif) |
|
Theorem | 8p4e12 9287 |
8 + 4 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
![( (](lp.gif) ![4 4](4.gif) ;![1 1](1.gif) ![2 2](2.gif) |
|
Theorem | 8p5e13 9288 |
8 + 5 = 13. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
![( (](lp.gif) ![5 5](5.gif) ;![1 1](1.gif) ![3 3](3.gif) |
|
Theorem | 8p6e14 9289 |
8 + 6 = 14. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
![( (](lp.gif) ![6 6](6.gif) ;![1 1](1.gif) ![4 4](4.gif) |
|
Theorem | 8p7e15 9290 |
8 + 7 = 15. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
![( (](lp.gif) ![7 7](7.gif) ;![1 1](1.gif) ![5 5](5.gif) |
|
Theorem | 8p8e16 9291 |
8 + 8 = 16. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
![( (](lp.gif) ![8 8](8.gif) ;![1 1](1.gif) ![6 6](6.gif) |
|
Theorem | 9p2e11 9292 |
9 + 2 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by
AV, 6-Sep-2021.)
|
![( (](lp.gif) ![2 2](2.gif) ;![1 1](1.gif) ![1 1](1.gif) |
|
Theorem | 9p3e12 9293 |
9 + 3 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
![( (](lp.gif) ![3 3](3.gif) ;![1 1](1.gif) ![2 2](2.gif) |
|
Theorem | 9p4e13 9294 |
9 + 4 = 13. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
![( (](lp.gif) ![4 4](4.gif) ;![1 1](1.gif) ![3 3](3.gif) |
|
Theorem | 9p5e14 9295 |
9 + 5 = 14. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
![( (](lp.gif) ![5 5](5.gif) ;![1 1](1.gif) ![4 4](4.gif) |
|
Theorem | 9p6e15 9296 |
9 + 6 = 15. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
![( (](lp.gif) ![6 6](6.gif) ;![1 1](1.gif) ![5 5](5.gif) |
|
Theorem | 9p7e16 9297 |
9 + 7 = 16. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
![( (](lp.gif) ![7 7](7.gif) ;![1 1](1.gif) ![6 6](6.gif) |
|
Theorem | 9p8e17 9298 |
9 + 8 = 17. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
![( (](lp.gif) ![8 8](8.gif) ;![1 1](1.gif) ![7 7](7.gif) |
|
Theorem | 9p9e18 9299 |
9 + 9 = 18. (Contributed by Mario Carneiro, 19-Apr-2015.)
|
![( (](lp.gif) ![9 9](9.gif) ;![1 1](1.gif) ![8 8](8.gif) |
|
Theorem | 10p10e20 9300 |
10 + 10 = 20. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by
AV, 6-Sep-2021.)
|
;![1 1](1.gif) ;![1 1](1.gif) ![0 0](0.gif) ;![2 2](2.gif) ![0
0](0.gif) |