Metamath Proof Explorer Home Metamath Proof Explorer
Most Recent Proofs
 
Mirrors  >  Home  >  MPE Home  >  Th. List  >  Recent Other  >  MM 100

Most recent proofs    These are the 10 (Unicode, GIF) or 1000 (Unicode, GIF) most recent proofs in the set.mm database for the Metamath Proof Explorer (and the Hilbert Space Explorer). The set.mm database is maintained on GitHub with master (stable) and develop (development) versions. This page was created from develop commit 5fa2769, also available here: set.mm (30MB) or set.mm.bz2 (compressed, 8MB).

The original proofs of theorems with recently shortened proofs can often be found by appending "OLD" to the theorem name, for example 19.43OLD for 19.43.

Other links    Email: Norm Megill.    Mailing list: Metamath Google Group Updated 15-Oct-2017 .    Syndication: RSS feed (courtesy of Dan Getz).    Related wikis: Wikiproofs (JHilbert) (Recent Changes); Ghilbert site; Ghilbert Google Group.

Recent news items    (4-Oct-2017) Alan Sare updated his completeusersproof program.

(3-Oct-2017) Sean B. Palmer created a web page that runs the metamath program under emulated Linux in JavaScript.

(3-Oct-2017) Sean B. Palmer wrote some programs to work with our shortest known proofs of the PM propositional calculus theorems.

(28-Sep-2017) Ivan Kuckir wrote a tutorial blog entry, Introduction to Metamath, that summarizes the language syntax. (It may have been written some time ago, but I was not aware of it before.)

(26-Sep-2017) The default directory for the Metamath Proof Explorer (MPE) has been changed from the GIF version (mpegif) to the Unicode version (mpeuni) throughout the site. Please let me know if you find broken links or other issues.

(24-Sep-2017) Saveliy Skresanov added a new proof to the 100 theorem list, Ceva's Theorem cevath, bringing the Metamath total to 67.

(3-Sep-2017) Brendan Leahy added a new proof to the 100 theorem list, Area of a Circle areacirc, bringing the Metamath total to 66.

(7-Aug-2017) Mario Carneiro added a new proof to the 100 theorem list, Principle of Inclusion/Exclusion incexc, bringing the Metamath total to 65.

(1-Jul-2017) Glauco Siliprandi added a new proof to the 100 theorem list, Stirling's Formula stirling, bringing the Metamath total to 64. Related theorems include 2 versions of Wallis' formula for π (wallispi and wallispi2).

(7-May-2017) Thierry Arnoux added a new proof to the 100 theorem list, Betrand's Ballot Problem ballotth, bringing the Metamath total to 63.

(20-Apr-2017) Glauco Siliprandi added a new proof in the supplementary list on the 100 theorem list, Stone-Weierstrass Theorem stowei.

(28-Feb-2017) David Moews added a new proof to the 100 theorem list, Product of Segments of Chords chordthm, bringing the Metamath total to 62.

(18-Feb-2017) Filip Cernatescu announced Milpgame 0.1 (MILP: Math is like a puzzle!).

(1-Jan-2017) Saveliy Skresanov added a new proof to the 100 theorem list, Isosceles triangle theorem isosctr, bringing the Metamath total to 61.

(1-Jan-2017) Mario Carneiro added 2 new proofs to the 100 theorem list, L'Hôpital's Rule lhop and Taylor's Theorem taylth, bringing the Metamath total to 60.    Older news...

Color key:   Metamath Proof Explorer  Metamath Proof Explorer   Hilbert Space Explorer  Hilbert Space Explorer   User Mathboxes  User Mathboxes  

Last updated on 16-Oct-2017 at 5:38 AM ET.
Recent Additions to the Metamath Proof Explorer   Notes (last updated 14-May-2017 )
DateLabelDescription
Theorem
 
14-Oct-2017cusgrauvtx 28168 In a complete (undirected simple) graph, each vertex is a universal vertex. (Contributed by Alexander van der Vekens, 14-Oct-2017.)
 |-  ( V ComplUSGrph  E  ->  ( V UnivVertex  E )  =  V )
 
14-Oct-2017uvtxnbgravtx 28167 A universal vertex is neighbor of all other vertices. (Contributed by Alexander van der Vekens, 14-Oct-2017.)
 |-  (
 ( V USGrph  E  /\  N  e.  ( V UnivVertex  E ) )  ->  A. v  e.  ( V  \  { N } ) N  e.  ( <. V ,  E >. Neighbors  v ) )
 
14-Oct-2017uvtxnm1nbgra 28166 A universal vertex has  n  -  1 neighbors in a graph with  n vertices. (Contributed by Alexander van der Vekens, 14-Oct-2017.)
 |-  (
 ( V USGrph  E  /\  V  e.  Fin )  ->  ( N  e.  ( V UnivVertex  E )  ->  ( # `
  ( <. V ,  E >. Neighbors  N ) )  =  ( ( # `  V )  -  1 ) ) )
 
14-Oct-2017uvtxnbgra 28165 A universal vertex has all other vertices as neighbors. (Contributed by Alexander van der Vekens, 14-Oct-2017.)
 |-  (
 ( V USGrph  E  /\  N  e.  ( V UnivVertex  E ) )  ->  ( <. V ,  E >. Neighbors  N )  =  ( V  \  { N } )
 )
 
14-Oct-2017eqid 2283 Law of identity (reflexivity of class equality). Theorem 6.4 of [Quine] p. 41.

This law is thought to have originated with Aristotle (Metaphysics, Zeta, 17, 1041 a, 10-20: "Therefore, inquiring why a thing is itself, it's inquiring nothing; ... saying that the thing is itself constitutes the sole reasoning and the sole cause, in every case, to the question of why the man is man or the musician musician."). (Thanks to Stefan Allan and Benoit Jubin for this information.) (Contributed by NM, 5-Aug-1993.) (Revised by Benoit Jubin, 14-Oct-2017.)

 |-  A  =  A
 
13-Oct-2017cusgra1v 28157 A graph with one vertex (and therefore no edges) is complete. (Contributed by Alexander van der Vekens, 13-Oct-2017.)
 |-  { A } ComplUSGrph  (/)
 
13-Oct-2017cusgra0v 28156 A graph with no vertices (and therefore no edges) is complete. (Contributed by Alexander van der Vekens, 13-Oct-2017.)
 |-  (/) ComplUSGrph  (/)
 
13-Oct-2017cusisusgra 28155 A complete (undirected simple) graph is an undirected simple graph. (Contributed by Alexander van der Vekens, 13-Oct-2017.)
 |-  ( V ComplUSGrph  E  ->  V USGrph  E )
 
13-Oct-2017iscusgra0 28154 The property of being a complete (undirected simple) graph. (Contributed by Alexander van der Vekens, 13-Oct-2017.)
 |-  ( V ComplUSGrph  E  ->  ( V USGrph  E 
 /\  A. k  e.  V  A. n  e.  ( V 
 \  { k }
 ) { n ,  k }  e.  ran  E ) )
 
13-Oct-2017usgra1v 28126 A class with one (or no) vertex is a graph if and only if it has no edges. (Contributed by Alexander van der Vekens, 13-Oct-2017.)
 |-  ( { A } USGrph  E  <->  E  =  (/) )
 
13-Oct-2017difprsng 28069 Removal of a singleton from a (proper) unordered pair. (Contributed by Alexander van der Vekens, 13-Oct-2017.)
 |-  ( A  =/=  B  ->  ( { A ,  B }  \  { A } )  =  { B } )
 
12-Oct-2017uvtx01vtx 28164 If a graph/class has no edges, it has universal vertices if and only if it has at most one vertex. This theorem could have been stated  ( ( V UnivVertex  (/) )  =/=  (/)  <->  ( # `  V
)  =  1 ), but a lot of auxiliary theorems would have been needed. (Contributed by Alexander van der Vekens, 12-Oct-2017.)
 |-  (
 ( V UnivVertex  (/) )  =/=  (/)  <->  E. x  V  =  { x } )
 
12-Oct-2017uvtx0 28163 There is no universal vertex if there is no vertex. (Contributed by Alexander van der Vekens, 12-Oct-2017.)
 |-  ( (/) UnivVertex  E )  =  (/)
 
12-Oct-2017uvtxisvtx 28162 A universal vertex is a vertex. (Contributed by Alexander van der Vekens, 12-Oct-2017.)
 |-  ( N  e.  ( V UnivVertex  E )  ->  N  e.  V )
 
12-Oct-2017uvtxel 28161 An element of the set of all universal vertices. (Contributed by Alexander van der Vekens, 12-Oct-2017.)
 |-  (
 ( V  e.  X  /\  E  e.  Y ) 
 ->  ( N  e.  ( V UnivVertex  E )  <->  ( N  e.  V  /\  A. k  e.  ( V  \  { N } ) { k ,  N }  e.  ran  E ) ) )
 
12-Oct-2017isuvtx 28160 The set of all universal vertices. (Contributed by Alexander van der Vekens, 12-Oct-2017.)
 |-  (
 ( V  e.  X  /\  E  e.  Y ) 
 ->  ( V UnivVertex  E )  =  { n  e.  V  |  A. k  e.  ( V  \  { n }
 ) { k ,  n }  e.  ran  E } )
 
12-Oct-2017nbcusgra 28159 In a complete (undirected simple) graph, each vertex has all other vertices as neighbors. (Contributed by Alexander van der Vekens, 12-Oct-2017.)
 |-  (
 ( V ComplUSGrph  E  /\  N  e.  V )  ->  ( <. V ,  E >. Neighbors  N )  =  ( V  \  { N } )
 )
 
12-Oct-2017cusgra2v 28158 A graph with two (different) vertices is complete if and only if there is an edge between these two vertices. (Contributed by Alexander van der Vekens, 12-Oct-2017.)
 |-  (
 ( A  e.  V  /\  B  e.  W  /\  A  =/=  B )  ->  ( { A ,  B } USGrph  E  ->  ( { A ,  B } ComplUSGrph  E  <->  { A ,  B }  e.  ran  E ) ) )
 
12-Oct-2017iscusgra 28153 The property of being a complete (undirected simple) graph. (Contributed by Alexander van der Vekens, 12-Oct-2017.)
 |-  (
 ( V  e.  X  /\  E  e.  Y ) 
 ->  ( V ComplUSGrph  E  <->  ( V USGrph  E  /\  A. k  e.  V  A. n  e.  ( V 
 \  { k }
 ) { n ,  k }  e.  ran  E ) ) )
 
12-Oct-2017nbgrasym 28152 A vertex in a graph is a neighbor of a second vertex if and only if the second vertex is a neighbor of the first vertex. (Contributed by Alexander van der Vekens, 12-Oct-2017.)
 |-  ( V USGrph  E  ->  ( N  e.  ( <. V ,  E >. Neighbors  K )  <->  K  e.  ( <. V ,  E >. Neighbors  N ) ) )
 
12-Oct-2017nbgranself2 28151 A class is not a neighbor of itself (whether it is a vertex or not). (Contributed by Alexander van der Vekens, 12-Oct-2017.)
 |-  ( V USGrph  E  ->  N  e/  ( <. V ,  E >. Neighbors  N ) )
 
12-Oct-2017nbgrassovt 28150 The neighbors of a vertex are a subset of the other vertices. (Contributed by Alexander van der Vekens, 12-Oct-2017.)
 |-  ( V USGrph  E  ->  ( N  e.  V  ->  ( <. V ,  E >. Neighbors  N ) 
 C_  ( V  \  { N } ) ) )
 
12-Oct-2017nbgranself 28149 A node in a graph (without loops!) is not a neighbor of itself. (Contributed by Alexander van der Vekens, 12-Oct-2017.)
 |-  ( V USGrph  E  ->  A. v  e.  V  v  e/  ( <. V ,  E >. Neighbors  v
 ) )
 
12-Oct-2017nbgrassvt 28148 The neighbors of a node in a graph are a subset of all nodes of the graph. (Contributed by Alexander van der Vekens, 12-Oct-2017.)
 |-  ( V USGrph  E  ->  ( <. V ,  E >. Neighbors  N ) 
 C_  V )
 
12-Oct-2017nbgra0edg 28147 In a graph with no edges, every vertex has no neighbor. (Contributed by Alexander van der Vekens, 12-Oct-2017.)
 |-  ( V USGrph 
 (/)  ->  ( <. V ,  (/)
 >. Neighbors  K )  =  (/) )
 
12-Oct-2017nbgraisvtx 28146 Every neighbor of a class/vertex is a vertex. (Contributed by Alexander van der Vekens, 12-Oct-2017.)
 |-  ( V USGrph  E  ->  ( N  e.  ( <. V ,  E >. Neighbors  K )  ->  N  e.  V ) )
 
12-Oct-2017nbgra0nb 28144 A vertex which is not endpoint of an edge has no neighbor. (Contributed by Alexander van der Vekens, 12-Oct-2017.)
 |-  ( V USGrph  E  ->  ( A. x  e.  ran  E  N  e/  x  ->  ( <. V ,  E >. Neighbors  N )  =  (/) ) )
 
12-Oct-2017nbgranv0 28142 There are no neighbors of a class which is not a vertex. (Contributed by Alexander van der Vekens, 12-Oct-2017.)
 |-  ( N  e/  V  ->  ( <. V ,  E >. Neighbors  N )  =  (/) )
 
12-Oct-2017df-uvtx 28139 Define the class of all universal vertices (in a graphs). A vertex is called universal if it is adjacent, i.e. connected by an edge, to all other vertices (of the graph). (Contributed by Alexander van der Vekens, 12-Oct-2017.)
 |- UnivVertex  =  ( v  e.  _V ,  e  e.  _V  |->  { n  e.  v  |  A. k  e.  ( v  \  { n } ) { k ,  n }  e.  ran  e } )
 
12-Oct-2017df-cusgra 28138 Define the class of all complete (undirected simple) graphs. A undirected simple graph is called complete if every pair of distinct vertices is connected by a (unique) edge. (Contributed by Alexander van der Vekens, 12-Oct-2017.)
 |- ComplUSGrph  =  { <. v ,  e >.  |  ( v USGrph  e  /\  A. k  e.  v  A. n  e.  ( v  \  { k } ) { n ,  k }  e.  ran  e ) }
 
12-Oct-2017mpt2ndm0 28078 The value of an operation given by a maps-to rule is the empty set if the arguments ar not contained in the base sets of the rule. (Contributed by Alexander van der Vekens, 12-Oct-2017.)
 |-  F  =  ( x  e.  X ,  y  e.  Y  |->  C )   =>    |-  ( -.  ( V  e.  X  /\  W  e.  Y )  ->  ( V F W )  =  (/) )
 
12-Oct-2017repfuntw 25160 Representation as a set of pairs of a function whose domain has two distinct elements. (Contributed by FL, 26-Jun-2011.) (Proof shortened by Scott Fenton, 12-Oct-2017.)
 |-  I  e.  A   &    |-  J  e.  B   =>    |-  ( I  =/=  J  ->  ( F  Fn  { I ,  J }  <->  F  =  { <. I ,  ( F `
  I ) >. , 
 <. J ,  ( F `
  J ) >. } ) )
 
11-Oct-2017nbgraeledg 28145 A class/vertex is a neighbor of another class/vertex if and only if it is an endpoint of an edge. (Contributed by Alexander van der Vekens, 11-Oct-2017.)
 |-  ( V USGrph  E  ->  ( N  e.  ( <. V ,  E >. Neighbors  K )  <->  { N ,  K }  e.  ran  E ) )
 
11-Oct-2017mpt2xopoveqd 28087 Value of an operation given by a maps-to rule, where the first argument is a pair and the base set of the second argument is the first component of the first argument, deduction version. (Contributed by Alexander van der Vekens, 11-Oct-2017.)
 |-  F  =  ( x  e.  _V ,  y  e.  ( 1st `  x )  |->  { n  e.  ( 1st `  x )  |  ph } )   &    |-  ( ps  ->  ( V  e.  X  /\  W  e.  Y )
 )   &    |-  ( ( ps  /\  -.  K  e.  V ) 
 ->  { n  e.  V  |  [. <. V ,  W >.  /  x ]. [. K  /  y ]. ph }  =  (/) )   =>    |-  ( ps  ->  ( <. V ,  W >. F K )  =  { n  e.  V  |  [.
 <. V ,  W >.  /  x ]. [. K  /  y ]. ph } )
 
11-Oct-2017mpt2xopoveq 28085 Value of an operation given by a maps-to rule, where the first argument is a pair and the base set of the second argument is the first component of the first argument. (Contributed by Alexander van der Vekens, 11-Oct-2017.)
 |-  F  =  ( x  e.  _V ,  y  e.  ( 1st `  x )  |->  { n  e.  ( 1st `  x )  |  ph } )   =>    |-  ( ( ( V  e.  X  /\  W  e.  Y )  /\  K  e.  V )  ->  ( <. V ,  W >. F K )  =  { n  e.  V  |  [.
 <. V ,  W >.  /  x ]. [. K  /  y ]. ph } )
 
10-Oct-2017mpt2xopovel 28086 Element of the value of an operation given by a maps-to rule, where the first argument is a pair and the base set of the second argument is the first component of the first argument. (Contributed by Alexander van der Vekens and Mario Carneiro, 10-Oct-2017.)
 |-  F  =  ( x  e.  _V ,  y  e.  ( 1st `  x )  |->  { n  e.  ( 1st `  x )  |  ph } )   =>    |-  ( ( V  e.  X  /\  W  e.  Y )  ->  ( N  e.  ( <. V ,  W >. F K )  <->  ( K  e.  V  /\  N  e.  V  /\  [. <. V ,  W >.  /  x ]. [. K  /  y ]. [. N  /  n ]. ph )
 ) )
 
10-Oct-2017mpt2xopynvov0 28084 If the second argument of an operation given by a maps-to rule, where the first argument is a pair and the base set of the second argument is the first component of the first argument is not element of the the first component of the first argument, then the value of the operation is the empty set. (Contributed by Alexander van der Vekens, 10-Oct-2017.)
 |-  F  =  ( x  e.  _V ,  y  e.  ( 1st `  x )  |->  C )   =>    |-  ( K  e/  V  ->  ( <. V ,  W >. F K )  =  (/) )
 
10-Oct-2017mpt2xopxprcov0 28083 If the components of the first argument of an operation given by a maps-to rule, where the first argument is a pair and the base set of the second argument is the first component of the first argument, are not sets, then the value of the operation is the empty set. (Contributed by Alexander van der Vekens, 10-Oct-2017.)
 |-  F  =  ( x  e.  _V ,  y  e.  ( 1st `  x )  |->  C )   =>    |-  ( -.  ( V  e.  _V  /\  W  e.  _V )  ->  ( <. V ,  W >. F K )  =  (/) )
 
10-Oct-2017mpt2xopx0ov0 28082 If the first argument of an operation given by a maps-to rule, where the first argument is a pair and the base set of the second argument is the first component of the first argument, is the empty set, then the value of the operation is the empty set. (Contributed by Alexander van der Vekens, 10-Oct-2017.)
 |-  F  =  ( x  e.  _V ,  y  e.  ( 1st `  x )  |->  C )   =>    |-  ( (/) F K )  =  (/)
 
10-Oct-2017mpt2xopxnop0 28081 If the first argument of an operation given by a maps-to rule, where the first argument is a pair and the base set of the second argument is the first component of the first argument, is not an ordered pair, then the value of the operation is the empty set. (Contributed by Alexander van der Vekens, 10-Oct-2017.)
 |-  F  =  ( x  e.  _V ,  y  e.  ( 1st `  x )  |->  C )   =>    |-  ( -.  V  e.  ( _V  X.  _V )  ->  ( V F K )  =  (/) )
 
10-Oct-2017mpt2xopynvov0g 28080 If the second argument of an operation given by a maps-to rule, where the first argument is a pair and the base set of the second argument is the first component of the first argument is not element of the the first component of the first argument, then the value of the operation is the empty set. (Contributed by Alexander van der Vekens, 10-Oct-2017.)
 |-  F  =  ( x  e.  _V ,  y  e.  ( 1st `  x )  |->  C )   =>    |-  ( ( ( V  e.  X  /\  W  e.  Y )  /\  K  e/  V )  ->  ( <. V ,  W >. F K )  =  (/) )
 
10-Oct-2017mpt2xopn0yelv 28079 If there is an element of the value of an operation given by a maps-to rule, where the first argument is a pair and the base set of the second argument is the first component of the first argument, then the second argument is an element of the first component of the first argument. (Contributed by Alexander van der Vekens, 10-Oct-2017.)
 |-  F  =  ( x  e.  _V ,  y  e.  ( 1st `  x )  |->  C )   =>    |-  ( ( V  e.  X  /\  W  e.  Y )  ->  ( N  e.  ( <. V ,  W >. F K )  ->  K  e.  V )
 )
 
9-Oct-2017nbusgra 28143 The set of neighbors of a vertex in a graph. (Contributed by Alexander van der Vekens, 9-Oct-2017.)
 |-  ( V USGrph  E  ->  ( <. V ,  E >. Neighbors  N )  =  { n  e.  V  |  { N ,  n }  e.  ran  E } )
 
9-Oct-2017nbgrael 28141 The set of neighbors of an element of the first component of an ordered pair, especially of a vertex in a graph. (Contributed by Alexander van der Vekens and Mario Carneiro, 9-Oct-2017.)
 |-  (
 ( V  e.  X  /\  E  e.  Y ) 
 ->  ( N  e.  ( <. V ,  E >. Neighbors  K ) 
 <->  ( K  e.  V  /\  N  e.  V  /\  { K ,  N }  e.  ran  E ) ) )
 
8-Oct-2017rmo4f 23180 Restricted "at most one" using implicit substitution. (Contributed by NM, 24-Oct-2006.) (Revised by Thierry Arnoux, 11-Oct-2016.) (Revised by Thierry Arnoux, 8-Mar-2017.) (Revised by Thierry Arnoux, 8-Oct-2017.)
 |-  F/_ x A   &    |-  F/_ y A   &    |-  F/ x ps   &    |-  ( x  =  y  ->  (
 ph 
 <->  ps ) )   =>    |-  ( E* x  e.  A ph  <->  A. x  e.  A  A. y  e.  A  ( ( ph  /\  ps )  ->  x  =  y ) )
 
8-Oct-2017rmo3f 23178 Restricted "at most one" using explicit substitution. (Contributed by NM, 4-Nov-2012.) (Revised by NM, 16-Jun-2017.) (Revised by Thierry Arnoux, 8-Oct-2017.)
 |-  F/_ x A   &    |-  F/_ y A   &    |-  F/ y ph   =>    |-  ( E* x  e.  A ph  <->  A. x  e.  A  A. y  e.  A  (
 ( ph  /\  [ y  /  x ] ph )  ->  x  =  y ) )
 
8-Oct-2017ssrmo 23148 "At most one" existential quantification restricted to a subclass. (Contributed by Thierry Arnoux, 8-Oct-2017.)
 |-  F/_ x A   &    |-  F/_ x B   =>    |-  ( A  C_  B  ->  ( E* x  e.  B ph  ->  E* x  e.  A ph ) )
 
8-Oct-2017rmoxfrd 23147 Transfer "at most one" restricted quantification from a variable  x to another variable  y contained in expression 
A. (Contributed by Thierry Arnoux, 7-Apr-2017.) (Revised by Thierry Arnoux, 8-Oct-2017.)
 |-  (
 ( ph  /\  y  e.  C )  ->  A  e.  B )   &    |-  ( ( ph  /\  x  e.  B ) 
 ->  E! y  e.  C  x  =  A )   &    |-  (
 ( ph  /\  x  =  A )  ->  ( ps 
 <->  ch ) )   =>    |-  ( ph  ->  ( E* x  e.  B ps 
 <->  E* y  e.  C ch ) )
 
8-Oct-2017reuxfr3d 23138 Transfer existential uniqueness from a variable  x to another variable  y contained in expression  A. Cf. reuxfr2d 4557 (Contributed by Thierry Arnoux, 7-Apr-2017.) (Revised by Thierry Arnoux, 8-Oct-2017.)
 |-  (
 ( ph  /\  y  e.  C )  ->  A  e.  B )   &    |-  ( ( ph  /\  x  e.  B ) 
 ->  E* y  e.  C x  =  A )   =>    |-  ( ph  ->  ( E! x  e.  B  E. y  e.  C  ( x  =  A  /\  ps )  <->  E! y  e.  C  ps ) )
 
7-Oct-2017nbgraop 28140 The set of neighbors of an element of the first component of an ordered pair, especially of a vertex in a graph. (Contributed by Alexander van der Vekens, 7-Oct-2017.)
 |-  (
 ( ( V  e.  Y  /\  E  e.  Z )  /\  N  e.  V )  ->  ( <. V ,  E >. Neighbors  N )  =  { n  e.  V  |  { N ,  n }  e.  ran  E } )
 
7-Oct-2017df-nbgra 28137 Define the class of all Neighbors of a vertex in a graph. The neighbors of a vertex are all vertices which are connected with this vertex by an edge. (Contributed by Alexander van der Vekens and Mario Carneiro, 7-Oct-2017.)
 |- Neighbors  =  ( g  e.  _V ,  k  e.  ( 1st `  g )  |->  { n  e.  ( 1st `  g
 )  |  { k ,  n }  e.  ran  ( 2nd `  g ) } )
 
7-Oct-2017usgraedgrnv 28123 An edge of an undirected simple graph always connects to vertices. (Contributed by Alexander van der Vekens, 7-Oct-2017.)
 |-  (
 ( V USGrph  E  /\  { M ,  N }  e.  ran  E )  ->  ( M  e.  V  /\  N  e.  V ) )
 
7-Oct-2017elprchashprn2 28088 If one element of an unordered pair is not a set, the size of the unordered pair is not 2. (Contributed by Alexander van der Vekens, 7-Oct-2017.)
 |-  ( -.  M  e.  _V  ->  -.  ( # `  { M ,  N } )  =  2 )
 
7-Oct-2017eqri 23187 Infer equality of classes from equivalence of membership. (Contributed by Thierry Arnoux, 7-Oct-2017.)
 |-  F/_ x A   &    |-  F/_ x B   &    |-  ( x  e.  A  <->  x  e.  B )   =>    |-  A  =  B
 
7-Oct-2017brprcneu 5518 If  A is a proper class, then there is no unique binary relationship with  A as the first element. (Contributed by Scott Fenton, 7-Oct-2017.)
 |-  ( -.  A  e.  _V 
 ->  -.  E! x  A F x )
 
6-Oct-20171to3vfriendship 28186 The friendship theorem for small graphs: In every friendship graph with one, two or three vertices, there is a vertex which is adjacent to all other vertices. (Contributed by Alexander van der Vekens, 6-Oct-2017.)
 |-  (
 ( A  e.  X  /\  ( V  =  { A }  \/  V  =  { A ,  B }  \/  V  =  { A ,  B ,  C } ) )  ->  ( V FriendGrph  E  ->  E. v  e.  V  A. w  e.  ( V  \  {
 v } ) {
 v ,  w }  e.  ran  E ) )
 
6-Oct-20171to3vfriswmgra 28185 Every friendship graph with one, two or three vertices is a windmill graph. (Contributed by Alexander van der Vekens, 6-Oct-2017.)
 |-  (
 ( A  e.  X  /\  ( V  =  { A }  \/  V  =  { A ,  B }  \/  V  =  { A ,  B ,  C } ) )  ->  ( V FriendGrph  E  ->  E. h  e.  V  A. v  e.  ( V  \  { h } ) ( {
 v ,  h }  e.  ran  E  /\  E! w  e.  ( V  \  { h } ) { v ,  w }  e.  ran  E ) ) )
 
6-Oct-20171to2vfriswmgra 28184 Every friendship graph with one or two vertices is a windmill graph. (Contributed by Alexander van der Vekens, 6-Oct-2017.)
 |-  (
 ( A  e.  X  /\  ( V  =  { A }  \/  V  =  { A ,  B } ) )  ->  ( V FriendGrph  E  ->  E. h  e.  V  A. v  e.  ( V  \  { h } ) ( {
 v ,  h }  e.  ran  E  /\  E! w  e.  ( V  \  { h } ) { v ,  w }  e.  ran  E ) ) )
 
6-Oct-20173vfriswmgra 28183 Every friendship graph with three (different) vertices is a windmill graph. (Contributed by Alexander van der Vekens, 6-Oct-2017.)
 |-  (
 ( ( A  e.  X  /\  B  e.  Y  /\  C  e.  Z ) 
 /\  ( A  =/=  B 
 /\  A  =/=  C  /\  B  =/=  C ) 
 /\  V  =  { A ,  B ,  C } )  ->  ( V FriendGrph  E  ->  E. h  e.  V  A. v  e.  ( V  \  { h } ) ( {
 v ,  h }  e.  ran  E  /\  E! w  e.  ( V  \  { h } ) { v ,  w }  e.  ran  E ) ) )
 
6-Oct-20173vfriswmgralem 28182 Lemma for 3vfriswmgra 28183. (Contributed by Alexander van der Vekens, 6-Oct-2017.)
 |-  (
 ( ( A  e.  X  /\  B  e.  Y )  /\  A  =/=  B  /\  { A ,  B ,  C } USGrph  E )  ->  ( { A ,  B }  e.  ran  E 
 ->  E! w  e.  { A ,  B }  { A ,  w }  e.  ran  E ) )
 
6-Oct-2017tpprceq3 28072 An unordered triple is an unordered pair if one of its elemets is a proper class or is identical with another element. (Contributed by Alexander van der Vekens, 6-Oct-2017.)
 |-  ( -.  ( C  e.  _V  /\  C  =/=  B ) 
 ->  { A ,  B ,  C }  =  { A ,  B }
 )
 
6-Oct-2017tppreq3 28071 An unordered triple is an unordered pair if one of its elemets is identical with another element. (Contributed by Alexander van der Vekens, 6-Oct-2017.)
 |-  ( B  =  C  ->  { A ,  B ,  C }  =  { A ,  B }
 )
 
6-Oct-2017fveu 5517 The value of a function at a unique point. (Contributed by Scott Fenton, 6-Oct-2017.)
 |-  ( E! x  A F x  ->  ( F `
  A )  = 
 U. { x  |  A F x } )
 
6-Oct-2017df-fv 5263 Define the value of a function,  ( F `  A
), also known as function application. For example,  ( cos `  0
)  =  1 (we prove this in cos0 12430 after we define cosine in df-cos 12352). Typically function  F is defined using maps-to notation (see df-mpt 4079 and df-mpt2 5863), but this is not required. For example,  F  =  { <. 2 ,  6 >. ,  <. 3 ,  9
>. }  ->  ( F `  3 )  =  9 (ex-fv 20830). Note that df-ov 5861 will define two-argument functions using ordered pairs as  ( A F B )  =  ( F `  <. A ,  B >. ). This particular definition is quite convenient: it can be applied to any class and evaluates to the empty set when it is not meaningful (as shown by ndmfv 5552 and fvprc 5519). The left apostrophe notation originated with Peano and was adopted in Definition *30.01 of [WhiteheadRussell] p. 235, Definition 10.11 of [Quine] p. 68, and Definition 6.11 of [TakeutiZaring] p. 26. It means the same thing as the more familiar  F ( A ) notation for a function's value at  A, i.e. " F of  A," but without context-dependent notational ambiguity. Alternate definitions are dffv2 5592, dffv3 5521, fv2 5520, and fv3 5541 (the latter two previously required  A to be a set.) Restricted equivalents that require  F to be a function are shown in funfv 5586 and funfv2 5587. For the familiar definition of function value in terms of ordered pair membership, see funopfvb 5566. (Contributed by Scott Fenton, 6-Oct-2017.)
 |-  ( F `  A )  =  ( iota x A F x )
 
6-Oct-2017csbiotag 5248 Class substitution within a description binder. (Contributed by Scott Fenton, 6-Oct-2017.)
 |-  ( A  e.  V  -> 
 [_ A  /  x ]_ ( iota y ph )  =  ( iota y [. A  /  x ].
 ph ) )
 
6-Oct-2017dfiota4 5247 The  iota operation using the  if operator. (Contributed by Scott Fenton, 6-Oct-2017.)
 |-  ( iota x ph )  =  if ( E! x ph ,  U. { x  |  ph } ,  (/) )
 
5-Oct-20171vwmgra 28181 Every graph with one vertex is a windmill graph. (Contributed by Alexander van der Vekens, 5-Oct-2017.)
 |-  (
 ( A  e.  X  /\  V  =  { A } )  ->  E. h  e.  V  A. v  e.  ( V  \  { h } ) ( {
 v ,  h }  e.  ran  E  /\  E! w  e.  ( V  \  { h } ) { v ,  w }  e.  ran  E ) )
 
5-Oct-2017frgra3v 28180 Any graph with three vertices which are completely connected with each other is a friendship graph. (Contributed by Alexander van der Vekens, 5-Oct-2017.)
 |-  (
 ( ( A  e.  X  /\  B  e.  Y  /\  C  e.  Z ) 
 /\  ( A  =/=  B 
 /\  A  =/=  C  /\  B  =/=  C ) )  ->  ( { A ,  B ,  C } USGrph  E  ->  ( { A ,  B ,  C } FriendGrph  E  <->  ( { A ,  B }  e.  ran  E 
 /\  { B ,  C }  e.  ran  E  /\  { C ,  A }  e.  ran  E ) ) ) )
 
5-Oct-2017diftpsneq 28070 Removal of a singleton from an unordered triple. (Contributed by Alexander van der Vekens, 5-Oct-2017.)
 |-  (
 ( A  =/=  C  /\  B  =/=  C ) 
 ->  ( { A ,  B ,  C }  \  { C } )  =  { A ,  B } )
 
5-Oct-2017difprsneq 28068 Removal of a singleton from an unordered pair. (Contributed by Alexander van der Vekens, 5-Oct-2017.)
 |-  ( A  =/=  B  ->  ( { A ,  B }  \  { B } )  =  { A } )
 
4-Oct-2017frgra3vlem2 28179 Lemma 2 for frgra3v 28180. (Contributed by Alexander van der Vekens, 4-Oct-2017.)
 |-  (
 ( ( A  e.  X  /\  B  e.  Y  /\  C  e.  Z ) 
 /\  ( A  =/=  B 
 /\  A  =/=  C  /\  B  =/=  C ) )  ->  ( { A ,  B ,  C } USGrph  E  ->  ( E! x  e.  { A ,  B ,  C }  { { x ,  A } ,  { x ,  B } }  C_  ran 
 E 
 <->  ( { C ,  A }  e.  ran  E 
 /\  { C ,  B }  e.  ran  E ) ) ) )
 
4-Oct-2017frgra3vlem1 28178 Lemma 1 for frgra3v 28180. (Contributed by Alexander van der Vekens, 4-Oct-2017.)
 |-  (
 ( ( ( A  e.  X  /\  B  e.  Y  /\  C  e.  Z )  /\  ( A  =/=  B  /\  A  =/=  C  /\  B  =/=  C ) )  /\  { A ,  B ,  C } USGrph  E )  ->  A. x A. y ( ( ( x  e. 
 { A ,  B ,  C }  /\  { { x ,  A } ,  { x ,  B } }  C_  ran  E )  /\  ( y  e. 
 { A ,  B ,  C }  /\  { { y ,  A } ,  { y ,  B } }  C_  ran 
 E ) )  ->  x  =  y )
 )
 
4-Oct-2017frgra1v 28176 Any graph with only one vertex is a friendship graph. (Contributed by Alexander van der Vekens, 4-Oct-2017.)
 |-  (
 ( V  e.  X  /\  { V } USGrph  E ) 
 ->  { V } FriendGrph  E )
 
4-Oct-2017frgra0v 28174 Any graph with no vertex is a friendship graph if and only if the edge function is empty. (Contributed by Alexander van der Vekens, 4-Oct-2017.)
 |-  ( (/) FriendGrph  E  <->  E  =  (/) )
 
4-Oct-2017frisusgra 28173 A friendship graph is an undirected simple graph without loops. (Contributed by Alexander van der Vekens, 4-Oct-2017.)
 |-  ( V FriendGrph  E  ->  V USGrph  E )
 
4-Oct-2017frisusgrapr 28172 A friendship graph is an undirected simple graph without loops with special properties. (Contributed by Alexander van der Vekens, 4-Oct-2017.)
 |-  ( V FriendGrph  E  ->  ( V USGrph  E 
 /\  A. k  e.  V  A. l  e.  ( V 
 \  { k }
 ) E! x  e.  V  { { x ,  k } ,  { x ,  l } }  C_  ran  E )
 )
 
4-Oct-2017isfrgra 28171 The property of being a friendship graph. (Contributed by Alexander van der Vekens, 4-Oct-2017.)
 |-  (
 ( V  e.  X  /\  E  e.  Y ) 
 ->  ( V FriendGrph  E  <->  ( V USGrph  E  /\  A. k  e.  V  A. l  e.  ( V 
 \  { k }
 ) E! x  e.  V  { { x ,  k } ,  { x ,  l } }  C_  ran  E )
 ) )
 
2-Oct-2017df-frgra 28170 Define the class of all Friendship Graphs. A graph is called a friendship graph if every pair of its vertices has exactly one common neighbor. (Contributed by Alexander van der Vekens and Mario Carneiro, 2-Oct-2017.)
 |- FriendGrph  =  { <. v ,  e >.  |  ( v USGrph  e  /\  A. k  e.  v  A. l  e.  ( v  \  { k } ) E! x  e.  v  { { x ,  k } ,  { x ,  l } }  C_  ran  e ) }
 
30-Sep-2017frgra2v 28177 Any graph with two (different) vertices is not a friendship graph. (Contributed by Alexander van der Vekens, 30-Sep-2017.)
 |-  (
 ( ( A  e.  X  /\  B  e.  Y )  /\  A  =/=  B )  ->  -.  { A ,  B } FriendGrph  E )
 
30-Sep-2017frgra0 28175 Any empty graph (graph without vertices) is a friendship graph. (Contributed by Alexander van der Vekens, 30-Sep-2017.)
 |-  (/) FriendGrph  (/)
 
30-Sep-2017usgra0v 28117 The empty graph with no vertices is a graph if and only if the edge function is empty. (Contributed by Alexander van der Vekens, 30-Sep-2017.)
 |-  ( (/) USGrph  E 
 <->  E  =  (/) )
 
27-Sep-2017log2le1 23409  log 2 is less than  1. This is just a weaker form of log2ub 20245 when no tight upper bound is required. (Contributed by Thierry Arnoux, 27-Sep-2017.)
 |-  ( log `  2 )  < 
 1
 
27-Sep-2017logblt 23408 The general logarithm function is monotone. See logltb 19953 (Contributed by Thierry Arnoux, 27-Sep-2017.)
 |-  (
 ( B  e.  ( ZZ>=
 `  2 )  /\  X  e.  RR+  /\  Y  e.  RR+ )  ->  ( X  <  Y  <->  ( Blogb X )  <  ( Blogb Y ) ) )
 
27-Sep-2017logbrec 23407 Logarithm of a reciprocal changes sign. See logrec 20117 (Contributed by Thierry Arnoux, 27-Sep-2017.)
 |-  (
 ( B  e.  ( ZZ>=
 `  2 )  /\  A  e.  RR+ )  ->  ( Blogb ( 1  /  A ) )  =  -u ( Blogb A ) )
 
27-Sep-2017nnlogbexp 23406 Identity law for general logarithm with integer base. (Contributed by Thierry Arnoux, 27-Sep-2017.)
 |-  (
 ( B  e.  ( ZZ>=
 `  2 )  /\  M  e.  ZZ )  ->  ( Blogb ( B ^ M ) )  =  M )
 
27-Sep-2017logb1 23405 The natural logarithm of  1 in base  B. See log1 19939 (Contributed by Thierry Arnoux, 27-Sep-2017.)
 |-  (
 ( B  e.  CC  /\  B  =/=  0  /\  B  =/=  1 )  ->  ( Blogb 1 )  =  0 )
 
27-Sep-2017relogbcl 23404 Closure of the general logarithm with integer base on positive reals. (Contributed by Thierry Arnoux, 27-Sep-2017.)
 |-  (
 ( B  e.  RR+  /\  X  e.  RR+  /\  B  =/=  1 )  ->  ( Blogb X )  e.  RR )
 
27-Sep-2017rnlogbcl 23403 Closure of the general logarithm with integer base on positive reals. See logbcl 23399. (Contributed by Thierry Arnoux, 27-Sep-2017.)
 |-  (
 ( B  e.  ( ZZ>=
 `  2 )  /\  X  e.  RR+ )  ->  ( Blogb X )  e. 
 RR )
 
27-Sep-2017rnlogbval 23402 Value of the general logarithm with integer base. (Contributed by Thierry Arnoux, 27-Sep-2017.)
 |-  (
 ( B  e.  ( ZZ>=
 `  2 )  /\  X  e.  RR+ )  ->  ( Blogb X )  =  ( ( log `  X )  /  ( log `  B ) ) )
 
27-Sep-2017cnre2csqima 23295 Image of a centered square by the canonical bijection from  ( RR  X.  RR ) to  CC. (Contributed by Thierry Arnoux, 27-Sep-2017.)
 |-  F  =  ( x  e.  RR ,  y  e.  RR  |->  ( x  +  ( _i  x.  y ) ) )   =>    |-  ( ( X  e.  ( RR  X.  RR )  /\  Y  e.  ( RR 
 X.  RR )  /\  D  e.  RR+ )  ->  ( Y  e.  ( (
 ( ( 1st `  X )  -  D ) [,) ( ( 1st `  X )  +  D )
 )  X.  ( (
 ( 2nd `  X )  -  D ) [,) (
 ( 2nd `  X )  +  D ) ) ) 
 ->  ( ( abs `  ( Re `  ( ( F `
  Y )  -  ( F `  X ) ) ) )  <_  D  /\  ( abs `  ( Im `  ( ( F `
  Y )  -  ( F `  X ) ) ) )  <_  D ) ) )
 
27-Sep-2017cnre2csqlem 23294 Lemma for cnre2csqima 23295 (Contributed by Thierry Arnoux, 27-Sep-2017.)
 |-  ( G  |`  ( RR  X.  RR ) )  =  ( H  o.  F )   &    |-  F  Fn  ( RR  X.  RR )   &    |-  G  Fn  _V   &    |-  ( x  e.  ( RR  X. 
 RR )  ->  ( G `  x )  e. 
 RR )   &    |-  ( ( x  e.  ran  F  /\  y  e.  ran  F ) 
 ->  ( H `  ( x  -  y ) )  =  ( ( H `
  x )  -  ( H `  y ) ) )   =>    |-  ( ( X  e.  ( RR  X.  RR )  /\  Y  e.  ( RR 
 X.  RR )  /\  D  e.  RR+ )  ->  ( Y  e.  ( `' ( G  |`  ( RR 
 X.  RR ) ) "
 ( ( ( G `
  X )  -  D ) [,) (
 ( G `  X )  +  D )
 ) )  ->  ( abs `  ( H `  ( ( F `  Y )  -  ( F `  X ) ) ) )  <_  D ) )
 
27-Sep-2017df2ndres 23244 Definition for a restriction of the  2nd (second member of an ordered pair) function. (Contributed by Thierry Arnoux, 27-Sep-2017.)
 |-  ( 2nd  |`  ( A  X.  B ) )  =  ( x  e.  A ,  y  e.  B  |->  y )
 
27-Sep-2017df1stres 23243 Definition for a restriction of the  1st (first member of an ordered pair) function. (Contributed by Thierry Arnoux, 27-Sep-2017.)
 |-  ( 1st  |`  ( A  X.  B ) )  =  ( x  e.  A ,  y  e.  B  |->  x )
 
26-Sep-2017rnlogblem 23401 Useful lemma for working with integer logarithm bases (with is a common case, e.g. base 2, base 3 or base 10) (Contributed by Thierry Arnoux, 26-Sep-2017.)
 |-  ( B  e.  ( ZZ>= `  2 )  ->  ( B  e.  RR+  /\  B  =/=  0  /\  B  =/=  1
 ) )
 
26-Sep-2017difioo 23275 The difference between two opened intervals sharing the same lower bound (Contributed by Thierry Arnoux, 26-Sep-2017.)
 |-  (
 ( ( A  e.  RR*  /\  B  e.  RR*  /\  C  e.  RR* )  /\  A  <  B )  ->  (
 ( A (,) C )  \  ( A (,) B ) )  =  ( B [,) C ) )
 
26-Sep-2017joiniooico 23265 Disjoint joining an open interval with a closed below, open above interval to form a closed below, open above interval. (Contributed by Thierry Arnoux, 26-Sep-2017.)
 |-  (
 ( ( A  e.  RR*  /\  B  e.  RR*  /\  C  e.  RR* )  /\  ( A  <  B  /\  B  <_  C ) )  ->  ( ( ( A (,) B )  i^i  ( B [,) C ) )  =  (/)  /\  (
 ( A (,) B )  u.  ( B [,) C ) )  =  ( A (,) C ) ) )
 
26-Sep-2017ioossioo 23264 Condition for an open interval to be a subset of an open interval. (Contributed by Thierry Arnoux, 26-Sep-2017.)
 |-  (
 ( ( A  e.  RR*  /\  B  e.  RR* )  /\  ( A  <_  C  /\  D  <_  B )
 )  ->  ( C (,) D )  C_  ( A (,) B ) )
 
25-Sep-2017sqsscirc2 23293 The complex square of side  D is a subset of the complex circle of radius  D. (Contributed by Thierry Arnoux, 25-Sep-2017.)
 |-  (
 ( ( A  e.  CC  /\  B  e.  CC )  /\  D  e.  RR+ )  ->  ( ( ( abs `  ( Re `  ( B  -  A ) ) )  <_  ( D  /  2
 )  /\  ( abs `  ( Im `  ( B  -  A ) ) )  <_  ( D  /  2 ) )  ->  ( abs `  ( B  -  A ) )  <  D ) )
 
25-Sep-2017sqsscirc1 23292 The complex square of side  D is a subset of the complex circle of radius  D. (Contributed by Thierry Arnoux, 25-Sep-2017.)
 |-  (
 ( ( ( X  e.  RR  /\  0  <_  X )  /\  ( Y  e.  RR  /\  0  <_  Y ) )  /\  D  e.  RR+ )  ->  ( ( X  <_  ( D  /  2 ) 
 /\  Y  <_  ( D  /  2 ) ) 
 ->  ( sqr `  (
 ( X ^ 2
 )  +  ( Y ^ 2 ) ) )  <  D ) )
 
25-Sep-2017curry2ima 23247 The image of a curried function with a constant second argument. (Contributed by Thierry Arnoux, 25-Sep-2017.)
 |-  G  =  ( F  o.  `' ( 1st  |`  ( _V  X.  { C } ) ) )   =>    |-  ( ( F  Fn  ( A  X.  B ) 
 /\  C  e.  B  /\  D  C_  A )  ->  ( G " D )  =  { y  |  E. x  e.  D  y  =  ( x F C ) } )
 
25-Sep-2017rabss3d 23136 Subclass law for restricted abstraction. (Contributed by Thierry Arnoux, 25-Sep-2017.)
 |-  (
 ( ph  /\  ( x  e.  A  /\  ps ) )  ->  x  e.  B )   =>    |-  ( ph  ->  { x  e.  A  |  ps }  C_ 
 { x  e.  B  |  ps } )
 
24-Sep-2017cevath 27859 Ceva's theorem. Let  A B C be a triangle and let points  F,  D and  E lie on sides  A B,  B C,  C A correspondingly. Suppose that cevians  A D,  B E and  C F intersect at one point  O. Then triangle's sides are partitioned into segments and their lengths satisfy a certain identity. Here we obtain a bit stronger version by using complex numbers themselves instead of their absolute values.

The proof goes by applying cevathlem2 27858 three times and then using cevathlem1 27857 to multiply obtained identities and prove the theorem.

In the theorem statement we are using function  G as a collinearity indicator. For justification of that use, see sigarcol 27854. (Contributed by Saveliy Skresanov, 24-Sep-2017.)

 |-  G  =  ( x  e.  CC ,  y  e.  CC  |->  ( Im `  ( ( * `  x )  x.  y ) ) )   &    |-  ( ph  ->  ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC ) )   &    |-  ( ph  ->  ( F  e.  CC  /\  D  e.  CC  /\  E  e.  CC )
 )   &    |-  ( ph  ->  O  e.  CC )   &    |-  ( ph  ->  ( ( ( A  -  O ) G ( D  -  O ) )  =  0  /\  ( ( B  -  O ) G ( E  -  O ) )  =  0  /\  ( ( C  -  O ) G ( F  -  O ) )  =  0 ) )   &    |-  ( ph  ->  ( ( ( A  -  F ) G ( B  -  F ) )  =  0  /\  ( ( B  -  D ) G ( C  -  D ) )  =  0  /\  ( ( C  -  E ) G ( A  -  E ) )  =  0 ) )   &    |-  ( ph  ->  ( ( ( A  -  O ) G ( B  -  O ) )  =/=  0  /\  ( ( B  -  O ) G ( C  -  O ) )  =/=  0  /\  ( ( C  -  O ) G ( A  -  O ) )  =/=  0 ) )   =>    |-  ( ph  ->  (
 ( ( A  -  F )  x.  ( C  -  E ) )  x.  ( B  -  D ) )  =  ( ( ( F  -  B )  x.  ( E  -  A ) )  x.  ( D  -  C ) ) )
 
24-Sep-2017cevathlem2 27858 Ceva's theorem second lemma. Relate (doubled) areas of triangles  C A O and 
A B O with of segments  B D and 
D C. (Contributed by Saveliy Skresanov, 24-Sep-2017.)
 |-  G  =  ( x  e.  CC ,  y  e.  CC  |->  ( Im `  ( ( * `  x )  x.  y ) ) )   &    |-  ( ph  ->  ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC ) )   &    |-  ( ph  ->  ( F  e.  CC  /\  D  e.  CC  /\  E  e.  CC )
 )   &    |-  ( ph  ->  O  e.  CC )   &    |-  ( ph  ->  ( ( ( A  -  O ) G ( D  -  O ) )  =  0  /\  ( ( B  -  O ) G ( E  -  O ) )  =  0  /\  ( ( C  -  O ) G ( F  -  O ) )  =  0 ) )   &    |-  ( ph  ->  ( ( ( A  -  F ) G ( B  -  F ) )  =  0  /\  ( ( B  -  D ) G ( C  -  D ) )  =  0  /\  ( ( C  -  E ) G ( A  -  E ) )  =  0 ) )   &    |-  ( ph  ->  ( ( ( A  -  O ) G ( B  -  O ) )  =/=  0  /\  ( ( B  -  O ) G ( C  -  O ) )  =/=  0  /\  ( ( C  -  O ) G ( A  -  O ) )  =/=  0 ) )   =>    |-  ( ph  ->  (
 ( ( C  -  O ) G ( A  -  O ) )  x.  ( B  -  D ) )  =  ( ( ( A  -  O ) G ( B  -  O ) )  x.  ( D  -  C ) ) )
 
24-Sep-2017cevathlem1 27857 Ceva's theorem first lemma. Multiplies three identities and divides by the common factors. (Contributed by Saveliy Skresanov, 24-Sep-2017.)
 |-  ( ph  ->  ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )
 )   &    |-  ( ph  ->  ( D  e.  CC  /\  E  e.  CC  /\  F  e.  CC ) )   &    |-  ( ph  ->  ( G  e.  CC  /\  H  e.  CC  /\  K  e.  CC ) )   &    |-  ( ph  ->  ( A  =/=  0  /\  E  =/=  0  /\  C  =/=  0 ) )   &    |-  ( ph  ->  ( ( A  x.  B )  =  ( C  x.  D )  /\  ( E  x.  F )  =  ( A  x.  G )  /\  ( C  x.  H )  =  ( E  x.  K ) ) )   =>    |-  ( ph  ->  (
 ( B  x.  F )  x.  H )  =  ( ( D  x.  G )  x.  K ) )
 
24-Sep-2017sigariz 27853 If signed area is zero, the signed area with swapped arguments is also zero. Deduction version. ( Contributed by Saveliy Skresanov, 23-Sep-2017.) (Contributed by Saveliy Skresanov, 24-Sep-2017.)
 |-  G  =  ( x  e.  CC ,  y  e.  CC  |->  ( Im `  ( ( * `  x )  x.  y ) ) )   &    |-  ( ph  ->  ( A  e.  CC  /\  B  e.  CC )
 )   &    |-  ( ph  ->  ( A G B )  =  0 )   =>    |-  ( ph  ->  ( B G A )  =  0 )
 
24-Sep-2017dya2iocrrnval 23582 The value of a dyadic square cover of 
( RR  X.  RR ). (Contributed by Thierry Arnoux, 24-Sep-2017.)
 |-  J  =  ( topGen `  ran  (,) )   &    |-  I  =  ( x  e.  ZZ ,  n  e.  ZZ  |->  ( ( x  /  ( 2 ^ n ) ) [,) (
 ( x  +  1 )  /  ( 2 ^ n ) ) ) )   &    |-  R  =  ( n  e.  ZZ  |->  ran  ( x  e.  ZZ ,  y  e.  ZZ  |->  ( ( x I n )  X.  (
 y I n ) ) ) )   =>    |-  ( N  e.  ZZ  ->  ( V  e.  ( R `  N )  <->  E. x  e.  ZZ  E. y  e.  ZZ  V  =  ( ( x I N )  X.  (
 y I N ) ) ) )
 
24-Sep-2017dya2iocival 23576 The function  I returns closed below opened above dyadic rational intervals covering the the real line. This is the same construction as in dyadmbl 18955. (Contributed by Thierry Arnoux, 24-Sep-2017.)
 |-  J  =  ( topGen `  ran  (,) )   &    |-  I  =  ( x  e.  ZZ ,  n  e.  ZZ  |->  ( ( x  /  ( 2 ^ n ) ) [,) (
 ( x  +  1 )  /  ( 2 ^ n ) ) ) )   &    |-  R  =  ( n  e.  ZZ  |->  ran  ( x  e.  ZZ ,  y  e.  ZZ  |->  ( ( x I n )  X.  (
 y I n ) ) ) )   =>    |-  ( ( N  e.  ZZ  /\  X  e.  ZZ )  ->  ( X I N )  =  ( ( X  /  ( 2 ^ N ) ) [,) (
 ( X  +  1 )  /  ( 2 ^ N ) ) ) )
 
24-Sep-2017xpct 23338 The cartesian product of two countable sets is countable. (Contributed by Thierry Arnoux, 24-Sep-2017.)
 |-  (
 ( A  ~<_  om  /\  B 
 ~<_  om )  ->  ( A  X.  B )  ~<_  om )
 
24-Sep-2017rnmptss 23238 The range of an operation given by the "maps to" notation as a subset. (Contributed by Thierry Arnoux, 24-Sep-2017.)
 |-  F  =  ( x  e.  A  |->  B )   =>    |-  ( A. x  e.  A  B  e.  C  ->  ran  F  C_  C )
 
24-Sep-2017difeq 23128 Rewriting an equation with set difference, without using quantifiers. (Contributed by Thierry Arnoux, 24-Sep-2017.)
 |-  (
 ( A  \  B )  =  C  <->  ( ( C  i^i  B )  =  (/)  /\  ( C  u.  B )  =  ( A  u.  B ) ) )
 
23-Sep-2017sigaradd 27856 Subtracting (double) area of  A D C from  A B C yields the (double) area of  D B C. (Contributed by Saveliy Skresanov, 23-Sep-2017.)
 |-  G  =  ( x  e.  CC ,  y  e.  CC  |->  ( Im `  ( ( * `  x )  x.  y ) ) )   &    |-  ( ph  ->  ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC ) )   &    |-  ( ph  ->  ( D  e.  CC  /\  ( ( A  -  D ) G ( B  -  D ) )  =  0
 ) )   =>    |-  ( ph  ->  (
 ( ( B  -  C ) G ( A  -  C ) )  -  ( ( D  -  C ) G ( A  -  C ) ) )  =  ( ( B  -  C ) G ( D  -  C ) ) )
 
23-Sep-2017sharhght 27855 Let  A B C be a triangle, and let  D lie on the line  A B. Then (doubled) areas of triangles  A D C and  C D B relate as lengths of corresponding bases  A D and  D B. (Contributed by Saveliy Skresanov, 23-Sep-2017.)
 |-  G  =  ( x  e.  CC ,  y  e.  CC  |->  ( Im `  ( ( * `  x )  x.  y ) ) )   &    |-  ( ph  ->  ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC ) )   &    |-  ( ph  ->  ( D  e.  CC  /\  ( ( A  -  D ) G ( B  -  D ) )  =  0
 ) )   =>    |-  ( ph  ->  (
 ( ( C  -  A ) G ( D  -  A ) )  x.  ( B  -  D ) )  =  ( ( ( C  -  B ) G ( D  -  B ) )  x.  ( A  -  D ) ) )
 
23-Sep-2017sigarimcd 27852 Signed area takes value in complex numbers. Deduction version. (Contributed by Saveliy Skresanov, 23-Sep-2017.)
 |-  G  =  ( x  e.  CC ,  y  e.  CC  |->  ( Im `  ( ( * `  x )  x.  y ) ) )   &    |-  ( ph  ->  ( A  e.  CC  /\  B  e.  CC )
 )   =>    |-  ( ph  ->  ( A G B )  e. 
 CC )
 
23-Sep-2017sspreima 23210 The preimage of a subset is a subset of the preimage. (Contributed by Brendan Leahy, 23-Sep-2017.)
 |-  (
 ( Fun  F  /\  A  C_  B )  ->  ( `' F " A ) 
 C_  ( `' F " B ) )
 
22-Sep-2017sigarcol 27854 Given three points  A,  B and  C such that  -.  A  =  B, the point  C lies on the line going through  A and  B iff the corresponding signed area is zero. That justifies the usage of signed area as a collinearity indicator. (Contributed by Saveliy Skresanov, 22-Sep-2017.)
 |-  G  =  ( x  e.  CC ,  y  e.  CC  |->  ( Im `  ( ( * `  x )  x.  y ) ) )   &    |-  ( ph  ->  ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC ) )   &    |-  ( ph  ->  -.  A  =  B )   =>    |-  ( ph  ->  (
 ( ( A  -  C ) G ( B  -  C ) )  =  0  <->  E. t  e.  RR  C  =  ( B  +  ( t  x.  ( A  -  B ) ) ) ) )
 
22-Sep-2017sigardiv 27851 If signed area between vectors  B  -  A and  C  -  A is zero, then those vectors lie on the same line. (Contributed by Saveliy Skresanov, 22-Sep-2017.)
 |-  G  =  ( x  e.  CC ,  y  e.  CC  |->  ( Im `  ( ( * `  x )  x.  y ) ) )   &    |-  ( ph  ->  ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC ) )   &    |-  ( ph  ->  -.  C  =  A )   &    |-  ( ph  ->  ( ( B  -  A ) G ( C  -  A ) )  =  0 )   =>    |-  ( ph  ->  (
 ( B  -  A )  /  ( C  -  A ) )  e. 
 RR )
 
22-Sep-2017areacirc 24931 The area of a circle of radius  R is  pi  x.  R ^ 2. (Contributed by Brendan Leahy, 31-Aug-2017.) (Revised by Brendan Leahy, 22-Sep-2017.)
 |-  S  =  { <. x ,  y >.  |  ( ( x  e.  RR  /\  y  e.  RR )  /\  (
 ( x ^ 2
 )  +  ( y ^ 2 ) ) 
 <_  ( R ^ 2
 ) ) }   =>    |-  ( ( R  e.  RR  /\  0  <_  R )  ->  (area `  S )  =  ( pi  x.  ( R ^ 2 ) ) )
 
22-Sep-2017areacirclem6 24930 Finding the cross-section of a circle. (Contributed by Brendan Leahy, 31-Aug-2017.) (Revised by Brendan Leahy, 22-Sep-2017.)
 |-  S  =  { <. x ,  y >.  |  ( ( x  e.  RR  /\  y  e.  RR )  /\  (
 ( x ^ 2
 )  +  ( y ^ 2 ) ) 
 <_  ( R ^ 2
 ) ) }   =>    |-  ( ( R  e.  RR  /\  0  <_  R  /\  t  e. 
 RR )  ->  ( S " { t }
 )  =  if (
 ( abs `  t )  <_  R ,  ( -u ( sqr `  ( ( R ^ 2 )  -  ( t ^ 2
 ) ) ) [,] ( sqr `  (
 ( R ^ 2
 )  -  ( t ^ 2 ) ) ) ) ,  (/) ) )
 
22-Sep-2017dya2iocbrsiga 23578 Dyadic intervals are Borel sets of 
RR. (Contributed by Thierry Arnoux, 22-Sep-2017.)
 |-  J  =  ( topGen `  ran  (,) )   &    |-  I  =  ( x  e.  ZZ ,  n  e.  ZZ  |->  ( ( x  /  ( 2 ^ n ) ) [,) (
 ( x  +  1 )  /  ( 2 ^ n ) ) ) )   &    |-  R  =  ( n  e.  ZZ  |->  ran  ( x  e.  ZZ ,  y  e.  ZZ  |->  ( ( x I n )  X.  (
 y I n ) ) ) )   =>    |-  ( ( N  e.  ZZ  /\  X  e.  ZZ )  ->  ( X I N )  e. 𝔅 )
 
22-Sep-2017br2base 23574 The base set for the generator of the Borel sigma algebra on  ( RR  X.  RR ) is indeed  ( RR  X.  RR ). (Contributed by Thierry Arnoux, 22-Sep-2017.)
 |-  U. ran  ( x  e. 𝔅 ,  y  e. 𝔅 
 |->  ( x  X.  y
 ) )  =  ( RR  X.  RR )
 
22-Sep-2017sssigagen2 23507 A subset of the generating set is also a subset of the generated sigma algebra. (Contributed by Thierry Arnoux, 22-Sep-2017.)
 |-  (
 ( A  e.  V  /\  B  C_  A )  ->  B  C_  (sigaGen `  A ) )
 
22-Sep-2017xpinpreima2 23291 Rewrite the cartesian product of two sets as the intersection of their preimage by  1st and  2nd, the projections on the first and second elements. (Contributed by Thierry Arnoux, 22-Sep-2017.)
 |-  (
 ( A  C_  E  /\  B  C_  F )  ->  ( A  X.  B )  =  ( ( `' ( 1st  |`  ( E  X.  F ) )
 " A )  i^i  ( `' ( 2nd  |`  ( E  X.  F ) ) " B ) ) )
 
22-Sep-2017xpinpreima 23290 Rewrite the cartesian product of two sets as the intersection of their preimage by  1st and  2nd, the projections on the first and second elements. (Contributed by Thierry Arnoux, 22-Sep-2017.)
 |-  ( A  X.  B )  =  ( ( `' ( 1st  |`  ( _V  X.  _V ) ) " A )  i^i  ( `' ( 2nd  |`  ( _V  X.  _V ) ) " B ) )
 
22-Sep-20172ndnpr 23246 Value of the second-member function at non-pairs. (Contributed by Thierry Arnoux, 22-Sep-2017.)
 |-  ( -.  A  e.  ( _V 
 X.  _V )  ->  ( 2nd `  A )  =  (/) )
 
22-Sep-20171stnpr 23245 Value of the first-member function at non-pairs. (Contributed by Thierry Arnoux, 22-Sep-2017.)
 |-  ( -.  A  e.  ( _V 
 X.  _V )  ->  ( 1st `  A )  =  (/) )
 
22-Sep-2017ax16 1985 Proof of older axiom ax-16 2083. (Contributed by NM, 8-Nov-2006.) (Revised by NM, 22-Sep-2017.)
 |-  ( A. x  x  =  y  ->  ( ph  ->  A. x ph )
 )
 
21-Sep-2017tpr2rico 23296 For any point of an open set of the usual topology on  ( RR  X.  RR ) there is a closed below opened above square which contains that point and is entirely in the open set. This is square is actually similar to a ball by the  ( l ^  +oo ) norm, closed below, centered on  X. (Contributed by Thierry Arnoux, 21-Sep-2017.)
 |-  J  =  ( topGen `  ran  (,) )   &    |-  G  =  ( u  e.  RR ,  v  e.  RR  |->  ( u  +  ( _i  x.  v ) ) )   &    |-  B  =  ran  ( x  e.  ran  [,)
 ,  y  e.  ran  [,)  |->  ( x  X.  y
 ) )   =>    |-  ( ( A  e.  ( J  tX  J ) 
 /\  X  e.  A )  ->  E. r  e.  B  ( X  e.  r  /\  r  C_  A ) )
 
21-Sep-2017clduni 23289 For any topology, the union of the closed sets is the base set. (Contributed by Thierry Arnoux, 21-Sep-2017.)
 |-  ( J  e.  Top  ->  U. ( Clsd `  J )  = 
 U. J )
 
21-Sep-2017tpr2uni 23288 The usual topology on  ( RR  X.  RR ) is the product topology of the usual topology on  RR. (Contributed by Thierry Arnoux, 21-Sep-2017.)
 |-  J  =  ( topGen `  ran  (,) )   =>    |-  U. ( J  tX  J )  =  ( RR  X.  RR )
 
21-Sep-2017tpr2tp 23287 The usual topology on  ( RR  X.  RR ) is the product topology of the usual topology on  RR. (Contributed by Thierry Arnoux, 21-Sep-2017.)
 |-  J  =  ( topGen `  ran  (,) )   =>    |-  ( J  tX  J )  e.  (TopOn `  ( RR  X. 
 RR ) )
 
21-Sep-2017icossico 23263 Condition for a closed interval to be a subset of an open interval. (Contributed by Thierry Arnoux, 21-Sep-2017.)
 |-  (
 ( ( A  e.  RR*  /\  B  e.  RR* )  /\  ( A  <_  C  /\  D  <_  B )
 )  ->  ( C [,) D )  C_  ( A [,) B ) )
 
20-Sep-2017sigarperm 27850 Signed area  ( A  -  C ) G ( B  -  C ) acts as a double area of a triangle  A B C. Here we prove that cyclically permuting the vertices doesn't change the area. (Contributed by Saveliy Skresanov, 20-Sep-2017.)
 |-  G  =  ( x  e.  CC ,  y  e.  CC  |->  ( Im `  ( ( * `  x )  x.  y ) ) )   =>    |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  ( ( A  -  C ) G ( B  -  C ) )  =  ( ( B  -  A ) G ( C  -  A ) ) )
 
20-Sep-2017sigarexp 27849 Expand the signed area formula by linearity. (Contributed by Saveliy Skresanov, 20-Sep-2017.)
 |-  G  =  ( x  e.  CC ,  y  e.  CC  |->  ( Im `  ( ( * `  x )  x.  y ) ) )   =>    |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  ( ( A  -  C ) G ( B  -  C ) )  =  ( ( ( A G B )  -  ( A G C ) )  -  ( C G B ) ) )
 
20-Sep-2017sigarid 27848 Signed area of a flat parallelogram is zero. (Contributed by Saveliy Skresanov, 20-Sep-2017.)
 |-  G  =  ( x  e.  CC ,  y  e.  CC  |->  ( Im `  ( ( * `  x )  x.  y ) ) )   =>    |-  ( A  e.  CC  ->  ( A G A )  =  0 )
 
19-Sep-2017chordthmALT 28710 The intersecting chords theorem. If points A, B, C, and D lie on a circle (with center Q, say), and the point P is on the interior of the segments AB and CD, then the two products of lengths PA  x. PB and PC  x. PD are equal. The Euclidean plane is identified with the complex plane, and the fact that P is on AB and on CD is expressed by the hypothesis that the angles APB and CPD are equal to  pi. The result is proven by using chordthmlem5 20133 twice to show that PA  x. PB and PC  x. PD both equal BQ 2  - PQ 2 . This is similar to the proof of the theorem given in Euclid's Elements_, where it is Proposition III.35. Proven by David Moews on 28-Feb-2017 as chordthm 20134. http://www.virtualdeduction.com/chordthmaltvd.html is a Virtual Deduction User's Proof transcription of chordthm 20134. That VD User's Proof was input into completeusersproof, automatically generating this chordthmALT 28710 Metamath proof. (Contributed by Alan Sare, 19-Sep-2017.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  F  =  ( x  e.  ( CC  \  { 0 } ) ,  y  e.  ( CC  \  {
 0 } )  |->  ( Im `  ( log `  ( y  /  x ) ) ) )   &    |-  ( ph  ->  A  e.  CC )   &    |-  ( ph  ->  B  e.  CC )   &    |-  ( ph  ->  C  e.  CC )   &    |-  ( ph  ->  D  e.  CC )   &    |-  ( ph  ->  P  e.  CC )   &    |-  ( ph  ->  A  =/=  P )   &    |-  ( ph  ->  B  =/=  P )   &    |-  ( ph  ->  C  =/=  P )   &    |-  ( ph  ->  D  =/=  P )   &    |-  ( ph  ->  (
 ( A  -  P ) F ( B  -  P ) )  =  pi )   &    |-  ( ph  ->  ( ( C  -  P ) F ( D  -  P ) )  =  pi )   &    |-  ( ph  ->  Q  e.  CC )   &    |-  ( ph  ->  ( abs `  ( A  -  Q ) )  =  ( abs `  ( B  -  Q ) ) )   &    |-  ( ph  ->  ( abs `  ( A  -  Q ) )  =  ( abs `  ( C  -  Q ) ) )   &    |-  ( ph  ->  ( abs `  ( A  -  Q ) )  =  ( abs `  ( D  -  Q ) ) )   =>    |-  ( ph  ->  (
 ( abs `  ( P  -  A ) )  x.  ( abs `  ( P  -  B ) ) )  =  ( ( abs `  ( P  -  C ) )  x.  ( abs `  ( P  -  D ) ) ) )
 
19-Sep-2017sigarls 27847 Signed area is linear by the second argument. (Contributed by Saveliy Skresanov, 19-Sep-2017.)
 |-  G  =  ( x  e.  CC ,  y  e.  CC  |->  ( Im `  ( ( * `  x )  x.  y ) ) )   =>    |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  RR )  ->  ( A G ( B  x.  C ) )  =  ( ( A G B )  x.  C ) )
 
19-Sep-2017sigarms 27846 Signed area is additive (with respect to subtraction) by the second argument. (Contributed by Saveliy Skresanov, 19-Sep-2017.)
 |-  G  =  ( x  e.  CC ,  y  e.  CC  |->  ( Im `  ( ( * `  x )  x.  y ) ) )   =>    |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  ( A G ( B  -  C ) )  =  ( ( A G B )  -  ( A G C ) ) )
 
19-Sep-2017sigaras 27845 Signed area is additive by the second argument. (Contributed by Saveliy Skresanov, 19-Sep-2017.)
 |-  G  =  ( x  e.  CC ,  y  e.  CC  |->  ( Im `  ( ( * `  x )  x.  y ) ) )   =>    |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  ( A G ( B  +  C ) )  =  ( ( A G B )  +  ( A G C ) ) )
 
19-Sep-2017sigarmf 27844 Signed area is additive (with respect to subtraction) by the first argument. (Contributed by Saveliy Skresanov, 19-Sep-2017.)
 |-  G  =  ( x  e.  CC ,  y  e.  CC  |->  ( Im `  ( ( * `  x )  x.  y ) ) )   =>    |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  ( ( A  -  C ) G B )  =  ( ( A G B )  -  ( C G B ) ) )
 
19-Sep-2017sigaraf 27843 Signed area is additive by the first argument. (Contributed by Saveliy Skresanov, 19-Sep-2017.)
 |-  G  =  ( x  e.  CC ,  y  e.  CC  |->  ( Im `  ( ( * `  x )  x.  y ) ) )   =>    |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  ( ( A  +  C ) G B )  =  ( ( A G B )  +  ( C G B ) ) )
 
19-Sep-2017sigarac 27842 Signed area is anticommutative. (Contributed by Saveliy Skresanov, 19-Sep-2017.)
 |-  G  =  ( x  e.  CC ,  y  e.  CC  |->  ( Im `  ( ( * `  x )  x.  y ) ) )   =>    |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A G B )  =  -u ( B G A ) )
 
19-Sep-2017sigarim 27841 Signed area takes value in reals. (Contributed by Saveliy Skresanov, 19-Sep-2017.)
 |-  G  =  ( x  e.  CC ,  y  e.  CC  |->  ( Im `  ( ( * `  x )  x.  y ) ) )   =>    |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A G B )  e.  RR )
 
19-Sep-2017sigarval 27840 Define the signed area by treating complex numbers as vectors with two components. (Contributed by Saveliy Skresanov, 19-Sep-2017.)
 |-  G  =  ( x  e.  CC ,  y  e.  CC  |->  ( Im `  ( ( * `  x )  x.  y ) ) )   =>    |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A G B )  =  ( Im `  ( ( * `
  A )  x.  B ) ) )
 
19-Sep-2017dya2iocrfn 23580 The function returning dyadic square covering for a given size has domain  ZZ. (Contributed by Thierry Arnoux, 19-Sep-2017.)
 |-  J  =  ( topGen `  ran  (,) )   &    |-  I  =  ( x  e.  ZZ ,  n  e.  ZZ  |->  ( ( x  /  ( 2 ^ n ) ) [,) (
 ( x  +  1 )  /  ( 2 ^ n ) ) ) )   &    |-  R  =  ( n  e.  ZZ  |->  ran  ( x  e.  ZZ ,  y  e.  ZZ  |->  ( ( x I n )  X.  (
 y I n ) ) ) )   =>    |-  R  Fn  ZZ
 
19-Sep-2017dya2iocseg 23579 For any point and any closed below, opened above interval of  RR centered on that point, there is a closed below opened above dyadic rational interval which contains that point and is included in the original interval. (Contributed by Thierry Arnoux, 19-Sep-2017.)
 |-  J  =  ( topGen `  ran  (,) )   &    |-  I  =  ( x  e.  ZZ ,  n  e.  ZZ  |->  ( ( x  /  ( 2 ^ n ) ) [,) (
 ( x  +  1 )  /  ( 2 ^ n ) ) ) )   &    |-  R  =  ( n  e.  ZZ  |->  ran  ( x  e.  ZZ ,  y  e.  ZZ  |->  ( ( x I n )  X.  (
 y I n ) ) ) )   &    |-  N  =  ( |_ `  (
 1  -  ( 2logb
 D ) ) )   &    |-  G  =  ( I  o.  `' ( 1st  |`  ( _V 
 X.  { N } )
 ) )   =>    |-  ( ( X  e.  RR  /\  D  e.  RR+ )  ->  E. b  e.  ( G " ZZ ) ( X  e.  b  /\  b  C_  ( ( X  -  D ) [,) ( X  +  D ) ) ) )
 
19-Sep-2017dya2ub 23575 An upper bound for a dyadic number. (Contributed by Thierry Arnoux, 19-Sep-2017.)
 |-  ( R  e.  RR+  ->  (
 1  /  ( 2 ^ ( |_ `  (
 1  -  ( 2logb
 R ) ) ) ) )  <  R )
 
19-Sep-2017rexunirn 23140 Restricted existential quantification over the union of the range of a function. Cf. rexrn 5667 and eluni2 3831. (Contributed by Thierry Arnoux, 19-Sep-2017.)
 |-  F  =  ( x  e.  A  |->  B )   &    |-  ( x  e.  A  ->  B  e.  V )   =>    |-  ( E. x  e.  A  E. y  e.  B  ph  ->  E. y  e.  U. ran  F ph )
 
18-Sep-2017dya2iocct 23581 The dyadic rectangle set is countable. (Contributed by Thierry Arnoux, 18-Sep-2017.)
 |-  J  =  ( topGen `  ran  (,) )   &    |-  I  =  ( x  e.  ZZ ,  n  e.  ZZ  |->  ( ( x  /  ( 2 ^ n ) ) [,) (
 ( x  +  1 )  /  ( 2 ^ n ) ) ) )   &    |-  R  =  ( n  e.  ZZ  |->  ran  ( x  e.  ZZ ,  y  e.  ZZ  |->  ( ( x I n )  X.  (
 y I n ) ) ) )   =>    |-  U. ran  R  ~<_  om
 
18-Sep-2017dya2iocress 23577 Dyadic intervals are subsets of  RR. (Contributed by Thierry Arnoux, 18-Sep-2017.)
 |-  J  =  ( topGen `  ran  (,) )   &    |-  I  =  ( x  e.  ZZ ,  n  e.  ZZ  |->  ( ( x  /  ( 2 ^ n ) ) [,) (
 ( x  +  1 )  /  ( 2 ^ n ) ) ) )   &    |-  R  =  ( n  e.  ZZ  |->  ran  ( x  e.  ZZ ,  y  e.  ZZ  |->  ( ( x I n )  X.  (
 y I n ) ) ) )   =>    |-  ( ( N  e.  ZZ  /\  X  e.  ZZ )  ->  ( X I N )  C_  RR )
 
17-Sep-2017elsigagen2 23509 A any countable union of elements of a set is also in the sigma algebra that set generates. (Contributed by Thierry Arnoux, 17-Sep-2017.)
 |-  (
 ( A  e.  V  /\  B  C_  A  /\  B 
 ~<_  om )  ->  U. B  e.  (sigaGen `  A )
 )
 
17-Sep-2017mpt2cti 23346 An operation is countable if both its domains are countable. (Contributed by Thierry Arnoux, 17-Sep-2017.)
 |-  A. x  e.  A  A. y  e.  B  C  e.  V   =>    |-  (
 ( A  ~<_  om  /\  B 
 ~<_  om )  ->  ( x  e.  A ,  y  e.  B  |->  C )  ~<_ 
 om )
 
13-Sep-2017ssnnssfz 23277 For any finite subset of  NN, find a superset in the form of a set of sequential integers. (Contributed by Thierry Arnoux, 13-Sep-2017.)
 |-  ( A  e.  ( ~P NN  i^i  Fin )  ->  E. n  e.  NN  A  C_  (
 1 ... n ) )
 
12-Sep-2017w5a 28368 Extend wff definition to include 5-way conjunction ('and'). (Contributed by Alan Sare, 12-Sep-2017.) (New usage is discouraged.)
 wff  ( ph  /\  ps  /\  ch 
 /\  th  /\  ta )
 
12-Sep-2017wvhc5 28367 Syntax for a 5-virtual hypotheses collection. (Contributed by Alan Sare, 12-Sep-2017.) (New usage is discouraged.)
 wff  (.
 ph ,. ps ,. ch ,. th ,. ta ).
 
12-Sep-2017wvhc4 28366 Syntax for a 4-virtual hypotheses collection. (Contributed by Alan Sare, 12-Sep-2017.) (New usage is discouraged.)
 wff  (.
 ph ,. ps ,. ch ,. th ).
 
12-Sep-2017xrlelttric 23250 Trichotomy law for extended reals. (Contributed by Thierry Arnoux, 12-Sep-2017.)
 |-  (
 ( A  e.  RR*  /\  B  e.  RR* )  ->  ( A  <_  B  \/  B  <  A ) )
 
7-Sep-2017nssdmovg 28077 The value of an operation outside its domain. (Contributed by Alexander van der Vekens, 7-Sep-2017.)
 |-  (
 ( dom  F  C_  ( R  X.  S )  /\  -.  ( A  e.  R  /\  B  e.  S ) )  ->  ( A F B )  =  (/) )
 
5-Sep-2017ceqsrexv2 24078 Alternate elimitation of a restricted existential quantifier, using implicit substitution. (Contributed by Scott Fenton, 5-Sep-2017.)
 |-  ( x  =  A  ->  (
 ph 
 <->  ps ) )   =>    |-  ( E. x  e.  B  ( x  =  A  /\  ph )  <->  ( A  e.  B  /\  ps ) )
 
5-Sep-2017esumcvg2 23455 Simpler version of esumcvg 23454. (Contributed by Thierry Arnoux, 5-Sep-2017.)
 |-  J  =  ( TopOpen `  ( RR* ss  ( 0 [,]  +oo ) ) )   &    |-  ( ( ph  /\  k  e.  NN )  ->  A  e.  ( 0 [,]  +oo ) )   &    |-  ( k  =  l  ->  A  =  B )   &    |-  ( k  =  m  ->  A  =  C )   =>    |-  ( ph  ->  ( n  e.  NN  |-> Σ* k  e.  (
 1 ... n ) A ) ( ~~> t `  J )Σ* k  e.  NN A )
 
5-Sep-2017esumcvg 23454 The sequence of partial sums of an extended sum converges to the whole sum. cf. fsumcvg2 12200. (Contributed by Thierry Arnoux, 5-Sep-2017.)
 |-  J  =  ( TopOpen `  ( RR* ss  ( 0 [,]  +oo ) ) )   &    |-  F  =  ( n  e.  NN  |-> Σ*
 k  e.  ( 1
 ... n ) A )   &    |-  ( ( ph  /\  k  e.  NN )  ->  A  e.  ( 0 [,]  +oo ) )   &    |-  (
 k  =  m  ->  A  =  B )   =>    |-  ( ph  ->  F ( ~~> t `  J )Σ* k  e.  NN A )
 
5-Sep-2017esumex 23412 An extended sum is a set by definition. (Contributed by Thierry Arnoux, 5-Sep-2017.)
 |- Σ* k  e.  A B  e.  _V
 
2-Sep-2017usgraedgrn 28125 An edge of an undirected simple graph without loops always connects two different vertices. (Contributed by Alexander van der Vekens, 2-Sep-2017.)
 |-  (
 ( V USGrph  E  /\  { M ,  N }  e.  ran  E )  ->  M  =/=  N )
 
31-Aug-2017areacirclem5 24929 Endpoint-inclusive continuity of antiderivative of cross-section of circle. (Contributed by Brendan Leahy, 31-Aug-2017.)
 |-  ( R  e.  RR+  ->  (
 t  e.  ( -u R [,] R )  |->  ( ( R ^ 2
 )  x.  ( (arcsin `  ( t  /  R ) )  +  (
 ( t  /  R )  x.  ( sqr `  (
 1  -  ( ( t  /  R ) ^ 2 ) ) ) ) ) ) )  e.  ( (
 -u R [,] R ) -cn-> CC ) )
 
31-Aug-2017esumpmono 23447 The partial sums in an extended sum form a monotonic sequence. (Contributed by Thierry Arnoux, 31-Aug-2017.)
 |-  ( ph  ->  M  e.  NN )   &    |-  ( ph  ->  N  e.  ( ZZ>= `  M )
 )   &    |-  ( ( ph  /\  k  e.  NN )  ->  A  e.  ( 0 [,)  +oo ) )   =>    |-  ( ph  -> Σ* k  e.  (
 1 ... M ) A 
 <_ Σ* k  e.  ( 1 ... N ) A )
 
30-Aug-2017dffun10 24453 Another potential definition of functionhood. Based on statements in http://people.math.gatech.edu/~belinfan/research/autoreas/otter/sum/fs/. (Contributed by Scott Fenton, 30-Aug-2017.)
 |-  ( Fun  F  <->  F  C_  (  _I 
 o.  ( _V  \  (
 ( _V  \  _I  )  o.  F ) ) ) )
 
29-Aug-2017areacirclem4 24927 Endpoint-inclusive continuity of Cartesian ordinate of circle. (Contributed by Brendan Leahy, 29-Aug-2017.)
 |-  (
 ( R  e.  RR  /\  0  <_  R )  ->  ( t  e.  ( -u R [,] R ) 
 |->  ( sqr `  (
 ( R ^ 2
 )  -  ( t ^ 2 ) ) ) )  e.  (
 ( -u R [,] R ) -cn-> CC ) )
 
28-Aug-2017areacirclem3 24926 Continuity of cross-section of circle. (Contributed by Brendan Leahy, 28-Aug-2017.)
 |-  ( R  e.  RR+  ->  (
 t  e.  ( -u R (,) R )  |->  ( 2  x.  ( sqr `  ( ( R ^
 2 )  -  (
 t ^ 2 ) ) ) ) )  e.  ( ( -u R (,) R ) -cn-> CC ) )
 
28-Aug-2017areacirclem2 24925 Antiderivative of cross-section of circle. (Contributed by Brendan Leahy, 28-Aug-2017.)
 |-  ( R  e.  RR+  ->  ( RR  _D  ( t  e.  ( -u R (,) R )  |->  ( ( R ^ 2 )  x.  ( (arcsin `  (
 t  /  R )
 )  +  ( ( t  /  R )  x.  ( sqr `  (
 1  -  ( ( t  /  R ) ^ 2 ) ) ) ) ) ) ) )  =  ( t  e.  ( -u R (,) R )  |->  ( 2  x.  ( sqr `  ( ( R ^
 2 )  -  (
 t ^ 2 ) ) ) ) ) )
 
28-Aug-2017esumpfinvalf 23444 Same as esumpfinval 23443, minus distinct variable restrictions. (Contributed by Thierry Arnoux, 28-Aug-2017.)
 |-  F/_ k A   &    |- 
 F/ k ph   &    |-  ( ph  ->  A  e.  Fin )   &    |-  (
 ( ph  /\  k  e.  A )  ->  B  e.  ( 0 [,)  +oo ) )   =>    |-  ( ph  -> Σ* k  e.  A B  =  sum_ k  e.  A  B )
 
26-Aug-2017areacirclem1 24928 Integrability of cross-section of circle. (Contributed by Brendan Leahy, 26-Aug-2017.)
 |-  (
 ( R  e.  RR  /\  0  <_  R )  ->  ( t  e.  ( -u R [,] R ) 
 |->  ( 2  x.  ( sqr `  ( ( R ^ 2 )  -  ( t ^ 2
 ) ) ) ) )  e.  L ^1 )
 
23-Aug-2017indpreima 23608 A function with range  { 0 ,  1 } as an indicator of the preimage of  { 1 } (Contributed by Thierry Arnoux, 23-Aug-2017.)
 |-  (
 ( O  e.  V  /\  F : O --> { 0 ,  1 } )  ->  F  =  ( (D7ED; `  O ) `  ( `' F " { 1 } ) ) )
 
23-Aug-2017indv 23596 Value of the indicator function generator with domain  O. (Contributed by Thierry Arnoux, 23-Aug-2017.)
 |-  ( O  e.  V  ->  (D7ED; `  O )  =  ( a  e.  ~P O  |->  ( x  e.  O  |->  if ( x  e.  a ,  1 ,  0 ) ) ) )
 
23-Aug-2017elpreq 23188 Equality wihin a pair (Contributed by Thierry Arnoux, 23-Aug-2017.)
 |-  ( ph  ->  X  e.  { A ,  B }
 )   &    |-  ( ph  ->  Y  e.  { A ,  B } )   &    |-  ( ph  ->  ( X  =  A  <->  Y  =  A ) )   =>    |-  ( ph  ->  X  =  Y )
 
22-Aug-2017indf1ofs 23609 The bijection between finite subsets and the indicator functions with finite support. (Contributed by Thierry Arnoux, 22-Aug-2017.)
 |-  ( O  e.  V  ->  ( (D7ED; `  O )  |` 
 Fin ) : ( ~P O  i^i  Fin )
 -1-1-onto-> { f  e.  ( { 0 ,  1 }  ^m  O )  |  ( `' f " { 1 } )  e.  Fin } )
 
22-Aug-2017ind1a 23604 Value of the indicator function where it is  1. (Contributed by Thierry Arnoux, 22-Aug-2017.)
 |-  (
 ( O  e.  V  /\  A  C_  O  /\  X  e.  O )  ->  ( ( ( (D7ED; `  O ) `  A ) `  X )  =  1  <->  X  e.  A ) )
 
21-Aug-2017indpi1 23605 Preimage of the singleton  { 1 } by the indicator function. See i1f1lem 19044. (Contributed by Thierry Arnoux, 21-Aug-2017.)
 |-  (
 ( O  e.  V  /\  A  C_  O )  ->  ( `' ( (D7ED; `  O ) `  A ) " { 1 } )  =  A )
 
21-Aug-2017nfequid 1645 Bound-variable hypothesis builder for  x  =  x. This theorem tells us that any variable, including  x, is effectively not free in  x  =  x, even though  x is technically free according to the traditional definition of free variable. (Contributed by NM, 13-Jan-2011.) (Revised by NM, 21-Aug-2017.)
 |- 
 F/ y  x  =  x
 
21-Aug-2017axmeredith 1395 Alias for meredith 1394 which "verify markup *" will match to ax-meredith 1396. (Contributed by NM, 21-Aug-2017.) (New usage is discouraged.)
 |-  ( ( ( ( ( ph  ->  ps )  ->  ( -.  ch  ->  -. 
 th ) )  ->  ch )  ->  ta )  ->  ( ( ta  ->  ph )  ->  ( th  -> 
 ph ) ) )
 
20-Aug-2017usisumgra 28114 An undirected simple graph without loops is an undirected multigraph. (Contributed by Alexander van der Vekens, 20-Aug-2017.)
 |-  ( V USGrph  E  ->  V UMGrph  E )
 
20-Aug-2017uslgrav 28100 The classes of vertices and edges of an undirected simple graph with loops are sets. (Contributed by Alexander van der Vekens, 20-Aug-2017.)
 |-  ( V USLGrph  E  ->  ( V  e.  _V  /\  E  e.  _V ) )
 
19-Aug-2017usgranloop 28124 In an undirected simple graph without loops, there is no edge connecting a vertex with itself. (Contributed by Alexander van der Vekens, 19-Aug-2017.)
 |-  ( V USGrph  E  ->  ( E. x  e.  dom  E ( E `  x )  =  { M ,  N }  ->  M  =/=  N ) )
 
19-Aug-2017usgraedgprv 28122 In an undirected graph, an edge is an unordered pair of vertices. (Contributed by Alexander van der Vekens, 19-Aug-2017.)
 |-  (
 ( V USGrph  E  /\  X  e.  dom  E ) 
 ->  ( ( E `  X )  =  { M ,  N }  ->  ( M  e.  V  /\  N  e.  V ) ) )
 
19-Aug-2017usgrass 28110 An edge is a subset of vertices, analogous to umgrass 23871. (Contributed by Alexander van der Vekens, 19-Aug-2017.)
 |-  (
 ( V USGrph  E  /\  F  e.  dom  E ) 
 ->  ( E `  F )  C_  V )
 
19-Aug-2017usgrav 28101 The classes of vertices and edges of an undirected simple graph without loops are sets. (Contributed by Alexander van der Vekens, 19-Aug-2017.)
 |-  ( V USGrph  E  ->  ( V  e.  _V  /\  E  e.  _V ) )
 
19-Aug-2017ax17o 2096 Axiom to quantify a variable over a formula in which it does not occur. Axiom C5 in [Megill] p. 444 (p. 11 of the preprint). Also appears as Axiom B6 (p. 75) of system S2 of [Tarski] p. 77 and Axiom C5-1 of [Monk2] p. 113.

(This theorem simply repeats ax-17 1603 so that we can include the following note, which applies only to the obsolete axiomatization.)

This axiom is logically redundant in the (logically complete) predicate calculus axiom system consisting of ax-gen 1533, ax-5o 2075, ax-4 2074, ax-7 1708, ax-6o 2076, ax-8 1643, ax-12o 2081, ax-9o 2077, ax-10o 2078, ax-13 1686, ax-14 1688, ax-15 2082, ax-11o 2080, and ax-16 2083: in that system, we can derive any instance of ax-17 1603 not containing wff variables by induction on formula length, using ax17eq 2122 and ax17el 2128 for the basis together hbn 1720, hbal 1710, and hbim 1725. However, if we omit this axiom, our development would be quite inconvenient since we could work only with specific instances of wffs containing no wff variables - this axiom introduces the concept of a set variable not occurring in a wff (as opposed to just two set variables being distinct). (Contributed by NM, 19-Aug-2017.) (New usage is discouraged.) (Proof modification discouraged.)

 |-  ( ph  ->  A. x ph )
 
18-Aug-2017usgrafun 28108 The edge function of an undirected simple graph without loops is a function. (Contributed by Alexander van der Vekens, 18-Aug-2017.)
 |-  ( V USGrph  E  ->  Fun  E )
 
18-Aug-2017ax4 2084 This theorem repeats sp 1716 under the name ax4 2084, so that the metamath program's "verify markup" command will check that it matches axiom scheme ax-4 2074. It is preferred that references to this theorem use the name sp 1716. (Contributed by NM, 18-Aug-2017.) (New usage is discouraged.) (Proof modification is discouraged.)
 |-  ( A. x ph  -> 
 ph )
 
17-Aug-2017usgraedgop 28109 An edge of an undirected simple graph as second component of an ordered pair. (Contributed by Alexander van der Vekens, 17-Aug-2017.)
 |-  (
 ( V USGrph  E  /\  X  e.  dom  E ) 
 ->  ( ( E `  X )  =  { M ,  N }  <->  <. X ,  { M ,  N } >.  e.  E ) )
 
15-Aug-2017usgraexmpl 28133  <. V ,  E >. is a graph of five vertices  0 ,  1 , 
2 ,  3 ,  4, with edges  { 0 ,  1 } ,  {
1 ,  2 } ,  { 2 ,  0 } ,  {
0 ,  3 }. (Contributed by Alexander van der Vekens, 15-Aug-2017.)
 |-  V  =  ( 0 ... 4
 )   &    |-  E  =  <" {
 0 ,  1 }  { 1 ,  2 }  { 2 ,  0 }  { 0 ,  3 } ">   =>    |-  V USGrph  E
 
15-Aug-2017usgraexmpldifpr 28132 Lemma for usgraexmpl 28133: all "edges" are different. (Contributed by Alexander van der Vekens, 15-Aug-2017.)
 |-  (
 ( { 0 ,  1 }  =/=  {
 1 ,  2 } 
 /\  { 0 ,  1 }  =/=  { 2 ,  0 }  /\  { 0 ,  1 }  =/=  { 0 ,  3 } )  /\  ( { 1 ,  2 }  =/=  { 2 ,  0 }  /\  { 1 ,  2 }  =/=  { 0 ,  3 }  /\  {
 2 ,  0 }  =/=  { 0 ,  3 } ) )
 
15-Aug-2017s4dom 28092 The domain of a length 4 word is the union of two (disjunct) pairs. (Contributed by Alexander van der Vekens, 15-Aug-2017.)
 |-  (
 ( ( A  e.  S  /\  B  e.  S )  /\  ( C  e.  S  /\  D  e.  S ) )  ->  ( E  =  <" A B C D ">  ->  dom 
 E  =  ( {
 0 ,  1 }  u.  { 2 ,  3 } ) ) )
 
14-Aug-2017s4f1o 28093 A length 4 word with mutually different symbols is a one-to-one function onto the set of the symbols. (Contributed by Alexander van der Vekens, 14-Aug-2017.)
 |-  (
 ( ( A  e.  S  /\  B  e.  S )  /\  ( C  e.  S  /\  D  e.  S ) )  ->  ( ( ( A  =/=  B  /\  A  =/=  C  /\  A  =/=  D )  /\  ( B  =/=  C  /\  B  =/=  D  /\  C  =/=  D ) )  ->  ( E  =  <" A B C D ">  ->  E : dom  E -1-1-onto-> ( { A ,  B }  u.  { C ,  D } ) ) ) )
 
14-Aug-2017s2f1o 28091 A length 2 word with mutually different symbols is a one-to-one function onto the set of the symbols. (Contributed by Alexander van der Vekens, 14-Aug-2017.)
 |-  (
 ( A  e.  S  /\  B  e.  S  /\  A  =/=  B )  ->  ( E  =  <" A B ">  ->  E : { 0 ,  1 } -1-1-onto-> { A ,  B } ) )
 
14-Aug-2017s4prop 28090 A length 4 word is a union of two unordered pairs of ordered pairs. (Contributed by Alexander van der Vekens, 14-Aug-2017.)
 |-  (
 ( ( A  e.  S  /\  B  e.  S )  /\  ( C  e.  S  /\  D  e.  S ) )  ->  <" A B C D ">  =  ( { <. 0 ,  A >. ,  <. 1 ,  B >. }  u.  { <. 2 ,  C >. , 
 <. 3 ,  D >. } ) )
 
14-Aug-2017s2prop 28089 A length 2 word is an unordered pair of ordered pairs. (Contributed by Alexander van der Vekens, 14-Aug-2017.)
 |-  (
 ( A  e.  S  /\  B  e.  S ) 
 ->  <" A B ">  =  { <. 0 ,  A >. ,  <. 1 ,  B >. } )
 
14-Aug-2017f1oun2prg 28076 A union of unordered pairs of ordered pairs with different elements is a one-to-one onto function. (Contributed by Alexander van der Vekens, 14-Aug-2017.)
 |-  (
 ( ( A  e.  V  /\  B  e.  W )  /\  ( C  e.  X  /\  D  e.  Y ) )  ->  ( ( ( A  =/=  B  /\  A  =/=  C  /\  A  =/=  D )  /\  ( B  =/=  C  /\  B  =/=  D  /\  C  =/=  D ) )  ->  ( { <. 0 ,  A >. ,  <. 1 ,  B >. }  u.  { <. 2 ,  C >. ,  <. 3 ,  D >. } ) : ( { 0 ,  1 }  u.  { 2 ,  3 } ) -1-1-onto-> ( { A ,  B }  u.  { C ,  D } ) ) )
 
14-Aug-2017f1oprg 28075 An unordered pair of ordered pairs with different elements is a one-to-one onto function, analogous to f1oprswap 5515. (Contributed by Alexander van der Vekens, 14-Aug-2017.)
 |-  (
 ( ( A  e.  V  /\  B  e.  W )  /\  ( C  e.  X  /\  D  e.  Y ) )  ->  ( ( A  =/=  C  /\  B  =/=  D )  ->  { <. A ,  B >. ,  <. C ,  D >. } : { A ,  C } -1-1-onto-> { B ,  D } ) )
 
14-Aug-2017indf1o 23607 The bijection between a power set and the set of indicator functions. (Contributed by Thierry Arnoux, 14-Aug-2017.)
 |-  ( O  e.  V  ->  (D7ED; `  O ) : ~P O
 -1-1-onto-> ( { 0 ,  1 }  ^m  O ) )
 
14-Aug-2017indsum 23606 Finite sum of a product with the indicator function / cross-product with the indicator function. (Contributed by Thierry Arnoux, 14-Aug-2017.)
 |-  ( ph  ->  O  e.  Fin )   &    |-  ( ph  ->  A  C_  O )   &    |-  ( ( ph  /\  x  e.  O ) 
 ->  B  e.  CC )   =>    |-  ( ph  ->  sum_ x  e.  O  ( ( ( (D7ED; `  O ) `  A ) `  x )  x.  B )  =  sum_ x  e.  A  B )
 
14-Aug-2017ind0 23603 Value of the indicator function where it is  0. (Contributed by Thierry Arnoux, 14-Aug-2017.)
 |-  (
 ( O  e.  V  /\  A  C_  O  /\  X  e.  ( O  \  A ) )  ->  ( ( (D7ED; `  O ) `  A ) `  X )  =  0
 )
 
14-Aug-2017ind1 23602 Value of the indicator function where it is  1. (Contributed by Thierry Arnoux, 14-Aug-2017.)
 |-  (
 ( O  e.  V  /\  A  C_  O  /\  X  e.  A )  ->  ( ( (D7ED; `  O ) `  A ) `  X )  =  1
 )
 
14-Aug-2017pr01ssre 23601 The range of the indicator function is a subset of  RR. (Contributed by Thierry Arnoux, 14-Aug-2017.)
 |-  { 0 ,  1 }  C_  RR
 
13-Aug-2017usgraex3elv 28131 Lemma 3 for usgraexmpl 28133. (Contributed by Alexander van der Vekens, 13-Aug-2017.)
 |-  V  =  ( 0 ... 4
 )   =>    |-  3  e.  V
 
13-Aug-2017usgraex2elv 28130 Lemma 2 for usgraexmpl 28133. (Contributed by Alexander van der Vekens, 13-Aug-2017.)
 |-  V  =  ( 0 ... 4
 )   =>    |-  2  e.  V
 
13-Aug-2017usgraex1elv 28129 Lemma 1 for usgraexmpl 28133. (Contributed by Alexander van der Vekens, 13-Aug-2017.)
 |-  V  =  ( 0 ... 4
 )   =>    |-  1  e.  V
 
13-Aug-2017usgraex0elv 28128 Lemma 0 for usgraexmpl 28133. (Contributed by Alexander van der Vekens, 13-Aug-2017.)
 |-  V  =  ( 0 ... 4
 )   =>    |-  0  e.  V
 
13-Aug-2017usgraexvlem 28127 Lemma for usgraexmpl 28133. (Contributed by Alexander van der Vekens, 13-Aug-2017.)
 |-  V  =  ( 0 ... 4
 )   =>    |-  V  =  ( {
 0 ,  1 ,  2 }  u.  {
 3 ,  4 } )
 
13-Aug-2017usgraf0 28107 The edge function of an undirected simple graph without loops is a one to one function into unordered pairs of vertices. (Contributed by Alexander van der Vekens, 13-Aug-2017.)
 |-  ( V USGrph  E  ->  E : dom  E -1-1-> { x  e.  ~P V  |  ( # `  x )  =  2 }
 )
 
13-Aug-2017isusgra0 28106 The property of being an undirected simple graph without loops. (Contributed by Alexander van der Vekens, 13-Aug-2017.)
 |-  (
 ( V  e.  W  /\  E  e.  X ) 
 ->  ( V USGrph  E  <->  E : dom  E -1-1-> { x  e.  ~P V  |  ( # `  x )  =  2 }
 ) )
 
13-Aug-2017prelpw 28074 A pair of elements of a set is an element of the set's power set. (Contributed by Alexander van der Vekens, 13-Aug-2017.)
 |-  (
 ( A  e.  V  /\  B  e.  V ) 
 ->  ( P  =  { A ,  B }  ->  P  e.  ~P V ) )
 
13-Aug-2017prneimg 28073 Two pairs are not equal if one element of the first pair is not contained in the second pair. (Contributed by Alexander van der Vekens, 13-Aug-2017.)
 |-  (
 ( ( A  e.  U  /\  B  e.  V )  /\  ( C  e.  X  /\  D  e.  Y ) )  ->  ( ( ( A  =/=  C  /\  A  =/=  D )  \/  ( B  =/=  C 
 /\  B  =/=  D ) )  ->  { A ,  B }  =/=  { C ,  D }
 ) )
 
13-Aug-2017indfval 23600 Value of the indicator function. (Contributed by Thierry Arnoux, 13-Aug-2017.)
 |-  (
 ( O  e.  V  /\  A  C_  O  /\  X  e.  O )  ->  ( ( (D7ED; `  O ) `  A ) `  X )  =  if ( X  e.  A ,  1 ,  0 ) )
 
13-Aug-2017indf 23599 An indicator function as a function with domain and codomain. (Contributed by Thierry Arnoux, 13-Aug-2017.)
 |-  (
 ( O  e.  V  /\  A  C_  O )  ->  ( (D7ED; `  O ) `  A ) : O --> { 0 ,  1 } )
 
13-Aug-2017spnfw 1640 Weak version of sp 1716. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 1-Aug-2017.) (Proof shortened by Wolf Lammen, 13-Aug-2017.)
 |-  ( -.  ph  ->  A. x  -.  ph )   =>    |-  ( A. x ph  ->  ph )
 
12-Aug-2017ax12b 1655 Two equivalent ways of expressing ax-12 1866. See the comment for ax-12 1866. (Contributed by NM, 2-May-2017.) (Proof shortened by Wolf Lammen, 12-Aug-2017.)
 |-  ( ( -.  x  =  y  ->  ( y  =  z  ->  A. x  y  =  z )
 ) 
 <->  ( -.  x  =  y  ->  ( -.  x  =  z  ->  ( y  =  z  ->  A. x  y  =  z ) ) ) )
 
11-Aug-2017usgraedg2 28121 The value of the "edge function" of a graph is a set containing two elements (the vertices the corresponding edge is connecting), analogous to umgrale 23873. (Contributed by Alexander van der Vekens, 11-Aug-2017.)
 |-  (
 ( V USGrph  E  /\  X  e.  dom  E ) 
 ->  ( # `  ( E `  X ) )  =  2 )
 
11-Aug-2017usgraeq12d 28111 Equality of simple graphs without loops. (Contributed by Alexander van der Vekens, 11-Aug-2017.)
 |-  (
 ( ( V  e.  X  /\  E  e.  Y )  /\  ( V  =  W  /\  E  =  F ) )  ->  ( V USGrph  E 
 <->  W USGrph  F ) )
 
10-Aug-2017uslgraun 28120 If  <. V ,  E >. and  <. V ,  F >. are (simple) graphs (with loops), then  <. V ,  E  u.  F >. is a multigraph (the vertex set stays the same, but the edges from both graphs are kept, maybe resulting incident two edges between two vertices), analogous to umgraun 23879. (Contributed by Alexander van der Vekens, 10-Aug-2017.)
 |-  ( ph  ->  E  Fn  A )   &    |-  ( ph  ->  F  Fn  B )   &    |-  ( ph  ->  ( A  i^i  B )  =  (/) )   &    |-  ( ph  ->  V USLGrph  E )   &    |-  ( ph  ->  V USLGrph  F )   =>    |-  ( ph  ->  V UMGrph  ( E  u.  F ) )
 
10-Aug-2017usgra1 28119 The graph with one edge, analogous to umgra1 23878 ( with additional assumption that  B  =/=  C since otherwise the edge is a loop!). (Contributed by Alexander van der Vekens, 10-Aug-2017.)
 |-  (
 ( ( V  e.  W  /\  A  e.  X )  /\  ( B  e.  V  /\  C  e.  V ) )  ->  ( B  =/=  C  ->  V USGrph  {
 <. A ,  { B ,  C } >. } )
 )
 
10-Aug-2017uslgra1 28118 The graph with one edge, analogous to umgra1 23878. (Contributed by Alexander van der Vekens, 10-Aug-2017.)
 |-  (
 ( ( V  e.  W  /\  A  e.  X )  /\  ( B  e.  V  /\  C  e.  V ) )  ->  V USLGrph  { <. A ,  { B ,  C } >. } )
 
10-Aug-2017usgra0 28116 The empty graph, with vertices but no edges, is a graph, analogous to umgra0 23877. (Contributed by Alexander van der Vekens, 10-Aug-2017.)
 |-  ( V  e.  W  ->  V USGrph  (/) )
 
10-Aug-2017usgrares 28115 A subgraph of a graph (formed by removing some edges from the original graph) is a graph, analogous to umgrares 23876. (Contributed by Alexander van der Vekens, 10-Aug-2017.)
 |-  ( V USGrph  E  ->  V USGrph  ( E  |`  A ) )
 
10-Aug-2017usisuslgra 28113 An undirected simple graph without loops is an undirected simple graph with loops. (Contributed by Alexander van der Vekens, 10-Aug-2017.)
 |-  ( V USGrph  E  ->  V USLGrph  E )
 
10-Aug-2017uslisumgra 28112 An undirected simple graph with loops is an undirected multigraph. (Contributed by Alexander van der Vekens, 10-Aug-2017.)
 |-  ( V USLGrph  E  ->  V UMGrph  E )
 
10-Aug-2017usgraf 28105 The edge function of an undirected simple graph without loops is a one to one function into unordered pairs of vertices. (Contributed by Alexander van der Vekens, 10-Aug-2017.)
 |-  ( V USGrph  E  ->  E : dom  E -1-1-> { x  e.  ( ~P V  \  { (/) } )  |  ( # `  x )  =  2 }
 )
 
10-Aug-2017uslgraf 28104 The edge function of an undirected simple graph with loops is a one to one function into unordered pairs of vertices. (Contributed by Alexander van der Vekens, 10-Aug-2017.)
 |-  ( V USLGrph  E  ->  E : dom  E -1-1-> { x  e.  ( ~P V  \  { (/) } )  |  ( # `  x )  <_  2 } )
 
10-Aug-2017isusgra 28103 The property of being an undirected simple graph without loops. (Contributed by Alexander van der Vekens, 10-Aug-2017.)
 |-  (
 ( V  e.  W  /\  E  e.  X ) 
 ->  ( V USGrph  E  <->  E : dom  E -1-1-> { x  e.  ( ~P V  \  { (/) } )  |  ( # `  x )  =  2 }
 ) )
 
10-Aug-2017isuslgra 28102 The property of being an undirected simple graph with loops. (Contributed by Alexander van der Vekens, 10-Aug-2017.)
 |-  (
 ( V  e.  W  /\  E  e.  X ) 
 ->  ( V USLGrph  E  <->  E : dom  E -1-1-> { x  e.  ( ~P V  \  { (/) } )  |  ( # `  x )  <_  2 } )
 )
 
10-Aug-2017relusgra 28099 The class of all undirected simple graph without loops is a relation. (Contributed by Alexander van der Vekens, 10-Aug-2017.)
 |-  Rel USGrph
 
10-Aug-2017reluslgra 28098 The class of all undirected simple graph with loops is a relation. (Contributed by Alexander van der Vekens, 10-Aug-2017.)
 |-  Rel USLGrph
 
10-Aug-2017df-usgra 28097 Define the class of all undirected simple graphs without loops. An undirected simple graph without loops is a special undirected simple graph  <. V ,  E >. where 
E is an injective (one-to-one) function into subsets of  V of cardinality two, representing the two vertices incident to the edge. Such graphs are usually simply called "undirected graphs", so if only the term "undirected graph" is used, an undirected simple graph without loops is meant. Therefore, an undirected graph has no loops (edges a vertex to itsself). (Contributed by Alexander van der Vekens, 10-Aug-2017.)
 |- USGrph  =  { <. v ,  e >.  |  e : dom  e -1-1-> { x  e.  ( ~P v  \  { (/) } )  |  ( # `  x )  =  2 } }
 
10-Aug-2017df-uslgra 28096 Define the class of all undirected simple graphs with loops. An undirected simple graph with loops is a special undirected multigraph  <. V ,  E >. where  E is an injective (one-to-one) function into subsets of  V of cardinality one or two, representing the two vertices incident to the edge, or the one vertex if the edge is a loop. In contrast to a multigraph, there is at most one edge between two vertices. (Contributed by Alexander van der Vekens, 10-Aug-2017.)
 |- USLGrph  =  { <. v ,  e >.  |  e : dom  e -1-1-> { x  e.  ( ~P v  \  { (/) } )  |  ( # `  x )  <_  2 } }
 
7-Aug-2017iocinif 23274 Relate intersection of two opened below, closed above intervals with the same upper bound with a conditional construct. (Contributed by Thierry Arnoux, 7-Aug-2017.)
 |-  (
 ( A  e.  RR*  /\  B  e.  RR*  /\  C  e.  RR* )  ->  (
 ( A (,] C )  i^i  ( B (,] C ) )  =  if ( A  <  B ,  ( B (,] C ) ,  ( A (,] C ) ) )
 
7-Aug-2017iocinioc2 23272 Intersection between two opened below, closed above intervals sharing the same upper bound. (Contributed by Thierry Arnoux, 7-Aug-2017.)
 |-  (
 ( ( A  e.  RR*  /\  B  e.  RR*  /\  C  e.  RR* )  /\  A  <_  B )  ->  (
 ( A (,] C )  i^i  ( B (,] C ) )  =  ( B (,] C ) )
 
7-Aug-2017incexc2 12297 The inclusion/exclusion principle for counting the elements of a finite union of finite sets. (Contributed by Mario Carneiro, 7-Aug-2017.)
 |-  ( ( A  e.  Fin  /\  A  C_  Fin )  ->  ( # `  U. A )  =  sum_ n  e.  ( 1 ... ( # `
  A ) ) ( ( -u 1 ^ ( n  -  1 ) )  x. 
 sum_ s  e.  { k  e.  ~P A  |  ( # `  k )  =  n }  ( # ` 
 |^| s ) ) )
 
7-Aug-2017incexc 12296 The inclusion/exclusion principle for counting the elements of a finite union of finite sets. (Contributed by Mario Carneiro, 7-Aug-2017.)
 |-  ( ( A  e.  Fin  /\  A  C_  Fin )  ->  ( # `  U. A )  =  sum_ s  e.  ( ~P A  \  { (/) } ) ( ( -u 1 ^ (
 ( # `  s )  -  1 ) )  x.  ( # `  |^| s
 ) ) )
 
7-Aug-2017incexclem 12295 Lemma for incexc 12296. (Contributed by Mario Carneiro, 7-Aug-2017.)
 |-  ( ( A  e.  Fin  /\  B  e.  Fin )  ->  ( ( # `  B )  -  ( # `  ( B  i^i  U. A ) ) )  =  sum_ s  e.  ~P  A ( (
 -u 1 ^ ( # `
  s ) )  x.  ( # `  ( B  i^i  |^| s ) ) ) )
 
7-Aug-2017spimw 1638 Specialization. Lemma 8 of [KalishMontague] p. 87. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 19-Apr-2017.) (Proof shortened by Wolf Lammen, 7-Aug-2017.)
 |-  ( -.  ps  ->  A. x  -.  ps )   &    |-  ( x  =  y  ->  (
 ph  ->  ps ) )   =>    |-  ( A. x ph 
 ->  ps )
 
7-Aug-2017spimfw 1627 Specialization, with additional weakening to allow bundling of  x and  y. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 23-Apr-1017.) (Proof shortened by Wolf Lammen, 7-Aug-2017.)
 |-  ( -.  ps  ->  A. x  -.  ps )   &    |-  ( x  =  y  ->  (
 ph  ->  ps ) )   =>    |-  ( -.  A. x  -.  x  =  y 
 ->  ( A. x ph  ->  ps ) )
 
6-Aug-2017hashun3 11366 The size of the union of finite sets is the sum of their sizes minus the size of the intersection. (Contributed by Mario Carneiro, 6-Aug-2017.)
 |-  ( ( A  e.  Fin  /\  B  e.  Fin )  ->  ( # `  ( A  u.  B ) )  =  ( ( ( # `  A )  +  ( # `  B ) )  -  ( # `  ( A  i^i  B ) ) ) )
 
5-Aug-2017speimfw 1626 Specialization, with additional weakening to allow bundling of  x and  y. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 23-Apr-2017.) (Proof shortened by Wolf Lammen, 5-Aug-2017.)
 |-  ( x  =  y 
 ->  ( ph  ->  ps )
 )   =>    |-  ( -.  A. x  -.  x  =  y  ->  ( A. x ph  ->  E. x ps )
 )
 
4-Aug-2017lmdvg 23376 If a monotonic sequence of real numbers diverges, it is unbounded. (Contributed by Thierry Arnoux, 4-Aug-2017.)
 |-  ( ph  ->  F : NN --> ( 0 [,)  +oo ) )   &    |-  ( ( ph  /\  k  e.  NN )  ->  ( F `  k
 )  <_  ( F `  ( k  +  1 ) ) )   &    |-  ( ph  ->  -.  F  e.  dom  ~~>  )   =>    |-  ( ph  ->  A. x  e.  RR  E. j  e. 
 NN  A. k  e.  ( ZZ>=
 `  j ) x  <  ( F `  k ) )
 
4-Aug-2017fzssnn 23276 Finite sets of sequential integers starting from a natural are a subset of the natural numbers. (Contributed by Thierry Arnoux, 4-Aug-2017.)
 |-  ( M  e.  NN  ->  ( M ... N ) 
 C_  NN )
 
4-Aug-2017equequ2 1649 An equivalence law for equality. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 4-Aug-2017.)
 |-  ( x  =  y 
 ->  ( z  =  x  <-> 
 z  =  y ) )
 
3-Aug-2017dvreacos 24924 Real derivative of arccosine. (Contributed by Brendan Leahy, 3-Aug-2017.)
 |-  ( RR  _D  (arccos  |`  ( -u 1 (,) 1 ) ) )  =  ( x  e.  ( -u 1 (,) 1 )  |->  ( -u 1  /  ( sqr `  (
 1  -  ( x ^ 2 ) ) ) ) )
 
3-Aug-2017dvreasin 24923 Real derivative of arcsine. (Contributed by Brendan Leahy, 3-Aug-2017.)
 |-  ( RR  _D  (arcsin  |`  ( -u 1 (,) 1 ) ) )  =  ( x  e.  ( -u 1 (,) 1 )  |->  ( 1 
 /  ( sqr `  (
 1  -  ( x ^ 2 ) ) ) ) )
 
3-Aug-2017lmdvglim 23377 If a monotonic real number sequence 
F diverges, it converges in the extended real numbers and its limit is plus infinity. (Contributed by Thierry Arnoux, 3-Aug-2017.)
 |-  J  =  ( TopOpen `  ( RR* ss  ( 0 [,]  +oo ) ) )   &    |-  ( ph  ->  F : NN
 --> ( 0 [,)  +oo ) )   &    |-  ( ( ph  /\  k  e.  NN )  ->  ( F `  k
 )  <_  ( F `  ( k  +  1 ) ) )   &    |-  ( ph  ->  -.  F  e.  dom  ~~>  )   =>    |-  ( ph  ->  F (
 ~~> t `  J ) 
 +oo )
 
3-Aug-2017a9ev 1637 At least one individual exists. Weaker version of a9e 1891. When possible, use of this theorem rather than a9e 1891 is preferred since its derivation from axioms is much shorter. (Contributed by NM, 3-Aug-2017.)
 |- 
 E. x  x  =  y
 
2-Aug-2017ralbinrald 27977 Elemination of a restricted universal quantification under certain conditions. (Contributed by Alexander van der Vekens, 2-Aug-2017.)
 |-  ( ph  ->  X  e.  A )   &    |-  ( x  e.  A  ->  x  =  X )   &    |-  ( x  =  X  ->  ( ps  <->  th ) )   =>    |-  ( ph  ->  (
 A. x  e.  A  ps 
 <-> 
 th ) )
 
2-Aug-2017lmxrge0 23375 Express "sequence  F converges to plus infinity" (i.e. diverges), for a sequence of non-negative extended real numbers. (Contributed by Thierry Arnoux, 2-Aug-2017.)
 |-  J  =  ( TopOpen `  ( RR* ss  ( 0 [,]  +oo ) ) )   &    |-  ( ph  ->  F : NN
 --> ( 0 [,]  +oo ) )   &    |-  ( ( ph  /\  k  e.  NN )  ->  ( F `  k
 )  =  A )   =>    |-  ( ph  ->  ( F (
 ~~> t `  J ) 
 +oo 
 <-> 
 A. x  e.  RR  E. j  e.  NN  A. k  e.  ( ZZ>= `  j ) x  <  A ) )
 
2-Aug-201719.2 1671 Theorem 19.2 of [Margaris] p. 89. Note: This proof is very different from Margaris' because we only have Tarski's FOL axiom schemes available at this point. See the later 19.2g 1780 for a more conventional proof. (Contributed by NM, 2-Aug-2017.)
 |-  ( A. x ph  ->  E. x ph )
 
1-Aug-2017xrdifh 23273 Set difference of a half-opened interval in the extended reals. (Contributed by Thierry Arnoux, 1-Aug-2017.)
 |-  A  e.  RR*   =>    |-  ( RR*  \  ( A [,]  +oo ) )  =  (  -oo [,) A )
 
1-Aug-2017dvelimhw 1735 Proof of dvelimh 1904 without using ax-12 1866 but with additional distinct variable conditions. (Contributed by Andrew Salmon, 21-Jul-2011.) (Revised by NM, 1-Aug-2017.)
 |-  ( ph  ->  A. x ph )   &    |-  ( ps  ->  A. z ps )   &    |-  (
 z  =  y  ->  ( ph  <->  ps ) )   &    |-  ( -.  A. x  x  =  y  ->  ( y  =  z  ->  A. x  y  =  z )
 )   =>    |-  ( -.  A. x  x  =  y  ->  ( ps  ->  A. x ps ) )
 
1-Aug-201719.21h 1731 Theorem 19.21 of [Margaris] p. 90. The hypothesis can be thought of as " x is not free in  ph." (Contributed by NM, 1-Aug-2017.)
 |-  ( ph  ->  A. x ph )   =>    |-  ( A. x (
 ph  ->  ps )  <->  ( ph  ->  A. x ps ) )
 
1-Aug-201719.9v 1663 Special case of Theorem 19.9 of [Margaris] p. 89. (Contributed by NM, 28-May-1995.) (Revised by NM, 1-Aug-2017.)
 |-  ( E. x ph  <->  ph )
 
1-Aug-201719.3v 1662 Special case of Theorem 19.3 of [Margaris] p. 89. (Contributed by NM, 1-Aug-2017.)
 |-  ( A. x ph  <->  ph )
 
1-Aug-201719.8w 1659 Weak version of 19.8a 1718. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 1-Aug-2017.)
 |-  ( ph  ->  A. x ph )   =>    |-  ( ph  ->  E. x ph )
 
1-Aug-2017spnfwOLD 1658 Weak version of sp 1716. Uses only Tarski's FOL axiom schemes. Obsolete version of spnfw 1640 as of 13-Aug-2017. (Contributed by NM, 1-Aug-2017.) (New usage is discouraged.)
 |-  ( -.  ph  ->  A. x  -.  ph )   =>    |-  ( A. x ph  ->  ph )
 
31-Jul-2017esumpcvgval 23446 The value of the extended sum when the corresponding series sum is convergent. (Contributed by Thierry Arnoux, 31-Jul-2017.)
 |-  (
 ( ph  /\  k  e. 
 NN )  ->  A  e.  ( 0 [,)  +oo ) )   &    |-  ( k  =  l  ->  A  =  B )   &    |-  ( ph  ->  ( n  e.  NN  |->  sum_ k  e.  ( 1 ... n ) A )  e.  dom  ~~>  )   =>    |-  ( ph  -> Σ* k  e.  NN A  =  sum_ k  e. 
 NN  A )
 
31-Jul-2017pnfneige0 23374 A neighborhood of  +oo contains an unbounded interval based at a real number. See pnfnei 16950 (Contributed by Thierry Arnoux, 31-Jul-2017.)
 |-  J  =  ( TopOpen `  ( RR* ss  ( 0 [,]  +oo ) ) )   =>    |-  ( ( A  e.  J  /\  +oo  e.  A )  ->  E. x  e.  RR  ( x (,]  +oo )  C_  A )
 
28-Jul-2017tz6.12-afv 28035 Function value (Theorem 6.12(1) of [TakeutiZaring] p. 27, , analogous to tz6.12-1 5544, but it is required for A to be a set. (Contributed by Alexander van der Vekens, 28-Jul-2017.)
 |-  ( A  e.  V  ->  ( ( A F y 
 /\  E! y  A F y )  ->  ( F''' A )  =  y
 ) )
 
28-Jul-2017rge0scvg 23373 Implication of convergence for a non-negative series. This could be used to shorten prmreclem6 12968 (Contributed by Thierry Arnoux, 28-Jul-2017.)
 |-  (
 ( F : NN --> ( 0 [,)  +oo )  /\  seq  1 (  +  ,  F )  e.  dom  ~~>  )  ->  sup ( ran  seq  1 (  +  ,  F ) ,  RR ,  <  )  e.  RR )
 
26-Jul-2017xrge0haus 23326 The topology of the extended non-negative real numbers is Hausdorf. (Contributed by Thierry Arnoux, 26-Jul-2017.)
 |-  ( TopOpen `  ( RR* ss  ( 0 [,]  +oo ) ) )  e. 
 Haus
 
25-Jul-2017funressnfv 27991 A restriction to a singleton with a function value is a function under certain conditions. (Contributed by Alexander van der Vekens, 25-Jul-2017.)
 |-  (
 ( ( X  e.  dom  ( F  o.  G )  /\  Fun  ( ( F  o.  G )  |`  { X } ) ) 
 /\  ( G  Fn  A  /\  X  e.  A ) )  ->  Fun  ( F  |`  { ( G `
  X ) }
 ) )
 
25-Jul-2017funcoressn 27990 A composition restricted to a singleton is a function under certain conditions. (Contributed by Alexander van der Vekens, 25-Jul-2017.)
 |-  (
 ( ( ( G `
  X )  e. 
 dom  F  /\  Fun  ( F  |`  { ( G `
  X ) }
 ) )  /\  ( G  Fn  A  /\  X  e.  A ) )  ->  Fun  ( ( F  o.  G )  |`  { X } ) )
 
25-Jul-2017fnresfnco 27989 Composition of two functions, similar to fnco 5352. (Contributed by Alexander van der Vekens, 25-Jul-2017.)
 |-  (
 ( ( F  |`  ran  G )  Fn  ran  G  /\  G  Fn  B )  ->  ( F  o.  G )  Fn  B )
 
25-Jul-2017funresfunco 27988 Composition of two functions, generalization of funco 5292. (Contributed by Alexander van der Vekens, 25-Jul-2017.)
 |-  (
 ( Fun  ( F  |` 
 ran  G )  /\  Fun  G )  ->  Fun  ( F  o.  G ) )
 
23-Jul-2017afvco2 28037 Value of a function composition, analogous to fvco2 5594. (Contributed by Alexander van der Vekens, 23-Jul-2017.)
 |-  (
 ( G  Fn  A  /\  X  e.  A ) 
 ->  ( ( F  o.  G )''' X )  =  ( F''' ( G''' X ) ) )
 
23-Jul-2017dmfcoafv 28036 Domains of a function composition, analogous to dmfco 5593. (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 ) )
 
23-Jul-2017csbafv12g 28000 Move class substitution in and out of a function value, analogous to csbfv12g 5535, with a direct proof proposed by Mario Carneiro, analogous to csbovg 5889. (Contributed by Alexander van der Vekens, 23-Jul-2017.)
 |-  ( A  e.  V  ->  [_ A  /  x ]_ ( F''' B )  =  (
 [_ A  /  x ]_ F''' [_ A  /  x ]_ B ) )
 
23-Jul-2017sbcfun 27985 Distribute proper substitution through the function predicate. (Contributed by Alexander van der Vekens, 23-Jul-2017.)
 |-  ( A  e.  V  ->  (
 [. A  /  x ].
 Fun  F  <->  Fun  [_ A  /  x ]_ F ) )
 
23-Jul-2017csbdmg 27980 Distribute proper substitution through the domain of a class. (Contributed by Alexander van der Vekens, 23-Jul-2017.)
 |-  ( A  e.  V  ->  [_ A  /  x ]_ dom  B  =  dom  [_ A  /  x ]_ B )
 
23-Jul-2017sbcrel 27979 Distribute proper substitution through a relation predicate. (Contributed by Alexander van der Vekens, 23-Jul-2017.)
 |-  ( A  e.  V  ->  (
 [. A  /  x ].
 Rel  R  <->  Rel  [_ A  /  x ]_ R ) )
 
23-Jul-2017sbcss 3564 Distribute proper substitution through a subclass relation. (Contributed by Alan Sare, 22-Jul-2012.) (Proof shortened by Alexander van der Vekens, 23-Jul-2017.)
 |-  ( A  e.  B  ->  ( [. A  /  x ]. C  C_  D  <->  [_ A  /  x ]_ C  C_  [_ A  /  x ]_ D ) )
 
22-Jul-2017afvres 28034 The value of a restricted function, analogous to fvres 5542. (Contributed by Alexander van der Vekens, 22-Jul-2017.)
 |-  ( A  e.  B  ->  ( ( F  |`  B )''' A )  =  ( F''' A ) )
 
22-Jul-2017afveq2 27998 Equality theorem for function value, analogous to fveq1 5524. (Contributed by Alexander van der Vekens, 22-Jul-2017.)
 |-  ( A  =  B  ->  ( F''' A )  =  ( F''' B ) )
 
22-Jul-2017afveq1 27997 Equality theorem for function value, analogous to fveq1 5524. (Contributed by Alexander van der Vekens, 22-Jul-2017.)
 |-  ( F  =  G  ->  ( F''' A )  =  ( G''' A ) )
 
22-Jul-2017dfafv2 27995 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 )
 
22-Jul-2017dfdfat2 27994 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 ) )
 
22-Jul-2017logbid1 23400 General logarithm when base and arg match (Contributed by David A. Wheeler, 22-Jul-2017.)
 |-  (
 ( A  e.  CC  /\  A  =/=  0  /\  A  =/=  1 )  ->  ( Alogb A )  =  1 )
 
22-Jul-2017logeq0im1 23396 if  ( log `  A )  =  0 then 
A  =  1 (Contributed by David A. Wheeler, 22-Jul-2017.)
 |-  (
 ( A  e.  CC  /\  A  =/=  0  /\  ( log `  A )  =  0 )  ->  A  =  1 )
 
22-Jul-2017eldiftp 23395 Membership in a set with three elements removed. Similar to eldifsn 3749 and eldifpr 23394. (Contributed by David A. Wheeler, 22-Jul-2017.)
 |-  ( A  e.  ( B  \  { C ,  D ,  E } )  <->  ( A  e.  B  /\  ( A  =/=  C 
 /\  A  =/=  D  /\  A  =/=  E ) ) )
 
18-Jul-2017eldifpr 23394 Membership in a set with two elements removed. Similar to eldifsn 3749 and eldiftp 23395. (Contributed by Mario Carneiro, 18-Jul-2017.)
 |-  ( A  e.  ( B  \  { C ,  D } )  <->  ( A  e.  B  /\  A  =/=  C  /\  A  =/=  D ) )
 
17-Jul-2017logbcl 23399 General logarithm closure. (Contributed by David A. Wheeler, 17-Jul-2017.)
 |-  (
 ( B  e.  ( CC  \  { 0 ,  1 } )  /\  X  e.  ( CC  \  { 0 } )
 )  ->  ( Blogb X )  e.  CC )
 
17-Jul-2017logccne0ALT 23398 log isn't 0 if argument isn't 0 or 1. Unlike logne0 19956, this handles complex numbers. (Contributed by David A. Wheeler, 17-Jul-2017.)
 |-  (
 ( A  e.  CC  /\  A  =/=  0  /\  A  =/=  1 )  ->  ( log `  A )  =/=  0 )
 
17-Jul-2017logccne0 23397 log isn't 0 if argument isn't 0 or 1. Unlike logne0 19956, this handles complex numbers. (Contributed by David A. Wheeler, 17-Jul-2017.)
 |-  (
 ( A  e.  CC  /\  A  =/=  0  /\  A  =/=  1 )  ->  ( log `  A )  =/=  0 )
 
16-Jul-2017logb2aval 23393 Define the value of the logb function, the logarithm generalized to an arbitrary base, when used in the 2-argument form logb <. B ,  X >. (Contributed by David A. Wheeler, 21-Jan-2017.) (Revised by David A. Wheeler, 16-Jul-2017.)
 |-  (
 ( B  e.  ( CC  \  { 0 ,  1 } )  /\  X  e.  ( CC  \  { 0 } )
 )  ->  (logb `  <. B ,  X >. )  =  ( ( log `  X )  /  ( log `  B ) ) )
 
16-Jul-2017logbval 23392 Define the value of the logb function, the logarithm generalized to an arbitrary base, when used as infix. Most Metamath statements select variables in order of their use, but to make the order clearer we use "B" for base and "X" for the other operand here. Proof is similar to modval 10975. (Contributed by David A. Wheeler, 21-Jan-2017.) (Revised by David A. Wheeler, 16-Jul-2017.)
 |-  (
 ( B  e.  ( CC  \  { 0 ,  1 } )  /\  X  e.  ( CC  \  { 0 } )
 )  ->  ( Blogb X )  =  ( ( log `  X )  /  ( log `  B ) ) )
 
16-Jul-2017prmz 12762 A prime number is an integer. (Contributed by Paul Chapman, 22-Jun-2011.) (Proof shortened by Jonathan Yan, 16-Jul-2017.)
 |-  ( P  e.  Prime  ->  P  e.  ZZ )
 
14-Jul-2017df-log_ 28258 Define the log_ operator. This is the logarithm generalized to an arbitrary base. It can be used as  ( (log_ `  B ) `  X ) for "log base B of X". This formulation suggested by Mario Carneiro. (Contributed by David A. Wheeler, 14-Jul-2017.)
 |- log_  =  ( b  e.  ( CC  \  { 0 ,  1 } )  |->  ( x  e.  ( CC  \  { 0 } )  |->  ( ( log `  x )  /  ( log `  b
 ) ) ) )
 
11-Jul-2017dstfrvclim1 23678 The limit of the cumulative distribution function is one. (Contributed by Thierry Arnoux, 12-Feb-2017.) (Revised by Thierry Arnoux, 11-Jul-2017.)
 |-  ( ph  ->  P  e. Prob )   &    |-  ( ph  ->  X  e.  (rRndVar `  P ) )   &    |-  ( ph  ->  F  =  ( x  e.  RR  |->  ( P `  ( XRV/𝑐  <_  x ) ) ) )   =>    |-  ( ph  ->  F  ~~>  1 )
 
11-Jul-2017meascnbl 23546 A measure is continuous from below. Cf. volsup 18913. (Contributed by Thierry Arnoux, 18-Jan-2017.) (Revised by Thierry Arnoux, 11-Jul-2017.)
 |-  J  =  ( TopOpen `  ( RR* ss  ( 0 [,]  +oo ) ) )   &    |-  ( ph  ->  M  e.  (measures `  S ) )   &    |-  ( ph  ->  F : NN
 --> S )   &    |-  ( ( ph  /\  n  e.  NN )  ->  ( F `  n )  C_  ( F `  ( n  +  1
 ) ) )   =>    |-  ( ph  ->  ( M  o.  F ) ( ~~> t `  J ) ( M `  U.
 ran  F ) )
 
11-Jul-2017lmlimxrge0 23372 Relate a limit in the non-negative extended reals to a complex limit, provided the considered function is a real function. (Contributed by Thierry Arnoux, 11-Jul-2017.)
 |-  J  =  ( TopOpen `  ( RR* ss  ( 0 [,]  +oo ) ) )   &    |-  ( ph  ->  F : NN
 --> X )   &    |-  ( ph  ->  P  e.  X )   &    |-  X  C_  ( 0 [,)  +oo )   =>    |-  ( ph  ->  ( F ( ~~> t `  J ) P  <->  F  ~~>  P ) )
 
11-Jul-2017lmlim 23371 Relate a limit in a given topology to a complex number limit, provided that topology agrees with the common topology on  CC on the required subset. (Contributed by Thierry Arnoux, 11-Jul-2017.)
 |-  J  e.  (TopOn `  Y )   &    |-  ( ph  ->  F : NN --> X )   &    |-  ( ph  ->  P  e.  X )   &    |-  ( Jt  X )  =  (
 ( TopOpen ` fld )t  X )   &    |-  X  C_  CC   =>    |-  ( ph  ->  ( F ( ~~> t `  J ) P  <->  F  ~~>  P ) )
 
6-Jul-2017esumdivc 23451 An extended sum divided by a constant. (Contributed by Thierry Arnoux, 6-Jul-2017.)
 |-  ( ph  ->  A  e.  V )   &    |-  ( ( ph  /\  k  e.  A )  ->  B  e.  ( 0 [,]  +oo ) )   &    |-  ( ph  ->  C  e.  RR+ )   =>    |-  ( ph  ->  (Σ* k  e.  A B /𝑒  C )  = Σ* k  e.  A ( B /𝑒  C )
 )
 
6-Jul-2017esummulc2 23450 An extended sum multiplied by a constant. (Contributed by Thierry Arnoux, 6-Jul-2017.)
 |-  ( ph  ->  A  e.  V )   &    |-  ( ( ph  /\  k  e.  A )  ->  B  e.  ( 0 [,]  +oo ) )   &    |-  ( ph  ->  C  e.  ( 0 [,)  +oo ) )   =>    |-  ( ph  ->  ( C x eΣ* k  e.  A B )  = Σ* k  e.  A ( C x e B ) )
 
6-Jul-2017esummulc1 23449 An extended sum multiplied by a constant. (Contributed by Thierry Arnoux, 6-Jul-2017.)
 |-  ( ph  ->  A  e.  V )   &    |-  ( ( ph  /\  k  e.  A )  ->  B  e.  ( 0 [,]  +oo ) )   &    |-  ( ph  ->  C  e.  ( 0 [,)  +oo ) )   =>    |-  ( ph  ->  (Σ* k  e.  A B x e C )  = Σ* k  e.  A ( B x e C ) )
 
6-Jul-2017xrge0addgt0 23331 The sum of nonnegative and positive numbers is positive. See addgtge0 9262 (Contributed by Thierry Arnoux, 6-Jul-2017.)
 |-  (
 ( ( A  e.  ( 0 [,]  +oo )  /\  B  e.  (
 0 [,]  +oo ) ) 
 /\  0  <  A )  ->  0  <  ( A + e B ) )
 
6-Jul-2017xrge0mulc1cn 23323 The operation multiplying a non-negative real numbers by a non-negative constant is continuous. (Contributed by Thierry Arnoux, 6-Jul-2017.)
 |-  J  =  ( (ordTop `  <_  )t  ( 0 [,]  +oo )
 )   &    |-  F  =  ( x  e.  ( 0 [,]  +oo )  |->  ( x x e C ) )   &    |-  ( ph  ->  C  e.  ( 0 [,)  +oo ) )   =>    |-  ( ph  ->  F  e.  ( J  Cn  J ) )
 
6-Jul-2017elicoelioo 23271 Relate elementhood to a closed-below, opened-above interval with elementhood to the same opened interval or to its lower bound. (Contributed by Thierry Arnoux, 6-Jul-2017.)
 |-  (
 ( A  e.  RR*  /\  B  e.  RR*  /\  A  <  B )  ->  ( C  e.  ( A [,) B )  <->  ( C  =  A  \/  C  e.  ( A (,) B ) ) ) )
 
5-Jul-2017esumcst 23436 The extended sum of a constant. (Contributed by Thierry Arnoux, 3-Mar-2017.) (Revised by Thierry Arnoux, 5-Jul-2017.)
 |-  F/_ k A   &    |-  F/_ k B   =>    |-  ( ( A  e.  V  /\  B  e.  (
 0 [,]  +oo ) ) 
 -> Σ* k  e.  A B  =  ( ( # `  A ) x e B ) )
 
5-Jul-2017ishashinf 23389 Any set that is not finite contains subsets of arbitrarily large finite cardinality. Cf. isinf 7076 (Contributed by Thierry Arnoux, 5-Jul-2017.)
 |-  ( -.  A  e.  Fin  ->  A. n  e.  NN  E. x  e.  ~P  A ( # `  x )  =  n )
 
5-Jul-2017gsumconstf 23381 Sum of a constant series (Contributed by Thierry Arnoux, 5-Jul-2017.)
 |-  F/_ k X   &    |-  B  =  ( Base `  G )   &    |-  .x.  =  (.g `  G )   =>    |-  ( ( G  e.  Mnd  /\  A  e.  Fin  /\  X  e.  B )  ->  ( G  gsumg  ( k  e.  A  |->  X ) )  =  ( ( # `  A )  .x.  X ) )
 
5-Jul-2017xrmulc1cn 23303 The operation multiplying an extended real number by a non-negative constant is continuous. (Contributed by Thierry Arnoux, 5-Jul-2017.)
 |-  J  =  (ordTop `  <_  )   &    |-  F  =  ( x  e.  RR*  |->  ( x x e C ) )   &    |-  ( ph  ->  C  e.  RR+ )   =>    |-  ( ph  ->  F  e.  ( J  Cn  J ) )
 
5-Jul-2017xeqlelt 23269 Equality in terms of 'less than or equal to', 'less than'. (Contributed by Thierry Arnoux, 5-Jul-2017.)
 |-  (
 ( A  e.  RR*  /\  B  e.  RR* )  ->  ( A  =  B  <->  ( A  <_  B  /\  -.  A  <  B ) ) )
 
5-Jul-2017xdivrec 23110 Relationship between division and reciprocal. (Contributed by Thierry Arnoux, 5-Jul-2017.)
 |-  (
 ( A  e.  RR*  /\  B  e.  RR  /\  B  =/=  0 )  ->  ( A /𝑒  B )  =  ( A x e ( 1 /𝑒 
 B ) ) )
 
3-Jul-2017eliccelico 23270 Relate elementhood to a closed interval with elementhood to the same closed-below, opened-above interval or to its upper bound. (Contributed by Thierry Arnoux, 3-Jul-2017.)
 |-  (
 ( A  e.  RR*  /\  B  e.  RR*  /\  A  <_  B )  ->  ( C  e.  ( A [,] B )  <->  ( C  e.  ( A [,) B )  \/  C  =  B ) ) )
 
3-Jul-2017or3dir 23124 Distributive law for disjunction. (Contributed by Thierry Arnoux, 3-Jul-2017.)
 |-  (
 ( ( ph  /\  ps  /\ 
 ch )  \/  ta ) 
 <->  ( ( ph  \/  ta )  /\  ( ps 
 \/  ta )  /\  ( ch  \/  ta ) ) )
 
3-Jul-2017or3di 23123 Distributive law for disjunction. (Contributed by Thierry Arnoux, 3-Jul-2017.)
 |-  (
 ( ph  \/  ( ps  /\  ch  /\  ta ) )  <->  ( ( ph  \/  ps )  /\  ( ph  \/  ch )  /\  ( ph  \/  ta )
 ) )
 
2-Jul-2017eldmressnsn 27984 The element of the domain of a restriction to a singleton is the element of the singleton. (Contributed by Alexander van der Vekens, 2-Jul-2017.)
 |-  ( A  e.  dom  F  ->  A  e.  dom  ( F  |` 
 { A } )
 )
 
2-Jul-2017dmressnsn 27983 The domain of a restriction to a singleton is a singleton. (Contributed by Alexander van der Vekens, 2-Jul-2017.)
 |-  ( A  e.  dom  F  ->  dom  ( F  |`  { A } )  =  { A } )
 
2-Jul-2017eldmressn 27982 Element of the domain of a restriction to a singleton. (Contributed by Alexander van der Vekens, 2-Jul-2017.)
 |-  ( B  e.  dom  ( F  |`  { A } )  ->  B  =  A )
 
2-Jul-20172reu8 27970 Two equivalent expressions for double restricted existential uniqueness, analogous to 2eu8 2230. Curiously, we can put  E! on either of the internal conjuncts but not both. We can also commute  E! x  e.  A E! y  e.  B using 2reu7 27969. (Contributed by Alexander van der Vekens, 2-Jul-2017.)
 |-  ( E! x  e.  A  E! y  e.  B  ( E. x  e.  A  ph 
 /\  E. y  e.  B  ph )  <->  E! x  e.  A  E! y  e.  B  ( E! x  e.  A  ph 
 /\  E. y  e.  B  ph ) )