P. 376 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 37501-37600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	f1oeq2d 37501	Equality deduction for one-to-one onto functions. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> A = B )   =>    |- ( ph -> ( F : A -1-1-onto-> C <-> F : B -1-1-onto-> C ) )
Theorem	rnresun 37502	Distribution law for range of a restriction over a union. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ran ( F |` ( A u. B ) ) = ( ran ( F |` A ) u. ran ( F |` B ) )
Theorem	f1oeq1d 37503	Equality deduction for one-to-one onto functions. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> F = G )   =>    |- ( ph -> ( F : A -1-1-onto-> B <-> G : A -1-1-onto-> B ) )
Theorem	dffo3f 37504*	An onto mapping expressed in terms of function values. As dffo3 6065 but with less disjoint vars constraints. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- F/_ x F   =>    |- ( F : A -onto-> B <-> ( F : A --> B /\ A. y e. B E. x e. A y = ( F ` x ) ) )
Theorem	rnresss 37505	The range of a restriction is a subset of the whole range. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ran ( A |` B ) C_ ran A
Theorem	mpteq1i 37506*	An equality theorem for the maps to notation. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- A = B   =>    |- ( x e. A |-> C ) = ( x e. B |-> C )
Theorem	elrnmptd 37507*	The range of a function in maps-to notation. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- F = ( x e. A |-> B )   &    |- ( ph -> E. x e. A C = B )   &    |- ( ph -> C e. V )   =>    |- ( ph -> C e. ran F )
Theorem	elrnmptf 37508	The range of a function in maps-to notation. Same as elrnmpt 5103, but using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- F/_ x C   &    |- F = ( x e. A |-> B )   =>    |- ( C e. V -> ( C e. ran F <-> E. x e. A C = B ) )
Theorem	mptss 37509*	Sufficient condition for inclusion in map-to notation. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( A C_ B -> ( x e. A |-> C ) C_ ( x e. B |-> C ) )
Theorem	rnmptssrn 37510*	Inclusion relation for two ranges expressed in map-to notation. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ( ph /\ x e. A ) -> B e. V )   &    |- ( ( ph /\ x e. A ) -> E. y e. C B = D )   =>    |- ( ph -> ran ( x e. A |-> B ) C_ ran ( y e. C |-> D ) )
Theorem	disjf1 37511*	A 1 to 1 mapping built from disjoint, nonempty sets . (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- F/ x ph   &    |- F = ( x e. A |-> B )   &    |- ( ( ph /\ x e. A ) -> B e. V )   &    |- ( ( ph /\ x e. A ) -> B =/= (/) )   &    |- ( ph -> Disj x e. A B )   =>    |- ( ph -> F : A -1-1-> V )
Theorem	rnsnf 37512	The range of a function whose domain is a singleton. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> A e. V )   &    |- ( ph -> F : { A } --> B )   =>    |- ( ph -> ran F = { ( F ` A ) } )
Theorem	wessf1ornlem 37513*	Given a function F on a well ordered domain A there exists a subset of A such that F restricted to such subset is injective and onto the range of F (without using the axiom of choice). (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> F Fn A )   &    |- ( ph -> A e. V )   &    |- ( ph -> R We A )   &    |- G = ( y e. ran F |-> ( iota_ x e. ( `' F " { y } ) A. z e. ( `' F " { y } ) -. z R x ) )   =>    |- ( ph -> E. x e. ~P A ( F |` x ) : x -1-1-onto-> ran F )
Theorem	wessf1orn 37514*	Given a function F on a well ordered domain A there exists a subset of A such that F restricted to such subset is injective and onto the range of F (without using the axiom of choice). (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> F Fn A )   &    |- ( ph -> A e. V )   &    |- ( ph -> R We A )   =>    |- ( ph -> E. x e. ~P A ( F |` x ) : x -1-1-onto-> ran F )
Theorem	foelrnf 37515*	Property of a surjective function. As foelrn 6069 but with less disjoint vars constraints. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- F/_ x F   =>    |- ( ( F : A -onto-> B /\ C e. B ) -> E. x e. A C = ( F ` x ) )
Theorem	nelrnres 37516	If A is not in the range, it is not in the range of any restriction. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( -. A e. ran B -> -. A e. ran ( B |` C ) )
Theorem	disjrnmpt2 37517*	Disjointness of the range of a function in map-to notation. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- F = ( x e. A |-> B )   =>    |- (Disj x e. A B -> Disj y e. ran F y )
Theorem	elrnmpt1sf 37518*	Elementhood in an image set. Same as elrnmpt1s 5104, but using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- F/_ x C   &    |- F = ( x e. A |-> B )   &    |- ( x = D -> B = C )   =>    |- ( ( D e. A /\ C e. V ) -> C e. ran F )
Theorem	founiiun0 37519*	Union expressed as an indexed union, when a map onto is given. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( F : A -onto-> ( B u. { (/) } ) -> U. B = U_ x e. A ( F ` x ) )
Theorem	disjf1o 37520*	A bijection built from disjoint sets. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- F/ x ph   &    |- F = ( x e. A |-> B )   &    |- ( ( ph /\ x e. A ) -> B e. V )   &    |- ( ph -> Disj x e. A B )   &    |- C = { x e. A | B =/= (/) }   &    |- D = ( ran F \ { (/) } )   =>    |- ( ph -> ( F |` C ) : C -1-1-onto-> D )
Theorem	fompt 37521*	Express being onto for a mapping operation. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- F = ( x e. A |-> C )   =>    |- ( F : A -onto-> B <-> ( A. x e. A C e. B /\ A. y e. B E. x e. A y = C ) )
Theorem	disjinfi 37522*	Only a finite number of disjoint sets can have a non empty intersection with a finite set C (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ( ph /\ x e. A ) -> B e. V )   &    |- ( ph -> Disj x e. A B )   &    |- ( ph -> C e. Fin )   =>    |- ( ph -> { x e. A | ( B i^i C ) =/= (/) } e. Fin )
Theorem	fvovco 37523	Value of the composition of an operator, with a given function. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
|- ( ph -> F : X --> ( V X. W ) )   &    |- ( ph -> Y e. X )   =>    |- ( ph -> ( ( O o. F ) ` Y ) = ( ( 1st ` ( F ` Y ) ) O ( 2nd ` ( F ` Y ) ) ) )
Theorem	ssnnf1octb 37524*	There exists a bijection between a subset of NN and a given nonempty countable set. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
|- ( ( A ~<_ om /\ A =/= (/) ) -> E. f ( dom f C_ NN /\ f : dom f -1-1-onto-> A ) )
Theorem	mapdm0 37525	The empty set is the only map with empty domain. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
|- ( A e. V -> ( A ^m (/) ) = { (/) } )
Theorem	nnf1oxpnn 37526	There is a bijection between the set of positive integers and the Cartesian product of the set of positive integers with itself. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
|- E. f f : NN -1-1-onto-> ( NN X. NN )
Theorem	rnmptssd 37527*	The range of an operation given by the "maps to" notation as a subset. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
|- F/ x ph   &    |- F = ( x e. A |-> B )   &    |- ( ( ph /\ x e. A ) -> B e. C )   =>    |- ( ph -> ran F C_ C )
Theorem	projf1o 37528*	A biijection from a set to a projection in a two dimensional space. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
|- ( ph -> A e. V )   &    |- F = ( x e. B |-> <. A , x >. )   =>    |- ( ph -> F : B -1-1-onto-> ( { A } X. B ) )
Theorem	fvmap 37529	Function value for a member of a set exponentiation. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
|- ( ph -> A e. V )   &    |- ( ph -> B e. W )   &    |- ( ph -> F e. ( A ^m B ) )   &    |- ( ph -> C e. B )   =>    |- ( ph -> ( F ` C ) e. A )
Theorem	mapsnd 37530*	The value of set exponentiation with a singleton exponent. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
|- ( ph -> A e. V )   &    |- ( ph -> B e. W )   =>    |- ( ph -> ( A ^m { B } ) = { f | E. y e. A f = { <. B , y >. } } )
Theorem	mptexd 37531*	If the domain of a function given by maps-to notation is a set, the function is a set. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
|- ( ph -> A e. V )   =>    |- ( ph -> ( x e. A |-> B ) e. _V )
Theorem	fvixp2 37532*	Projection of a factor of an indexed Cartesian product. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
|- ( ( F e. X_ x e. A B /\ x e. A ) -> ( F ` x ) e. B )
Theorem	fidmfisupp 37533	A function with a finite domain is finitely supported. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
|- ( ph -> F : D --> R )   &    |- ( ph -> D e. Fin )   &    |- ( ph -> Z e. V )   =>    |- ( ph -> F finSupp Z )
Theorem	mapsnend 37534	Set exponentiation to a singleton exponent is equinumerous to its base. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
|- ( ph -> A e. V )   &    |- ( ph -> B e. W )   =>    |- ( ph -> ( A ^m { B } ) ~~ A )
Theorem	choicefi 37535*	For a finite set, a choice function exists, without using the axiom of choice. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
|- ( ph -> A e. Fin )   &    |- ( ( ph /\ x e. A ) -> B e. W )   &    |- ( ( ph /\ x e. A ) -> B =/= (/) )   =>    |- ( ph -> E. f ( f Fn A /\ A. x e. A ( f ` x ) e. B ) )
Theorem	mpct 37536	The exponentiation of a countable set to a finite set is countable. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
|- ( ph -> A ~<_ om )   &    |- ( ph -> B e. Fin )   =>    |- ( ph -> ( A ^m B ) ~<_ om )
Theorem	cnmetcoval 37537	Value of the distance function of the metric space of complex numbers, composed with a function. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
|- D = ( abs o. - )   &    |- ( ph -> F : A --> ( CC X. CC ) )   &    |- ( ph -> B e. A )   =>    |- ( ph -> ( ( D o. F ) ` B ) = ( abs ` ( ( 1st ` ( F ` B ) ) - ( 2nd ` ( F ` B ) ) ) ) )
Theorem	fcomptss 37538*	Express composition of two functions as a maps-to applying both in sequence. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
|- ( ph -> F : A --> B )   &    |- ( ph -> B C_ C )   &    |- ( ph -> G : C --> D )   =>    |- ( ph -> ( G o. F ) = ( x e. A |-> ( G ` ( F ` x ) ) ) )
Theorem	elmapsnd 37539	Membership in a set exponentiated to a singleton. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
|- ( ph -> F Fn { A } )   &    |- ( ph -> B e. V )   &    |- ( ph -> ( F ` A ) e. B )   =>    |- ( ph -> F e. ( B ^m { A } ) )
Theorem	mapss2 37540	Subset inheritance for set exponentiation. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
|- ( ph -> A e. V )   &    |- ( ph -> B e. W )   &    |- ( ph -> C e. Z )   &    |- ( ph -> C =/= (/) )   =>    |- ( ph -> ( A C_ B <-> ( A ^m C ) C_ ( B ^m C ) ) )
Theorem	fsneq 37541	Equality condition for two functions defined on a singleton. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
|- ( ph -> A e. V )   &    |- B = { A }   &    |- ( ph -> F Fn B )   &    |- ( ph -> G Fn B )   =>    |- ( ph -> ( F = G <-> ( F ` A ) = ( G ` A ) ) )
Theorem	mpbirand 37542	Detach truth from conjunction in biconditional. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
|- ( ph -> ch )   &    |- ( ph -> ( ps <-> ( ch /\ th ) ) )   =>    |- ( ph -> ( ps <-> th ) )
Theorem	difmap 37543	Difference of two sets exponentiations. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
|- ( ph -> A e. V )   &    |- ( ph -> B e. W )   &    |- ( ph -> C e. Z )   &    |- ( ph -> C =/= (/) )   =>    |- ( ph -> ( ( A \ B ) ^m C ) C_ ( ( A ^m C ) \ ( B ^m C ) ) )
Theorem	unirnmap 37544	Given a subset of a set exponentiation, the base set can be restricted. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
|- ( ph -> A e. V )   &    |- ( ph -> X C_ ( B ^m A ) )   =>    |- ( ph -> X C_ ( ran U. X ^m A ) )
Theorem	ffrn 37545	A function maps to its range. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
|- ( F : A --> B -> F : A --> ran F )
Theorem	ffund 37546	A mapping is a function. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
|- ( ph -> F : A --> B )   =>    |- ( ph -> Fun F )
Theorem	inmap 37547	Intersection of two sets exponentiations. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
|- ( ph -> A e. V )   &    |- ( ph -> B e. W )   &    |- ( ph -> C e. Z )   =>    |- ( ph -> ( ( A ^m C ) i^i ( B ^m C ) ) = ( ( A i^i B ) ^m C ) )
Theorem	fcoss 37548	Composition of two mappings. Similar to fco 5766, but with a weaker condition on the domain of F. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
|- ( ph -> F : A --> B )   &    |- ( ph -> C C_ A )   &    |- ( ph -> G : D --> C )   =>    |- ( ph -> ( F o. G ) : D --> B )
Theorem	fsneqrn 37549	Equality condition for two functions defined on a singleton. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
|- ( ph -> A e. V )   &    |- B = { A }   &    |- ( ph -> F Fn B )   &    |- ( ph -> G Fn B )   =>    |- ( ph -> ( F = G <-> ( F ` A ) e. ran G ) )
Theorem	difmapsn 37550	Difference of two sets exponentiatiated to a singleton. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
|- ( ph -> A e. V )   &    |- ( ph -> B e. W )   &    |- ( ph -> C e. Z )   =>    |- ( ph -> ( ( A ^m { C } ) \ ( B ^m { C } ) ) = ( ( A \ B ) ^m { C } ) )
Theorem	mapssbi 37551	Subset inheritance for set exponentiation. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
|- ( ph -> A e. V )   &    |- ( ph -> B e. W )   &    |- ( ph -> C e. Z )   &    |- ( ph -> C =/= (/) )   =>    |- ( ph -> ( A C_ B <-> ( A ^m C ) C_ ( B ^m C ) ) )
Theorem	unirnmapsn 37552	Equality theorem for a subset of a set exponentiation, where the exponent is a singleton. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
|- ( ph -> A e. V )   &    |- ( ph -> B e. W )   &    |- C = { A }   &    |- ( ph -> X C_ ( B ^m C ) )   =>    |- ( ph -> X = ( ran U. X ^m C ) )
Theorem	iunmapss 37553*	The indexed union of set exponentiations is a subset of the set exponentiation of the indexed union. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
|- F/ x ph   &    |- ( ph -> A e. V )   &    |- ( ( ph /\ x e. A ) -> B e. W )   =>    |- ( ph -> U_ x e. A ( B ^m C ) C_ ( U_ x e. A B ^m C ) )
Theorem	ssmapsn 37554*	A subset C of a set exponentiation to a singleton, is its projection D exponentiated to the singleton. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
|- F/_ f D   &    |- ( ph -> A e. V )   &    |- ( ph -> C C_ ( B ^m { A } ) )   &    |- D = U_ f e. C ran f   =>    |- ( ph -> C = ( D ^m { A } ) )
Theorem	iunmapsn 37555*	The indexed union of set exponentiations to a singleton is equal to the set exponentiation of the indexed union. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
|- F/ x ph   &    |- ( ph -> A e. V )   &    |- ( ( ph /\ x e. A ) -> B e. W )   &    |- ( ph -> C e. Z )   =>    |- ( ph -> U_ x e. A ( B ^m { C } ) = ( U_ x e. A B ^m { C } ) )
Theorem	absfico 37556	Mapping domain and codomain of the absolute value function. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
|- abs : CC --> ( 0 [,) +oo )
Theorem	icof 37557	The set of left-closed right-open intervals of extended reals maps to subsets of extended reals. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
|- [,) : ( RR* X. RR* ) --> ~P RR*
21.30.3  Ordering on real numbers - Real and complex numbers basic operations
Theorem	sub2times 37558	Subtracting from a number, twice the number itself, gives negative the number. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( A e. CC -> ( A - ( 2 x. A ) ) = -u A )
Theorem	xrltled 37559	'Less than' implies 'less than or equal to', for extended reals. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> A e. RR* )   &    |- ( ph -> B e. RR* )   &    |- ( ph -> A < B )   =>    |- ( ph -> A <_ B )
Theorem	abssubrp 37560	The distance of two distinct complex number is a strictly positive real. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ( A e. CC /\ B e. CC /\ A =/= B ) -> ( abs ` ( A - B ) ) e. RR+ )
Theorem	elfzfzo 37561	Relationship between membership in a half open finite set of sequential integers and membership in a finite set of sequential intergers. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( A e. ( M..^ N ) <-> ( A e. ( M ... N ) /\ A < N ) )
Theorem	oddfl 37562	Odd number representation by using the floor function. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ( K e. ZZ /\ ( K mod 2 ) =/= 0 ) -> K = ( ( 2 x. ( |_ ` ( K / 2 ) ) ) + 1 ) )
Theorem	abscosbd 37563	Bound for the absolute value of the cosine of a real number. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( A e. RR -> ( abs ` ( cos ` A ) ) <_ 1 )
Theorem	mul13d 37564	Commutative/associative law that swaps the first and the third factor in a triple product. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   =>    |- ( ph -> ( A x. ( B x. C ) ) = ( C x. ( B x. A ) ) )
Theorem	negpilt0 37565	Negative pi is negative. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- -u pi < 0
Theorem	dstregt0 37566*	A complex number A that is not real, has a distance from the reals that is strictly larger than 0. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> A e. ( CC \ RR ) )   =>    |- ( ph -> E. x e. RR+ A. y e. RR x < ( abs ` ( A - y ) ) )
Theorem	subadd4b 37567	Rearrangement of 4 terms in a mixed addition and subtraction. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> D e. CC )   =>    |- ( ph -> ( ( A - B ) + ( C - D ) ) = ( ( A - D ) + ( C - B ) ) )
Theorem	xrlttri5d 37568	Not equal and not larger implies smaller. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> A e. RR* )   &    |- ( ph -> B e. RR* )   &    |- ( ph -> A =/= B )   &    |- ( ph -> -. B < A )   =>    |- ( ph -> A < B )
Theorem	neglt 37569	The negative of a positive number is less than the number itself. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( A e. RR+ -> -u A < A )
Theorem	zltlesub 37570	If an integer N is smaller or equal to a real, and we subtract a quantity smaller than 1, then N is smaller or equal to the result. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> N e. ZZ )   &    |- ( ph -> A e. RR )   &    |- ( ph -> N <_ A )   &    |- ( ph -> B e. RR )   &    |- ( ph -> B < 1 )   &    |- ( ph -> ( A - B ) e. ZZ )   =>    |- ( ph -> N <_ ( A - B ) )
Theorem	divlt0gt0d 37571	The ratio of a negative numerator and a positive denominator is negative. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR+ )   &    |- ( ph -> A < 0 )   =>    |- ( ph -> ( A / B ) < 0 )
Theorem	3rp 37572	3 is a positive real. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- 3 e. RR+
Theorem	leimnltdOLD 37573	'Less than or equal to' implies 'not less than'. (Contributed by Glauco Siliprandi, 11-Dec-2019.) Obsolete as of 18-Jul-2020. Use lensymd 9817 instead, which is the same. (New usage is discouraged.) (Proof modification is discouraged.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> A <_ B )   =>    |- ( ph -> -. B < A )
Theorem	lt2addmuld 37574	If two real numbers are less than a third real number, the sum of the two real numbers is less than twice the third real number. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   &    |- ( ph -> A < C )   &    |- ( ph -> B < C )   =>    |- ( ph -> ( A + B ) < ( 2 x. C ) )
Theorem	subsub23d 37575	Swap subtrahend and result of subtraction. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   =>    |- ( ph -> ( ( A - B ) = C <-> ( A - C ) = B ) )
Theorem	2timesgt 37576	Double of a positive real is larger than the real itself. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( A e. RR+ -> A < ( 2 x. A ) )
Theorem	reopn 37577	The reals are open with respect to the standard topology. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- RR e. ( topGen ` ran (,) )
Theorem	elfzop1le2 37578	A member in a half-open integer interval plus 1 is less or equal than the upper bound. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( K e. ( M..^ N ) -> ( K + 1 ) <_ N )
Theorem	sub31 37579	Swap the first and third terms in a double subtraction. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A - ( B - C ) ) = ( C - ( B - A ) ) )
Theorem	nnne1ge2 37580	A positive integer which is not 1 is greater than or equal to 2. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ( N e. NN /\ N =/= 1 ) -> 2 <_ N )
Theorem	lefldiveq 37581	A closed enough, smaller real C has the same floor of A when both are divided by B. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR+ )   &    |- ( ph -> C e. ( ( A - ( A mod B ) ) [,] A ) )   =>    |- ( ph -> ( |_ ` ( A / B ) ) = ( |_ ` ( C / B ) ) )
Theorem	negsubdi3d 37582	Distribution of negative over subtraction. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> -u ( A - B ) = ( -u A - -u B ) )
Theorem	ltaddneg 37583	Adding a negative number to another number decreases it. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ( A e. RR /\ B e. RR ) -> ( A < 0 <-> ( B + A ) < B ) )
Theorem	ltdiv2dd 37584	Division of a positive number by both sides of 'less than'. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> A e. RR+ )   &    |- ( ph -> B e. RR+ )   &    |- ( ph -> C e. RR+ )   &    |- ( ph -> A < B )   =>    |- ( ph -> ( C / B ) < ( C / A ) )
Theorem	adddirp1d 37585	Distributive law, plus 1 version. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( ( A + 1 ) x. B ) = ( ( A x. B ) + B ) )
Theorem	absnpncand 37586	Triangular inequality, combined with cancellation law for subtraction. (Contributed by Glauco Siliprandi, 11-Dec-2019.) TODO (NM): usage (2 times) should be replaced by abs3difd 13577, and absnpncand 37586 should be deleted afterwards.
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   =>    |- ( ph -> ( abs ` ( A - C ) ) <_ ( ( abs ` ( A - B ) ) + ( abs ` ( B - C ) ) ) )
Theorem	abssinbd 37587	Bound for the absolute value of the sine of a real number. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( A e. RR -> ( abs ` ( sin ` A ) ) <_ 1 )
Theorem	halffl 37588	Floor of ( 1 / 2 ). (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( |_ ` ( 1 / 2 ) ) = 0
Theorem	monoords 37589*	Ordering relation for a strictly monotonic sequence, increasing case. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ( ph /\ k e. ( M ... N ) ) -> ( F ` k ) e. RR )   &    |- ( ( ph /\ k e. ( M..^ N ) ) -> ( F ` k ) < ( F ` ( k + 1 ) ) )   &    |- ( ph -> I e. ( M ... N ) )   &    |- ( ph -> J e. ( M ... N ) )   &    |- ( ph -> I < J )   =>    |- ( ph -> ( F ` I ) < ( F ` J ) )
Theorem	hashssle 37590	The size of a subset of a finite set is less than the size of the containing set. (Contributed by Glauco Siliprandi, 11-Dec-2019.) TODO (NM): usage (2 times) should be replaced by hashss 12624, and hashssle 37590 should be deleted afterwards.
|- ( ( A e. Fin /\ B C_ A ) -> ( # ` B ) <_ ( # ` A ) )
Theorem	flltnz 37591	If A is not an integer, then the floor of A is less than A. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ( A e. RR /\ -. A e. ZZ ) -> ( |_ ` A ) < A )
Theorem	lttri5d 37592	Not equal and not larger implies smaller. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> A =/= B )   &    |- ( ph -> -. B < A )   =>    |- ( ph -> A < B )
Theorem	fzisoeu 37593*	A finite ordered set has a unique order isomorphism to a generic finite sequence of integers. This theorem generalizes fz1iso 12664 for the base index and also states the uniqueness condition. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> H e. Fin )   &    |- ( ph -> < Or H )   &    |- ( ph -> M e. ZZ )   &    |- N = ( ( # ` H ) + ( M - 1 ) )   =>    |- ( ph -> E! f f Isom < , < ( ( M ... N ) , H ) )
Theorem	lt3addmuld 37594	If three real numbers are less than a fourth real number, the sum of the three real numbers is less than three times the third real number. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   &    |- ( ph -> D e. RR )   &    |- ( ph -> A < D )   &    |- ( ph -> B < D )   &    |- ( ph -> C < D )   =>    |- ( ph -> ( ( A + B ) + C ) < ( 3 x. D ) )
Theorem	absnpncan2d 37595	Triangular inequality, combined with cancellation law for subtraction (applied twice). (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> D e. CC )   =>    |- ( ph -> ( abs ` ( A - D ) ) <_ ( ( ( abs ` ( A - B ) ) + ( abs ` ( B - C ) ) ) + ( abs ` ( C - D ) ) ) )
Theorem	fperiodmullem 37596*	A function with period T is also periodic with period nonnegative multiple of T. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> F : RR --> CC )   &    |- ( ph -> T e. RR )   &    |- ( ph -> N e. NN0 )   &    |- ( ph -> X e. RR )   &    |- ( ( ph /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )   =>    |- ( ph -> ( F ` ( X + ( N x. T ) ) ) = ( F ` X ) )
Theorem	fperiodmul 37597*	A function with period T is also periodic with period multiple of T. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> F : RR --> CC )   &    |- ( ph -> T e. RR )   &    |- ( ph -> N e. ZZ )   &    |- ( ph -> X e. RR )   &    |- ( ( ph /\ x e. RR ) -> ( F ` ( x + T ) ) = ( F ` x ) )   =>    |- ( ph -> ( F ` ( X + ( N x. T ) ) ) = ( F ` X ) )
Theorem	upbdrech 37598*	Choice of an upper bound for a non empty bunded set (image set version). (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> A =/= (/) )   &    |- ( ( ph /\ x e. A ) -> B e. RR )   &    |- ( ph -> E. y e. RR A. x e. A B <_ y )   &    |- C = sup ( { z | E. x e. A z = B } , RR , < )   =>    |- ( ph -> ( C e. RR /\ A. x e. A B <_ C ) )
Theorem	lt4addmuld 37599	If four real numbers are less than a fifth real number, the sum of the four real numbers is less than four times the fifth real number. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   &    |- ( ph -> D e. RR )   &    |- ( ph -> E e. RR )   &    |- ( ph -> A < E )   &    |- ( ph -> B < E )   &    |- ( ph -> C < E )   &    |- ( ph -> D < E )   =>    |- ( ph -> ( ( ( A + B ) + C ) + D ) < ( 4 x. E ) )
Theorem	absnpncan3d 37600	Triangular inequality, combined with cancellation law for subtraction (applied three times). (Contributed by Glauco Siliprandi, 11-Dec-2019.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   &    |- ( ph -> D e. CC )   &    |- ( ph -> E e. CC )   =>    |- ( ph -> ( abs ` ( A - E ) ) <_ ( ( ( ( abs ` ( A - B ) ) + ( abs ` ( B - C ) ) ) + ( abs ` ( C - D ) ) ) + ( abs ` ( D - E ) ) ) )