P. 386 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 38501-38600   *Has distinct variable group(s)

Type	Label	Description
Statement
21.33.2.6  Predicate "defined at"
Theorem	dfateq12d 38501	Equality deduction for "defined at". (Contributed by Alexander van der Vekens, 26-May-2017.)
|- ( ph -> F = G )   &    |- ( ph -> A = B )   =>    |- ( ph -> ( F defAt A <-> G defAt B ) )
Theorem	nfdfat 38502	Bound-variable hypothesis builder for "defined at". To prove a deduction version of this theorem is not easily possible because many deduction versions for bound-variable hypothesis builder for constructs the definition of "defined at" is based on are not available (e.g. for Fun/Rel, dom, C_, etc.). (Contributed by Alexander van der Vekens, 26-May-2017.)
|- F/_ x F   &    |- F/_ x A   =>    |- F/ x F defAt A
Theorem	dfdfat2 38503*	Alternate definition of the predicate "defined at" not using the Fun predicate. (Contributed by Alexander van der Vekens, 22-Jul-2017.)
|- ( F defAt A <-> ( A e. dom F /\ E! y A F y ) )
21.33.2.7  Alternative definition of the value of a function
Theorem	dfafv2 38504	Alternative definition of ( F''' A ) using ( F ` A ) directly. (Contributed by Alexander van der Vekens, 22-Jul-2017.)
|- ( F''' A ) = if ( F defAt A , ( F ` A ) , _V )
Theorem	afveq12d 38505	Equality deduction for function value, analogous to fveq12d 5887. (Contributed by Alexander van der Vekens, 26-May-2017.)
|- ( ph -> F = G )   &    |- ( ph -> A = B )   =>    |- ( ph -> ( F''' A ) = ( G''' B ) )
Theorem	afveq1 38506	Equality theorem for function value, analogous to fveq1 5880. (Contributed by Alexander van der Vekens, 22-Jul-2017.)
|- ( F = G -> ( F''' A ) = ( G''' A ) )
Theorem	afveq2 38507	Equality theorem for function value, analogous to fveq1 5880. (Contributed by Alexander van der Vekens, 22-Jul-2017.)
|- ( A = B -> ( F''' A ) = ( F''' B ) )
Theorem	nfafv 38508	Bound-variable hypothesis builder for function value, analogous to nffv 5888. To prove a deduction version of this analogous to nffvd 5890 is not easily possible because a deduction version of nfdfat 38502 cannot be shown easily. (Contributed by Alexander van der Vekens, 26-May-2017.)
|- F/_ x F   &    |- F/_ x A   =>    |- F/_ x ( F''' A )
Theorem	csbafv12g 38509	Move class substitution in and out of a function value, analogous to csbfv12 5916, with a direct proof proposed by Mario Carneiro, analogous to csbov123 6339. (Contributed by Alexander van der Vekens, 23-Jul-2017.)
|- ( A e. V -> [_ A / x ]_ ( F''' B ) = ( [_ A / x ]_ F''' [_ A / x ]_ B ) )
Theorem	afvfundmfveq 38510	If a class is a function restricted to a member of its domain, then the function value for this member is equal for both definitions. (Contributed by Alexander van der Vekens, 25-May-2017.)
|- ( F defAt A -> ( F''' A ) = ( F ` A ) )
Theorem	afvnfundmuv 38511	If a set is not in the domain of a class or the class is not a function restricted to the set, then the function value for this set is the universe. (Contributed by Alexander van der Vekens, 26-May-2017.)
|- ( -. F defAt A -> ( F''' A ) = _V )
Theorem	ndmafv 38512	The value of a class outside its domain is the universe, compare with ndmfv 5905. (Contributed by Alexander van der Vekens, 25-May-2017.)
|- ( -. A e. dom F -> ( F''' A ) = _V )
Theorem	afvvdm 38513	If the function value of a class for an argument is a set, the argument is contained in the domain of the class. (Contributed by Alexander van der Vekens, 25-May-2017.)
|- ( ( F''' A ) e. B -> A e. dom F )
Theorem	nfunsnafv 38514	If the restriction of a class to a singleton is not a function, its value is the universe, compare with nfunsn 5912 (Contributed by Alexander van der Vekens, 25-May-2017.)
|- ( -. Fun ( F |` { A } ) -> ( F''' A ) = _V )
Theorem	afvvfunressn 38515	If the function value of a class for an argument is a set, the class restricted to the singleton of the argument is a function. (Contributed by Alexander van der Vekens, 25-May-2017.)
|- ( ( F''' A ) e. B -> Fun ( F |` { A } ) )
Theorem	afvprc 38516	A function's value at a proper class is the universe, compare with fvprc 5875. (Contributed by Alexander van der Vekens, 25-May-2017.)
|- ( -. A e. _V -> ( F''' A ) = _V )
Theorem	afvvv 38517	If a function's value at an argument is a set, the argument is also a set. (Contributed by Alexander van der Vekens, 25-May-2017.)
|- ( ( F''' A ) e. B -> A e. _V )
Theorem	afvpcfv0 38518	If the value of the alternative function at an argument is the universe, the function's value at this argument is the empty set. (Contributed by Alexander van der Vekens, 25-May-2017.)
|- ( ( F''' A ) = _V -> ( F ` A ) = (/) )
Theorem	afvnufveq 38519	The value of the alternative function at a set as argument equals the function's value at this argument. (Contributed by Alexander van der Vekens, 25-May-2017.)
|- ( ( F''' A ) =/= _V -> ( F''' A ) = ( F ` A ) )
Theorem	afvvfveq 38520	The value of the alternative function at a set as argument equals the function's value at this argument. (Contributed by Alexander van der Vekens, 25-May-2017.)
|- ( ( F''' A ) e. B -> ( F''' A ) = ( F ` A ) )
Theorem	afv0fv0 38521	If the value of the alternative function at an argument is the empty set, the function's value at this argument is the empty set. (Contributed by Alexander van der Vekens, 25-May-2017.)
|- ( ( F''' A ) = (/) -> ( F ` A ) = (/) )
Theorem	afvfvn0fveq 38522	If the function's value at an argument is not the empty set, it equals the value of the alternative function at this argument. (Contributed by Alexander van der Vekens, 25-May-2017.)
|- ( ( F ` A ) =/= (/) -> ( F''' A ) = ( F ` A ) )
Theorem	afv0nbfvbi 38523	The function's value at an argument is an element of a set if and only if the value of the alternative function at this argument is an element of that set, if the set does not contain the empty set. (Contributed by Alexander van der Vekens, 25-May-2017.)
|- ( (/) e/ B -> ( ( F''' A ) e. B <-> ( F ` A ) e. B ) )
Theorem	afvfv0bi 38524	The function's value at an argument is the empty set if and only if the value of the alternative function at this argument is either the empty set or the universe. (Contributed by Alexander van der Vekens, 25-May-2017.)
|- ( ( F ` A ) = (/) <-> ( ( F''' A ) = (/) \/ ( F''' A ) = _V ) )
Theorem	afveu 38525*	The value of a function at a unique point, analogous to fveu 5873. (Contributed by Alexander van der Vekens, 29-Nov-2017.)
|- ( E! x A F x -> ( F''' A ) = U. { x | A F x } )
Theorem	fnbrafvb 38526	Equivalence of function value and binary relation, analogous to fnbrfvb 5921. (Contributed by Alexander van der Vekens, 25-May-2017.)
|- ( ( F Fn A /\ B e. A ) -> ( ( F''' B ) = C <-> B F C ) )
Theorem	fnopafvb 38527	Equivalence of function value and ordered pair membership, analogous to fnopfvb 5922. (Contributed by Alexander van der Vekens, 25-May-2017.)
|- ( ( F Fn A /\ B e. A ) -> ( ( F''' B ) = C <-> <. B , C >. e. F ) )
Theorem	funbrafvb 38528	Equivalence of function value and binary relation, analogous to funbrfvb 5923. (Contributed by Alexander van der Vekens, 25-May-2017.)
|- ( ( Fun F /\ A e. dom F ) -> ( ( F''' A ) = B <-> A F B ) )
Theorem	funopafvb 38529	Equivalence of function value and ordered pair membership, analogous to funopfvb 5924. (Contributed by Alexander van der Vekens, 25-May-2017.)
|- ( ( Fun F /\ A e. dom F ) -> ( ( F''' A ) = B <-> <. A , B >. e. F ) )
Theorem	funbrafv 38530	The second argument of a binary relation on a function is the function's value, analogous to funbrfv 5919. (Contributed by Alexander van der Vekens, 25-May-2017.)
|- ( Fun F -> ( A F B -> ( F''' A ) = B ) )
Theorem	funbrafv2b 38531	Function value in terms of a binary relation, analogous to funbrfv2b 5925. (Contributed by Alexander van der Vekens, 25-May-2017.)
|- ( Fun F -> ( A F B <-> ( A e. dom F /\ ( F''' A ) = B ) ) )
Theorem	dfafn5a 38532*	Representation of a function in terms of its values, analogous to dffn5 5926 (only one direction of implication!). (Contributed by Alexander van der Vekens, 25-May-2017.)
|- ( F Fn A -> F = ( x e. A |-> ( F''' x ) ) )
Theorem	dfafn5b 38533*	Representation of a function in terms of its values, analogous to dffn5 5926 (only if it is assumed that the function value for each x is a set). (Contributed by Alexander van der Vekens, 25-May-2017.)
|- ( A. x e. A ( F''' x ) e. V -> ( F Fn A <-> F = ( x e. A |-> ( F''' x ) ) ) )
Theorem	fnrnafv 38534*	The range of a function expressed as a collection of the function's values, analogous to fnrnfv 5927. (Contributed by Alexander van der Vekens, 25-May-2017.)
|- ( F Fn A -> ran F = { y | E. x e. A y = ( F''' x ) } )
Theorem	afvelrnb 38535*	A member of a function's range is a value of the function, analogous to fvelrnb 5928 with the additional requirement that the member must be a set. (Contributed by Alexander van der Vekens, 25-May-2017.)
|- ( ( F Fn A /\ B e. V ) -> ( B e. ran F <-> E. x e. A ( F''' x ) = B ) )
Theorem	afvelrnb0 38536*	A member of a function's range is a value of the function, only one direction of implication of fvelrnb 5928. (Contributed by Alexander van der Vekens, 1-Jun-2017.)
|- ( F Fn A -> ( B e. ran F -> E. x e. A ( F''' x ) = B ) )
Theorem	dfaimafn 38537*	Alternate definition of the image of a function, analogous to dfimafn 5930. (Contributed by Alexander van der Vekens, 25-May-2017.)
|- ( ( Fun F /\ A C_ dom F ) -> ( F " A ) = { y | E. x e. A ( F''' x ) = y } )
Theorem	dfaimafn2 38538*	Alternate definition of the image of a function as an indexed union of singletons of function values, analogous to dfimafn2 5931. (Contributed by Alexander van der Vekens, 25-May-2017.)
|- ( ( Fun F /\ A C_ dom F ) -> ( F " A ) = U_ x e. A { ( F''' x ) } )
Theorem	afvelima 38539*	Function value in an image, analogous to fvelima 5933. (Contributed by Alexander van der Vekens, 25-May-2017.)
|- ( ( Fun F /\ A e. ( F " B ) ) -> E. x e. B ( F''' x ) = A )
Theorem	afvelrn 38540	A function's value belongs to its range, analogous to fvelrn 6030. (Contributed by Alexander van der Vekens, 25-May-2017.)
|- ( ( Fun F /\ A e. dom F ) -> ( F''' A ) e. ran F )
Theorem	fnafvelrn 38541	A function's value belongs to its range, analogous to fnfvelrn 6034. (Contributed by Alexander van der Vekens, 25-May-2017.)
|- ( ( F Fn A /\ B e. A ) -> ( F''' B ) e. ran F )
Theorem	fafvelrn 38542	A function's value belongs to its codomain, analogous to ffvelrn 6035. (Contributed by Alexander van der Vekens, 25-May-2017.)
|- ( ( F : A --> B /\ C e. A ) -> ( F''' C ) e. B )
Theorem	ffnafv 38543*	A function maps to a class to which all values belong, analogous to ffnfv 6064. (Contributed by Alexander van der Vekens, 25-May-2017.)
|- ( F : A --> B <-> ( F Fn A /\ A. x e. A ( F''' x ) e. B ) )
Theorem	afvres 38544	The value of a restricted function, analogous to fvres 5895. (Contributed by Alexander van der Vekens, 22-Jul-2017.)
|- ( A e. B -> ( ( F |` B )''' A ) = ( F''' A ) )
Theorem	tz6.12-afv 38545*	Function value. Theorem 6.12(1) of [TakeutiZaring] p. 27, analogous to tz6.12 5898. (Contributed by Alexander van der Vekens, 29-Nov-2017.)
|- ( ( <. A , y >. e. F /\ E! y <. A , y >. e. F ) -> ( F''' A ) = y )
Theorem	tz6.12-1-afv 38546*	Function value (Theorem 6.12(1) of [TakeutiZaring] p. 27, analogous to tz6.12-1 5897. (Contributed by Alexander van der Vekens, 29-Nov-2017.)
|- ( ( A F y /\ E! y A F y ) -> ( F''' A ) = y )
Theorem	dmfcoafv 38547	Domains of a function composition, analogous to dmfco 5955. (Contributed by Alexander van der Vekens, 23-Jul-2017.)
|- ( ( Fun G /\ A e. dom G ) -> ( A e. dom ( F o. G ) <-> ( G''' A ) e. dom F ) )
Theorem	afvco2 38548	Value of a function composition, analogous to fvco2 5956. (Contributed by Alexander van der Vekens, 23-Jul-2017.)
|- ( ( G Fn A /\ X e. A ) -> ( ( F o. G )''' X ) = ( F''' ( G''' X ) ) )
Theorem	rlimdmafv 38549	Two ways to express that a function has a limit, analogous to rlimdm 13614. (Contributed by Alexander van der Vekens, 27-Nov-2017.)
|- ( ph -> F : A --> CC )   &    |- ( ph -> sup ( A , RR* , < ) = +oo )   =>    |- ( ph -> ( F e. dom ~~> r <-> F ~~> r ( ~~> r ''' F ) ) )
21.33.2.8  Alternative definition of the value of an operation
Theorem	aoveq123d 38550	Equality deduction for operation value, analogous to oveq123d 6326. (Contributed by Alexander van der Vekens, 26-May-2017.)
|- ( ph -> F = G )   &    |- ( ph -> A = B )   &    |- ( ph -> C = D )   =>    |- ( ph -> (( A F C)) = (( B G D)) )
Theorem	nfaov 38551	Bound-variable hypothesis builder for operation value, analogous to nfov 6331. To prove a deduction version of this analogous to nfovd 6330 is not quickly possible because many deduction versions for bound-variable hypothesis builder for constructs the definition of alternative operation values is based on are not available (see nfafv 38508). (Contributed by Alexander van der Vekens, 26-May-2017.)
|- F/_ x A   &    |- F/_ x F   &    |- F/_ x B   =>    |- F/_ x (( A F B))
Theorem	csbaovg 38552	Move class substitution in and out of an operation. (Contributed by Alexander van der Vekens, 26-May-2017.)
|- ( A e. D -> [_ A / x ]_ (( B F C)) = (( [_ A / x ]_ B [_ A / x ]_ F [_ A / x ]_ C)) )
Theorem	aovfundmoveq 38553	If a class is a function restricted to an ordered pair of its domain, then the value of the operation on this pair is equal for both definitions. (Contributed by Alexander van der Vekens, 26-May-2017.)
|- ( F defAt <. A , B >. -> (( A F B)) = ( A F B ) )
Theorem	aovnfundmuv 38554	If an ordered pair is not in the domain of a class or the class is not a function restricted to the ordered pair, then the operation value for this pair is the universal class. (Contributed by Alexander van der Vekens, 26-May-2017.)
|- ( -. F defAt <. A , B >. -> (( A F B)) = _V )
Theorem	ndmaov 38555	The value of an operation outside its domain, analogous to ndmafv 38512. (Contributed by Alexander van der Vekens, 26-May-2017.)
|- ( -. <. A , B >. e. dom F -> (( A F B)) = _V )
Theorem	ndmaovg 38556	The value of an operation outside its domain, analogous to ndmovg 6466. (Contributed by Alexander van der Vekens, 26-May-2017.)
|- ( ( dom F = ( R X. S ) /\ -. ( A e. R /\ B e. S ) ) -> (( A F B)) = _V )
Theorem	aovvdm 38557	If the operation value of a class for an ordered pair is a set, the ordered pair is contained in the domain of the class. (Contributed by Alexander van der Vekens, 26-May-2017.)
|- ( (( A F B)) e. C -> <. A , B >. e. dom F )
Theorem	nfunsnaov 38558	If the restriction of a class to a singleton is not a function, its operation value is the universal class. (Contributed by Alexander van der Vekens, 26-May-2017.)
|- ( -. Fun ( F |` { <. A , B >. } ) -> (( A F B)) = _V )
Theorem	aovvfunressn 38559	If the operation value of a class for an argument is a set, the class restricted to the singleton of the argument is a function. (Contributed by Alexander van der Vekens, 26-May-2017.)
|- ( (( A F B)) e. C -> Fun ( F |` { <. A , B >. } ) )
Theorem	aovprc 38560	The value of an operation when the one of the arguments is a proper class, analogous to ovprc 6335. (Contributed by Alexander van der Vekens, 26-May-2017.)
|- Rel dom F   =>    |- ( -. ( A e. _V /\ B e. _V ) -> (( A F B)) = _V )
Theorem	aovrcl 38561	Reverse closure for an operation value, analogous to afvvv 38517. In contrast to ovrcl 6338, elementhood of the operation's value in a set is required, not containing an element. (Contributed by Alexander van der Vekens, 26-May-2017.)
|- Rel dom F   =>    |- ( (( A F B)) e. C -> ( A e. _V /\ B e. _V ) )
Theorem	aovpcov0 38562	If the alternative value of the operation on an ordered pair is the universal class, the operation's value at this ordered pair is the empty set. (Contributed by Alexander van der Vekens, 26-May-2017.)
|- ( (( A F B)) = _V -> ( A F B ) = (/) )
Theorem	aovnuoveq 38563	The alternative value of the operation on an ordered pair equals the operation's value at this ordered pair. (Contributed by Alexander van der Vekens, 26-May-2017.)
|- ( (( A F B)) =/= _V -> (( A F B)) = ( A F B ) )
Theorem	aovvoveq 38564	The alternative value of the operation on an ordered pair equals the operation's value on this ordered pair. (Contributed by Alexander van der Vekens, 26-May-2017.)
|- ( (( A F B)) e. C -> (( A F B)) = ( A F B ) )
Theorem	aov0ov0 38565	If the alternative value of the operation on an ordered pair is the empty set, the operation's value at this ordered pair is the empty set. (Contributed by Alexander van der Vekens, 26-May-2017.)
|- ( (( A F B)) = (/) -> ( A F B ) = (/) )
Theorem	aovovn0oveq 38566	If the operation's value at an argument is not the empty set, it equals the value of the alternative operation at this argument. (Contributed by Alexander van der Vekens, 26-May-2017.)
|- ( ( A F B ) =/= (/) -> (( A F B)) = ( A F B ) )
Theorem	aov0nbovbi 38567	The operation's value on an ordered pair is an element of a set if and only if the alternative value of the operation on this ordered pair is an element of that set, if the set does not contain the empty set. (Contributed by Alexander van der Vekens, 26-May-2017.)
|- ( (/) e/ C -> ( (( A F B)) e. C <-> ( A F B ) e. C ) )
Theorem	aovov0bi 38568	The operation's value on an ordered pair is the empty set if and only if the alternative value of the operation on this ordered pair is either the empty set or the universal class. (Contributed by Alexander van der Vekens, 26-May-2017.)
|- ( ( A F B ) = (/) <-> ( (( A F B)) = (/) \/ (( A F B)) = _V ) )
Theorem	rspceaov 38569*	A frequently used special case of rspc2ev 3193 for operation values, analogous to rspceov 6344. (Contributed by Alexander van der Vekens, 26-May-2017.)
|- ( ( C e. A /\ D e. B /\ S = (( C F D)) ) -> E. x e. A E. y e. B S = (( x F y)) )
Theorem	fnotaovb 38570	Equivalence of operation value and ordered triple membership, analogous to fnopfvb 5922. (Contributed by Alexander van der Vekens, 26-May-2017.)
|- ( ( F Fn ( A X. B ) /\ C e. A /\ D e. B ) -> ( (( C F D)) = R <-> <. C , D , R >. e. F ) )
Theorem	ffnaov 38571*	An operation maps to a class to which all values belong, analogous to ffnov 6414. (Contributed by Alexander van der Vekens, 26-May-2017.)
|- ( F : ( A X. B ) --> C <-> ( F Fn ( A X. B ) /\ A. x e. A A. y e. B (( x F y)) e. C ) )
Theorem	faovcl 38572	Closure law for an operation, analogous to fovcl 6415. (Contributed by Alexander van der Vekens, 26-May-2017.)
|- F : ( R X. S ) --> C   =>    |- ( ( A e. R /\ B e. S ) -> (( A F B)) e. C )
Theorem	aovmpt4g 38573*	Value of a function given by the "maps to" notation, analogous to ovmpt4g 6433. (Contributed by Alexander van der Vekens, 26-May-2017.)
|- F = ( x e. A , y e. B |-> C )   =>    |- ( ( x e. A /\ y e. B /\ C e. V ) -> (( x F y)) = C )
Theorem	aoprssdm 38574*	Domain of closure of an operation. In contrast to oprssdm 6464, no additional property for S ( -. (/) e. S) is required! (Contributed by Alexander van der Vekens, 26-May-2017.)
|- ( ( x e. S /\ y e. S ) -> (( x F y)) e. S )   =>    |- ( S X. S ) C_ dom F
Theorem	ndmaovcl 38575	The "closure" of an operation outside its domain, when the operation's value is a set in contrast to ndmovcl 6468 where it is required that the domain contains the empty set ( (/) e. S). (Contributed by Alexander van der Vekens, 26-May-2017.)
|- dom F = ( S X. S )   &    |- ( ( A e. S /\ B e. S ) -> (( A F B)) e. S )   &    |- (( A F B)) e. _V   =>    |- (( A F B)) e. S
Theorem	ndmaovrcl 38576	Reverse closure law, in contrast to ndmovrcl 6469 where it is required that the operation's domain doesn't contain the empty set ( -. (/) e. S), no additional asumption is required. (Contributed by Alexander van der Vekens, 26-May-2017.)
|- dom F = ( S X. S )   =>    |- ( (( A F B)) e. S -> ( A e. S /\ B e. S ) )
Theorem	ndmaovcom 38577	Any operation is commutative outside its domain, analogous to ndmovcom 6470. (Contributed by Alexander van der Vekens, 26-May-2017.)
|- dom F = ( S X. S )   =>    |- ( -. ( A e. S /\ B e. S ) -> (( A F B)) = (( B F A)) )
Theorem	ndmaovass 38578	Any operation is associative outside its domain. In contrast to ndmovass 6471 where it is required that the operation's domain doesn't contain the empty set ( -. (/) e. S), no additional assumption is required. (Contributed by Alexander van der Vekens, 26-May-2017.)
|- dom F = ( S X. S )   =>    |- ( -. ( A e. S /\ B e. S /\ C e. S ) -> (( (( A F B)) F C)) = (( A F (( B F C)) )) )
Theorem	ndmaovdistr 38579	Any operation is distributive outside its domain. In contrast to ndmovdistr 6472 where it is required that the operation's domain doesn't contain the empty set ( -. (/) e. S), no additional assumption is required. (Contributed by Alexander van der Vekens, 26-May-2017.)
|- dom F = ( S X. S )   &    |- dom G = ( S X. S )   =>    |- ( -. ( A e. S /\ B e. S /\ C e. S ) -> (( A G (( B F C)) )) = (( (( A G B)) F (( A G C)) )) )
21.33.3  General auxiliary theorems
21.33.3.1  Miscellanea
Theorem	1t10e1p1e11 38580	11 is 1 times 10 to the power of 1, plus 1. (Contributed by AV, 4-Aug-2020.)
|- ; 1 1 = ( ( 1 x. ( 10 ^ 1 ) ) + 1 )
Theorem	xp1d2m1eqxm1d2 38581	A complex number increased by 1, then divided by 2, then decreased by 1 equals the complex number decreased by 1 and then divided by 2. (Contributed by AV, 24-May-2020.)
|- ( X e. CC -> ( ( ( X + 1 ) / 2 ) - 1 ) = ( ( X - 1 ) / 2 ) )
Theorem	elprneb 38582	An element of a proper unordered pair is the first element iff it is not the second element. (Contributed by AV, 18-Jun-2020.)
|- ( ( A e. { B , C } /\ B =/= C ) -> ( A = B <-> A =/= C ) )
Theorem	halfge0 38583	One-half is not negative. (Contributed by AV, 7-Jun-2020.)
|- 0 <_ ( 1 / 2 )
Theorem	leltletr 38584	Transitive law, weaker form of lelttr 9731. (Contributed by AV, 14-Oct-2018.)
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A <_ B /\ B < C ) -> A <_ C ) )
Theorem	deccarry 38585	Add 1 to a 2 digit number with carry. This is a special case of decsucc 11085, but in closed form. As observed by ML, this theorem allows for carrying the 1 down multiple decimal constructors, so we can carry the 1 multiple times down a multi-digit number, e.g. by applying this theorem three times we get (;; 9 9 9 + 1 ) = ;;; 1 0 0 0. (Contributed by AV, 4-Aug-2020.) (Revised by ML, 8-Aug-2020.)
|- ( A e. NN -> (; A 9 + 1 ) = ; ( A + 1 ) 0 )
Theorem	nltle2tri 38586	Negated extended trichotomy law for 'less than' and 'less than or equal to'. (Contributed by AV, 18-Jul-2020.)
|- ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> -. ( A < B /\ B <_ C /\ C <_ A ) )
Theorem	zgeltp1eq 38587	If an integer is between another integer and its successor, the integer is equal to the other integer. (Contributed by AV, 30-May-2020.)
|- ( ( I e. ZZ /\ A e. ZZ ) -> ( ( A <_ I /\ I < ( A + 1 ) ) -> I = A ) )
Theorem	smonoord 38588*	Ordering relation for a strictly monotonic sequence, increasing case. Analogous to monoord 12249 (except that the case M = N must be excluded). Duplicate of monoords 37468? (Contributed by AV, 12-Jul-2020.)
|- ( ph -> M e. ZZ )   &    |- ( ph -> N e. ( ZZ>= ` ( M + 1 ) ) )   &    |- ( ( ph /\ k e. ( M ... N ) ) -> ( F ` k ) e. RR )   &    |- ( ( ph /\ k e. ( M ... ( N - 1 ) ) ) -> ( F ` k ) < ( F ` ( k + 1 ) ) )   =>    |- ( ph -> ( F ` M ) < ( F ` N ) )
Theorem	fzopred 38589	Join a predecessor to the beginning of an open integer interval. Generalization of fzo0sn0fzo1 12007. (Contributed by AV, 14-Jul-2020.)
|- ( ( M e. ZZ /\ N e. ZZ /\ M < N ) -> ( M..^ N ) = ( { M } u. ( ( M + 1 )..^ N ) ) )
Theorem	fzopredsuc 38590	Join a predecessor and a successor to the beginning and the end of an open integer interval. This theorem holds even if N = M (then ( M ... N ) = { M } = ( { M } u. (/) ) u. { M } ). (Contributed by AV, 14-Jul-2020.)
|- ( N e. ( ZZ>= ` M ) -> ( M ... N ) = ( ( { M } u. ( ( M + 1 )..^ N ) ) u. { N } ) )
Theorem	1fzopredsuc 38591	Join 0 and a successor to the beginning and the end of an open integer interval starting at 1. (Contributed by AV, 14-Jul-2020.)
|- ( N e. NN0 -> ( 0 ... N ) = ( ( { 0 } u. ( 1..^ N ) ) u. { N } ) )
Theorem	el1fzopredsuc 38592	An element of an open integer interval starting at 1 joined by 0 and a successor at the beginning and the end is either 0 or an element of the open integer interval or the successor. (Contributed by AV, 14-Jul-2020.)
|- ( N e. NN0 -> ( I e. ( 0 ... N ) <-> ( I = 0 \/ I e. ( 1..^ N ) \/ I = N ) ) )
21.33.3.2  The modulo (remainder) operation (extension)
Theorem	m1mod0mod1 38593	An integer decreased by 1 is 0 modulo a positive integer iff the integer is 1 modulo the same modulus. (Contributed by AV, 6-Jun-2020.)
|- ( ( A e. RR /\ N e. RR /\ 1 < N ) -> ( ( ( A - 1 ) mod N ) = 0 <-> ( A mod N ) = 1 ) )
Theorem	elmod2 38594	An integer modulo 2 is either 0 or 1. (Contributed by AV, 24-May-2020.) (Proof shortened by OpenAI, 3-Jul-2020.)
|- ( N e. ZZ -> ( N mod 2 ) e. { 0 , 1 } )
Theorem	mod2eq1n2dvds 38595	An integer is 1 modulo 2 iff it is not divisible by 2. (Contributed by AV, 24-May-2020.) (Proof shortened by AV, 5-Jul-2020.)
|- ( N e. ZZ -> ( ( N mod 2 ) = 1 <-> -. 2 || N ) )
Theorem	elmod2OLD 38596	An integer modulo 2 is either 0 or 1. (Contributed by AV, 24-May-2020.) Obsolete version of elmod2 38594 as of 3-Jul-2020. (New usage is discouraged.) (Proof modification is discouraged.)
|- ( N e. ZZ -> ( N mod 2 ) e. { 0 , 1 } )
21.33.3.3  Partitions of real intervals Based on the theorems of the fourierdlem* series of GS's mathbox
Syntax	ciccp 38597	Extend class notation with the partitions of a closed interval of extended reals.
class RePart
Definition	df-iccp 38598*	Define partitions of a closed interval of extended reals. Such partitions are finite increasing sequences of extended reals. (Contributed by AV, 8-Jul-2020.)
|- RePart = ( m e. NN |-> { p e. ( RR* ^m ( 0 ... m ) ) | A. i e. ( 0..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) } )
Theorem	iccpval 38599*	Partition consisting of a fixed number M of parts. (Contributed by AV, 9-Jul-2020.)
|- ( M e. NN -> (RePart ` M ) = { p e. ( RR* ^m ( 0 ... M ) ) | A. i e. ( 0..^ M ) ( p ` i ) < ( p ` ( i + 1 ) ) } )
Theorem	iccpart 38600*	A special partition. Corresponds to fourierdlem2 37911 in GS's mathbox. (Contributed by AV, 9-Jul-2020.)
|- ( M e. NN -> ( P e. (RePart ` M ) <-> ( P e. ( RR* ^m ( 0 ... M ) ) /\ A. i e. ( 0..^ M ) ( P ` i ) < ( P ` ( i + 1 ) ) ) ) )