P. 94 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 9301-9400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	dfuzi 9301*	An expression for the upper integers that start at N that is analogous to dfnn2 8859 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 9302*	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 9303*	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 9304*	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 9305*	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 9306*	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 9307*	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 9308*	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 9309*	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 9310*	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 9311	A positive integer is an integer. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. NN0 )   =>    |- ( ph -> A e. ZZ )
Theorem	nnzd 9312	A nonnegative integer is an integer. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. NN )   =>    |- ( ph -> A e. ZZ )
Theorem	zred 9313	An integer is a real number. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. ZZ )   =>    |- ( ph -> A e. RR )
Theorem	zcnd 9314	An integer is a complex number. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. ZZ )   =>    |- ( ph -> A e. CC )
Theorem	znegcld 9315	Closure law for negative integers. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. ZZ )   =>    |- ( ph -> -u A e. ZZ )
Theorem	peano2zd 9316	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 9317	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 9318	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 9319	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 9320	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 9321	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 9322	Constant used for decimal constructor.
class ; A B
Definition	df-dec 9323	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 13615. (Contributed by Mario Carneiro, 17-Apr-2015.) (Revised by AV, 1-Aug-2021.)
|- ; A B = ( ( ( 9 + 1 ) x. A ) + B )
Theorem	9p1e10 9324	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 9325	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 9326	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 9327	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 9328	Equality theorem for the decimal constructor. (Contributed by Mario Carneiro, 17-Apr-2015.)
|- A = B   =>    |- ; A C = ; B C
Theorem	deceq2i 9329	Equality theorem for the decimal constructor. (Contributed by Mario Carneiro, 17-Apr-2015.)
|- A = B   =>    |- ; C A = ; C B
Theorem	deceq12i 9330	Equality theorem for the decimal constructor. (Contributed by Mario Carneiro, 17-Apr-2015.)
|- A = B   &    |- C = D   =>    |- ; A C = ; B D
Theorem	numnncl 9331	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 9332	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 9333	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 9334	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 9335	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 9336	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 9337	10 is a positive integer. (Contributed by NM, 8-Nov-2012.) (Revised by AV, 6-Sep-2021.)
|- ; 1 0 e. NN
Theorem	10pos 9338	The number 10 is positive. (Contributed by NM, 5-Feb-2007.) (Revised by AV, 8-Sep-2021.)
|- 0 < ; 1 0
Theorem	10nn0 9339	10 is a nonnegative integer. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.)
|- ; 1 0 e. NN0
Theorem	10re 9340	The number 10 is real. (Contributed by NM, 5-Feb-2007.) (Revised by AV, 8-Sep-2021.)
|- ; 1 0 e. RR
Theorem	decnncl 9341	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 9342	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 9343	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 9344	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 9345	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 9346	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 9347	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 9348	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 9349	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 9350	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 9351	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 9352	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 9353	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 9354	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 9355	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 9356	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 9357	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 9358	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 9359	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 9360	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 9361	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 9362	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 9363	The successor of zero. (Contributed by Mario Carneiro, 18-Feb-2014.)
|- 1 = ( 0 + 1 )
Theorem	dec10p 9364	Ten plus an integer. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.)
|- (; 1 0 + A ) = ; 1 A
Theorem	numma 9365	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 9366	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 9367	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 9368	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 9369	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 9370	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 9371	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 9372	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 9373	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 9374	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 9375	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 9376	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 9377	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 9378	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 9379	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 9380	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 9381	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 9382	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 9383	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 9384	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 9385	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 9386	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 9387	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 9388	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 9389	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 9390	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 9391	Lemma for 6p5e11 9394 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 9392	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 9393	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 9394	6 + 5 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.)
|- ( 6 + 5 ) = ; 1 1
Theorem	6p6e12 9395	6 + 6 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- ( 6 + 6 ) = ; 1 2
Theorem	7p3e10 9396	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 9397	7 + 4 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.)
|- ( 7 + 4 ) = ; 1 1
Theorem	7p5e12 9398	7 + 5 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- ( 7 + 5 ) = ; 1 2
Theorem	7p6e13 9399	7 + 6 = 13. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- ( 7 + 6 ) = ; 1 3
Theorem	7p7e14 9400	7 + 7 = 14. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- ( 7 + 7 ) = ; 1 4