P. 361 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 36001-36100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	cnsrexpcl 36001	Exponentiation is closed in number rings. (Contributed by Stefan O'Rear, 30-Nov-2014.)
|- ( ph -> S e. (SubRing ` ℂfld ) )   &    |- ( ph -> X e. S )   &    |- ( ph -> Y e. NN0 )   =>    |- ( ph -> ( X ^ Y ) e. S )
Theorem	fsumcnsrcl 36002*	Finite sums are closed in number rings. (Contributed by Stefan O'Rear, 30-Nov-2014.)
|- ( ph -> S e. (SubRing ` ℂfld ) )   &    |- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> B e. S )   =>    |- ( ph -> sum_ k e. A B e. S )
Theorem	cnsrplycl 36003	Polynomials are closed in number rings. (Contributed by Stefan O'Rear, 30-Nov-2014.)
|- ( ph -> S e. (SubRing ` ℂfld ) )   &    |- ( ph -> P e. (Poly ` C ) )   &    |- ( ph -> X e. S )   &    |- ( ph -> C C_ S )   =>    |- ( ph -> ( P ` X ) e. S )
Theorem	rgspnval 36004*	Value of the ring-span of a set of elements in a ring. (Contributed by Stefan O'Rear, 7-Dec-2014.)
|- ( ph -> R e. Ring )   &    |- ( ph -> B = ( Base ` R ) )   &    |- ( ph -> A C_ B )   &    |- ( ph -> N = (RingSpan ` R ) )   &    |- ( ph -> U = ( N ` A ) )   =>    |- ( ph -> U = |^| { t e. (SubRing ` R ) | A C_ t } )
Theorem	rgspncl 36005	The ring-span of a set is a subring. (Contributed by Stefan O'Rear, 7-Dec-2014.)
|- ( ph -> R e. Ring )   &    |- ( ph -> B = ( Base ` R ) )   &    |- ( ph -> A C_ B )   &    |- ( ph -> N = (RingSpan ` R ) )   &    |- ( ph -> U = ( N ` A ) )   =>    |- ( ph -> U e. (SubRing ` R ) )
Theorem	rgspnssid 36006	The ring-span of a set contains the set. (Contributed by Stefan O'Rear, 30-Nov-2014.)
|- ( ph -> R e. Ring )   &    |- ( ph -> B = ( Base ` R ) )   &    |- ( ph -> A C_ B )   &    |- ( ph -> N = (RingSpan ` R ) )   &    |- ( ph -> U = ( N ` A ) )   =>    |- ( ph -> A C_ U )
Theorem	rgspnmin 36007	The ring-span is contained in all subspaces which contain all the generators. (Contributed by Stefan O'Rear, 30-Nov-2014.)
|- ( ph -> R e. Ring )   &    |- ( ph -> B = ( Base ` R ) )   &    |- ( ph -> A C_ B )   &    |- ( ph -> N = (RingSpan ` R ) )   &    |- ( ph -> U = ( N ` A ) )   &    |- ( ph -> S e. (SubRing ` R ) )   &    |- ( ph -> A C_ S )   =>    |- ( ph -> U C_ S )
Theorem	rgspnid 36008	The span of a subring is itself. (Contributed by Stefan O'Rear, 30-Nov-2014.)
|- ( ph -> R e. Ring )   &    |- ( ph -> A e. (SubRing ` R ) )   &    |- ( ph -> S = ( (RingSpan ` R ) ` A ) )   =>    |- ( ph -> S = A )
Theorem	rngunsnply 36009*	Adjoining one element to a ring results in a set of polynomial evaluations. (Contributed by Stefan O'Rear, 30-Nov-2014.)
|- ( ph -> B e. (SubRing ` ℂfld ) )   &    |- ( ph -> X e. CC )   &    |- ( ph -> S = ( (RingSpan ` ℂfld ) ` ( B u. { X } ) ) )   =>    |- ( ph -> ( V e. S <-> E. p e. (Poly ` B ) V = ( p ` X ) ) )
Theorem	flcidc 36010*	Finite linear combinations with an indicator function. (Contributed by Stefan O'Rear, 5-Dec-2014.)
|- ( ph -> F = ( j e. S |-> if ( j = K , 1 , 0 ) ) )   &    |- ( ph -> S e. Fin )   &    |- ( ph -> K e. S )   &    |- ( ( ph /\ i e. S ) -> B e. CC )   =>    |- ( ph -> sum_ i e. S ( ( F ` i ) x. B ) = [_ K / i ]_ B )
21.23.47  Endomorphism algebra
Syntax	cmend 36011	Syntax for module endomorphism algebra.
class MEndo
Definition	df-mend 36012*	Define the endomorphism algebra of a module. (Contributed by Stefan O'Rear, 2-Sep-2015.)
|- MEndo = ( m e. _V |-> [_ ( m LMHom m ) / b ]_ ( { <. ( Base ` ndx ) , b >. , <. ( +g ` ndx ) , ( x e. b , y e. b |-> ( x oF ( +g ` m ) y ) ) >. , <. ( .r ` ndx ) , ( x e. b , y e. b |-> ( x o. y ) ) >. } u. { <. (Scalar ` ndx ) , (Scalar ` m ) >. , <. ( .s ` ndx ) , ( x e. ( Base ` (Scalar ` m ) ) , y e. b |-> ( ( ( Base ` m ) X. { x } ) oF ( .s ` m ) y ) ) >. } ) )
Theorem	algstr 36013	Lemma to shorten proofs of algbase 36014 through algvsca 36018. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 29-Aug-2015.)
|- A = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .X. >. } u. { <. (Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , .x. >. } )   =>    |- A Struct <. 1 , 6 >.
Theorem	algbase 36014	The base set of a constructed algebra. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 29-Aug-2015.)
|- A = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .X. >. } u. { <. (Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , .x. >. } )   =>    |- ( B e. V -> B = ( Base ` A ) )
Theorem	algaddg 36015	The additive operation of a constructed algebra. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 29-Aug-2015.)
|- A = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .X. >. } u. { <. (Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , .x. >. } )   =>    |- ( .+ e. V -> .+ = ( +g ` A ) )
Theorem	algmulr 36016	The multiplicative operation of a constructed algebra. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 29-Aug-2015.)
|- A = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .X. >. } u. { <. (Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , .x. >. } )   =>    |- ( .X. e. V -> .X. = ( .r ` A ) )
Theorem	algsca 36017	The set of scalars of a constructed algebra. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 29-Aug-2015.)
|- A = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .X. >. } u. { <. (Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , .x. >. } )   =>    |- ( S e. V -> S = (Scalar ` A ) )
Theorem	algvsca 36018	The scalar product operation of a constructed algebra. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 29-Aug-2015.)
|- A = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .X. >. } u. { <. (Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , .x. >. } )   =>    |- ( .x. e. V -> .x. = ( .s ` A ) )
Theorem	mendval 36019*	Value of the module endomorphism algebra. (Contributed by Stefan O'Rear, 2-Sep-2015.)
|- B = ( M LMHom M )   &    |- .+ = ( x e. B , y e. B |-> ( x oF ( +g ` M ) y ) )   &    |- .X. = ( x e. B , y e. B |-> ( x o. y ) )   &    |- S = (Scalar ` M )   &    |- .x. = ( x e. ( Base ` S ) , y e. B |-> ( ( ( Base ` M ) X. { x } ) oF ( .s ` M ) y ) )   =>    |- ( M e. X -> (MEndo ` M ) = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .X. >. } u. { <. (Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , .x. >. } ) )
Theorem	mendbas 36020	Base set of the module endomorphism algebra. (Contributed by Stefan O'Rear, 2-Sep-2015.)
|- A = (MEndo ` M )   =>    |- ( M LMHom M ) = ( Base ` A )
Theorem	mendplusgfval 36021*	Addition in the module endomorphism algebra. (Contributed by Stefan O'Rear, 2-Sep-2015.)
|- A = (MEndo ` M )   &    |- B = ( Base ` A )   &    |- .+ = ( +g ` M )   =>    |- ( +g ` A ) = ( x e. B , y e. B |-> ( x oF .+ y ) )
Theorem	mendplusg 36022	A specific addition in the module endomorphism algebra. (Contributed by Stefan O'Rear, 3-Sep-2015.)
|- A = (MEndo ` M )   &    |- B = ( Base ` A )   &    |- .+ = ( +g ` M )   &    |- .+b = ( +g ` A )   =>    |- ( ( X e. B /\ Y e. B ) -> ( X .+b Y ) = ( X oF .+ Y ) )
Theorem	mendmulrfval 36023*	Multiplication in the module endomorphism algebra. (Contributed by Stefan O'Rear, 2-Sep-2015.)
|- A = (MEndo ` M )   &    |- B = ( Base ` A )   =>    |- ( .r ` A ) = ( x e. B , y e. B |-> ( x o. y ) )
Theorem	mendmulr 36024	A specific multiplication in the module endormoprhism algebra. (Contributed by Stefan O'Rear, 3-Sep-2015.)
|- A = (MEndo ` M )   &    |- B = ( Base ` A )   &    |- .x. = ( .r ` A )   =>    |- ( ( X e. B /\ Y e. B ) -> ( X .x. Y ) = ( X o. Y ) )
Theorem	mendsca 36025	The module endomorphism algebra has the same scalars as the underlying module. (Contributed by Stefan O'Rear, 2-Sep-2015.)
|- A = (MEndo ` M )   &    |- S = (Scalar ` M )   =>    |- S = (Scalar ` A )
Theorem	mendvscafval 36026*	Scalar multiplication in the module endomorphism algebra. (Contributed by Stefan O'Rear, 2-Sep-2015.)
|- A = (MEndo ` M )   &    |- .x. = ( .s ` M )   &    |- B = ( Base ` A )   &    |- S = (Scalar ` M )   &    |- K = ( Base ` S )   &    |- E = ( Base ` M )   =>    |- ( .s ` A ) = ( x e. K , y e. B |-> ( ( E X. { x } ) oF .x. y ) )
Theorem	mendvsca 36027	A specific scalar multiplication in the module endomorphism algebra. (Contributed by Stefan O'Rear, 3-Sep-2015.)
|- A = (MEndo ` M )   &    |- .x. = ( .s ` M )   &    |- B = ( Base ` A )   &    |- S = (Scalar ` M )   &    |- K = ( Base ` S )   &    |- E = ( Base ` M )   &    |- .xb = ( .s ` A )   =>    |- ( ( X e. K /\ Y e. B ) -> ( X .xb Y ) = ( ( E X. { X } ) oF .x. Y ) )
Theorem	mendring 36028	The module endomorphism algebra is a ring. (Contributed by Stefan O'Rear, 5-Sep-2015.)
|- A = (MEndo ` M )   =>    |- ( M e. LMod -> A e. Ring )
Theorem	mendlmod 36029	The module endomorphism algebra is a left module. (Contributed by Mario Carneiro, 22-Sep-2015.)
|- A = (MEndo ` M )   &    |- S = (Scalar ` M )   =>    |- ( ( M e. LMod /\ S e. CRing ) -> A e. LMod )
Theorem	mendassa 36030	The module endomorphism algebra is an algebra. (Contributed by Mario Carneiro, 22-Sep-2015.)
|- A = (MEndo ` M )   &    |- S = (Scalar ` M )   =>    |- ( ( M e. LMod /\ S e. CRing ) -> A e. AssAlg )
21.23.48  Subfields
Syntax	csdrg 36031	Syntax for subfields (sub-division-rings).
class SubDRing
Definition	df-sdrg 36032*	A sub-division-ring is a subset of a division ring's set which is a division ring under the induced operation. If the overring is commutative this is a field; no special consideration is made of the fields in the center of a skew field. (Contributed by Stefan O'Rear, 3-Oct-2015.)
|- SubDRing = ( w e. DivRing |-> { s e. (SubRing ` w ) | ( w ↾s s ) e. DivRing } )
Theorem	issdrg 36033	Property of a division subring. (Contributed by Stefan O'Rear, 3-Oct-2015.)
|- ( S e. (SubDRing ` R ) <-> ( R e. DivRing /\ S e. (SubRing ` R ) /\ ( R ↾s S ) e. DivRing ) )
Theorem	issdrg2 36034*	Property of a division subring (closure version). (Contributed by Mario Carneiro, 3-Oct-2015.)
|- I = ( invr ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( S e. (SubDRing ` R ) <-> ( R e. DivRing /\ S e. (SubRing ` R ) /\ A. x e. ( S \ { .0. } ) ( I ` x ) e. S ) )
Theorem	acsfn1p 36035*	Construction of a closure rule from a one-parameter partial operation. (Contributed by Stefan O'Rear, 12-Sep-2015.)
|- ( ( X e. V /\ A. b e. Y E e. X ) -> { a e. ~P X | A. b e. ( a i^i Y ) E e. a } e. (ACS ` X ) )
Theorem	subrgacs 36036	Closure property of subrings. (Contributed by Stefan O'Rear, 12-Sep-2015.)
|- B = ( Base ` R )   =>    |- ( R e. Ring -> (SubRing ` R ) e. (ACS ` B ) )
Theorem	sdrgacs 36037	Closure property of division subrings. (Contributed by Mario Carneiro, 3-Oct-2015.)
|- B = ( Base ` R )   =>    |- ( R e. DivRing -> (SubDRing ` R ) e. (ACS ` B ) )
Theorem	cntzsdrg 36038	Centralizers in division rings/fields are subfields. (Contributed by Mario Carneiro, 3-Oct-2015.)
|- B = ( Base ` R )   &    |- M = (mulGrp ` R )   &    |- Z = (Cntz ` M )   =>    |- ( ( R e. DivRing /\ S C_ B ) -> ( Z ` S ) e. (SubDRing ` R ) )
21.23.49  Cyclic groups and order
Theorem	idomrootle 36039*	No element of an integral domain can have more than N N-th roots. (Contributed by Stefan O'Rear, 11-Sep-2015.)
|- B = ( Base ` R )   &    |- .^ = (.g ` (mulGrp ` R ) )   =>    |- ( ( R e. IDomn /\ X e. B /\ N e. NN ) -> ( # ` { y e. B | ( N .^ y ) = X } ) <_ N )
Theorem	idomodle 36040*	Limit on the number of N-th roots of unity in an integral domain. (Contributed by Stefan O'Rear, 12-Sep-2015.)
|- G = ( (mulGrp ` R ) ↾s (Unit ` R ) )   &    |- B = ( Base ` G )   &    |- O = ( od ` G )   =>    |- ( ( R e. IDomn /\ N e. NN ) -> ( # ` { x e. B | ( O ` x ) || N } ) <_ N )
Theorem	fiuneneq 36041	Two finite sets of equal size have a union of the same size iff they were equal. (Contributed by Stefan O'Rear, 12-Sep-2015.)
|- ( ( A ~~ B /\ A e. Fin ) -> ( ( A u. B ) ~~ A <-> A = B ) )
Theorem	idomsubgmo 36042*	The units of an integral domain have at most one subgroup of any single finite cardinality. (Contributed by Stefan O'Rear, 12-Sep-2015.) (Revised by NM, 17-Jun-2017.)
|- G = ( (mulGrp ` R ) ↾s (Unit ` R ) )   =>    |- ( ( R e. IDomn /\ N e. NN ) -> E* y e. (SubGrp ` G ) ( # ` y ) = N )
Theorem	proot1mul 36043	Any primitive N-th root of unity is a multiple of any other. (Contributed by Stefan O'Rear, 2-Nov-2015.)
|- G = ( (mulGrp ` R ) ↾s (Unit ` R ) )   &    |- O = ( od ` G )   &    |- K = (mrCls ` (SubGrp ` G ) )   =>    |- ( ( ( R e. IDomn /\ N e. NN ) /\ ( X e. ( `' O " { N } ) /\ Y e. ( `' O " { N } ) ) ) -> X e. ( K ` { Y } ) )
Theorem	hashgcdlem 36044*	A correspondence between elements of specific GCD and relative primes in a smaller ring. (Contributed by Stefan O'Rear, 12-Sep-2015.)
|- A = { y e. ( 0..^ ( M / N ) ) | ( y gcd ( M / N ) ) = 1 }   &    |- B = { z e. ( 0..^ M ) | ( z gcd M ) = N }   &    |- F = ( x e. A |-> ( x x. N ) )   =>    |- ( ( M e. NN /\ N e. NN /\ N || M ) -> F : A -1-1-onto-> B )
Theorem	hashgcdeq 36045*	Number of initial positive integers with specified divisors. (Contributed by Stefan O'Rear, 12-Sep-2015.)
|- ( ( M e. NN /\ N e. NN ) -> ( # ` { x e. ( 0..^ M ) | ( x gcd M ) = N } ) = if ( N || M , ( phi ` ( M / N ) ) , 0 ) )
Theorem	phisum 36046*	The divisor sum identity of the totient function. (Contributed by Stefan O'Rear, 12-Sep-2015.)
|- ( N e. NN -> sum_ d e. { x e. NN | x || N } ( phi ` d ) = N )
Theorem	proot1hash 36047	If an integral domain has a primitive N-th root of unity, it has exactly ( phi ` N ) of them. (Contributed by Stefan O'Rear, 12-Sep-2015.)
|- G = ( (mulGrp ` R ) ↾s (Unit ` R ) )   &    |- O = ( od ` G )   =>    |- ( ( R e. IDomn /\ N e. NN /\ X e. ( `' O " { N } ) ) -> ( # ` ( `' O " { N } ) ) = ( phi ` N ) )
Theorem	proot1ex 36048	The complex field has primitive N-th roots of unity for all N. (Contributed by Stefan O'Rear, 12-Sep-2015.)
|- G = ( (mulGrp ` ℂfld ) ↾s ( CC \ { 0 } ) )   &    |- O = ( od ` G )   =>    |- ( N e. NN -> ( -u 1 ^c ( 2 / N ) ) e. ( `' O " { N } ) )
21.23.50  Cyclotomic polynomials
Syntax	ccytp 36049	Syntax for the sequence of cyclotomic polynomials.
class CytP
Definition	df-cytp 36050*	The Nth cyclotomic polynomial is the polynomial which has as its zeros precisely the primitive Nth roots of unity. (Contributed by Stefan O'Rear, 5-Sep-2015.)
|- CytP = ( n e. NN |-> ( (mulGrp ` (Poly1 ` ℂfld ) ) gsumg ( r e. ( `' ( od ` ( (mulGrp ` ℂfld ) ↾s ( CC \ { 0 } ) ) ) " { n } ) |-> ( (var1 ` ℂfld ) ( -g ` (Poly1 ` ℂfld ) ) ( (algSc ` (Poly1 ` ℂfld ) ) ` r ) ) ) ) )
Theorem	isdomn3 36051	Nonzero elements form a multiplicative submonoid of any domain. (Contributed by Stefan O'Rear, 11-Sep-2015.)
|- B = ( Base ` R )   &    |- .0. = ( 0g ` R )   &    |- U = (mulGrp ` R )   =>    |- ( R e. Domn <-> ( R e. Ring /\ ( B \ { .0. } ) e. (SubMnd ` U ) ) )
Theorem	mon1pid 36052	Monicity and degree of the unit polynomial. (Contributed by Stefan O'Rear, 12-Sep-2015.)
|- P = (Poly1 ` R )   &    |- .1. = ( 1r ` P )   &    |- M = (Monic1p ` R )   &    |- D = ( deg1 ` R )   =>    |- ( R e. NzRing -> ( .1. e. M /\ ( D ` .1. ) = 0 ) )
Theorem	mon1psubm 36053	Monic polynomials are a multiplicative submonoid. (Contributed by Stefan O'Rear, 12-Sep-2015.)
|- P = (Poly1 ` R )   &    |- M = (Monic1p ` R )   &    |- U = (mulGrp ` P )   =>    |- ( R e. NzRing -> M e. (SubMnd ` U ) )
Theorem	deg1mhm 36054	Homomorphic property of the polynomial degree. (Contributed by Stefan O'Rear, 12-Sep-2015.)
|- D = ( deg1 ` R )   &    |- B = ( Base ` P )   &    |- P = (Poly1 ` R )   &    |- .0. = ( 0g ` P )   &    |- Y = ( (mulGrp ` P ) ↾s ( B \ { .0. } ) )   &    |- N = (ℂfld ↾s NN0 )   =>    |- ( R e. Domn -> ( D |` ( B \ { .0. } ) ) e. ( Y MndHom N ) )
Theorem	cytpfn 36055	Functionality of the cyclotomic polynomial sequence. (Contributed by Stefan O'Rear, 5-Sep-2015.)
|- CytP Fn NN
Theorem	cytpval 36056*	Substitutions for the Nth cyclotomic polynomial. (Contributed by Stefan O'Rear, 5-Sep-2015.)
|- T = ( (mulGrp ` ℂfld ) ↾s ( CC \ { 0 } ) )   &    |- O = ( od ` T )   &    |- P = (Poly1 ` ℂfld )   &    |- X = (var1 ` ℂfld )   &    |- Q = (mulGrp ` P )   &    |- .- = ( -g ` P )   &    |- A = (algSc ` P )   =>    |- ( N e. NN -> (CytP ` N ) = ( Q gsumg ( r e. ( `' O " { N } ) |-> ( X .- ( A ` r ) ) ) ) )
21.23.51  Miscellaneous topology
Theorem	fgraphopab 36057*	Express a function as a subset of the Cartesian product. (Contributed by Stefan O'Rear, 25-Jan-2015.)
|- ( F : A --> B -> F = { <. a , b >. | ( ( a e. A /\ b e. B ) /\ ( F ` a ) = b ) } )
Theorem	fgraphxp 36058*	Express a function as a subset of the Cartesian product. (Contributed by Stefan O'Rear, 25-Jan-2015.)
|- ( F : A --> B -> F = { x e. ( A X. B ) | ( F ` ( 1st ` x ) ) = ( 2nd ` x ) } )
Theorem	hausgraph 36059	The graph of a continuous function into a Hausdorff space is closed. (Contributed by Stefan O'Rear, 25-Jan-2015.)
|- ( ( K e. Haus /\ F e. ( J Cn K ) ) -> F e. ( Clsd ` ( J tX K ) ) )
Syntax	ctopsep 36060	The class of separable toplogies.
class TopSep
Syntax	ctoplnd 36061	The class of Lindelöf toplogies.
class TopLnd
Definition	df-topsep 36062*	A topology is separable iff it has a countable dense subset. (Contributed by Stefan O'Rear, 8-Jan-2015.)
|- TopSep = { j e. Top | E. x e. ~P U. j ( x ~<_ om /\ ( ( cls ` j ) ` x ) = U. j ) }
Definition	df-toplnd 36063*	A topology is Lindelöf iff every open cover has a countable subcover. (Contributed by Stefan O'Rear, 8-Jan-2015.)
|- TopLnd = { x e. Top | A. y e. ~P x ( U. x = U. y -> E. z e. ~P x ( z ~<_ om /\ U. x = U. z ) ) }
21.24  Mathbox for Jon Pennant
Theorem	ioounsn 36064	The closure of the upper end of an open real interval. (Contributed by Jon Pennant, 8-Jun-2019.)
|- ( ( A e. RR* /\ B e. RR* /\ A < B ) -> ( ( A (,) B ) u. { B } ) = ( A (,] B ) )
Theorem	iocunico 36065	Split an open interval into two pieces at point B, Co-author TA. (Contributed by Jon Pennant, 8-Jun-2019.)
|- ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A < B /\ B < C ) ) -> ( ( A (,] B ) u. ( B [,) C ) ) = ( A (,) C ) )
Theorem	iocinico 36066	The intersection of two sets that meet at a point is that point. (Contributed by Jon Pennant, 12-Jun-2019.)
|- ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A < B /\ B < C ) ) -> ( ( A (,] B ) i^i ( B [,) C ) ) = { B } )
Theorem	iocmbl 36067	An open-below, closed-above real interval is measurable. (Contributed by Jon Pennant, 12-Jun-2019.)
|- ( ( A e. RR* /\ B e. RR ) -> ( A (,] B ) e. dom vol )
Theorem	cnioobibld 36068*	A bounded, continuous function on an open bounded interval is integrable. The function must be bounded. For a counterexample, consider F = ( x e. ( 0 (,) 1 ) |-> ( 1 / x ) ). See cniccibl 22796 for closed bounded intervals. (Contributed by Jon Pennant, 31-May-2019.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> F e. ( ( A (,) B ) -cn-> CC ) )   &    |- ( ph -> E. x e. RR A. y e. dom F ( abs ` ( F ` y ) ) <_ x )   =>    |- ( ph -> F e. L^1 )
Theorem	itgpowd 36069*	The integral of a monomial on a closed bounded interval of the real line. Co-authors TA and MC. (Contributed by Jon Pennant, 31-May-2019.) (Revised by Thierry Arnoux, 14-Jun-2019.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   &    |- ( ph -> A <_ B )   &    |- ( ph -> N e. NN0 )   =>    |- ( ph -> S. ( A [,] B ) ( x ^ N ) _d x = ( ( ( B ^ ( N + 1 ) ) - ( A ^ ( N + 1 ) ) ) / ( N + 1 ) ) )
Theorem	arearect 36070	The area of a rectangle whose sides are parallel to the coordinate axes in ( RR X. RR ) is its width multiplied by its height. (Contributed by Jon Pennant, 19-Mar-2019.)
|- A e. RR   &    |- B e. RR   &    |- C e. RR   &    |- D e. RR   &    |- A <_ B   &    |- C <_ D   &    |- S = ( ( A [,] B ) X. ( C [,] D ) )   =>    |- (area ` S ) = ( ( B - A ) x. ( D - C ) )
Theorem	areaquad 36071*	The area of a quadrilateral with two sides which are parallel to the y-axis in ( RR X. RR ) is its width multiplied by the average height of its higher edge minus the average height of its lower edge. Co-author TA. (Contributed by Jon Pennant, 31-May-2019.)
|- A e. RR   &    |- B e. RR   &    |- C e. RR   &    |- D e. RR   &    |- E e. RR   &    |- F e. RR   &    |- A < B   &    |- C <_ E   &    |- D <_ F   &    |- U = ( C + ( ( ( x - A ) / ( B - A ) ) x. ( D - C ) ) )   &    |- V = ( E + ( ( ( x - A ) / ( B - A ) ) x. ( F - E ) ) )   &    |- S = { <. x , y >. | ( x e. ( A [,] B ) /\ y e. ( U [,] V ) ) }   =>    |- (area ` S ) = ( ( ( ( F + E ) / 2 ) - ( ( D + C ) / 2 ) ) x. ( B - A ) )
21.25  Mathbox for Richard Penner
21.25.1  Short Studies
21.25.1.1  Additional work on conditional logical operator
Theorem	ifpan123g 36072	Conjunction of conditional logical operators. (Contributed by RP, 18-Apr-2020.)
|- ( (if- ( ph , ch , ta ) /\ if- ( ps , th , et ) ) <-> ( ( ( -. ph \/ ch ) /\ ( ph \/ ta ) ) /\ ( ( -. ps \/ th ) /\ ( ps \/ et ) ) ) )
Theorem	ifpan23 36073	Conjunction of conditional logical operators. (Contributed by RP, 20-Apr-2020.)
|- ( (if- ( ph , ps , ch ) /\ if- ( ph , th , ta ) ) <-> if- ( ph , ( ps /\ th ) , ( ch /\ ta ) ) )
Theorem	ifpdfor2 36074	Define or in terms of conditional logic operator. (Contributed by RP, 20-Apr-2020.)
|- ( ( ph \/ ps ) <-> if- ( ph , ph , ps ) )
Theorem	ifporcor 36075	Corollary of commutation of or. (Contributed by RP, 20-Apr-2020.)
|- (if- ( ph , ph , ps ) <-> if- ( ps , ps , ph ) )
Theorem	ifpdfan2 36076	Define and with conditional logic operator. (Contributed by RP, 25-Apr-2020.)
|- ( ( ph /\ ps ) <-> if- ( ph , ps , ph ) )
Theorem	ifpancor 36077	Corollary of commutation of and. (Contributed by RP, 25-Apr-2020.)
|- (if- ( ph , ps , ph ) <-> if- ( ps , ph , ps ) )
Theorem	ifpdfor 36078	Define or in terms of conditional logic operator and true. (Contributed by RP, 20-Apr-2020.)
|- ( ( ph \/ ps ) <-> if- ( ph , T. , ps ) )
Theorem	ifpdfan 36079	Define and with conditional logic operator and false. (Contributed by RP, 20-Apr-2020.)
|- ( ( ph /\ ps ) <-> if- ( ph , ps , F. ) )
Theorem	ifpbi2 36080	Equivalence theorem for conditional logical operators. (Contributed by RP, 14-Apr-2020.)
|- ( ( ph <-> ps ) -> (if- ( ch , ph , th ) <-> if- ( ch , ps , th ) ) )
Theorem	ifpbi3 36081	Equivalence theorem for conditional logical operators. (Contributed by RP, 14-Apr-2020.)
|- ( ( ph <-> ps ) -> (if- ( ch , th , ph ) <-> if- ( ch , th , ps ) ) )
Theorem	ifpim1 36082	Restate implication as conditional logic operator. (Contributed by RP, 20-Apr-2020.)
|- ( ( ph -> ps ) <-> if- ( -. ph , T. , ps ) )
Theorem	ifpnot 36083	Restate negated wff as conditional logic operator. (Contributed by RP, 20-Apr-2020.)
|- ( -. ph <-> if- ( ph , F. , T. ) )
Theorem	ifpid2 36084	Restate wff as conditional logic operator. (Contributed by RP, 20-Apr-2020.)
|- ( ph <-> if- ( ph , T. , F. ) )
Theorem	ifpim2 36085	Restate implication as conditional logic operator. (Contributed by RP, 20-Apr-2020.)
|- ( ( ph -> ps ) <-> if- ( ps , T. , -. ph ) )
Theorem	ifpbi23 36086	Equivalence theorem for conditional logical operators. (Contributed by RP, 15-Apr-2020.)
|- ( ( ( ph <-> ps ) /\ ( ch <-> th ) ) -> (if- ( ta , ph , ch ) <-> if- ( ta , ps , th ) ) )
Theorem	ifpdfbi 36087	Define biimplication as conditional logic operator. (Contributed by RP, 20-Apr-2020.)
|- ( ( ph <-> ps ) <-> if- ( ph , ps , -. ps ) )
Theorem	ifpbiidcor 36088	Restatement of biid 239. (Contributed by RP, 25-Apr-2020.)
|- if- ( ph , ph , -. ph )
Theorem	ifpbicor 36089	Corollary of commutation of biimplication. (Contributed by RP, 25-Apr-2020.)
|- (if- ( ph , ps , -. ps ) <-> if- ( ps , ph , -. ph ) )
Theorem	ifpxorcor 36090	Corollary of commutation of biimplication. (Contributed by RP, 25-Apr-2020.)
|- (if- ( ph , -. ps , ps ) <-> if- ( ps , -. ph , ph ) )
Theorem	ifpbi1 36091	Equivalence theorem for conditional logical operators. (Contributed by RP, 14-Apr-2020.)
|- ( ( ph <-> ps ) -> (if- ( ph , ch , th ) <-> if- ( ps , ch , th ) ) )
Theorem	ifpnot23 36092	Negation of conditional logical operator. (Contributed by RP, 18-Apr-2020.)
|- ( -. if- ( ph , ps , ch ) <-> if- ( ph , -. ps , -. ch ) )
Theorem	ifpnotnotb 36093	Factor conditional logic operator over negation in terms 2 and 3. (Contributed by RP, 21-Apr-2020.)
|- (if- ( ph , -. ps , -. ch ) <-> -. if- ( ph , ps , ch ) )
Theorem	ifpnorcor 36094	Corollary of commutation of nor. (Contributed by RP, 25-Apr-2020.)
|- (if- ( ph , -. ph , -. ps ) <-> if- ( ps , -. ps , -. ph ) )
Theorem	ifpnancor 36095	Corollary of commutation of and. (Contributed by RP, 25-Apr-2020.)
|- (if- ( ph , -. ps , -. ph ) <-> if- ( ps , -. ph , -. ps ) )
Theorem	ifpnot23b 36096	Negation of conditional logical operator. (Contributed by RP, 25-Apr-2020.)
|- ( -. if- ( ph , -. ps , ch ) <-> if- ( ph , ps , -. ch ) )
Theorem	ifpbiidcor2 36097	Restatement of biid 239. (Contributed by RP, 25-Apr-2020.)
|- -. if- ( ph , -. ph , ph )
Theorem	ifpnot23c 36098	Negation of conditional logical operator. (Contributed by RP, 25-Apr-2020.)
|- ( -. if- ( ph , ps , -. ch ) <-> if- ( ph , -. ps , ch ) )
Theorem	ifpnot23d 36099	Negation of conditional logical operator. (Contributed by RP, 25-Apr-2020.)
|- ( -. if- ( ph , -. ps , -. ch ) <-> if- ( ph , ps , ch ) )
Theorem	ifpdfnan 36100	Define nand as conditional logic operator. (Contributed by RP, 20-Apr-2020.)
|- ( ( ph -/\ ps ) <-> if- ( ph , -. ps , T. ) )