P. 96 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 9501-9600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	zadd2cl 9501	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 9502	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 9503	Constant used for decimal constructor.
class ; A B
Definition	df-dec 9504	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 15593. (Contributed by Mario Carneiro, 17-Apr-2015.) (Revised by AV, 1-Aug-2021.)
|- ; A B = ( ( ( 9 + 1 ) x. A ) + B )
Theorem	9p1e10 9505	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 9506	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 9507	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 9508	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 9509	Equality theorem for the decimal constructor. (Contributed by Mario Carneiro, 17-Apr-2015.)
|- A = B   =>    |- ; A C = ; B C
Theorem	deceq2i 9510	Equality theorem for the decimal constructor. (Contributed by Mario Carneiro, 17-Apr-2015.)
|- A = B   =>    |- ; C A = ; C B
Theorem	deceq12i 9511	Equality theorem for the decimal constructor. (Contributed by Mario Carneiro, 17-Apr-2015.)
|- A = B   &    |- C = D   =>    |- ; A C = ; B D
Theorem	numnncl 9512	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 9513	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 9514	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 9515	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 9516	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 9517	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 9518	10 is a positive integer. (Contributed by NM, 8-Nov-2012.) (Revised by AV, 6-Sep-2021.)
|- ; 1 0 e. NN
Theorem	10pos 9519	The number 10 is positive. (Contributed by NM, 5-Feb-2007.) (Revised by AV, 8-Sep-2021.)
|- 0 < ; 1 0
Theorem	10nn0 9520	10 is a nonnegative integer. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.)
|- ; 1 0 e. NN0
Theorem	10re 9521	The number 10 is real. (Contributed by NM, 5-Feb-2007.) (Revised by AV, 8-Sep-2021.)
|- ; 1 0 e. RR
Theorem	decnncl 9522	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 9523	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 9524	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 9525	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 9526	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 9527	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 9528	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 9529	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 9530	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 9531	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 9532	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 9533	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 9534	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 9535	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 9536	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 9537	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 9538	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 9539	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 9540	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 9541	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 9542	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 9543	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 9544	The successor of zero. (Contributed by Mario Carneiro, 18-Feb-2014.)
|- 1 = ( 0 + 1 )
Theorem	dec10p 9545	Ten plus an integer. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.)
|- (; 1 0 + A ) = ; 1 A
Theorem	numma 9546	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 9547	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 9548	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 9549	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 9550	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 9551	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 9552	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 9553	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 9554	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 9555	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 9556	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 9557	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 9558	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 9559	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 9560	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 9561	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 9562	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 9563	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 9564	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 9565	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 9566	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 9567	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 9568	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 9569	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 9570	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 9571	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 9572	Lemma for 6p5e11 9575 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 9573	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 9574	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 9575	6 + 5 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.)
|- ( 6 + 5 ) = ; 1 1
Theorem	6p6e12 9576	6 + 6 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- ( 6 + 6 ) = ; 1 2
Theorem	7p3e10 9577	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 9578	7 + 4 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.)
|- ( 7 + 4 ) = ; 1 1
Theorem	7p5e12 9579	7 + 5 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- ( 7 + 5 ) = ; 1 2
Theorem	7p6e13 9580	7 + 6 = 13. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- ( 7 + 6 ) = ; 1 3
Theorem	7p7e14 9581	7 + 7 = 14. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- ( 7 + 7 ) = ; 1 4
Theorem	8p2e10 9582	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 9583	8 + 3 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.)
|- ( 8 + 3 ) = ; 1 1
Theorem	8p4e12 9584	8 + 4 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- ( 8 + 4 ) = ; 1 2
Theorem	8p5e13 9585	8 + 5 = 13. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- ( 8 + 5 ) = ; 1 3
Theorem	8p6e14 9586	8 + 6 = 14. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- ( 8 + 6 ) = ; 1 4
Theorem	8p7e15 9587	8 + 7 = 15. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- ( 8 + 7 ) = ; 1 5
Theorem	8p8e16 9588	8 + 8 = 16. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- ( 8 + 8 ) = ; 1 6
Theorem	9p2e11 9589	9 + 2 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.)
|- ( 9 + 2 ) = ; 1 1
Theorem	9p3e12 9590	9 + 3 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- ( 9 + 3 ) = ; 1 2
Theorem	9p4e13 9591	9 + 4 = 13. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- ( 9 + 4 ) = ; 1 3
Theorem	9p5e14 9592	9 + 5 = 14. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- ( 9 + 5 ) = ; 1 4
Theorem	9p6e15 9593	9 + 6 = 15. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- ( 9 + 6 ) = ; 1 5
Theorem	9p7e16 9594	9 + 7 = 16. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- ( 9 + 7 ) = ; 1 6
Theorem	9p8e17 9595	9 + 8 = 17. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- ( 9 + 8 ) = ; 1 7
Theorem	9p9e18 9596	9 + 9 = 18. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- ( 9 + 9 ) = ; 1 8
Theorem	10p10e20 9597	10 + 10 = 20. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.)
|- (; 1 0 + ; 1 0 ) = ; 2 0
Theorem	10m1e9 9598	10 - 1 = 9. (Contributed by AV, 6-Sep-2021.)
|- (; 1 0 - 1 ) = 9
Theorem	4t3lem 9599	Lemma for 4t3e12 9600 and related theorems. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- A e. NN0   &    |- B e. NN0   &    |- C = ( B + 1 )   &    |- ( A x. B ) = D   &    |- ( D + A ) = E   =>    |- ( A x. C ) = E
Theorem	4t3e12 9600	4 times 3 equals 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- ( 4 x. 3 ) = ; 1 2