P. 98 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 9701-9800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	zeo 9701	An integer is even or odd. (Contributed by NM, 1-Jan-2006.)
|- ( N e. ZZ -> ( ( N / 2 ) e. ZZ \/ ( ( N + 1 ) / 2 ) e. ZZ ) )
Theorem	zeo2 9702	An integer is even or odd but not both. (Contributed by Mario Carneiro, 12-Sep-2015.)
|- ( N e. ZZ -> ( ( N / 2 ) e. ZZ <-> -. ( ( N + 1 ) / 2 ) e. ZZ ) )
Theorem	peano2uz2 9703*	Second Peano postulate for upper integers. (Contributed by NM, 3-Oct-2004.)
|- ( ( A e. ZZ /\ B e. { x e. ZZ | A <_ x } ) -> ( B + 1 ) e. { x e. ZZ | A <_ x } )
Theorem	peano5uzti 9704*	Peano's inductive postulate for upper integers. (Contributed by NM, 6-Jul-2005.) (Revised by Mario Carneiro, 25-Jul-2013.)
|- ( N e. ZZ -> ( ( N e. A /\ A. x e. A ( x + 1 ) e. A ) -> { k e. ZZ | N <_ k } C_ A ) )
Theorem	peano5uzi 9705*	Peano's inductive postulate for upper integers. (Contributed by NM, 6-Jul-2005.) (Revised by Mario Carneiro, 3-May-2014.)
|- N e. ZZ   =>    |- ( ( N e. A /\ A. x e. A ( x + 1 ) e. A ) -> { k e. ZZ | N <_ k } C_ A )
Theorem	dfuzi 9706*	An expression for the upper integers that start at N that is analogous to dfnn2 9256 for positive integers. (Contributed by NM, 6-Jul-2005.) (Proof shortened by Mario Carneiro, 3-May-2014.)
|- N e. ZZ   =>    |- { z e. ZZ | N <_ z } = |^| { x | ( N e. x /\ A. y e. x ( y + 1 ) e. x ) }
Theorem	uzind 9707*	Induction on the upper integers that start at M. The first four hypotheses give us the substitution instances we need; the last two are the basis and the induction step. (Contributed by NM, 5-Jul-2005.)
|- ( j = M -> ( ph <-> ps ) )   &    |- ( j = k -> ( ph <-> ch ) )   &    |- ( j = ( k + 1 ) -> ( ph <-> th ) )   &    |- ( j = N -> ( ph <-> ta ) )   &    |- ( M e. ZZ -> ps )   &    |- ( ( M e. ZZ /\ k e. ZZ /\ M <_ k ) -> ( ch -> th ) )   =>    |- ( ( M e. ZZ /\ N e. ZZ /\ M <_ N ) -> ta )
Theorem	uzind2 9708*	Induction on the upper integers that start after an integer M. The first four hypotheses give us the substitution instances we need; the last two are the basis and the induction step. (Contributed by NM, 25-Jul-2005.)
|- ( j = ( M + 1 ) -> ( ph <-> ps ) )   &    |- ( j = k -> ( ph <-> ch ) )   &    |- ( j = ( k + 1 ) -> ( ph <-> th ) )   &    |- ( j = N -> ( ph <-> ta ) )   &    |- ( M e. ZZ -> ps )   &    |- ( ( M e. ZZ /\ k e. ZZ /\ M < k ) -> ( ch -> th ) )   =>    |- ( ( M e. ZZ /\ N e. ZZ /\ M < N ) -> ta )
Theorem	uzind3 9709*	Induction on the upper integers that start at an integer M. The first four hypotheses give us the substitution instances we need, and the last two are the basis and the induction step. (Contributed by NM, 26-Jul-2005.)
|- ( j = M -> ( ph <-> ps ) )   &    |- ( j = m -> ( ph <-> ch ) )   &    |- ( j = ( m + 1 ) -> ( ph <-> th ) )   &    |- ( j = N -> ( ph <-> ta ) )   &    |- ( M e. ZZ -> ps )   &    |- ( ( M e. ZZ /\ m e. { k e. ZZ | M <_ k } ) -> ( ch -> th ) )   =>    |- ( ( M e. ZZ /\ N e. { k e. ZZ | M <_ k } ) -> ta )
Theorem	nn0ind 9710*	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. (Contributed by NM, 13-May-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	fzind 9711*	Induction on the integers from M to N inclusive . The first four hypotheses give us the substitution instances we need; the last two are the basis and the induction step. (Contributed by Paul Chapman, 31-Mar-2011.)
|- ( x = M -> ( ph <-> ps ) )   &    |- ( x = y -> ( ph <-> ch ) )   &    |- ( x = ( y + 1 ) -> ( ph <-> th ) )   &    |- ( x = K -> ( ph <-> ta ) )   &    |- ( ( M e. ZZ /\ N e. ZZ /\ M <_ N ) -> ps )   &    |- ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( y e. ZZ /\ M <_ y /\ y < N ) ) -> ( ch -> th ) )   =>    |- ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( K e. ZZ /\ M <_ K /\ K <_ N ) ) -> ta )
Theorem	fnn0ind 9712*	Induction on the integers from 0 to N inclusive . The first four hypotheses give us the substitution instances we need; the last two are the basis and the induction step. (Contributed by Paul Chapman, 31-Mar-2011.)
|- ( x = 0 -> ( ph <-> ps ) )   &    |- ( x = y -> ( ph <-> ch ) )   &    |- ( x = ( y + 1 ) -> ( ph <-> th ) )   &    |- ( x = K -> ( ph <-> ta ) )   &    |- ( N e. NN0 -> ps )   &    |- ( ( N e. NN0 /\ y e. NN0 /\ y < N ) -> ( ch -> th ) )   =>    |- ( ( N e. NN0 /\ K e. NN0 /\ K <_ N ) -> ta )
Theorem	nn0ind-raph 9713*	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 9714*	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 9715*	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 9716	A positive integer is an integer. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. NN0 )   =>    |- ( ph -> A e. ZZ )
Theorem	nnzd 9717	A nonnegative integer is an integer. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. NN )   =>    |- ( ph -> A e. ZZ )
Theorem	zred 9718	An integer is a real number. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. ZZ )   =>    |- ( ph -> A e. RR )
Theorem	zcnd 9719	An integer is a complex number. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. ZZ )   =>    |- ( ph -> A e. CC )
Theorem	znegcld 9720	Closure law for negative integers. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. ZZ )   =>    |- ( ph -> -u A e. ZZ )
Theorem	peano2zd 9721	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 9722	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 9723	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 9724	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 9725	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 9726	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 9727	Constant used for decimal constructor.
class ; A B
Definition	df-dec 9728	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 16618. (Contributed by Mario Carneiro, 17-Apr-2015.) (Revised by AV, 1-Aug-2021.)
|- ; A B = ( ( ( 9 + 1 ) x. A ) + B )
Theorem	9p1e10 9729	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 9730	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 9731	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 9732	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 9733	Equality theorem for the decimal constructor. (Contributed by Mario Carneiro, 17-Apr-2015.)
|- A = B   =>    |- ; A C = ; B C
Theorem	deceq2i 9734	Equality theorem for the decimal constructor. (Contributed by Mario Carneiro, 17-Apr-2015.)
|- A = B   =>    |- ; C A = ; C B
Theorem	deceq12i 9735	Equality theorem for the decimal constructor. (Contributed by Mario Carneiro, 17-Apr-2015.)
|- A = B   &    |- C = D   =>    |- ; A C = ; B D
Theorem	numnncl 9736	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 9737	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 9738	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 9739	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 9740	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 9741	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 9742	10 is a positive integer. (Contributed by NM, 8-Nov-2012.) (Revised by AV, 6-Sep-2021.)
|- ; 1 0 e. NN
Theorem	10pos 9743	The number 10 is positive. (Contributed by NM, 5-Feb-2007.) (Revised by AV, 8-Sep-2021.)
|- 0 < ; 1 0
Theorem	10nn0 9744	10 is a nonnegative integer. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.)
|- ; 1 0 e. NN0
Theorem	10re 9745	The number 10 is real. (Contributed by NM, 5-Feb-2007.) (Revised by AV, 8-Sep-2021.)
|- ; 1 0 e. RR
Theorem	decnncl 9746	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 9747	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 9748	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 9749	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 9750	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 9751	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 9752	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 9753	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 9754	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 9755	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 9756	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 9757	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 9758	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 9759	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 9760	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 9761	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 9762	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 9763	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 9764	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 9765	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 9766	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 9767	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 9768	The successor of zero. (Contributed by Mario Carneiro, 18-Feb-2014.)
|- 1 = ( 0 + 1 )
Theorem	dec10p 9769	Ten plus an integer. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.)
|- (; 1 0 + A ) = ; 1 A
Theorem	numma 9770	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 9771	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 9772	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 9773	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 9774	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 9775	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 9776	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 9777	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 9778	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 9779	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 9780	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 9781	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 9782	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 9783	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 9784	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 9785	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 9786	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 9787	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 9788	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 9789	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 9790	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 9791	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 9792	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 9793	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 9794	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 9795	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 9796	Lemma for 6p5e11 9799 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 9797	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 9798	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 9799	6 + 5 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.)
|- ( 6 + 5 ) = ; 1 1
Theorem	6p6e12 9800	6 + 6 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- ( 6 + 6 ) = ; 1 2