P. 95 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 9401-9500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	nn0ind-raph 9401*	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 -> ( ph <-> ps ) )   &    |- ( x = y -> ( ph <-> ch ) )   &    |- ( x = ( y + 1 ) -> ( ph <-> th ) )   &    |- ( x = A -> ( ph <-> ta ) )   &    |- ps   &    |- ( y e. NN0 -> ( ch -> th ) )   =>    |- ( A e. NN0 -> ta )
Theorem	zindd 9402*	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 -> ( ph <-> ps ) )   &    |- ( x = y -> ( ph <-> ch ) )   &    |- ( x = ( y + 1 ) -> ( ph <-> ta ) )   &    |- ( x = -u y -> ( ph <-> th ) )   &    |- ( x = A -> ( ph <-> et ) )   &    |- ( ze -> ps )   &    |- ( ze -> ( y e. NN0 -> ( ch -> ta ) ) )   &    |- ( ze -> ( y e. NN -> ( ch -> th ) ) )   =>    |- ( ze -> ( A e. ZZ -> et ) )
Theorem	btwnz 9403*	Any real number can be sandwiched between two integers. Exercise 2 of [Apostol] p. 28. (Contributed by NM, 10-Nov-2004.)
|- ( A e. RR -> ( E. x e. ZZ x < A /\ E. y e. ZZ A < y ) )
Theorem	nn0zd 9404	A positive integer is an integer. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. NN0 )   =>    |- ( ph -> A e. ZZ )
Theorem	nnzd 9405	A nonnegative integer is an integer. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. NN )   =>    |- ( ph -> A e. ZZ )
Theorem	zred 9406	An integer is a real number. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. ZZ )   =>    |- ( ph -> A e. RR )
Theorem	zcnd 9407	An integer is a complex number. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. ZZ )   =>    |- ( ph -> A e. CC )
Theorem	znegcld 9408	Closure law for negative integers. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. ZZ )   =>    |- ( ph -> -u A e. ZZ )
Theorem	peano2zd 9409	Deduction from second Peano postulate generalized to integers. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. ZZ )   =>    |- ( ph -> ( A + 1 ) e. ZZ )
Theorem	zaddcld 9410	Closure of addition of integers. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. ZZ )   &    |- ( ph -> B e. ZZ )   =>    |- ( ph -> ( A + B ) e. ZZ )
Theorem	zsubcld 9411	Closure of subtraction of integers. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. ZZ )   &    |- ( ph -> B e. ZZ )   =>    |- ( ph -> ( A - B ) e. ZZ )
Theorem	zmulcld 9412	Closure of multiplication of integers. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. ZZ )   &    |- ( ph -> B e. ZZ )   =>    |- ( ph -> ( A x. B ) e. ZZ )
Theorem	zadd2cl 9413	Increasing an integer by 2 results in an integer. (Contributed by Alexander van der Vekens, 16-Sep-2018.)
|- ( N e. ZZ -> ( N + 2 ) e. ZZ )
Theorem	btwnapz 9414	A number between an integer and its successor is apart from any integer. (Contributed by Jim Kingdon, 6-Jan-2023.)
|- ( ph -> A e. ZZ )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. ZZ )   &    |- ( ph -> A < B )   &    |- ( ph -> B < ( A + 1 ) )   =>    |- ( ph -> B # C )
4.4.10  Decimal arithmetic
Syntax	cdc 9415	Constant used for decimal constructor.
class ; A B
Definition	df-dec 9416	Define the "decimal constructor", which is used to build up "decimal integers" or "numeric terms" in base 1 0. For example, (;;; 1 0 0 0 + ;;; 2 0 0 0 ) = ;;; 3 0 0 0 1kp2ke3k 14954. (Contributed by Mario Carneiro, 17-Apr-2015.) (Revised by AV, 1-Aug-2021.)
|- ; A B = ( ( ( 9 + 1 ) x. A ) + B )
Theorem	9p1e10 9417	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 ) = ; 1 0
Theorem	dfdec10 9418	Version of the definition of the "decimal constructor" using ; 1 0 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 B = ( (; 1 0 x. A ) + B )
Theorem	deceq1 9419	Equality theorem for the decimal constructor. (Contributed by Mario Carneiro, 17-Apr-2015.) (Revised by AV, 6-Sep-2021.)
|- ( A = B -> ; A C = ; B C )
Theorem	deceq2 9420	Equality theorem for the decimal constructor. (Contributed by Mario Carneiro, 17-Apr-2015.) (Revised by AV, 6-Sep-2021.)
|- ( A = B -> ; C A = ; C B )
Theorem	deceq1i 9421	Equality theorem for the decimal constructor. (Contributed by Mario Carneiro, 17-Apr-2015.)
|- A = B   =>    |- ; A C = ; B C
Theorem	deceq2i 9422	Equality theorem for the decimal constructor. (Contributed by Mario Carneiro, 17-Apr-2015.)
|- A = B   =>    |- ; C A = ; C B
Theorem	deceq12i 9423	Equality theorem for the decimal constructor. (Contributed by Mario Carneiro, 17-Apr-2015.)
|- A = B   &    |- C = D   =>    |- ; A C = ; B D
Theorem	numnncl 9424	Closure for a numeral (with units place). (Contributed by Mario Carneiro, 18-Feb-2014.)
|- T e. NN0   &    |- A e. NN0   &    |- B e. NN   =>    |- ( ( T x. A ) + B ) e. NN
Theorem	num0u 9425	Add a zero in the units place. (Contributed by Mario Carneiro, 18-Feb-2014.)
|- T e. NN0   &    |- A e. NN0   =>    |- ( T x. A ) = ( ( T x. A ) + 0 )
Theorem	num0h 9426	Add a zero in the higher places. (Contributed by Mario Carneiro, 18-Feb-2014.)
|- T e. NN0   &    |- A e. NN0   =>    |- A = ( ( T x. 0 ) + A )
Theorem	numcl 9427	Closure for a decimal integer (with units place). (Contributed by Mario Carneiro, 18-Feb-2014.)
|- T e. NN0   &    |- A e. NN0   &    |- B e. NN0   =>    |- ( ( T x. A ) + B ) e. NN0
Theorem	numsuc 9428	The successor of a decimal integer (no carry). (Contributed by Mario Carneiro, 18-Feb-2014.)
|- T e. NN0   &    |- A e. NN0   &    |- B e. NN0   &    |- ( B + 1 ) = C   &    |- N = ( ( T x. A ) + B )   =>    |- ( N + 1 ) = ( ( T x. A ) + C )
Theorem	deccl 9429	Closure for a numeral. (Contributed by Mario Carneiro, 17-Apr-2015.) (Revised by AV, 6-Sep-2021.)
|- A e. NN0   &    |- B e. NN0   =>    |- ; A B e. NN0
Theorem	10nn 9430	10 is a positive integer. (Contributed by NM, 8-Nov-2012.) (Revised by AV, 6-Sep-2021.)
|- ; 1 0 e. NN
Theorem	10pos 9431	The number 10 is positive. (Contributed by NM, 5-Feb-2007.) (Revised by AV, 8-Sep-2021.)
|- 0 < ; 1 0
Theorem	10nn0 9432	10 is a nonnegative integer. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.)
|- ; 1 0 e. NN0
Theorem	10re 9433	The number 10 is real. (Contributed by NM, 5-Feb-2007.) (Revised by AV, 8-Sep-2021.)
|- ; 1 0 e. RR
Theorem	decnncl 9434	Closure for a numeral. (Contributed by Mario Carneiro, 17-Apr-2015.) (Revised by AV, 6-Sep-2021.)
|- A e. NN0   &    |- B e. NN   =>    |- ; A B e. NN
Theorem	dec0u 9435	Add a zero in the units place. (Contributed by Mario Carneiro, 17-Apr-2015.) (Revised by AV, 6-Sep-2021.)
|- A e. NN0   =>    |- (; 1 0 x. A ) = ; A 0
Theorem	dec0h 9436	Add a zero in the higher places. (Contributed by Mario Carneiro, 17-Apr-2015.) (Revised by AV, 6-Sep-2021.)
|- A e. NN0   =>    |- A = ; 0 A
Theorem	numnncl2 9437	Closure for a decimal integer (zero units place). (Contributed by Mario Carneiro, 9-Mar-2015.)
|- T e. NN   &    |- A e. NN   =>    |- ( ( T x. A ) + 0 ) e. NN
Theorem	decnncl2 9438	Closure for a decimal integer (zero units place). (Contributed by Mario Carneiro, 17-Apr-2015.) (Revised by AV, 6-Sep-2021.)
|- A e. NN   =>    |- ; A 0 e. NN
Theorem	numlt 9439	Comparing two decimal integers (equal higher places). (Contributed by Mario Carneiro, 18-Feb-2014.)
|- T e. NN   &    |- A e. NN0   &    |- B e. NN0   &    |- C e. NN   &    |- B < C   =>    |- ( ( T x. A ) + B ) < ( ( T x. A ) + C )
Theorem	numltc 9440	Comparing two decimal integers (unequal higher places). (Contributed by Mario Carneiro, 18-Feb-2014.)
|- T e. NN   &    |- A e. NN0   &    |- B e. NN0   &    |- C e. NN0   &    |- D e. NN0   &    |- C < T   &    |- A < B   =>    |- ( ( T x. A ) + C ) < ( ( T x. B ) + D )
Theorem	le9lt10 9441	A "decimal digit" (i.e. a nonnegative integer less than or equal to 9) is less then 10. (Contributed by AV, 8-Sep-2021.)
|- A e. NN0   &    |- A <_ 9   =>    |- A < ; 1 0
Theorem	declt 9442	Comparing two decimal integers (equal higher places). (Contributed by Mario Carneiro, 17-Apr-2015.) (Revised by AV, 6-Sep-2021.)
|- A e. NN0   &    |- B e. NN0   &    |- C e. NN   &    |- B < C   =>    |- ; A B < ; A C
Theorem	decltc 9443	Comparing two decimal integers (unequal higher places). (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by AV, 6-Sep-2021.)
|- A e. NN0   &    |- B e. NN0   &    |- C e. NN0   &    |- D e. NN0   &    |- C < ; 1 0   &    |- A < B   =>    |- ; A C < ; B D
Theorem	declth 9444	Comparing two decimal integers (unequal higher places). (Contributed by AV, 8-Sep-2021.)
|- A e. NN0   &    |- B e. NN0   &    |- C e. NN0   &    |- D e. NN0   &    |- C <_ 9   &    |- A < B   =>    |- ; A C < ; B D
Theorem	decsuc 9445	The successor of a decimal integer (no carry). (Contributed by Mario Carneiro, 17-Apr-2015.) (Revised by AV, 6-Sep-2021.)
|- A e. NN0   &    |- B e. NN0   &    |- ( B + 1 ) = C   &    |- N = ; A B   =>    |- ( N + 1 ) = ; A C
Theorem	3declth 9446	Comparing two decimal integers with three "digits" (unequal higher places). (Contributed by AV, 8-Sep-2021.)
|- A e. NN0   &    |- B e. NN0   &    |- C e. NN0   &    |- D e. NN0   &    |- E e. NN0   &    |- F e. NN0   &    |- A < B   &    |- C <_ 9   &    |- E <_ 9   =>    |- ;; A C E < ;; B D F
Theorem	3decltc 9447	Comparing two decimal integers with three "digits" (unequal higher places). (Contributed by AV, 15-Jun-2021.) (Revised by AV, 6-Sep-2021.)
|- A e. NN0   &    |- B e. NN0   &    |- C e. NN0   &    |- D e. NN0   &    |- E e. NN0   &    |- F e. NN0   &    |- A < B   &    |- C < ; 1 0   &    |- E < ; 1 0   =>    |- ;; A C E < ;; B D F
Theorem	decle 9448	Comparing two decimal integers (equal higher places). (Contributed by AV, 17-Aug-2021.) (Revised by AV, 8-Sep-2021.)
|- A e. NN0   &    |- B e. NN0   &    |- C e. NN0   &    |- B <_ C   =>    |- ; A B <_ ; A C
Theorem	decleh 9449	Comparing two decimal integers (unequal higher places). (Contributed by AV, 17-Aug-2021.) (Revised by AV, 8-Sep-2021.)
|- A e. NN0   &    |- B e. NN0   &    |- C e. NN0   &    |- D e. NN0   &    |- C <_ 9   &    |- A < B   =>    |- ; A C <_ ; B D
Theorem	declei 9450	Comparing a digit to a decimal integer. (Contributed by AV, 17-Aug-2021.)
|- A e. NN   &    |- B e. NN0   &    |- C e. NN0   &    |- C <_ 9   =>    |- C <_ ; A B
Theorem	numlti 9451	Comparing a digit to a decimal integer. (Contributed by Mario Carneiro, 18-Feb-2014.)
|- T e. NN   &    |- A e. NN   &    |- B e. NN0   &    |- C e. NN0   &    |- C < T   =>    |- C < ( ( T x. A ) + B )
Theorem	declti 9452	Comparing a digit to a decimal integer. (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by AV, 6-Sep-2021.)
|- A e. NN   &    |- B e. NN0   &    |- C e. NN0   &    |- C < ; 1 0   =>    |- C < ; A B
Theorem	decltdi 9453	Comparing a digit to a decimal integer. (Contributed by AV, 8-Sep-2021.)
|- A e. NN   &    |- B e. NN0   &    |- C e. NN0   &    |- C <_ 9   =>    |- C < ; A B
Theorem	numsucc 9454	The successor of a decimal integer (with carry). (Contributed by Mario Carneiro, 18-Feb-2014.)
|- Y e. NN0   &    |- T = ( Y + 1 )   &    |- A e. NN0   &    |- ( A + 1 ) = B   &    |- N = ( ( T x. A ) + Y )   =>    |- ( N + 1 ) = ( ( T x. B ) + 0 )
Theorem	decsucc 9455	The successor of a decimal integer (with carry). (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by AV, 6-Sep-2021.)
|- A e. NN0   &    |- ( A + 1 ) = B   &    |- N = ; A 9   =>    |- ( N + 1 ) = ; B 0
Theorem	1e0p1 9456	The successor of zero. (Contributed by Mario Carneiro, 18-Feb-2014.)
|- 1 = ( 0 + 1 )
Theorem	dec10p 9457	Ten plus an integer. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.)
|- (; 1 0 + A ) = ; 1 A
Theorem	numma 9458	Perform a multiply-add of two decimal integers M and N against a fixed multiplicand P (no carry). (Contributed by Mario Carneiro, 18-Feb-2014.)
|- T e. NN0   &    |- A e. NN0   &    |- B e. NN0   &    |- C e. NN0   &    |- D e. NN0   &    |- M = ( ( T x. A ) + B )   &    |- N = ( ( T x. C ) + D )   &    |- P e. NN0   &    |- ( ( A x. P ) + C ) = E   &    |- ( ( B x. P ) + D ) = F   =>    |- ( ( M x. P ) + N ) = ( ( T x. E ) + F )
Theorem	nummac 9459	Perform a multiply-add of two decimal integers M and N against a fixed multiplicand P (with carry). (Contributed by Mario Carneiro, 18-Feb-2014.)
|- T e. NN0   &    |- A e. NN0   &    |- B e. NN0   &    |- C e. NN0   &    |- D e. NN0   &    |- M = ( ( T x. A ) + B )   &    |- N = ( ( T x. C ) + D )   &    |- P e. NN0   &    |- F e. NN0   &    |- G e. NN0   &    |- ( ( A x. P ) + ( C + G ) ) = E   &    |- ( ( B x. P ) + D ) = ( ( T x. G ) + F )   =>    |- ( ( M x. P ) + N ) = ( ( T x. E ) + F )
Theorem	numma2c 9460	Perform a multiply-add of two decimal integers M and N against a fixed multiplicand P (with carry). (Contributed by Mario Carneiro, 18-Feb-2014.)
|- T e. NN0   &    |- A e. NN0   &    |- B e. NN0   &    |- C e. NN0   &    |- D e. NN0   &    |- M = ( ( T x. A ) + B )   &    |- N = ( ( T x. C ) + D )   &    |- P e. NN0   &    |- F e. NN0   &    |- G e. NN0   &    |- ( ( P x. A ) + ( C + G ) ) = E   &    |- ( ( P x. B ) + D ) = ( ( T x. G ) + F )   =>    |- ( ( P x. M ) + N ) = ( ( T x. E ) + F )
Theorem	numadd 9461	Add two decimal integers M and N (no carry). (Contributed by Mario Carneiro, 18-Feb-2014.)
|- T e. NN0   &    |- A e. NN0   &    |- B e. NN0   &    |- C e. NN0   &    |- D e. NN0   &    |- M = ( ( T x. A ) + B )   &    |- N = ( ( T x. C ) + D )   &    |- ( A + C ) = E   &    |- ( B + D ) = F   =>    |- ( M + N ) = ( ( T x. E ) + F )
Theorem	numaddc 9462	Add two decimal integers M and N (with carry). (Contributed by Mario Carneiro, 18-Feb-2014.)
|- T e. NN0   &    |- A e. NN0   &    |- B e. NN0   &    |- C e. NN0   &    |- D e. NN0   &    |- M = ( ( T x. A ) + B )   &    |- N = ( ( T x. C ) + D )   &    |- F e. NN0   &    |- ( ( A + C ) + 1 ) = E   &    |- ( B + D ) = ( ( T x. 1 ) + F )   =>    |- ( M + N ) = ( ( T x. E ) + F )
Theorem	nummul1c 9463	The product of a decimal integer with a number. (Contributed by Mario Carneiro, 18-Feb-2014.)
|- T e. NN0   &    |- P e. NN0   &    |- A e. NN0   &    |- B e. NN0   &    |- N = ( ( T x. A ) + B )   &    |- D e. NN0   &    |- E e. NN0   &    |- ( ( A x. P ) + E ) = C   &    |- ( B x. P ) = ( ( T x. E ) + D )   =>    |- ( N x. P ) = ( ( T x. C ) + D )
Theorem	nummul2c 9464	The product of a decimal integer with a number (with carry). (Contributed by Mario Carneiro, 18-Feb-2014.)
|- T e. NN0   &    |- P e. NN0   &    |- A e. NN0   &    |- B e. NN0   &    |- N = ( ( T x. A ) + B )   &    |- D e. NN0   &    |- E e. NN0   &    |- ( ( P x. A ) + E ) = C   &    |- ( P x. B ) = ( ( T x. E ) + D )   =>    |- ( P x. N ) = ( ( T x. C ) + D )
Theorem	decma 9465	Perform a multiply-add of two numerals M and N against a fixed multiplicand P (no carry). (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by AV, 6-Sep-2021.)
|- A e. NN0   &    |- B e. NN0   &    |- C e. NN0   &    |- D e. NN0   &    |- M = ; A B   &    |- N = ; C D   &    |- P e. NN0   &    |- ( ( A x. P ) + C ) = E   &    |- ( ( B x. P ) + D ) = F   =>    |- ( ( M x. P ) + N ) = ; E F
Theorem	decmac 9466	Perform a multiply-add of two numerals M and N against a fixed multiplicand P (with carry). (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by AV, 6-Sep-2021.)
|- A e. NN0   &    |- B e. NN0   &    |- C e. NN0   &    |- D e. NN0   &    |- M = ; A B   &    |- N = ; C D   &    |- P e. NN0   &    |- F e. NN0   &    |- G e. NN0   &    |- ( ( A x. P ) + ( C + G ) ) = E   &    |- ( ( B x. P ) + D ) = ; G F   =>    |- ( ( M x. P ) + N ) = ; E F
Theorem	decma2c 9467	Perform a multiply-add of two numerals M and N against a fixed multiplier P (with carry). (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by AV, 6-Sep-2021.)
|- A e. NN0   &    |- B e. NN0   &    |- C e. NN0   &    |- D e. NN0   &    |- M = ; A B   &    |- N = ; C D   &    |- P e. NN0   &    |- F e. NN0   &    |- G e. NN0   &    |- ( ( P x. A ) + ( C + G ) ) = E   &    |- ( ( P x. B ) + D ) = ; G F   =>    |- ( ( P x. M ) + N ) = ; E F
Theorem	decadd 9468	Add two numerals M and N (no carry). (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by AV, 6-Sep-2021.)
|- A e. NN0   &    |- B e. NN0   &    |- C e. NN0   &    |- D e. NN0   &    |- M = ; A B   &    |- N = ; C D   &    |- ( A + C ) = E   &    |- ( B + D ) = F   =>    |- ( M + N ) = ; E F
Theorem	decaddc 9469	Add two numerals M and N (with carry). (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by AV, 6-Sep-2021.)
|- A e. NN0   &    |- B e. NN0   &    |- C e. NN0   &    |- D e. NN0   &    |- M = ; A B   &    |- N = ; C D   &    |- ( ( A + C ) + 1 ) = E   &    |- F e. NN0   &    |- ( B + D ) = ; 1 F   =>    |- ( M + N ) = ; E F
Theorem	decaddc2 9470	Add two numerals M and N (with carry). (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by AV, 6-Sep-2021.)
|- A e. NN0   &    |- B e. NN0   &    |- C e. NN0   &    |- D e. NN0   &    |- M = ; A B   &    |- N = ; C D   &    |- ( ( A + C ) + 1 ) = E   &    |- ( B + D ) = ; 1 0   =>    |- ( M + N ) = ; E 0
Theorem	decrmanc 9471	Perform a multiply-add of two numerals M and N against a fixed multiplicand P (no carry). (Contributed by AV, 16-Sep-2021.)
|- A e. NN0   &    |- B e. NN0   &    |- N e. NN0   &    |- M = ; A B   &    |- P e. NN0   &    |- ( A x. P ) = E   &    |- ( ( B x. P ) + N ) = F   =>    |- ( ( M x. P ) + N ) = ; E F
Theorem	decrmac 9472	Perform a multiply-add of two numerals M and N against a fixed multiplicand P (with carry). (Contributed by AV, 16-Sep-2021.)
|- A e. NN0   &    |- B e. NN0   &    |- N e. NN0   &    |- M = ; A B   &    |- P e. NN0   &    |- F e. NN0   &    |- G e. NN0   &    |- ( ( A x. P ) + G ) = E   &    |- ( ( B x. P ) + N ) = ; G F   =>    |- ( ( M x. P ) + N ) = ; E F
Theorem	decaddm10 9473	The sum of two multiples of 10 is a multiple of 10. (Contributed by AV, 30-Jul-2021.)
|- A e. NN0   &    |- B e. NN0   =>    |- (; A 0 + ; B 0 ) = ; ( A + B ) 0
Theorem	decaddi 9474	Add two numerals M and N (no carry). (Contributed by Mario Carneiro, 18-Feb-2014.)
|- A e. NN0   &    |- B e. NN0   &    |- N e. NN0   &    |- M = ; A B   &    |- ( B + N ) = C   =>    |- ( M + N ) = ; A C
Theorem	decaddci 9475	Add two numerals M and N (no carry). (Contributed by Mario Carneiro, 18-Feb-2014.)
|- A e. NN0   &    |- B e. NN0   &    |- N e. NN0   &    |- M = ; A B   &    |- ( A + 1 ) = D   &    |- C e. NN0   &    |- ( B + N ) = ; 1 C   =>    |- ( M + N ) = ; D C
Theorem	decaddci2 9476	Add two numerals M and N (no carry). (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by AV, 6-Sep-2021.)
|- A e. NN0   &    |- B e. NN0   &    |- N e. NN0   &    |- M = ; A B   &    |- ( A + 1 ) = D   &    |- ( B + N ) = ; 1 0   =>    |- ( M + N ) = ; D 0
Theorem	decsubi 9477	Difference between a numeral M and a nonnegative integer N (no underflow). (Contributed by AV, 22-Jul-2021.) (Revised by AV, 6-Sep-2021.)
|- A e. NN0   &    |- B e. NN0   &    |- N e. NN0   &    |- M = ; A B   &    |- ( A + 1 ) = D   &    |- ( B - N ) = C   =>    |- ( M - N ) = ; A C
Theorem	decmul1 9478	The product of a numeral with a number (no carry). (Contributed by AV, 22-Jul-2021.) (Revised by AV, 6-Sep-2021.)
|- P e. NN0   &    |- A e. NN0   &    |- B e. NN0   &    |- N = ; A B   &    |- D e. NN0   &    |- ( A x. P ) = C   &    |- ( B x. P ) = D   =>    |- ( N x. P ) = ; C D
Theorem	decmul1c 9479	The product of a numeral with a number (with carry). (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by AV, 6-Sep-2021.)
|- P e. NN0   &    |- A e. NN0   &    |- B e. NN0   &    |- N = ; A B   &    |- D e. NN0   &    |- E e. NN0   &    |- ( ( A x. P ) + E ) = C   &    |- ( B x. P ) = ; E D   =>    |- ( N x. P ) = ; C D
Theorem	decmul2c 9480	The product of a numeral with a number (with carry). (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by AV, 6-Sep-2021.)
|- P e. NN0   &    |- A e. NN0   &    |- B e. NN0   &    |- N = ; A B   &    |- D e. NN0   &    |- E e. NN0   &    |- ( ( P x. A ) + E ) = C   &    |- ( P x. B ) = ; E D   =>    |- ( P x. N ) = ; C D
Theorem	decmulnc 9481	The product of a numeral with a number (no carry). (Contributed by AV, 15-Jun-2021.)
|- N e. NN0   &    |- A e. NN0   &    |- B e. NN0   =>    |- ( N x. ; A B ) = ; ( N x. A ) ( N x. B )
Theorem	11multnc 9482	The product of 11 (as numeral) with a number (no carry). (Contributed by AV, 15-Jun-2021.)
|- N e. NN0   =>    |- ( N x. ; 1 1 ) = ; N N
Theorem	decmul10add 9483	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.)
|- A e. NN0   &    |- B e. NN0   &    |- M e. NN0   &    |- E = ( M x. A )   &    |- F = ( M x. B )   =>    |- ( M x. ; A B ) = (; E 0 + F )
Theorem	6p5lem 9484	Lemma for 6p5e11 9487 and related theorems. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- A e. NN0   &    |- D e. NN0   &    |- E e. NN0   &    |- B = ( D + 1 )   &    |- C = ( E + 1 )   &    |- ( A + D ) = ; 1 E   =>    |- ( A + B ) = ; 1 C
Theorem	5p5e10 9485	5 + 5 = 10. (Contributed by NM, 5-Feb-2007.) (Revised by Stanislas Polu, 7-Apr-2020.) (Revised by AV, 6-Sep-2021.)
|- ( 5 + 5 ) = ; 1 0
Theorem	6p4e10 9486	6 + 4 = 10. (Contributed by NM, 5-Feb-2007.) (Revised by Stanislas Polu, 7-Apr-2020.) (Revised by AV, 6-Sep-2021.)
|- ( 6 + 4 ) = ; 1 0
Theorem	6p5e11 9487	6 + 5 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.)
|- ( 6 + 5 ) = ; 1 1
Theorem	6p6e12 9488	6 + 6 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- ( 6 + 6 ) = ; 1 2
Theorem	7p3e10 9489	7 + 3 = 10. (Contributed by NM, 5-Feb-2007.) (Revised by Stanislas Polu, 7-Apr-2020.) (Revised by AV, 6-Sep-2021.)
|- ( 7 + 3 ) = ; 1 0
Theorem	7p4e11 9490	7 + 4 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.)
|- ( 7 + 4 ) = ; 1 1
Theorem	7p5e12 9491	7 + 5 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- ( 7 + 5 ) = ; 1 2
Theorem	7p6e13 9492	7 + 6 = 13. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- ( 7 + 6 ) = ; 1 3
Theorem	7p7e14 9493	7 + 7 = 14. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- ( 7 + 7 ) = ; 1 4
Theorem	8p2e10 9494	8 + 2 = 10. (Contributed by NM, 5-Feb-2007.) (Revised by Stanislas Polu, 7-Apr-2020.) (Revised by AV, 6-Sep-2021.)
|- ( 8 + 2 ) = ; 1 0
Theorem	8p3e11 9495	8 + 3 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.)
|- ( 8 + 3 ) = ; 1 1
Theorem	8p4e12 9496	8 + 4 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- ( 8 + 4 ) = ; 1 2
Theorem	8p5e13 9497	8 + 5 = 13. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- ( 8 + 5 ) = ; 1 3
Theorem	8p6e14 9498	8 + 6 = 14. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- ( 8 + 6 ) = ; 1 4
Theorem	8p7e15 9499	8 + 7 = 15. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- ( 8 + 7 ) = ; 1 5
Theorem	8p8e16 9500	8 + 8 = 16. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- ( 8 + 8 ) = ; 1 6