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	zdclt 9701	Integer < is decidable. (Contributed by Jim Kingdon, 1-Jun-2020.)
|- ( ( A e. ZZ /\ B e. ZZ ) -> DECID A < B )
Theorem	zfidc 9702	Whether an integer is an element of a finite set of integers is decidable. (Contributed by Jim Kingdon, 8-Jun-2026.)
|- ( ( S C_ ZZ /\ A e. ZZ /\ S e. Fin ) -> DECID A e. S )
Theorem	zltlen 9703	Integer 'Less than' expressed in terms of 'less than or equal to'. Also see ltleap 8950 which is a similar result for real numbers. (Contributed by Jim Kingdon, 14-Mar-2020.)
|- ( ( A e. ZZ /\ B e. ZZ ) -> ( A < B <-> ( A <_ B /\ B =/= A ) ) )
Theorem	nn0n0n1ge2b 9704	A nonnegative integer is neither 0 nor 1 if and only if it is greater than or equal to 2. (Contributed by Alexander van der Vekens, 17-Jan-2018.)
|- ( N e. NN0 -> ( ( N =/= 0 /\ N =/= 1 ) <-> 2 <_ N ) )
Theorem	nn0lt10b 9705	A nonnegative integer less than 1 is 0. (Contributed by Paul Chapman, 22-Jun-2011.)
|- ( N e. NN0 -> ( N < 1 <-> N = 0 ) )
Theorem	nn0lt2 9706	A nonnegative integer less than 2 must be 0 or 1. (Contributed by Alexander van der Vekens, 16-Sep-2018.)
|- ( ( N e. NN0 /\ N < 2 ) -> ( N = 0 \/ N = 1 ) )
Theorem	nn0le2is012 9707	A nonnegative integer which is less than or equal to 2 is either 0 or 1 or 2. (Contributed by AV, 16-Mar-2019.)
|- ( ( N e. NN0 /\ N <_ 2 ) -> ( N = 0 \/ N = 1 \/ N = 2 ) )
Theorem	nn0lem1lt 9708	Nonnegative integer ordering relation. (Contributed by NM, 21-Jun-2005.)
|- ( ( M e. NN0 /\ N e. NN0 ) -> ( M <_ N <-> ( M - 1 ) < N ) )
Theorem	nnlem1lt 9709	Positive integer ordering relation. (Contributed by NM, 21-Jun-2005.)
|- ( ( M e. NN /\ N e. NN ) -> ( M <_ N <-> ( M - 1 ) < N ) )
Theorem	nnltlem1 9710	Positive integer ordering relation. (Contributed by NM, 21-Jun-2005.)
|- ( ( M e. NN /\ N e. NN ) -> ( M < N <-> M <_ ( N - 1 ) ) )
Theorem	nnm1ge0 9711	A positive integer decreased by 1 is greater than or equal to 0. (Contributed by AV, 30-Oct-2018.)
|- ( N e. NN -> 0 <_ ( N - 1 ) )
Theorem	nn0ge0div 9712	Division of a nonnegative integer by a positive number is not negative. (Contributed by Alexander van der Vekens, 14-Apr-2018.)
|- ( ( K e. NN0 /\ L e. NN ) -> 0 <_ ( K / L ) )
Theorem	zdiv 9713*	Two ways to express " M divides N. (Contributed by NM, 3-Oct-2008.)
|- ( ( M e. NN /\ N e. ZZ ) -> ( E. k e. ZZ ( M x. k ) = N <-> ( N / M ) e. ZZ ) )
Theorem	zdivadd 9714	Property of divisibility: if D divides A and B then it divides A + B. (Contributed by NM, 3-Oct-2008.)
|- ( ( ( D e. NN /\ A e. ZZ /\ B e. ZZ ) /\ ( ( A / D ) e. ZZ /\ ( B / D ) e. ZZ ) ) -> ( ( A + B ) / D ) e. ZZ )
Theorem	zdivmul 9715	Property of divisibility: if D divides A then it divides B x. A. (Contributed by NM, 3-Oct-2008.)
|- ( ( ( D e. NN /\ A e. ZZ /\ B e. ZZ ) /\ ( A / D ) e. ZZ ) -> ( ( B x. A ) / D ) e. ZZ )
Theorem	zextle 9716*	An extensionality-like property for integer ordering. (Contributed by NM, 29-Oct-2005.)
|- ( ( M e. ZZ /\ N e. ZZ /\ A. k e. ZZ ( k <_ M <-> k <_ N ) ) -> M = N )
Theorem	zextlt 9717*	An extensionality-like property for integer ordering. (Contributed by NM, 29-Oct-2005.)
|- ( ( M e. ZZ /\ N e. ZZ /\ A. k e. ZZ ( k < M <-> k < N ) ) -> M = N )
Theorem	recnz 9718	The reciprocal of a number greater than 1 is not an integer. (Contributed by NM, 3-May-2005.)
|- ( ( A e. RR /\ 1 < A ) -> -. ( 1 / A ) e. ZZ )
Theorem	btwnnz 9719	A number between an integer and its successor is not an integer. (Contributed by NM, 3-May-2005.)
|- ( ( A e. ZZ /\ A < B /\ B < ( A + 1 ) ) -> -. B e. ZZ )
Theorem	gtndiv 9720	A larger number does not divide a smaller positive integer. (Contributed by NM, 3-May-2005.)
|- ( ( A e. RR /\ B e. NN /\ B < A ) -> -. ( B / A ) e. ZZ )
Theorem	halfnz 9721	One-half is not an integer. (Contributed by NM, 31-Jul-2004.)
|- -. ( 1 / 2 ) e. ZZ
Theorem	3halfnz 9722	Three halves is not an integer. (Contributed by AV, 2-Jun-2020.)
|- -. ( 3 / 2 ) e. ZZ
Theorem	suprzclex 9723*	The supremum of a set of integers is an element of the set. (Contributed by Jim Kingdon, 20-Dec-2021.)
|- ( ph -> E. x e. RR ( A. y e. A -. x < y /\ A. y e. RR ( y < x -> E. z e. A y < z ) ) )   &    |- ( ph -> A C_ ZZ )   =>    |- ( ph -> sup ( A , RR , < ) e. A )
Theorem	prime 9724*	Two ways to express " A is a prime number (or 1)". (Contributed by NM, 4-May-2005.)
|- ( A e. NN -> ( A. x e. NN ( ( A / x ) e. NN -> ( x = 1 \/ x = A ) ) <-> A. x e. NN ( ( 1 < x /\ x <_ A /\ ( A / x ) e. NN ) -> x = A ) ) )
Theorem	msqznn 9725	The square of a nonzero integer is a positive integer. (Contributed by NM, 2-Aug-2004.)
|- ( ( A e. ZZ /\ A =/= 0 ) -> ( A x. A ) e. NN )
Theorem	zneo 9726	No even integer equals an odd integer (i.e. no integer can be both even and odd). Exercise 10(a) of [Apostol] p. 28. (Contributed by NM, 31-Jul-2004.) (Proof shortened by Mario Carneiro, 18-May-2014.)
|- ( ( A e. ZZ /\ B e. ZZ ) -> ( 2 x. A ) =/= ( ( 2 x. B ) + 1 ) )
Theorem	nneoor 9727	A positive integer is even or odd. (Contributed by Jim Kingdon, 15-Mar-2020.)
|- ( N e. NN -> ( ( N / 2 ) e. NN \/ ( ( N + 1 ) / 2 ) e. NN ) )
Theorem	nneo 9728	A positive integer is even or odd but not both. (Contributed by NM, 1-Jan-2006.) (Proof shortened by Mario Carneiro, 18-May-2014.)
|- ( N e. NN -> ( ( N / 2 ) e. NN <-> -. ( ( N + 1 ) / 2 ) e. NN ) )
Theorem	nneoi 9729	A positive integer is even or odd but not both. (Contributed by NM, 20-Aug-2001.)
|- N e. NN   =>    |- ( ( N / 2 ) e. NN <-> -. ( ( N + 1 ) / 2 ) e. NN )
Theorem	zeo 9730	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 9731	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 9732*	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 9733*	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 9734*	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 9735*	An expression for the upper integers that start at N that is analogous to dfnn2 9285 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 9736*	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 9737*	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 9738*	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 9739*	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 9740*	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 9741*	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 9742*	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 9743*	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 9744*	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 9745	A positive integer is an integer. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. NN0 )   =>    |- ( ph -> A e. ZZ )
Theorem	nnzd 9746	A nonnegative integer is an integer. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. NN )   =>    |- ( ph -> A e. ZZ )
Theorem	zred 9747	An integer is a real number. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. ZZ )   =>    |- ( ph -> A e. RR )
Theorem	zcnd 9748	An integer is a complex number. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. ZZ )   =>    |- ( ph -> A e. CC )
Theorem	znegcld 9749	Closure law for negative integers. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. ZZ )   =>    |- ( ph -> -u A e. ZZ )
Theorem	peano2zd 9750	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 9751	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 9752	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 9753	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 9754	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 9755	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 9756	Constant used for decimal constructor.
class ; A B
Definition	df-dec 9757	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 16652. (Contributed by Mario Carneiro, 17-Apr-2015.) (Revised by AV, 1-Aug-2021.)
|- ; A B = ( ( ( 9 + 1 ) x. A ) + B )
Theorem	9p1e10 9758	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 9759	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 9760	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 9761	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 9762	Equality theorem for the decimal constructor. (Contributed by Mario Carneiro, 17-Apr-2015.)
|- A = B   =>    |- ; A C = ; B C
Theorem	deceq2i 9763	Equality theorem for the decimal constructor. (Contributed by Mario Carneiro, 17-Apr-2015.)
|- A = B   =>    |- ; C A = ; C B
Theorem	deceq12i 9764	Equality theorem for the decimal constructor. (Contributed by Mario Carneiro, 17-Apr-2015.)
|- A = B   &    |- C = D   =>    |- ; A C = ; B D
Theorem	numnncl 9765	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 9766	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 9767	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 9768	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 9769	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 9770	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 9771	10 is a positive integer. (Contributed by NM, 8-Nov-2012.) (Revised by AV, 6-Sep-2021.)
|- ; 1 0 e. NN
Theorem	10pos 9772	The number 10 is positive. (Contributed by NM, 5-Feb-2007.) (Revised by AV, 8-Sep-2021.)
|- 0 < ; 1 0
Theorem	10nn0 9773	10 is a nonnegative integer. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.)
|- ; 1 0 e. NN0
Theorem	10re 9774	The number 10 is real. (Contributed by NM, 5-Feb-2007.) (Revised by AV, 8-Sep-2021.)
|- ; 1 0 e. RR
Theorem	decnncl 9775	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 9776	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 9777	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 9778	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 9779	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 9780	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 9781	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 9782	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 9783	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 9784	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 9785	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 9786	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 9787	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 9788	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 9789	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 9790	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 9791	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 9792	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 9793	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 9794	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 9795	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 9796	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 9797	The successor of zero. (Contributed by Mario Carneiro, 18-Feb-2014.)
|- 1 = ( 0 + 1 )
Theorem	dec10p 9798	Ten plus an integer. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.)
|- (; 1 0 + A ) = ; 1 A
Theorem	numma 9799	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 9800	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 )