P. 97 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 9601-9700   *Has distinct variable group(s)

Type	Label	Description
Statement
4.4.10  Decimal arithmetic
Syntax	cdc 9601	Constant used for decimal constructor.
class ; A B
Definition	df-dec 9602	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 16256. (Contributed by Mario Carneiro, 17-Apr-2015.) (Revised by AV, 1-Aug-2021.)
|- ; A B = ( ( ( 9 + 1 ) x. A ) + B )
Theorem	9p1e10 9603	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 9604	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 9605	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 9606	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 9607	Equality theorem for the decimal constructor. (Contributed by Mario Carneiro, 17-Apr-2015.)
|- A = B   =>    |- ; A C = ; B C
Theorem	deceq2i 9608	Equality theorem for the decimal constructor. (Contributed by Mario Carneiro, 17-Apr-2015.)
|- A = B   =>    |- ; C A = ; C B
Theorem	deceq12i 9609	Equality theorem for the decimal constructor. (Contributed by Mario Carneiro, 17-Apr-2015.)
|- A = B   &    |- C = D   =>    |- ; A C = ; B D
Theorem	numnncl 9610	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 9611	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 9612	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 9613	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 9614	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 9615	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 9616	10 is a positive integer. (Contributed by NM, 8-Nov-2012.) (Revised by AV, 6-Sep-2021.)
|- ; 1 0 e. NN
Theorem	10pos 9617	The number 10 is positive. (Contributed by NM, 5-Feb-2007.) (Revised by AV, 8-Sep-2021.)
|- 0 < ; 1 0
Theorem	10nn0 9618	10 is a nonnegative integer. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.)
|- ; 1 0 e. NN0
Theorem	10re 9619	The number 10 is real. (Contributed by NM, 5-Feb-2007.) (Revised by AV, 8-Sep-2021.)
|- ; 1 0 e. RR
Theorem	decnncl 9620	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 9621	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 9622	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 9623	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 9624	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 9625	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 9626	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 9627	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 9628	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 9629	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 9630	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 9631	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 9632	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 9633	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 9634	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 9635	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 9636	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 9637	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 9638	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 9639	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 9640	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 9641	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 9642	The successor of zero. (Contributed by Mario Carneiro, 18-Feb-2014.)
|- 1 = ( 0 + 1 )
Theorem	dec10p 9643	Ten plus an integer. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.)
|- (; 1 0 + A ) = ; 1 A
Theorem	numma 9644	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 9645	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 9646	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 9647	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 9648	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 9649	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 9650	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 9651	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 9652	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 9653	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 9654	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 9655	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 9656	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 9657	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 9658	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 9659	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 9660	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 9661	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 9662	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 9663	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 9664	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 9665	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 9666	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 9667	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 9668	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 9669	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 9670	Lemma for 6p5e11 9673 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 9671	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 9672	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 9673	6 + 5 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.)
|- ( 6 + 5 ) = ; 1 1
Theorem	6p6e12 9674	6 + 6 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- ( 6 + 6 ) = ; 1 2
Theorem	7p3e10 9675	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 9676	7 + 4 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.)
|- ( 7 + 4 ) = ; 1 1
Theorem	7p5e12 9677	7 + 5 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- ( 7 + 5 ) = ; 1 2
Theorem	7p6e13 9678	7 + 6 = 13. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- ( 7 + 6 ) = ; 1 3
Theorem	7p7e14 9679	7 + 7 = 14. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- ( 7 + 7 ) = ; 1 4
Theorem	8p2e10 9680	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 9681	8 + 3 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.)
|- ( 8 + 3 ) = ; 1 1
Theorem	8p4e12 9682	8 + 4 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- ( 8 + 4 ) = ; 1 2
Theorem	8p5e13 9683	8 + 5 = 13. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- ( 8 + 5 ) = ; 1 3
Theorem	8p6e14 9684	8 + 6 = 14. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- ( 8 + 6 ) = ; 1 4
Theorem	8p7e15 9685	8 + 7 = 15. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- ( 8 + 7 ) = ; 1 5
Theorem	8p8e16 9686	8 + 8 = 16. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- ( 8 + 8 ) = ; 1 6
Theorem	9p2e11 9687	9 + 2 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.)
|- ( 9 + 2 ) = ; 1 1
Theorem	9p3e12 9688	9 + 3 = 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- ( 9 + 3 ) = ; 1 2
Theorem	9p4e13 9689	9 + 4 = 13. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- ( 9 + 4 ) = ; 1 3
Theorem	9p5e14 9690	9 + 5 = 14. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- ( 9 + 5 ) = ; 1 4
Theorem	9p6e15 9691	9 + 6 = 15. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- ( 9 + 6 ) = ; 1 5
Theorem	9p7e16 9692	9 + 7 = 16. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- ( 9 + 7 ) = ; 1 6
Theorem	9p8e17 9693	9 + 8 = 17. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- ( 9 + 8 ) = ; 1 7
Theorem	9p9e18 9694	9 + 9 = 18. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- ( 9 + 9 ) = ; 1 8
Theorem	10p10e20 9695	10 + 10 = 20. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.)
|- (; 1 0 + ; 1 0 ) = ; 2 0
Theorem	10m1e9 9696	10 - 1 = 9. (Contributed by AV, 6-Sep-2021.)
|- (; 1 0 - 1 ) = 9
Theorem	4t3lem 9697	Lemma for 4t3e12 9698 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 9698	4 times 3 equals 12. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- ( 4 x. 3 ) = ; 1 2
Theorem	4t4e16 9699	4 times 4 equals 16. (Contributed by Mario Carneiro, 19-Apr-2015.)
|- ( 4 x. 4 ) = ; 1 6
Theorem	5t2e10 9700	5 times 2 equals 10. (Contributed by NM, 5-Feb-2007.) (Revised by AV, 4-Sep-2021.)
|- ( 5 x. 2 ) = ; 1 0