P. 108 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 10701-10800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	bccl 10701	A binomial coefficient, in its extended domain, is a nonnegative integer. (Contributed by NM, 10-Jul-2005.) (Revised by Mario Carneiro, 9-Nov-2013.)
|- ( ( N e. NN0 /\ K e. ZZ ) -> ( N _C K ) e. NN0 )
Theorem	bccl2 10702	A binomial coefficient, in its standard domain, is a positive integer. (Contributed by NM, 3-Jan-2006.) (Revised by Mario Carneiro, 10-Mar-2014.)
|- ( K e. ( 0 ... N ) -> ( N _C K ) e. NN )
Theorem	bcn2m1 10703	Compute the binomial coefficient " N choose 2 " from " ( N - 1 ) choose 2 ": (N-1) + ( (N-1) 2 ) = ( N 2 ). (Contributed by Alexander van der Vekens, 7-Jan-2018.)
|- ( N e. NN -> ( ( N - 1 ) + ( ( N - 1 ) _C 2 ) ) = ( N _C 2 ) )
Theorem	bcn2p1 10704	Compute the binomial coefficient " ( N + 1 ) choose 2 " from " N choose 2 ": N + ( N 2 ) = ( (N+1) 2 ). (Contributed by Alexander van der Vekens, 8-Jan-2018.)
|- ( N e. NN0 -> ( N + ( N _C 2 ) ) = ( ( N + 1 ) _C 2 ) )
Theorem	permnn 10705	The number of permutations of N - R objects from a collection of N objects is a positive integer. (Contributed by Jason Orendorff, 24-Jan-2007.)
|- ( R e. ( 0 ... N ) -> ( ( ! ` N ) / ( ! ` R ) ) e. NN )
Theorem	bcnm1 10706	The binomial coefficent of ( N - 1 ) is N. (Contributed by Scott Fenton, 16-May-2014.)
|- ( N e. NN0 -> ( N _C ( N - 1 ) ) = N )
Theorem	4bc3eq4 10707	The value of four choose three. (Contributed by Scott Fenton, 11-Jun-2016.)
|- ( 4 _C 3 ) = 4
Theorem	4bc2eq6 10708	The value of four choose two. (Contributed by Scott Fenton, 9-Jan-2017.)
|- ( 4 _C 2 ) = 6
4.6.10  The ` # ` (set size) function
Syntax	chash 10709	Extend the definition of a class to include the set size function.
class ♯
Definition	df-ihash 10710*	Define the set size function ♯, which gives the cardinality of a finite set as a member of NN0, and assigns all infinite sets the value +oo. For example, (♯ ` { 0 , 1 , 2 } ) = 3. Note that we use the sharp sign (♯) for this function and we use the different character octothorpe (#) for the apartness relation (see df-ap 8501). We adopt the former notation from Corollary 8.2.4 of [AczelRathjen], p. 80 (although that work only defines it for finite sets). This definition (in terms of U. and ~<_) is not taken directly from the literature, but for finite sets should be equivalent to the conventional definition that the size of a finite set is the unique natural number which is equinumerous to the given set. (Contributed by Jim Kingdon, 19-Feb-2022.)
|- ♯ = ( (frec ( ( x e. ZZ |-> ( x + 1 ) ) , 0 ) u. { <. om , +oo >. } ) o. ( x e. _V |-> U. { y e. ( om u. { om } ) | y ~<_ x } ) )
Theorem	hashinfuni 10711*	The ordinal size of an infinite set is om. (Contributed by Jim Kingdon, 20-Feb-2022.)
|- ( om ~<_ A -> U. { y e. ( om u. { om } ) | y ~<_ A } = om )
Theorem	hashinfom 10712	The value of the ♯ function on an infinite set. (Contributed by Jim Kingdon, 20-Feb-2022.)
|- ( om ~<_ A -> (♯ ` A ) = +oo )
Theorem	hashennnuni 10713*	The ordinal size of a set equinumerous to an element of om is that element of om. (Contributed by Jim Kingdon, 20-Feb-2022.)
|- ( ( N e. om /\ N ~~ A ) -> U. { y e. ( om u. { om } ) | y ~<_ A } = N )
Theorem	hashennn 10714*	The size of a set equinumerous to an element of om. (Contributed by Jim Kingdon, 21-Feb-2022.)
|- ( ( N e. om /\ N ~~ A ) -> (♯ ` A ) = (frec ( ( x e. ZZ |-> ( x + 1 ) ) , 0 ) ` N ) )
Theorem	hashcl 10715	Closure of the ♯ function. (Contributed by Paul Chapman, 26-Oct-2012.) (Revised by Mario Carneiro, 13-Jul-2014.)
|- ( A e. Fin -> (♯ ` A ) e. NN0 )
Theorem	hashfiv01gt1 10716	The size of a finite set is either 0 or 1 or greater than 1. (Contributed by Jim Kingdon, 21-Feb-2022.)
|- ( M e. Fin -> ( (♯ ` M ) = 0 \/ (♯ ` M ) = 1 \/ 1 < (♯ ` M ) ) )
Theorem	hashfz1 10717	The set ( 1 ... N ) has N elements. (Contributed by Paul Chapman, 22-Jun-2011.) (Revised by Mario Carneiro, 15-Sep-2013.)
|- ( N e. NN0 -> (♯ ` ( 1 ... N ) ) = N )
Theorem	hashen 10718	Two finite sets have the same number of elements iff they are equinumerous. (Contributed by Paul Chapman, 22-Jun-2011.) (Revised by Mario Carneiro, 15-Sep-2013.)
|- ( ( A e. Fin /\ B e. Fin ) -> ( (♯ ` A ) = (♯ ` B ) <-> A ~~ B ) )
Theorem	hasheqf1o 10719*	The size of two finite sets is equal if and only if there is a bijection mapping one of the sets onto the other. (Contributed by Alexander van der Vekens, 17-Dec-2017.)
|- ( ( A e. Fin /\ B e. Fin ) -> ( (♯ ` A ) = (♯ ` B ) <-> E. f f : A -1-1-onto-> B ) )
Theorem	fiinfnf1o 10720*	There is no bijection between a finite set and an infinite set. By infnfi 6873 the theorem would also hold if "infinite" were expressed as om ~<_ B. (Contributed by Alexander van der Vekens, 25-Dec-2017.)
|- ( ( A e. Fin /\ -. B e. Fin ) -> -. E. f f : A -1-1-onto-> B )
Theorem	focdmex 10721	The codomain of an onto function is a set if its domain is a set. (Contributed by AV, 4-May-2021.)
|- ( ( A e. V /\ F : A -onto-> B ) -> B e. _V )
Theorem	fihasheqf1oi 10722	The size of two finite sets is equal if there is a bijection mapping one of the sets onto the other. (Contributed by Jim Kingdon, 21-Feb-2022.)
|- ( ( A e. Fin /\ F : A -1-1-onto-> B ) -> (♯ ` A ) = (♯ ` B ) )
Theorem	fihashf1rn 10723	The size of a finite set which is a one-to-one function is equal to the size of the function's range. (Contributed by Jim Kingdon, 21-Feb-2022.)
|- ( ( A e. Fin /\ F : A -1-1-> B ) -> (♯ ` F ) = (♯ ` ran F ) )
Theorem	fihasheqf1od 10724	The size of two finite sets is equal if there is a bijection mapping one of the sets onto the other. (Contributed by Jim Kingdon, 21-Feb-2022.)
|- ( ph -> A e. Fin )   &    |- ( ph -> F : A -1-1-onto-> B )   =>    |- ( ph -> (♯ ` A ) = (♯ ` B ) )
Theorem	fz1eqb 10725	Two possibly-empty 1-based finite sets of sequential integers are equal iff their endpoints are equal. (Contributed by Paul Chapman, 22-Jun-2011.) (Proof shortened by Mario Carneiro, 29-Mar-2014.)
|- ( ( M e. NN0 /\ N e. NN0 ) -> ( ( 1 ... M ) = ( 1 ... N ) <-> M = N ) )
Theorem	filtinf 10726	The size of an infinite set is greater than the size of a finite set. (Contributed by Jim Kingdon, 21-Feb-2022.)
|- ( ( A e. Fin /\ om ~<_ B ) -> (♯ ` A ) < (♯ ` B ) )
Theorem	isfinite4im 10727	A finite set is equinumerous to the range of integers from one up to the hash value of the set. (Contributed by Jim Kingdon, 22-Feb-2022.)
|- ( A e. Fin -> ( 1 ... (♯ ` A ) ) ~~ A )
Theorem	fihasheq0 10728	Two ways of saying a finite set is empty. (Contributed by Paul Chapman, 26-Oct-2012.) (Revised by Mario Carneiro, 27-Jul-2014.) (Intuitionized by Jim Kingdon, 23-Feb-2022.)
|- ( A e. Fin -> ( (♯ ` A ) = 0 <-> A = (/) ) )
Theorem	fihashneq0 10729	Two ways of saying a finite set is not empty. Also, "A is inhabited" would be equivalent by fin0 6863. (Contributed by Alexander van der Vekens, 23-Sep-2018.) (Intuitionized by Jim Kingdon, 23-Feb-2022.)
|- ( A e. Fin -> ( 0 < (♯ ` A ) <-> A =/= (/) ) )
Theorem	hashnncl 10730	Positive natural closure of the hash function. (Contributed by Mario Carneiro, 16-Jan-2015.)
|- ( A e. Fin -> ( (♯ ` A ) e. NN <-> A =/= (/) ) )
Theorem	hash0 10731	The empty set has size zero. (Contributed by Mario Carneiro, 8-Jul-2014.)
|- (♯ ` (/) ) = 0
Theorem	fihashelne0d 10732	A finite set with an element has nonzero size. (Contributed by Rohan Ridenour, 3-Aug-2023.)
|- ( ph -> B e. A )   &    |- ( ph -> A e. Fin )   =>    |- ( ph -> -. (♯ ` A ) = 0 )
Theorem	hashsng 10733	The size of a singleton. (Contributed by Paul Chapman, 26-Oct-2012.) (Proof shortened by Mario Carneiro, 13-Feb-2013.)
|- ( A e. V -> (♯ ` { A } ) = 1 )
Theorem	fihashen1 10734	A finite set has size 1 if and only if it is equinumerous to the ordinal 1. (Contributed by AV, 14-Apr-2019.) (Intuitionized by Jim Kingdon, 23-Feb-2022.)
|- ( A e. Fin -> ( (♯ ` A ) = 1 <-> A ~~ 1o ) )
Theorem	fihashfn 10735	A function on a finite set is equinumerous to its domain. (Contributed by Mario Carneiro, 12-Mar-2015.) (Intuitionized by Jim Kingdon, 24-Feb-2022.)
|- ( ( F Fn A /\ A e. Fin ) -> (♯ ` F ) = (♯ ` A ) )
Theorem	fseq1hash 10736	The value of the size function on a finite 1-based sequence. (Contributed by Paul Chapman, 26-Oct-2012.) (Proof shortened by Mario Carneiro, 12-Mar-2015.)
|- ( ( N e. NN0 /\ F Fn ( 1 ... N ) ) -> (♯ ` F ) = N )
Theorem	omgadd 10737	Mapping ordinal addition to integer addition. (Contributed by Jim Kingdon, 24-Feb-2022.)
|- G = frec ( ( x e. ZZ |-> ( x + 1 ) ) , 0 )   =>    |- ( ( A e. om /\ B e. om ) -> ( G ` ( A +o B ) ) = ( ( G ` A ) + ( G ` B ) ) )
Theorem	fihashdom 10738	Dominance relation for the size function. (Contributed by Jim Kingdon, 24-Feb-2022.)
|- ( ( A e. Fin /\ B e. Fin ) -> ( (♯ ` A ) <_ (♯ ` B ) <-> A ~<_ B ) )
Theorem	hashunlem 10739	Lemma for hashun 10740. Ordinal size of the union. (Contributed by Jim Kingdon, 25-Feb-2022.)
|- ( ph -> A e. Fin )   &    |- ( ph -> B e. Fin )   &    |- ( ph -> ( A i^i B ) = (/) )   &    |- ( ph -> N e. om )   &    |- ( ph -> M e. om )   &    |- ( ph -> A ~~ N )   &    |- ( ph -> B ~~ M )   =>    |- ( ph -> ( A u. B ) ~~ ( N +o M ) )
Theorem	hashun 10740	The size of the union of disjoint finite sets is the sum of their sizes. (Contributed by Paul Chapman, 30-Nov-2012.) (Revised by Mario Carneiro, 15-Sep-2013.)
|- ( ( A e. Fin /\ B e. Fin /\ ( A i^i B ) = (/) ) -> (♯ ` ( A u. B ) ) = ( (♯ ` A ) + (♯ ` B ) ) )
Theorem	1elfz0hash 10741	1 is an element of the finite set of sequential nonnegative integers bounded by the size of a nonempty finite set. (Contributed by AV, 9-May-2020.)
|- ( ( A e. Fin /\ A =/= (/) ) -> 1 e. ( 0 ... (♯ ` A ) ) )
Theorem	hashunsng 10742	The size of the union of a finite set with a disjoint singleton is one more than the size of the set. (Contributed by Paul Chapman, 30-Nov-2012.)
|- ( B e. V -> ( ( A e. Fin /\ -. B e. A ) -> (♯ ` ( A u. { B } ) ) = ( (♯ ` A ) + 1 ) ) )
Theorem	hashprg 10743	The size of an unordered pair. (Contributed by Mario Carneiro, 27-Sep-2013.) (Revised by Mario Carneiro, 5-May-2016.) (Revised by AV, 18-Sep-2021.)
|- ( ( A e. V /\ B e. W ) -> ( A =/= B <-> (♯ ` { A , B } ) = 2 ) )
Theorem	prhash2ex 10744	There is (at least) one set with two different elements: the unordered pair containing 0 and 1. In contrast to pr0hash2ex 10750, numbers are used instead of sets because their representation is shorter (and more comprehensive). (Contributed by AV, 29-Jan-2020.)
|- (♯ ` { 0 , 1 } ) = 2
Theorem	hashp1i 10745	Size of a natural number ordinal. (Contributed by Mario Carneiro, 5-Jan-2016.)
|- A e. om   &    |- B = suc A   &    |- (♯ ` A ) = M   &    |- ( M + 1 ) = N   =>    |- (♯ ` B ) = N
Theorem	hash1 10746	Size of a natural number ordinal. (Contributed by Mario Carneiro, 5-Jan-2016.)
|- (♯ ` 1o ) = 1
Theorem	hash2 10747	Size of a natural number ordinal. (Contributed by Mario Carneiro, 5-Jan-2016.)
|- (♯ ` 2o ) = 2
Theorem	hash3 10748	Size of a natural number ordinal. (Contributed by Mario Carneiro, 5-Jan-2016.)
|- (♯ ` 3o ) = 3
Theorem	hash4 10749	Size of a natural number ordinal. (Contributed by Mario Carneiro, 5-Jan-2016.)
|- (♯ ` 4o ) = 4
Theorem	pr0hash2ex 10750	There is (at least) one set with two different elements: the unordered pair containing the empty set and the singleton containing the empty set. (Contributed by AV, 29-Jan-2020.)
|- (♯ ` { (/) , { (/) } } ) = 2
Theorem	fihashss 10751	The size of a subset is less than or equal to the size of its superset. (Contributed by Alexander van der Vekens, 14-Jul-2018.)
|- ( ( A e. Fin /\ B e. Fin /\ B C_ A ) -> (♯ ` B ) <_ (♯ ` A ) )
Theorem	fiprsshashgt1 10752	The size of a superset of a proper unordered pair is greater than 1. (Contributed by AV, 6-Feb-2021.)
|- ( ( ( A e. V /\ B e. W /\ A =/= B ) /\ C e. Fin ) -> ( { A , B } C_ C -> 2 <_ (♯ ` C ) ) )
Theorem	fihashssdif 10753	The size of the difference of a finite set and a finite subset is the set's size minus the subset's. (Contributed by Jim Kingdon, 31-May-2022.)
|- ( ( A e. Fin /\ B e. Fin /\ B C_ A ) -> (♯ ` ( A \ B ) ) = ( (♯ ` A ) - (♯ ` B ) ) )
Theorem	hashdifsn 10754	The size of the difference of a finite set and a singleton subset is the set's size minus 1. (Contributed by Alexander van der Vekens, 6-Jan-2018.)
|- ( ( A e. Fin /\ B e. A ) -> (♯ ` ( A \ { B } ) ) = ( (♯ ` A ) - 1 ) )
Theorem	hashdifpr 10755	The size of the difference of a finite set and a proper ordered pair subset is the set's size minus 2. (Contributed by AV, 16-Dec-2020.)
|- ( ( A e. Fin /\ ( B e. A /\ C e. A /\ B =/= C ) ) -> (♯ ` ( A \ { B , C } ) ) = ( (♯ ` A ) - 2 ) )
Theorem	hashfz 10756	Value of the numeric cardinality of a nonempty integer range. (Contributed by Stefan O'Rear, 12-Sep-2014.) (Proof shortened by Mario Carneiro, 15-Apr-2015.)
|- ( B e. ( ZZ>= ` A ) -> (♯ ` ( A ... B ) ) = ( ( B - A ) + 1 ) )
Theorem	hashfzo 10757	Cardinality of a half-open set of integers. (Contributed by Stefan O'Rear, 15-Aug-2015.)
|- ( B e. ( ZZ>= ` A ) -> (♯ ` ( A..^ B ) ) = ( B - A ) )
Theorem	hashfzo0 10758	Cardinality of a half-open set of integers based at zero. (Contributed by Stefan O'Rear, 15-Aug-2015.)
|- ( B e. NN0 -> (♯ ` ( 0..^ B ) ) = B )
Theorem	hashfzp1 10759	Value of the numeric cardinality of a (possibly empty) integer range. (Contributed by AV, 19-Jun-2021.)
|- ( B e. ( ZZ>= ` A ) -> (♯ ` ( ( A + 1 ) ... B ) ) = ( B - A ) )
Theorem	hashfz0 10760	Value of the numeric cardinality of a nonempty range of nonnegative integers. (Contributed by Alexander van der Vekens, 21-Jul-2018.)
|- ( B e. NN0 -> (♯ ` ( 0 ... B ) ) = ( B + 1 ) )
Theorem	hashxp 10761	The size of the Cartesian product of two finite sets is the product of their sizes. (Contributed by Paul Chapman, 30-Nov-2012.)
|- ( ( A e. Fin /\ B e. Fin ) -> (♯ ` ( A X. B ) ) = ( (♯ ` A ) x. (♯ ` B ) ) )
Theorem	fimaxq 10762*	A finite set of rational numbers has a maximum. (Contributed by Jim Kingdon, 6-Sep-2022.)
|- ( ( A C_ QQ /\ A e. Fin /\ A =/= (/) ) -> E. x e. A A. y e. A y <_ x )
Theorem	fiubm 10763*	Lemma for fiubz 10764 and fiubnn 10765. A general form of those theorems. (Contributed by Jim Kingdon, 29-Oct-2024.)
|- ( ph -> A C_ B )   &    |- ( ph -> B C_ QQ )   &    |- ( ph -> C e. B )   &    |- ( ph -> A e. Fin )   =>    |- ( ph -> E. x e. B A. y e. A y <_ x )
Theorem	fiubz 10764*	A finite set of integers has an upper bound which is an integer. (Contributed by Jim Kingdon, 29-Oct-2024.)
|- ( ( A C_ ZZ /\ A e. Fin ) -> E. x e. ZZ A. y e. A y <_ x )
Theorem	fiubnn 10765*	A finite set of natural numbers has an upper bound which is a a natural number. (Contributed by Jim Kingdon, 29-Oct-2024.)
|- ( ( A C_ NN /\ A e. Fin ) -> E. x e. NN A. y e. A y <_ x )
Theorem	resunimafz0 10766	The union of a restriction by an image over an open range of nonnegative integers and a singleton of an ordered pair is a restriction by an image over an interval of nonnegative integers. (Contributed by Mario Carneiro, 8-Apr-2015.) (Revised by AV, 20-Feb-2021.)
|- ( ph -> Fun I )   &    |- ( ph -> F : ( 0..^ (♯ ` F ) ) --> dom I )   &    |- ( ph -> N e. ( 0..^ (♯ ` F ) ) )   =>    |- ( ph -> ( I |` ( F " ( 0 ... N ) ) ) = ( ( I |` ( F " ( 0..^ N ) ) ) u. { <. ( F ` N ) , ( I ` ( F ` N ) ) >. } ) )
Theorem	fnfz0hash 10767	The size of a function on a finite set of sequential nonnegative integers. (Contributed by Alexander van der Vekens, 25-Jun-2018.)
|- ( ( N e. NN0 /\ F Fn ( 0 ... N ) ) -> (♯ ` F ) = ( N + 1 ) )
Theorem	ffz0hash 10768	The size of a function on a finite set of sequential nonnegative integers equals the upper bound of the sequence increased by 1. (Contributed by Alexander van der Vekens, 15-Mar-2018.) (Proof shortened by AV, 11-Apr-2021.)
|- ( ( N e. NN0 /\ F : ( 0 ... N ) --> B ) -> (♯ ` F ) = ( N + 1 ) )
Theorem	ffzo0hash 10769	The size of a function on a half-open range of nonnegative integers. (Contributed by Alexander van der Vekens, 25-Mar-2018.)
|- ( ( N e. NN0 /\ F Fn ( 0..^ N ) ) -> (♯ ` F ) = N )
Theorem	fnfzo0hash 10770	The size of a function on a half-open range of nonnegative integers equals the upper bound of this range. (Contributed by Alexander van der Vekens, 26-Jan-2018.) (Proof shortened by AV, 11-Apr-2021.)
|- ( ( N e. NN0 /\ F : ( 0..^ N ) --> B ) -> (♯ ` F ) = N )
Theorem	hashfacen 10771*	The number of bijections between two sets is a cardinal invariant. (Contributed by Mario Carneiro, 21-Jan-2015.)
|- ( ( A ~~ B /\ C ~~ D ) -> { f | f : A -1-1-onto-> C } ~~ { f | f : B -1-1-onto-> D } )
Theorem	leisorel 10772	Version of isorel 5787 for strictly increasing functions on the reals. (Contributed by Mario Carneiro, 6-Apr-2015.) (Revised by Mario Carneiro, 9-Sep-2015.)
|- ( ( F Isom < , < ( A , B ) /\ ( A C_ RR* /\ B C_ RR* ) /\ ( C e. A /\ D e. A ) ) -> ( C <_ D <-> ( F ` C ) <_ ( F ` D ) ) )
Theorem	zfz1isolemsplit 10773	Lemma for zfz1iso 10776. Removing one element from an integer range. (Contributed by Jim Kingdon, 8-Sep-2022.)
|- ( ph -> X e. Fin )   &    |- ( ph -> M e. X )   =>    |- ( ph -> ( 1 ... (♯ ` X ) ) = ( ( 1 ... (♯ ` ( X \ { M } ) ) ) u. { (♯ ` X ) } ) )
Theorem	zfz1isolemiso 10774*	Lemma for zfz1iso 10776. Adding one element to the order isomorphism. (Contributed by Jim Kingdon, 8-Sep-2022.)
|- ( ph -> X e. Fin )   &    |- ( ph -> X C_ ZZ )   &    |- ( ph -> M e. X )   &    |- ( ph -> A. z e. X z <_ M )   &    |- ( ph -> G Isom < , < ( ( 1 ... (♯ ` ( X \ { M } ) ) ) , ( X \ { M } ) ) )   &    |- ( ph -> A e. ( 1 ... (♯ ` X ) ) )   &    |- ( ph -> B e. ( 1 ... (♯ ` X ) ) )   =>    |- ( ph -> ( A < B <-> ( ( G u. { <. (♯ ` X ) , M >. } ) ` A ) < ( ( G u. { <. (♯ ` X ) , M >. } ) ` B ) ) )
Theorem	zfz1isolem1 10775*	Lemma for zfz1iso 10776. Existence of an order isomorphism given the existence of shorter isomorphisms. (Contributed by Jim Kingdon, 7-Sep-2022.)
|- ( ph -> K e. om )   &    |- ( ph -> A. y ( ( ( y C_ ZZ /\ y e. Fin ) /\ y ~~ K ) -> E. f f Isom < , < ( ( 1 ... (♯ ` y ) ) , y ) ) )   &    |- ( ph -> X C_ ZZ )   &    |- ( ph -> X e. Fin )   &    |- ( ph -> X ~~ suc K )   &    |- ( ph -> M e. X )   &    |- ( ph -> A. z e. X z <_ M )   =>    |- ( ph -> E. f f Isom < , < ( ( 1 ... (♯ ` X ) ) , X ) )
Theorem	zfz1iso 10776*	A finite set of integers has an order isomorphism to a one-based finite sequence. (Contributed by Jim Kingdon, 3-Sep-2022.)
|- ( ( A C_ ZZ /\ A e. Fin ) -> E. f f Isom < , < ( ( 1 ... (♯ ` A ) ) , A ) )
Theorem	seq3coll 10777*	The function F contains a sparse set of nonzero values to be summed. The function G is an order isomorphism from the set of nonzero values of F to a 1-based finite sequence, and H collects these nonzero values together. Under these conditions, the sum over the values in H yields the same result as the sum over the original set F. (Contributed by Mario Carneiro, 2-Apr-2014.) (Revised by Jim Kingdon, 9-Apr-2023.)
|- ( ( ph /\ k e. S ) -> ( Z .+ k ) = k )   &    |- ( ( ph /\ k e. S ) -> ( k .+ Z ) = k )   &    |- ( ( ph /\ ( k e. S /\ n e. S ) ) -> ( k .+ n ) e. S )   &    |- ( ph -> Z e. S )   &    |- ( ph -> G Isom < , < ( ( 1 ... (♯ ` A ) ) , A ) )   &    |- ( ph -> N e. ( 1 ... (♯ ` A ) ) )   &    |- ( ph -> A C_ ( ZZ>= ` M ) )   &    |- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( F ` k ) e. S )   &    |- ( ( ph /\ k e. ( ZZ>= ` 1 ) ) -> ( H ` k ) e. S )   &    |- ( ( ph /\ k e. ( ( M ... ( G ` (♯ ` A ) ) ) \ A ) ) -> ( F ` k ) = Z )   &    |- ( ( ph /\ n e. ( 1 ... (♯ ` A ) ) ) -> ( H ` n ) = ( F ` ( G ` n ) ) )   =>    |- ( ph -> ( seq M ( .+ , F ) ` ( G ` N ) ) = ( seq 1 ( .+ , H ) ` N ) )
4.7  Elementary real and complex functions
4.7.1  The "shift" operation
Syntax	cshi 10778	Extend class notation with function shifter.
class shift
Definition	df-shft 10779*	Define a function shifter. This operation offsets the value argument of a function (ordinarily on a subset of CC) and produces a new function on CC. See shftval 10789 for its value. (Contributed by NM, 20-Jul-2005.)
|- shift = ( f e. _V , x e. CC |-> { <. y , z >. | ( y e. CC /\ ( y - x ) f z ) } )
Theorem	shftlem 10780*	Two ways to write a shifted set ( B + A ). (Contributed by Mario Carneiro, 3-Nov-2013.)
|- ( ( A e. CC /\ B C_ CC ) -> { x e. CC | ( x - A ) e. B } = { x | E. y e. B x = ( y + A ) } )
Theorem	shftuz 10781*	A shift of the upper integers. (Contributed by Mario Carneiro, 5-Nov-2013.)
|- ( ( A e. ZZ /\ B e. ZZ ) -> { x e. CC | ( x - A ) e. ( ZZ>= ` B ) } = ( ZZ>= ` ( B + A ) ) )
Theorem	shftfvalg 10782*	The value of the sequence shifter operation is a function on CC. A is ordinarily an integer. (Contributed by NM, 20-Jul-2005.) (Revised by Mario Carneiro, 3-Nov-2013.)
|- ( ( A e. CC /\ F e. V ) -> ( F shift A ) = { <. x , y >. | ( x e. CC /\ ( x - A ) F y ) } )
Theorem	ovshftex 10783	Existence of the result of applying shift. (Contributed by Jim Kingdon, 15-Aug-2021.)
|- ( ( F e. V /\ A e. CC ) -> ( F shift A ) e. _V )
Theorem	shftfibg 10784	Value of a fiber of the relation F. (Contributed by Jim Kingdon, 15-Aug-2021.)
|- ( ( F e. V /\ A e. CC /\ B e. CC ) -> ( ( F shift A ) " { B } ) = ( F " { ( B - A ) } ) )
Theorem	shftfval 10785*	The value of the sequence shifter operation is a function on CC. A is ordinarily an integer. (Contributed by NM, 20-Jul-2005.) (Revised by Mario Carneiro, 3-Nov-2013.)
|- F e. _V   =>    |- ( A e. CC -> ( F shift A ) = { <. x , y >. | ( x e. CC /\ ( x - A ) F y ) } )
Theorem	shftdm 10786*	Domain of a relation shifted by A. The set on the right is more commonly notated as ( dom F + A ) (meaning add A to every element of dom F). (Contributed by Mario Carneiro, 3-Nov-2013.)
|- F e. _V   =>    |- ( A e. CC -> dom ( F shift A ) = { x e. CC | ( x - A ) e. dom F } )
Theorem	shftfib 10787	Value of a fiber of the relation F. (Contributed by Mario Carneiro, 4-Nov-2013.)
|- F e. _V   =>    |- ( ( A e. CC /\ B e. CC ) -> ( ( F shift A ) " { B } ) = ( F " { ( B - A ) } ) )
Theorem	shftfn 10788*	Functionality and domain of a sequence shifted by A. (Contributed by NM, 20-Jul-2005.) (Revised by Mario Carneiro, 3-Nov-2013.)
|- F e. _V   =>    |- ( ( F Fn B /\ A e. CC ) -> ( F shift A ) Fn { x e. CC | ( x - A ) e. B } )
Theorem	shftval 10789	Value of a sequence shifted by A. (Contributed by NM, 20-Jul-2005.) (Revised by Mario Carneiro, 4-Nov-2013.)
|- F e. _V   =>    |- ( ( A e. CC /\ B e. CC ) -> ( ( F shift A ) ` B ) = ( F ` ( B - A ) ) )
Theorem	shftval2 10790	Value of a sequence shifted by A - B. (Contributed by NM, 20-Jul-2005.) (Revised by Mario Carneiro, 5-Nov-2013.)
|- F e. _V   =>    |- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( F shift ( A - B ) ) ` ( A + C ) ) = ( F ` ( B + C ) ) )
Theorem	shftval3 10791	Value of a sequence shifted by A - B. (Contributed by NM, 20-Jul-2005.)
|- F e. _V   =>    |- ( ( A e. CC /\ B e. CC ) -> ( ( F shift ( A - B ) ) ` A ) = ( F ` B ) )
Theorem	shftval4 10792	Value of a sequence shifted by -u A. (Contributed by NM, 18-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.)
|- F e. _V   =>    |- ( ( A e. CC /\ B e. CC ) -> ( ( F shift -u A ) ` B ) = ( F ` ( A + B ) ) )
Theorem	shftval5 10793	Value of a shifted sequence. (Contributed by NM, 19-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.)
|- F e. _V   =>    |- ( ( A e. CC /\ B e. CC ) -> ( ( F shift A ) ` ( B + A ) ) = ( F ` B ) )
Theorem	shftf 10794*	Functionality of a shifted sequence. (Contributed by NM, 19-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.)
|- F e. _V   =>    |- ( ( F : B --> C /\ A e. CC ) -> ( F shift A ) : { x e. CC | ( x - A ) e. B } --> C )
Theorem	2shfti 10795	Composite shift operations. (Contributed by NM, 19-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.)
|- F e. _V   =>    |- ( ( A e. CC /\ B e. CC ) -> ( ( F shift A ) shift B ) = ( F shift ( A + B ) ) )
Theorem	shftidt2 10796	Identity law for the shift operation. (Contributed by Mario Carneiro, 5-Nov-2013.)
|- F e. _V   =>    |- ( F shift 0 ) = ( F |` CC )
Theorem	shftidt 10797	Identity law for the shift operation. (Contributed by NM, 19-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.)
|- F e. _V   =>    |- ( A e. CC -> ( ( F shift 0 ) ` A ) = ( F ` A ) )
Theorem	shftcan1 10798	Cancellation law for the shift operation. (Contributed by NM, 4-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.)
|- F e. _V   =>    |- ( ( A e. CC /\ B e. CC ) -> ( ( ( F shift A ) shift -u A ) ` B ) = ( F ` B ) )
Theorem	shftcan2 10799	Cancellation law for the shift operation. (Contributed by NM, 4-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.)
|- F e. _V   =>    |- ( ( A e. CC /\ B e. CC ) -> ( ( ( F shift -u A ) shift A ) ` B ) = ( F ` B ) )
Theorem	shftvalg 10800	Value of a sequence shifted by A. (Contributed by Scott Fenton, 16-Dec-2017.)
|- ( ( F e. V /\ A e. CC /\ B e. CC ) -> ( ( F shift A ) ` B ) = ( F ` ( B - A ) ) )